about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/Feature/ExprLogging.c5
-rw-r--r--test/Feature/IntrinsicTrap.ll28
-rw-r--r--test/Feature/MemoryLimit.c24
-rw-r--r--test/Feature/OvershiftCheck.c26
-rw-r--r--test/Feature/consecutive_divide_by_zero.c30
-rw-r--r--test/Runtime/POSIX/Futimesat.c45
-rw-r--r--test/Runtime/POSIX/Isatty.c4
-rw-r--r--test/Runtime/POSIX/Openat.c18
-rw-r--r--test/Runtime/POSIX/SeedAndFail.c6
-rw-r--r--test/Runtime/POSIX/Stdin.c2
-rw-r--r--test/Solver/LargeIntegers.pc2
11 files changed, 172 insertions, 18 deletions
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
index ad671a5e..9e9df87a 100644
--- a/test/Feature/ExprLogging.c
+++ b/test/Feature/ExprLogging.c
@@ -1,5 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
-// RUN: %klee --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log
+// We disable the cex-cache to eliminate nondeterminism across different solvers, in particular when counting the number of queries in the last two commands
+// RUN: %klee --use-cex-cache=false --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log
 // RUN: %kleaver -print-ast klee-last/all-queries.pc > %t3.log
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
@@ -7,7 +8,7 @@
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
 // RUN: grep "^; Query" klee-last/all-queries.smt2 | wc -l | grep -q 17
-// RUN: grep "^; Query" klee-last/solver-queries.smt2 | wc -l | grep -q 10
+// RUN: grep "^; Query" klee-last/solver-queries.smt2 | wc -l | grep -q 17
 
 #include <assert.h>
 
diff --git a/test/Feature/IntrinsicTrap.ll b/test/Feature/IntrinsicTrap.ll
new file mode 100644
index 00000000..5af46225
--- /dev/null
+++ b/test/Feature/IntrinsicTrap.ll
@@ -0,0 +1,28 @@
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: %klee -disable-opt %t1.bc
+; RUN: grep abort() klee-last/assembly.ll | wc -l | grep -q 2
+; RUN: echo "llvm.trap()" > %t2.ll
+; RUN: grep llvm.trap() klee-last/assembly.ll %t2.ll | wc -l | grep -q 1
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-f128:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+define i32 @main() nounwind {
+entry:
+  %a = add i32 1, 2
+  %b = add i32 %a, 3
+  %c = icmp ne i32 %b, 6
+  br i1 %c, label %btrue, label %bfalse
+
+btrue:
+  call void @llvm.trap() noreturn nounwind
+  unreachable
+
+bfalse:
+  br label %return
+
+return:
+  ret i32 0
+}
+
+declare void @llvm.trap() noreturn nounwind
diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c
index 3b1bacaf..d959c3de 100644
--- a/test/Feature/MemoryLimit.c
+++ b/test/Feature/MemoryLimit.c
@@ -2,35 +2,43 @@
 // 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 "MALLOC FAILED" %t.little.log
+// RUN: not grep -q "MALLOC FAILED" %t.big.log
 // RUN: not grep -q "DONE" %t.little.log
 // RUN: not grep -q "DONE" %t.big.log
 
 #include <stdlib.h>
+#include <stdio.h>
 
 int main() {
-  int i, j, x=0;
+  int i, j, x=0, malloc_failed = 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);
+  for (i=0; i<100 && !malloc_failed; i++) {
+    for (j=0; j<(1<<16); j++){
+      void * p = malloc(1<<5);
+      malloc_failed |= (p == 0);
+    }
   }
 #else
   printf("IN BIG ALLOC\n");
   
   // 200 MBs total
-  for (i=0; i<100; i++) {
-    malloc(1<<21);
-    
+  for (i=0; i<100 && !malloc_failed; i++) {
+    void *p = malloc(1<<21);
+    malloc_failed |= (p == 0);
     // Ensure we hit the periodic check
+    // Use the pointer to be not optimized out by the compiler
     for (j=0; j<10000; j++)
-      x++;
+      x+=(unsigned)p;
   }
 #endif
 
+  if (malloc_failed)
+    printf("MALLOC FAILED\n");
   printf("DONE!\n");
 
   return x;
diff --git a/test/Feature/OvershiftCheck.c b/test/Feature/OvershiftCheck.c
new file mode 100644
index 00000000..bb967166
--- /dev/null
+++ b/test/Feature/OvershiftCheck.c
@@ -0,0 +1,26 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %klee -check-overshift %t.bc 2> %t.log
+// RUN: grep -c "overshift error" %t.log
+// RUN: grep -c "OvershiftCheck.c:19: overshift error" %t.log
+// RUN: grep -c "OvershiftCheck.c:23: overshift error" %t.log
+
+/* This test checks that two consecutive potential overshifts
+ * are reported as errors.
+ */
+int main()
+{
+  unsigned int x=15;
+  unsigned int y;
+  unsigned int z;
+  volatile unsigned int result;
+
+  /* Overshift if y>= sizeof(x) */
+  klee_make_symbolic(&y,sizeof(y),"shift_amount1");
+  result = x << y;
+
+  /* Overshift is z>= sizeof(x) */
+  klee_make_symbolic(&z,sizeof(z),"shift_amount2");
+  result = x >> z;
+
+  return 0;
+}
diff --git a/test/Feature/consecutive_divide_by_zero.c b/test/Feature/consecutive_divide_by_zero.c
new file mode 100644
index 00000000..c1185870
--- /dev/null
+++ b/test/Feature/consecutive_divide_by_zero.c
@@ -0,0 +1,30 @@
+// RUN: %llvmgcc -emit-llvm -c -g -O0 %s -o %t.bc
+// RUN: %klee -check-div-zero -emit-all-errors=0 %t.bc 2> %t.log
+// RUN: grep "completed paths = 3" %t.log
+// RUN: grep "generated tests = 3" %t.log
+// RUN: grep "consecutive_divide_by_zero.c:24: divide by zero" %t.log
+// RUN: grep "consecutive_divide_by_zero.c:27: divide by zero" %t.log
+
+/* This test case captures a bug where two distinct division
+*  by zero errors are treated as the same error and so
+*  only one test case is generated EVEN IF THERE ARE MULTIPLE 
+*  DISTINCT ERRORS!
+*/
+int main()
+{
+  unsigned int a=15;
+  unsigned int b=15;
+  volatile unsigned int d1;
+  volatile unsigned int d2;
+
+  klee_make_symbolic(&d1, sizeof(d1),"divisor1");
+  klee_make_symbolic(&d2, sizeof(d2),"divisor2");
+
+  // deliberate division by zero possible
+  unsigned int result1 = a / d1;
+
+  // another deliberate division by zero possible
+  unsigned int result2 = b / d2;
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Futimesat.c b/test/Runtime/POSIX/Futimesat.c
new file mode 100644
index 00000000..6ae0ca7c
--- /dev/null
+++ b/test/Runtime/POSIX/Futimesat.c
@@ -0,0 +1,45 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -g -c -o %t2.bc
+// RUN: touch /tmp/futimesat-dummy
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: rm /tmp/futimesat-dummy
+
+#include <assert.h>
+#include <fcntl.h>
+#include <sys/stat.h>
+#include <sys/time.h>
+#include <time.h>
+#include <unistd.h>
+
+int main(int argc, char **argv) {
+  int r;
+  struct stat buf;
+  struct timeval times[2];
+
+  times[0].tv_sec = time(NULL)-3600;
+  times[0].tv_usec = 0;
+  times[1].tv_sec = time(NULL)-3600;
+  times[1].tv_usec = 0;
+
+  r = futimesat(AT_FDCWD, "A", times);
+  assert(r != -1);
+
+  r = fstatat(AT_FDCWD, "A", &buf, 0);
+  assert(r != -1);
+  assert(buf.st_atime == times[0].tv_sec &&
+         buf.st_mtime == times[1].tv_sec);
+
+  /* assumes /tmp exists and is writeable */
+  int fd = open("/tmp", O_RDONLY);
+  assert(fd > 0);
+  r = futimesat(fd, "futimesat-dummy", times);
+  assert(r != -1);
+
+  r = fstatat(fd, "futimesat-dummy", &buf, 0);
+  assert(r != -1);
+  assert(buf.st_atime == times[0].tv_sec &&
+         buf.st_mtime == times[1].tv_sec);
+
+  close(fd);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c
index 4f8d1425..293ee653 100644
--- a/test/Runtime/POSIX/Isatty.c
+++ b/test/Runtime/POSIX/Isatty.c
@@ -1,16 +1,16 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
 // RUN: %klee --libc=uclibc --posix-runtime %t.bc --sym-files 0 10 --sym-stdout 2>%t.log
-
 // RUN: test -f klee-last/test000001.ktest
 // RUN: test -f klee-last/test000002.ktest
 // RUN: test -f klee-last/test000003.ktest
 // RUN: test -f klee-last/test000004.ktest
-
 // RUN: grep -q "stdin is a tty" %t.log
 // RUN: grep -q "stdin is NOT a tty" %t.log
 // RUN: grep -q "stdout is a tty" %t.log
 // RUN: grep -q "stdout is NOT a tty" %t.log
 
+// Depending on how uClibc is compiled (i.e. without -DKLEE_SYM_PRINTF)
+// fprintf prints out on stdout even stderr is provided.
 #include <unistd.h>
 #include <stdio.h>
 #include <assert.h>
diff --git a/test/Runtime/POSIX/Openat.c b/test/Runtime/POSIX/Openat.c
new file mode 100644
index 00000000..d417ee47
--- /dev/null
+++ b/test/Runtime/POSIX/Openat.c
@@ -0,0 +1,18 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: test -f klee-last/test000001.ktest
+
+#include <assert.h>
+#include <fcntl.h>
+
+int main(int argc, char **argv) {
+  int fd = openat(AT_FDCWD, "A", O_RDWR|O_TRUNC);
+  if (fd != -1) {
+    char buf[10];
+    assert(read(fd, buf, 10) == 10);
+    assert(klee_is_symbolic(buf[0]));
+  } else {
+    klee_silent_exit(0);
+  }
+  return 0;
+}
diff --git a/test/Runtime/POSIX/SeedAndFail.c b/test/Runtime/POSIX/SeedAndFail.c
index db02217a..740db664 100644
--- a/test/Runtime/POSIX/SeedAndFail.c
+++ b/test/Runtime/POSIX/SeedAndFail.c
@@ -1,12 +1,10 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
 // RUN: rm -rf tmp-123
-// RUN: %klee --libc=klee --output-dir=tmp-123 --posix-runtime %t.bc --sym-files 1 10  2>%t.log
+// RUN: %klee --libc=uclibc --output-dir=tmp-123 --posix-runtime %t.bc --sym-files 1 10  2>%t.log
 // RUN: %klee --seed-out-dir=tmp-123 --zero-seed-extension --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1
 // RUN: ls klee-last | grep -c assert | grep 4
 
-
-
-#include <stdio.h>
+#include <string.h>
 #include <assert.h>
 #include <unistd.h>
 #include <sys/types.h>
diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c
index e7e3f2ff..b5402cf1 100644
--- a/test/Runtime/POSIX/Stdin.c
+++ b/test/Runtime/POSIX/Stdin.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --libc=klee --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log
+// RUN: %klee --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log
 // RUN: grep "mode:file" %t.log
 // RUN: grep "mode:dir" %t.log
 // RUN: grep "mode:chr" %t.log
diff --git a/test/Solver/LargeIntegers.pc b/test/Solver/LargeIntegers.pc
index 99d1a61b..53ff3a51 100644
--- a/test/Solver/LargeIntegers.pc
+++ b/test/Solver/LargeIntegers.pc
@@ -11,7 +11,7 @@ array a[64] : w32 -> w8 = symbolic
 (query [] false [(Extract w5 60 (Concat w128 (w64 1) (w64 2)))])
 
 # RUN: grep -A 1 \"Query 2\" %t > %t2
-# RUN: grep \"Array 0:\ta.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0\" %t2
+# RUN: grep \"Array 0:\ta.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1\" %t2
 (query [(Eq 0x0102030405060708090A0B0C0D0E0F10 (ReadLSB w128 0 a))] 
        false 
        [] [a])