[Mono-list] Verification runtime support

[Hinne Hettema (DSL AK)]

I've done some work looking at what needs to happen for verification and
what is currently in the code--attached are some thoughts (ramblings rather)
on what needs to happen to make this work. 

I'm interested to bring the code verification forward, but would appreciate
comments on these ideas, to figure out whether I'm off or on the right
track.

Verification
============

Key is the difference between

o (Syntactically) Correct Code
o Valid Code
o Typesafe Code
o Verifiable Code

Verification ensures that code is safe to execute.

Tests performed by the validator:

o Syntax checks (compiler?)
o Metadata checks

In addition, the verifier checks that

o All uses of data are consistent with their declarations (needs access to 
multiple assemblies)
o Every method is called with the correct number of parameters
o Each parameter is of the correct type
o Local variables are never used unless initialised along every control flow

path that leads to the attempted use (no memory is read without having 
previously been written to).

Algorithm
Partition III of the ECMA proposed standard outlines the verification
algorithm 
in section 1.8. This is a rehash of this text:

The algorithm shall attempt to associate a valid stack state with every CIL 
instruction. A stack state is the number of slots on the stack as well as
the 
type for each of them. The initial stack state is empty.

Verification assumes that the CLI zeroes all memory other than the
evaluation 
stack before this memory is made available to other programs.

The algorithm has to simulate all possible control flow paths through the
code 
abd ensure that a legal stack state exists for every CIL instruction. Only
type 
assignments are used.

Termination occurs successfully if all paths have been simulated.
Unsuccessfully 
if an invalid stack state was found or when "additional tests specifiedi in
this 
clause fail" (what is this supposed to mean?)

Stack states may have to be joined and the algorithm specifies valid joins.

As I read this, this essentially specifies a dataflow algorithm.

A possible order for verification is

1. Validation tests (metadata) -- some of these are already in the code
AFAIK
2. Type tests (uses are consistent with declarations)
3. Initialisation tests with a dataflow algorithm

If this is what needs to happen, some observations on the current code would
be

-- We only call code verification from the interpreter but not yet from the
JIT compiler?
-- The current verification code looks at (some) metadata and pointers on
the stack, but doesn't     do any type checking or dataflow analysis


Hinne Hettema