[SwayamInSync]

A record that describes a buffer by a pointer and a length (a string view, a span) could not state the buffer's extent. On the base (with #71):

error: zero: valid marker requires a bare complete-object pointer and an integer element count

Now cv::valid(b.data, b.len) is the extent of the buffer the field addresses:

struct Buf {
  int *data;
  int len;
};

void zero(Buf &b)
  cv::pre(cv::valid(b.data, b.len) && 0 <= b.len)
  cv::modifies(b.data[0 : b.len])
  cv::post(cv::forall(k, 0, b.len, b.data[k] == 0))
{
  for (int i = 0; i < b.len; i = i + 1)
    cv::invariant(0 <= i && i <= b.len)
    cv::invariant(cv::forall(k, 0, i, b.data[k] == 0))
    cv::modifies(b.data[0 : b.len])
    cv::decreases(b.len - i)
  {
    b.data[i] = 0;
  }
}

void zero_prefix(int *p, int n, int k)
  cv::pre(cv::valid(p, n) && 0 <= k && k <= n)
  cv::modifies(p[0 : n])
  cv::post(cv::forall(j, 0, k, p[j] == 0))
{
  Buf b;
  b.data = p;
  b.len = k;
  zero(b);
}

void zero_more(int *p, int n)
  cv::pre(cv::valid(p, n) && 0 <= n && n < 100)
  cv::modifies(p[0 : n])
{
  Buf b;
  b.data = p;
  b.len = n + 1;
  zero(b);
}

Verified: zero [backend=z3]
Verified: zero_prefix [backend=z3]
buf.cpp:39:3: error: verification failed: zero_more [...::bounds@39:3] (counterexample: n [ssa=n_0] [type=i32] = 0, p [ssa=p_0] [type=pointer] = 1; trace: ... -> call.zero@39:3 arg0=231056) [backend=z3] [reason=counterexample]

Stacked on #71 (B3a-5, the last part of plan item B3a; zero_prefix lends a local Buf to zero, which is #71).

Design

• The field's entry value is an input. An extent is a fact about a pointer the function receives. A field's value at entry is received as a parameter's is, the way Frama-C names it \at(s->data, Pre), so the field gets a synthetic parameter after the declared ones: s->data (VFunction::FieldParams, fields joined by ->), displayed as written, b.data for a reference. It is the field's value at entry by definition: enter assumes s->data_0 == load(s + offset) in the entry heap, an entry fact without definedness (it says nothing where the field cannot be read) that no caller establishes, since a call binds the parameter in ParamMap to the field at its arguments. The marker's argument converts to the parameter, so instrumentUBChecks sees a bare pointer and records the extent, its validity clause, and the bounds checks exactly as for a parameter.
• Which fields (pointerFieldOfParameter): a pointer to a complete object type, a field of the object a pointer or reference parameter addresses, nested fields included: s->f, r.f, (*s).f, s->inner.f. A field of an array element (s->items[k].f) keeps the marker error.
• In the body an access through the field has no known origin (it is read from memory), so it must lie in some parameter's object, which now includes the field's extent; where the field still holds its entry value, the solver relates the two through the heap. A field given another pointer addresses that pointer's object.
• At a call the field's value at the arguments must have the extent in the caller's objects, as an extent argument must; the bound value also serves as the argument whose origins (unknown) place it.
• Separation. The default separation of address parameters takes the synthetic entries (AddressEntry, mutable unless the field points to const; the marker's parameter converts the argument to a pointer to const, so the field's own type decides): a mutable buffer is disjoint from the other address parameters' objects, its own record's included, so b.data[i] = 0 leaves b.len alone; two buffers through pointers to const may be one.
• Found and fixed: empty extents next to other objects. DESIGN says that two address parameters of which one has a valid extent are disjoint "unless either pointer is null or either extent is empty". The extent separation said so, but the pair's one-object separation was required as well, so an empty extent into another object (touch(b, &b->len, 0)) failed aliasing, and so did a local Buf holding a zero-length extent of a parameter. dropSingleObjectSeparation removes a pair's one-object separation where one of them has an extent; a pointer with an empty extent reaches nothing, so the fact it carried was never used.

Tests

suite/pointer_field_extents.cpp (Z3, BMC, VCR):

• reads and writes through v->data, b.data (a reference), p->out.data and p.out.data (nested fields), each bounded by its extent (past fails bounds); a field without an extent is no object (unknown fails bounds);
• the length keeps its value across writes to the buffer (separation from the record);
• calls: the callee's extent from the caller's field extent, from the caller's own parameter through a local Buf, and one element too long (bounds at the call);
• a field given another pointer addresses that pointer's object (one past it fails bounds);
• two mutable buffers are disjoint (copy verifies, copy(b, b) fails aliasing), two const views may be one;
• an empty extent into another object (empty_inside verifies, nonempty_inside fails aliasing);
• a field of an array element keeps the marker error;
• VCR: the synthetic parameter after the declared ones.

extent_separation.cpp now expects one aliasing assert at a call between two extents, their separation, where it expected the first elements' separation as well.

Mutants, each built and run on pointer_field_extents.cpp, extent_separation.cpp, record_references.cpp, and local_record_arguments.cpp: 11 of 11 killed.

Mutant	Killed by
no field extents (the base)	pointer_field_extents
no entry fact binding the parameter	pointer_field_extents
no binding at calls	pointer_field_extents
no argument for the extent containment of a field	pointer_field_extents
field buffers not in the separation	pointer_field_extents
field buffers taken as read-only	pointer_field_extents
mutability read from the marker's converted type	pointer_field_extents
the one-object separation kept (the base)	pointer_field_extents, extent_separation
references not field roots	pointer_field_extents
nested fields not roots	pointer_field_extents (p.out.data, added for it)
the one-object separation dropped for pairs without an extent	pointer_field_extents, local_record_arguments, record_references

Docs

• structs.rst: "Extents of pointer fields", a checked example.
• pointers.rst, ch14, ch18, limitations.rst: the marker's forms, separation over extents.
• Release notes: "Extents of pointer fields"; "An empty extent inside another object" (failures that were not real).
• DESIGN.md: 3e, the marker, the separation rule. ARCHITECTURE.md: field extents, the separation drop.

Checked

• The Verify suite on a release build: 454 passed, and extent_separation.cpp failed only its Layer 2 check of the second aliasing assert, which this PR removes (every verdict of it unchanged, the --no-check-ub run, where extents fold away and the element separation remains, included); 1202 s with 40 workers.
• After the test updates and formatting: the 7 extent, reference, subobject, and docs tests pass.
• The doc pages' examples (structs, pointers, ch14, ch18, DESIGN): 76 checked, 0 failed.