[SwayamInSync]

Passing storage that is not initialized yet to a function that writes it before reading it was Unresolved [construct.unsupported] (#35): every pointer and reference parameter required initialized storage. C++ requires no such thing, since binding a reference or passing a pointer reads nothing ([dcl.init.ref], [basic.indet]). Now a parameter whose storage the body writes before it reads it is an out-parameter, and callers may pass it storage not yet initialized:

namespace cv = cppverify;

struct Pair {
  int a;
  int b;
};

void init_ref(int &r)
  cv::modifies(r)
  cv::post(r == 0)
{
  r = 0;
}

bool try_get(int &out, bool ok)
  cv::modifies(out)
  cv::post(!cv::result || out == 5)
{
  if (!ok)
    return false;
  out = 5;
  return true;
}

void make_pair(Pair &p)
  cv::modifies(p)
{
  p.a = 1;
  p.b = 2;
}

int array_out()
  cv::post(cv::result == 0)
{
  int a[2];
  init_ref(a[0]);
  return a[0];
}

int got(bool ok)
  cv::post(cv::result == 5 || cv::result == 0)
{
  int a[1];
  bool found = try_get(a[0], ok);
  if (found)
    return a[0];
  return 0;
}

int made()
  cv::post(cv::result == 0)
{
  Pair p;
  make_pair(p);
  int s = p.a;
  return 0;
}

int missed()
  cv::post(cv::result == 0)
{
  int a[1];
  try_get(a[0], false);
  return a[0];
}

Verified: init_ref [backend=z3]
Verified: try_get [backend=z3]
Verified: make_pair [backend=z3]
Verified: array_out [backend=z3]
Verified: got [backend=z3]
Verified: made [backend=z3]
out.cpp:64:3: error: verification failed: missed [fn_...::initialization@64:3] (counterexample: trace: allocation.automatic allocation@62:3 address=4948 provenance=6 -> call.try_get@63:3 arg0=4948 arg1=false) [backend=z3] [reason=counterexample]

On the base (#82):

out.cpp:36:3: Unresolved: array_out [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)
out.cpp:44:3: Unresolved: got [backend=z3] [reason=construct.unsupported] (...)
out.cpp:54:3: Unresolved: made [backend=z3] [reason=construct.unsupported] (...)
out.cpp:63:3: Unresolved: missed [backend=z3] [reason=construct.unsupported] (...)

Stacked on #82. Plan item A23 (F42, R33), the 0.2 form after #35's fail-closed one.

Design

The contract follows from the body, as freshOwnedReturn does (C# out parameters by definite assignment are the model), and the body is verified against it, so a wrong classification can make a proof fail but never make one wrong.

• Classification (Transform/OutParameters.cpp, inferOutParameters, run on the converted functions after inferFreshOwnedReturns). For each pointer or reference parameter of a function with a verified body (not a constructor's this, never assigned), a walk keeps the byte offsets from the parameter written on every path: a branch joins by intersection, a loop adds nothing after it, a return records the exit state. The parameter is an input when the walk finds a read of an offset not written, a read at a computed offset (p[i]), any use of the pointer other than an access, a null test, valid_ptr, or an address step (a copy, a store, a return, a comparison), a call passing it to a callee parameter that is not an out-parameter whose leaves are not all written (or that has an extent, or whose callee has no verified body), or a read of the entry state in a clause: preconditions (a class invariant is one), recommends, the measure, behaviors, old. Postconditions, invariants, and cppverify::check describe what the body wrote, so the verifier checks their reads instead; but if the function never writes the storage they read the caller's values, and the parameter is an input (max_index reads its array only in its postcondition).
• Two fixpoints. The leaves each function writes on every path are a least fixpoint (a call writes the callee's leaves at the argument's offset; nothing rests on an induction the walk does not do); the out-parameters a greatest one (a recursive call passing the storage on reads nothing).
• Contract. The generated validity precondition loses initialized_ptr; the converter's subobject binding pair (assert the object initialized, assume the part initialized) is removed for out-parameters, since binding reads nothing; each leaf written at every exit becomes a generated postcondition initialized_ptr(p + k) of kind initialization, which generalizes a constructor's exit checks. --dump-ir=1 prints param p out.
• Callee. tracksInitialization: provenance, or based on an out-parameter (source name or entry version). Stores set the initialization bit, loops count the initialization heap as modified (so the head keeps what was initialized and assumes the invariants' definedness), loads check initialized_ptr at the exact address (also under --no-check-ub), and so do the reads of postconditions at exit. Validity, frames, and origins stay those of any parameter.
• Caller. Where an out-parameter's argument is tracked storage (a local, dynamic storage, or the caller's own out-parameter), the call gives the initialization heap a fresh version that keeps everything initialized (initialization only grows), assumes the postconditions with the generated ones, then the initialization checks of each postcondition's reads, with the call's origin, so post(!result || out == 5) gives initialized storage where the result is true. A call in a loop counts as modifying the initialization heap. emitRecordActualChecks skips the per-leaf check for an out record parameter.
• Inputs keep the fail-closed rule; its note now reads "which the callee may read before writing it". Two guards keep verdicts right should the classification err: abstractValidity keeps initialized_ptr on tracked storage, and a caller's own out-parameter passed to an input record gets the per-leaf checks.
• Constructors (found by constructors.cpp). A constructor calling a member function that writes its object failed with a certified counterexample on main once the member was initialized (Resets() : v(1) { reset(); }: pointer-validity@6:5#2, and behind it frame): the record argument's last-byte check had no fact about the constructor's own object, and the entry state's this lost its lifetime companion, so the frame *this and the argument this were different objects. The constructor's precondition now includes its last byte (which its callers already prove), and the entry state's this keeps the companion (VConstructedObjectLifetime, now in the IR). Calling such a member before the members are initialized is fine now when its object is an out-parameter.

Not changed: external and trusted callees (their parameters are inputs), returned pointers (UninitializedResultNote), constructors' this.

Tests

• suite/out_parameters.cpp (Z3, with a check that no proof is vacuous; Layer 1 dumps; --no-check-ub), rewritten: local, array-element, and heap storage passed to out-parameters; a function written on every path with no postcondition (set_some); written on one path with a postcondition saying where (try_get), and a read after a miss that fails initialization; write then read (write_then_update); inputs: read on a path first, read by the precondition, under old, passed to a reading callee first, through a trusted callee, through a pointer copy (alias_reads_garbage stays Unresolved); pass-through to another function's out-parameter; records written field by field, through field references, and partly written (reads_unmade fails initialization); a postcondition about storage never written (an input) and one written on a path (set_if fails); loops in the callee and in the caller, across iterations; recursion; null tests; array filling and pass-through (fill_three fails); a member function writing *this.
• local_record_arguments.cpp: out_parameter verifies; a reading callee with a partly initialized record stays Unresolved.
• constructors.cpp: Resets::Resets verifies; a member function that reads its object first, called before initialization, stays Unresolved.
• region_frames.cpp: claims_too_much, whose p is written only through a callee, fails initialization at the cell its postcondition reads.
• local_reference_lowering.cpp, shared_logic_terms.test: the passive form and node count of a call to an out-parameter.

The six fail on the base (each run with the base verifier): scalar_out and the other new verdicts, out_parameter, Resets::Resets, claims_too_much's initialization, the passive forall __init_address, and the node count.

Mutants, each built on an assertions build and run on the six tests and record_references.cpp, nested_quantifier_counterexamples.cpp, and pointer_subobjects.cpp: 24 of 26 killed; the two guards survive alone, as the classification never lets them decide, and kill their combinations.

Mutant	Killed by
no out-parameters	out_parameters, constructors, local_record_arguments, local_reference_lowering, region_frames
an unwritten read is no read	out_parameters, record_references
other uses of the pointer are no uses	out_parameters (alias_reads_garbage)
a reading callee reads nothing	out_parameters (read_then_write: the call-site guard), record_references
preconditions read nothing	out_parameters, region_frames
old reads nothing	out_parameters, region_frames, record_references, pointer_subobjects
storage never written, read by a contract, is no input	out_parameters, pointer_subobjects, record_references, nested_quantifier_counterexamples
no generated postconditions	out_parameters
a branch joins by union	out_parameters (try_get)
a loop writes on every path	out_parameters (zero_each)
a call writes nothing	out_parameters (set_twice)
the binding initialization kept	out_parameters (make_by_parts), record_references
initialization still required	out_parameters, constructors
stores do not initialize an out-parameter	constructors, local_record_arguments, out_parameters, record_references, region_frames, local_reference_lowering, pointer_subobjects
loads not checked	out_parameters, region_frames
loops keep the initialization heap	out_parameters, local_record_arguments, region_frames
no fresh initialization heap at a call	out_parameters, local_reference_lowering
postconditions give no initialization	out_parameters (got)
calls in loops keep the initialization heap	out_parameters (init_once_in_loop)
record out-parameters need initialized leaves	local_record_arguments, out_parameters, record_references, constructors
no last byte in a constructor's precondition	constructors (Resets)
the entry this without its lifetime	constructors (Resets: frame)
guard: tracked initialization taken as true	survives alone; with "a reading callee reads nothing", out_parameters (write_a_then_read, by the other guard)
guard: tracked record arguments unchecked	survives alone; with "a reading callee reads nothing", out_parameters (read_then_write, by the other guard)

Docs

• pointers.rst: "Out-parameters" rewritten: the rule, what the function and its callers get, a checked example (init, try_get, copy_to), what stays unsupported.
• structs.rst: record arguments and member calls in constructors; the counter.cpp example now verifies half_initialized and shows a reading callee Unresolved.
• limitations.rst, release notes ("Out-parameters").
• DESIGN.md: "Out-parameters" under references, record calls, constructors. ARCHITECTURE.md: inferOutParameters, the passivizer's tracking, record calls, the constructor's this.

Checked

• The Verify suite on a release build: 468 passed (the exhaustive decoder filtered out), 1270 s with 40 workers.
• The doc pages' examples: docs_examples.test and docs_coverage.test pass; the edited pages' 60 examples check, 20 against the verdicts they show; the site builds with warnings as errors.