Inside Microsoft .NET IL Assembler

Code Verifiability

The verification algorithm associates IL instructions with valid evaluation stack states and, first of all, with the number of stack slots occupied and available at each moment. Stack overflows and underflows render the code not only unverifiable but invalid as well. The verification algorithm also presumes all local variables are zero-initialized before the method execution begins. As a result, the .locals directive—at least one, if several of these are used throughout the method—must have the init clause in order for the method to be verifiable.

The verification algorithm simulates all possible control flow paths and branchings, checking to see whether legal stack states correspond to every reachable instruction. It is impossible, of course, to predict the actual values stored on the evaluation stack at every moment, but the number of stack slots occupied and the types of the slots can be assessed.

As mentioned, the evaluation stack type system is coarser than the metadata type system used for field, argument, and local variable types. Hence, the type validity of instructions transferring data between the stack and other typed memory categories depends on the type conversion performed during such transfers. Table 10-5 lists type conversions between different type systems.

Table 10-5  Evaluation Stack Type Conversions 

Metadata Type

Stack Type

Managed Pointer to Type

[unsigned] int8, bool

int32

int8&

[unsigned] int16, char

int32

int16&

[unsigned] int32

int32

int32&

[unsigned] int64

int64

int64&

native [unsigned] int, function pointer

native int

native int&

float32

Float

float32&

float64

Float

float64&

Value type

Same type (see substitution rules in this section)

Same type&

Object

Same type (see substitution rules in this section)

Same type&

According to verification rules, type A can be replaced with type B in the following cases only:

These substitution rules set the limits of “type leeway” allowed for the IL code to remain verifiable. As the verification algorithm proceeds from one instruction to another along every possible path, it checks the simulated stack types against the types expected by the next instruction. Failure to comply with the substitution rules results in verification failure and possibly indicates invalid IL code.

A few verification rules, rather heuristic than formal, are based on the question, “Is it possible in principle to do something unpredictable using this construct?”:

A great many additional rules regulate structured exception handling, but the place to discuss them is the next chapter.

Категории