[SwayamInSync]

#98 settles contracts across files when one run verifies them all. A build verifies each object on its own, though: clang++ -fverify-contracts -c src/a.cpp sees clamp100 declared without a definition. Before this PR such a run could only warn about the contract and leave every caller that relies on it Unresolved [callee.contract]. Nothing ever checked those callers against the definition's verification in src/mathx.cpp.

Now each file verified apart can record its contracts, and one check settles the records, as the link settles symbols. This is the third step of plan item E14. On R26 (#98's example), with the wrong definition return 101;:

$ clang++ -fverify-contracts -fverify-contracts-out=a.o.cppverify -c src/a.cpp -o a.o -Iinclude
Verified: scaled [backend=z3] [assumes=clamp100]
$ clang++ -fverify-contracts -fverify-contracts-out=mathx.o.cppverify -c src/mathx.cpp -o mathx.o -Iinclude
include/mathx.h:2:42: error: verification failed: clamp100 [...]
$ cpp-verify --check-contracts a.o.cppverify mathx.o.cppverify
src/a.cpp:3:5: error: the proof of scaled relies on the contract of clamp100, which its verification in src/mathx.cpp does not establish
Contracts: 1 proof rests on contracts of other files, 1 on one not established

The check exits non-zero. With return 100; it prints Contracts: 1 proof rests on contracts of other files, 0 on one not established and exits 0. cpp-verify --contracts-out=FILE records one file the same way.

On the base (#98), compiling a.cpp warns that clamp100 has no definition and reports scaled as Unresolved [callee.contract], whether or not clamp100 is right.

Stacked on #98.

Design

• Recording a file. --contracts-out=FILE, or -fverify-contracts-out=FILE on the compiler, makes a file's contracts declared without a definition hold provisionally, exactly as in a run over several files (Verifier::deferredContracts).
  • Each proof that rests on such a contract says so in its verdict, as [assumes=clamp100], so the file's own output never presents it as settled.
  • The "no definition" warning is not printed, since the check decides it.
  • recordContracts then writes a cppverify.contracts/1 JSON record:
    • defined: each contract the file verifies, with its key (identity and contract text, as in E14: contracts across the files of one run, and trust that stays on the definition #98), its name, whether the file establishes it, and the other files' contracts that rests on;
    • proofs: each proof that rests on contracts of other files, with its function, the location of its declaration, and those contracts.
• The check. cpp-verify --check-contracts RECORD... reads the records and settles them with the least fixpoint of E14: contracts across the files of one run, and trust that stays on the definition #98, now the class ContractSettlement, which CrossFileRun::finish uses too. So files verified apart are settled exactly as one run over them would be.
  • It prints each proof that relies on a contract not established, at the proof's function. The message says which of three cases applies, as in E14: contracts across the files of one run, and trust that stays on the definition #98:
    • the definition's verification does not establish the contract;
    • its proof rests in turn on contracts not established (a cycle through files);
    • no record defines it.
  • It then prints a line counting the proofs that rest on other files and how many of them rest on a contract not established. The exit status is non-zero when there is one.
  • A file that is not a record is an error.
• One file per record. --contracts-out with several sources is an error, since a run over several files settles their contracts itself.
• The compiler path. -fverify-contracts-out is a driver option that is forwarded to -cc1 (FrontendOptions::VerifyContractsOut). CodeGenAction passes it to startCppVerifyAsync, which writes the record once the compile-time verification ends.

Tests

suite/contracts_link_check.test (new) reuses #98's inputs and covers:

• APART: each file recorded apart, and [assumes=clamp100] on the proofs that rest on it, with no warning.
• WRONG and RIGHT: the check against the wrong and the right definition.
• MISSING: a contract that no record defines.
• The compiler path: clang -fverify-contracts-out, then the check against the right and the wrong definition, the failure located at the proof's function.
• CYCLE: two files whose proofs rest on each other's contracts.
• NOT-RECORD: a file that is not a record.
• SEVERAL: --contracts-out with several sources.

Each mutant below, applied alone, makes the test fail:

Mutant	Change
L1	a recorded file does not hold its external contracts provisionally
L2	proofs that rest on other files are not tagged [assumes=...]
L3	the record lists no proofs
L4	a defined contract is recorded as established whatever its verification
L5	the check ignores what a defined contract rests on
L6	the check exits 0 whatever it finds
L7	the compiler records nothing
L8	a proof is reported without a location
L9	the "no definition" warning stays in a recorded file
L10	a file that is not a record is ignored
L11	several files may share one record

L7 survived its first run, which tested the mutated build's cpp-verify with the unmutated clang; with the mutated clang it fails the test.

Docs

• functions-loops.rst: files verified apart, with the example.
• tooling.rst: both options and the record's contents.
• limitations.rst: contracts across files are no longer a limitation for separate runs.
• Book ch15: the options.
• Book ch17: a pointer to the check in modular calls.
• Release notes: an entry for the check.
• DESIGN.md: the decision.
• ARCHITECTURE.md: the record, the shared settlement, and the compiler path.

Checked

• lit of clang/test/Verify on this branch: 488 passed, 1 unsupported (darwin only), no failure. Its compiler-path lines ran a clang linked before the last change to the record's locations, which the check of the wrong definition through the compiler now catches. With clang rebuilt, contracts_link_check.test, contracts_across_files.test, trusted_declarations.cpp, docs_examples.test, and Driver/verify_contracts.cpp pass.
• The example above, run as shown.
• A file verified alone without --contracts-out, and every run over several files, gives the output it gave on the base: every existing test passes unchanged.