[SwayamInSync]

Real code declares a function with its contract in a header and defines it in one .cpp file. Before this PR, two things went wrong with that layout:

• Every caller in the other files was Unresolved [callee.contract], even when one run verified both files.
• The warning's advice, [[cppverify::trusted]] on the declaration, also stopped the verification of the definition, which inherits the mark through Clang's attribute inheritance. A wrong body was then never checked.

Now one run over several files settles such a contract. This is R26 from the plan:

// include/mathx.h
int clamp100(int x)
  cppverify::post(cppverify::result >= 0 && cppverify::result <= 100);

// src/mathx.cpp
#include "mathx.h"

int clamp100(int x)
{
  if (x < 0)
    return 0;
  if (x > 100)
    return 101;
  return x;
}

// src/a.cpp
#include "mathx.h"

int scaled(int x)
  cppverify::post(cppverify::result >= 0 && cppverify::result <= 200)
{
  return 2 * clamp100(x);
}

$ cpp-verify src/a.cpp src/mathx.cpp -- -Iinclude
Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in src/mathx.cpp does not establish)
include/mathx.h:2:42: error: verification failed: clamp100 [fn_...::postcondition@2:42] (counterexample: result [ssa=__result_1] [type=i32] = 101, x [ssa=x_0] [type=i32] = 101; ...) [backend=z3] [reason=counterexample]
Summary: 1 failed, 1 unresolved (callee.contract 1) in 0.0 s

With return 100; both functions verify, and the warning that clamp100 has no definition is not printed.

On the base (#97), scaled is Unresolved because clamp100 has "no definition", whether or not clamp100 is right. With the header's declaration marked trusted, mathx.cpp reports Trusted: clamp100 and the bug goes unchecked.

Stacked on #97. This is plan item E14, its first two steps: decision Q13, taken as recommended, (a); and one invocation over several files. Separate compilation with a link check, the third step, is left for later.

Design

• Trust stays on the definition (Q13). A function with a definition is trusted only when the definition carries the mark itself (!Attr->isInherited()). A declaration's mark means that callers which see no definition assume the contract. A spec still rejects the mark on any of its declarations.

• One run over several files. With more than one file, the driver creates a CrossFileRun. Each file is then handled as follows:

  • Provisional contracts. A contract the file declares without a definition holds provisionally (Verifier::Externals), instead of leaving its callers unresolved at once.
  • What each proof rests on. After the file's fixpoints, each proof records the external contracts it rests on, transitively through the file's own contracts' verdicts (ExternalOf).
  • What the file offers. Each contract the file verifies is offered with whether the file establishes it, and on which external contracts that rests (DefinedContracts).
  • Rendering. The file's results are rendered while its AST lives (renderReport). Each line is rendered as verified. A proof that rests on external contracts is also rendered as demote makes it, with a placeholder for the contracts. Both variants are counted for the summary.

• Settlement. Once every file is verified, CrossFileRun::finish establishes contracts by a least fixpoint, starting from none, as within a file. A contract is established once every definition of it is established in its file, and the external contracts that rests on are. It then prints each file's lines in the order given, with the demoted form where a contract a proof rests on is not established. The message says which of three cases applies:

  • a definition whose verification does not establish its contract;
  • one whose proof rests in turn on contracts not established (a cycle through files);
  • a declaration whose contract differs from the definition's.

  The settlement also drops the "no definition" warning of a contract some file defines, and the findings of a demoted proof (except those of the entry state, as within a file). Files with a demoted proof fail the exit status.

• Matching. A declaration matches a definition by the function's identity (its mangled name) and its contract as written, each clause printed by Clang (ASTConverter::contractText). A declaration that states another contract (an ODR violation) is not matched, which keeps it from borrowing a proof of a different claim.

• Unchanged. A file verified alone behaves exactly as before. A trusted declaration stays an assumption, flagged with [trusts=...]. Lean runs and --list-functions do not settle across files.

Tests

• suite/trusted_declarations.cpp (new): a header-style trusted declaration whose definition in the same file breaks the contract (now a failure, and its caller Unresolved), a trusted definition (still Trusted), a trusted declaration without a definition (assumed, [trusts=above]), and a spec with a trusted declaration (an error).
• suite/contracts_across_files.test (new, inputs in Inputs/across/):
  • R26 with a right definition (everything verified, no warning) and a wrong one (both callers Unresolved, transitively, and the definition's failure);
  • the files in the other order;
  • JSON;
  • a file alone, as before;
  • a declaration with another contract;
  • two files whose proofs rest on each other's contracts, which establish nothing and fail the run.

Each mutant below, applied alone, makes one of the two tests fail:

Mutant	Change
Q1	an inherited trust mark counts
Q2	a spec accepts a trusted declaration
X1	a contract without a definition is not provisional in a run over several files
X2	a proof rests only on its direct callees' contracts
X3	a file establishes every contract it verifies
X4	a contract rests on no other file's
X5	the "no definition" warning stays when a file defines the contract
X6	a declaration matches by the function alone, whatever its contract
X7	a file with a demoted proof succeeds
X8	a demoted proof counts as verified in the summary
X9	a run over several files settles nothing
X10	the files print in reverse
X11	a declaration with another contract reads as one without a definition

X6 is the soundness check of the matching. Under it, a declaration that promises result <= 50 borrows a proof of result <= 100, and its caller verifies.

Docs

• functions-loops.rst: the trust rules, and a new section "Contracts across files", with the example.
• tooling.rst: several files in one run.
• limitations.rst: contracts across files.
• Book ch17.
• Release notes.
• DESIGN.md: the decision and the settlement.
• ARCHITECTURE.md: how a run over several files holds and settles its files.

Checked

• lit of clang/test/Verify on this branch: 487 passed, 1 unsupported (darwin only), no failure, including docs_examples.test and docs_coverage.test with the new section.
• A file verified alone gives the output it gave on the base: every existing test passes unchanged.