Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

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}]]