[SwayamInSync]

Plan item B6 (globals beyond scalars), second part: static locals. Every static local that was not a constant table stopped its function (static local variables are unsupported). Stacked on #127 (B6a), whose commits it shows until that merges.

On the base

The example below (with this PR's output further down):

$ cpp-verify statics.cpp
statics.cpp:5:3: error: next_id: static local variables are unsupported
statics.cpp:15:3: error: first_call: static local variables are unsupported
Summary: 2 unresolved (construct.unsupported 2) in 0.0 s

With this PR

namespace cv = cppverify;
int next_id()
  cv::post(cv::result >= 1 && cv::result <= 1000)
{
  static int last = 0;
  if (last < 0 || last >= 1000)
    last = 0;
  last = last + 1;
  return last;
}

int first_call()
  cv::post(cv::result == 1)
{
  static int calls = 0;
  if (calls < 0 || calls >= 1000)
    calls = 0;
  calls = calls + 1;
  return calls;
}

Verified: next_id [backend=z3]
statics.cpp:13:23: error: verification failed: first_call [postcondition] [backend=z3] [reason=counterexample]
   13 |   cv::post(cv::result == 1)
      |            ~~~~~~~~~~~^~~~
statics.cpp:13:23: note: counterexample: result = 2
...

first_call returns 1 only the first time.

Design

A static local with a constant initializer is a global object (B6a) that only its function names. No contract can name it: ACSL scopes contracts the same way, and Frama-C, which renames a static local to a global, leaves a function that writes one unable to state its assigns. So it is the function's private state:

• Entry. Its value at entry is arbitrary, whatever earlier calls left.
• Frame. The function writes it without a footprint: a store into one of its private objects passes the frame check (inPrivateObject).
• Calls. A call changes it exactly when the callee may reach the owner: each function's private objects (VFunction::PrivateObjects) are its own statics and, after conversion, those of every function its call graph reaches (recursion, a callback through another function); an inlined helper's (B5) join the function it runs in. After a call, each of the callee's objects is changed (havocPrivateObjects), and a loop that makes the call has them in its write set. A call of any other function keeps them, and callers state nothing about them.
• Leaves. Each scalar leaf of a static record or array is changed alone, with a fresh value of its type, as a loop's written cell is (an object of more than 64 leaves is changed as a whole, by a heap frame). The heap frame first used for every object left counterexamples to model search, which took 60 s and ended solver.timeout; leaf by leaf they take milliseconds.
• No escape. A pointer to or into a static local is rejected (a pointer to the static local value is unsupported: its function's state would escape), which is what makes the call graph a sound bound on who changes it. A static local whose initializer runs code at the first call (static int first = x;) is rejected too.
• cppverify::old of a static local in its function's loop invariants is its value at entry.

Tests

suite/static_locals.cpp (new): a counter that saturates, and its callers; the initializer is not the value at entry (first_call); a record and an array; a value kept across a call of an unrelated function (keeps); a value changed by a callee that calls back (owner, through pass_on), by a direct recursive call (recursive), by a recursive call to a function with a static record (recursive_record), and by a call in a loop (looped), each a certified failure; a helper's static in the function it is inlined into (ticked); a loop invariant over a static and cppverify::old of one; and the three rejections. lookup_tables.cpp: seen, a static array, now verifies.

On a release build of this branch, the whole Verify suite passes (512 of 513, one unsupported). A first run failed shared_logic_terms.test, which pins the size of set_value's module: the store frame check of every function had gained || false where it has no static locals (8 more nodes before simplification, one more rewrite). The disjunct is now added only with private state, so a function without static locals lowers to the same module as before.

Mutants

Each mutant below, applied alone and rebuilt, is caught by static_locals.cpp (and lookup_tables.cpp for S11), 11 of 11:

Mutant	Change
S1	no closure over the call graph (a callee that calls back keeps the owner's static)
S2	an inlined helper's statics stay the helper's own
S3	a store to the function's own static needs a footprint
S4	a call keeps the callee's statics
S5	a loop's calls do not put the callees' statics in its write set
S6	a call that changes only private state is not counted as writing the heap
S7	a static record changes as a whole (by a heap frame): recursive_record ends solver.timeout instead of failing
S8	an initializer that runs code is accepted
S9	a pointer into a static local is allowed
S10	cppverify::old of a static local is rejected
S11	static locals are not objects (the base's behavior)

Docs

• Pointers: static locals, the rules and an example with its output; limitations (supported and unsupported columns);
• the book, chapter 14; release notes; DESIGN (3c); ARCHITECTURE ("Static locals").

Not done

• A static local initialized by running code (the first call's guard), and pointers to static locals.
• Counterexamples do not show a static local's value by name yet: it is a cell, shown as a store at its address.