From a801ac5dfef0533c3fc00a7dbfb630eccb0b8f30 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Sun, 9 Aug 2015 12:14:39 +0200 Subject: [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. --- lib/Solver/STPBuilder.cpp | 2 +- test/Feature/srem.c | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 34 insertions(+), 1 deletion(-) create mode 100644 test/Feature/srem.c 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 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 +#include + +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); +} -- cgit 1.4.1