Documentation

When live loop-carried dependencies are discovered as we traverse a loop body, new "widening" variables are introduced to stand in for those locations. When we introduce such a varible, we capture what value the variable had when we entered the loop (the "header" value); this is essentially the initial value of the variable. We also compute what value the variable should take on its next iteration assuming the loop doesn't exit and executes along its backedge. This "body" value will be computed in terms of the the set of all discovered live variables so far. We know we have reached fixpoint when we don't need to introduce and more fresh widening variables, and the body values for each variable are stable across iterations.

This execution feature is designed to allow a limited form of verification for programs with unbounded looping structures.

It is currently highly experimental and has many limititations. Most notibly, it only really works properly for functions consiting of a single, non-nested loop with a single exit point. Moreover, the loop must have an indexing variable that counts up from a starting point by a fixed stride amount.

Currently, these assumptions about the loop strucutre are not checked.

The basic use case here is for verifiying functions that loop through an array of data of symbolic length. This is done by providing a ""fixpoint function" which describes how the live values in the loop at an arbitrary iteration are used to compute the final values of those variables before execution leaves the loop. The number and order of these variables depends on internal details of the representation, so is relatively fragile.