Implementing loop invariant generation

[fortunac]

We need to engineer a system such that we can create and check loop invariants. We have loop unrolling for now, but this is still open. We also need a way to select which loop handler to invoke, and how to tag each SCC.

[fortunac]

The rule for structured loops is as follows:

      {I && cond} body  { I }
----------------------------------
{ I } while(cond) body {I && !cond}

However, to be of any use in a WP setting, it needs to be paired with the weakening rule:

{ P' } p { Q' }    P => P', Q' => Q valid
-----------------------------------------
               { P } p { Q }

In practice, we combine those rules in one to produce:

{ I && cond} body { I }    I && !cond => Q valid
-----------------------------------------------------
            { I } while(cond) body { Q }

If we're doing WP, and a similar rule if we do Strongest Postconditions.

Unfortunately, in BIR we do not have structured loops. It is more difficult to formulate a simple rule for WP for the unstructured setting.

What I propose:

Reconstruct the loop structure for "simple" loops, which I describe as loops for which the SCC has a dominator and a postdominator.

For such loops, we compute the WP in the following manner:

• WP(l) = I, where i is the last instruction of the post-dominating block for the SCC. We create the side condition I => P where P is the current post-condition.

• We then get WP(e) = I' for the first instruction of the dominating block for the SCC, and we add the side condition I' => I.

I think this is sound for simple loops, but I'd be happy if someone could chime in with a confirmation or infirmation (is that a word?).

Implementation therefore requires 2 steps:

• Adding side conditions to env, to be checked at precondition checking time. In fact, I wonder if we should just be returning a set of VCCs.

• Adding hooks for looking up invariants and generating the VCCs when entering and leaving an SCC.