This module provides an execution feature that can be installed into the Crucible simulator which facilitates reasoning about certain kinds of loops by using loop invariants instead of requiring that loops symbolically terminate. In order for this feature to work, the loop in question needs to be single-entry/single-exit, and needs to have a constant memory footprint on each loop iteration (except that memory regions backed by SMT arrays are treated as a whole, so loops can write into different regions of an SMT-array memory region on different iterations). In addition, loop-involved memory writes must be sufficiently concrete that we can determine their region values, and writes to the same region value must have concrete distances from each other, so we can determine if/when they alias.

To set up a loop invariant for a loop, you must specify which CFG the loop is in, indicate which loop (of potentially several) in the CFG is the one of interest, and give a function that is used to construct the statement of the loop invariant. When given a CFG, the execution feature computes a weak topological ordering to find the loops in the program; the number given by the user selects which of these to install the invariant for.

At runtime, we will interrupt execution when the loop head is reached; at this point we will record the values of the memory and the incoming local variables. Then, we will begin a series of "hypothetical" executions of the loop body and track how the memory and local variables are modified by the loop body. On each iteration where we find a difference, we replace the local or memory region with a fresh "join variable" which represents the unknown value of a loop-carried dependency. We continue this process until we reach a fixpoint; then we will have captured all the locations that are potentially of interest for the loop invariant.

Once we have found all the loop-carried dependencies, we assert that the loop invariant holds on the initial values upon entry to the loop. Then, we set up another execution starting from the loop head where we first assume the loop invariant over the join variables invented earlier, and begin execution again. In this mode, when we reach the loop head once more, we assert the loop invariant on the computed values and abort execution along that path. Paths exiting the loop continue as normal.

Provided the user suppiles an appropriate loop invarant function and can discharge all the generated proof obligations, this procedure should result in a sound proof of partial correctness for the function in question.

This whole procedure has some relatively fragile elements that are worth calling out. First, specifying which loop you want to reason about may require some trial-and-error, the WTO ordering might not directly correspond to what is seen in the source code. The most reliable way to select the right loop is to ensure there is only one loop of interest in a given function, and use loop index 0. The other fragility has to do with the discovery of loop-carried dependencies. The number and order of values that are supplied to the loop invariant depend on the internal details of the compiler and simulator, so the user may have to spend some time and effort to discover what the values appearing in the invariant correspond to. This process may well be quite sensitive to changes in the source code.

Limitiations: currently, this feature is restricted to 64-bit code.