Have you ever thought how exciting verification tools are? How do you prove the correctness of a program? Of course, the green tests bring some confidence… but we all know it’s not a proof.
Pex Logo

Just look at Pex, it definitely can’t leave anybody cold (recommendation: skip this step for now, it was a trap).

But this story is not about Pex, but what powers it - Z3, an efficient SMT solver from Microsoft Research. You may ask why you should care (at least I always  do when looking at something new - a tool/language/app/whatever), the answer is simple - because we want the proof, not only a bunch of valid inputs. The work made me a bit paranoid to this point - it takes more time, but the shining correctness allows you not to worry about how much customers can lose just because someone forgot about a not-likely-to-happen workflow, like an unexpected negative number from nowhere -> power -> NaN (surprise, surprise!).

Resources:

Z3 Logo * Z3 on codeplex, with documentation, papers and slides.
* Try it online with Rise4Fun.
* Z3 Constraint Solver on Ch9 .
* Original home of Z3 project.

Z3 is supported on Windows, OSX, Linux and FreeBSD and has an extensive API:  C, C++, OCaml, .NET languages, Python, Java.

Z3 + Mono

The standard Z3 distrubution for OSX comes with x64 binaries, but to get it working with Mono we need to compile it ourselves with x86 architecture.

1. Download the sources here.
2. Open the folder and generate the makefiles.

1
2
python scripts/mk_make.py
cd build

3. We’re interested in config.mk file. By default the result architecture is x86_x64, that’s where the compiler flags help:

1
2
3
4
5
CXXFLAGS= -D_MP_INTERNAL -m32  -c -fopenmp -mfpmath=sse -O3
 -D _EXTERNAL_RELEASE -fomit-frame-pointer -fPIC -msse -msse2
LINK_FLAGS=-m32
SLINK_FLAGS=-dynamiclib

Update: according to the Yu’s comment you might need to replace the option -fopenmp with -D_NO_OMP_.

4. Just make it 1. The recent Z3 versions require a little change as compiler gives typename outside of template error, I just removed typename from fdd.h.

5. Check the architecture

1
2
$ lipo -info libz3.dylib
Non-fat file: libz3.dylib is architecture: i386

6.  cd to z3/src/api/dotnet folder and compile Microsoft.Z3.csproj with Mono/.NET 4.0 as a target framework 2. Also you’d need to add a config file to map libz3.dll to our fresh native libz3.dylib.

1
2
3
4
<?xml version="1.0" encoding="utf-8">
<configuration>
    <dllmap dll="libz3.dll" target="libz3.dylib" os="osx" cpu="x86"/>
</configuration>

Now we are ready to try it!

Examples time

Let’s start with a simple script using official Z3 API, the C# version of examples below can be found in Z3 repository. There’s also a nice set of F# examples - I couldn’t leave it just in comments - Z3Fs, a DSL to solve SMT problems by  @dungpa.

For simplicity we assume that Microsoft.Z3.dll, config and libz3.dylib are in the script’s folder.

Prove that x = y implies g(x) = g(y).

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
#r "Microsoft.Z3.dll"  

open System
open Microsoft.Z3
open Microsoft.FSharp.Quotations
open DerivedPatterns
open Patterns  
  
let prove (ctx: Context) f =  
    let s = ctx.MkSolver()  
    s.Assert (ctx.MkNot f)  
    match s.Check() with  
    | Status.UNKNOWN     -> printfn "unknown because %A" s.ReasonUnknown  
    | Status.SATISFIABLE -> printfn "error"  
    | _                  -> printfn "ok, proof: %A" s.Proof  


///Prove that x = y implies g(x) = g(y)
let proveSample() =  
    // create context
    let prms = System.Collections.Generic.Dictionary(dict [ "proof", "true" ])
    let ctx  = new Context(prms)

    // create uninterpreted type
    let U = ctx.MkUninterpretedSort (ctx.MkSymbol "U")
    // declare function g
    let g = ctx.MkFuncDecl("g", U, U)

    // create x and y
    let x = ctx.MkConst("x", U)
    let y = ctx.MkConst("y", U)
    // create g(x), g(y)
    let gx, gy = g.[x], g.[y]

    // assert x = y
    let eq = ctx.MkEq(x, y)

    // prove g(x) = g(y)
    let f = ctx.MkEq(gx, gy)
    printfn "prove: x = y implies g(x) = g(y)"
    prove ctx (ctx.MkImplies(eq, f))

proveSample()

Well, it’s a pain to write all those ctx.Mk*. That’s where F# quotations come to hand. Some papers and slides mention Z3 support for quotations, though they seem to be a bit outdated - haven’t seen anything similar in the sources. Here is an example of what it can look like.

Simplify expression “x + (y - (x + z))”

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
/// SimplifiedSpecificCall
let inline (|Func|_|) expr =
    match expr with
    | Lambdas(_, (Call(_, minfo1, _))) -> function
	   | Call(obj, minfo2, args) when minfo1.MetadataToken = minfo2.MetadataToken -> Some args
	   | _ -> None
    | _ -> failwith "invalid template parameter"

/// From quotations to Z3 objects
let z3 expr =
    // create context
    let prms = System.Collections.Generic.Dictionary(dict [ "proof", "true" ])
    let ctx  = new Context(prms)
    let rec unquote expr =
        match expr with
        | Func <@@ (+) @@> [x; y] -> ctx.MkAdd (unquote x, unquote y)
        | Func <@@ (-) @@> [x; y] -> ctx.MkSub (unquote x, unquote y)
        | Lambdas (_, e)          -> unquote e
        | Var var                 -> ctx.MkIntConst var.Name :> ArithExpr
        | x                       -> failwithf "unknown expression %A" x
    unquote expr

/// Simplify expression "x + (y - (x + z))"
let simplifier() =
    let t1 = z3 <@@ fun x y z -> x + (y - (x + z)) @@>  
    let t2 = t1.Simplify()
    printfn "%A -> %A" t1 t2

simplifier()

Looks much better, doesn’t it?

Next time: bringing another f-language to mono…


  1. don’t forget to clean up (.a and .obj files) the folder if you have built x64 lib before. [return]
  2. MD-generated makefile & co are available on github [return]