Add a few simple solver tests

6 files changed, 81 insertions, 0 deletions

diff --git a/test/Solver/CrosscheckCoreStpZ3.c b/test/Solver/CrosscheckCoreStpZ3.c
new file mode 100644
index 00000000..9847d8a6
--- /dev/null
+++ b/test/Solver/CrosscheckCoreStpZ3.c
@@ -0,0 +1,10 @@
+// REQUIRES: stp
+// REQUIRES: z3
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --solver-backend=stp --use-forked-solver=false --debug-crosscheck-core-solver=z3 %t1.bc
+
+#include "ExerciseSolver.c.inc"
+
+// CHECK: KLEE: done: completed paths = 15
+// CHECK: KLEE: done: partially completed paths = 0
diff --git a/test/Solver/DummySolver.c b/test/Solver/DummySolver.c
new file mode 100644
index 00000000..f6fe3671
--- /dev/null
+++ b/test/Solver/DummySolver.c
@@ -0,0 +1,8 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --solver-backend=dummy %t1.bc
+
+#include "ExerciseSolver.c.inc"
+
+// CHECK: KLEE: done: completed paths = 0
+// CHECK: KLEE: done: partially completed paths = 1
diff --git a/test/Solver/ExerciseSolver.c.inc b/test/Solver/ExerciseSolver.c.inc
new file mode 100644
index 00000000..0cd16a25
--- /dev/null
+++ b/test/Solver/ExerciseSolver.c.inc
@@ -0,0 +1,35 @@
+#include "klee/klee.h"
+
+#include <stddef.h>
+#include <stdio.h>
+
+// just play around with a few symbolic values to exercise the solver a bit
+int main(int argc, char **argv) {
+  unsigned arr[4];
+  klee_make_symbolic(arr, sizeof(arr), "arr");
+
+  arr[0] ^= arr[1];
+  arr[2] += arr[3];
+  arr[3] %= 8191;
+
+  {
+    size_t i;
+    klee_make_symbolic(&i, sizeof(i), "i");
+    if (i < sizeof(arr) / sizeof(*arr)) {
+      arr[i] = 0;
+    } else {
+      arr[0] = 0;
+    }
+  }
+
+  if (arr[0] + 8192 == arr[1]) {
+    arr[3] *= 2;
+  }
+
+  unsigned minimum = arr[0];
+  for (size_t i = 1; i < sizeof(arr) / sizeof(*arr); ++i) {
+    if (arr[i] < minimum) {
+      minimum = arr[i];
+    }
+  }
+}
diff --git a/test/Solver/NoSTP.c b/test/Solver/NoSTP.c
new file mode 100644
index 00000000..0e0a90c5
--- /dev/null
+++ b/test/Solver/NoSTP.c
@@ -0,0 +1,10 @@
+// REQUIRES: not-stp
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: not %klee --output-dir=%t.klee-out --solver-backend=stp %t1.bc 2>&1 | FileCheck %s
+// CHECK: Not compiled with STP support
+// CHECK: ERROR: Failed to create core solver
+
+int main(int argc, char **argv) {
+  return 0;
+}
diff --git a/test/Solver/NoZ3.c b/test/Solver/NoZ3.c
new file mode 100644
index 00000000..6e8d4479
--- /dev/null
+++ b/test/Solver/NoZ3.c
@@ -0,0 +1,10 @@
+// REQUIRES: not-z3
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: not %klee --output-dir=%t.klee-out --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s
+// CHECK: Not compiled with Z3 support
+// CHECK: ERROR: Failed to create core solver
+
+int main(int argc, char **argv) {
+  return 0;
+}
diff --git a/test/Solver/ValidatingSolver.c b/test/Solver/ValidatingSolver.c
new file mode 100644
index 00000000..86799a85
--- /dev/null
+++ b/test/Solver/ValidatingSolver.c
@@ -0,0 +1,8 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --debug-validate-solver --debug-assignment-validating-solver %t1.bc
+
+#include "ExerciseSolver.c.inc"
+
+// CHECK: KLEE: done: completed paths = 15
+// CHECK: KLEE: done: partially completed paths = 0
\ No newline at end of file