Ideally any verifier we use would be capable of being extended to add custom intra-procedural verification rules and possibly even add inter-procedure linking constraints.
i.e. For intra-procedural constraints we could add rules to ensure;
- @Unpreemtible functions do not contain any "illegal" opcodes
- @Pure functions do not not contain any mutator opcodes.
- null is never assigned to a @Unboxed value
- @Unboxed values never cast
For inter-procedural constraints we could add rules like
- @Unpreemtible functions can only call @Unpreemtible methods or equiv
- @Pure functions can only call @Pure functions
In the future we could also add all sorts of annotations and verify them. (Using Haskells naming mechanisms)
- @IO procedure has side-effects and can only call @IO or @Pure
- @STM procedure is a software transactional procedure and can only call @Pure or @STM
- @STM_RO is a read-only STM and can only call @Pure or @STM_RO
We could also use the "verifier" to automagically classify different procedures as @IO, @Pure, @STM etc which would simplify the compiler and enable many more optimizations with relatively minimal overhead (as data flow analysis already donw within verifier).