[pcshrosbree]

TL;DR: This draft adds ilverify --validation-only to check IL validity while skipping most checks that enforce only verifiability. In scans made before the rebase onto main, findings on the .NET 10 shared framework dropped from 84,235 to 954, with some valid IL still reported. Please review point 1 first: when checking values on the stack, should this mode also check their declared types?

#136133 has merged; this draft now contains one commit rebased onto main.

What changes

With ValidationOnly set, checks generally stay for correctness rules and are not reported for rules that only enforce verifiability (ECMA-335 III.1.8). A few verifiability checks remain (review point 7). ILVerify also approximates one correctness rule by keeping a stricter verification check (review point 5). These retained checks can report valid IL. The option is off by default. With it off, ILVerify keeps its existing verification checks.

The classification rule. Each Partition III instruction has a Correctness paragraph and a Verifiability paragraph. I classified each reporting site, not each error code, because codes such as StackUnexpected are used for both kinds of rule.

• A check stays if the instruction's Correctness paragraph, its Description, its stack diagram, or a validity rule of Partition I or II states the rule.
• A check is not reported if only a Verifiability paragraph, the verification algorithm of III.1.8.1, or a shaded cell of Tables III.2 to III.9 states it.
• Where the augments change a rule, the augments win. Where the spec is silent or ambiguous, the check stays.

A check that is not reported does not abort the basic block or the method, and the importer keeps a stack model after it. For example, ldind.ref through an unmanaged pointer pushes an object reference of unknown class. If ldelem.ref then uses that reference as its array operand, the importer pushes a null reference, as it does for a null array. The fix that keeps ldelem.ref from crashing on such an operand is #136159, which has merged, so this PR no longer contains it.

Type checks. Most checks that compare a value on the stack with a declared type compare only the stack types of I.12.3.2.1 (review point 1), with the exceptions below. The following checks still use declared types, not only stack types:

• comparing a delegate's target method with the delegate's Invoke signature (II.14.6);
• checking that the delegate constructor's own parameters are System.Object and native int (II.14.6).

A few checks of values also look past the stack type. The array instructions need a single-dimensional, zero-based array. A readonly & cannot be used where a writable & is expected, for example as the destination of initobj (III.1.8.1.2.2). Neither mode enforces this rule for the destination of cpobj; that existing gap remains. With SanityChecks set, thrown and caught types must be System.Object or derive from System.Exception.

Public surface.

• VerifierOptions.ValidationOnly (bool, default false), beside SanityChecks.
• ilverify --validation-only, also described in the README's usage section. In this mode the summary line and the --statistics lines say "validated" instead of "verified".

Tests. Every existing method test now also runs in validation-only mode. By default, it expects the same errors as in verification mode. A name suffix beginning with _Validation_ overrides the expected errors for validation-only mode (the format is described in the README). Type tests and the other tests run once. 61 existing test methods carry the suffix. A malformed suffix fails the tests instead of silently dropping the method. The new ValidationOnlyTests.il has 189 test methods: each reaches one check that is no longer reported, or one rule that is still reported.

Evidence

After the rebase onto main. With this PR rebased onto main commit b3c0988, ILVerification.Tests passes 1,448 of 1,448 in Release on linux-x64. The ParseExpectedError helper from #136135 accepts numeric error codes. I therefore removed the two suffix-parser tests that expected those codes to be rejected, leaving 5 parser tests. The parser now accepts those two numeric codes, but a method test expecting either code would still fail: no check reports it. I have not re-run the scans since this rebase, which brought in #136159, #136033 and #136176.

Earlier evidence (before the rebase onto main). Built and run on linux-x64, Release and Debug.

The scan figures below use the .NET 10.0.12 shared framework. They were measured before the rebase onto #136133's latest commit. That commit removed one calli check.

I checked the effect of that earlier rebase onto #136133's latest commit separately on .NET 10.0.13. Results were identical before and after that rebase in both modes. With the option off, the version rebased onto #136133 also matched #136133's new head.

• ILVerification.Tests: 1,407 of 1,407 pass in Release and in Debug (546 on ILVerify: continue checking methods that use calli, mkrefany, refanyval and refanytype instead of aborting them #136133's head). That is 665 method tests run in both modes, 66 type tests, 4 other tests, and 7 tests of the suffix parser.
• Mutation testing: I changed one guard at a time and ran the full suite.
  • A first pass of 317 mutants covered the classified sites, before I settled the decisions in review points 1 to 4. 311 failed at least one test. The 6 survivors are kept checks that ilasm cannot reach: a zero-size body, two fall-through checks that need a filter without its final endfilter, two handler entry-stack checks, and a by-ref catch type.
  • A second pass of 84 mutants covered every site those decisions added or changed. 83 failed at least one test. The survivor uses class-level assignability for the delegate constructor's object parameter. That check cannot fail for a well-formed delegate constructor, whose first parameter is System.Object; validation-only mode now checks that parameter directly (II.14.6).
  • A third pass of 14 mutants covered the sites I changed after that: the delegate constructor's method pointer, the closed delegate's target, tail calls and their return type, and the suffix parser. 13 failed at least one test at first; the last one did after I added a test for it.
  • A fourth pass of 7 mutants covered the value passed in a tail call and the delegate constructor's first parameter. All 7 failed at least one test.
  • A fifth pass of 7 mutants covered initobj through a readonly &, and readonly values at joins. All 7 failed at least one test.
  • I did not re-run the earlier passes on the final code. For sites that later changes did not touch, the tests that caught their mutants are still in the suite.
• With the option off, finding codes and offsets are identical to ILVerify: continue checking methods that use calli, mkrefany, refanyval and refanytype instead of aborting them #136133's head on every method of the shared framework (172 assemblies, 130,146 method bodies) and of the package corpora below. Package finding messages are also identical; the framework scan does not record messages.

Shared framework, with the option on. 954 findings in 952 methods, against 84,235 findings in 35,248 methods in verification mode. Of the 954 findings, 691 are in System.Private.CoreLib. The 954 findings fall into four groups, all from existing ILVerify behavior. Validation-only mode can expose more of them, because it reaches blocks that verification skips (review point 6):

Findings	CoreLib	What it is
862	625	BadTypeSpec: ILVerify rejects the TypeSpec Roslyn emits for unmanaged constraints (modreq(UnmanagedType) ValueType): #136142, which #136143 fixes. Verification mode reports it too.
57	51	MethodAccess on constrained calls to protected static abstract interface members (INumberBase<T>.TryConvertTo* in the generic-math Create* methods).
25	5	A readonly & returned where a writable & is expected (ImmutableArray<T>.ItemRef, frozen collections). ILVerify does not model ref readonly returns (#57444). Verification mode reports it too.
10	10	The return check on CoreLib's runtime-async AsyncHelpers.Await* methods.

302 of the 954 are at offsets where verification mode reports nothing (review point 6).

Packages. 388,490 method bodies from hand-written IL packages, packages built with InlineIL.Fody, the 300 most-downloaded nuget.org packages and saved dynamic proxies. Verification mode reports 39,774 findings in 20,884 methods, and validation-only mode 2,099 in 2,033. The largest groups are the same BadTypeSpec (1,473; #136142, fixed by #136143) and type or assembly load failures from my scan setup (388). The rest:

• 59 readonly & returns and 52 MethodAccess, as above.
• 48 object references where a generic parameter is expected, such as Unsafe.As<T>(object). ILVerify gives every generic parameter the value-type stack kind.
• 36 unbox of a struct-constrained T (ValueTypeExpected).
• 12 object references used as & and 9 native ints used as object references. These are stack-type mismatches in hand-written IL and Castle proxies, so they stay.
• 3 TailByRef in one InlineIL method (review point 5).
• 19 others, such as 3 where a pointer type is compared with native int.

Points for review

1. Most checks of values on the stack use only stack types. The exceptions are under Type checks and in point 5. When it checks a value on the stack in validation-only mode, ILVerify uses the stack types of I.12.3.2.1 (int32, int64, native int, F, O, &, and value types). It also accepts a native int where a & is expected (III.1.6). It does not check the class of an object reference, the type a pointer points to, an array's element type, or the exact type for mkrefany and constrained.. In validation-only mode, the .ref forms of ldind, stind, ldelem and stelem are treated as object-reference loads or stores regardless of the pointer's target type or the array's element type. I chose this reading because it follows [ILVerify] Add option for IL validation without IL verification #37391's words, "suppress all verification checks related to type safety". But the Correctness paragraphs of call, stind/stobj, mkrefany and ldfld do state class-level agreement, and I can switch to that literal reading. A scratch build using the literal reading adds:

   • 19 findings in 15 framework methods: 16 are ldind.i/stind.i through a T*&, where ILVerify compares T* with IntPtr, and 3 are constrained. calls in System.Net.Quic.
   • 69 findings in 65 package methods: 42 are in Unsafe.WriteUnaligned<T>(ref byte, T) in System.Runtime.CompilerServices.Unsafe, MonoMod.ILHelpers and DotNetCross.Memory.Unsafe.

2. A & passed where a native int or void* is expected. For arguments to call, callvirt, newobj and calli, a & is accepted where a native int is expected. This also applies to a delegate constructor's method pointer. This is the conversion that conv.u makes explicitly. Table III.8 marks it valid but not verifiable (a shaded cell), because the GC no longer tracks a & once it is a native int. Validation-only mode also accepts the explicit conversions of a writable & or an object reference to int64 or native int. Roslyn passes a & directly to a void* parameter for u8 literals and static data: ldsflda <RVA field>; newobj ReadOnlySpan<byte>::.ctor(void*, int32). Accepting a & directly where a native int or void* argument is expected removes 333 framework findings and 1,353 package findings. A readonly & is still reported (III.1.8.1.2.2), and so is a & stored into a native int local, argument or field, or passed in a tail call (point 5).

3. A native int and a writable & that meet at a join merge to a native int. CoreLib's Overlapped.set_OffsetLow, set_OffsetHigh and set_EventHandleIntPtr do cond ? ref field : ref ptr->Field, and ldflda through an unmanaged pointer pushes a native int (III.4.11). One limit: if ILVerify first imports the join block with a & on the stack, it reports an error if the block uses that value where only a native int is accepted. A later merge to native int does not remove the error, because ILVerify does not import a block again once it has an error.

   Merging a readonly & with a native int would convert the readonly & to a native int, which III.1.8.1.2.2 does not allow. Both modes report an error at such a join. When two & values to different types meet, the result is readonly if either one is. ILVerify checks the join block again unless it already has an error; in that case, the method is already reported.

   One older defect remains in both modes: when a writable T& reaches a join before a readonly T& of the same type, the merged value is not readonly. A later write through that merged pointer is usually reported in verification mode for another reason; validation-only mode may miss it.

4. A native int this for constrained. callvirt. The augments' Description and Verifiability paragraphs say "the type of ptr must be a managed pointer (&) to thisType", but the Correctness paragraph does not. I accept a native int there, as for a value type's this in call (III.1.6, III.1.1.5.1). The three NativeCallback methods in System.Net.Quic do this.

5. Tail calls with managed pointers are still reported. III.2.4 Correctness says "no managed pointers can be passed to the method being called if they point into the stack frame that is about to be removed". ILVerify does not track which frame a pointer points into, so validation-only mode keeps the verification rule, which rejects any & or byref-like argument. It checks the value passed as well as the declared parameter, so a & passed where a native int is declared is rejected too. The retained tail-call rule also rejects valid code: the 3 package findings come from one InlineIL method that passes two of its own & parameters and an unmanaged pointer to a tail. calli. A precise rule would have to follow addresses of locals and arguments through every instruction that derives one address from another, and through merges; I can try it if you want.

6. Validation reaches blocks that verification skips. ILVerify does not import a block that is reached only through a block with an error. Validation-only mode reports fewer errors, so it imports more blocks. In Decimal.CreateChecked, for example, verification stops at an InitLocals error before a later block that validation-only mode reaches.

7. Other judgement calls. Checks are kept unless noted.

   • Kept: this initialization in constructors (III.1.8.1.4), access checks and CallAbstract for call (III.3.19 lists them under Verifiability, but the runtime enforces them), CallVirtOnValueType, DelegateCtor for a target whose signature does not match the delegate's, NewobjAbstractClass, CallCtor, LdftnCtor, the switch operand type, InitOnly for stsfld (II.16.1.2), and value-type agreement for box.
   • Not reported: BackwardBranch (the augments delete the rule), ConstrainedTypeNoInterfaceImpl (augmented III.2.1 Verifiability), EndfilterStack (only III.3.34 Verifiability states it), and merging & values that point to different types.

Fixes #37391

Note

This PR was prepared with AI assistance (Anthropic Claude and OpenAI Codex), under my direction. I reviewed it before posting.

[dotnet-policy-service]

Tagging subscribers to this area: @JulieLeeMSFT, @dotnet/jit-contrib
See info in area-owners.md if you want to be subscribed.