# Analyzing Programs with Z3

## Boolean Satisfiability (SAT)

• boolean variables

$$(x_1 \lor \lnot x_2) \land (x_1 \lor x_3 \lor \lnot x_4) \land \cdots$$
• solves or returns “unsat”

## SMT

• Satsifiability Modulo Theories

$$x_1 \le 10 \land x_3 \le x_1 + x_2 \land \cdots$$
• 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
• API bindings in Haskell, OCaml, C♯…

• SBV
• high-level DSL
• supports multiple solvers
• 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

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₂

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 = ??


## Interactive Tools

• nondeterministic execution
• model concurrency
• debugging aides
• test case generation
• synthesis-powered code completion

## Resources

Created by Tikhon Jelvis.