[SwayamInSync]

Plan item B6 (globals beyond scalars), first part: mutable global records and arrays. Only integral globals were supported; a record or array global stopped its function (global aggregate access is unsupported, the global array 'table' is unsupported).

On the base

The example below (with this PR's output further down) stops all three functions, with 16 errors:

$ cpp-verify globals.cpp
globals.cpp:13:12: error: set_mode: global aggregate access is unsupported
...
globals.cpp:15:3: error: set_mode: global aggregate assignment is unsupported
globals.cpp:20:32: error: clear_history: the global array 'history' is unsupported
...
globals.cpp:35:10: error: entry: the array member 'table' of the global 'config' is unsupported
Summary: 3 unresolved (construct.unsupported 3) in 0.0 s

With this PR

namespace cv = cppverify;
struct Config {
  int mode;
  int limit;
  int table[4];
};

Config config;
int history[8];

void set_mode(int m)
  cv::modifies(config.mode)
  cv::post(config.mode == m && config.limit == cv::old(config.limit))
{
  config.mode = m;
}

void clear_history()
  cv::modifies(history[0 : 8])
  cv::post(cv::forall(k, 0, 8, history[k] == 0))
{
  for (int i = 0; i < 8; i = i + 1)
    cv::invariant(0 <= i && i <= 8)
    cv::invariant(cv::forall(k, 0, i, history[k] == 0))
    cv::modifies(history[0 : 8])
    cv::decreases(8 - i)
  {
    history[i] = 0;
  }
}

int entry(int i)
  cv::pre(0 <= i && i <= 4)
{
  return config.table[i];
}

Verified: set_mode [backend=z3]
Verified: clear_history [backend=z3]
globals.cpp:35:10: error: verification failed: entry [bounds] [backend=z3] [reason=counterexample]
   35 |   return config.table[i];
      |          ^
globals.cpp:35:10: note: counterexample: i = 4
Summary: 2 verified, 1 failed in 1.0 s

Design

As Frama-C models globals: a mutable global of an integral, record, or array type is one object at a fixed address of its own, in the global region above every other object, where scalar globals already were.

• Places. objectPlace roots a global object at its address (globalObjectPlace), so config.mode, config.table[i], grid[1][j], and slots[i].key are places like a promoted local's: cells with their access conditions (each index bounded by its array, kind bounds). Reads, stores, cppverify::old, range-based for, and cppverify::modifies footprints (the whole object, a field, an element, a range) all go through them.
• Entry state and frames. Its value at entry is arbitrary, as for a scalar global, since any function may have changed it; a function writes it only within its modifies; a call changes only the callee's footprints.
• Pointers into it. history, &config.limit, config.table are subobject pointers (B3a-2) bounded by the array, field, or record they are formed from. Their address converts the global's literal (a Cast) instead of retyping it: the literal's type names the whole object and gives the origin @address/size, which retyping shrank to one element, so every access past the first failed. abstractValidity now counts the global objects a pointer's origins name as valid storage, so such a pointer may be passed as a valid(p, n) slice; before, only parameters' objects were.
• Fail closed, located: a whole record or array of a global read as a value, a global of a class with a cppverify::type_invariant (nothing establishes or maintains it at every function's boundary), a global that is itself a pointer (nothing could state that the pointer it holds is valid), a spec reading a mutable global, ghost or proof code writing one, thread-local and volatile globals. Static locals stay rejected: they are B6's second part, which needs private frames (a function writes its own static locals without naming them, and only calls that may reach it change them).

Tests

• suite/global_objects.cpp (new): a field written within its frame and outside it (frame); an element read, with a Layer-1 dump of its place; an element in range and one past it (bounds); a global array cleared in a loop with a range frame; a callee writing one field keeping the others; the whole object as a footprint; a decayed global array passed as a slice, and one element too long (bounds); a pointer into a global array, in range and one past (bounds); a field's address given to a writing callee, within the frame and outside it; records in an array and a two-dimensional array (one index past its row fails); a parameter's pointer stored in a field; and every rejection above with its message. A Layer-1 dump shows the store at the global's address plus the field's offset.
• Tests that used a global array as their example of an unsupported construct now verify it: lookup_tables.cpp (counter now fails its claim that an element is 0, since a mutable global's value at entry is arbitrary, as the test's own comment says), range_for.cpp, pointer_subobjects.cpp, dynamic_loaded_values.cpp; per_function_errors.test uses a pointer global instead; ghost-runtime-mutation-unsupported.cpp is rejected for the right reason now (a proof writing a global, instead of aggregate assignment); z3_calls_fail_closed.cpp has the new message.

On a release build of this branch, the whole Verify suite passes (510 of 511, one unsupported).

Mutants

Each mutant below, applied alone and rebuilt, is caught by the tests named above (12 of 12):

Mutant	Change	Caught by
G1	no global objects (the base's behavior)	six tests
G2	objectPlace has no global root	global_objects, lookup_tables, range_for
G4	a pointer into a global retypes its literal	global_objects, dynamic_loaded_values
G5	global objects are not valid storage for a slice	global_objects
G6	no store to a global place	global_objects, ghost-runtime-mutation-unsupported
G7	ghost and proof code may write a global object	ghost-runtime-mutation-unsupported
G8	a whole global object is read as a value	global_objects
G9	a class invariant is ignored	global_objects
G10	a global array's element goes through its decayed pointer	global_objects (Layer-1 dump)
G11	a global object is no footprint	global_objects
G12	no pointer into a global object	global_objects, dynamic_loaded_values
G13	a spec reads a global object	global_objects

• G10 survived a first run: through the decayed pointer, an element's bounds are still checked (by the subobject pointer's companions), so every verdict was the same; the place is the direct form, one load with its bounds as the access condition, which the dump now pins.
• A first version also skipped the binding check of a pointer formed into a global object (G3 survived): once a global's object counts as valid storage, the general check holds there, so the special case is gone.

Docs

• Pointers: a section "Global variables" (the rules, an example with its output, what fails closed); functions and loops (range-based for over a global array); limitations (supported column, storage row, control flow row);
• the book, chapter 14: "Global records and arrays", with an example;
• release notes; DESIGN (3c, global objects); ARCHITECTURE (global objects).

check-doc-examples.py passes on every changed page.

Not done

• Static locals (B6's second part) and globals that are pointers.
• Invariants over globals (ACSL's global invariant).