[SwayamInSync]

A local record could not be lent to a callee, so a function over Counter & or Counter * could not be called on a local, which is what a method call on a local object will be. On the base (with #70), bump(c) on a local Counter c was

Unresolved: ... [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to bump, which may keep, offset, or free it, or has no verified body)

and reset(&c) an error (raw address-of is unsupported until lexical lifetime and escape effects are modeled). Now:

struct Counter {
  int n;
  int limit;
};

void bump(Counter &c)
  cv::pre(c.n < c.limit)
  cv::modifies(c.n)
  cv::post(c.n == cv::old(c.n) + 1)
  cv::post(c.limit == cv::old(c.limit))
{
  c.n = c.n + 1;
}

void reset(Counter *c)
  cv::pre(c != nullptr)
  cv::modifies(*c)
  cv::post(c->n == 0 && c->limit == 10)
{
  c->n = 0;
  c->limit = 10;
}

void set_n(Counter &c)
  cv::modifies(c.n)
  cv::post(c.n == 1)
{
  c.n = 1;
}

int counted()
  cv::post(cv::result == 11)
{
  Counter c;
  c.n = 0;
  c.limit = 5;
  bump(c);
  int k = c.n;
  reset(&c);
  return k + c.limit;
}

int half_initialized()
  cv::post(cv::result == 1)
{
  Counter c;
  c.n = 0;
  set_n(c);
  return c.n;
}

Verified: bump [backend=z3]
Verified: reset [backend=z3]
Verified: set_n [backend=z3]
Verified: counted [backend=z3]
counter.cpp:48:3: Unresolved: half_initialized [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, since the callee is verified as reading initialized storage)

Stacked on #70 (B3a-4 of plan item B3a).

Design

The scalar rule lends a local to a callee whose scan shows it only dereferences the parameter directly, because the caller frames the callee's whole-object footprint as the one cell at the address. A record has more than one cell, and the callee reaches them by offsets, which that scan rejects. But a callee verified in the object model already proves that every access through its parameter, at any field or element, lies in its object (the UB checks against the parameter's entry object). So what a record needs from the scan is only that no address of the local outlives the call: a borrow in Rust's sense, which Rust's borrow checker (and so Verus) enforces by types, and which here is checked on the callee's body.

• keepsNoAddress (Transform/Passivize.cpp) closes the parameter's aliases over the pointer variables assigned an address derived from one (copies, steps, subobject pointers, local references), to a fixpoint, and rejects: storing such an address in memory, returning it, freeing it, passing it to a callee that keeps one (scanned the same way; its valid extent is allowed there, since the function passing it proved the extent inside its own object) or that returns a pointer, and a callee without a verified body (an external contract, a proof, or a function that allocates). A scan that reaches itself again through recursion assumes the callee keeps none: an escape is a finite path to a statement that keeps an address. Converting an address to an integer is no escape, since the frontend rejects every cast back to a pointer; the generated subobject invariant q % S == q.__lo % S does exactly that.
• VFunction::RecordParams names the pointer and reference parameters to a record, with the identity of its layout. A provenance-backed actual for one takes keepsNoAddress (only when the caller is in the object model); every other provenance-backed actual keeps the scalar scan.
• At the call (emitRecordActualChecks): the generated validity clause names the record's first byte; the call also asserts the validity of its last byte, which puts the whole record in the first byte's live allocation (an allocation's bytes are contiguous), and the initialization of every leaf of the callee's layout, as an unsupported obligation with the out-parameter note, as a scalar out-parameter already is. Before, only the first leaf was checked, so a callee would have read a partly initialized record as initialized.
• Frames (havocFootprints): a footprint rooted at a record parameter is framed by its bytes (footprintBytes, a HeapFrame or cell stores), a region as the whole record and never only the exact first cell of the scalar rule. The caller's frame check accepts footprints in its own allocations; its alternative for an empty range replaced that disjunction instead of joining it, so a callee's range in the caller's own record failed frame (clear(r) with modifies(r.buf[0 : 4])). On the base no actual reached it: the scalar scan rejects such a callee.
• The converter lowers &place rooted at a promoted local, not an array, passed to a pointer parameter, as it lowers a reference argument: the address with its provenance, the element access condition, and the binding check. &x of a scalar local takes the scalar rule. Stored in a variable, &x is still an error.

What stays out

• A local not fully initialized passed to a callee (construct.unsupported, as for scalars).
• A decayed local array passed to a buffer callee (first(local.buf, 4)): the scalar scan rejects its offsets. Inside a lent record it works, since nested calls take keepsNoAddress.
• --no-check-ub: nothing proves the callee's accesses inside its object, so a record local passed to a callee is construct.unsupported.

Tests

suite/local_record_arguments.cpp, with Z3, BMC, --no-check-ub, and a Layer 2 dump:

• a local record by reference and by address, a member (bump(p.left)), an element (bump(a[1])), &c.n and &x to a scalar pointer parameter; the other field and other locals keep their values; a wrong result fails;
• callees that forward the reference (twice), walk a member array with a pointer (for (int *q = r.buf; ...)), pass a decayed member to a buffer callee, and recurse;
• a range footprint in the caller's own record (clear), and a caller whose own modifies names only its out-parameter;
• two locals are disjoint, one passed twice fails aliasing;
• construct.unsupported for a partly initialized record; a callee that stores the address in the record, stores a copy of it, forwards it to one that stores it, or returns it; a callee with a valid extent (it could write past the local); and a callee without a body, called directly or through another;
• Layer 2: the last byte's validity and both leaves' initialization at the call.

record_references.cpp now expects its local passed by reference to verify.

Mutants, each built and run on local_record_arguments.cpp and record_references.cpp (the first sweep also on the seven local, reference, and dynamic-storage tests beside them): 14 of 14 killed.

Mutant	Killed by
stores of the address allowed	local_record_arguments
returns of the address allowed	local_record_arguments
copies are not the address (no alias closure)	local_record_arguments
callees it is passed to are not scanned	local_record_arguments
callees without a body accepted (nested)	local_record_arguments
recursion rejected	local_record_arguments
an extent offered to a local	local_record_arguments
records take the scalar scan (the base)	local_record_arguments, record_references
no initialization check of the leaves	local_record_arguments
only the first leaf checked	local_record_arguments
no validity of the last byte	local_record_arguments
a record's region framed as its first cell	local_record_arguments
the empty-range alternative replaces owned storage (the base)	local_record_arguments
&local rejected (the base)	local_record_arguments

The first sweep left two rules surviving because they were redundant, and both are gone: rejecting a callee that returns a pointer (the callee's own scan rejects returning the address), and a scan of delete and new statements (a function with either is UsesDynamicStorage, rejected before its statements are scanned, which the scan now says).

Docs

• structs.rst: "Local records passed to callees", a checked example (four verified, the out-parameter construct.unsupported), what the call checks, what stays out.
• ch14, limitations.rst: locals and &x as arguments.
• Release notes: "Local objects passed to callees".
• DESIGN.md: 3d. ARCHITECTURE.md: the scan, the call's checks, framing, the frame-check fix.

Checked

• The Verify suite on a release build: 454 passed (the exhaustive decoder filtered out), 1201 s with 40 workers.
• After the last change (the two redundant rules, formatting, four test cases): the 13 local, reference, dynamic-storage, subobject, and docs tests pass, and the four mutants they were written for are killed.
• The doc pages' examples (structs, ch14, pointers, DESIGN): 65 checked, 0 failed.
• local_record_arguments.cpp fails under each mutant that restores a rule of the base: the scalar scan for records, &local rejected, and the empty-range alternative replacing owned storage.