Verification algorithm for managed pointers.

Note in the specification on verifiability algorithm of the CLI:

While a compliant implementation is required to accept and run any program this verification algorithm states is verifiable, there may be programs that are accepted as verifiable by a given implementation but which this verification algorithm will fail to consider verifiable. Such programs will run in the given implementation but need not be considered verifiable by other implementations.

Rationale in the specification on managed pointer as return type:

Some uses of returning a managed pointer are perfectly verifiable (eg, returning a reference to a field in an object); but some not (eg, returning a pointer to a local variable of the called method). Tracking this in the general case is a burden, and therefore not included in this standard.

Verification rules:

These two excerpts from the specification allow to provide implementation specific verification rules and particulary rules for verification of managed pointer as return type.

I have developed liberal and simple JIT-time rules for a such verification process. For each managed poiner in stack JIT tracks it's source origin. JIT realizes following origins:

managed pointer to the heap (ByRefToHeap) - refers to object's fields or static fields, this is most liberal pointer;
managed pointer to data in the caller stack frames (ByRefToCaller) - refers to a local variable into the stack frame of the caller, or some of it's callers;
managed pointer to data in the local stack frame (ByRefToLocal) - refers to a local variable in the current stack frame.

At the start of process of compilation of method JIT designates:

ByRefToCaller to all arguments of managed pointer type;
ByRefToLocal to all local variables of managed pointer type.

Note: origin of managed pointer that is stored in local variable or argument is changeable. It should be considered rather as value of variable at JIT time then property or type of variable itself.

During compilation JIT tracks origins of all managed pointers in local variables, arguments and stack guiding by the following rules:

when managed pointer is loaded into the stack from local variable or argument, origin of variable on the stack becomes the same as origin of variable being loaded;
when managed pointer is stored from the stack to a local variable or an argument, origin of variable becomes the same as origin of variable on stack being stored;
managed pointer as result of ldsflda has ByRefToHeap origin;
managed pointer as result of ldflda has origin either ByRefToHeap if field is of ref type, or has the same origin as value type managed pointer whose field adress is getting;
managed pointer as result of ldloca, and ldarga has ByRefToLocal origin;
managed pointer as result of method call is a subject of origin adjustment.

Origin adjustment. This process allows to change origin of managed pointer as result of method call to more liberal. Considering all arguments to a method. Note that "this" value is considered also. The following rules are used:

if method have no arguments that are managed pointers, or all such arguments have ByRefToHeap origin, then result has ByRefToHeap origin,
otherwise if all arguments that are managed pointers have either ByRefToHeap or ByRefToCaller origins then result has ByRefToCaller origin,
otherwise result has ByRefToLocal origin.

Merge stacks. This process adjust origins of managed pointers in the stack when stack merge is performed. Result of merge is a managed pointer with less liberal origin. Following table shows how origin is adjusted as result of merge operation:

source\with ByRefToHeap ByRefToCaller ByRefToLocal

ByRefToHeap ByRefToHeap ByRefToCaller (rejit required) ByRefToLocal (rejit required)

ByRefToCaller ByRefToCaller ByRefToCaller ByRefToLocal (rejit required)

ByRefToLocal ByRefToLocal ByRefToLocal ByRefToLocal

source\with	ByRefToHeap	ByRefToCaller	ByRefToLocal
ByRefToHeap	ByRefToHeap	ByRefToCaller (rejit required)	ByRefToLocal (rejit required)
ByRefToCaller	ByRefToCaller	ByRefToCaller	ByRefToLocal (rejit required)
ByRefToLocal	ByRefToLocal	ByRefToLocal	ByRefToLocal

Virification rule:

it's possible to return managed pointer that have ByRefToHeap or ByRefToCaller origin only.

Conclusion: this set of rules allows more complete usage of managed pointer type with addition of simple set of rules at JIT only.