Using SMT Abductive Reasoning with cvc5

[arjunvish]

Internship goals and tasks for Summer 2022.

Feature

The standard integration with an SMT solver dispatches proof goals. To prove some formula F, we want the SMT solver to determine that ~F is unsatisfiable. If ~F is satisfiable, the solver returns a counterexample instead: values for variables in F for which ~F is true (for which F doesn’t hold). Often, these counterexamples might be unhelpful. Perhaps the variables in F are part of an elaborate encoding which makes it hard to trace back the counterexample value to make it useful. Moreover, a counterexample value might not obviously tell us what would help the SMT solver prove F. A new alternative offered by cvc4/cvc5 is to offer abducts: for F that doesn’t hold, an abduct is a formula H such that H |= F. The goal is to get abducts in addition to counterexamples from the SMT solver so that the user has more information on how to prove F.

Applications:

1. SAW tries to prove equivalences between program specs and implementations by converting them into (mostly) first-order formulas and (among other methods,) asking an SMT solver to prove these equivalences. Often, the SMT solver times out. In such cases, SAW can ask the SMT solver to prove the equivalence, by taking some functions as uninterpreted. This changes the result from timeout/unknown to sat. A counterexample that includes uninterpreted functions isn’t too helpful. The idea is that, in our query to the SMT solver, a fully uninterpreted function would make the solver fail (sat). We want to axiomatize the function just enough so that the SMT solver is able to prove the goal. With the abduction integration, we hope to ask the SMT solver for the axioms about the function which will help us prove the goal.
2. Crux performs symbolic execution of program code to - among other things - check whether assertions hold, via SMT queries. When the SMT solver finds that an assertion doesn’t hold, it returns a counterexample for the assertion. We can imagine asking the SMT solver instead (in addition) for abducts that would entail the assertion.

Examples:

SAW

Here is a manufactured example, suggesting the kind of problems we hope this integration will help solve. We ask cvc4 to prove t1 in the following, making f uninterpreted:

let {{
    f x y = (x : [32]) + y
}};
t1 <- {{ \a b c -> (a == b + 1) ==> f b c == f c (a - 1) }};
prove_print (w4_unint_cvc4 ["f"]) t1;

and it fails:

prove: 1 unsolved subgoal(s)
Invalid: [a = 2, b = 1, c = 0]

In the following, I have extracted the SMT script from the query to cvc4 above, modified it to ask for 5 abducts, and restricted the grammar over which the solver can produce abducts:

(set-option :produce-abducts true)
(set-option :incremental true)
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_UFBV)
(define-fun s3 () (_ BitVec 32) #x00000001)
(declare-fun s0 () (_ BitVec 32))                                                      ;variable "x0_a"
(declare-fun s1 () (_ BitVec 32))                                                      ;variable "x1_b"
(declare-fun s2 () (_ BitVec 32))                                                      ;variable "x2_c"
(declare-fun |f#826| ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))     ;uninterpreted function f

(define-fun s4 () (_ BitVec 32) (bvadd s1 s3))   ;b + 1
(define-fun s5 () Bool (= s0 s4))   ;a = b + 1
(define-fun s6 () (_ BitVec 32) (|f#826| s1 s2))   ;f b c
(define-fun s7 () (_ BitVec 32) (bvsub s0 s3))   ;a - 1
(define-fun s8 () (_ BitVec 32) (|f#826| s2 s7))   ;f c (a - 1)
(define-fun s9 () Bool (= s6 s8))   ;(f b c) = f c (a - 1)
(define-fun s10 () Bool (not s5))   ;~(a = b + 1)
; Final goal (implication unfolded): (f b c = f c (a - 1)) v ~(a = b + 1)
(define-fun s11 () Bool (or s9 s10))
; Goal negated for unsat query: ~((f b c = f c (a - 1)) v ~(a = b + 1))
(define-fun s12 () Bool (not s11))

; -- finalAssert ---
;(assert s12)
;(check-sat)

;Give me 5 abducts with the give grammar, the disjunction of which would entail s11
(get-abduct abd s11
((GB Bool) (GBV32 (_ BitVec 32))) ;Grammar non-terminals
  ( ;Grammar rules    
      (GB Bool (
                ;(bvult GBV32 GBV32) (bvugt GBV32 GBV32)   ;unsigned comp
                ;(bvslt GBV32 GBV32) (bvsgt GBV32 GBV32)   ;signed comp
                (= GBV32 GBV32) (not GB) (and GB GB) (or GB GB)   ;both
               ))
      (GBV32 (_ BitVec 32) (
                s0 s1 s2   ;variables
                #x00000001 #x00000000 #xFFFFFFFF   ;constants
                (|f#826| GBV32 GBV32)   ; uninterpreted functions
                ;(bvnot GBV32) (bvand GBV32 GBV32) (bvor GBV32 GBV32) (bvxor GBV32 GBV32)   ;logical
                ;(bvneg GBV32) (bvadd GBV32 GBV32) (bvsub GBV32 GBV32)   ;linear arithmetic
                ;(bvmul GBV32 GBV32)   ;mult   
                ;(bvudiv GBV32 GBV32) (bvurem GBV32 GBV32)   ;unsigned div/rem
                ;(bvsdiv GBV32 GBV32) (bvsrem GBV32 GBV32)   ;signed div/rem
                ;(bvshl GBV32 GBV32) (bvlshr GBV32 GBV32)   ;shifts
                ;(bvashr GBV32 GBV32)   ;signed shift
                ;(ite GB GBV32 GBV32)   ;ite
            ))
  )
)
(get-abduct-next)
(get-abduct-next)
(get-abduct-next)
(get-abduct-next)

The solver gives me the following 5 abducts:

a = b
b = c
f b c = f c b
x = y ^ x = z
x = y ^ x = 1

The third one might suggest to the user that the SMT solver doesn’t need the entire interpretation of f, but just that it is commutative. One can imagine the following integration: with f fully interpreted, the solver times out (this doesn't actually happen with this example). So the user sees if the goal can be proved by the solver with f uninterpreted, but it fails. Now the user has a third option of asking the solver some details (primarily about f) that would help the solver prove the goal, without the entire definition of f. For this integration to work, we need to be able to call the get-abduct and get-abduct-next commands from cvc5, we need a better interface for the user to be able to specify the symbols over which they want abducts (as opposed to the clunky grammar I have manipulated above in the SMTLib script), and perhaps some smart way for SAW to choose default grammars.

Crux

From the Crux release blogpost, the following code returns a counterexample of MAX_INT for x:

#[crux_test]
fn test_inc_correct_symbolic() {
    let x = u32::symbolic("x");
    assert!(x + 1 > x);
}

This corrected code is proved by the SMT solver:

#[crux_test]
fn test_inc_correct_good() {
    let x = u32::symbolic("x");
    if(x != u32::MAX) {
        assert!(x + 1 > x);
    }
}

The following SMT script asks for 5 abducts for code snippet 1, also with a restricted grammar:

(set-option :produce-abducts true)
(set-option :incremental true)
(set-logic QF_BV)
(declare-fun x () (_ BitVec 32))   ;variable x

;Give me 5 abducts with the give grammar, the disjunction of which would entail the assertion
(get-abduct abd (bvugt (bvadd x #x00000001) x)
((GB Bool) (GBV32 (_ BitVec 32))) ;Grammar non-terminals
  ( ;Grammar rules    
      (GB Bool ((= GBV32 GBV32) (not GB) (and GB GB) (or GB GB)   ;both
                (bvult GBV32 GBV32) (bvugt GBV32 GBV32)   ;unsigned 
                ;(bvslt GBV32 GBV32) (bvsgt GBV32 GBV32)   ;signed
               ))
      (GBV32 (_ BitVec 32)  (x   ;variables
                   #x00000001 #x00000000 #xFFFFFFFF   ;constants
                          ;(bvnot GBV32) (bvand GBV32 GBV32) (bvor GBV32 GBV32) (bvxor GBV32 GBV32)   ;logical
                          (bvneg GBV32) (bvadd GBV32 GBV32) (bvsub GBV32 GBV32) (bvmul GBV32 GBV32)   ;arithmetic
                          ;(bvudiv GBV32 GBV32) (bvurem GBV32 GBV32)   ;div/rem
                          ;(bvsdiv GBV32 GBV32) (bvsrem GBV32 GBV32)   ;signed div/rem
                          ;(bvshl GBV32 GBV32) (bvlshr GBV32 GBV32)   ;shifts
                          ;(bvashr GBV32 GBV32)   ;signed shifts
                          (ite GB GBV32 GBV32)))   ;ite
  )
)
(get-abduct-next)
(get-abduct-next)
(get-abduct-next)
(get-abduct-next)

Again, grammar restriction is crucial. Manually, since I see + in the input assertion, I use all arithmetic operators in the grammar, since I see unsigned >, I use all unsigned comparison operators, and the constants 0, 1, and MAX_INT since it might be useful to have abducts over them. This process is to be automated, or delegated to the user or some combination thereof. The result from the SMT solver:

(define-fun abd () Bool (= x #b00000000000000000000000000000001))
(define-fun abd () Bool (= x #b00000000000000000000000000000000))
(define-fun abd () Bool (bvult x #b00000000000000000000000000000001))
(define-fun abd () Bool (bvult x #b11111111111111111111111111111111))
(define-fun abd () Bool (= (bvneg x) x))

One of the 5 formulas would suffice to prove the previously unprovable goal from code snippet 1. A user might find the 4th solution most useful and comparable to the guard used in the conditional in code snippet 2.

Tasks:

• [x] Add cvc5 to what4's solvers.
• [x] Add a get-abduct feature to what4’s cvc5 interface.
  • [x] Offline
  • [x] Ability to ask for n abducts
  • [x] Online
  • [x] cvc5 has a bug where grammars are produced over the define-fun variables when global-declarations are on. Fixed by this PR. This is part of the cvc5-1.0.1 release.
  • [x] cvc5 doesn't allow produce-abducts and produce-unsat-cores to be turned on together. This is a complex patch consisting in at least 3 (1, 2, 3) PRs and their corresponding commits.
  • [x] cvc5 throws the parse error "Overloaded constants must be type cast." when define-funs interact with named variables in some way. Fixed here.
  • [x] Update flake and what4 to use cvc5-1.0.1 which addresses the first issue.
  • [x] Once its out (expected in the next month), update flake and what4 to ise cvc5-1.0.2 which will address the last 2 issues.
  • [x] In the meantime, we will deal with issue 2 as follows. Since get-abduct and unsat-cores aren't compatible, what4 will automatically turn off unsat-cores when get-abduct is turned on, make get-abduct an opt-in feature.
• [ ] Allow grammar modifications. We do this in a separate branch for now.
  • [x] In what4, allow to specify grammar.
  • [ ] We define a new ADT for SMT sorts. Can we use something that's already defined in what4?
  • [ ] Automatically find the grammar from the goal. Pattern match on the goal so we can add each symbol to the grammar.
• [x] Integrate abduction with crux
  • [x] Add cvc5 as a solver
  • [x] Build a small example suite. This is tracked here.
  • [x] Add an interface to what4 so that we can add a new assertion frame in which to perform the final assertion and the check-sat. This stack frame needs to be popped before calling get-abduct.
  • [x] In online solving, go through all the goals, and if they're sat, ask for 3 abducts.
  • [x] Add an option to get n abducts and run the abduction code only if the option is turned on and asks for more than 0 abducts.
  • [x] Automatically turn off unsat-cores when --get-abducts n with n > 0.
• [ ] Crux integration extensions:
  • [ ] Arrays:
  • [ ] How does abduction interact with arrays? Test some examples.
  • [ ] We would like abducts in term of an array length to mention the length. Can we use uninterpreted functions for this? Can we annotate the length of the array so that it isn't forgotten when assertion frames change, and then use this annotation in the abduct?
  • [ ] Pretty-printing:
  • [ ] Currently abducts are printed on to cmd, can we put them in the HTML files?
  • [ ] Abducts are in terms of SMT, can we write them in terms of C?
  • [x] Minor, but remove those quotes around abducts, and add bullets for them.
  • [ ] UI
  • [ ] We ask the abduction tactic for n abducts and it either passes or fails, instead can we have a mode where it can give abducts incrementally?
  • [x] Can we separate online solving with abduction from online solving? Either add an entirely new tactic, or make it optional to call the tactic with abduction.
  • [ ] When abduction is invoked in crux, it should automatically default to cvc5.
  • [ ] How much does what4 rewrite the initial problem, and what does that do to abducts?
  • [ ] LLVM icmp returns a bool which crux/crucible turns into a 1 bit BV and then pads it using an ITE. If this is done automatically, perhaps we would benefit from replacing this whole thing by a much simpler translation of this construct, one that avoids all the (potentially) unnecessary padding and ITEs.
• [ ] Integrate abduction with SAW

[RyanGlScott]

Oops, I think that was accidentally closed by merging GaloisInc/crucible#1037. That does address a number of bullet points in this issue, but not all of them.