Lecture 10: SMT & Rosette

1 Purpose

Introduce SMT as generalization of SAT, Rosette as tool that does translation automatically. Show simple validations.

2 Outline

All files should now start with #lang rosette/safe.

SAT & SMT

Last time, we saw how SAT can be used to reason about programs. In particular, how we can encode programs, or at least finite approximations of programs, as SAT formulas, and then use SAT solvers to try to find examples that violate assertions in the programs. This idea, Bounded Model Checking, is quite important, but one limitation to doing it with SAT solvers is that you have to encode everything in terms of booleans, which can lead to massive formula explosion.

SMT solvers are a generalization of SAT solvers that can additionally reason about other data types: integers, bit vectors, etc. This doesn’t make the encoding challenge go away, as you still have to translate the program into a formula, but the language that the formulas can include is much richer, and thus the formulas can be much smaller.

In this class, we aren’t actually going to directly use either a SAT solver or an SMT solver: the encoding challenge is large enough that it would take too much time. Instead, we are going to use a state-of-the-art tool called Rosette, that packages up SMT and additionally does some amount of concrete evaluation, so you can write programs that involve "symbolic variables" that can be solved for, but also write normal functional code that will operate as expected.

Example If we think back to examples from property based testing, we can see how this can be useful.

Sometimes it’s not obvious what the important inputs are. For example, what if we defined a (pathological) multiplication function as:

(require quickcheck)

(define (bad-mult x y)
  (if (= x 10417)
      0
      (* x y)))

Then we could certainly test it with quickcheck:

(define (bad-mult-prop x y)
  (= (bad-mult x y)
     (* x y)))

(quickcheck (property [(x arbitrary-integer)
                       (y arbitrary-integer)]
                      (bad-mult-prop x y)))

Note that here we are using the same quickcheck library that ISL-Spec wraps up, but here using it directly. First we import it with (require quickcheck). The invocation quickcheck corresponds to check-property, and property corresponds to for-all.

While we can run this,more than likely, these test will pass: indeed, on all inputs except x = 10417, the property is true. When we select randomly, the chance that we find this pathological input is quite small. Indeed, this is a general problem: uncommon bugs may be hard to find with PBT. There can even be "common" bugs (i.e., ones that happen a lot), but if the distribution of random inputs don’t happen to hit that input – e.g., I can change the pathological function to:

(define (bad-mult-2 x y)
  (if (> x 10417)
      0
      (* x y)))

And even though there are now tons of bad inputs, our random integers are not uniformly distributed: they are much more frequently small numbers, and as a result, it’s still quite unlikely that this is caught by our testing. We could fix this by coming up with a different distribution for testing, but there’s an issue: now you need to know where the bad inputs are. If you knew that, you might not have had the bug!

There is an alternative: exhaustively testing all inputs. Now, naively doing this would we way too slow. But if remember the bounded model checking idea, if this program could be translated to SAT such that a counterexample corresponds to a satisfying assignment, we can do exhaustive testing in quite reasonable time. e.g., there are SAT solvers that can solve formulas with a half million variables! Naively doing that would take an astronomical amount of time (actually, much longer than astronomical! Our language fails to capture the magnitude of 2^{5000000})

Now, as it turns out, directly encoding things in terms of SAT can be really hard, and lead to massive explosions, so people have been working on developing solvers that can also handle, for example, integers, bit vectors, strings, etc. These so-called SMT (SAT Modulo Theory) solvers underly lots of modern automated tools.

Rosette allows us to do that by defining symbolic variables of a handful of types and then writing assertions. It will then translate portions of your code into SMT and use a solver to see if there is a way to violate the assertion.

In this case, we can define symbolic variables for integers, and then get Rosette to find a falsifying assignment for our bad-mult-prop:

(define-symbolic x y integer?)
(verify (assert (bad-mult-prop x y)))

Rosette has several different purposes, but the only one we will use is verify, which takes some expression (which should involve symbolic values) that contains assertions, and looks for an assignment to those values that causes it to be false. If it finds one, it will say that it found a model, and you can print that model out, or use it in various ways. Thus, it gives a concrete counter-example. If it can prove that there is no such assignment, it will report unsat.

Troubleshooting with Rosette

We use Quickcheck before running Rosette because Rosette will treat any error it finds as a counterexample, which means that if our code always fails (e.g., it has a typo), Rosette will report (model), which means it found a counterexample, but without needing to put any constraints on the symbolic values (hence the model being empty). If you instead first run the code on concrete values (either with Quickcheck, or just by hand), you’ll find those bugs, get stacktraces, and can fix before you go to Rosette.

Second: always put assert inside the call to verify. If you put it outside, it will change the meaning of the query: the assertion will instead we ensured to be true, rather than being used to search for a counter example. What that means is that an otherwise reasonable refactoring to your code (to pull out the expression assert ... as a named variable) will result in (unsat) for no reason.

Creating your own symbolic values

While Rosette has a few built-in types, you can also define your own symbolic values. For example, we can define a symbolic Color as the following:

(define-struct gray [value] #:transparent)
(define choose-color
  (generator-bind
   (choose-integer 0 255)
   (λ(n)
     (choose-one-of (list "red"
                          "green"
                          "blue"
                          (make-gray n))))))

(define (not-gray? c)
  (not (gray? c)))

(quickcheck (property [(c choose-color)]
                      (not-gray? c)))


(require rosette/lib/synthax) ;; for ??
(require rosette/lib/angelic) ;; for choose*

(define-struct rgb [R G B] #:transparent)
(define (symbolic-color) (choose* 'red 'green 
                                  'blue 
                                  (make-rgb (?? integer?) (?? integer?) (?? integer?))))

(define (is-named-color? c)
  (or (equal? c 'red)
      (equal? c 'green)
      (equal? c 'blue)))

(define c (symbolic-color))
(define m1 (verify (assert (is-named-color? c))))
(define m2 (verify (assert (not (is-named-color? c)))))
(evaluate c m1) ; (rgb ??:10:44:45 ??:10:44:59 ??:10:44:73)
(evaluate c m2) ; 'green

(define (symbolic-rgb) (make-rgb (?? integer?) (?? integer?) (?? integer?)))
(define (red-positive? rgb)
  (> (rgb-R rgb) 0))
(define c2 (symbolic-rgb))
(define m3 (verify (assert (red-positive? c2))))
(evaluate c2 m3) ; (rgb 0 ??:10:57:48 ??:10:57:62)