diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-04-10 09:49:04 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-04-15 21:08:38 +0100 |
| commit | 1a175c67402430c8e6a970d42660dcf3b23110aa (patch) | |
| tree | 9001b1ac943bf1e45a24a0620e87bcafc1c08f24 /test/Solver | |
| parent | 44cceb1eb7ab58b153a20d12c84d6b0b352e05da (diff) | |
| download | klee-1a175c67402430c8e6a970d42660dcf3b23110aa.tar.gz | |
Fix the handling of AShrExpr in ExprSMTLIBPrinter so that an overshift
always goes to zero (matches LLVM's APInt::ashr(...)). This is meant to partially address issue #218. There are a few problems with this commit * It is possible for AShrExpr to not be abbreviated because the scan methods will not see that we print the 0th child of the AShrExpr twice * The added test case should really be run through an SMT solver ( i.e. STP) but that requires infrastructure changes.
Diffstat (limited to 'test/Solver')
| -rw-r--r-- | test/Solver/AShr_to_smtlib.kquery | 16 | ||||
| -rw-r--r-- | test/Solver/AShr_to_smtlib.kquery.good.smt2 | 7 |
2 files changed, 23 insertions, 0 deletions
diff --git a/test/Solver/AShr_to_smtlib.kquery b/test/Solver/AShr_to_smtlib.kquery new file mode 100644 index 00000000..774c46d9 --- /dev/null +++ b/test/Solver/AShr_to_smtlib.kquery @@ -0,0 +1,16 @@ +# RUN: %kleaver -print-smtlib -smtlib-abbreviation-mode=none %s > %t +# RUN: diff -u %t %s.good.smt2 + +# This test tries to check that the SMT-LIBv2 we generate when a AShrExpr is +# used is correct. +# +# FIXME: We should really pass the generated query to an SMT solver that supports +# SMT-LIBv2 and check it gives the correct answer ``unsat``. An older version of +# KLEE where AShrExpr wasn't handled correctly would give ``sat`` for this query. +# +# We could fix this if we required STP to be in the user's PATH and made available +# as a substitution in llvm-lit + +array value[1] : w32 -> w8 = symbolic +array shift[1] : w32 -> w8 = symbolic +(query [(Ule 8 (Read w8 0 shift))] (Eq 0 (AShr w8 (Read w8 0 value) (Read w8 0 shift))) ) diff --git a/test/Solver/AShr_to_smtlib.kquery.good.smt2 b/test/Solver/AShr_to_smtlib.kquery.good.smt2 new file mode 100644 index 00000000..e9478da6 --- /dev/null +++ b/test/Solver/AShr_to_smtlib.kquery.good.smt2 @@ -0,0 +1,7 @@ +;SMTLIBv2 Query 0 +(set-logic QF_AUFBV ) +(declare-fun shift () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun value () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(assert (and (= false (= (_ bv0 8) (ite (bvuge (select shift (_ bv0 32) ) (_ bv8 8) ) (_ bv0 8) (bvashr (select value (_ bv0 32) ) (select shift (_ bv0 32) ) ) ) ) ) (bvule (_ bv8 8) (select shift (_ bv0 32) ) ) ) ) +(check-sat) +(exit) |