From a480b43bf38d4b030d3ceda92549fb721800c026 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 7 Nov 2013 15:02:08 +0000 Subject: Added C test case that checks that concrete and symbolic overshift behaviour for logical right shift are identical. --- test/Feature/logical-right-overshift-sym-conc.c | 65 +++++++++++++++++++++++++ 1 file changed, 65 insertions(+) create mode 100644 test/Feature/logical-right-overshift-sym-conc.c (limited to 'test') diff --git a/test/Feature/logical-right-overshift-sym-conc.c b/test/Feature/logical-right-overshift-sym-conc.c new file mode 100644 index 00000000..47e0959c --- /dev/null +++ b/test/Feature/logical-right-overshift-sym-conc.c @@ -0,0 +1,65 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: %klee -use-cex-cache=1 -check-overshift=0 %t.bc +// RUN: not grep "ASSERTION FAIL" klee-last/messages.txt +// RUN: grep "KLEE: done: explored paths = 1" klee-last/info +#include +#include + +typedef enum +{ + TO_ZERO, + MASKED, + UNKNOWN +} overshift_t; + +// We're using unsigned ints so should be doing +// logical right shift. +int overshift(volatile unsigned int y, const char * type) +{ + overshift_t ret; + volatile unsigned int x=15; + unsigned int limit = sizeof(x)*8; + + volatile unsigned int result; + result = x >> y; // Potential overshift + + if (result ==0) + { + printf("%s : Overshift to zero\n", type); + ret = TO_ZERO; + } + else if (result == ( x >> (y % limit)) ) + { + printf("%s : Bitmasked overshift\n", type); + ret = MASKED; + } + else + { + printf("%s : Unrecognised behaviour.\n", type); + ret = UNKNOWN; + } + + return ret; +} + +int main(int argc, char** argv) +{ + // Concrete overshift + volatile unsigned int y = sizeof(unsigned int)*8; + overshift_t conc = overshift(y, "Concrete"); + assert( conc == TO_ZERO); + + // Symbolic overshift + volatile unsigned int y2; + klee_make_symbolic(&y2,sizeof(y),"y2"); + // Add constraints so only one value possible + klee_assume(y2 > (y-1)); + klee_assume(y2 < (y+1)); + overshift_t sym = overshift(y2, "Symbolic"); + assert( sym == TO_ZERO); + + // Concrete and symbolic behaviour should be the same + assert( conc == sym); + + return 0; +} -- cgit 1.4.1