In my research, I make heavy use of SMT solvers to build software verification tools (specificially, Microsoft’s Z3). Anyone who’s tried writing this sort of software eventually runs into a fundamental question: what interface should I use between my tool and the solver?

In general, there are two strategies for implementing this integration:

1. Use the z3 standalone executable, and pass it queries through its command line interface. This strategy requires that you first output queries in a file format such as SMT-LIB2. I call this strategy “lightweight” integration.

2. Integrate with Z3 at the API level by using or writing FFI bindings with the underlying C API. Rather than encoding queries as text files and sending them in batch to Z3, you use relevant API calls to construct and dispatch queries in memory. I call this strategy “heavyweight” integration.

Advantages of lightweight integration

1. Significantly eases the burden of debugging queries. You have a text file that you can examine, edit, and debug as you please. These queries files also serve as persisted “proofs”.

2. Does not require the existence of a binding library between your language and Z3.

3. Isolates errors in your tool from those in Z3. If your program crashes, you can be sure it wasn’t because of something like a segfault in Z3 (so long as you have adequate checks for z3 abnormal termination).

4. Compatibility with other SMT solvers. The SMT-LIB2 format is a standard that is mostly compatible with other solvers as long as you don’t make use of Z3-specific constructs.

Advantages of heavyweight integration

1. Faster. Lightweight integration is comparatively slow due to the overhead of writing files and invoking an external process for each dispatch to z3. Some verification tools can dispatch hundreds of thousands of small queries, and IO+process overhead can be quite significant.

2. Allows incremental computation. Rather than sending an entire query at once, you can make use of features like push and pop all within a single Z3 process. This also makes use of Z3’s internal ability to cache incremental results.

Regardless of your integration strategy, it’s a good idea to isolate the low-level Z3 interface from a higher-level interface for constructing queries at a higher level of abstraction.

For instance, I encapsulate my low-level lightweight Z3 interface in a Scala module called Z3 that defines types corresponding to entities at the logic level. These types essentially map one-to-one to language entities in SMT-LIB2. Here’s a skeleton of Z3, although I’ve omitted a lot for brevity:

object Z3 { // binary operations sealed trait Bop case object Add extends Bop case object Sub extends Bop ... // expressions sealed trait Expr case class EBin(b: Bop, e1: Expr, e2: Expr) extends Expr case class EVar(s: String) extends Expr ... // predicates sealed trait Pred case object PTrue extends Pred case object PFalse extends Pred case object PAnd(ps: Seq[Pred]) extends Pred case object PAtom(b: Brel, e1: Expr, e2: Expr) extends Pred ... // relations sealed trait Brel case object Eq extends Brel case object Ne extends Brel ... // types sealed trait Ty case class BoolTy extends Ty case class IntTy extends Ty ... // declarations sealed trait Declaration case class ConstDeclaration(name: String, ty: Ty) extends Declaration ... // assertions case class Assertion(p: Pred) // commands sealed trait Command case object CheckSat extends Command ... def toQuery(decls: Seq[Declaration], assns: Seq[Assertion]): String = { ... } def executeRaw(q: String): String = { ... } def isSat(decls: Seq[Declaration], assns: Seq[Assertion]): Boolean = { executeRaw(toQuery(decls, assns)) match { case "unsat" => false case "sat" => true case _ => // ... error } } }

The function toQuery constructs a query string from a set of declarations and assertions by recursive construction. executeRaw then simply emits the query string to a file, invokes z3, waits for it to terminate, then returns the output of z3. isSat, as its name suggests, just returns true if the supplied system of constraints (assertions) is satisfiable by using toQuery and executeRaw under the hood.

I then have a higher level module called Check that translates verification obligations from the source language being verified down to types from the Z3 module. To check those obligations, it invokes isSat with a properly crafted set of assertions:

object Check { def check(pre: SExpr, path: SPath, post: SExpr): Boolean = { ... } ... }

In particular, the function check verifies that any program state satisfying the precondition pre entails the postcondition post after executing path, so long as path terminates. In more formal terms, it checks that the strongest postcondition of pre with respect to path implies post. I’ve elided the contents of check because its implementation depends greatly on the source language, but the general idea is to translate path into a sequence of assertions where each assertion encodes the effect of a statement in that path. We then check the validity of the encoded formula $pre \land path \rightarrow post$ by checking that the formula $pre \land path \land \lnot post$ is unsatisfiable.¹

What makes Check high-level? Well, the module’s public interface makes no reference to the low-level types from Z3, but rather types corresponding to elements of the source language being verified: SExpr is the type of expressions in the source language, and SPath encodes a sequence of statements along an execution path. Thus, one can use Check without ever having to worry about the underlying logic or constraint solving engine.