diff --git a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py index 359b8cb7d5..46ac53062f 100644 --- a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py +++ b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py @@ -147,13 +147,17 @@ def function_records(records): return selected -def check_matrix(records, backend): +def check_matrix(records, backend, replay=False): + # Replay proves each module alone, without the verdicts it rests on. + proved = "proved-obligations" if replay else "verified" selected = function_records(records) for name, expected in EXPECTED_STATUS.items(): + if expected == "verified": + expected = proved record = selected[name] actual = record.get("status") if backend in {"cvc5", "portfolio"} and name in CONSERVATIVE_CVC5: - if actual == "verified": + if actual == proved: continue if actual != "unresolved" or record.get("reason") != "solver.unknown": fail( @@ -365,7 +369,7 @@ def check_archive_matrix(cpp_verify, source, work, source_records): replayed = parse_json_lines( run(replay_command(cpp_verify, backend, canonical), {1}) ) - selected = check_matrix(replayed, backend) + selected = check_matrix(replayed, backend, replay=True) for name in INVALID_FUNCTIONS: if diagnostic_identity(selected[name]) != diagnostic_identity( function_records(source_records[backend])[name] @@ -383,7 +387,7 @@ def check_archive_matrix(cpp_verify, source, work, source_records): replayed_bmc = parse_json_lines( run(replay_command(cpp_verify, "bmc", bmc_archive), {1}) ) - selected_bmc = check_matrix(replayed_bmc, "bmc") + selected_bmc = check_matrix(replayed_bmc, "bmc", replay=True) source_bmc = function_records(source_records["bmc"]) for name in INVALID_FUNCTIONS: if diagnostic_identity(selected_bmc[name]) != diagnostic_identity( diff --git a/clang/test/Verify/suite/backend_execution.test b/clang/test/Verify/suite/backend_execution.test index 9dbd7dcfae..8e3e04a054 100644 --- a/clang/test/Verify/suite/backend_execution.test +++ b/clang/test/Verify/suite/backend_execution.test @@ -118,8 +118,8 @@ # LEAN-JOBS: error: --jobs and --proof-cache are not supported by the Lean backend # LOWER-CACHE: error: --proof-cache cannot be combined with --lower-only -# REPLAY: Verified: cached_identity [backend=z3] [cache=[[RN:[1-9][0-9]*]]/[[RN]]] -# REPLAY: Verified: cached_offset [backend=z3] [cache=[[RM:[1-9][0-9]*]]/[[RM]]] +# REPLAY: Proved obligations: cached_identity (dependencies not checked in replay) [backend=z3] [cache=[[RN:[1-9][0-9]*]]/[[RN]]] +# REPLAY: Proved obligations: cached_offset (dependencies not checked in replay) [backend=z3] [cache=[[RM:[1-9][0-9]*]]/[[RM]]] # FAILED-FIRST: error: verification failed: parallel_failure # FAILED-FIRST-SAME: [cache=0/4] diff --git a/clang/test/Verify/suite/collections.cpp b/clang/test/Verify/suite/collections.cpp index 89651a5469..fd2d88e85a 100644 --- a/clang/test/Verify/suite/collections.cpp +++ b/clang/test/Verify/suite/collections.cpp @@ -115,8 +115,8 @@ int count_equal(const int *a, int n, int x) } // CHECK-DAG: Verified: count_equal -// REPLAY-DAG: Verified: sets -// REPLAY-DAG: Verified: count_equal +// REPLAY-DAG: Proved obligations: sets (dependencies not checked in replay) +// REPLAY-DAG: Proved obligations: count_equal (dependencies not checked in replay) // REPLAY-DAG: error: verification failed: map_wrong // VC-LABEL: vc sets diff --git a/clang/test/Verify/suite/heap_reading_spec.cpp b/clang/test/Verify/suite/heap_reading_spec.cpp index 95a9551ce6..5110b10fce 100644 --- a/clang/test/Verify/suite/heap_reading_spec.cpp +++ b/clang/test/Verify/suite/heap_reading_spec.cpp @@ -44,7 +44,7 @@ int total(const int *p, int n) } // LOOP-DAG: Verified: total // CVC5-DAG: {{Verified|Unresolved}}: total -// REPLAY-DAG: Verified: total +// REPLAY-DAG: Proved obligations: total (dependencies not checked in replay) // VC: features {{.*}}heap-functions int skip_first(const int *p, int n) @@ -79,7 +79,7 @@ void clear_first(int *p) p[0] = 0; } // CHECK-DAG: Verified: clear_first -// REPLAY-DAG: Verified: clear_first +// REPLAY-DAG: Proved obligations: clear_first (dependencies not checked in replay) void clear_first_unchanged(int *p) cppverify::pre(valid(p, 2)) diff --git a/clang/test/Verify/suite/obligation_archive.test b/clang/test/Verify/suite/obligation_archive.test index d0812b82ae..9939b4d523 100644 --- a/clang/test/Verify/suite/obligation_archive.test +++ b/clang/test/Verify/suite/obligation_archive.test @@ -91,19 +91,19 @@ # RUN: not %cpp-verify --obligation-in=%t.bad-binder-sort 2>&1 | FileCheck %s --check-prefix=BAD-BINDER-SORT # RUN: %cpp-verify --lower-only --dump-ir=3 %S/heap_memcpy_pass.cpp -- 2>&1 | grep -B1 '__quant_.* : int' | FileCheck %s --check-prefix=QUANTIFIED-INDEX -# REPLAY: Verified: canonical_obligations [backend=z3] [semantic-hash=sha256:{{[0-9a-f]+}}] +# REPLAY: Proved obligations: canonical_obligations (dependencies not checked in replay) [backend=z3] [semantic-hash=sha256:{{[0-9a-f]+}}] # LOWER: vc canonical_obligations # LOWER: schema cppverify.obligation/2 # LOWER: (let # LOWER: Lowered: canonical_obligations [backend=z3] [semantic-hash=sha256:{{[0-9a-f]+}}] # LEAN: Exported: lean obligation: canonical_obligations [backend=lean] # LEAN-FILE: theorem cppverify_canonical_obligations_ -# MULTI-COUNT-2: Verified: canonical_obligations +# MULTI-COUNT-2: Proved obligations: canonical_obligations (dependencies not checked in replay) # BAD-MAGIC: error: invalid obligation archive: invalid obligation archive magic # TRUNCATED: error: invalid obligation archive: truncated obligation archive # VERSION: error: invalid obligation archive: unsupported obligation archive version # SCHEMA-V1: error: invalid obligation archive: invalid obligation kind in obligation archive -# SCHEMA-V1-KINDS: Verified: canonical_obligations [backend=z3] +# SCHEMA-V1-KINDS: Proved obligations: canonical_obligations (dependencies not checked in replay) [backend=z3] # KIND: error: invalid obligation archive: invalid expression kind in obligation archive # FEATURES: error: invalid obligation archive: obligation archive feature declaration does not match contents # DUPLICATE-ID: error: invalid obligation archive: obligation module has an empty or duplicate obligation identity @@ -118,15 +118,15 @@ # SYMBOL-SORT: error: invalid obligation archive: logical variable has inconsistent sorts: # TRACE-SORT: error: invalid obligation archive: obligation module has invalid diagnostic trace value # INVALID-UTF8: "function":"{{.*}}anonical_obligations" -# INVALID-UTF8-SAME: "status":"verified" +# INVALID-UTF8-SAME: "status":"proved-obligations" # DUPLICATE-FUNCTION: error: invalid obligation archive: duplicate logical function in obligation archive # BAD-BINDER-SORT: error: invalid obligation archive: quantifier binder occurrence is not a mathematical integer # QUANTIFIED-INDEX: * : int # QUANTIFIED-INDEX-NEXT: __quant_{{[0-9]+}}_{{.*}} : int # BMC: error: BMC cannot replay an untransformed backend-neutral archive -# BMC-REPLAY-DAG: Verified: zero_iterations [backend=bmc, bound=0] +# BMC-REPLAY-DAG: Proved obligations: zero_iterations (dependencies not checked in replay) [backend=bmc, bound=0] # BMC-REPLAY-DAG: cov_loop_unroll_zero.cpp:22:3: BoundedSafe: one_step_may_run (unwinding bound 0 is insufficient for a complete proof) [backend=bmc, bound=0] # BMC-BOUND: error: requested BMC bound 1 does not match archived bound 0 # BMC-LOWER: transform bmc-unroll 0 -# BMC-DECREASES: Verified: dec.decreases [backend=bmc, bound=2] +# BMC-DECREASES: Proved obligations: dec.decreases (dependencies not checked in replay) [backend=bmc, bound=2] # FAIL: obligation_archive_fail.cpp:2:37: error: verification failed: archived_failure diff --git a/clang/test/Verify/suite/replay_dependencies.cpp b/clang/test/Verify/suite/replay_dependencies.cpp new file mode 100644 index 0000000000..040bfb02ad --- /dev/null +++ b/clang/test/Verify/suite/replay_dependencies.cpp @@ -0,0 +1,66 @@ +// RUN: rm -f %t.cpv +// RUN: not %cpp-verify --obligation-out=%t.cpv %s -- 2>&1 | FileCheck %s --check-prefix=SOURCE +// RUN: not %cpp-verify --obligation-in=%t.cpv 2>&1 \ +// RUN: | FileCheck %s --check-prefix=REPLAY --implicit-check-not=Verified +// RUN: not %cpp-verify --obligation-in=%t.cpv --diagnostics-format=json 2>&1 \ +// RUN: | FileCheck %s --check-prefix=JSON --implicit-check-not='"status":"verified"' +// +// Replay proves each archived module alone. A source verdict also rests on +// callee contracts, trust, termination, and vacuity, which replay does not +// check, so a replayed proof is never reported as verified. + +// caller's proof rests on the contract of bad_callee, which is false. +int bad_callee(int x) + cppverify::post(cppverify::result > 0) +{ + return x; +} + +int caller(int x) + cppverify::post(cppverify::result > 0) +{ + return bad_callee(x); +} + +int vac(int x) + cppverify::pre(x > 0 && x < 0) + cppverify::post(cppverify::result == 42) +{ + return 0; +} + +[[cppverify::trusted]] int tr(int x) + cppverify::post(cppverify::result > 100); + +int uses_tr(int x) + cppverify::post(cppverify::result > 100) +{ + return tr(x); +} + +int loop_star(int n) + cppverify::post(cppverify::result == 7) +{ + while (true) + cppverify::invariant(true) + cppverify::decreases(*) + { + if (n == 3) + return 7; + } +} + +// SOURCE-DAG: error: verification failed: bad_callee +// SOURCE-DAG: Unresolved: caller [backend=z3] [reason=callee.contract] +// SOURCE-DAG: Verified: vac [backend=z3] [vacuous] +// SOURCE-DAG: Verified: uses_tr [backend=z3] [trusts=tr] +// SOURCE-DAG: Verified: loop_star [backend=z3] [partial] + +// REPLAY-DAG: error: verification failed: bad_callee +// REPLAY-DAG: Proved obligations: caller (dependencies not checked in replay) [backend=z3] +// REPLAY-DAG: Proved obligations: vac (dependencies not checked in replay) [backend=z3] +// REPLAY-DAG: Proved obligations: uses_tr (dependencies not checked in replay) [backend=z3] +// REPLAY-DAG: Proved obligations: loop_star (dependencies not checked in replay) [backend=z3] + +// JSON-DAG: "function":"bad_callee"{{.*}}"status":"failed" +// JSON-DAG: "function":"caller","message":"dependencies not checked in replay"{{.*}}"status":"proved-obligations" diff --git a/clang/test/Verify/suite/sequences.cpp b/clang/test/Verify/suite/sequences.cpp index 118f8c68b0..1a008e1b2c 100644 --- a/clang/test/Verify/suite/sequences.cpp +++ b/clang/test/Verify/suite/sequences.cpp @@ -178,9 +178,9 @@ void ghost_loop_wrong(int n) } // CHECK-DAG: error: verification failed: ghost_loop_wrong [{{.*}}::assertion@[[@LINE-2]]:3] (counterexample: {{.*}}s [ssa=s_2] [type=seq] = [{{-?[0-9]+}}]{{.*}}) [backend=z3] [reason=counterexample] -// REPLAY-DAG: Verified: basics -// REPLAY-DAG: Verified: reverse_index -// REPLAY-DAG: Verified: count_positive +// REPLAY-DAG: Proved obligations: basics (dependencies not checked in replay) +// REPLAY-DAG: Proved obligations: reverse_index (dependencies not checked in replay) +// REPLAY-DAG: Proved obligations: count_positive (dependencies not checked in replay) // REPLAY-DAG: error: verification failed: elements_differ // REPLAY-DAG: error: verification failed: ghost_loop_wrong diff --git a/clang/test/Verify/suite/solver_portfolio.cpp b/clang/test/Verify/suite/solver_portfolio.cpp index 526fc152f6..a7295add33 100644 --- a/clang/test/Verify/suite/solver_portfolio.cpp +++ b/clang/test/Verify/suite/solver_portfolio.cpp @@ -116,9 +116,9 @@ int invalid_spec_arithmetic() // LOWER-DAG: Lowered: unsafe_add // LOWER-NOT: Verified: -// REPLAY-DAG: Verified: valid_spec_arithmetic [backend=portfolio] -// REPLAY-DAG: Verified: valid_zero_arity_spec [backend=portfolio] -// REPLAY-DAG: Verified: write_pointer [backend=portfolio] +// REPLAY-DAG: Proved obligations: valid_spec_arithmetic (dependencies not checked in replay) [backend=portfolio] +// REPLAY-DAG: Proved obligations: valid_zero_arity_spec (dependencies not checked in replay) [backend=portfolio] +// REPLAY-DAG: Proved obligations: write_pointer (dependencies not checked in replay) [backend=portfolio] // REPLAY-DAG: error: verification failed: unsafe_add // REPLAY-DAG: error: verification failed: invalid_unsigned // REPLAY-DAG: error: verification failed: invalid_spec_arithmetic diff --git a/clang/test/Verify/suite/solver_race.cpp b/clang/test/Verify/suite/solver_race.cpp index 0203a61d50..939ce8ddb1 100644 --- a/clang/test/Verify/suite/solver_race.cpp +++ b/clang/test/Verify/suite/solver_race.cpp @@ -25,7 +25,7 @@ int add_one(int x) // CHECK-DAG: Verified: add_one [backend={{z3|cvc5|z3\+cvc5}}] // LOWER-DAG: Lowered: add_one // LOWER-NOT: Verified: -// REPLAY-DAG: Verified: {{.*}}add_one{{.*}} [backend={{z3|cvc5|z3\+cvc5}}] +// REPLAY-DAG: Proved obligations: {{.*}}add_one{{.*}} (dependencies not checked in replay) [backend={{z3|cvc5|z3\+cvc5}}] int wrong_bound(int x) cppverify::pre(x >= 0 && x < 10) diff --git a/clang/test/Verify/suite/spec_reads.cpp b/clang/test/Verify/suite/spec_reads.cpp index 5bbab38962..bc6ae82f89 100644 --- a/clang/test/Verify/suite/spec_reads.cpp +++ b/clang/test/Verify/suite/spec_reads.cpp @@ -33,7 +33,7 @@ void write_after(int *p, int n) } // CHECK-DAG: Verified: write_after // The frames are ordinary assumptions of the archived query. -// REPLAY-DAG: Verified: write_after +// REPLAY-DAG: Proved obligations: write_after (dependencies not checked in replay) // Each store is framed separately, through both branches. void write_around(int *p, int n, bool front) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index 1292dbe927..32e12ac7d2 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -361,12 +361,17 @@ class VerifyAction : public ASTFrontendAction { } }; +// Replay proves each module alone: the contracts and spec facts its proof +// rests on, its qualifiers, and its vacuity belong to the source run. +static constexpr const char ReplayProofNote[] = + "dependencies not checked in replay"; + static llvm::StringRef replayStatusCode(verify::VerifyStatus Status) { switch (Status) { case verify::VerifyStatus::Lowered: return "lowered"; case verify::VerifyStatus::Verified: - return "verified"; + return "proved-obligations"; case verify::VerifyStatus::Failed: return "failed"; case verify::VerifyStatus::Unresolved: @@ -414,7 +419,9 @@ static void printReplayJSON(const verify::ObligationModule &Module, ? "error" : "note"; Record["function"] = jsonText(Module.FunctionName); - Record["message"] = jsonText(Result.Message); + Record["message"] = Result.Status == verify::VerifyStatus::Verified + ? ReplayProofNote + : jsonText(Result.Message); Record["semantic_hash"] = ("sha256:" + SemanticHash).str(); if (!Result.BackendName.empty()) Record["backend"] = Result.BackendName; @@ -691,7 +698,8 @@ static int replayObligationArchive() { llvm::outs() << "Lowered: " << Module.FunctionName << Suffix << "\n"; break; case verify::VerifyStatus::Verified: - llvm::outs() << "Verified: " << Module.FunctionName << Suffix << "\n"; + llvm::outs() << "Proved obligations: " << Module.FunctionName << " (" + << ReplayProofNote << ")" << Suffix << "\n"; break; case verify::VerifyStatus::Exported: llvm::outs() << "Exported: lean obligation: " << Module.FunctionName diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index ee87afbf7a..e1423d2ac4 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -578,6 +578,13 @@ reach any adapter. Semantically equivalent records that differ only by supported constant structure or unreachable logical declarations therefore converge to the same backend module and semantic identity. +Replay settles each module alone. What a source verdict also rests on (callee +and trusted contracts, spec facts, partiality) and the vacuity checks are not +archived, so a module whose obligations all hold reports `Proved obligations: +f (dependencies not checked in replay)` (JSON status `proved-obligations`), +never `Verified`. A counterexample is still a failure: postconditions are not +archived either, so replay certifies it by the definitions alone. + BMC-produced modules retain the unroll bound as semantic transform provenance. Replay aggregates those modules with BMC unwinding semantics even when Z3 is the selected solver, so an exhausted frontier remains `BoundedSafe(N)` rather diff --git a/docs/DESIGN.md b/docs/DESIGN.md index ac1b25db13..3de525666b 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1645,7 +1645,10 @@ diagnostic identities advanced it to v3, and excluding diagnostic kinds advances it to v4. `--obligation-in=FILE` validates and replays the records through Z3, cvc5, strict Z3+cvc5 portfolio, lower-only/Layer 3-4 dumps, or Lean scratch export -without reparsing C++. +without reparsing C++. Each module is replayed alone, without the contracts, +spec facts, partiality, and vacuity checks its source verdict rests on, so a +module whose obligations hold reports `Proved obligations` (JSON +`proved-obligations`), never `Verified`. BMC-produced records carry their unroll bound in semantics and replay through the BMC result aggregator; untransformed records cannot acquire BMC semantics after this boundary. Lean scratch replay of bounded records is rejected. diff --git a/website/source/book/part-ii/ch15-toolchain-and-flags.rst b/website/source/book/part-ii/ch15-toolchain-and-flags.rst index bc79fc77f4..7950c75a3e 100644 --- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst +++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst @@ -90,7 +90,8 @@ Other flags obligation records with semantic hashes - ``cpp-verify --obligation-in=FILE`` — validate and replay records through Z3, lower-only dumps, or Lean scratch export without reparsing C++; records made - by BMC retain and enforce their archived unroll bound + by BMC retain and enforce their archived unroll bound. A proof is reported + as ``Proved obligations``, since what a verdict rests on is not archived IR layers --------- diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 3c32c5c8bc..56b1a9d692 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -209,6 +209,14 @@ ill-scoped variables, and contradictory complete/ordered goals fail closed. Different records may request different reveal fuel for one logical function, but its shared parameter/result signature must remain compatible. +Replay proves each module's obligations alone. What a source verdict also +rests on is not archived: the callee and trusted contracts and spec facts it +uses, ``[partial]``, and the vacuity checks. Where the source run reports +``Verified``, replay therefore reports ``Proved obligations: f (dependencies +not checked in replay)``, with JSON status ``proved-obligations``. A +counterexample is checked against the definitions alone and is still a +failure. + Source-built and replayed records pass through the same conservative canonicalizer before hashing and dispatch. It folds only trivial Boolean structure and reflexive equality/inequality, removes transitively unreachable diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index d1d91af60e..0fcf753ef3 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -200,9 +200,11 @@ Backends produced after BMC unrolling retain their bound and replay with BMC unwinding semantics; applying BMC to an untransformed archive is rejected because unrolling must run before obligation lowering. - Each module is replayed on its own: a module that relies on a spec's - termination, ``cppverify::reads``, or ``cppverify::post`` is not demoted when that spec's own - module fails, which the replay reports separately. + Each module is replayed on its own, without the callee and trusted + contracts, spec facts, partiality, and vacuity its source verdict + rests on: a module whose obligations all hold reports ``Proved + obligations: f (dependencies not checked in replay)`` (JSON + ``"status":"proved-obligations"``), never ``Verified``. ``--lower-only`` is deliberately different from compiler ``-fno-verify``. ``-fno-verify`` stops after Clang syntax and contract semantic checks;