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).
New Feature
Open
Major
RVM-929
Follow Java Virtual Machine Specification
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;
For inter-procedural constraints we could add rules like
In the future we could also add all sorts of annotations and verify them. (Using Haskells naming mechanisms)
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).