diff options
Diffstat (limited to 'test/regression')
18 files changed, 350 insertions, 0 deletions
diff --git a/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c b/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c new file mode 100644 index 00000000..ad585ddd --- /dev/null +++ b/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c @@ -0,0 +1,20 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc + +#include <assert.h> + +int main(void) { + char c[2]; + + klee_make_symbolic(&c, sizeof(c)); + + if (c[0] > 10) { + int x; + + c[1] = 1; // copy object state + + assert(c[0] > 10); + } + + return 0; +} diff --git a/test/regression/2007-07-30-unflushed-byte.c b/test/regression/2007-07-30-unflushed-byte.c new file mode 100644 index 00000000..ba8a08a7 --- /dev/null +++ b/test/regression/2007-07-30-unflushed-byte.c @@ -0,0 +1,18 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc + +#include <assert.h> + +int main() { + char i, x[3]; + + klee_make_symbolic(&i, sizeof i); + + x[0] = i; + + // DEMAND FAILED:Memory.cpp:read8:199: <isByteFlushed(offset)> is false: "unflushed byte without cache value" + char y = x[1]; + + return 0; +} + diff --git a/test/regression/2007-08-01-bool-zext-in-call.ll b/test/regression/2007-08-01-bool-zext-in-call.ll new file mode 100644 index 00000000..3f3e26ab --- /dev/null +++ b/test/regression/2007-08-01-bool-zext-in-call.ll @@ -0,0 +1,22 @@ +; RUN: llvm-as -f %s -o - | %klee 2> %t1.log +; RUN: not test -f klee-last/test0001.abort.err + +declare void @klee_abort() + +define i32 @foo(i8 signext %val) { + %tmp = zext i8 %val to i32 + ret i32 %tmp +} + +define i32 @main() { + %res = call i32 bitcast (i32 (i8 signext)* @foo to i32 (i1)*)( i1 1 ) + %check = icmp ne i32 %res, 255 + br i1 %check, label %error, label %exit + +error: + call void @klee_abort() + unreachable + +exit: + ret i32 0 +} diff --git a/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c b/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c new file mode 100644 index 00000000..15f4e90e --- /dev/null +++ b/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c @@ -0,0 +1,25 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc + +#include <assert.h> +#include <stdio.h> + +int main() { + unsigned char x; + + klee_make_symbolic(&x, sizeof x); + if (x >= 2) klee_silent_exit(0); + + char delete[2] = {0,1}; + + char tmp = delete[ x ]; + char tmp2 = delete[0]; + delete[ x ] = tmp2; + + if (x==1) { + assert(delete[1] == 0); + return 0; + } + + return 0; +} diff --git a/test/regression/2007-08-06-64bit-shift.c b/test/regression/2007-08-06-64bit-shift.c new file mode 100644 index 00000000..958e56c0 --- /dev/null +++ b/test/regression/2007-08-06-64bit-shift.c @@ -0,0 +1,20 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc + +#include <assert.h> + +int main() { + int d; + + klee_make_symbolic( &d, sizeof(d) ); + + int l = d - 1; + unsigned long long m = ((unsigned long long) l << 32) / d; + if (d==2) { + assert(m == 2147483648u); + } + + klee_silent_exit(0); + + return 0; +} diff --git a/test/regression/2007-08-06-access-after-free.c b/test/regression/2007-08-06-access-after-free.c new file mode 100644 index 00000000..a1812062 --- /dev/null +++ b/test/regression/2007-08-06-access-after-free.c @@ -0,0 +1,29 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc + +#include <assert.h> + +int main() { + int a; + unsigned char *p = malloc(4); + + klee_make_symbolic(&a, sizeof a); + klee_make_symbolic(p, sizeof p); + + p[0] |= 16; + + if (a) { + free(p); + + // this should give an error instead of + // pulling the state from the parent, where + // it is not free + assert(p[0] > 10); + + return 0; + } + + assert(p[0] > 10); + + return 0; +} diff --git a/test/regression/2007-08-08-free-zero.c b/test/regression/2007-08-08-free-zero.c new file mode 100644 index 00000000..964889a1 --- /dev/null +++ b/test/regression/2007-08-08-free-zero.c @@ -0,0 +1,8 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc +// RUN: ls klee-last | not grep *.err + +int main() { + free(0); + return 0; +} diff --git a/test/regression/2007-08-16-invalid-constant-value.c b/test/regression/2007-08-16-invalid-constant-value.c new file mode 100644 index 00000000..ecb3283f --- /dev/null +++ b/test/regression/2007-08-16-invalid-constant-value.c @@ -0,0 +1,31 @@ +// RUN: rm -f %t4.out %t4.err %t4.log +// RUN: %llvmgcc %s -emit-llvm -O2 -c -o %t1.bc +// RUN: llvm-as -f ../../Feature/_utils._ll -o %t2.bc +// RUN: llvm-ld -disable-opt %t1.bc %t2.bc -o %t3 +// RUN: %klee %t3.bc + +#include <assert.h> + +#include "../Feature/utils.h" + +int main() { + unsigned char a; + + klee_make_symbolic(&a, sizeof a); + + // demand was firing here because an invalid constant + // value was being created when implied value did not + // subtract using the proper type (so overflowed into + // invalid bits) + if (util_make_concat2(a+0xCD,0xCD) == 0xABCD) { + assert(!klee_is_symbolic(a)); + printf("add constant case: %d\n", a); + } + + if (util_make_concat2(0x0B-a,0xCD) == 0xABCD) { + assert(!klee_is_symbolic(a)); + printf("sub constant case: %d\n", a); + } + + return 0; +} diff --git a/test/regression/2007-08-16-valid-write-to-freed-object.c b/test/regression/2007-08-16-valid-write-to-freed-object.c new file mode 100644 index 00000000..472b7de8 --- /dev/null +++ b/test/regression/2007-08-16-valid-write-to-freed-object.c @@ -0,0 +1,24 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc + +unsigned sym() { + unsigned x; + klee_make_symbolic(&x, sizeof x); + return x; +} + +int main() { + unsigned x, y; + + // sym returns a symbolic object, but because it is + // alloca'd it is freed on sym()s return. thats fine, + // but the problem is that IVC is going to try to write + // into the object right here. + // + // to support this we need to have a facility for making + // state local copies of a freed object. + if (sym() == 0) + printf("ok\n"); + + return 0; +} diff --git a/test/regression/2007-10-11-free-of-alloca.c b/test/regression/2007-10-11-free-of-alloca.c new file mode 100644 index 00000000..71a16f6b --- /dev/null +++ b/test/regression/2007-10-11-free-of-alloca.c @@ -0,0 +1,9 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc +// RUN: test -f klee-last/test000001.free.err + +int main() { + int buf[4]; + free(buf); // this should give runtime error, not crash + return 0; +} diff --git a/test/regression/2007-10-11-illegal-access-after-free-and-branch.c b/test/regression/2007-10-11-illegal-access-after-free-and-branch.c new file mode 100644 index 00000000..fbbb99c3 --- /dev/null +++ b/test/regression/2007-10-11-illegal-access-after-free-and-branch.c @@ -0,0 +1,19 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee --optimize %t1.bc +// RUN: test -f klee-last/test000001.ptr.err + +#include <stdlib.h> +#include <stdio.h> +#include <assert.h> + +int main(int argc, char **argv) { + unsigned char *buf = malloc(3); + klee_make_symbolic(buf, 3); + if (buf[0]>4) klee_silent_exit(0); + unsigned char x = buf[1]; + free(buf); + if (x) + return buf[2]; + klee_silent_exit(0); + return 0; +} diff --git a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c new file mode 100644 index 00000000..144281fa --- /dev/null +++ b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc +// RUN: test -f klee-last/test000001.bout + +int main() { + unsigned x, y[4]; + + klee_make_symbolic(&x,sizeof x); + if (x>=4) klee_silent_exit(0); + + y[x] = 0; + + if (x) { // force branch so y is copied + klee_make_symbolic(&y, sizeof y); + if (y[x]==0) klee_silent_exit(0); + return 0; // should be reachable + } else { + // force read here in case we try to optimize copies smartly later + if (y[x]==0) klee_silent_exit(0); + return 0; // not reachable + } +} diff --git a/test/regression/2008-02-11-phi-nodes-after-invoke.ll b/test/regression/2008-02-11-phi-nodes-after-invoke.ll new file mode 100644 index 00000000..f6077f25 --- /dev/null +++ b/test/regression/2008-02-11-phi-nodes-after-invoke.ll @@ -0,0 +1,47 @@ +; RUN: llvm-as -f %s -o - | %klee --no-output --exit-on-error + +declare void @klee_abort() + +define i32 @foo(i32 %val, i32 %fail) { + %code = icmp ne i32 0, %fail + br i1 %code, label %failing, label %return +failing: + unwind +return: + ret i32 %val +} + +define void @test(i32 %should_fail) { +entry: + %res0 = invoke i32 (i32, i32)* @foo(i32 0, i32 %should_fail) + to label %check_phi unwind label %error + +error: + %res1 = zext i8 1 to i32 + br label %check_phi + +check_phi: + %val = phi i32 [%never_used, %never_used_label], [%res0, %entry], [%res1, %error] + %ok = icmp eq i32 %val, %should_fail + br i1 %ok, label %exit, label %on_error + call void @klee_abort() + unreachable + +on_error: + call void @klee_abort() + unreachable + +exit: + ret void + + ;; this is so we hopefully fail if incomingBBIndex isn't set properly +never_used_label: + %never_used = zext i8 undef to i32 + br label %check_phi +} + +define i32 @main() { + call void (i32)* @test(i32 0) + call void (i32)* @test(i32 1) + ret i32 0 +} diff --git a/test/regression/2008-03-04-free-of-global.c b/test/regression/2008-03-04-free-of-global.c new file mode 100644 index 00000000..7821398d --- /dev/null +++ b/test/regression/2008-03-04-free-of-global.c @@ -0,0 +1,10 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc +// RUN: test -f klee-last/test000001.free.err + +int buf[4]; + +int main() { + free(buf); // this should give runtime error, not crash + return 0; +} diff --git a/test/regression/2008-03-11-free-of-malloc-zero.c b/test/regression/2008-03-11-free-of-malloc-zero.c new file mode 100644 index 00000000..d096818b --- /dev/null +++ b/test/regression/2008-03-11-free-of-malloc-zero.c @@ -0,0 +1,16 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc + +#include <stdlib.h> + +int main() { + // concrete case + void *p = malloc(0); + free(p); + + p = malloc(0); + void *arr[4] = { p, 0, 0, 0 }; + + // symbolic case + free(arr[klee_range(0, 4, "range")]); +} diff --git a/test/regression/2008-04-10-bad-alloca-free.c b/test/regression/2008-04-10-bad-alloca-free.c new file mode 100644 index 00000000..46e2b0cf --- /dev/null +++ b/test/regression/2008-04-10-bad-alloca-free.c @@ -0,0 +1,12 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc + +void f(int *addr) { + klee_make_symbolic_name(addr, sizeof *addr, "moo"); +} + +int main() { + int x; + f(&x); + return x; +} diff --git a/test/regression/2008-05-23-gep-with-global-const.c b/test/regression/2008-05-23-gep-with-global-const.c new file mode 100644 index 00000000..5e03ec1d --- /dev/null +++ b/test/regression/2008-05-23-gep-with-global-const.c @@ -0,0 +1,15 @@ +// RUN: %llvmgcc -O0 -c -o %t.bc %s +// RUN: %klee --exit-on-error %t.bc + +#include <assert.h> + +int a; + +int main() { + void *p1 = &((char*) 0)[(long) &a]; + void *p2 = &a; + + assert(p1 == p2); + + return 0; +} diff --git a/test/regression/dg.exp b/test/regression/dg.exp new file mode 100644 index 00000000..879685ca --- /dev/null +++ b/test/regression/dg.exp @@ -0,0 +1,3 @@ +load_lib llvm.exp + +RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{ll,llx,c,cpp,tr}]] |