diff --git a/doc/architectural/proof-explanation-future.md b/doc/architectural/proof-explanation-future.md new file mode 100644 index 00000000000..835be23ecc3 --- /dev/null +++ b/doc/architectural/proof-explanation-future.md @@ -0,0 +1,115 @@ +## Plan: Addressing Proof Explanation Limitations + +### Limitation: Per-Property Explanations + +**Current state:** The proof explanation covers all properties together. +When multiple properties hold, the explanation is the union of all +contributing steps. + +**Goal:** Produce a separate explanation for each proved property. + +**Approach:** + +1. After the initial UNSAT result, iterate over each proved property. + +2. For each property P, create a focused query: assert only P's negation + (not all properties' negations). This isolates P's proof. + +3. Use the solver's incremental interface (push/pop) to add P's negation + as an assumption, solve, and extract the unsat core. Then pop and + move to the next property. + +4. The unsat core for each property gives a per-property explanation. + +**Implementation sketch:** +```cpp +for(const auto &prop : proved_properties) +{ + solver.push({prop.negation_literal}); + auto result = solver(); // Should be UNSAT + if(result == D_UNSATISFIABLE) + { + auto explanation = get_proof_explanation_with_core(equation, solver, ns); + output_per_property_explanation(prop.id, explanation); + } + solver.pop(); +} +``` + +**Complexity:** O(P × S) where P is the number of proved properties and +S is the solver time per query. Since each query reuses the existing +formula (just changing which property is negated), the solver can +leverage learned clauses and should be fast. + +**Prerequisites:** The solver must support push/pop (MiniSAT with +simplifier disabled, CaDiCaL, or SMT solvers all support this). + +### Limitation: Loop Invariant Synthesis + +**Current state:** For loops, the explanation shows concrete unrolled +assignments (e.g., `x#3 = x#2 + 1`, `x#4 = x#3 + 1`, ...) rather +than a synthesized invariant (e.g., `x >= initial_x`). + +**Goal:** Synthesize human-readable loop invariants from the unrolled +proof explanation. + +**Approach (template-based):** + +1. Identify groups of SSA steps that correspond to the same source + location (same file/line) but different SSA versions. These are + loop iterations. + +2. For each group, extract the pattern. Common patterns: + - Monotonic: `x#(i+1) = x#i + c` → invariant: `x >= x_init` + - Bounded: `x#i < N` for all i → invariant: `x < N` + - Constant: `x#i = c` for all i → invariant: `x = c` + +3. Verify the candidate invariant against the unsat core: check that + the invariant, together with the non-loop steps in the core, + implies the property. + +**Approach (Craig interpolation):** + +1. Partition the formula into A (loop body) and B (everything else). +2. Compute the Craig interpolant I such that A ⇒ I and I ∧ B is UNSAT. +3. I is a loop invariant that's sufficient to prove the property. + +This requires a solver that supports interpolation (e.g., MathSAT, +OpenSMT, or Z3 with interpolation enabled). + +**Approach (abstract interpretation):** + +1. Run CBMC's existing abstract interpretation (goto-analyzer) on the + loop to compute an over-approximation of reachable states. +2. Intersect the abstract domain with the unsat core to produce a + tighter invariant. +3. Report the intersection as the loop invariant. + +**Recommended first step:** The template-based approach is simplest +and handles the most common cases (counters, bounds). It can be +implemented by post-processing the proof explanation output without +changing the solver interface. + +**Implementation sketch for template-based approach:** +```cpp +// Group core steps by source location +std::map> by_location; +for(const auto &step : explanation) + if(step.in_core) + by_location[step.source_location].push_back(step); + +// For locations with multiple steps (loop iterations), try templates +for(const auto &[loc, steps] : by_location) +{ + if(steps.size() > 1) + { + auto invariant = try_monotonic_template(steps); + if(!invariant) + invariant = try_bounded_template(steps); + if(!invariant) + invariant = try_constant_template(steps); + if(invariant) + report_loop_invariant(loc, *invariant); + } +} +``` diff --git a/doc/architectural/proof-explanation.md b/doc/architectural/proof-explanation.md new file mode 100644 index 00000000000..8240587a361 --- /dev/null +++ b/doc/architectural/proof-explanation.md @@ -0,0 +1,503 @@ +\ingroup module_hidden + +\page proof-explanation Proof Explanation + +\author CBMC Contributors + +# Proof Explanation: Word-Level Explanations for Proved Properties + +## 1. Motivation + +When CBMC proves that a property holds, it reports `VERIFICATION SUCCESSFUL` +but provides no further evidence or explanation. A counterexample trace explains +*why* a property is violated; proof explanations are the dual concept, +explaining *why* a property holds. + +Users benefit from proof explanations in several ways: + +- **Trust.** An explanation provides evidence that the proof is meaningful, + not merely an artifact of modeling choices or bounds. +- **Understanding.** Developers can see which assignments, assumptions, and + constraints in their code are responsible for the property holding. +- **Debugging unreachability.** When code is unreachable, a proof explanation + for the unreachability query tells the user *why* the code cannot be reached. +- **Review.** In safety-critical development, reviewers can inspect the + explanation alongside the verification result to gain confidence that the + correct properties were checked against the correct code. + +## 2. Background + +CBMC performs bounded model checking by encoding a verification problem as a +Boolean satisfiability (SAT) formula. The formula is satisfiable if and only if +there exists an execution that violates the property. Therefore: + +- **SAT** means the property can be violated. CBMC extracts a counterexample + trace from the satisfying assignment. +- **UNSAT** means the property holds (it is impossible to violate within the + given bounds). Traditionally, CBMC reports success and stops. + +Modern SAT solvers can provide additional information on an UNSAT result. +In particular, they support **assumption-based conflict analysis**, which +identifies which of the assumptions passed to the solver participate in the +unsatisfiability proof: + +- **CaDiCaL** exposes this via the `failed()` method. After an UNSAT result, + calling `failed(literal)` returns true if the given literal (which must have + been added as an assumption) is part of the conflict. +- **MiniSAT2** exposes this via the conflict clause. After an UNSAT result, + the `conflict` member contains the set of assumption literals that form the + unsatisfiable core. + +Both mechanisms are already wired into CBMC through the `propt::is_in_conflict(literalt)` +virtual method, which is implemented by `satcheck_cadicalt` and +`satcheck_minisat2t`. At the word level, `prop_conv_solvert` wraps this as +`is_in_conflict(const exprt &)` via the `conflict_providert` interface. + +## 3. CBMC Encoding Pipeline + +The encoding pipeline transforms source code into a propositional formula +through several stages: + +``` +Source code + | + v +GOTO program (goto_modelt) + | + v +Symbolic Execution (goto_symext) + | + v +SSA equation (symex_target_equationt, containing SSA_stept entries) + | + v +Bit-vector encoding (boolbvt / prop_conv_solvert) + | + v +Propositional formula (CNF clauses) + | + v +SAT solver (CaDiCaL, MiniSAT2, etc.) +``` + +### Key mappings + +- **`exprt` to `literalt`:** The `prop_conv_solvert` maintains a symbol-to-literal + cache. When a word-level expression is converted, each bit of the result is + mapped to a propositional literal. The `boolbv_mapt` stores this mapping: + for each identifier, it records a `bvt` (vector of `literalt` values) + representing the individual bits. + +- **`literalt` to SAT variable:** Each `literalt` wraps a SAT variable number + and a sign bit. The SAT solver operates on these variables directly. + +- **SSA steps:** Each `SSA_stept` in the equation has a `guard_handle` and + a `cond_handle`, both stored as `literal_exprt` values after conversion. + The guard controls whether the step is active in a given execution path; + the condition encodes the step's semantic content (e.g., the right-hand + side of an assignment or the condition of an assumption). + +## 4. Implementation + +### Phase 1: SSA-step filtering (`--proof-explanation`) + +The `--proof-explanation` command-line option enables proof explanations +for properties that CBMC proves to hold. The implementation lives in +`src/goto-checker/proof_explanation.h` and `src/goto-checker/proof_explanation.cpp`. + +#### Algorithm + +After the SAT solver returns UNSAT (all properties hold), the +`get_proof_explanation()` function iterates over the SSA steps in the +`symex_target_equationt` and collects steps that are relevant to the proof: + +1. **Skip ignored steps.** Steps that were removed by the formula slicer + (`--slice-formula`) have their `ignore` flag set. These are excluded. + +2. **Filter by step type.** Only assignments, assumptions, and constraints + are included. Assertions (the properties being proved), declarations, + gotos, and other structural steps are excluded. + +3. **Filter internal steps.** Steps originating from built-in initialization + (source files matching `` or ``), internal SSA + variables (identifiers containing `goto_symex::` or `return'`), and + steps without useful source locations are excluded. + +4. **Collect results.** Each surviving step produces a `proof_explanation_stept` + containing: + - `source_location`: the source file, line, and function + - `step_type`: "assignment", "assumption", or "constraint" + - `description`: a human-readable rendering of the step's content + - `in_core`: whether the step is in the unsat core (see Phase 2) + +### Phase 2: Assumption-based unsat core extraction + +Phase 2 refines the proof explanation by using the SAT solver's +assumption-based conflict analysis to identify which steps are truly +part of the unsat core. The implementation is in +`get_proof_explanation_with_core()` in `proof_explanation.cpp`. + +#### Algorithm + +After the initial UNSAT solve, `get_proof_explanation_with_core()`: + +1. **Collects candidate steps** using the same filtering as Phase 1. + +2. **Gathers guard handles.** Each SSA step has a `guard_handle` that + was set during `convert_guards()` via `decision_procedure.handle(guard)`. + For steps with non-constant guards (branching), the guard handle is a + `literal_exprt` wrapping the SAT literal for the guard. Steps with + constant-true guards (straight-line code) are always active and are + trivially marked as in the core. + +3. **Pushes guard handles as SAT assumptions.** Using the + `stack_decision_proceduret::push(vector)` interface, the + non-constant guard handles are added to the solver's assumption stack. + This follows the same pattern used by `goto_symex_fault_localizert`. + +4. **Re-solves.** The solver is called again. Since the formula already + encodes all constraints and the guard assumptions only constrain + additional paths to be active, the result should still be UNSAT. + +5. **Checks conflict membership.** For each guard handle, the solver's + `is_in_conflict()` method (from the `conflict_providert` interface) + is called. This queries the SAT solver's `failed()` mechanism + (CaDiCaL) or conflict clause (MiniSAT2) to determine whether + the guard assumption participated in the UNSAT proof. + +6. **Marks core membership.** Steps whose guards are in the conflict + have `in_core=true`. Steps with constant-true guards are always + marked as in the core. Steps whose guards are not in the conflict + have `in_core=false`. + +7. **Cleans up.** The assumption context is popped via `solver.pop()`. + +The conflict provider is accessed via `dynamic_cast` +on the `stack_decision_proceduret`. If the solver does not support the +`conflict_providert` interface (e.g., some SMT backends), all steps are +marked as in the core as a safe fallback. + +#### Output + +Each step is annotated with `[core]` in the plain-text output. Steps +not in the core are shown without the marker. For JSON output, an +`inCore` boolean field is added. For XML output, an `in-core` attribute +is set. + +### Output format + +The explanation is printed after `VERIFICATION SUCCESSFUL` in a section +headed by `Proof explanation:`. Steps in the unsat core are prefixed with +`[core]`. For JSON and XML output modes, structured `proof-explanation` +elements are emitted with core annotations (`inCore` for JSON, +`in-core` for XML), following the same pattern as fault localization +output. The formatting logic is in `output_proof_explanation()` in +`src/goto-checker/report_util.cpp`. + +### Soundness + +Phase 1 produces a **sound over-approximation**: every step that is +genuinely necessary for the proof will be reported, but some reported +steps may not actually be required. The slicer (`--slice-formula`) +already removes syntactically irrelevant steps before solving, so the +explanation only includes steps that survived slicing. + +Phase 2 refines this using assumption-based conflict analysis on guard +handles. Steps whose guards are not in the UNSAT conflict are marked +`in_core=false`. For straight-line programs where all guards are +constant-true, all steps remain marked as in the core. For programs +with branching, steps on irrelevant branches may be identified as +not in the core. + +### Integration point + +The proof explanation is wired into the verification pipeline through the +`multi_path_symex_checkert`, which provides a `get_proof_explanation()` method. +The `stop_on_fail_verifier` and `all_properties_verifier_with_trace_storage` +templates call this method when `--proof-explanation` is enabled and the result +is PASS. A C++17 type trait (`has_get_proof_explanationt`) with `if constexpr` +is used to support checker types that do not provide proof explanations. + +## 5. Examples + +### 5.1 Simple assignment + +```c +int main() { + int x = 5; + __CPROVER_assert(x > 0, "x is positive"); + return 0; +} +``` + +Running `cbmc --proof-explanation` reports: + +``` +Proof explanation: + assignment: x = 5 (file main.c line 3) +``` + +The assignment `x = 5` is the key step that makes `x > 0` hold. + +### 5.2 Branching + +```c +int main() { + int y = 10; + int x; + if(y > 5) + x = 3; + else + x = -1; + __CPROVER_assert(x > 0, "x is positive"); + return 0; +} +``` + +The proof explanation reports both `y = 10` and `x = 3`. The branch +`y > 5` evaluates to true (since `y` is 10), so the assignment `x = 3` is +taken, making `x > 0` hold. The `else` branch (`x = -1`) is irrelevant +and excluded by slicing. + +### 5.3 Assumptions + +```c +int main() { + int input; + __CPROVER_assume(input >= 0); + __CPROVER_assume(input < 100); + int result = input + 1; + __CPROVER_assert(result > 0, "result is positive"); + return 0; +} +``` + +The proof explanation reports both assumptions (`input >= 0` and +`input < 100`) and the assignment `result = input + 1`. Together, +these constrain `result` to the range [1, 100], ensuring `result > 0`. + +## 6. Limitations of the Current Approach + +1. **Over-approximation, not minimal core.** The current implementation + collects all non-ignored, non-internal SSA steps of relevant types. + This is broader than a true unsat core: some reported steps may not + participate in the minimal proof of unsatisfiability. + +2. **SSA-level granularity.** The explanation operates at the level of + SSA steps, not at the level of individual SAT clauses or bit-level + constraints. Two steps that happen to share a variable may both be + reported even if only one is truly necessary. + +3. **Syntactic dependency, not semantic necessity.** The formula slicer + removes steps that have no syntactic dependency on the property. But + syntactic dependency is a necessary condition for semantic relevance, + not a sufficient one. Some syntactically connected steps may be + semantically irrelevant. + +4. **No support for incremental/single-path checking.** Currently, proof + explanations are only available with the multi-path symex checker. + Single-path and incremental checkers do not yet expose the needed + interface. + +## 7. Future Work: Toward True Unsat Core Extraction + +### 7.1 Clause-level unsat cores + +A more precise approach would track individual CNF clauses through the +bit-vector encoding and map each clause back to the SSA step that +produced it. After solving, the SAT solver's proof trace reveals which +original clauses were used in the refutation. + +CaDiCaL supports proof tracing via `connect_proof_tracer()` and +`trace_proof()`. From the proof trace, the set of original input clauses +used in the derivation of the empty clause can be extracted. Combined +with clause-to-SSA-step tracking in the `boolbvt` encoding layer, this +would yield a precise mapping from the unsat core to source-level steps. + +### 7.2 Assumption-based approach (implemented in Phase 2) + +Phase 2 implements a guard-handle-based variant of the assumption +approach. Instead of re-encoding with activation literals, it pushes +the existing guard handles as SAT assumptions and uses `is_in_conflict()` +to determine which are in the core. See Section 4 for details. + +A more precise variant would re-encode the SSA equation with one +activation literal per step: + +``` +activation_lit_i => step_constraint_i +``` + +All activation literals are passed as assumptions to the solver. After +UNSAT, calling `failed()` (or inspecting the MiniSAT2 conflict clause) +on each activation literal reveals which steps are in the core. This +produces a true assumption-based unsat core at the cost of a modified +encoding. It does not require re-solving; the activation literals are +simply additional assumptions in the same solve call. + +### 7.3 Lifting to word-level invariants (implemented in Phase 3) + +Phase 3 implements an initial version of word-level invariant extraction. +Given the proof explanation steps marked as core (from Phase 2), the +`extract_proof_invariants()` function groups them by variable to produce +structured invariant summaries. + +The algorithm works as follows: + +1. Correlate explanation steps back to their SSA steps by replaying + the same filtering logic (`is_relevant_proof_step()`). +2. For each core step that is an assignment, the key variable is the + left-hand side. The description is added as a constraint on that + variable. +3. For each core step that is an assumption or constraint, find all + symbol expressions referenced in the condition. For each such + symbol, add the condition as a constraint on that variable. +4. Group by variable name (stripped of SSA level suffixes) and produce + one `proof_invariantt` per variable, with a clean display name + (stripped of scope prefixes and renaming suffixes). + +For example, from the core steps `input >= 0`, `input < 100`, and +`result = input + 1`, the output is: + +``` +Proof invariants: + input: input >= 0, not(input >= 100) + result: result = input + 1 +``` + +This is a grouping-based approach rather than full invariant synthesis. +Future work may synthesize more abstract invariants (e.g., range +summaries like `input in [0, 100)`) or produce implications +(e.g., `input >= 0 AND input < 100 implies result > 0`). + +The implementation lives in `extract_proof_invariants()` in +`src/goto-checker/proof_explanation.cpp`, with output formatting in +`output_proof_invariants()` in `src/goto-checker/report_util.cpp`. +The `proof_invariantt` struct is defined in +`src/goto-checker/proof_explanation.h`. + +### 7.4 Integration with coverage analysis (implemented in Phase 4) + +Unreachable code corresponds to an UNSAT reachability query: the formula +encoding "can execution reach this program point?" is unsatisfiable. +Proof explanations for such queries tell users *why* the code cannot be +reached, which is valuable for: + +- **Coverage analysis:** Understanding why a test cannot cover a particular + branch. +- **Dead code detection:** Explaining to developers why a code path is + infeasible, helping them decide whether to remove it or fix the + conditions guarding it. + +Phase 4 integrates proof explanations with CBMC's coverage analysis. +When `--cover` is used alongside `--proof-explanation`, the +`cover_goals_verifier_with_trace_storaget` template now outputs proof +explanations for unreachable coverage goals (those with +`property_statust::PASS`, meaning the reachability query was UNSAT). + +The integration follows the same `if constexpr` type trait pattern used +in `stop_on_fail_verifier.h` and +`all_properties_verifier_with_trace_storage.h`: +- `has_get_proof_explanationt` detects whether the checker supports + proof explanations +- `has_get_proof_invariantst` detects whether the checker supports + proof invariants + +In coverage mode, the property status semantics are inverted relative +to normal verification: `FAIL` means the coverage goal was reached +(SATISFIED), while `PASS` means the goal is unreachable (the +reachability formula is UNSAT). The proof explanation is emitted only +when there are unreachable goals (`PASS` status), since those are the +cases where the UNSAT result can be explained. + +### 7.5 SMT-level unsat cores (implemented in Phase 5) + +When using SMT solvers (e.g., Z3 via the `--smt2` backend), the solver +natively supports unsat core extraction at the theory level. Phase 5 +integrates this capability so that the existing Phase 2 assumption-based +proof explanation approach works transparently with SMT backends. + +**Implementation approach.** Rather than using SMT `(get-unsat-core)` with +named assertions, Phase 5 uses `(get-unsat-assumptions)` with +`(check-sat-assuming ...)`. This reuses the same guard-handle-based +conflict analysis that Phase 2 uses for SAT solvers. The key changes: + +1. `smt2_convt` gains a `produce_unsat_cores` flag. When true, the SMT2 + preamble includes `(set-option :produce-unsat-cores true)`. + +2. `smt2_convt::write_footer()` emits `(get-unsat-assumptions)` after + `(check-sat-assuming ...)` when unsat core production is enabled. + +3. `smt2_dect` now inherits from `conflict_providert` and implements + `is_in_conflict(const exprt &)`. After an UNSAT result from + `check-sat-assuming`, `read_result()` parses the + `(get-unsat-assumptions)` response and stores the failed assumption + literal names. The `is_in_conflict()` method converts a `literal_exprt` + to its SMT2 identifier name and checks whether it appears in the + failed set. + +4. `solver_factory.cpp` enables `produce_unsat_cores` on the SMT2 solver + when `--proof-explanation` is active. + +With these changes, `get_proof_explanation_with_core()` in +`proof_explanation.cpp` works without modification: the +`dynamic_cast(&solver)` now succeeds for +`smt2_dect`, and the push/pop/is_in_conflict flow operates via the SMT +solver's native unsat-assumptions mechanism. + +**Solver compatibility.** This approach requires SMT solvers that support +both `check-sat-assuming` and `get-unsat-assumptions`. Z3, CVC5, and +Bitwuzla all set `use_check_sat_assuming = true` in the CBMC SMT2 +interface. Solvers that do not support `check-sat-assuming` (e.g., CVC3, +MathSAT, Yices) fall back to plain `(check-sat)` with assumptions as +assertions, and `get-unsat-assumptions` is not emitted; in this case the +Phase 2 code falls back to marking all steps as in_core=true. + +## 8. Related Work + +- **Error explanation (Kroening et al., STTT 2005).** This work computes + error explanations for failing properties using Craig interpolation + and similar techniques. Re-implementing this is listed in CBMC's + `FEATURE_IDEAS.md`. Proof explanation is the dual problem: explaining + why a property *holds* rather than why it *fails*. + +- **Fault localization.** CBMC already includes fault localization for + failing properties via `goto_symex_fault_localizert` in + `src/goto-checker/goto_symex_fault_localizer.cpp`. Fault localization + identifies which program locations are most likely responsible for a + property violation. Proof explanation applies analogous reasoning to + the UNSAT (passing) case. + +- **Proof witnesses (GraphML format).** CBMC can produce correctness + witnesses in the GraphML-based format defined by SV-COMP. These + witnesses encode structural information (e.g., loop invariant + locations) but do not explain *why* the property holds in terms of + contributing program steps. Proof explanations complement witnesses + by providing semantic content. + +## 9. Files + +| File | Purpose | +|------|---------| +| `src/goto-checker/proof_explanation.h` | `proof_explanation_stept` struct (with `in_core` field), `proof_invariantt` struct, `get_proof_explanation()`, `get_proof_explanation_with_core()`, `extract_proof_invariants()` declarations, `has_get_proof_explanationt` and `has_get_proof_invariantst` type traits | +| `src/goto-checker/proof_explanation.cpp` | Implementation of `get_proof_explanation()`, `get_proof_explanation_with_core()`, and `extract_proof_invariants()` | +| `src/goto-checker/goto_symex_property_decider.h` | `get_proof_explanation()` and `get_proof_invariants()` methods on the property decider | +| `src/goto-checker/goto_symex_property_decider.cpp` | Calls `get_proof_explanation_with_core()` and `extract_proof_invariants()` | +| `src/goto-checker/report_util.h` | Declarations of `output_proof_explanation()` and `output_proof_invariants()` | +| `src/goto-checker/report_util.cpp` | Plain (`[core]` markers), JSON (`inCore`), and XML (`in-core`) output for explanations; plain, JSON, and XML output for invariants | +| `src/goto-checker/multi_path_symex_checker.h` | `get_proof_explanation()` and `get_proof_invariants()` methods on the checker | +| `src/goto-checker/stop_on_fail_verifier.h` | Calls proof explanation and invariants in the PASS case | +| `src/goto-checker/all_properties_verifier_with_trace_storage.h` | Calls proof explanation and invariants for all proved properties | +| `src/goto-checker/cover_goals_verifier_with_trace_storage.h` | Calls proof explanation and invariants for unreachable coverage goals | +| `src/goto-checker/solver_factory.cpp` | Enables `produce_unsat_cores` on SMT2 solvers when `--proof-explanation` is active | +| `src/solvers/smt2/smt2_conv.h` | `produce_unsat_cores` flag for SMT-level unsat core extraction | +| `src/solvers/smt2/smt2_conv.cpp` | Emits `(set-option :produce-unsat-cores true)` and `(get-unsat-assumptions)` in the SMT2 output | +| `src/solvers/smt2/smt2_dec.h` | `smt2_dect` inherits from `conflict_providert`; `is_in_conflict()` declaration | +| `src/solvers/smt2/smt2_dec.cpp` | Parses `(get-unsat-assumptions)` response; implements `is_in_conflict()` for SMT-level conflict checking | +| `src/goto-checker/bmc_util.h` | `OPT_BMC` and `HELP_BMC` entries for `--proof-explanation` | +| `src/cbmc/cbmc_parse_options.h` | Includes `--proof-explanation` in `CBMC_OPTIONS` | +| `regression/cbmc/proof-explanation1/` | Regression test: basic proof explanation | +| `regression/cbmc/proof-explanation2/` | Regression test: unsat core `[core]` markers | +| `regression/cbmc/proof-explanation3/` | Regression test: word-level invariant extraction | +| `regression/cbmc/proof-explanation4/` | Regression test: coverage analysis integration | +| `regression/cbmc/proof-explanation5/` | Regression test: SMT-level unsat core (requires Z3, tagged `smt-backend`) | diff --git a/doc/cprover-manual/proof-explanation.md b/doc/cprover-manual/proof-explanation.md new file mode 100644 index 00000000000..58bd5231d86 --- /dev/null +++ b/doc/cprover-manual/proof-explanation.md @@ -0,0 +1,129 @@ +[CPROVER Manual TOC](../) + +# Proof Explanations + +When CBMC proves that all properties hold, it normally just reports +`VERIFICATION SUCCESSFUL`. The `--proof-explanation` option makes CBMC +additionally show *why* the properties hold — which assignments and +assumptions in your code are responsible for the proof. + +## Usage + +```sh +cbmc program.c --proof-explanation +``` + +The option works with all verification modes (bounded model checking, +coverage analysis) and all solver backends (SAT, SMT). + +## Reading the Output + +The proof explanation has two sections: + +### Proof Explanation + +Lists the program steps that contribute to the proof. Each line shows: +- `[core]` — this step is in the solver's unsat core (essential to the proof) +- The step type: `[assignment]`, `[assumption]`, or `[constraint]` +- The source file and line number +- The SSA expression (the symbolic value) + +Example: +``` +Proof explanation: + [core] [assumption] example.c:5 ¬(x ≥ 10) + [core] [assignment] example.c:6 y = x + 1 +``` + +This means: the proof relies on the assumption `x < 10` (line 5) and +the assignment `y = x + 1` (line 6). + +### Proof Invariants + +Groups the proof explanation by variable, showing what constraints each +variable satisfies: + +``` +Proof invariants: + x: ¬(x ≥ 10) + y: y = x + 1 +``` + +## Examples + +### Simple constant proof + +```c +int main() { + int x = 5; + assert(x > 0); +} +``` + +Output: +``` +Proof explanation: + [core] [assignment] example.c:2 x = 5 + +Proof invariants: + x: x = 5 +``` + +The proof relies solely on `x = 5`, which makes `x > 0` trivially true. + +### Assumption-based proof + +```c +int main() { + unsigned x; + __CPROVER_assume(x < 10); + unsigned y = x + 1; + assert(y > 0); + assert(y <= 10); +} +``` + +Output: +``` +Proof explanation: + [core] [assumption] example.c:3 ¬(x ≥ 10) + [core] [assignment] example.c:4 y = x + 1 + +Proof invariants: + x: ¬(x ≥ 10) + y: y = x + 1 +``` + +The proof uses the assumption `x < 10` and the computation `y = x + 1`. +Together these imply `y` is between 1 and 10, satisfying both assertions. + +### Explaining unreachable code (with --cover) + +```sh +cbmc program.c --cover location --proof-explanation +``` + +When a coverage goal is FAILED (unreachable), the proof explanation shows +why that code location cannot be reached. For example, if `x` is +constrained to `[0, 50]`, the branch `if(x > 100)` is unreachable, and +the explanation will show the constraint on `x`. + +## Limitations + +- **SSA names**: The output uses CBMC's internal SSA variable names + (e.g., `main::1::x!0@1#2`). The variable name before `::` is the + function, and the name after the last `::` is the local variable. + The `#N` suffix is the SSA version number. + +- **Loop invariants**: For programs with loops, the explanation shows + the concrete unrolled assignments rather than synthesized loop + invariants. This can be verbose for deeply unrolled loops. + +- **Per-property granularity**: The explanation covers all proved + properties together, not each property individually. When multiple + properties hold, the explanation shows the union of all contributing + steps. + +- **Solver dependence**: The quality of the explanation depends on the + SAT/SMT solver's unsat core. Different solvers may produce different + (but equally valid) explanations. diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 0e454caf4c1..2158d50de47 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -608,6 +608,12 @@ give a compact trace \fB\-\-stack\-trace\fR give a stack trace only .TP +\fB\-\-proof\-explanation\fR +When all properties are proved (UNSAT), show a word\-level explanation +identifying which assignments and assumptions contribute to the proof. +Uses the SAT solver's unsat core to determine the minimal set of +relevant program steps. +.TP \fB\-\-flush\fR flush every line of output .TP diff --git a/regression/cbmc/proof-explanation-cover/main.c b/regression/cbmc/proof-explanation-cover/main.c new file mode 100644 index 00000000000..76be2fdefd5 --- /dev/null +++ b/regression/cbmc/proof-explanation-cover/main.c @@ -0,0 +1,29 @@ +typedef struct +{ + int balance; + int is_locked; +} account_t; + +int withdraw(account_t *acc, int amount) +{ + if(acc->is_locked) + return -1; + + if(amount <= 0) + return -2; + + if(amount > acc->balance) + return -3; + + acc->balance -= amount; + return 0; +} + +int main() +{ + account_t acc; + acc.balance = 100; + acc.is_locked = 0; + + int result = withdraw(&acc, 50); +} diff --git a/regression/cbmc/proof-explanation-cover/test.desc b/regression/cbmc/proof-explanation-cover/test.desc new file mode 100644 index 00000000000..1dd1ebf80d4 --- /dev/null +++ b/regression/cbmc/proof-explanation-cover/test.desc @@ -0,0 +1,22 @@ +CORE +main.c +--cover location --proof-explanation +^EXIT=0$ +^SIGNAL=0$ +withdraw.coverage.*line 10.*FAILED +withdraw.coverage.*line 13.*FAILED +withdraw.coverage.*line 16.*FAILED +Proof explanation: +balance = 100 +is_locked = 0 +amount.*= 50 +Per-property proof explanations: +Property withdraw.coverage.3: +Property withdraw.coverage.5: +Property withdraw.coverage.8: +-- +^warning: ignoring +-- +Tests per-coverage-goal proof explanations. Three branches in +withdraw() are unreachable. Each gets its own explanation showing +which assignments make it unreachable. diff --git a/regression/cbmc/proof-explanation1/main.c b/regression/cbmc/proof-explanation1/main.c new file mode 100644 index 00000000000..76c6d88ec9b --- /dev/null +++ b/regression/cbmc/proof-explanation1/main.c @@ -0,0 +1,6 @@ +int main() +{ + int x = 5; + __CPROVER_assert(x > 0, "x is positive"); + return 0; +} diff --git a/regression/cbmc/proof-explanation1/test.desc b/regression/cbmc/proof-explanation1/test.desc new file mode 100644 index 00000000000..5d7d2603984 --- /dev/null +++ b/regression/cbmc/proof-explanation1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--proof-explanation +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +Proof explanation: +-- +^warning: ignoring diff --git a/regression/cbmc/proof-explanation2/main.c b/regression/cbmc/proof-explanation2/main.c new file mode 100644 index 00000000000..e123c1fdda2 --- /dev/null +++ b/regression/cbmc/proof-explanation2/main.c @@ -0,0 +1,7 @@ +int main() +{ + int x = 5; + int y = 10; + __CPROVER_assert(x > 0, "x is positive"); + return 0; +} diff --git a/regression/cbmc/proof-explanation2/test.desc b/regression/cbmc/proof-explanation2/test.desc new file mode 100644 index 00000000000..fcaa5f09439 --- /dev/null +++ b/regression/cbmc/proof-explanation2/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--proof-explanation +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +Proof explanation: +\[core\] \[assignment\].*main.c:3 +-- +^warning: ignoring diff --git a/regression/cbmc/proof-explanation3/main.c b/regression/cbmc/proof-explanation3/main.c new file mode 100644 index 00000000000..846e05578be --- /dev/null +++ b/regression/cbmc/proof-explanation3/main.c @@ -0,0 +1,9 @@ +int main() +{ + int input; + __CPROVER_assume(input >= 0); + __CPROVER_assume(input < 100); + int result = input + 1; + __CPROVER_assert(result > 0, "result is positive"); + return 0; +} diff --git a/regression/cbmc/proof-explanation3/test.desc b/regression/cbmc/proof-explanation3/test.desc new file mode 100644 index 00000000000..7b7410f4a09 --- /dev/null +++ b/regression/cbmc/proof-explanation3/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--proof-explanation +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +Proof explanation: +Proof invariants: +-- +^warning: ignoring diff --git a/regression/cbmc/proof-explanation4/main.c b/regression/cbmc/proof-explanation4/main.c new file mode 100644 index 00000000000..ee3fee2febb --- /dev/null +++ b/regression/cbmc/proof-explanation4/main.c @@ -0,0 +1,10 @@ +int main() +{ + int x = 5; + if(x < 0) + { + // This code is unreachable because x = 5 > 0 + int y = x + 1; + } + return 0; +} diff --git a/regression/cbmc/proof-explanation4/test.desc b/regression/cbmc/proof-explanation4/test.desc new file mode 100644 index 00000000000..3336930920a --- /dev/null +++ b/regression/cbmc/proof-explanation4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--cover location --proof-explanation +^EXIT=0$ +^SIGNAL=0$ +Proof explanation: +-- +^warning: ignoring diff --git a/regression/cbmc/proof-explanation5/main.c b/regression/cbmc/proof-explanation5/main.c new file mode 100644 index 00000000000..76c6d88ec9b --- /dev/null +++ b/regression/cbmc/proof-explanation5/main.c @@ -0,0 +1,6 @@ +int main() +{ + int x = 5; + __CPROVER_assert(x > 0, "x is positive"); + return 0; +} diff --git a/regression/cbmc/proof-explanation5/test.desc b/regression/cbmc/proof-explanation5/test.desc new file mode 100644 index 00000000000..270dcc1a257 --- /dev/null +++ b/regression/cbmc/proof-explanation5/test.desc @@ -0,0 +1,9 @@ +CORE smt-backend +main.c +--z3 --proof-explanation +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +Proof explanation: +-- +^warning: ignoring diff --git a/regression/goto-synthesizer/proof_guided_synthesis/main.c b/regression/goto-synthesizer/proof_guided_synthesis/main.c new file mode 100644 index 00000000000..0f29d3430df --- /dev/null +++ b/regression/goto-synthesizer/proof_guided_synthesis/main.c @@ -0,0 +1,19 @@ +// Test that proof-relevant variables help guide synthesis. +// The loop increments x and y, but only x matters for the assertion. +// The proof explanation should identify x as proof-relevant, +// helping the synthesizer focus on x rather than y. +int main() +{ + unsigned x = 0; + unsigned y = 0; + unsigned n; + __CPROVER_assume(n > 0 && n < 10); + + while(x < n) + { + x++; + y++; + } + + __CPROVER_assert(x == n, "x equals n after loop"); +} diff --git a/regression/goto-synthesizer/proof_guided_synthesis/test.desc b/regression/goto-synthesizer/proof_guided_synthesis/test.desc new file mode 100644 index 00000000000..3a24eb32185 --- /dev/null +++ b/regression/goto-synthesizer/proof_guided_synthesis/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--pointer-check _ --no-malloc-may-fail _ --no-standard-checks +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Tests that proof-guided synthesis can synthesize loop invariants. +The proof explanation identifies x as proof-relevant, narrowing +the search space for the invariant synthesizer. diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 6548067d791..e5fddeac880 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -330,6 +330,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("localize-faults")) options.set_option("localize-faults", true); + if(cmdline.isset("proof-explanation")) + options.set_option("proof-explanation", true); + if(cmdline.isset("unwind")) { options.set_option("unwind", cmdline.get_value("unwind")); diff --git a/src/goto-checker/all_properties_verifier_with_trace_storage.h b/src/goto-checker/all_properties_verifier_with_trace_storage.h index 5b039979810..9b54663c468 100644 --- a/src/goto-checker/all_properties_verifier_with_trace_storage.h +++ b/src/goto-checker/all_properties_verifier_with_trace_storage.h @@ -19,6 +19,7 @@ Author: Daniel Kroening, Peter Schrammel #include "goto_trace_storage.h" #include "goto_verifier.h" #include "incremental_goto_checker.h" +#include "proof_explanation.h" #include "properties.h" #include "report_util.h" @@ -82,6 +83,37 @@ class all_properties_verifier_with_trace_storaget : public goto_verifiert output_properties(properties, iterations, ui_message_handler); } output_overall_result(determine_result(properties), ui_message_handler); + if constexpr(has_get_proof_explanationt::value) + { + if( + options.get_bool_option("proof-explanation") && + determine_result(properties) == resultt::PASS) + { + auto explanation = incremental_goto_checker.get_proof_explanation(); + output_proof_explanation(explanation, ui_message_handler); + } + } + if constexpr(has_get_proof_invariantst::value) + { + if( + options.get_bool_option("proof-explanation") && + determine_result(properties) == resultt::PASS) + { + auto invariants = incremental_goto_checker.get_proof_invariants(); + output_proof_invariants(invariants, ui_message_handler); + } + } + if constexpr(has_get_proof_explanationt::value) + { + if( + options.get_bool_option("proof-explanation") && + determine_result(properties) == resultt::PASS) + { + auto per_prop = + incremental_goto_checker.get_per_property_proof_explanations(); + output_per_property_proof_explanations(per_prop, ui_message_handler); + } + } incremental_goto_checker.report(); } @@ -90,6 +122,17 @@ class all_properties_verifier_with_trace_storaget : public goto_verifiert return traces; } + /// Get per-property proof explanations from the underlying checker. + /// Available after operator() returns, for properties proved PASS. + std::map> + get_per_property_proof_explanations() + { + if constexpr(has_get_proof_explanationt::value) + return incremental_goto_checker.get_per_property_proof_explanations(); + else + return {}; + } + protected: abstract_goto_modelt &goto_model; incremental_goto_checkerT incremental_goto_checker; diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index c604856d7ba..e720128d1ad 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -187,7 +187,8 @@ void run_property_decider( "(unwind-min):" \ "(unwind-max):" \ "(ignore-properties-before-unwind-min)" \ - "(symex-cache-dereferences)" OPT_UNWINDSET + "(symex-cache-dereferences)" \ + "(proof-explanation)" OPT_UNWINDSET #define HELP_BMC \ " {y--paths} [strategy] \t explore paths one at a time\n" \ @@ -233,6 +234,8 @@ void run_property_decider( " {y--graphml-witness} {ufilename} \t write the witness in GraphML format " \ "to {ufilename}\n" \ " {y--symex-cache-dereferences} \t enable caching of repeated " \ - "dereferences\n" + "dereferences\n" \ + " {y--proof-explanation} \t " \ + "show word-level explanation for proved properties\n" #endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H diff --git a/src/goto-checker/cover_goals_verifier_with_trace_storage.h b/src/goto-checker/cover_goals_verifier_with_trace_storage.h index ff62445d81d..33177e81b9e 100644 --- a/src/goto-checker/cover_goals_verifier_with_trace_storage.h +++ b/src/goto-checker/cover_goals_verifier_with_trace_storage.h @@ -12,13 +12,14 @@ Author: Daniel Kroening, Peter Schrammel #ifndef CPROVER_GOTO_CHECKER_COVER_GOALS_VERIFIER_WITH_TRACE_STORAGE_H #define CPROVER_GOTO_CHECKER_COVER_GOALS_VERIFIER_WITH_TRACE_STORAGE_H -#include "goto_verifier.h" - #include "bmc_util.h" #include "cover_goals_report_util.h" #include "goto_trace_storage.h" +#include "goto_verifier.h" #include "incremental_goto_checker.h" +#include "proof_explanation.h" #include "properties.h" +#include "report_util.h" template class cover_goals_verifier_with_trace_storaget : public goto_verifiert @@ -59,6 +60,52 @@ class cover_goals_verifier_with_trace_storaget : public goto_verifiert void report() override { output_goals(properties, iterations, ui_message_handler); + if constexpr(has_get_proof_explanationt::value) + { + if(options.get_bool_option("proof-explanation")) + { + bool has_unreachable = + count_properties(properties, property_statust::PASS) > 0; + if(has_unreachable) + { + // Overall explanation + auto explanation = incremental_goto_checker.get_proof_explanation(); + output_proof_explanation(explanation, ui_message_handler); + + // Per-goal explanations (captured during incremental solving) + auto per_prop = + incremental_goto_checker.get_per_property_proof_explanations(); + // Filter to only unreachable goals (PASS in coverage = unreachable) + std::map> unreachable; + for(const auto &entry : per_prop) + { + auto it = properties.find(entry.first); + if( + it != properties.end() && + it->second.status == property_statust::PASS) + { + unreachable.insert(entry); + } + } + if(!unreachable.empty()) + output_per_property_proof_explanations( + unreachable, ui_message_handler); + } + } + } + if constexpr(has_get_proof_invariantst::value) + { + if(options.get_bool_option("proof-explanation")) + { + bool has_unreachable = + count_properties(properties, property_statust::PASS) > 0; + if(has_unreachable) + { + auto invariants = incremental_goto_checker.get_proof_invariants(); + output_proof_invariants(invariants, ui_message_handler); + } + } + } } const goto_trace_storaget &get_traces() const diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp index fdec0b18c19..39da7909304 100644 --- a/src/goto-checker/goto_symex_property_decider.cpp +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -11,17 +11,23 @@ Author: Daniel Kroening, Peter Schrammel #include "goto_symex_property_decider.h" +#include #include #include #include // IWYU pragma: keep +#include "proof_explanation.h" + goto_symex_property_decidert::goto_symex_property_decidert( const optionst &options, ui_message_handlert &ui_message_handler, symex_target_equationt &equation, const namespacet &ns) - : options(options), ui_message_handler(ui_message_handler), equation(equation) + : options(options), + ui_message_handler(ui_message_handler), + equation(equation), + ns(ns) { solver_factoryt solvers( options, @@ -98,13 +104,16 @@ void goto_symex_property_decidert::add_constraint_from_goals( exprt goal_disjunction = disjunction(disjuncts); decision_procedure.set_to_true(goal_disjunction); - with_solver_hardness(decision_procedure, [](solver_hardnesst &hardness) { - // SSA expr and involved steps have already been collected - // in symex_target_equationt::convert_assertions - exprt ssa_expr_unused; - std::vector involved_steps_unused; - hardness.register_assertion_ssas(ssa_expr_unused, involved_steps_unused); - }); + with_solver_hardness( + decision_procedure, + [](solver_hardnesst &hardness) + { + // SSA expr and involved steps have already been collected + // in symex_target_equationt::convert_assertions + exprt ssa_expr_unused; + std::vector involved_steps_unused; + hardness.register_assertion_ssas(ssa_expr_unused, involved_steps_unused); + }); } decision_proceduret::resultt goto_symex_property_decidert::solve() @@ -153,12 +162,100 @@ void goto_symex_property_decidert::update_properties_status_from_goals( if(!set_pass) break; - for(auto &property_pair : properties) { - if(property_pair.second.status == property_statust::UNKNOWN) + // Capture proof explanation for properties being proved. + // This must happen now because assertion steps may be removed + // from the equation after this point (coverage mode). + std::vector explanation; + explanation = ::get_proof_explanation_with_core( + equation, solver->decision_procedure(), ns); + + for(auto &property_pair : properties) { - property_pair.second.status |= property_statust::PASS; - updated_properties.insert(property_pair.first); + if(property_pair.second.status == property_statust::UNKNOWN) + { + property_pair.second.status |= property_statust::PASS; + updated_properties.insert(property_pair.first); + + // Per-property filtering via data dependency analysis + find_symbols_sett needed; + for(const auto &step : equation.SSA_steps) + { + if(step.is_assert() && step.property_id == property_pair.first) + find_symbols(step.cond_expr, needed); + } + + if(!needed.empty()) + { + // Expand data dependencies + bool changed = true; + while(changed) + { + changed = false; + for(const auto &step : equation.SSA_steps) + { + if(!step.is_assignment() || step.ignore) + continue; + if(needed.count(step.ssa_lhs.get_identifier())) + { + find_symbols_sett rhs; + find_symbols(step.ssa_rhs, rhs); + for(const auto &s : rhs) + if(needed.insert(s).second) + changed = true; + } + } + } + + // Filter to relevant steps + std::vector filtered; + for(const auto &e : explanation) + { + if(!e.in_core) + continue; + bool found = false; + for(const auto &step : equation.SSA_steps) + { + if(step.ignore) + continue; + if(step.source.pc->source_location() != e.source_location) + continue; + if( + step.is_assignment() && + needed.count(step.ssa_lhs.get_identifier())) + { + found = true; + break; + } + if(step.is_assume()) + { + find_symbols_sett syms; + find_symbols(step.cond_expr, syms); + for(const auto &s : syms) + if(needed.count(s)) + { + found = true; + break; + } + if(found) + break; + } + } + if(found) + filtered.push_back(e); + } + if(!filtered.empty()) + per_property_explanations_cache[property_pair.first] = + std::move(filtered); + else + per_property_explanations_cache[property_pair.first] = + explanation; + } + else + { + per_property_explanations_cache[property_pair.first] = explanation; + } + } } } break; @@ -174,3 +271,24 @@ void goto_symex_property_decidert::update_properties_status_from_goals( break; } } + +std::vector +goto_symex_property_decidert::get_proof_explanation(const namespacet &ns) +{ + return ::get_proof_explanation_with_core( + equation, solver->decision_procedure(), ns); +} + +std::map> +goto_symex_property_decidert::get_per_property_proof_explanations( + const namespacet &) +{ + return per_property_explanations_cache; +} + +std::vector +goto_symex_property_decidert::get_proof_invariants(const namespacet &ns) +{ + auto explanation = get_proof_explanation(ns); + return ::extract_proof_invariants(explanation, equation, ns); +} diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h index 368416763b2..fb37358d20c 100644 --- a/src/goto-checker/goto_symex_property_decider.h +++ b/src/goto-checker/goto_symex_property_decider.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, Peter Schrammel #include +#include "proof_explanation.h" #include "properties.h" #include "solver_factory.h" @@ -65,10 +66,35 @@ class goto_symex_property_decidert std::unordered_set &updated_properties, decision_proceduret::resultt dec_result, bool set_pass = true) const; + /// Get a word-level proof explanation for proved properties + /// with unsat core annotations. Uses the solver's assumption-based + /// conflict analysis when available, falling back to the basic + /// approach otherwise. + /// Must be called after solve() returns D_UNSATISFIABLE. + /// \param ns: the namespace for expression pretty-printing + /// \return a vector of proof explanation steps with core annotations + std::vector + get_proof_explanation(const namespacet &ns); + + /// Get per-property proof explanations using assumption-based solving. + /// For each proved property, solves with the property's goal literal + /// as an assumption and extracts the unsat core. This gives a focused + /// explanation for each property individually. + std::map> + get_per_property_proof_explanations(const namespacet &ns); + + /// Get word-level invariants from the proof explanation. + /// Groups core steps by the variables they constrain. + /// Must be called after solve() returns D_UNSATISFIABLE. + /// \param ns: the namespace for expression pretty-printing + /// \return a vector of proof invariants + std::vector get_proof_invariants(const namespacet &ns); + protected: const optionst &options; ui_message_handlert &ui_message_handler; symex_target_equationt &equation; + const namespacet &ns; std::unique_ptr solver; struct goalt @@ -87,6 +113,11 @@ class goto_symex_property_decidert /// the property. Uses `std::string` to maintain consistent (lexicographic) /// ordering as we iterate over this map to produce constraints. std::map goal_map; + +public: + /// Cached per-property proof explanations. + mutable std::map> + per_property_explanations_cache; }; #endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp index 40f60b6ed85..aaa28b55b63 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, Peter Schrammel #include "multi_path_symex_checker.h" +#include #include #include @@ -22,6 +23,7 @@ Author: Daniel Kroening, Peter Schrammel #include "bmc_util.h" #include "counterexample_beautification.h" #include "goto_symex_fault_localizer.h" +#include "proof_explanation.h" multi_path_symex_checkert::multi_path_symex_checkert( const optionst &options, @@ -37,8 +39,8 @@ multi_path_symex_checkert::multi_path_symex_checkert( PRECONDITION(!has_vector(goto_model.get_goto_functions())); } -incremental_goto_checkert::resultt multi_path_symex_checkert:: -operator()(propertiest &properties) +incremental_goto_checkert::resultt +multi_path_symex_checkert::operator()(propertiest &properties) { resultt result(resultt::progresst::DONE); @@ -62,6 +64,97 @@ operator()(propertiest &properties) update_properties(properties, result.updated_properties); + // Capture proof explanations for properties proved unreachable + // by the equation structure (before solver invocation). This is + // needed for coverage mode where unreachable goals are removed + // from the equation during incremental solving. + if(options.get_bool_option("proof-explanation")) + { + auto explanation = ::get_proof_explanation(equation, ns); + for(const auto &prop : properties) + { + if(prop.second.status != property_statust::PASS) + continue; + + // Find which symbols this property depends on + find_symbols_sett needed; + for(const auto &step : equation.SSA_steps) + { + if(step.is_assert() && step.property_id == prop.first) + { + find_symbols(step.cond_expr, needed); + } + } + + // Expand data dependencies (not guard dependencies) + bool changed = true; + while(changed) + { + changed = false; + for(const auto &step : equation.SSA_steps) + { + if(!step.is_assignment() || step.ignore) + continue; + if(needed.count(step.ssa_lhs.get_identifier())) + { + find_symbols_sett rhs; + find_symbols(step.ssa_rhs, rhs); + for(const auto &s : rhs) + if(needed.insert(s).second) + changed = true; + } + } + } + + // Build filtered explanation directly from SSA steps + std::vector filtered; + for(const auto &step : equation.SSA_steps) + { + if(step.ignore || !is_relevant_proof_step(step)) + continue; + bool relevant = false; + if( + step.is_assignment() && needed.count(step.ssa_lhs.get_identifier())) + { + relevant = true; + } + else if(step.is_assume()) + { + find_symbols_sett syms; + find_symbols(step.cond_expr, syms); + for(const auto &s : syms) + if(needed.count(s)) + { + relevant = true; + break; + } + } + if(relevant) + { + proof_explanation_stept pstep; + pstep.source_location = step.source.pc->source_location(); + pstep.step_type = step_type_string(step); + pstep.description = step_description(step, ns); + pstep.in_core = true; + if(step.is_assignment()) + pstep.symbols.insert(step.ssa_lhs.get_identifier()); + else if(step.is_assume()) + { + find_symbols_sett syms; + find_symbols(step.cond_expr, syms); + pstep.symbols = std::move(syms); + } + filtered.push_back(std::move(pstep)); + } + } + + if(filtered.empty()) + filtered = explanation; // fallback for coverage goals + property_decider.per_property_explanations_cache[prop.first] = + std::move(filtered); + } + } + // Have we got anything to check? Otherwise we return DONE. if(!has_properties_to_check(properties)) return result; @@ -147,6 +240,23 @@ void multi_path_symex_checkert::output_proof() output_graphml(equation, ns, options); } +std::vector +multi_path_symex_checkert::get_proof_explanation() +{ + return property_decider.get_proof_explanation(ns); +} + +std::map> +multi_path_symex_checkert::get_per_property_proof_explanations() +{ + return property_decider.get_per_property_proof_explanations(ns); +} + +std::vector multi_path_symex_checkert::get_proof_invariants() +{ + return property_decider.get_proof_invariants(ns); +} + void multi_path_symex_checkert::output_error_witness( const goto_tracet &error_trace) { diff --git a/src/goto-checker/multi_path_symex_checker.h b/src/goto-checker/multi_path_symex_checker.h index b604681a32b..ac626405e28 100644 --- a/src/goto-checker/multi_path_symex_checker.h +++ b/src/goto-checker/multi_path_symex_checker.h @@ -51,6 +51,21 @@ class multi_path_symex_checkert : public multi_path_symex_only_checkert, void output_error_witness(const goto_tracet &) override; void output_proof() override; + /// Get a word-level proof explanation for proved properties. + /// Must be called after the solver returns UNSATISFIABLE. + /// \return a vector of proof explanation steps with core annotations + std::vector get_proof_explanation(); + + /// Get per-property proof explanations. + std::map> + get_per_property_proof_explanations(); + + /// Get word-level invariants from the proof explanation. + /// Groups core steps by the variables they constrain. + /// Must be called after the solver returns UNSATISFIABLE. + /// \return a vector of proof invariants + std::vector get_proof_invariants(); + fault_location_infot localize_fault(const irep_idt &property_id) const override; diff --git a/src/goto-checker/proof_explanation.cpp b/src/goto-checker/proof_explanation.cpp new file mode 100644 index 00000000000..f5823dd3aff --- /dev/null +++ b/src/goto-checker/proof_explanation.cpp @@ -0,0 +1,412 @@ +/*******************************************************************\ + +Module: Word-level Proof Explanation + +Author: CBMC Contributors + +\*******************************************************************/ + +/// \file +/// Word-level Proof Explanation + +#include "proof_explanation.h" + +#include +#include +#include + +#include +#include +#include +#include + +#include +#include + +/// Return a human-readable string for an SSA step type +std::string step_type_string(const SSA_stept &step) +{ + if(step.is_assignment()) + return "assignment"; + if(step.is_assume()) + return "assumption"; + if(step.is_assert()) + return "assertion"; + if(step.is_constraint()) + return "constraint"; + if(step.is_goto()) + return "goto"; + if(step.is_decl()) + return "declaration"; + if(step.is_function_call()) + return "function call"; + if(step.is_function_return()) + return "function return"; + return "other"; +} + +/// Build a description string for an SSA step +std::string step_description(const SSA_stept &step, const namespacet &ns) +{ + std::ostringstream oss; + + if(step.is_assignment()) + { + oss << format(step.ssa_lhs) << " = " << format(step.ssa_rhs); + } + else if(step.is_assume()) + { + oss << format(step.cond_expr); + } + else if(step.is_assert()) + { + if(!step.comment.empty()) + oss << step.comment; + else + oss << format(step.cond_expr); + } + else if(step.is_constraint()) + { + oss << format(step.cond_expr); + } + else if(step.is_goto()) + { + oss << "branch on " << format(step.cond_expr); + } + else if(step.is_function_call()) + { + oss << step.called_function << "(...)"; + } + else if(step.is_decl()) + { + oss << format(step.ssa_lhs); + } + + return oss.str(); +} + +/// Check whether a source location has useful information +static bool has_useful_source_location(const source_locationt &loc) +{ + return !loc.get_file().empty() || !loc.get_line().empty(); +} + +/// Check whether an SSA step should be included in the proof explanation. +/// This contains the common filtering logic used by both the basic and +/// core-based approaches. +bool is_relevant_proof_step(const SSA_stept &step) +{ + // Skip steps that were sliced away + if(step.ignore) + return false; + + // We are interested in assignments, assumptions, and constraints + // that form the proof. Skip purely structural steps. + if( + !step.is_assignment() && !step.is_assume() && !step.is_constraint() && + !step.is_assert() && !step.is_goto() && !step.is_decl()) + { + return false; + } + + // Skip assertions (they are what we are proving, not + // part of the explanation) + if(step.is_assert()) + return false; + + // Skip declarations without meaningful content + if(step.is_decl()) + return false; + + // Skip gotos -- they add noise for the initial explanation + if(step.is_goto()) + return false; + + const source_locationt &loc = step.source.pc->source_location(); + if(!has_useful_source_location(loc)) + return false; + + // Skip internal built-in initialization steps + if( + id2string(loc.get_file()).find(" get_proof_explanation( + const symex_target_equationt &equation, + const namespacet &ns) +{ + std::vector result; + + for(const auto &step : equation.SSA_steps) + { + if(!is_relevant_proof_step(step)) + continue; + + proof_explanation_stept explanation_step; + explanation_step.source_location = step.source.pc->source_location(); + explanation_step.step_type = step_type_string(step); + explanation_step.description = step_description(step, ns); + explanation_step.in_core = true; + if(step.is_assignment()) + explanation_step.symbols.insert(step.ssa_lhs.get_identifier()); + else if(step.is_assume()) + { + find_symbols_sett syms; + find_symbols(step.cond_expr, syms); + explanation_step.symbols = std::move(syms); + } + + result.push_back(std::move(explanation_step)); + } + + return result; +} + +std::vector get_proof_explanation_with_core( + const symex_target_equationt &equation, + stack_decision_proceduret &solver, + const namespacet &ns) +{ + // Collect candidate steps and their guard handles + struct candidate_infot + { + const SSA_stept *step; + exprt guard_handle; + }; + + std::vector candidates; + for(const auto &step : equation.SSA_steps) + { + if(!is_relevant_proof_step(step)) + continue; + + candidates.push_back({&step, step.guard_handle}); + } + + if(candidates.empty()) + return {}; + + // Try to use assumption-based conflict analysis. + // We need the solver to support the conflict_providert interface. + auto *conflict_provider = dynamic_cast(&solver); + + // Collect non-constant guard handles as assumptions + std::vector assumptions; + // Track which candidate index maps to which assumption index + std::vector assumption_to_candidate; + + if(conflict_provider != nullptr) + { + for(std::size_t i = 0; i < candidates.size(); ++i) + { + const exprt &gh = candidates[i].guard_handle; + // Only non-constant handles can be checked for conflict. + // Constant-true guards are always active, constant-false + // guards mean the step is unreachable. + if(!gh.is_constant()) + { + assumptions.push_back(gh); + assumption_to_candidate.push_back(i); + } + } + } + + // Perform assumption-based conflict analysis if possible + std::vector in_conflict(candidates.size(), true); + + if(conflict_provider != nullptr && !assumptions.empty()) + { + solver.push(assumptions); + + auto result = solver(); + + if(result == decision_proceduret::resultt::D_UNSATISFIABLE) + { + // Mark all candidates as not-in-core initially + for(std::size_t j = 0; j < in_conflict.size(); ++j) + in_conflict[j] = false; + + // Check each assumption for conflict membership + for(std::size_t i = 0; i < assumptions.size(); ++i) + { + if(conflict_provider->is_in_conflict(assumptions[i])) + in_conflict[assumption_to_candidate[i]] = true; + } + + // Steps with constant-true guards are always active; + // keep them in the core + for(std::size_t i = 0; i < candidates.size(); ++i) + { + if(candidates[i].guard_handle.is_true()) + in_conflict[i] = true; + } + } + // If the result is not UNSAT (unexpected), we fall back + // to marking all steps as in-core (the default). + + solver.pop(); + } + + // Build the result + std::vector result; + for(std::size_t i = 0; i < candidates.size(); ++i) + { + const SSA_stept &step = *candidates[i].step; + + proof_explanation_stept explanation_step; + explanation_step.source_location = step.source.pc->source_location(); + explanation_step.step_type = step_type_string(step); + explanation_step.description = step_description(step, ns); + explanation_step.in_core = in_conflict[i]; + if(step.is_assignment()) + explanation_step.symbols.insert(step.ssa_lhs.get_identifier()); + else if(step.is_assume()) + { + find_symbols_sett syms; + find_symbols(step.cond_expr, syms); + explanation_step.symbols = std::move(syms); + } + + result.push_back(std::move(explanation_step)); + } + + return result; +} + +/// Strip SSA level suffixes from a variable name. +/// SSA identifiers have the form "name!N@M#L0#L1#L2"; +/// this function returns the portion before the first '#'. +static std::string strip_ssa_suffix(const std::string &id) +{ + auto pos = id.find('#'); + if(pos != std::string::npos) + return id.substr(0, pos); + return id; +} + +/// Strip scope encoding from a variable name. +/// CBMC scope-encoded names look like "function::N::name!N@M"; +/// this function extracts just the local name part after the +/// last "::" and before any '!' suffix. +static std::string clean_display_name(const std::string &name) +{ + std::string result = name; + + // Remove the scope prefix (e.g., "main::1::" -> "") + auto pos = result.rfind("::"); + if(pos != std::string::npos) + result = result.substr(pos + 2); + + // Remove renaming suffixes (e.g., "!0@1") + pos = result.find('!'); + if(pos != std::string::npos) + result = result.substr(0, pos); + + return result; +} + +std::vector extract_proof_invariants( + const std::vector &explanation, + const symex_target_equationt &equation, + const namespacet &ns) +{ + // We need to correlate explanation steps back to SSA steps + // to extract the underlying expressions. We collect the + // relevant SSA steps in the same order as the explanation. + std::vector relevant_steps; + for(const auto &step : equation.SSA_steps) + { + if(is_relevant_proof_step(step)) + relevant_steps.push_back(&step); + } + + // Map from stripped variable name to invariant entry. + // Use an ordered map so output is deterministic. + std::map invariant_map; + + // Process each explanation step that is in the core + for(std::size_t i = 0; i < explanation.size() && i < relevant_steps.size(); + ++i) + { + if(!explanation[i].in_core) + continue; + + const SSA_stept &ssa_step = *relevant_steps[i]; + + if(ssa_step.is_assignment()) + { + // For assignments, the key variable is the LHS + const std::string full_id = id2string(ssa_step.ssa_lhs.get_identifier()); + const std::string var_key = strip_ssa_suffix(full_id); + const std::string display = clean_display_name(var_key); + + if(display.empty()) + continue; + + auto &inv = invariant_map[var_key]; + inv.variable = var_key; + inv.display_name = display; + inv.constraints.push_back(explanation[i].description); + } + else if(ssa_step.is_assume() || ssa_step.is_constraint()) + { + // For assumptions/constraints, find all symbol variables + // referenced in the condition expression + std::set symbols; + find_symbols(ssa_step.cond_expr, symbols); + + if(symbols.empty()) + continue; + + for(const auto &sym : symbols) + { + const std::string full_id = id2string(sym.get_identifier()); + + // Skip internal symbols + if( + full_id.find("goto_symex::") != std::string::npos || + full_id.find("return'") != std::string::npos) + { + continue; + } + + const std::string var_key = strip_ssa_suffix(full_id); + const std::string display = clean_display_name(var_key); + + if(display.empty()) + continue; + + auto &inv = invariant_map[var_key]; + inv.variable = var_key; + inv.display_name = display; + inv.constraints.push_back(explanation[i].description); + } + } + } + + // Convert map to vector + std::vector result; + result.reserve(invariant_map.size()); + for(auto &pair : invariant_map) + result.push_back(std::move(pair.second)); + + return result; +} diff --git a/src/goto-checker/proof_explanation.h b/src/goto-checker/proof_explanation.h new file mode 100644 index 00000000000..915d4af2298 --- /dev/null +++ b/src/goto-checker/proof_explanation.h @@ -0,0 +1,156 @@ +/*******************************************************************\ + +Module: Word-level Proof Explanation + +Author: CBMC Contributors + +\*******************************************************************/ + +/// \file +/// Word-level Proof Explanation + +#ifndef CPROVER_GOTO_CHECKER_PROOF_EXPLANATION_H +#define CPROVER_GOTO_CHECKER_PROOF_EXPLANATION_H + +#include +#include + +#include +#include +#include +#include + +class namespacet; +class stack_decision_proceduret; +class symex_target_equationt; +struct SSA_stept; + +/// A single step in a proof explanation, representing a program step +/// that contributes to proving a property. +struct proof_explanation_stept +{ + /// Source location of the contributing step + source_locationt source_location; + + /// Type of the contributing step (e.g., "assignment", "assumption") + std::string step_type; + + /// Human-readable description of why this step contributes + std::string description; + + /// Whether this step is in the unsat core (true by default + /// for backward compatibility with the basic approach) + bool in_core = true; + + /// Symbols referenced by this step (LHS for assignments, + /// all symbols for assumptions). Used by the synthesizer + /// to identify proof-relevant variables. + std::unordered_set symbols; +}; + +/// Extract a word-level proof explanation from an UNSAT result. +/// After the solver returns UNSATISFIABLE, this function iterates +/// over the SSA steps in the equation and identifies which steps +/// contribute to the proof. Steps that are not sliced away and +/// have non-trivial guards or conditions are collected. +/// \param equation: the SSA equation after solving +/// \param ns: the namespace for expression pretty-printing +/// \return a vector of proof explanation steps +std::vector get_proof_explanation( + const symex_target_equationt &equation, + const namespacet &ns); + +// Helpers used by both proof_explanation.cpp and +// goto_symex_property_decider.cpp +std::string step_type_string(const SSA_stept &step); +std::string step_description(const SSA_stept &step, const namespacet &ns); +bool is_relevant_proof_step(const SSA_stept &step); + +/// Extract a word-level proof explanation with unsat core information. +/// After the solver returns UNSATISFIABLE, this function iterates +/// over the SSA steps in the equation and identifies which steps +/// contribute to the proof. Additionally, it uses the solver's +/// assumption-based conflict analysis to determine which steps are +/// truly in the unsat core. Steps whose guard handles are in the +/// conflict are marked with in_core=true. +/// \param equation: the SSA equation after solving +/// \param solver: the decision procedure (must support push/pop) +/// \param ns: the namespace for expression pretty-printing +/// \return a vector of proof explanation steps with core annotations +std::vector get_proof_explanation_with_core( + const symex_target_equationt &equation, + stack_decision_proceduret &solver, + const namespacet &ns); + +/// A word-level invariant extracted from the proof explanation. +/// Groups related constraints by the variable they constrain. +struct proof_invariantt +{ + /// The variable this invariant is about (original SSA name) + irep_idt variable; + + /// Source-level name of the variable (without SSA suffixes) + std::string display_name; + + /// The human-readable expressions constraining this variable + std::vector constraints; +}; + +/// Extract word-level invariants from a proof explanation. +/// Groups core steps by the variables they constrain and +/// produces one invariant summary per variable. +/// \param explanation: the proof explanation steps (with core info) +/// \param equation: the SSA equation used during analysis +/// \param ns: the namespace for expression pretty-printing +/// \return a vector of proof invariants, one per variable +std::vector extract_proof_invariants( + const std::vector &explanation, + const symex_target_equationt &equation, + const namespacet &ns); + +/// Type trait to detect whether a checker type T +/// has a get_proof_explanation() method. +template +struct has_get_proof_explanationt : std::false_type +{ +}; + +template +struct has_get_proof_explanationt< + T, + std::void_t().get_proof_explanation())>> + : std::true_type +{ +}; + +/// Type trait to detect whether a checker type T +/// has a get_proof_invariants() method. +template +struct has_get_proof_invariantst : std::false_type +{ +}; + +template +struct has_get_proof_invariantst< + T, + std::void_t().get_proof_invariants())>> + : std::true_type +{ +}; + +/// Type trait for get_per_property_proof_explanations(). +template +struct has_get_per_property_proof_explanationst : std::false_type +{ +}; + +template +struct has_get_per_property_proof_explanationst< + T, + std::void_t< + decltype(std::declval().get_per_property_proof_explanations())>> + : std::true_type +{ +}; + +#endif // CPROVER_GOTO_CHECKER_PROOF_EXPLANATION_H diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp index 1bf165f4ab8..0209ee82adf 100644 --- a/src/goto-checker/report_util.cpp +++ b/src/goto-checker/report_util.cpp @@ -11,8 +11,6 @@ Author: Daniel Kroening, Peter Schrammel #include "report_util.h" -#include - #include #include #include @@ -24,10 +22,12 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include "bmc_util.h" #include "fault_localization_provider.h" #include "goto_trace_storage.h" +#include "proof_explanation.h" -#include "bmc_util.h" +#include void report_success(ui_message_handlert &ui_message_handler) { @@ -206,7 +206,8 @@ is_property_less_than(const propertyt &property1, const propertyt &property2) std::stoul(id2string(p2.get_line())); const auto split_property_id = - [](const irep_idt &property_id) -> std::pair { + [](const irep_idt &property_id) -> std::pair + { const auto property_string = id2string(property_id); const auto last_dot = property_string.rfind('.'); std::string property_name; @@ -252,9 +253,8 @@ get_sorted_properties(const propertiest &properties) std::sort( sorted_properties.begin(), sorted_properties.end(), - [](propertiest::const_iterator pit1, propertiest::const_iterator pit2) { - return is_property_less_than(*pit1, *pit2); - }); + [](propertiest::const_iterator pit1, propertiest::const_iterator pit2) + { return is_property_less_than(*pit1, *pit2); }); return sorted_properties; } @@ -423,7 +423,9 @@ void output_fault_localization_scores( messaget &log) { log.conditional_output( - log.debug(), [fault_location](messaget::mstreamt &out) { + log.debug(), + [fault_location](messaget::mstreamt &out) + { out << "Fault localization scores:" << messaget::eom; for(auto &score_pair : fault_location.scores) { @@ -443,9 +445,8 @@ max_fault_localization_score(const fault_location_infot &fault_location) fault_location.scores.end(), []( fault_location_infot::score_mapt::value_type score_pair1, - fault_location_infot::score_mapt::value_type score_pair2) { - return score_pair1.second < score_pair2.second; - }) + fault_location_infot::score_mapt::value_type score_pair2) + { return score_pair1.second < score_pair2.second; }) ->first; } @@ -674,6 +675,191 @@ void output_error_trace_with_fault_localization( } } +void output_proof_explanation( + const std::vector &explanation, + ui_message_handlert &ui_message_handler) +{ + messaget log(ui_message_handler); + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + { + if(explanation.empty()) + { + log.result() << "\nProof explanation: no contributing steps found" + << messaget::eom; + break; + } + log.result() << "\nProof explanation:" << messaget::eom; + for(const auto &step : explanation) + { + if(step.in_core) + log.result() << " [core] "; + else + log.result() << " "; + log.result() << "[" << step.step_type << "] "; + if(!step.source_location.get_file().empty()) + log.result() << step.source_location.get_file() << ":"; + if(!step.source_location.get_line().empty()) + log.result() << step.source_location.get_line() << " "; + log.result() << step.description << messaget::eom; + } + break; + } + case ui_message_handlert::uit::JSON_UI: + { + json_stream_objectt &json_result = + ui_message_handler.get_json_stream().push_back_stream_object(); + json_stream_arrayt &json_steps = + json_result.push_back_stream_array("proofExplanation"); + for(const auto &step : explanation) + { + json_objectt json_step; + json_step["stepType"] = json_stringt(step.step_type); + json_step["description"] = json_stringt(step.description); + json_step["inCore"] = jsont::json_boolean(step.in_core); + json_objectt json_location; + if(!step.source_location.get_file().empty()) + { + json_location["file"] = + json_stringt(id2string(step.source_location.get_file())); + } + if(!step.source_location.get_line().empty()) + { + json_location["line"] = + json_stringt(id2string(step.source_location.get_line())); + } + if(!step.source_location.get_function().empty()) + { + json_location["function"] = + json_stringt(id2string(step.source_location.get_function())); + } + json_step["sourceLocation"] = std::move(json_location); + json_steps.push_back(std::move(json_step)); + } + break; + } + case ui_message_handlert::uit::XML_UI: + { + xmlt xml_explanation("proof-explanation"); + for(const auto &step : explanation) + { + xmlt xml_step("step"); + xml_step.set_attribute("type", step.step_type); + xml_step.set_attribute("description", step.description); + xml_step.set_attribute("in-core", step.in_core ? "true" : "false"); + if(!step.source_location.get_file().empty()) + { + xml_step.set_attribute( + "file", id2string(step.source_location.get_file())); + } + if(!step.source_location.get_line().empty()) + { + xml_step.set_attribute( + "line", id2string(step.source_location.get_line())); + } + xml_explanation.new_element().swap(xml_step); + } + log.result() << xml_explanation; + break; + } + } +} + +void output_per_property_proof_explanations( + const std::map> &per_property, + ui_message_handlert &ui_message_handler) +{ + messaget log(ui_message_handler); + if(per_property.empty()) + return; + log.result() << "\nPer-property proof explanations:" << messaget::eom; + for(const auto &entry : per_property) + { + log.result() << "\n Property " << entry.first << ":" << messaget::eom; + for(const auto &step : entry.second) + { + if(!step.in_core) + continue; + log.result() << " [" << step.step_type << "] "; + if(!step.source_location.get_file().empty()) + log.result() << step.source_location.get_file() << ":"; + if(!step.source_location.get_line().empty()) + log.result() << step.source_location.get_line() << " "; + log.result() << step.description << messaget::eom; + } + } +} + +void output_proof_invariants( + const std::vector &invariants, + ui_message_handlert &ui_message_handler) +{ + messaget log(ui_message_handler); + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + { + if(invariants.empty()) + { + log.result() << "\nProof invariants: none" << messaget::eom; + break; + } + log.result() << "\nProof invariants:" << messaget::eom; + for(const auto &inv : invariants) + { + log.result() << " " << inv.display_name << ": "; + for(std::size_t i = 0; i < inv.constraints.size(); ++i) + { + if(i > 0) + log.result() << ", "; + log.result() << inv.constraints[i]; + } + log.result() << messaget::eom; + } + break; + } + case ui_message_handlert::uit::JSON_UI: + { + json_stream_objectt &json_result = + ui_message_handler.get_json_stream().push_back_stream_object(); + json_stream_arrayt &json_invariants = + json_result.push_back_stream_array("proofInvariants"); + for(const auto &inv : invariants) + { + json_objectt json_inv; + json_inv["variable"] = json_stringt(id2string(inv.variable)); + json_inv["displayName"] = json_stringt(inv.display_name); + json_arrayt json_constraints; + for(const auto &c : inv.constraints) + json_constraints.push_back(json_stringt(c)); + json_inv["constraints"] = std::move(json_constraints); + json_invariants.push_back(std::move(json_inv)); + } + break; + } + case ui_message_handlert::uit::XML_UI: + { + xmlt xml_invariants("proof-invariants"); + for(const auto &inv : invariants) + { + xmlt xml_inv("invariant"); + xml_inv.set_attribute("variable", id2string(inv.variable)); + xml_inv.set_attribute("displayName", inv.display_name); + for(const auto &c : inv.constraints) + { + xmlt xml_constraint("constraint"); + xml_constraint.data = c; + xml_inv.new_element().swap(xml_constraint); + } + xml_invariants.new_element().swap(xml_inv); + } + log.result() << xml_invariants; + break; + } + } +} + void output_overall_result( resultt result, ui_message_handlert &ui_message_handler) diff --git a/src/goto-checker/report_util.h b/src/goto-checker/report_util.h index 6976ea7de7e..67cae052b90 100644 --- a/src/goto-checker/report_util.h +++ b/src/goto-checker/report_util.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, Peter Schrammel #include "properties.h" +#include + struct fault_location_infot; class goto_trace_storaget; class goto_tracet; @@ -58,6 +60,21 @@ void output_error_trace_with_fault_localization( const fault_location_infot &, ui_message_handlert &); +struct proof_explanation_stept; +struct proof_invariantt; + +void output_proof_explanation( + const std::vector &, + ui_message_handlert &); + +void output_per_property_proof_explanations( + const std::map> &, + ui_message_handlert &); + +void output_proof_invariants( + const std::vector &, + ui_message_handlert &); + void output_overall_result( resultt result, ui_message_handlert &ui_message_handler); diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 3e2bf918313..bacdca06df2 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -541,6 +541,9 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) if(options.get_bool_option("fpa")) smt2_dec->use_FPA_theory = true; + if(options.get_bool_option("proof-explanation")) + smt2_dec->produce_unsat_cores = true; + return std::make_unique(std::move(smt2_dec)); } else if(filename == "-") diff --git a/src/goto-checker/stop_on_fail_verifier.h b/src/goto-checker/stop_on_fail_verifier.h index f6a26a60132..0fd9e98ff7e 100644 --- a/src/goto-checker/stop_on_fail_verifier.h +++ b/src/goto-checker/stop_on_fail_verifier.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, Peter Schrammel #include "bmc_util.h" #include "goto_verifier.h" +#include "proof_explanation.h" +#include "report_util.h" /// Stops when the first failing property is found. /// Requires an incremental goto checker that is a @@ -47,6 +49,22 @@ class stop_on_fail_verifiert : public goto_verifiert output_properties(properties, 1, ui_message_handler); report_success(ui_message_handler); incremental_goto_checker.output_proof(); + if constexpr(has_get_proof_explanationt::value) + { + if(options.get_bool_option("proof-explanation")) + { + auto explanation = incremental_goto_checker.get_proof_explanation(); + output_proof_explanation(explanation, ui_message_handler); + } + } + if constexpr(has_get_proof_invariantst::value) + { + if(options.get_bool_option("proof-explanation")) + { + auto invariants = incremental_goto_checker.get_proof_invariants(); + output_proof_invariants(invariants, ui_message_handler); + } + } break; case resultt::FAIL: diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 9214c70608e..8e4b4436fab 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -32,6 +32,7 @@ Author: Qinheping Hu #include #include #include +#include #include #include #include @@ -612,6 +613,34 @@ std::optional cegis_verifiert::verify() // Run the checker to get the result. const resultt result = (*checker)(); + // Extract proof-relevant symbols from properties that passed. + // These symbols are in the unsat core and help narrow the search + // space for invariant synthesis. + proof_relevant_symbols.clear(); + if(options.get_bool_option("proof-explanation")) + { + auto per_prop = checker->get_per_property_proof_explanations(); + for(const auto &[prop_id, explanation] : per_prop) + { + for(const auto &step : explanation) + { + if(!step.in_core) + continue; + for(const auto &sym_id : step.symbols) + { + // Strip SSA suffixes (!N@M#L) to get the base symbol name + const std::string id_str = id2string(sym_id); + auto bang = id_str.find('!'); + std::string base_name = + (bang != std::string::npos) ? id_str.substr(0, bang) : id_str; + const auto *sym = ns.get_symbol_table().lookup(base_name); + if(sym != nullptr) + proof_relevant_symbols.insert(sym->symbol_expr()); + } + } + } + } + if(original_verbosity >= messaget::M_DEBUG) checker->report(); @@ -630,7 +659,11 @@ std::optional cegis_verifiert::verify() if(result == resultt::ERROR || result == resultt::UNKNOWN) { - INVARIANT(false, "Verification failed during loop contract synthesis."); + log.error() << "Verification returned " + << (result == resultt::ERROR ? "ERROR" : "UNKNOWN") + << " during loop contract synthesis" << messaget::eom; + restore_functions(); + return std::optional(); } properties = checker->get_properties(); diff --git a/src/goto-synthesizer/cegis_verifier.h b/src/goto-synthesizer/cegis_verifier.h index dc1e1aaa5be..018e1506f44 100644 --- a/src/goto-synthesizer/cegis_verifier.h +++ b/src/goto-synthesizer/cegis_verifier.h @@ -122,6 +122,11 @@ class cegis_verifiert propertiest properties; irep_idt target_violation_id; + /// Symbols identified as proof-relevant by the unsat core for properties + /// that passed verification. Used by the synthesizer to narrow the search + /// space for invariant candidates. + std::set proof_relevant_symbols; + protected: // Compute the cause loops of `violation`. // We say a loop is the cause loop if the violated predicate is dependent diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index f1f878c058b..5ba01623379 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp @@ -30,6 +30,8 @@ Author: Qinheping Hu #include "cegis_evaluator.h" #include "expr_enumerator.h" +#include + // substitute all tmp_post variables with their origins in `expr` void replace_tmp_post( exprt &dest, @@ -228,7 +230,8 @@ void enumerative_loop_contracts_synthesizert::synthesize_assigns( if(assigns_map[loop_id].insert(new_assign).second) return; } - INVARIANT(false, "Failed to synthesize a new assigns target."); + log.warning() << "Failed to synthesize a new assigns target for " + << format(new_assign) << messaget::eom; } void enumerative_loop_contracts_synthesizert::build_tmp_post_map() @@ -262,7 +265,8 @@ enumerative_loop_contracts_synthesizert::compute_dependent_symbols( const std::set &live_vars) { // We overapproximate dependent symbols as all symbols in live variables. - // TODO: using flow-dependency analysis to rule out not dependent symbols. + // The caller may narrow this set using proof-relevant variables from + // the unsat core (see synthesize_all). std::set result; for(const auto &e : live_vars) @@ -373,16 +377,22 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause( size_t count_all = 0; size_t count_filtered = 0; + // Maximum AST size for candidate expressions. Beyond this, the + // grammar produces too many candidates to enumerate in reasonable time. + static constexpr size_t max_enumeration_size = 20; + // Start to enumerate and check. - while(true) + while(size_bound < max_enumeration_size) { size_bound++; + size_t candidates_at_size = 0; // generate candidate and verify for(auto strengthening_candidate : start_bool_ph.enumerate(size_bound)) { - log.progress() << "Verifying candidate: " - << format(strengthening_candidate) << messaget::eom; + candidates_at_size++; + log.debug() << "Verifying candidate: " << format(strengthening_candidate) + << messaget::eom; invariant_mapt new_in_clauses = invariant_mapt(in_invariant_clause_map); new_in_clauses[cause_loop_id] = and_exprt(new_in_clauses[cause_loop_id], strengthening_candidate); @@ -424,8 +434,16 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause( return strengthening_candidate; } } + log.progress() << "Enumeration size " << size_bound << ": checked " + << candidates_at_size << " candidates (" << count_all + << " total, " << count_filtered << " filtered)" + << messaget::eom; } - UNREACHABLE; + + log.warning() << "Failed to synthesize a strengthening clause after " + << "enumerating " << count_all << " candidates up to size " + << max_enumeration_size << messaget::eom; + return true_exprt(); } invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() @@ -483,7 +501,38 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() return_cex->cause_loop_ids.front(), new_invariant_clause, return_cex->live_variables); + + // Narrow dependent symbols using proof-relevant variables from + // properties that passed. This identifies which variables actually + // matter for the proof, reducing the enumeration search space. + if(!verifier.proof_relevant_symbols.empty()) + { + std::set narrowed; + std::set_intersection( + dependent_symbols.begin(), + dependent_symbols.end(), + verifier.proof_relevant_symbols.begin(), + verifier.proof_relevant_symbols.end(), + std::inserter(narrowed, narrowed.end())); + if(!narrowed.empty()) + { + log.debug() << "Narrowed dependent symbols from " + << dependent_symbols.size() << " to " << narrowed.size() + << " using proof-relevant variables" << messaget::eom; + dependent_symbols = std::move(narrowed); + } + } + [[fallthrough]]; case cext::violation_typet::cex_not_preserved: + // When reached directly (not via fallthrough from cex_other), + // dependent_symbols may be empty. Compute them from live variables. + if(dependent_symbols.empty()) + { + dependent_symbols = compute_dependent_symbols( + return_cex->cause_loop_ids.front(), + new_invariant_clause, + return_cex->live_variables); + } terminal_symbols = construct_terminals(dependent_symbols); new_invariant_clause = synthesize_strengthening_clause( terminal_symbols, @@ -493,7 +542,9 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() break; case cext::violation_typet::cex_not_hold_upon_entry: - INVARIANT(false, "unsupported violation type"); + log.warning() + << "Unsupported violation type: invariant does not hold upon entry. " + << "Skipping this counterexample." << messaget::eom; break; } diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h index fd065e7e69f..ff410edaf02 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h @@ -27,6 +27,31 @@ class goto_modelt; /// `goto-instrument` with the `--pointer-check` flag. /// When other checks present, it will just enumerate candidates and check /// if they are valid. +/// +/// ## Known Limitations +/// +/// ### Fixed Grammar +/// The synthesizer uses a fixed grammar for candidate invariants: +/// StartBool -> StartBool && StartBool | Start == Start +/// | Start <= Start | Start < Start +/// Start -> Start + Start | terminal_symbols +/// This cannot express subtraction, multiplication, modular arithmetic, +/// disjunction, or implications. Invariants requiring these operators +/// (e.g., `i == n - 1`, `result == i * step`, `i > 0 ==> arr[i-1] <= arr[i]`) +/// cannot be synthesized. +/// +/// ### No Incremental Solving +/// Each CEGIS iteration creates a fresh SAT solver and re-encodes the +/// entire verification problem. Incremental solving (reusing the solver +/// state and adding clauses for the new candidate) would significantly +/// reduce the per-iteration cost, especially in the inner enumeration +/// loop where many candidates are checked against the same program. +/// +/// ### Per-Iteration Preprocessing +/// The goto model is preprocessed (library linking, asm removal, contract +/// application) on every call to `cegis_verifiert::verify()`. This +/// preprocessing is largely invariant across iterations and could be +/// cached. class enumerative_loop_contracts_synthesizert : public loop_contracts_synthesizer_baset { diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp index 6cd7628010a..f8d1c9cad92 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp @@ -227,6 +227,10 @@ optionst goto_synthesizer_parse_optionst::get_options() // Generating trace for counterexamples. options.set_option("trace", true); + // Enable proof explanations for identifying proof-relevant variables. + // This helps narrow the search space during invariant synthesis. + options.set_option("proof-explanation", true); + parse_solver_options(cmdline, options); return options; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 6e1903359d3..d009dbe53d4 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -198,6 +198,10 @@ void smt2_convt::write_header() out << "(set-option :produce-models true)" << "\n"; + if(produce_unsat_cores) + out << "(set-option :produce-unsat-cores true)" + << "\n"; + // We use a broad mixture of logics, so on some solvers // its better not to declare here. // set-logic should come after setting options @@ -221,6 +225,9 @@ void smt2_convt::write_footer() for(const auto &assumption : assumptions) convert_literal(assumption); out << "))\n"; + + if(produce_unsat_cores) + out << "(get-unsat-assumptions)\n"; } else { diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index a2a8168c8aa..cb46a2cdf9e 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -70,6 +70,10 @@ class smt2_convt : public stack_decision_proceduret bool use_check_sat_assuming; bool use_datatypes; bool use_lambda_for_array; + + /// When true, emit SMT2 options and commands for unsat core + /// extraction (e.g., produce-unsat-cores, get-unsat-assumptions). + bool produce_unsat_cores = false; bool emit_set_logic; exprt handle(const exprt &expr) override; diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 7f516674dda..4f22fa17b7f 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -13,10 +13,20 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "smt2irep.h" #include +static std::string drop_quotes(std::string src) +{ + if(src.size() >= 2 && src.front() == '|' && src.back() == '|') + return std::string(src, 1, src.size() - 2); + else + return src; +} + std::string smt2_dect::decision_procedure_text() const { // clang-format off @@ -35,6 +45,40 @@ std::string smt2_dect::decision_procedure_text() const // clang-format on } +bool smt2_dect::is_in_conflict(const exprt &expr) const +{ + if(expr.id() != ID_literal) + return false; + + const literalt lit = to_literal_expr(expr).get_literal(); + + if(lit.is_constant()) + return false; + + // Build the SMT2 identifier for this literal, matching + // what convert_literal() emits. + std::string smt2_id = convert_identifier("B" + std::to_string(lit.var_no())); + + // The failed_assumptions set may contain quoted or unquoted + // forms; check both. + if(failed_assumptions.count(smt2_id)) + return !lit.sign(); + + if(failed_assumptions.count(drop_quotes(smt2_id))) + return !lit.sign(); + + // Check the negated form for negated literals + const std::string negated = "(not " + smt2_id + ")"; + if(failed_assumptions.count(negated)) + return lit.sign(); + + const std::string negated_unquoted = "(not " + drop_quotes(smt2_id) + ")"; + if(failed_assumptions.count(negated_unquoted)) + return lit.sign(); + + return false; +} + decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption) { ++number_of_solver_calls; @@ -165,14 +209,6 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption) return read_result(in); } -static std::string drop_quotes(std::string src) -{ - if(src.size() >= 2 && src.front() == '|' && src.back() == '|') - return std::string(src, 1, src.size() - 2); - else - return src; -} - decision_proceduret::resultt smt2_dect::read_result(std::istream &in) { std::string line; @@ -233,6 +269,37 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) return decision_proceduret::resultt::D_ERROR; } } + else if(parsed.id().empty() && !parsed.get_sub().empty()) + { + // Check if this looks like an unsat-assumptions response: + // a list of identifiers or (not identifier) forms. + bool looks_like_assumptions = true; + for(const auto &sub : parsed.get_sub()) + { + if(sub.id().empty() && sub.get_sub().empty()) + { + looks_like_assumptions = false; + break; + } + } + + if(looks_like_assumptions) + { + for(const auto &sub : parsed.get_sub()) + { + if(!sub.id().empty()) + { + failed_assumptions.insert(id2string(sub.id())); + } + else if(sub.get_sub().size() == 2 && sub.get_sub()[0].id() == "not") + { + // Store as "(not name)" for negated literals + failed_assumptions.insert( + "(not " + id2string(sub.get_sub()[1].id()) + ")"); + } + } + } + } } // If the result is not satisfiable don't bother updating the assignments and diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h index 2b51118aee2..9fa3795e9ee 100644 --- a/src/solvers/smt2/smt2_dec.h +++ b/src/solvers/smt2/smt2_dec.h @@ -10,8 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_SMT2_SMT2_DEC_H #define CPROVER_SOLVERS_SMT2_SMT2_DEC_H +#include + #include "smt2_conv.h" +#include + class message_handlert; class smt2_stringstreamt @@ -22,7 +26,9 @@ class smt2_stringstreamt /*! \brief Decision procedure interface for various SMT 2.x solvers */ -class smt2_dect : protected smt2_stringstreamt, public smt2_convt +class smt2_dect : protected smt2_stringstreamt, + public smt2_convt, + public conflict_providert { public: smt2_dect( @@ -41,6 +47,10 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt std::string decision_procedure_text() const override; + /// Check whether the given expression is in the unsat core + /// (i.e., was a failed assumption). Only valid after an UNSAT result. + bool is_in_conflict(const exprt &expr) const override; + protected: std::string solver_binary_or_empty; message_handlert &message_handler; @@ -51,6 +61,10 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt std::stringstream cached_output; resultt read_result(std::istream &in); + + /// Set of assumption identifiers reported as failed by the SMT solver + /// after an UNSAT result. Populated by read_result(). + std::set failed_assumptions; }; #endif // CPROVER_SOLVERS_SMT2_SMT2_DEC_H