Idea: split basic blocks into preconditions+code

[elazarg]

Currently the verifier performs two passes: one for establishing invariants, and one for checking that these invariants imply the assertions. Both passes iterate complete basic blocks (though the verification pass ignore loops).

If basic block can be arranged such that each hold (a) code to execute and (b) a set of assertions denoting the precondition for the code to execute safely, then the second pass need not look at the code at all, and the first pass need not look at the assertions at all (though assertions are also assumptions, so it could sometimes be faster to look at them).

This would require either avoiding simplification before assertions, or some sort of preprocessing that will collect the assertions backwards to the beginning of each block. This is a kind of abstract interpretation in which the abstract domain is a set of assertions, but for our purposes we won't need any sophisticated join, meet or widening - merely collecting the assertions would be enough for significant improvement.

From a class design point of view, this would allow splitting the domain to operations on code and operations on assertions.

[caballa]

I don't fully follow what you are suggesting but if you want to reduce the checking time we can do the following. If a block is not part of any nested WTO component then we can check the assertions at the same time we apply the transfer function. If we are in a nested WTO component then we wait until the component stabilizes and then check. For programs without loops, we would have only one phase. That would also reduce memory footprint because we can throw away invariants as soon as we check the assertions.