[SwayamInSync]

Plan item B5 (helpers without contracts), decision Q10 (a): a call of a function without a contract stopped its caller, the most common first error users hit. Stacked on #118 (B13, on #117 and #116), whose commits it shows until those merge.

On the base

int count_zeros(const int *a, int n)
{
  int c = 0;
  for (int i = 0; i < n; i = i + 1)
    cv::invariant(0 <= i && i <= n && 0 <= c && c <= i)
    cv::decreases(n - i)
  {
    if (a[i] == 0)
      c = c + 1;
  }
  return c;
}

int zeros(const int *a, int n)
  cv::pre(valid(a, n) && 0 <= n && n <= 1000)
  cv::post(0 <= cv::result && cv::result <= n)
{
  return count_zeros(a, n);
}

int zeros_past(const int *a, int n)
  cv::pre(valid(a, n) && 0 <= n && n <= 1000)
{
  return count_zeros(a, n + 1);
}

zeros.cpp:22:10: error: zeros: call to function without a verification contract: count_zeros
zeros.cpp:28:10: error: zeros_past: call to function without a verification contract: count_zeros
zeros.cpp:9:31: error: verification failed: count_zeros [invariant-entry] [backend=z3] [reason=counterexample]
zeros.cpp:9:31: note: counterexample: a = 1, n = -1, c = 0, i = 0

Both callers stop, and the helper, verified on its own because it has a loop contract, fails at n = -1, which no caller passes.

With this PR

Verified: zeros [backend=z3]
zeros.cpp:12:9: error: verification failed: zeros_past [bounds] [backend=z3] [reason=counterexample]
   12 |     if (a[i] == 0)
      |         ^
zeros.cpp:12:9: note: counterexample: count_zeros::a = 1, count_zeros::n = 2, count_zeros::c = 0, count_zeros::i = 0 -> 1, a = 1, n = 1
...
note: an execution fails this check within 1 iteration of each loop (counterexample: count_zeros::a = 1, count_zeros::n = 1, count_zeros::c = 0, count_zeros::i = 0, a = 1, n = 0)

A call of a function with a body and no contract runs that body: the caller's proof covers it at the arguments the caller passes, its checks are the caller's, and it reads and writes the caller's objects within the caller's frame. count_zeros has no verdict of its own: a function without a contract is verified where verified code calls it, and on its own only when none does.

Design, from the references

• Kani and CBMC inline every call; SPARK's GNATprove inlines a subprogram without a contract at its calls ("contextual analysis of subprograms without contracts") and does not analyze it on its own. Dafny, Verus, and Frama-C's WP require a contract of every callee, which is what cpp-verify did. The rule here is SPARK's: a contract is the interface when there is one, the body when there is not.
• At the VCR level, after conversion, as SpecInliner does for specs. The converter lowers a call of a helper as it lowers a contracted call (lowersToCall, hoistExecCall, the call statements), so the arguments are evaluated in C++'s order (B9, B11), and atCall marks it InlinesHelper. After the main loop it converts each helper once (convertFunction(FD, /*AsInlineHelper=*/true), IsInlineHelper). inlineHelperCalls (Transform/InlineHelpers.cpp, new) then runs in the converter, before the call-graph analyses, so recursion groups, clusters, spec dependencies, origins, UB instrumentation, and passivization all see the inlined code, and no pass after it needed a change.
• Returns without a new statement kind. The body is cloned and renamed apart (__inline1_find$i); each parameter becomes a local assigned its argument. Each return e becomes result = e; returned = true; outside loops what follows a statement that may return is guarded by !returned, inside a loop the return also breaks, a loop that may return is followed by if (returned) break; in an enclosing loop, and each such loop gets the generated invariant !returned, proved like any other (a path that sets it leaves the loop at once). The body's result is a local of the helper (__inline1_find$__result), given a value of its type before the body and copied to the call's target after it, so that a value assigned on a loop's return path reaches the loop's exit (the passivizer treats a variable first assigned in a loop as the loop's own; without it index_of below failed with an arbitrary result). Havocking it instead had no type in the passive program (invalid sort with nested loops).
• Facts that travel. The caller receives the helper's source variables (shown as count_zeros::i), bounded pointers, spec dependencies, decreases(*) (the caller is [partial]), an unmeasured loop (decreases.missing), and its extent, so that a failure's focus inside the helper is shown (x + 1, not the return).

Fail closed

Each case below is Unresolved with construct.unsupported, at the call, with a message that names the helper and asks for a contract; the path ends there, so no other check of the caller can fail on a value the call would have produced:

• recursion: down has no contract and calls itself, so its body cannot be inlined; give it a contract, and through others, the functions without contracts even -> odd -> even call each other, ...;
• a record returned by value (a record parameter is its fields, and a pointer or reference to one, this included, addresses the caller's object);
• allocation, deallocation, or a pointer to dynamic storage as the result;
• cppverify::old or cppverify::result in the body, whose entry would be the caller's;
• a body that does not convert, whose first error is repeated: with_goto has no contract, and its body cannot be inlined (with_goto: goto is unsupported at 331:5); give it a contract;
• more than 2000 statements inlined into one function: its whole body becomes the obligation, at the call of the outermost helper (give h10 a contract), since a partly inlined body only grows the queries (with the budget at 10000, a chain of helpers that call two helpers each reached the 4-million-node query limit first, with a message that does not say why).

Unchanged: a constexpr function without a contract is still lifted as a spec, a constructor without a contract is not inlined, and a function without a body, of the standard library, or of a system header is still call to function without a verification contract.

Tests

• suite/inline_helpers.cpp (new), 28 functions: a scalar helper verified under one caller and failing under another (overflow at the helper's x + 1, with add_one::x in the counterexample); early returns (sign, its exact value, and a false claim); writes through a pointer within the caller's frame, outside it (frame), and past its extent (bounds); a loop with its invariant at the caller's extent and one past it; a return inside a loop (find) and a false claim about it; helpers calling helpers and contracted functions, whose precondition fails at a helper's call (precondition); member functions reading and writing their object; a helper's cppverify::check; a record parameter; a helper's local named like the caller's; every fail-closed case above, with its message; the budget; and a Layer-1 dump of the inlined loop (the renamed locals, the flag, its invariant, the break). QUIET-NOT checks that no helper gets a verdict of its own.
• suite/unused_template.cpp: a call of a function template without contracts now verifies through its body.

On the base the test's file gives 1 verified, 4 failed, 27 unresolved (construct.unsupported 27).

On a release build of this branch, the whole Verify suite passes (509 of 510, one unsupported).

Mutants

Each mutant below, applied alone to the converter or the inliner and rebuilt, is caught by inline_helpers.cpp or unused_template.cpp (17 of 17):

Mutant	Change
M1	no call is inlined
M2	no invariant keeps the return flag clear in a loop
M3	the result has no value before the body
M4	a return in a loop does not break
M5	what follows a statement that may return is not guarded
M6	the body's names are not renamed apart
M7	no break after an inner loop that returns
M8	helpers are verified on their own too
M9	a call that is not inlined does not end its path
M10	the helpers' extents are not the caller's
M11	no budget
M12	a body with cppverify::old is inlined
M13	the helper's result is shown in counterexamples
M14	recursion is not detected
M15	every helper may write (the purity scan says yes)
M16	no helper writes (the purity scan says no)
M17	the fuel a helper reveals stays its own

M9 survived a first run: every caller in the test that keeps a failed call is Unresolved either way, so verdicts alone do not show whether its path ends. The test now dumps use_mid, whose call of a helper returning a record is not inlined, and checks the assume false after its assert unsupported.

Docs

• Functions and loops: a section, "Calls of functions without contracts", with the example and its output, the rule, and what needs a contract;
• limitations: the supported column, the cases that need a contract, and the C library paragraph;
• the book: chapter 17, "Calls of helpers without contracts", with an example and its output; chapter 11;
• release notes; DESIGN; ARCHITECTURE ("Inlined Helpers").

check-doc-examples.py passes on every changed page.

Not done

• A note naming the call a failing helper was inlined from: the failure is shown at the helper's operation, in the caller's verdict, with the helper's variables, but the path does not show the call (it needs a trace step of its own in the VCR, which every pass would then carry).
• Records returned by value, dynamic storage, cppverify::old in a helper's invariant (its entry state would need a snapshot at the call), constructors, and constexpr helpers with loops.
• The note on a contracted callee, (its precondition is assumed, not checked, at calls from unverified h), still names helpers, which is true of their calls from code the verifier does not verify, but not of the calls inlined into verified code.