[SwayamInSync]

A record kept in memory could not be used by value: a local object (every constructed object is one since #76) could not be passed or returned, and a record read as a whole through a pointer or reference could not be passed, returned, or copied. On the base (#76):

struct Counter {
  Counter(int l)
    cv::post(n == 0 && limit == l)
    : n(0), limit(l) {}
  int n;
  int limit;
};

int limit_of(Counter c)
  cv::post(cv::result == c.limit)
{
  return c.limit;
}

int passed()
  cv::post(cv::result == 6)
{
  Counter c(6);
  return limit_of(c);
}

Counter make(int l)
  cv::post(cv::result.n == 0 && cv::result.limit == l)
{
  Counter c(l);
  return c;
}

int through_pointer(const Counter *p)
  cv::pre(p != nullptr)
  cv::post(cv::result == p->limit)
{
  return limit_of(*p);
}

values.cpp:19:19: error: passed: aggregate value use of an automatic object is unsupported: c
values.cpp:26:10: error: make: aggregate value use of an automatic object is unsupported: c
values.cpp:33:3: error: through_pointer: unsupported aggregate field base expression

Now all three verify. Stacked on #76, the follow-up its "Open" section names.

Design

• A record value in memory is its fields (recordFieldsInMemory): a promoted local, or a record in the object a pointer or a record reference addresses, through implicit copies, moves, and temporaries, is one VLoadExpr per field at its offset from the place's address (objectPlace). Each load carries the place's access condition, which passivization asserts where the load is evaluated, and gets the memory checks of a load from UB instrumentation: in bounds, valid, initialized. So a copy reads what it copies, as C++'s implicit copy does, and fails where a field was never written.
• Where: a by-value argument (appendRecordCallArgument, so calls in expressions too, a spec's included), a record return (through a flattened __aggregate_return_N, assigned before the lifetimes of the locals end), and a copy into a flattened local (appendRecordCopy, which handled promoted locals and now uses the same reads, so pointees too).
• A record with a member that is a record or an array stays an error there, as before.

Tests

suite/record_values_in_memory.cpp (Z3, with a check that no proof is vacuous, and BMC):

• a constructed object passed by value, returned, and its result used;
• *p passed, copied, returned, and given to a spec in a postcondition; a record reference's referent passed and returned;
• an element of an array member through a pointer, in bounds; one past its array, which is still inside the object (items[2] would be count and spare), fails bounds;
• a copy of a local with a field never written fails initialization.

record_references.cpp: a record through a reference passed by value now verifies, where it was an error.

On the base every case is an error. Mutants, each built on an assertions build and run on record_values_in_memory.cpp, constructors.cpp, local_record_arguments.cpp, record_references.cpp, local_object_lifetime.cpp, and local_object_unsupported.cpp: 6 of 6 killed.

Mutant	Killed by
no records read from memory (the base)	record_values_in_memory, constructors
the place's access condition dropped	record_values_in_memory (past_element verifies)
arguments not read from memory	record_values_in_memory
returns not read from memory	record_values_in_memory
copies not read from memory	record_values_in_memory, constructors
records through pointers and references not read	record_values_in_memory (through_pointer)

Docs

• structs.rst: records through pointers read as a whole, a checked example (sum, sum_at); constructed objects by value; records by value.
• limitations.rst: whole-record reads narrowed to records holding arrays or records.
• Release notes: "Records in memory by value".
• DESIGN.md: 3b, 3g. ARCHITECTURE.md: records in memory by value.

Checked

• The Verify suite on a release build: 461 passed and record_references.cpp failed only its expectation of the error this PR removes (updated since), 1233 s with 40 workers.
• The doc pages' examples (structs, DESIGN): 34 checked, 0 failed; docs_examples.test and docs_coverage.test pass.