From 37321de9d86ff45049eec83a069a10d4836b06f0 Mon Sep 17 00:00:00 2001
From: lyxia <lysxia@gmail.com>
Date: Sun, 25 Mar 2018 10:18:39 -0400
Subject: Implement klee_prefer_cex() and klee_abort() in Runtest and added
 corresponding tests

---
 runtime/Runtest/intrinsics.c                       |  6 +++
 test/Replay/libkleeruntest/replay_klee_abort.c     | 21 ++++++++++
 .../Replay/libkleeruntest/replay_klee_prefer_cex.c | 47 ++++++++++++++++++++++
 3 files changed, 74 insertions(+)
 create mode 100644 test/Replay/libkleeruntest/replay_klee_abort.c
 create mode 100644 test/Replay/libkleeruntest/replay_klee_prefer_cex.c

diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 4d785ee2..1e87d947 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -172,6 +172,12 @@ int klee_range(int begin, int end, const char* name) {
   return x;
 }
 
+void klee_prefer_cex(void *object, uintptr_t condition) { }
+
+void klee_abort() {
+  exit(1);
+}
+
 /* not sure we should even define.  is for debugging. */
 void klee_print_expr(const char *msg, ...) { }
 
diff --git a/test/Replay/libkleeruntest/replay_klee_abort.c b/test/Replay/libkleeruntest/replay_klee_abort.c
new file mode 100644
index 00000000..6d195423
--- /dev/null
+++ b/test/Replay/libkleeruntest/replay_klee_abort.c
@@ -0,0 +1,21 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc
+// RUN: test -f %t.klee-out/test000001.ktest
+// RUN: test -f %t.klee-out/test000001.abort.err
+// RUN: test ! -f %t.klee-out/test000002.ktest
+
+// Now try to replay with libkleeRuntest
+// RUN: %cc %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner
+
+// Check that the default is to exit with an error
+// RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1
+
+// Check that setting `KLEE_RUN_TEST_ERRORS_NON_FATAL` will still exit with an error
+// RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest KLEE_RUN_TEST_ERRORS_NON_FATAL=1 %t_runner 2>&1
+
+#include "klee/klee.h"
+
+int main(int argc, char** argv) {
+  klee_abort();
+}
diff --git a/test/Replay/libkleeruntest/replay_klee_prefer_cex.c b/test/Replay/libkleeruntest/replay_klee_prefer_cex.c
new file mode 100644
index 00000000..de494975
--- /dev/null
+++ b/test/Replay/libkleeruntest/replay_klee_prefer_cex.c
@@ -0,0 +1,47 @@
+// RUN: %llvmgcc -DPREFER_VALUE=33 %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc
+
+// This should produce three test cases.
+// RUN: test -f %t.klee-out/test000001.ktest
+// RUN: test -f %t.klee-out/test000002.ktest
+// RUN: test -f %t.klee-out/test000003.ktest
+// RUN: test ! -f %t.klee-out/test000004.ktest
+
+// Now try to replay with libkleeRuntest
+// RUN: %cc -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner
+
+// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_1 %s
+// RUN: env KTEST_FILE=%t.klee-out/test000002.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_2 %s
+// RUN: env KTEST_FILE=%t.klee-out/test000003.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_3 %s
+
+#include "klee/klee.h"
+#include <stdint.h>
+#include <stdio.h>
+
+int main(int argc, char** argv) {
+  int x = 54, y = 55;
+  klee_make_symbolic(&x, sizeof(x), "x");
+  klee_make_symbolic(&y, sizeof(y), "y");
+  klee_prefer_cex(&x, x == 33);
+
+  if (x < 40) {
+    if (y == 0) {
+      klee_assume(x == 0);
+      x++;
+      // It's fine if the prefered value cannot be used
+      // CHECK_3: x=1, y=0
+    } else {
+      // The prefered value should be used if it can be
+      // CHECK_2: x=33
+    }
+  } else {
+    // CHECK_1-NOT: x=33
+  }
+
+#ifdef PRINT_VALUE
+  printf("x=%d, y=%d\n", x, y);
+#endif
+
+  return 0;
+}
-- 
cgit 1.4.1