[STPBuilder] Generate SRrem expressions correctly

The '%' operater in C is not Gauss Modulo
but remainder operations.

Using a negative number as right operand
can result in a negative number.

Fix appropriate SRem building

Note: MetaSMTlib implementation doesn't have that bug.

2 files changed, 34 insertions, 1 deletions

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index c2f23c0a..ddeb3c37 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -751,7 +751,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
 #endif
 
     // XXX implement my fast path and test for proper handling of sign
-    return vc_sbvModExpr(vc, *width_out, left, right);
+    return vc_sbvRemExpr(vc, *width_out, left, right);
   }
 
     // Bitwise
diff --git a/test/Feature/srem.c b/test/Feature/srem.c
new file mode 100644
index 00000000..f4fa8aa5
--- /dev/null
+++ b/test/Feature/srem.c
@@ -0,0 +1,33 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 %t.bc
+// RUN: grep "KLEE: done: explored paths = 5" %t.klee-out/info
+// RUN: grep "KLEE: done: generated tests = 4" %t.klee-out/info
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv)
+{
+    int y;
+
+    klee_make_symbolic(&y, sizeof(y), "y");
+
+    // Test cases divisor is positive or negative
+    if (y >= 0) {
+      if (y < 2) {
+        // Two test cases generated taking this path, one for y == 0 and y ==1
+        assert(1 % y == 0);
+      } else {
+        assert(1 % y == 1);
+      }
+    } else {
+      if (y > -2) {
+        assert(1 % y == 0);
+      } else {
+        assert(1 % y == 1);
+      }
+    }
+
+    assert(0 % y == 0);
+    assert(-1 % y == -1);
+}