[SwayamInSync]

A call failed its frame check, with a counterexample, even when the callee wrote only cells the caller may write. This happened in 0.1.1 and on main:

void set(int *p, int v)
  cppverify::pre(p != nullptr)
  cppverify::modifies(*p)
  cppverify::post(*p == v)
{
  *p = v;
}

void set_third(int *a)
  cppverify::pre(cppverify::valid(a, 4))
  cppverify::modifies(a[2])
{
  set(a + 2, 5);        // main: verification failed [frame]
}

void set_through_copy(int *a)
  cppverify::pre(cppverify::valid(a, 4))
  cppverify::modifies(*a)
{
  int *q = a + 2;
  set(q, 5);            // main: verification failed [frame]
}

Cause

footprintWithin (Passivize.cpp) decides whether a callee footprint lies in a caller footprint. It has two gaps:

• Caller cell, callee region: it returned false, even though calleeFootprintBytes already computes a region of one scalar object as one cell.
• Caller region: it compared the two pointers' bases by name (samePointerRegion: a == q). A callee footprint reached through a copy of a pointer into the region's object therefore never fit.

A store already follows the semantic rule. In the function's own frame check, a store through any pointer is inside a region footprint when its address lies in the region parameter's entry object.

Fix

The call check now follows the same rule as stores:

• Caller cell: a callee region that is one cell lies in the caller's cell when the two are the same cell.
• Caller region on a parameter: a callee footprint reached through a pointer with another base lies in the region when its cells lie in that parameter's entry object. A one-cell region counts as its cell, and a range or an extent counts as its bytes.

A footprint with the same base as the caller's region produces exactly the query it did before. A call that failed before can now verify only when its cells provably lie in the caller's frame. The test's false twins check this:

• the neighboring cell;
• a copy into another parameter's object, including one placed above a by the precondition;
• a choice whose b side is outside the frame;
• a range that runs past the caller's cell;
• a callee whose modifies range is wider than its extent, from a + 3;
• a trusted result one cell before the object.

This is also the frame half of B3a-2. Passing &r->head to set under modifies(r->head) needs this check.

Tests

suite/frame_call_objects.cpp contains:

• Proofs: a cell for a one-object region; an element for a one-object region; a copy for a region; a copy for a range; a choice between two writable objects; and an empty range elsewhere, which writes nothing.
• Failures: each false twin above, each failing its frame check at the call, with c = false for the choice.

On main every function in the file except the callees fails.

Docs

• pointers.rst: a checked example and its verdicts.
• Rule text: the same rule in book chapters 14 and 17, DESIGN.md, and ARCHITECTURE.md.
• Release notes: an entry under "Failures that were not real".

Checked

On main at de4972d:

• Verify lit suite: 429 passed and 1 unsupported, on both the release build and an assertions build. This includes the docs tests.

• VerifyTests: 60 passed, 1 skipped.

• On main: frame_call_objects.cpp fails.

• Verdict differential against main: 437 test sources. Only the new test differs, and no file's time changed (3544 s → 3501 s in total).

• Mutation: 6 mutants, all killed by the test. They:

  • drop the one-cell rule;
  • compare the cell at its end;
  • drop the object containment;
  • drop either end of it;
  • count a range as its first cell.

  Two cases were added for mutants that first survived: the copy placed above a, and the wide callee. A redundant emptiness disjunct was removed, since an empty callee range is already accepted before this check.

• Docs: check-doc-examples.py passes on every page this changes (56 examples, 10 against the verdicts their pages show).

• Merges: this merges cleanly with each open PR, verify: Follow the body of a choose in a spec's reads and postcondition checks #43, verify: Make chooses with one condition one choice, kept across writes elsewhere #44, verify: Send crash reports to cpp-verify's issue tracker #46, verify: Bound what a run builds and what its solvers allocate #48, and docs: Publish the documentation of each release, and of main at /dev/ #49.