Analyzing Programs with Z3

Tikhon Jelvis

tikhon@jelv.is

Boolean Satisfiability (SAT)

boolean variables

\begin{equation} (x_1 \lor \lnot x_2) \land (x_1 \lor x_3 \lor \lnot x_4) \land \cdots \end{equation}
solves or returns “unsat”

SMT

Satsifiability Modulo Theories

\begin{equation} x_1 \le 10 \land x_3 \le x_1 + x_2 \land \cdots \end{equation}
different types of variables

Different Theories

unbounded integers
real numbers
fixed-size words (bitvectors)
floating point numbers
arrays
more

Z3

SMT solver from Microsoft Research
Open source: MIT license
API bindings in Haskell, OCaml, C♯…

Haskell

SBV
- high-level DSL
- supports multiple solvers
Haskell-Z3
- Z3-specific bindings
- useful for tools backed by Z3

Analyzing Programs

program ⇒ SMT formula
variables:
- inputs
- outputs
- intermediate states
bounded

Solving

solve for outputs: interpreter
solve for inputs: reverse interpreter
intermediate variables: check invariants
compare programs
- verify against specification

IMP

1 + x * 2
(x <= 10) && (y == 5)

side effects:

x := x + 1
⋯ ; ⋯
while cond { ⋯ }
if cond { ⋯ } else { ⋯ }

IMP

\begin{align} A ::&= x & \text{variable}\\ &|\quad n & \text{literal} \\ &|\quad A + A & \\ &|\quad A - A & \\ &|\quad A * A & \\ &|\quad A / A & \end{align}

IMP

data AExp = Var Name
          | Lit Int
          | AExp :+: AExp
          | AExp :-: AExp
          | AExp :*: AExp
          | AExp :/: AExp

data BExp = True' | False' | ⋯

IMP

data Cmd = Skip
         | Set Name AExp
         | Seq Cmd Cmd
         | If BExp Cmd Cmd
         | While BExp Cmd

Inline ⇒ Unroll ⇒ SSA

Inline

def foo(a, b) { <BODY> }
…
foo (1, 2);
stuff;

// fresh names
a := 1;
b := 2;
<BODY>
stuff;

Unroll

while x < 5 { <BODY> }

if x < 5 {
  <BODY>
  if x < 5 {
    … /* bound times */
  } else {}
} else {}

SSA

Single Static Assignment

x := 10;
a := 11;
x := x + a;

x₀ := 10;
a₀ := 11;
x₁ := x₀ + a₀;

if x < 5 {
  x := x + 1;
} else {
  x := x + 2;
}

if x < 5 {
  x₁ := x₀ + 1;
} else {
  x₂ := x₀ + 2;
}
x₃ := φ(x₁, x₂)

Interpreter

aexp :: (Scope Int) → AExp → Int
bexp :: (Scope Int) → BExp → Bool
cmd  :: (Scope Int) → Cmd  → Scope

Compiler

aexp :: (Scope AST) → AExp → Z3 AST
bexp :: (Scope AST) → BExp → Z3 AST
cmd  :: (Scope AST) → Cmd  → Z3 ()

5 + x

\begin{align} bvAdd(&bv(5, 32),\\ &bv(x_0, 32)) \end{align}

Expressions

Lit n     → n
Var x     → lookup scope x
e₁ :+: e₂ → aexp scope e₁ +
            aexp scope e₂

Lit n     → Z3.mkBv 32 n
Var x     → lookup x scope
e₁ :+: e₂ → do e₁ ← aexp scope e₁
               e₂ ← aexp scope e₂
               Z3.mkAdd e₁ e₂

x = 5 + x

\begin{align} \text{assert}(x_1 = bvAdd(&bv(5, 32), \\ &bv(x_0, 32))) \end{align}

Assignment

Set name val →
  let newVal = aexp scope val in
  update name newVal scope

Set name val →
  do newVal ← aexp scope val
     newVar ← Z3.mkFreshBvVar name 32
     eq     ← Z3.mkEq newVar newVal
     Z3.assert eq
     return (update name newVar scope)

if x < 5 {
  x := x + 1
} else {
  x := x + 2
}

\begin{align} &\text{assert}(x_1 = x_0 + 1) \\ &\text{assert}(x_2 = x_0 + 2) \\ &\text{assert}(x_3 = \phi(x_0 < 5, x_1, x_2)) \\ \end{align}

If: φ-functions

If cond c_1 c_2 →
  do cond'   ← bexp scope cond
     scope'  ← compile scope c_1
     scope'' ← compile scope c_2
     makePhis cond' scope scope' scope''

Z3.mkIte cond (lookup name scope₁)
              (lookup name scope₂)

Now What

interpret: starting variables
reverse: final variables
check invariants: intermediate variables
- model checking
- invariants in temporal logic

Temporal Logic

quantified over time
- \(\square P(x)\): \(P(x)\) always holds
- \(\diamond P(x)\): \(P(x)\) eventually holds
- …
safety and liveness

Verification

verify: compare two programs
- assert x1ₙ ≠ x2ₙ, y1ₙ ≠ y2ₙ…
- solve
  - unsat: programs are equal
  - sat: counterexample input

CEGIS

counterexample guided inductive synthesis

Optimization

synthesize faster programs
- original program: spec
- optimize a sliding window of instructions
easier than classic compiler optimizations

Sketching

while x <= ?? {
  x += a * ??
}

Example: Synquid

refinement types

termination measure len
  :: List a -> {Int | _v >= 0} where
  Nil -> 0
  Cons x xs -> 1 + len xs

replicate :: n: Nat -> x: a -> 
             {List a | len _v == n}
replicate = ??