Subregion Analysis

This MR implements a draft of a static analysis meant to circumvent a common issue we encounter with Why3's region based analysis in Creusot.

Sometimes only modify part of a mutable field in a loop but lose that information to Why3's eyes, thus forcing users to add what should be unnecessary loop invariants for their proofs to pass.

Rather than implementing this as a pass only within Creusot, I chose to add it to Why3 as it may be beneficial to other front-ends / tools. However, given the experimental nature of this pass, I wanted to avoid forcing it onto everyone from the outset and implemented it as a stand-alone module which is only run on mlcfg files.

If this works well enough and is interesting to other front-ends (perhaps the issue only occurs in the manner in which we use why3) then we can consider integrating this fully into why3.

---

I attempt to give a quick intuition of this analysis and why it's interesting.

The analysis in this patch performs a single pass over the code, calculating an abstract value for each local variable of the program. These values have the following form:

V = { .., f_i : V, ... } (* a record of values *)
  | V.f (* a field of a value *)
  | x (* a variable *)
  | ⊥ (* fresh / unknown value *)

There are two key rules in the analysis: assignments and loops

When we see an assignment x.f_i <- y, wlog, let the value of x be of the form { f_0 : V_0, .., f_i : V_i, ... } and the value of y be w. Then after assignment we update the value of x to be { f_0 : V_0, ... , f_i : w, ... }.

Note: we can always normalize the value x to be in the form { f_i : V_i }.

In the case of loops, we perform the analysis on the body of the loop with a context in which every variable has itself as its value (that is, the value of x is x). By considering the values of all variables after analyzing the body of the loop we can deduce parts of variables which are invariant with regards to the loop.

Suppose that after analyzing a loop body we have x -> { f_0: x.f_0, f_1 : z }, from this we can deduce that the value of x.f_0 was unchanged by the body of the loop.
We thus add after the loop an assume statement which states this fact, allowing proofs to leverage it.