Overview
We have added support for semi-automated proof assistance and repair to Crux, Galois’s symbolic testing tool for C/C++ and Rust. These new capabilities build on support for logical abduction provided by the cvc5 SMT solver that suggests possible facts for failed proof goals, that, when assumed, make the proof goals provable. This feature can be viewed as a form of proof completion for developers adding assertions to their code, or as a form of proof repair for developers modifying previously verified code.
Crux Background
The Crux tool proves properties about programs encoded as source-level assertions by using symbolic execution to prove that properties hold on all possible control paths under all possible inputs. Crux uses symbolic execution to encode C/C++ and Rust programs into SMT formulas, enabling it to prove assertions automatically using SMT solvers. Like most tools in this space, Crux’s typical mode of operation is to either report that it has proved all of its goals (i.e., programmer-provided assertions and memory safety side conditions) or it provides a model that demonstrates the failure. Crux models are assignments of concrete values that, when assigned to their respective symbolic values, drive the program to an assertion failure, serving as a concrete counterexample.
Deductive and Abductive Reasoning
While deductive and inductive reasoning derive new facts from a set of known logical premises, abductive reasoning generates hypotheses with relation to a set of hypotheses and goals. Typically, SMT solvers perform deductive reasoning, which can be considered as either proving that the entailment `H1 ∧ H2 ∧ … ∧ Hn ⊨ G` holds, demonstrating that it does not hold by providing a counter-example, or failing to do either (i.e., timing out).
In the second case above, we can apply abductive reasoning to find an abduct A such that the entailment `H1 ∧ H2 ∧ .. ∧ Hn ∧ A ⊨ G` holds. That is: A is an additional fact that, if assumed, would “fix” the proof of goal G. The abductive reasoning provided by cvc5 is built on its support for Syntax-Guided Synthesis (SyGuS).
From Models to Proof Assistance
While the counterexamples provided by verification tools (derived from SMT solver models) are helpful in understanding failure modes of programs, they do not tell the user of the tool how to fix the problem.
Crux is now able to use abduction to suggest additional assumptions that would make failing goals succeed. If you think of Crux as a tool that enables developers to craft correctness proofs of their software by specifying properties as assertions, then abduction can be seen as assisting in these proofs by establishing necessary assumptions or suggesting fixes to proofs as a software system evolves over time.
Example
As an example of abduction in action, consider the following C program:
//maxint–32.c |
This program allocates a 32-bit symbolic value x, and attempts to prove that x’s successor is always greater than it. This is clearly falsified by integer overflow, which Crux is able to tell us:
$ crux-llvm maxint-32.c --get-abducts 2 --solver=cvc5 |
The output shows that Crux was able to find a counterexample that disproves the goal stated by the check statement. Furthermore, the highlighted lines show that Crux was able to use abduction to suggest two alternatives for an additional assumption that would make the goal hold. While the first one is quite restrictive, the second one suggests to the user that they might not have accounted for overflow of x.
Implementation
We implemented this feature in two parts: 1) adding support for querying the SMT solver for abducts in what4, and 2) adding an option to enable Crux to report abducts to the user when verification fails.
What4 is a Haskell library that provides applications with a solver-agnostic frontend for interacting with SMT solvers. The main interface to what4, from a user point of view, is a uniform representation of logical formulas. It is intended to be a thin wrapper around all of the primitives supported by SMT solvers. It interacts with SMT solvers by translating formulas into SMTLib2, which it sends to SMT solvers in the form of definitions and queries. It also parses the responses from SMT solvers into data structures that can be traversed in Haskell. It supports two modes of operation:
- “One shot” mode where the query term is sent to the SMT solver and a single response is read back
- “Online” mode in an interactive session where multiple queries can be sent to the solver, including support for incremental solving (i.e., using push and pop)
The new features in what4 to support SMT abduction include two new commands: get-abduct and get-abduct-next, which enable a process interacting with the solver to enumerate possible abducts. Note that these new features are currently only supported with the cvc5 solver.
Next, we modified Crux to use these new primitives to produce abducts in cases where the SMT solver falsifies a proof goal. Recall that Crux uses symbolic execution to translate imperative programs into SMT. During this translation step, Crux collects all of the proof goals it encounters into a tree structure with goals to prove as its leaves and the assumptions in scope for each goal as internal nodes. After symbolic execution, Crux traverses the goals tree and attempts to verify that each proof goal always holds by querying the SMT solver. Prior to this work, it would produce a model (i.e., counterexample) for each failing goal.
Recall that, while verifying an assertion p, an automated verification tool like Crux asks the SMT solver if ¬p is satisfiable. If it is, that implies that the goal does not hold on all paths, and the model returned by the SMT solver is a counterexample that demonstrates an input that would cause the assertion to fail. If ¬p is unsatisfiable, the goal is proved to be true.
We have modified Crux to optionally ask the SMT solver for abducts when it falsifies a goal (i.e., ¬p is satisfiable). From the point of view of trying to complete falsified proofs, these could be more useful to the user than counter-models as witnesses of falsified proofs.
Next Steps
Cvc5’s support for abduction is based on Syntax-Guided Synthesis (SyGuS), for which a key component is the syntax guidance, which requires a grammar that specifies the solution space over which abducts are generated. Currently, Crux uses a grammar that admits all possible SMT formulas within the relevant theory of bit-vectors and core primitives such as equality, Boolean connectives.
On the one hand, this could result in the abduction engine spending too much time testing candidate solutions from the space that the user may not be interested in. For instance, from our overflow example above, a solution that involves the division of x by some value might not be of interest to the user, yet the abduction engine might spend a significant amount of its resources testing such a candidate and worse yet, it could offer such a solution to the user; we could improve both performance and quality of outputs by removing division from the grammar.
On the other hand, a grammar with too many constants could lead to the abduction engine quickly suggesting true but unhelpful abducts like assignments of concrete values to variables. The first abduct from our overflow examples suggests constraining x to a value below 1, which is quite unhelpful for a user trying to prove a generic property about x.
Exploring the construction of useful grammars, keeping in mind issues caused by over- and under-constrained grammars, will be a primary focus in future work.