diff options
Diffstat (limited to 'test/Feature')
52 files changed, 1498 insertions, 0 deletions
diff --git a/test/Feature/Alias.c b/test/Feature/Alias.c new file mode 100644 index 00000000..9300e2c7 --- /dev/null +++ b/test/Feature/Alias.c @@ -0,0 +1,25 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc + +// Darwin does not have strong aliases. +// XFAIL: darwin + +#include <assert.h> + +// alias for global +int b = 52; +extern int a __attribute__((alias("b"))); + +// alias for function +int __foo() { return 52; } +extern int foo() __attribute__((alias("__foo"))); + +int *c = &a; + +int main() { + assert(a == 52); + assert(foo() == 52); + assert(*c == 52); + + return 0; +} diff --git a/test/Feature/AliasFunction.c b/test/Feature/AliasFunction.c new file mode 100644 index 00000000..e7acfc19 --- /dev/null +++ b/test/Feature/AliasFunction.c @@ -0,0 +1,33 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc > %t1.log +// RUN: grep -c foo %t1.log | grep 5 +// RUN: grep -c bar %t1.log | grep 3 + +#include <stdio.h> +#include <stdlib.h> + +void foo() { printf(" foo()\n"); } +void bar() { printf(" bar()\n"); } + +int main() { + int x; + klee_make_symbolic_name(&x, sizeof(x), "x"); + + // no aliases + foo(); + + if (x > 10) + { + // foo -> bar + klee_alias_function("foo", "bar"); + + if (x > 20) + foo(); + } + + foo(); + + // undo + klee_alias_function("foo", "foo"); + foo(); +} diff --git a/test/Feature/AliasFunctionExit.c b/test/Feature/AliasFunctionExit.c new file mode 100644 index 00000000..fcaf7e6c --- /dev/null +++ b/test/Feature/AliasFunctionExit.c @@ -0,0 +1,30 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc > %t1.log +// RUN: grep -c START %t1.log | grep 1 +// RUN: grep -c END %t1.log | grep 2 + +#include <stdio.h> +#include <stdlib.h> +#include <unistd.h> + +void start(int x) { + printf("START\n"); + if (x == 53) + exit(1); +} + +void end(int status) { + klee_alias_function("exit", "exit"); + printf("END: status = %d\n", status); + exit(status); +} + + +int main() { + int x; + klee_make_symbolic_name(&x, sizeof(x), "x"); + + klee_alias_function("exit", "end"); + start(x); + end(0); +} diff --git a/test/Feature/AsmAddresses.c b/test/Feature/AsmAddresses.c new file mode 100644 index 00000000..a58fc059 --- /dev/null +++ b/test/Feature/AsmAddresses.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc -g -c -o %t.bc %s +// RUN: %klee --exit-on-error --use-asm-addresses %t.bc +// RUN: %llvmgcc -DOVERLAP -g -c -o %t.bc %s +// RUN: not %klee --exit-on-error --use-asm-addresses %t.bc + +#include <assert.h> + + +volatile unsigned char x0 __asm ("0x0021"); +volatile unsigned char whee __asm ("0x0WHEE"); + +#ifdef OVERLAP +volatile unsigned int y0 __asm ("0x0030"); +volatile unsigned int y1 __asm ("0x0032"); +#endif + +int main() { + assert(&x0 == (void*) 0x0021); + assert(&whee != (void*) 0x0); + + return 0; +} diff --git a/test/Feature/ByteSwap.c b/test/Feature/ByteSwap.c new file mode 100644 index 00000000..f85ac3b1 --- /dev/null +++ b/test/Feature/ByteSwap.c @@ -0,0 +1,16 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee --libc=klee --exit-on-error %t1.bc + +#include <arpa/inet.h> +#include <assert.h> + +int main() { + + uint32_t n = 0; + klee_make_symbolic(&n, sizeof(n)); + + uint32_t h = ntohl(n); + assert(htonl(h) == n); + + return 0; +} diff --git a/test/Feature/CallToUndefinedExternal.cpp b/test/Feature/CallToUndefinedExternal.cpp new file mode 100644 index 00000000..2f11f29d --- /dev/null +++ b/test/Feature/CallToUndefinedExternal.cpp @@ -0,0 +1,11 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee %t1.bc +// RUN: test -f klee-last/test000001.external.err + +extern "C" void poof(void); + +int main() { + poof(); + + return 0; +} diff --git a/test/Feature/CheckForImpliedValue.c.failing b/test/Feature/CheckForImpliedValue.c.failing new file mode 100644 index 00000000..7a088354 --- /dev/null +++ b/test/Feature/CheckForImpliedValue.c.failing @@ -0,0 +1,23 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: rm -f %t1.log +// RUN: %klee --log-file %t1.log --debug-check-for-implied-values %t1.bc +// RUN: grep "= 0 (ok)" %t1.log +// RUN: grep "= 2 (missed)" %t1.log + +#define swap(x) (((x)>>16) | (((x)&0xFFFF)<<16)) +int main() { + unsigned x, y; + + klee_make_symbolic(&x, sizeof x); + klee_make_symbolic(&y, sizeof y); + + if (!x) { // should give x = 0 hit by ivc + printf("ok\n"); + } else { + if (swap(y) == 0x00020000) { // should give y = 2 missed by ivc + printf("ok\n"); + } + } + + return 0; +} diff --git a/test/Feature/CheckMemoryAccess.c b/test/Feature/CheckMemoryAccess.c new file mode 100644 index 00000000..dd6e8745 --- /dev/null +++ b/test/Feature/CheckMemoryAccess.c @@ -0,0 +1,26 @@ +// RUN: %llvmgcc -g -c %s -o %t.bc +// RUN: %klee %t.bc > %t.log +// RUN: grep -q "good" %t.log +// RUN: not grep -q "bad" %t.log + +#include <assert.h> +#include <stdlib.h> +#include <stdio.h> + +int main() { + char buf[4]; + + klee_check_memory_access(&buf, 1); + printf("good\n"); + if (klee_range(0, 2, "range1")) { + klee_check_memory_access(0, 1); + printf("null pointer deref: bad\n"); + } + + if (klee_range(0, 2, "range2")) { + klee_check_memory_access(buf, 5); + printf("oversize access: bad\n"); + } + + return 0; +} diff --git a/test/Feature/CopyOnWrite.c b/test/Feature/CopyOnWrite.c new file mode 100644 index 00000000..ee3ea15e --- /dev/null +++ b/test/Feature/CopyOnWrite.c @@ -0,0 +1,26 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee --use-random-search --exit-on-error %t1.bc + +#include <assert.h> + +#define N 5 + +unsigned branches = 0; + +void explode(int *ap, int i, int *result) { + if (i<N) { + (*result)++; + if (ap[i]) // just cause a fork + branches++; + return explode(ap, i+1, result); + } +} + +int main() { + int result = 0; + int a[N]; + klee_make_symbolic(a, sizeof a); + explode(a,0,&result); + assert(result==N); + return 0; +} diff --git a/test/Feature/DanglingConcreteReadExpr.c b/test/Feature/DanglingConcreteReadExpr.c new file mode 100644 index 00000000..1bf44c3f --- /dev/null +++ b/test/Feature/DanglingConcreteReadExpr.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc +// RUN: grep "total queries = 2" klee-last/info + +#include <assert.h> + +int main() { + unsigned char x, y; + + klee_make_symbolic(&x, sizeof x); + + y = x; + + // should be exactly two queries (prove x is/is not 10) + // eventually should be 0 when we have fast solver + if (x==10) { + assert(y==10); + } + + klee_silent_exit(0); + return 0; +} diff --git a/test/Feature/DefineFixedObject.c b/test/Feature/DefineFixedObject.c new file mode 100644 index 00000000..36822434 --- /dev/null +++ b/test/Feature/DefineFixedObject.c @@ -0,0 +1,17 @@ +// RUN: %llvmgcc -c -o %t1.bc %s +// RUN: %klee --exit-on-error %t1.bc + +#include <stdio.h> + +#define ADDRESS ((int*) 0x0080) + +int main() { + klee_define_fixed_object(ADDRESS, 4); + + int *p = ADDRESS; + + *p = 10; + printf("*p: %d\n", *p); + + return 0; +} diff --git a/test/Feature/DoubleFree.c b/test/Feature/DoubleFree.c new file mode 100644 index 00000000..3727ef2b --- /dev/null +++ b/test/Feature/DoubleFree.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.ptr.err + +int main() { + int *x = malloc(4); + free(x); + free(x); + return 0; +} diff --git a/test/Feature/DumpStatesOnHalt.c b/test/Feature/DumpStatesOnHalt.c new file mode 100644 index 00000000..7e9cf46a --- /dev/null +++ b/test/Feature/DumpStatesOnHalt.c @@ -0,0 +1,8 @@ +// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee --stop-after-n-instructions=1 --dump-states-on-halt=true %t1.bc +// RUN: test -f klee-last/test000001.bout + +int main() { + int x = 10; + return x; +} diff --git a/test/Feature/Envp.c b/test/Feature/Envp.c new file mode 100644 index 00000000..f1f62a72 --- /dev/null +++ b/test/Feature/Envp.c @@ -0,0 +1,18 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc + +#include <assert.h> + +int main(int argc, char **argv, char **envp) { + unsigned i; + assert(argv[argc] == 0); + printf("argc: %d, argv: %p, envp: %p\n", argc, argv, envp); + printf("--environ--\n"); + int haspwd = 0; + for (i=0; envp[i]; i++) { + printf("%d: %s\n", i, envp[i]); + haspwd |= strncmp(envp[i], "PWD=", 4)==0; + } + assert(haspwd); + return 0; +} diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c new file mode 100644 index 00000000..2abf0070 --- /dev/null +++ b/test/Feature/ExprLogging.c @@ -0,0 +1,43 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc +// RUN: %klee --use-query-pc-log --write-pcs --write-cvcs %t1.bc 2> %t2.log +// RUN: %kleaver -print-ast klee-last/test000001.pc + +// FIXME: Ideally we would verify a roundtrip that we parsed the pc +// file and can dump it back out as the same file. + +#include <assert.h> + +int constantArr[16 ] = { + 1 << 0, 1 << 1, 1 << 2, 1 << 3, + 1 << 4, 1 << 5, 1 << 6, 1 << 7, + 1 << 8, 1 << 9, 1 << 10, 1 << 11, + 1 << 12, 1 << 13, 1 << 14, 1 << 15 +}; + + +int main() { + char buf[4]; + klee_make_symbolic(buf, sizeof buf); + + buf[1] = 'a'; + + constantArr[klee_range(0, 16, "idx.0")] = buf[0]; + + // Use this to trigger an interior update list usage. + int y = constantArr[klee_range(0, 16, "idx.1")]; + + constantArr[klee_range(0, 16, "idx.2")] = buf[3]; + + buf[klee_range(0, 4, "idx.3")] = 0; + klee_assume(buf[0] == 'h'); + + int x = *((int*) buf); + klee_assume(x > 2); + klee_assume(x == constantArr[12]); + + klee_assume(y != (1 << 5)); + + assert(0); + + return 0; +} diff --git a/test/Feature/ExternalWeakLinkage.c b/test/Feature/ExternalWeakLinkage.c new file mode 100644 index 00000000..c2008136 --- /dev/null +++ b/test/Feature/ExternalWeakLinkage.c @@ -0,0 +1,11 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc + +#include <assert.h> + +void __attribute__((weak)) IAmSoWeak(int); + +int main() { + assert(IAmSoWeak==0); + return 0; +} diff --git a/test/Feature/FunctionPointer.c b/test/Feature/FunctionPointer.c new file mode 100644 index 00000000..e1ae1e37 --- /dev/null +++ b/test/Feature/FunctionPointer.c @@ -0,0 +1,36 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee --no-output --exit-on-error %t1.bc + +#include <stdio.h> + +void foo(const char *msg) { printf("foo: %s\n", msg); } +void baz(const char *msg) { printf("baz: %s\n", msg); } + +void (*xx)(const char *) = foo; + +void bar(void (*fp)(const char *)) { fp("called via bar"); } + +int main(int argc, char **argv) { + void (*fp)(const char *) = foo; + + printf("going to call through fp\n"); + fp("called via fp"); + + printf("calling via pass through\n"); + bar(foo); + + fp = baz; + fp("called via fp"); + + xx("called via xx"); + +#if 0 + klee_make_symbolic(&fp, sizeof fp); + if(fp == baz) { + printf("fp = %p, baz = %p\n", fp, baz); + fp("calling via symbolic!"); + } +#endif + + return 0; +} diff --git a/test/Feature/GetValue.c b/test/Feature/GetValue.c new file mode 100644 index 00000000..391b68e3 --- /dev/null +++ b/test/Feature/GetValue.c @@ -0,0 +1,17 @@ +// RUN: %llvmgcc -c -o %t1.bc %s +// RUN: %klee --exit-on-error %t1.bc + +#include <stdio.h> +#include <assert.h> + +int main() { + int x = klee_int("x"); + klee_assume(x > 10); + klee_assume(x < 20); + + assert(!klee_is_symbolic(klee_get_value(x))); + assert(klee_get_value(x) > 10); + assert(klee_get_value(x) < 20); + + return 0; +} diff --git a/test/Feature/ImpliedValue.c.failing b/test/Feature/ImpliedValue.c.failing new file mode 100644 index 00000000..2f169970 --- /dev/null +++ b/test/Feature/ImpliedValue.c.failing @@ -0,0 +1,147 @@ +// RUN: rm -f %t4.out %t4.err %t4.log +// RUN: %llvmgcc %s -emit-llvm -O2 -c -o %t1.bc +// RUN: llvm-as -f ../_utils._ll -o %t2.bc +// RUN: llvm-ld -disable-opt -link-as-library %t1.bc %t2.bc -o %t3.bc +// RUN: %klee --log-file %t4.log --debug-check-for-implied-values %t3.bc > %t4.out 2> %t4.err +// RUN: ls klee-last | not grep .err +// RUN: not grep "(missed)" %t4.log + +#include <assert.h> + +#include "utils.h" + +int main() { + unsigned char which; + volatile unsigned char a,b,c,d,e,f,g,h; + + klee_make_symbolic(&which, sizeof which); + klee_make_symbolic(&a, sizeof a); + klee_make_symbolic(&b, sizeof b); + klee_make_symbolic(&c, sizeof c); + klee_make_symbolic(&d, sizeof d); + klee_make_symbolic(&e, sizeof e); + klee_make_symbolic(&f, sizeof f); + klee_make_symbolic(&g, sizeof g); + klee_make_symbolic(&h, sizeof h); + + switch (which) { +// RUN: grep "simple read(2) = value case" %t4.out + case 0: + if (a == 2) { + assert(!klee_is_symbolic(a)); + printf("simple read(%d) = value case\n", a); + } + break; + +// RUN: grep "select(0) has distinct constant result case (false)" %t4.out + case 1: + if (util_make_select(a, 12, 14) == 14) { + assert(!klee_is_symbolic(a)); + printf("select(%d) has distinct constant result case (false)\n", a); + } + break; + +// RUN: grep "select(0) has distinct constant result case (true)" %t4.out + case 2: + if (util_make_select(!a, 12, 14) == 12) { + assert(!klee_is_symbolic(a)); + printf("select(%d) has distinct constant result case (true)\n", a); + } + break; + +// RUN: grep "concat2(0xBE,0xEF) = value case" %t4.out + case 3: + if (util_make_concat2(a,b) == 0xBEEF) { + assert(!klee_is_symbolic(a)); + assert(!klee_is_symbolic(b)); + printf("concat2(0x%X,0x%X) = value case\n", + a, b); + } + break; + +// RUN: grep "concat4(0xDE,0xAD,0xBE,0xEF) = value case" %t4.out + case 4: + if (util_make_concat4(a,b,c,d) == 0xDEADBEEF) { + assert(!klee_is_symbolic(a)); + assert(!klee_is_symbolic(b)); + assert(!klee_is_symbolic(c)); + assert(!klee_is_symbolic(d)); + printf("concat4(0x%X,0x%X,0x%X,0x%X) = value case\n", + a, b, c, d); + } + break; + +// RUN: grep "concat8(0xDE,0xAD,0xBE,0xEF,0xAB,0xCD,0xAB,0xCD) = value case" %t4.out + case 5: + if (util_make_concat8(a,b,c,d,e,f,g,h) == 0xDEADBEEFABCDABCDLL) { + assert(!klee_is_symbolic(a)); + assert(!klee_is_symbolic(b)); + assert(!klee_is_symbolic(c)); + assert(!klee_is_symbolic(d)); + assert(!klee_is_symbolic(e)); + assert(!klee_is_symbolic(f)); + assert(!klee_is_symbolic(g)); + assert(!klee_is_symbolic(h)); + printf("concat8(0x%X,0x%X,0x%X,0x%X,0x%X,0x%X,0x%X,0x%X) = value case\n", + a, b, c, d, e, f, g, h); + } + break; + +// RUN: grep "and(0,0) = true case" %t4.out + case 6: + if (util_make_and_i1(!a, !b)) { + assert(!klee_is_symbolic(a)); + assert(!klee_is_symbolic(b)); + printf("and(%d,%d) = true case\n", a, b); + } + break; + +// RUN: grep "or(0,0) = false case" %t4.out + case 7: + if (!util_make_or_i1(a, b)) { + assert(!klee_is_symbolic(a)); + assert(!klee_is_symbolic(b)); + printf("or(%d,%d) = false case\n", a, b); + } + break; + + // we use concat to prevent folding, will need to fix if that gets + // partial evaluated +// RUN: grep "add constant case: 0xDE" %t4.out + case 8: + if (util_make_concat2(a+0xCD,0xCD) == 0xABCD) { + assert(!klee_is_symbolic(a)); + printf("add constant case: 0x%X\n", a); + } + break; + +// RUN: grep "sub constant case: 0x60" %t4.out + case 9: + if (util_make_concat2(0x0B-a,0xCD) == 0xABCD) { + assert(!klee_is_symbolic(a)); + printf("sub constant case: 0x%X\n", a); + } + break; + +// RUN: grep "xor constant case: 0xA0" %t4.out + case 10: + if (util_make_concat2(0x0B ^ a,0xCD) == 0xABCD) { + assert(!klee_is_symbolic(a)); + printf("xor constant case: 0x%X\n", a); + } + break; + +// RUN: grep "sext constant case: 244" %t4.out + case 11: + if (! util_make_or_i1(((short) (signed char) a) + 12,b)) { + assert(!klee_is_symbolic(a)); + printf("sext constant case: %d\n", a); + } + break; + + default: + break; + } + + return 0; +} diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c new file mode 100644 index 00000000..18e5d2b2 --- /dev/null +++ b/test/Feature/InAndOutOfBounds.c @@ -0,0 +1,19 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc +// RUN: test -f klee-last/test000001.ptr.err -o -f klee-last/test000002.ptr.err +// RUN: test ! -f klee-last/test000001.ptr.err -o ! -f klee-last/test000002.ptr.err +// RUN: test ! -f klee-last/test000003.bout + +unsigned klee_urange(unsigned start, unsigned end) { + unsigned x; + klee_make_symbolic(&x, sizeof x); + if (x-start>=end-start) klee_silent_exit(0); + return x; +} + +int main() { + int *x = malloc(4); + x[klee_urange(0,2)] = 1; + free(x); + return 0; +} diff --git a/test/Feature/IndirectCallToBuiltin.c b/test/Feature/IndirectCallToBuiltin.c new file mode 100644 index 00000000..591a5601 --- /dev/null +++ b/test/Feature/IndirectCallToBuiltin.c @@ -0,0 +1,15 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee %t1.bc + +#include <stdlib.h> +#include <stdio.h> + +int main() { + void *(*allocator)(size_t) = malloc; + int *mem = allocator(10); + + printf("mem: %p\n", mem); + printf("mem[0]: %d\n", mem[0]); + + return 0; +} diff --git a/test/Feature/IndirectCallToExternal.c b/test/Feature/IndirectCallToExternal.c new file mode 100644 index 00000000..4603213b --- /dev/null +++ b/test/Feature/IndirectCallToExternal.c @@ -0,0 +1,15 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee %t1.bc + +#include <stdlib.h> +#include <stdio.h> +#include <string.h> +#include <assert.h> + +int main() { + int (*scmp)(char*,char*) = strcmp; + + assert(scmp("hello","hi") < 0); + + return 0; +} diff --git a/test/Feature/InvalidBitfieldAccess.c.failing b/test/Feature/InvalidBitfieldAccess.c.failing new file mode 100644 index 00000000..ae8bfe5e --- /dev/null +++ b/test/Feature/InvalidBitfieldAccess.c.failing @@ -0,0 +1,28 @@ +// RUN: %llvmgcc -c -o %t1.bc %s +// RUN: %klee --exit-on-error %t1.bc + +// This is a bug in llvm-gcc4.0 but seems to be fixed in llvm-gcc4.2, +// its included here mostly as a reminder. + +#include <assert.h> +#include <stdio.h> +#include <stdlib.h> + +struct foo { + unsigned int a : 5; + unsigned int b : 10; + unsigned int c : 1; +} __attribute__((packed)); + +int main() { + struct foo *a = malloc(sizeof *a); + + a->b = 12; // problem here is that llvm-gcc emits a 4 byte access + // which is out of bounds. + + int x = a->b; + + assert(x == 12); + + return 0; +} diff --git a/test/Feature/IsSymbolic.c b/test/Feature/IsSymbolic.c new file mode 100644 index 00000000..4a86368a --- /dev/null +++ b/test/Feature/IsSymbolic.c @@ -0,0 +1,16 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc + +#include <assert.h> + +int main() { + int x, y, z = 0; + klee_make_symbolic(&x, sizeof x); + klee_make_symbolic(&y, sizeof y); + if (x) { + assert(klee_is_symbolic(y)); + } else { + assert(!klee_is_symbolic(z)); + } + return 0; +} diff --git a/test/Feature/KleeReportError.c b/test/Feature/KleeReportError.c new file mode 100644 index 00000000..dda72fd0 --- /dev/null +++ b/test/Feature/KleeReportError.c @@ -0,0 +1,23 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc +// RUN: %klee --emit-all-errors %t2.bc > %t3.log +// RUN: ls klee-last/ | grep .my.err | wc -l | grep 2 +#include <stdio.h> +#include <assert.h> + +int main(int argc, char** argv) { + int x, y, *p = 0; + + klee_make_symbolic(&x, sizeof x); + klee_make_symbolic(&y, sizeof y); + + if (x) + fprintf(stderr, "x\n"); + else fprintf(stderr, "!x\n"); + + if (y) { + fprintf(stderr, "My error\n"); + klee_report_error(__FILE__, __LINE__, "My error", "my.err"); + } + + return 0; +} diff --git a/test/Feature/LongDoubleSupport.c b/test/Feature/LongDoubleSupport.c new file mode 100644 index 00000000..b4631832 --- /dev/null +++ b/test/Feature/LongDoubleSupport.c @@ -0,0 +1,20 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc > %t2.out + +#include <stdio.h> +#include <float.h> + +// FIXME: This doesn't really work at all, it just doesn't +// crash. Until we have wide constant support, that is all we care +// about; the only reason this comes up is in initialization of +// constants, we don't actually end up seeing much code which uses long +// double. +int main() { + long double a = LDBL_MAX; + long double b = -1; + long double c = a + b; + printf("a = %Lg\n", a); + printf("b = %Lg\n", b); + printf("c = %Lg\n", c); + return 0; +} diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c new file mode 100644 index 00000000..c4d9644a --- /dev/null +++ b/test/Feature/LowerSwitch.c @@ -0,0 +1,30 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc +// RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc +// RUN: not test -f klee-last/test000010.bout +// RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc +// RUN: test -f klee-last/test000010.bout + +#include <stdio.h> + +int main(int argc, char **argv) { + int c = klee_range(0, 256, "range"); + + switch(c) { + case 0: printf("0\n"); break; + case 10: printf("10\n"); break; + case 16: printf("16\n"); break; + case 17: printf("17\n"); break; + case 18: printf("18\n"); break; + case 19: printf("19\n"); break; +#define C(x) case x: case x+1: case x+2: case x+3 +#define C2(x) C(x): C(x+4): C(x+8): C(x+12) +#define C3(x) C2(x): C2(x+16): C2(x+32): C2(x+48) + C3(128): + printf("bignums: %d\n", c); break; + default: + printf("default\n"); + break; + } + + return 0; +} diff --git a/test/Feature/MakeConcreteSymbolic.c b/test/Feature/MakeConcreteSymbolic.c new file mode 100644 index 00000000..29b43a04 --- /dev/null +++ b/test/Feature/MakeConcreteSymbolic.c @@ -0,0 +1,19 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc +// RUN: grep "done: total queries = 0" klee-last/info +// RUN: %klee --make-concrete-symbolic=1 --exit-on-error %t1.bc +// RUN: grep "done: total queries = 2" klee-last/info + + +#include <assert.h> + +#define N 2 +int main() { + int i; + char a; + + a = 10; + assert(a == 10); + + return 0; +} diff --git a/test/Feature/MakeSymbolicName.c b/test/Feature/MakeSymbolicName.c new file mode 100644 index 00000000..c1f11424 --- /dev/null +++ b/test/Feature/MakeSymbolicName.c @@ -0,0 +1,17 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: %klee --use-random-search --exit-on-error %t1.bc + +#include <assert.h> + +int main() { + int a[4] = {1, 2, 3, 4}; + unsigned i; + + klee_make_symbolic_name(&i, sizeof(i), "index"); + if (i > 3) + klee_silent_exit(0); + + assert(a[i] << 1 != 5); + if (a[i] << 1 == 6) + assert(i == 2); +} diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c new file mode 100644 index 00000000..3b1bacaf --- /dev/null +++ b/test/Feature/MemoryLimit.c @@ -0,0 +1,37 @@ +// RUN: %llvmgcc -DLITTLE_ALLOC -g -c %s -o %t.little.bc +// RUN: %llvmgcc -g -c %s -o %t.big.bc +// RUN: %klee --max-memory=20 %t.little.bc > %t.little.log +// RUN: %klee --max-memory=20 %t.big.bc > %t.big.log +// RUN: not grep -q "DONE" %t.little.log +// RUN: not grep -q "DONE" %t.big.log + +#include <stdlib.h> + +int main() { + int i, j, x=0; + +#ifdef LITTLE_ALLOC + printf("IN LITTLE ALLOC\n"); + + // 200 MBs total (in 32 byte chunks) + for (i=0; i<100; i++) { + for (j=0; j<(1<<16); j++) + malloc(1<<5); + } +#else + printf("IN BIG ALLOC\n"); + + // 200 MBs total + for (i=0; i<100; i++) { + malloc(1<<21); + + // Ensure we hit the periodic check + for (j=0; j<10000; j++) + x++; + } +#endif + + printf("DONE!\n"); + + return x; +} diff --git a/test/Feature/MultipleFreeResolution.c b/test/Feature/MultipleFreeResolution.c new file mode 100644 index 00000000..872d6856 --- /dev/null +++ b/test/Feature/MultipleFreeResolution.c @@ -0,0 +1,39 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee --emit-all-errors %t1.bc +// RUN: ls klee-last/ | grep .out | wc -l | grep 4 +// RUN: ls klee-last/ | grep .err | wc -l | grep 3 + +#include <stdlib.h> +#include <stdio.h> + +unsigned klee_urange(unsigned start, unsigned end) { + unsigned x; + klee_make_symbolic(&x, sizeof x); + if (x-start>=end-start) klee_silent_exit(0); + return x; +} + +int *make_int(int i) { + int *x = malloc(sizeof(*x)); + *x = i; + return x; +} + +int main() { + int *buf[4]; + int i,s; + + for (i=0; i<3; i++) + buf[i] = make_int(i); + buf[3] = 0; + + s = klee_urange(0,4); + + free(buf[s]); + + for (i=0; i<3; i++) { + printf("*buf[%d] = %d\n", i, *buf[i]); + } + + return 0; +} diff --git a/test/Feature/MultipleReadResolution.c b/test/Feature/MultipleReadResolution.c new file mode 100644 index 00000000..9297cf8d --- /dev/null +++ b/test/Feature/MultipleReadResolution.c @@ -0,0 +1,43 @@ +// RUN: echo "x" > %t1.res +// RUN: echo "x" >> %t1.res +// RUN: echo "x" >> %t1.res +// RUN: echo "x" >> %t1.res +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc > %t1.log +// RUN: diff %t1.res %t1.log + +#include <stdio.h> + +unsigned klee_urange(unsigned start, unsigned end) { + unsigned x; + klee_make_symbolic(&x, sizeof x); + if (x-start>=end-start) klee_silent_exit(0); + return x; +} + +int *make_int(int i) { + int *x = malloc(sizeof(*x)); + *x = i; + return x; +} + +int main() { + int *buf[4]; + int i,s,t; + + for (i=0; i<4; i++) + buf[i] = make_int((i+1)*2); + + s = klee_urange(0,4); + + int x = *buf[s]; + + if (x == 4) + if (s!=1) + abort(); + + printf("x\n"); + fflush(stdout); + + return 0; +} diff --git a/test/Feature/MultipleReallocResolution.c b/test/Feature/MultipleReallocResolution.c new file mode 100644 index 00000000..b1a14ace --- /dev/null +++ b/test/Feature/MultipleReallocResolution.c @@ -0,0 +1,63 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc +// RUN: ls klee-last/ | grep .err | wc -l | grep 2 +// RUN: ls klee-last/ | grep .ptr.err | wc -l | grep 2 + +#include <assert.h> +#include <stdlib.h> +#include <stdio.h> + +unsigned klee_urange(unsigned start, unsigned end) { + unsigned x; + klee_make_symbolic(&x, sizeof x); + if (x-start>=end-start) klee_silent_exit(0); + return x; +} + +int *make_int(int i, int N) { + int *x = malloc(sizeof(*x) * N); + *x = i; + return x; +} + +int main() { + int *buf[4]; + + buf[0] = malloc(sizeof(int)*4); + buf[1] = malloc(sizeof(int)); + buf[2] = 0; // gets malloc'd + buf[3] = (int*) 0xdeadbeef; // boom + + buf[0][0] = 10; + buf[0][1] = 42; + buf[1][0] = 20; + + int i = klee_urange(0,4); + int new_size = 2 * sizeof(int) * klee_urange(0,2); // 0 or 8 + + // whee, party time, needs to: + // Fork if size == 0, in which case all buffers get free'd and + // we will crash in prints below. + // Fork if buf[s] == 0, in which case the buffer gets malloc'd (for s==2) + // Fork on other buffers (s in [0,1]) and do realloc + // for s==0 this is shrinking + // for s==1 this is growing + buf[i] = realloc(buf[i], new_size); + + if (new_size == 0) { + assert(!buf[2]); // free(0) is a no-op + if (i==0) assert(!buf[0] && buf[1]); + if (i==1) assert(buf[0] && !buf[1]); + assert(i != 3); // we should have crashed on free of invalid + } else { + assert(new_size == sizeof(int)*2); + assert(buf[0][0] == 10); + assert(buf[0][1] == 42); // make sure copied + assert(buf[1][0] == 20); + if (i==1) { int x = buf[1][1]; } // should be safe + if (i==2) { int x = buf[2][0]; } // should be safe + assert(i != 3); // we should have crashed on realloc of invalid + } + + return 0; +} diff --git a/test/Feature/MultipleWriteResolution.c b/test/Feature/MultipleWriteResolution.c new file mode 100644 index 00000000..f07b9710 --- /dev/null +++ b/test/Feature/MultipleWriteResolution.c @@ -0,0 +1,43 @@ +// RUN: echo "x" > %t1.res +// RUN: echo "x" >> %t1.res +// RUN: echo "x" >> %t1.res +// RUN: echo "x" >> %t1.res +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc > %t1.log +// RUN: diff %t1.res %t1.log + +#include <stdio.h> + +unsigned klee_urange(unsigned start, unsigned end) { + unsigned x; + klee_make_symbolic(&x, sizeof x); + if (x-start>=end-start) klee_silent_exit(0); + return x; +} + +int *make_int(int i) { + int *x = malloc(sizeof(*x)); + *x = i; + return x; +} + +int main() { + int *buf[4]; + int i,s,t; + + for (i=0; i<4; i++) + buf[i] = make_int((i+1)*2); + + s = klee_urange(0,4); + + *buf[s] = 5; + + if ((*buf[0] + *buf[1] + *buf[2] + *buf[3]) == 17) + if (s!=3) + abort(); + + printf("x\n"); + fflush(stdout); + + return 0; +} diff --git a/test/Feature/NamedSeedMatching.c b/test/Feature/NamedSeedMatching.c new file mode 100644 index 00000000..6d52e7a4 --- /dev/null +++ b/test/Feature/NamedSeedMatching.c @@ -0,0 +1,41 @@ +// RUN: %llvmgcc -c -g %s -o %t.bc +// RUN: rm -rf %t.out +// RUN: %klee --output-dir=%t.out %t.bc "initial" +// RUN: test -f %t.out/test000001.bout +// RUN: not test -f %t.out/test000002.bout +// RUN: %klee --only-replay-seeds --named-seed-matching --seed-out %t.out/test000001.bout %t.bc > %t.log +// RUN: grep -q "a==3" %t.log +// RUN: grep -q "b==4" %t.log +// RUN: grep -q "c==5" %t.log +// RUN: grep -q "x==6" %t.log + +#include <string.h> +#include <stdio.h> + +int main(int argc, char **argv) { + int a, b, c, x; + + if (argc==2 && strcmp(argv[1], "initial") == 0) { + klee_make_symbolic_name(&a, sizeof a, "a"); + klee_make_symbolic_name(&b, sizeof b, "b"); + klee_make_symbolic_name(&c, sizeof c, "c"); + klee_make_symbolic_name(&x, sizeof x, "a"); + + klee_assume(a == 3); + klee_assume(b == 4); + klee_assume(c == 5); + klee_assume(x == 6); + } else { + klee_make_symbolic_name(&a, sizeof a, "a"); + klee_make_symbolic_name(&c, sizeof c, "c"); + klee_make_symbolic_name(&b, sizeof b, "b"); + klee_make_symbolic_name(&x, sizeof x, "a"); + } + + if (a==3) printf("a==3\n"); + if (b==4) printf("b==4\n"); + if (c==5) printf("c==5\n"); + if (x==6) printf("x==6\n"); + + return 0; +} diff --git a/test/Feature/OneFreeError.c b/test/Feature/OneFreeError.c new file mode 100644 index 00000000..8eb13298 --- /dev/null +++ b/test/Feature/OneFreeError.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.ptr.err + +int main() { + int *x = malloc(4); + free(x); + x[0] = 1; + return 0; +} diff --git a/test/Feature/OneOutOfBounds.c b/test/Feature/OneOutOfBounds.c new file mode 100644 index 00000000..11a9eecb --- /dev/null +++ b/test/Feature/OneOutOfBounds.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.ptr.err + +int main() { + int *x = malloc(4); + x[1] = 1; + free(x); + return 0; +} diff --git a/test/Feature/Optimize.c b/test/Feature/Optimize.c new file mode 100644 index 00000000..3c9159c7 --- /dev/null +++ b/test/Feature/Optimize.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s --emit-llvm -O0 -c -o %t2.bc +// RUN: rm -f %t2.log +// RUN: %klee --stop-after-n-instructions=100 --optimize %t2.bc > %t3.log +// RUN: echo "good" > %t3.good +// RUN: diff %t3.log %t3.good + +// should complete by 100 instructions if opt is on + +int main() { + int i, res = 0; + + for (i=1; i<=1000; i++) + res += i; + + if (res == (1000*1001)/2) { + printf("good\n"); + } else { + printf("bad\n"); + } + + return 0; +} diff --git a/test/Feature/OverlappedError.c b/test/Feature/OverlappedError.c new file mode 100644 index 00000000..3c79380c --- /dev/null +++ b/test/Feature/OverlappedError.c @@ -0,0 +1,19 @@ +// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc +// RUN: ls klee-last/ | grep .out | wc -l | grep 4 +// RUN: ls klee-last/ | grep .ptr.err | wc -l | grep 2 + +#include <stdlib.h> + +int main() { + if (klee_range(0,2, "range")) { + char *x = malloc(8); + *((int*) &x[klee_range(0,6, "range")]) = 1; + free(x); + } else { + char *x = malloc(8); + *((int*) &x[klee_range(-1,5, "range")]) = 1; + free(x); + } + return 0; +} diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c new file mode 100644 index 00000000..d73b6076 --- /dev/null +++ b/test/Feature/PreferCex.c @@ -0,0 +1,18 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc +// RUN: klee-bout-tool klee-last/test000001.bout | grep -F 'Hi\x00\x00' + +#include <assert.h> +#include <stdlib.h> +#include <stdio.h> + +int main() { + char buf[4]; + + klee_make_symbolic(buf, sizeof buf); + klee_prefer_cex(buf, buf[0]=='H'); + klee_prefer_cex(buf, buf[1]=='i'); + klee_prefer_cex(buf, buf[2]=='\0'); + + return 0; +} diff --git a/test/Feature/RaiseAsm.c b/test/Feature/RaiseAsm.c new file mode 100644 index 00000000..5b8acab4 --- /dev/null +++ b/test/Feature/RaiseAsm.c @@ -0,0 +1,39 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc + +#include <assert.h> + +typedef unsigned short uint16; +typedef unsigned int uint32; + +uint16 byteswap_uint16(uint16 x) { + return (x << 8) | (x >> 8); +} +uint32 byteswap_uint32(uint32 x) { + return ((byteswap_uint16(x) << 16) | + (byteswap_uint16(x >> 16))); +} + +uint16 byteswap_uint16_asm(uint16 x) { + uint16 res; + __asm__("rorw $8, %w0" : "=r" (res) : "0" (x) : "cc"); + return res; +} + +uint32 byteswap_uint32_asm(uint32 x) { + uint32 res; + __asm__("rorw $8, %w0;" + "rorl $16, %0;" + "rorw $8, %w0" : "=r" (res) : "0" (x) : "cc"); + return res; +} + +int main() { + uint16 ui16 = klee_int("ui16"); + uint32 ui32 = klee_int("ui32"); + + assert(ui16 == byteswap_uint16(byteswap_uint16_asm(ui16))); + assert(ui32 == byteswap_uint32(byteswap_uint32_asm(ui32))); + + return 0; +} diff --git a/test/Feature/ReallocFailure.c b/test/Feature/ReallocFailure.c new file mode 100644 index 00000000..e5105c33 --- /dev/null +++ b/test/Feature/ReallocFailure.c @@ -0,0 +1,18 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee --exit-on-error %t1.bc + +#include <assert.h> +#include <stdlib.h> +#include <stdio.h> + +int main() { + int *p = malloc(sizeof(int)*2); + assert(p); + p[1] = 52; + + int *p2 = realloc(p, 1<<30); + assert(p2 == 0); + assert(p[1] == 52); + + return 0; +} diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c new file mode 100644 index 00000000..3f01fa80 --- /dev/null +++ b/test/Feature/ReplayPath.c @@ -0,0 +1,27 @@ +// RUN: echo "1" > %t1.path +// RUN: echo "0" >> %t1.path +// RUN: echo "1" >> %t1.path +// RUN: echo "0" >> %t1.path +// RUN: echo "1" >> %t1.path +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc +// RUN: %klee --replay-path %t1.path %t2.bc > %t3.log +// RUN: echo "res: 110" > %t3.good +// RUN: diff %t3.log %t3.good + +int main() { + int res = 1; + int x; + + klee_make_symbolic(&x, sizeof x); + + if (x&1) res *= 2; + if (x&2) res *= 3; + if (x&4) res *= 5; + + // get forced branch coverage + if (x&2) res *= 7; + if (!(x&2)) res *= 11; + printf("res: %d\n", res); + + return 0; +} diff --git a/test/Feature/Searchers.c b/test/Feature/Searchers.c new file mode 100644 index 00000000..95ebddf2 --- /dev/null +++ b/test/Feature/Searchers.c @@ -0,0 +1,52 @@ +// RUN: %llvmgcc %s --emit-llvm -O0 -c -o %t2.bc +// RUN: %klee %t2.bc +// RUN: %klee --use-random-search %t2.bc +// RUN: %klee --use-non-uniform-random-search %t2.bc +// RUN: %klee --use-non-uniform-random-search --weight-type=query-cost %t2.bc +// RUN: %klee --use-batching-search %t2.bc +// RUN: %klee --use-batching-search --use-random-search %t2.bc +// RUN: %klee --use-batching-search --use-non-uniform-random-search %t2.bc +// RUN: %klee --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc +// RUN: %klee --use-merge --debug-log-merge --debug-log-state-merge %t2.bc +// RUN: %klee --use-merge --use-batching-search %t2.bc +// RUN: %klee --use-merge --use-batching-search --use-random-search %t2.bc +// RUN: %klee --use-merge --use-batching-search --use-non-uniform-random-search %t2.bc +// RUN: %klee --use-merge --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc +// RUN: %klee --use-iterative-deepening-time-search --use-batching-search %t2.bc +// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-random-search %t2.bc +// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-non-uniform-random-search %t2.bc +// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc + + +/* this test is basically just for coverage and doesn't really do any + correctness check (aside from testing that the various combinations + don't crash) */ + +int validate(char *buf, int N) { + + int i; + + for (i=0; i<N; i++) { + if (buf[i]==0) { + klee_merge(); + return 0; + } + } + + klee_merge(); + return 1; +} + +#ifndef SYMBOLIC_SIZE +#define SYMBOLIC_SIZE 15 +#endif +int main(int argc, char **argv) { + int N = SYMBOLIC_SIZE; + unsigned char *buf = malloc(N); + int i; + + klee_make_symbolic(buf, N); + if (validate(buf, N)) + return buf[0]; + return 0; +} diff --git a/test/Feature/SetForking.c b/test/Feature/SetForking.c new file mode 100644 index 00000000..8620110d --- /dev/null +++ b/test/Feature/SetForking.c @@ -0,0 +1,28 @@ +// RUN: %llvmgcc -g -c %s -o %t.bc +// RUN: %klee %t.bc > %t.log +// RUN: sort %t.log | uniq -c > %t.uniq.log +// RUN: grep "1 A" %t.uniq.log +// RUN: grep "1 B" %t.uniq.log +// RUN: grep "1 C" %t.uniq.log + +#include <stdio.h> + +int main() { + klee_set_forking(0); + + if (klee_range(0, 2, "range")) { + printf("A\n"); + } else { + printf("A\n"); + } + + klee_set_forking(1); + + if (klee_range(0, 2, "range")) { + printf("B\n"); + } else { + printf("C\n"); + } + + return 0; +} diff --git a/test/Feature/Vararg.c b/test/Feature/Vararg.c new file mode 100644 index 00000000..f782c15e --- /dev/null +++ b/test/Feature/Vararg.c @@ -0,0 +1,82 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc +// RUN: %klee %t1.bc > %t2.out +// RUN: grep "types: (52, 37, 2.00, (9,12,15))" %t2.out +// RUN: test -f klee-last/test000001.ptr.err + +#include <stdarg.h> +#include <assert.h> +#include <stdio.h> + +struct triple { + int first, second, third; +}; + +int test1(int x, ...) { + va_list ap; + va_start(ap, x); + int i32 = va_arg(ap, int); + long long i64 = va_arg(ap, long long); + double d = va_arg(ap, double); + struct triple p = va_arg(ap, struct triple); + printf("types: (%d, %lld, %.2f, (%d,%d,%d))\n", i32, i64, d, p.first, p.second, p.third); + va_end(ap); +} + +int sum(int N, ...) { + int i, res = 0; + va_list ap,ap2; + + va_start(ap, N); + for (i=0; i<N; i++) { + if (i==1) + va_copy(ap2, ap); + res += va_arg(ap, int); + } + for (i=0; i<N-1; i++) + res += va_arg(ap2, int); + va_end(ap); + + return res; +} + +// test using aps in an array (no multiple resolution +// testing, though) +int va_array(int N, ...) { + va_list aps[2]; + unsigned i; + unsigned sum1 = 0, sum2 = 0; + + for (i=0; i<2; i++) + va_start(aps[i], N); + + for (i=0; i<N; i++) { + unsigned cmd = va_arg(aps[0], int); + + if (cmd==0) { + sum1 += va_arg(aps[0],int); + } else if (cmd==1) { + sum2 += va_arg(aps[1],int); + } else if (cmd==2) { + va_copy(aps[1], aps[0]); + } + } + + for (i=0; i<2; i++) + va_end(aps[i]); + + return 3*sum1 + 5*sum2; +} + +int main() { + struct triple p = { 9, 12, 15 }; + test1(-1, 52, 37ll, 2.0, p); + + assert(sum(2, 3, 4) == 11); + assert(sum(0) == 0); + assert(va_array(5, 0, 5, 1, 1, 2, 1)==45); // 15 + 30 + + // should give memory error + test1(-1, 52, 37, 2.0, p); + + return 0; +} diff --git a/test/Feature/WithLibc.c b/test/Feature/WithLibc.c new file mode 100644 index 00000000..5e84eb4a --- /dev/null +++ b/test/Feature/WithLibc.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc +// RUN: %klee --libc=klee %t2.bc > %t3.log +// RUN: echo "good" > %t3.good +// RUN: diff %t3.log %t3.good + +int main() { + char buf[4]; + char *s = "foo"; + + klee_make_symbolic(buf, sizeof buf); + buf[3] = 0; + + if (strcmp(buf, s)==0) { + if (buf[0]=='f' && buf[1]=='o' && buf[2]=='o' && buf[3]==0) { + printf("good\n"); + } else { + printf("bad\n"); + } + } + + return 0; +} diff --git a/test/Feature/WriteCov.c b/test/Feature/WriteCov.c new file mode 100644 index 00000000..defc7e59 --- /dev/null +++ b/test/Feature/WriteCov.c @@ -0,0 +1,15 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t2.bc +// RUN: %klee --exit-on-error --write-cov %t2.bc +// RUN: grep WriteCov.c:10 klee-last/test000002.cov +// RUN: grep WriteCov.c:12 klee-last/test000001.cov + +#include <assert.h> + +int main() { + if (klee_range(0,2, "range")) { + assert(__LINE__ == 10); printf("__LINE__ = %d\n", __LINE__); + } else { + assert(__LINE__ == 12); printf("__LINE__ = %d\n", __LINE__); + } + return 0; +} diff --git a/test/Feature/_utils._ll b/test/Feature/_utils._ll new file mode 100644 index 00000000..32a73bb1 --- /dev/null +++ b/test/Feature/_utils._ll @@ -0,0 +1,71 @@ +define i32 @util_make_and_i1(i32 %a, i32 %b) { + %a_i1 = icmp ne i32 %a, 0 + %b_i1 = icmp ne i32 %b, 0 + %res_i1 = and i1 %a_i1, %b_i1 + %res = zext i1 %res_i1 to i32 + ret i32 %res +} + +define i32 @util_make_or_i1(i32 %a, i32 %b) { + %a_i1 = icmp ne i32 %a, 0 + %b_i1 = icmp ne i32 %b, 0 + %res_i1 = or i1 %a_i1, %b_i1 + %res = zext i1 %res_i1 to i32 + ret i32 %res +} + +define i16 @util_make_concat2(i8 %a, i8 %b) { + %tmp = alloca i16 + %tmp8 = bitcast i16* %tmp to i8* + %p0 = getelementptr i8* %tmp8, i32 0 + %p1 = getelementptr i8* %tmp8, i32 1 + store i8 %b, i8* %p0 + store i8 %a, i8* %p1 + %concat = load i16* %tmp + ret i16 %concat +} + +define i32 @util_make_concat4(i8 %a, i8 %b, i8 %c, i8 %d) { + %tmp = alloca i32 + %tmp8 = bitcast i32* %tmp to i8* + %p0 = getelementptr i8* %tmp8, i32 0 + %p1 = getelementptr i8* %tmp8, i32 1 + %p2 = getelementptr i8* %tmp8, i32 2 + %p3 = getelementptr i8* %tmp8, i32 3 + store i8 %d, i8* %p0 + store i8 %c, i8* %p1 + store i8 %b, i8* %p2 + store i8 %a, i8* %p3 + %concat = load i32* %tmp + ret i32 %concat +} + +define i64 @util_make_concat8(i8 %a, i8 %b, i8 %c, i8 %d, + i8 %e, i8 %f, i8 %g, i8 %h) { + %tmp = alloca i64 + %tmp8 = bitcast i64* %tmp to i8* + %p0 = getelementptr i8* %tmp8, i32 0 + %p1 = getelementptr i8* %tmp8, i32 1 + %p2 = getelementptr i8* %tmp8, i32 2 + %p3 = getelementptr i8* %tmp8, i32 3 + %p4 = getelementptr i8* %tmp8, i32 4 + %p5 = getelementptr i8* %tmp8, i32 5 + %p6 = getelementptr i8* %tmp8, i32 6 + %p7 = getelementptr i8* %tmp8, i32 7 + store i8 %h, i8* %p0 + store i8 %g, i8* %p1 + store i8 %f, i8* %p2 + store i8 %e, i8* %p3 + store i8 %d, i8* %p4 + store i8 %c, i8* %p5 + store i8 %b, i8* %p6 + store i8 %a, i8* %p7 + %concat = load i64* %tmp + ret i64 %concat +} + +define i32 @util_make_select(i32 %cond, i32 %t, i32 %f) { + %cond_i1 = icmp ne i32 %cond, 0 + %res = select i1 %cond_i1, i32 %t, i32 %f + ret i32 %res +} \ No newline at end of file diff --git a/test/Feature/const_array_opt1.c b/test/Feature/const_array_opt1.c new file mode 100644 index 00000000..96c46fb9 --- /dev/null +++ b/test/Feature/const_array_opt1.c @@ -0,0 +1,37 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// RUN: %klee --const-array-opt --max-time=10 --only-output-states-covering-new %t.bc >%t.log +// grep -q "Finished successfully!\n" + +/* This is testing the const array optimization. On my 2.3GHz machine + this takes under 2 seconds w/ the optimization and almost 6 minutes + w/o. So we kill it in 10 sec and check if it has finished + successfully. */ + +#include <unistd.h> +#include <assert.h> +#include <stdio.h> + +int main() { +#define N 8192 +#define N_IDX 16 + unsigned char a[N]; + unsigned i, k[N_IDX]; + + for (i=0; i<N; i++) + a[i] = i % 256; + + klee_make_symbolic_name(k, sizeof(k), "k"); + + for (i=0; i<N_IDX; i++) { + if (k[i] >= N) + klee_silent_exit(0); + + if (a[k[i]] == i) + assert(k[i] % 256 == i); + else klee_silent_exit(0); + } + + printf("Finished successfully!\n"); + + return 0; +} diff --git a/test/Feature/dg.exp b/test/Feature/dg.exp new file mode 100644 index 00000000..879685ca --- /dev/null +++ b/test/Feature/dg.exp @@ -0,0 +1,3 @@ +load_lib llvm.exp + +RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{ll,llx,c,cpp,tr}]] diff --git a/test/Feature/utils.h b/test/Feature/utils.h new file mode 100644 index 00000000..5423a0dc --- /dev/null +++ b/test/Feature/utils.h @@ -0,0 +1,16 @@ +typedef unsigned char uint8_t; +typedef unsigned short uint16_t; +typedef unsigned int uint32_t; +typedef unsigned long long uint64_t; + +uint32_t util_make_and_i1(uint32_t a, uint32_t b); +uint32_t util_make_or_i1(uint32_t a, uint32_t b); + +uint16_t util_make_concat2(uint8_t a, uint8_t b); +uint32_t util_make_concat4(uint8_t a, uint8_t b, + uint8_t c, uint8_t d); +uint64_t util_make_concat8(uint8_t a, uint8_t b, + uint8_t c, uint8_t d, + uint8_t e, uint8_t f, + uint8_t g, uint8_t h); +uint32_t util_make_select(uint32_t cond, uint32_t true, uint32_t false); |