[SwayamInSync]

A loop that wrote local or dynamic storage forgot the value of every object. On the base (#74):

int other_array()
  cv::post(cv::result == 7)
{
  int a[3];
  int b[2];
  b[0] = 3;
  b[1] = 4;
  for (int i = 0; i < 3; i = i + 1)
    cv::invariant(0 <= i && i <= 3)
    cv::decreases(3 - i)
  {
    a[i] = 0;
  }
  return b[0] + b[1];
}

frames.cpp:14:3: error: verification failed: other_array [...::overflow@14:3] (counterexample: ...) [backend=z3] [reason=counterexample]

Now:

Verified: other_array [backend=z3]

Stacked on #74, which found it: a loop that fills a local array is now verified, but it still forgot every other local.

Cause

A loop writes only the objects its stores and calls reach (loopWriteRegions): a parameter's cell, the entry objects of a pointer's origins, or a parameter's or global's object (rootRegion). Local and dynamic storage has no origin (it carries its lifetime companion instead) and is no root there, so a loop that stored to it was not framed and the whole value heap was havocked. The other bound, the function's own frame, rightly declines when the function owns storage: a store to its own storage is never checked against its modifies, so assuming that frame would freeze the loop's writes to its locals.

Design

The object model already bounds where such a store lands; the frame now says so, as it does for parameters.

• A store through a pointer into local or dynamic storage (representedCell): when its address is that pointer, a reference to a local say, and the loop assigns neither the pointer nor its lifetime companion, it writes that one cell. So does a call whose footprint is the one cell its reference argument binds.
• A store rooted at the pointer an allocation defined (representedRegions, RepresentedObjects: the allocated type and size, recorded at each VAllocateStmt and fresh-owned call), under the same condition, writes that object: its fields lie in the record's layout and its fixed-array indices are checked (kind bounds), as a store through a parameter lies in its entry object by the object model's checks; a dynamic object is one scalar. So does a call whose footprint's argument is rooted there.
• The object as cells. The object is its scalar leaves (VFunction::Layouts, array repeats expanded), each one cell, so the loop's frame stays the chain of stores of fresh values (ARCHITECTURE, loop frames); without a layout it is its bytes. As a byte range (a HeapFrame, an unbounded quantifier), Z3 found no counterexample to overwritten below in 90 s; with the cells it fails in 0.2 s.
• The condition that the loop assigns neither pointer cannot be exercised today: the converter rejects allocation and pointer reassignment in loops. It keeps the frame sound if they are admitted.

Tests

suite/loop_local_frames.cpp (Z3, with a check that no proof is vacuous, and BMC):

• kept_value: a scalar behind a reference keeps its value across a loop that writes an array;
• other_array: so does another array;
• record_read: a local record the loop reads keeps the field it does not write;
• with_parameter: a loop writing a parameter's object and a local array keeps a third object;
• through_call: a call in the loop writing an element of a local array (set(a[i], 0));
• dynamic_kept: a new object keeps its value;
• reference_written, reference_call: a store or a call through a reference to a local writes only that local;
• overwritten: a cell the loop writes is not kept (postcondition), which a frame too small would prove;
• through_reference: neither is a local written through a reference to it (postcondition).

On the base, all eight that verify fail their postconditions (other_array its overflow check first).

Mutants, each built on an assertions build and run on loop_local_frames.cpp, loop_initialization.cpp, loop_frames.cpp, out_parameters.cpp, and local_record_arguments.cpp: 6 of 6 killed.

Mutant	Killed by
no local or dynamic objects in the write set (the base)	loop_local_frames (the eight that verify)
an object framed as its first leaf only	loop_local_frames (overwritten verifies: the false proof a frame too small gives)
an object framed as its bytes	loop_local_frames (overwritten, through_reference: solver.timeout)
no exact cell for a store through a local pointer	loop_local_frames (reference_written)
calls whose argument is rooted at a local object havoc the heap	loop_local_frames (through_call)
no exact cell for a call's reference argument	loop_local_frames (reference_call)

Docs

• functions-loops.rst: local and dynamic objects in a loop's write set, a checked example (other_array, overwritten).
• Release notes: "Loops that write local storage".
• DESIGN.md: loop contracts. ARCHITECTURE.md: loop frames of local and dynamic storage.

Checked

• The Verify suite on a release build: 460 passed (the exhaustive decoder filtered out), 1240 s with 40 workers.
• The doc pages' examples (functions-loops, DESIGN): 33 checked, 0 failed; docs_examples.test and docs_coverage.test pass.