Generating SMT from traces

ARM logo In a previous post about formal validation of the Arm architecture I sketched how you can reason about Arm’s processor specifications using SMT solvers such as Z3, Boolector and CVC4. The main idea is that you translate ASL (the language that Arm’s specifications are written in) to SMT-Lib2 (the language that SMT solvers accept).

The main challenge in doing this translation is that although SMT has almost all the arithmetic operations that ASL uses, it has none of the conventional programming language features such as function calls, assignments, if-statements, for-loops, while loops, polymorphism, dependent types, exceptions, etc. This makes generating SMT quite complex and my previous post is really only a rough sketch of the main steps you have to go through. In this post, I am going to describe an easier way that gives you a lot of the benefit for a fraction of the effort.

There are two parts to the technique:

  1. Generating execution traces
  2. Translating traces to SMT

(In fact, it is easy to skip the step of generating traces and directly generate SMT — but it is easier to explain and easier to debug if you generate a trace and then translate that to SMT.)

Execution traces

In this simplified version of SMT generation, we are not going to translate the entire specification at once. Instead, we will execute the specification in an interpreter and generate a trace of the path generated by that particular execution. A lot of the complexity of generating SMT comes from handling multiple paths (e.g., handling both sides of an if-statement, multiple iterations of a loop, etc.); by focussing on just one possible path through the program at a time, we avoid all that complexity. This will let us use SMT solvers to reason about all possible behaviours that follow the same path through the code.

As an example, I’m going to work with this function that is used to specify the “Add with carry” instruction “ADC” that contains two branches.

// AddWithCarry()
// ==============

(bits(N), bit, bit) AddWithCarry(bits(N) x, bits(N) y, bit carry_in)
    unsigned_sum = UInt(x) + UInt(y) + UInt(carry_in);
    signed_sum   = SInt(x) + SInt(y) + UInt(carry_in);
    result       = unsigned_sum[0 +: N];  // same value as signed_sum[0 +: N]
    carry_out    = if UInt(result) == unsigned_sum then '0' else '1';
    overflow     = if SInt(result) == signed_sum then '0' else '1';
    return (result, carry_out, overflow);

What we want to generate when we execute this function on some input like “N: 32; x: -5, y: 4, carry_in ‘1’”. is a trace that shows all the intermediate calculations and (crucially) the dependencies between them. There is no standard format for these traces so I am just going to make something up that will be fairly easy to read and fairly easy to translate to SMT.

; AddWithCarry(bits(N) x, bits(N) y, bit carry_in)
input x        : bits(32) = %1
input y        : bits(32) = %2
input carry_in : bits(1)  = %3

; unsigned_sum = UInt(x) + UInt(y) + UInt(carry_in);
%4 = cvt_bits_uint(%1)
%5 = cvt_bits_uint(%2)
%6 = add_int(%4, %5)
%7 = cvt_bits_uint(%3)
%8 = add_int(%6, %7)

; signed_sum   = SInt(x) + SInt(y) + UInt(carry_in);
%9  = cvt_bits_sint(%1)
%10 = cvt_bits_sint(%2)
%11 = add_int(%9, %10)
%12 = cvt_bits_uint(%3)
%13 = add_int(%11, %12)

; result       = unsigned_sum[0 +: N];  // same value as signed_sum[0 +: N]
%14 = getslice_bits(0, 32, %8)

; carry_out    = if UInt(result) == unsigned_sum then '0' else '1';
%15 = cvt_bits_uint(%14)
%16 = eq_bits(%15, %8)
branch %16 = FALSE
%17 = '1'

; overflow     = if SInt(result) == signed_sum then '0' else '1';
%18 = cvt_bits_sint(%14)
%19 = eq_bits(%18, %13)
branch %19 = TRUE
%20 = '0'

; return (result, carry_out, overflow);
output return.1 = %14
output return.2 = %17
output return.3 = %20

This trace has three kinds of entries:

  1. Calculations such as “%6 = add_int(%4, %5)”. These are the most important part of the trace since they are what we translate to SMT.
  2. Input/output statements that will tell us what the inputs and outputs of the calculation are.
  3. Path statements such as “branch %16 = FALSE” that tell us that there was a branch in the control flow and, in this particular execution, the condition was FALSE. These statements let us explore what behaviour occurs if we stay on the same path as this trace and they let us solve for inputs that would deviate from this path.

Since we are generating the trace from an execution with concrete input values, things don’t get any harder as we add more language features: if statements, case statements, etc. just add some more conditional branches; etc.

Well, not quite… There are a small number of places in the Arm specs where the value in some register is used to calculate the width of some value. e.g., if you imagine that “LogPageSize” contains the log2 of the size of memory pages, then you might find something like this:

page_number = address[31 : UInt(LogPageSize)];

The solution is just to remember the bitwidth used and record it as another constraint on the trace in the same way that we treat the branches taken as a constraint on the trace.

Generating execution traces

I generated the above trace by hand (so it probably has an error or two in it) but it is easy to generate a trace like this by modifying an interpreter. The key change is to modify how values are represented and then to modify all the builtin functions to use this new representation.

If your interpreter is written in Haskell, it probably represents values like this:

data Value = VInt Integer | VBool Boolean | VTuple [Value] | ...

and the add_int primitive is probably written like this:

add_int :: Value -> Value -> Value
add_int (VInt x) (VInt y) = VInt (x+y)

To generate a trace like the above, you need to uniquely number the result of each calculation and primitives have to generate trace. So you might change the code to:

data RawValue = VInt Integer | VBool Boolean | VTuple [Value] | ...
type Value = (Int, RawValue)

add_int :: Value -> Value -> IO Value
add_int (nx, VInt x) (ny, VInt y) = do
    n <- nextNumber  // generate an unused number
    println "%n = add_int(%nx, %ny)"   // this line is not real Haskell :-)
    (n, VInt (x+y))

(Of course, there are lots of other ways you could do this in many different languages. All you really need is to generate a globally unique label for every intermediate calculation during execution.)

That is the big change — it is quite invasive but the change is easy and repetitive. In addition to this, we need three other changes:

  1. At all control flow, we need to emit branch trace. That is: if-statements, loops, case statements, if-expressions, &&, ||. To translate an assertion, add a dummy global variable “ASSERT_FAILED” and generate trace as though “assert(c)” really read as “ASSERT_FAILED = ASSERT_FAILED || !c;”
  2. The first time a global variable is used, we need to emit an input trace.
  3. At the end of execution, we need to emit an output trace for all the return values and all the global variables that have been assigned to.

Convert a trace to SMT

All the hard work has been done in generating trace so generating SMT is quite easy.

  1. Convert all input trace to variable declarations
  2. Convert all calculation trace to variable definitions using appropriate SMT functions.
  3. Convert all output trace to variable definitions
  4. Ignore all branch trace — we will use that when invoking the SMT solver

The only tricky thing is that SMT-Lib2 does not have good operations for converting between integers and bitvectors so I will just use very long bitvectors to represent integers. Some SMT solvers provide operations that detect overflow so I recommend using those if available - and adjusting the size so that it is just big enough not to trigger an overflow.

So, using 200-bit bitvectors to represent ASL’s “integer” type, we can generate SMT constraints like this:

(declare-const input.x        (_ BitVec 32))
(declare-const input.y        (_ BitVec 32))
(declare-const input.carry_in (_ BitVec 1))

(define-const v1 (_ BitVec 32) input.x)
(define-const v2 (_ BitVec 32) input.y)
(define-const v3 (_ BitVec 1) input.carry_in)

; unsigned_sum = UInt(x) + UInt(y) + UInt(carry_in);
(define-const v4 (_ BitVec 200) ((_ zero_extend 168) v1))
(define-const v5 (_ BitVec 200) ((_ zero_extend 168) v2))
(define-const v6 (_ BitVec 200) (bvadd v4 v5))
(define-const v7 (_ BitVec 200) ((_ zero_extend 199) v3))
(define-const v8 (_ BitVec 200) (bvadd v6 v7))

; signed_sum   = SInt(x) + SInt(y) + UInt(carry_in);
(define-const v9  (_ BitVec 200) ((_ sign_extend 168) v1))
(define-const v10 (_ BitVec 200) ((_ sign_extend 168) v2))
(define-const v11 (_ BitVec 200) (bvadd v9 v10))
(define-const v12 (_ BitVec 200) ((_ zero_extend 199) v3))
(define-const v13 (_ BitVec 200) (bvadd v11 v12))

; result       = unsigned_sum[0 +: N];  // same value as signed_sum[0 +: N]
(define-const v14 (_ BitVec 32) ((_ extract 31 0) v8))

; carry_out    = if UInt(result) == unsigned_sum then '0' else '1';
(define-const v15 (_ BitVec 200) ((_ zero_extend 168) v14))
(define-const v16 Bool (= v15 v8))
(define-const v17 (_ BitVec 1) #b1)

; overflow     = if SInt(result) == signed_sum then '0' else '1';
(define-const v18 (_ BitVec 200) ((_ sign_extend 168) v14))
(define-const v19 Bool (= v18 v13))
(define-const v20 (_ BitVec 1) #b0)

; return (result, carry_out, overflow);
(define-const output.return.1 (_ BitVec 32) v14)
(define-const output.return.2 (_ BitVec 1)  v17)
(define-const output.return.3 (_ BitVec 1)  v20)

Testing the flow

We can test that the SMT we generated behaves the same as the original program for the input value used to generate the trace. To do this, we add the following lines to the end of the SMT file we generated.

(assert (= input.x (bvneg #x00000005)))
(assert (= input.y #x00000004))
(assert (= input.carry_in #b1))
(check-sat)
(get-value (output.return.1))
(get-value (output.return.2))
(get-value (output.return.3))

These lines do the following:

  1. Constrain the input variable “x” to be -5.
  2. Ask the SMT solver to check whether the constraints are consistent.
  3. Displays the value of the return value.

The output generated is as follows (using the z3 solver)

$ z3 t1.smt2
sat
((output.return.1 #x00000000))
((output.return.2 #b1))
((output.return.3 #b0))

The output “sat” indicates that the constraints are consistent and that the return value is (0, ‘1’, ‘0’) — which matches the execution that produced the execution trace.

So things are looking good but we are only checking the final result of the function. If we want to check that the translation is correct, it would be much better to check every intermediate value in the trace. To do this, all we need to do is tweak the interpreter again so that as well as printing symbolic information such as

%6 = add_int(%4, %5)

the interpreter also prints the concrete value of that calculation — in this case, that was ‘4294967295’. Armed with that information, we can add additional assertions to our test to check each of the intermediate values. For example, we can check that “%6 == 4294967295” by adding this.

(assert (= v6 (_ bv4294967295 200)))

After doing this for all intermediate results, we can check this with the Z3 solver:

$ z3 t2.smt2
sat
((output.return.1 #x00000000))
((output.return.2 #b1))
((output.return.3 #b0))

Obviously, this is not a very exciting result since it is the same as the last time we ran the solver. But, these traces can be thousands of lines long and putting a bit of effort into testing the generation path will save you a lot of debug time later.

Summary

What I have sketched in the above is enough that you can take an execution trace and turn it into a symbolic trace that you can probe using an SMT solver. So far, all we have done with it is to check that the symbolic trace matches the original; future posts will explore other (more useful) uses for the symbolic trace.

I also sketched how you can check that your translation from traces to SMT is correct. I don’t really expect you to pay any attention to that now. But, maybe in a week’s time when you have a 3000-line trace and you are trying to figure out why v2473 is 253 instead of 3, you will remember this bit of the post.

Historical note

I first got interested in generating SMT from traces when I saw this paper presented at ASPLOS 2012 in London. I was so excited about the idea that I decided to implement it myself for the Arm processor specification. By the end of the weekend, I had a crude but effective version of the paper that could generate test programs that I could run on simulators, the architecture specifications, etc.

If you want to know more about this area, the Related Work section in that paper is pretty good. The references about KLEE, SAGE and Concolic execution are pretty good.

Written on February 2, 2019.
The opinions expressed are my own views and not my employer's.