Passes for CHC-based invariant inference - #168
Conversation
There was a problem hiding this comment.
The code generally looks fine but the load/store encoding seems to not work yet. For the final version it would be good to achieve parity with the python implementation up to the loopy benchmarks if its possible. We can set the test up like here https://github.com/UQ-PAC/bincaml-test/tree/main/gtirb, happy to help with that if needed.
full-ssa → load-store-reduction → lambda-lifting this sequence requirement can also be expressed now with the new pass dependency system.
| (precondition queries at the call site, postcondition queries on the body) | ||
| is performed independently of [use_spec] whenever the callee has a | ||
| [requires] or [ensures]. *) | ||
| let encode_block ~(use_spec : Program.proc -> bool) (prog : Program.t) |
There was a problem hiding this comment.
Most of the inner functions in this function should be made top-level so its clear they only depend on their in-parameters rather than any prior local definitions. In particular translation of regular statements, calls, and blocks should be different top-level functions.
fdcdb3e to
12a5096
Compare
This has been simplified as load-store reduction and lambda-lifting now happen internally in the CHC encoding process. I have added SSA as a dependency. Technically, the CHC pass works fine without SSA. However, I think it still makes sense to include it as a dependency, so that people run SSA before it. If SSA is run after it, the loop invariants can get messed up: the assertions (encoding the invariants) are no longer the first statement in the block, which seems to have the effect of Boogie no longer accepting them. |
44c5649 to
9127b9d
Compare
Loopy tests added here: UQ-PAC/bincaml-test#1 The CHC pass completes on 460/468 benchmarks. For 3 benchmarks, Z3 crashes; for the other 5, bincaml SSA crashes (I can open an issue). CHC solver results (timeout of 10s):
Boogie verifies 316 benchmarks (annotated with the inferred invariants). |
| | _ -> BasilExpr.fix node) | ||
| | None -> BasilExpr.fix node) | ||
| | _ -> BasilExpr.fix node) | ||
| | _ -> BasilExpr.fix node) |
There was a problem hiding this comment.
This should be much simpler, with BasilExpr.unfix3 and BasilExpr.rewrite_down rather than cata; it should have one match on multiple levels of the ast rather than 4 levels of nested match. It probably makes mores sense using downard recursion rather than upward.
| in | ||
| list [ atom "assert"; forall_ binders body ] | ||
|
|
||
| type solve_result = Sat | Unsat | Unknown |
There was a problem hiding this comment.
Could put the model in the SAT case rather than returning a tuple
2 participants
This PR adds passes for inferring program invariants (loop invariants, and pre/postconditions) in the Basil IL using CHC solving. In short, the passes encode the program's IL as CHCs, and then uses a CHC solver to find a model; the invariants are extracted from the CHC model and then added to the IL as assertions.
The two invariant-inference passes are:
chc-infer-invariants: this pass is all or nothing - it finds invariants strong enough to discharge all obligations, or nothingchc-infer-invariants-per-query: this pass infers invariants on a per-query basis (e.g., per assertion/pre/postcondition), which means that it can find invariants that are strong enough to discharge some, but not all obligationsRight now, we use Z3/Spacer to do the CHC solving; it should be possible to add support for other CHC solvers, like Eldarica, in the future.
The encoding of the IL into CHCs is based on the encoding used in this paper: Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving. However, we have augmented the encoding to support pre/postcondition specs for procedures.
use_specsover procedures; ifuse_specs pis true for some procedurep, then the pre/postconditions forpare inlined at call sites ofp, instead of generating CHCs encoding that control flow goes to the actual body ofpuse_specs preturns true iff the procedurephas non-trivial specificationsThis PR also adds aload-store-reductionpass, which uses some of the pre-processing infrastructure from the Boogie backend to simplify the IL; it is required to run this pass before the CHC invariant inference passes. In particular, we require this sequence of passes to be run first:full-ssa → load-store-reduction → lambda-lifting.