From 1a175c67402430c8e6a970d42660dcf3b23110aa Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 10 Apr 2015 09:49:04 +0100 Subject: 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. --- test/Solver/AShr_to_smtlib.kquery | 16 ++++++++++++++++ test/Solver/AShr_to_smtlib.kquery.good.smt2 | 7 +++++++ 2 files changed, 23 insertions(+) create mode 100644 test/Solver/AShr_to_smtlib.kquery create mode 100644 test/Solver/AShr_to_smtlib.kquery.good.smt2 (limited to 'test') 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) -- cgit 1.4.1