SMTransform is framework with the goal to find unsoundness bugs in SMT solvers through fuzzing. From a satisfiable seed formula, SMTransform incrementally generates new formulas which are satisfiable by construction.
- Cargo
- Python 3.9
The project is used and developed on Linux, but it should work on any platform supported by rust and python.
Compiling the project is as easy as running
cargo build --release
The smtransform
executable will then be placed in target/release/smtransform
.
USAGE:
smtransform [OPTIONS] <FILE>
ARGS:
<FILE> File containing seed formula in the SMT-LIB2 format
OPTIONS:
-h, --help Print help information
--json Print generated formulas wrapped in JSON object
--print-original Also print the seed formula
--rounds <ROUNDS> How many formulas to generate [default: 1]
--seed <SEED> Seed for the PRNG [default: 0]
-V, --version Print version information
Sample usage:
$ cat in.smt2
(set-info :status sat)
(set-logic QF_NIA)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= x 3))
(assert (= y 9))
(check-sat)
(exit)
$ ./target/release/smtransform in.smt2
(set-logic QF_NIA)
(set-info :status sat)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun v0 () Int)
(assert (= (- v0 y) 3))
(assert (= (- v0 x) 9))
(check-sat)
(exit)
A large collection of seed formulas is available in the SMT-LIB benchmark repository.
Pipe the JSON output from the smtransform
executable into the runner script:
./target/release/smtransform --json in.smt2 | ./scripts/runner.py -- z3 /dev/stdin
This will run each generated formula through the given SMT solver (the solver command should accept a formula on stdin) and report each failure.
Runs the generator for multiple seed formulas, passes each formula to
runner.py
, and collects failures in the given output directory.
$ ./scripts/wrapper.py \
--seeds seeds \
--out out \
--gen target/release/smtransform \
--iterations 20 \
--rounds 10 \
-- z3 /dev/stdin
Using seed seeds/20170427-VeryMax_ITS_From_T2__ex36.t2_fixed__p23162_safety_0.smt2 20/20: T..........
Using seed seeds/20170427-VeryMax_ITS_From_T2__ex36.t2_fixed__p23504_safety_0.smt2 20/20: TTTTT......
Using seed seeds/20170427-VeryMax_ITS_From_T2__s1.t2_fixed__p15649_safety_0.smt2 20/20: ...........
Using seed seeds/20170427-VeryMax_SAT14_279.smt2 20/20: T..........
Using seed seeds/AProVE_aproveSMT1179149253451050796.smt2 20/20: ..T......T.
Using seed seeds/AProVE_aproveSMT2322179511678559502.smt2 20/20: ....TTT.TTT
Using seed seeds/AProVE_aproveSMT2821114236865559656.smt2 20/20: T......TT..
Using seed seeds/AProVE_aproveSMT4248959283647504950.smt2 20/20: ..........T
Using seed seeds/AProVE_aproveSMT4556648541890562734.smt2 20/20: .T.........
Using seed seeds/AProVE_aproveSMT5479381539249843197.smt2 20/20: ......TTTTT
Success: 1611
Failure: 3
Timeout: 586
Signal: 0
Unknown: 0
Unsound: 0
Runs per iteration (approx): 11
Runs per seed (approx): 220
Seeds: 10
Total runs: 2200
- There is no type checker, so we don't really know the type of a term unless it is a variable with known type.
- The
ConstantReplacement
transformation currently assumesNUMERAL
is of sortInt
, which would be unsound if the numeral was actually used as aReal
. - The
AssertExpandBinary
transformations assumes that function names from the standard SMT-LIB theories are not overloaded (e.g.and
,>=
, etc.) because it needs to assume the function signature.
- The