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.

1 files changed, 16 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))) )