[SwayamInSync]

Since #50, the fields and fixed-array elements of a record reached through a pointer can be read and written (r->buf[i]). A pointer into such a record was still an error, so common forms could not be verified:

Form	main
a member array passed to a buffer function: first(r->buf, 8)	a pointer to the array member 'buf' is unsupported
a pointer walking a member array: for (const int *q = r->buf; q != r->buf + 8; q = q + 1)	same
the address of an element, a field, or a nested record: &r->buf[i], &r->head, &r->inner	raw address-of is unsupported until lexical lifetime and escape effects are modeled
the address of an element of a parameter's own buffer: &a[2]	same

The second message also gave the wrong reason: the pointee is the caller's storage, so lexical lifetime has nothing to do with it.

All of these are supported now:

struct Ring { int buf[8]; int head; int count; };

int first(const int *p, int n)
  cppverify::pre(cppverify::valid(p, n) && n >= 1)
  cppverify::post(cppverify::result == p[0])
{
  return p[0];
}

int oldest(const Ring *r)
  cppverify::pre(r != nullptr)
  cppverify::post(cppverify::result == r->buf[0])
{
  return first(r->buf, 8);        // Verified
}

int past(const Ring *r)
  cppverify::pre(r != nullptr)
{
  const int *q = r->buf;
  return q[8];                    // bounds: q[8] is r->head, inside *r, but past buf
}

Design

A pointer into a record may address only the subobject it points into. That is the array it decays from or whose element it addresses, or else the field or record. A check against the object alone would accept q[8] above, because it is r->head, inside *r.

How the references handle this:

• Frama-C's RTE emits index_bound for s->a[i] (plugins/rte/src/rte.ml:71-83). But once q = s->a, it checks only \valid(q + i) against the whole object, so q[8] passes there.
• CHERI narrows a capability to the subobject when the pointer is formed (subobject bounds), and hardware checks it on each access.
• Rust and Verus slices carry their length with the pointer.

This PR combines them: the bounds are narrowed where the pointer is formed, as in CHERI, carried with the pointer, as in a slice, and proved instead of checked at run time.

Forming the pointer. ASTConverter::subobjectPointer lowers the pointer.

• Inside a statement (a declaration, an assignment, a call argument, a return), it first asserts what C++ requires for the address to exist:

  • the place's access condition, so every index on the path is inside its array, strictly: &r->buf[i] needs i < 8, while r->buf + 8 is fine;
  • the place's accessibility (non-null root), through the existing reference-binding check.

  It then binds the address to a fresh pointer, __subobject_N, with two ghost companions, .__lo and .__hi. They hold the first byte and the end of the subobject.

• In a condition or a contract, the pointer is only a value to compare, so it is the address alone.

Spreading the bounds. propagateSubobjectBounds (a new pass, Transform/SubobjectBounds.cpp) runs on the converted body:

• every pointer variable assigned a value rooted at a bounded pointer is bounded too, whether through steps, casts, or conditionals (c ? r->buf : r->other selects the bounds like the value);
• its companions take the value's bounds before the assignment; a root without bounds may address any byte;
• a step keeps the bounds;
• each bounded variable starts with "any byte" at entry;
• a loop that moves a bounded pointer gets the generated invariant q == 0 || q.__lo == 0 || q % S == q.__lo % S. Like the origin analysis's own invariants, it is proved, not assumed. It keeps a stepped pointer on element boundaries, which the subobject's bounds need: the origin analysis's alignment invariant applies only when the pointer has its origin's type, and int * into a Ring does not.

Returning a bounded pointer, or storing it in memory, would lose the bounds, so it is a conversion error.

Checking the bounds:

• Accesses and steps (UB instrumentation): lo <= addr < hi at each access, and lo <= p <= hi at each step.
• Pointer differences: each operand must lie in the other's closed bounds, as [expr.add] requires both pointers in one array. So &r->head - r->buf is an error, while q - r->buf with q in buf is fine.
• Calls (emitCallStmt): the bytes a callee's extent or single object takes from a bounded argument must lie in the bounds. So first(r->buf, 9) fails, as does get(r->buf + 8).

Bugs this uncovered, fixed here because the new pointers expose them

• Field offsets:
  • Cause: a field offset is a constant of pointer type, so r + 32 is a sum of two pointers. The origin analysis and the step rule did not treat it as a step from r.
  • Effect: a pointer into a record got no origin. Worse, an access at a field offset through a bounded pointer (it[1].v) lost its bound check and verified.
  • Fix: steppedPointer (Origins.cpp) reads the constant in a sum of two pointers as the offset, keeping a global's literal address a pointer. It is shared by the origin analysis, pointerOrigins, pointerOriginTerm, and the bounds pass.
• Pointer-difference positions:
  • Cause: positions measured a single-object origin in the pointer's own elements, 4 bytes for int *, rather than the origin object's, 40 bytes for Ring. That held only while every pointer with origin r had r's type.
  • Effect: q - r->buf failed, a wrong failure.
  • Fix: PassivizerImpl::OriginObjects gives originPositionSafety each parameter's own object.

Tests

suite/subobject_pointers.cpp has three runs.

• Proofs:
  • the member array passed whole and from an element;
  • a local pointer, an element's address, a field passed to set, a nested record passed to a function over it;
  • a row of a 2-D member, an element record, a parameter's own element;
  • a stepping loop with q == r->buf + i, and a for loop comparing with the end and measured by q - r->buf;
  • a pointer difference, a choice between two members, reassignment to a parameter, a write through a copy under modifies(r->buf[0 : 8]), and a cppverify::check through the pointer.
• Failures, each at its access, call, or formation, with its counterexample:
  • 9 elements from buf, and 4 from buf + 5;
  • q[8], which is r->head; q[6] from &buf[2]; q[1] from &r->head, which is r->inner.x;
  • q[4] of a row, which is the next row; it[1] past items; q[-1] before other, which is the last item;
  • the other side of a choice; a walk one element too far;
  • get(r->buf + 8), which reads the end; &r->buf[i] with i == 8; a null root;
  • a difference across members; a write to other outside the frame.
• Layer 1 dump: the companions where r->buf is formed, and their copy into q.
• Escape errors: storing into a pointer field, and returning &r->buf[2], with locations.

pointer_subobjects.cpp (#50) no longer expects the decay error for a member through a pointer; its global cases stay.

Docs

• structs.rst: a new "Pointers into a record" section, with a checked example (pass, walk, q[8]), the C++ rules for forming, steps, differences and comparisons, and the escape error as a rejected example.
• ch14: a pointer walking the stack's items, with a checked failing twin and an explanation of its counterexample.
• pointers.rst: origins and subobject bounds.
• limitations.rst: the Arrays row and the supported list.
• Release notes: an entry under "C++ that compiles now".
• DESIGN.md and ARCHITECTURE.md: the design above.

Checked

On main at 573c171 (with #52 and #43):

• Verify lit suite: 431 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: all three RUN lines of subobject_pointers.cpp fail; main rejects the file's subobject pointers with the decay and address-of errors.

• Verdict differential against main: 439 test sources. Only subobject_pointers.cpp differs, and no file's time changed (3510 s → 3466 s in total). The changes to origins and pointer-difference positions alter no existing verdict.

• Mutation: 21 mutants; 20 are killed by the tests:

  • no bounds;
  • an element bounded by itself instead of its array;
  • bounds one element longer;
  • no formation index check, and no formation accessibility check;
  • difference operands not taken as subobject pointers;
  • the address keeping its generic place type;
  • copies taking no bounds, and a step resetting them;
  • no return or store escape check;
  • no alignment invariant;
  • an access allowed at the end, a step forbidden at it, and no lower bound;
  • differences across subobjects allowed;
  • call arguments unbounded, and a one-object argument of no bytes;
  • origin positions in the pointer's own elements;
  • field offsets read as pointers.

  The before_member and pass_end cases were added for mutants that first survived. The 21st mutant lets the bound companions have origins. It is equivalent, since no verdict can depend on it; the exclusion keeps the companions' "any byte" sentinel, 2^64, from being read by the origin analysis as a global's address.

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

• Merges: this merges cleanly with each open PR, 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.