Generating SMT Libv2 output

Taintgrind can be made to generate SMT-Libv2 formulae to solve for alternative input values whenever tainted conditional branches and load/store addresses are encountered via the --smt2=yes option.

Using the sign32.c example, run with

    [valgrind-x.xx.x] ./inst/bin/valgrind --tool=taintgrind --smt2=yes ~/sign32

Save to sign32.smt2 with

    [valgrind-x.xx.x] ./inst/bin/valgrind --tool=taintgrind --smt2=yes ~/sign32 2>&1 >/dev/null | grep -v "==" | tee sign32.smt2

Use z3 (https://github.com/Z3Prover/z3) to solve for alternative input values with

> z3 sign32.smt2 | grep -A 1 myint

Which should give

  (define-fun myint0 () (_ BitVec 8)
    #x00)
--
  (define-fun myint1 () (_ BitVec 8)
    #x00)
--
  (define-fun myint3 () (_ BitVec 8)
    #x00)
--
  (define-fun myint2 () (_ BitVec 8)
    #x00)
--
  (define-fun myint1 () (_ BitVec 8)
    #x00)
--
  (define-fun myint0 () (_ BitVec 8)
    #x00)
--
  (define-fun myint3 () (_ BitVec 8)
    #x80)
--
  (define-fun myint2 () (_ BitVec 8)
    #x00)

The two alternative values for myint are 0x00000000 and 0x80000000 (or -2147483648 as a signed 32-bit int). If TNT_TAINT() was used, the default prefix is 'byte'.