From f7791f216ffdc5a7eb1166b2bd6462c00e7e5854 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Fri, 23 Feb 2018 14:50:44 -0800
Subject: [PATCH 01/19] Add stub header that declares the KLEE API

---
 src/include/deepstate/Klee.h | 112 +++++++++++++++++++++++++++++++++++
 1 file changed, 112 insertions(+)
 create mode 100644 src/include/deepstate/Klee.h

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
new file mode 100644
index 0000000..6689266
--- /dev/null
+++ b/src/include/deepstate/Klee.h
@@ -0,0 +1,112 @@
+/*
+ * Copyright (c) 2018 Trail of Bits, Inc.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#ifndef SRC_INCLUDE_DEEPSTATE_KLEE_H_
+#define SRC_INCLUDE_DEEPSTATE_KLEE_H_
+
+#include <deepstate/DeepState.h>
+
+#define KLEE_GET_VALUE(suffix, type) type klee_get_value ## suffix(type expr)
+
+DEEPSTATE_BEGIN_EXTERN_C
+
+/* TODO(joe): Implement */
+static void klee_define_fixed_object(void *addr, size_t nbytes);
+
+/* TODO(joe): Implement */
+static void klee_make_symbolic(void *addr, size_t nbytes, const char *name);
+
+/* TODO(joe): Implement */
+static int klee_range(int begin, int end, const char *name);
+
+/* TODO(joe): Implement */
+static int klee_int(const char *name);
+
+/* TODO(joe): Implement */
+DEEPSTATE_NORETURN static void klee_silent_exit(int status);
+
+/* TODO(joe): Implement */
+static size_t klee_get_obj_size(void *ptr);
+
+/* TODO(joe): Implement */
+static void klee_print_expr(const char *msg, ...);
+
+/* TODO(joe): Implement */
+static uintptr_t klee_choose(uintptr_t n);
+
+/* TODO(joe): Implement */
+static unsigned klee_is_symbolic(uintptr_t n);
+
+/* TODO(joe): Implement */
+static void klee_assume(uintptr_t condition);
+
+/* TODO(joe): Implement */
+static void klee_warning(const char *message);
+
+/* TODO(joe): Implement */
+static void klee_warning_once(const char *message);
+
+/* TODO(joe): Implement */
+static void klee_prefer_cex(void *object, uintptr_t condition);
+
+/* TODO(joe): Implement */
+static void klee_posix_prefer_cex(void *object, uintptr_t condition);
+
+/* TODO(joe): Implement */
+static void klee_mark_global(void *object);
+
+/* TODO(joe): Implement */
+static KLEE_GET_VALUE(f, float);
+
+/* TODO(joe): Implement */
+static KLEE_GET_VALUE(d, double);
+
+/* TODO(joe): Implement */
+static KLEE_GET_VALUE(l, long);
+
+/* TODO(joe): Implement */
+static KLEE_GET_VALUE(ll, long long);
+
+/* TODO(joe): Implement */
+static KLEE_GET_VALUE(_i32, int32_t);
+
+/* TODO(joe): Implement */
+static KLEE_GET_VALUE(_i64, int64_t);
+
+/* TODO(joe): Implement */
+static void klee_check_memory_access(const void *address, size_t size);
+
+/* TODO(joe): Implement */
+static void klee_set_forking(unsigned enable);
+
+/* TODO(joe): Implement */
+static void klee_alias_function(const char *fn_name, const char *new_fn_name);
+
+/* TODO(joe): Implement */
+static void klee_stack_trace(void);
+
+/* TODO(joe): Implement */
+static void klee_print_range(const char *name, int arg);
+
+/* TODO(joe): Implement */
+static void klee_open_merge(void);
+
+/* TODO(joe): Implement */
+static void klee_close_merge(void);
+
+DEEPSTATE_END_EXTERN_C
+
+#endif  /* SRC_INCLUDE_DEEPSTATE_KLEE_H_ */

From 236ee6856e7d7aa85375f3df6f72ef00b0d8917a Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Fri, 23 Feb 2018 15:09:02 -0800
Subject: [PATCH 02/19] Add lib impl for `klee_make_symbolic()`

---
 src/include/deepstate/Klee.h | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index 6689266..982391f 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -26,8 +26,9 @@ DEEPSTATE_BEGIN_EXTERN_C
 /* TODO(joe): Implement */
 static void klee_define_fixed_object(void *addr, size_t nbytes);
 
-/* TODO(joe): Implement */
-static void klee_make_symbolic(void *addr, size_t nbytes, const char *name);
+static void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
+  DeepState_SymbolizeData(addr, addr + nbytes);
+}
 
 /* TODO(joe): Implement */
 static int klee_range(int begin, int end, const char *name);

From 973d2a92649c09111b41dc5bd62085eaaa41589d Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Fri, 23 Feb 2018 14:51:26 -0800
Subject: [PATCH 03/19] Add KLEE example

---
 examples/CMakeLists.txt |  3 +++
 examples/Klee.c         | 39 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+)
 create mode 100644 examples/Klee.c

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 8db60a0..295d7b5 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -46,3 +46,6 @@ set_target_properties(Squares PROPERTIES COMPILE_DEFINITIONS "DEEPSTATE_TEST")
 
 add_executable(TakeOver TakeOver.cpp)
 target_link_libraries(TakeOver deepstate)
+
+add_executable(Klee Klee.c)
+target_link_libraries(Klee deepstate)
diff --git a/examples/Klee.c b/examples/Klee.c
new file mode 100644
index 0000000..2d15523
--- /dev/null
+++ b/examples/Klee.c
@@ -0,0 +1,39 @@
+/*
+ * Copyright (c) 2018 Trail of Bits, Inc.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include <deepstate/Klee.h>
+
+DEEPSTATE_NOINLINE int get_sign(int x) {
+  if (x == 0) {
+    printf("zero\n");
+    return 0;
+  }
+
+  if (x < 0) {
+    printf("negative\n");
+    return -1;
+  } else {
+    printf("positive\n");
+    return 1;
+  }
+}
+
+int main(int argc, char *argv[]) {
+  int a;
+  klee_make_symbolic(&a, sizeof(a), "a");
+
+  return get_sign(a);
+}

From 4edfccd95389ee3340d4b3887177b9353ae00023 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Fri, 23 Feb 2018 14:47:57 -0800
Subject: [PATCH 04/19] Internally support varying take-over symbols in angr
 executor

---
 bin/deepstate/main_angr.py | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/bin/deepstate/main_angr.py b/bin/deepstate/main_angr.py
index cade611..cd0b60b 100644
--- a/bin/deepstate/main_angr.py
+++ b/bin/deepstate/main_angr.py
@@ -360,13 +360,14 @@ def hook_apis(project, run_state):
   return mc, apis
 
 
-def main_take_over(args, project):
-  takeover_ea = find_symbol_ea(project, 'DeepState_TakeOver')
+def main_take_over(args, project, takeover_symbol):
+  takeover_ea = find_symbol_ea(project, takeover_symbol)
 
   hook_function(project, takeover_ea, TakeOver)
 
   if not takeover_ea:
-    L.critical("Cannot find symbol `DeepState_TakeOver` in binary `{}`".format(
+    L.critical("Cannot find symbol `{}` in binary `{}`".format(
+        takeover_symbol,
         args.binary))
     return 1
 
@@ -385,14 +386,16 @@ def main_take_over(args, project):
   try:
     takeover_state = concrete_manager.found[0]
   except:
-    L.critical("Execution never hit `DeepState_TakeOver` in binary `{}`".format(
+    L.critical("Execution never hit `{}` in binary `{}`".format(
+        takeover_symbol,
         args.binary))
     return 1
 
   try:
     run_state = takeover_state.step().successors[0]
   except:
-    L.critical("Unable to exit from `DeepState_TakeOver` in binary `{}`".format(
+    L.critical("Unable to exit from `{}` in binary `{}`".format(
+        takeover_symbol,
         args.binary))
     return 1
 
@@ -486,7 +489,7 @@ def main():
     return 1
 
   if args.take_over:
-    return main_take_over(args, project)
+    return main_take_over(args, project, 'DeepState_TakeOver')
   else:
     return main_unit_test(args, project)
 

From 330f58b9448874ef7996879544a64a58ab020dc1 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Fri, 23 Feb 2018 14:49:21 -0800
Subject: [PATCH 05/19] Add KLEE support to angr executor

---
 bin/deepstate/common.py    | 4 ++++
 bin/deepstate/main_angr.py | 5 ++++-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/bin/deepstate/common.py b/bin/deepstate/common.py
index db77def..57d096d 100644
--- a/bin/deepstate/common.py
+++ b/bin/deepstate/common.py
@@ -125,6 +125,10 @@ class DeepState(object):
         "--take_over", action='store_true',
         help="Explore the program starting at the `TakeOver` hook.")
 
+    parser.add_argument(
+        "--klee", action='store_true',
+        help="Expect the test binary to use the KLEE API and use `main()` as entry point.")
+
     parser.add_argument(
         "binary", type=str, help="Path to the test binary to run.")
 
diff --git a/bin/deepstate/main_angr.py b/bin/deepstate/main_angr.py
index cd0b60b..6f2b3c8 100644
--- a/bin/deepstate/main_angr.py
+++ b/bin/deepstate/main_angr.py
@@ -363,7 +363,8 @@ def hook_apis(project, run_state):
 def main_take_over(args, project, takeover_symbol):
   takeover_ea = find_symbol_ea(project, takeover_symbol)
 
-  hook_function(project, takeover_ea, TakeOver)
+  if not args.klee:
+      hook_function(project, takeover_ea, TakeOver)
 
   if not takeover_ea:
     L.critical("Cannot find symbol `{}` in binary `{}`".format(
@@ -490,6 +491,8 @@ def main():
 
   if args.take_over:
     return main_take_over(args, project, 'DeepState_TakeOver')
+  elif args.klee:
+    return main_take_over(args, project, 'main')
   else:
     return main_unit_test(args, project)
 

From 9e3d1d1eb252b498a7da5a2fe210bf934f902bfa Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Fri, 23 Feb 2018 16:40:11 -0800
Subject: [PATCH 06/19] Impl KLEE warning funcs

---
 src/include/deepstate/Klee.h | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index 982391f..0cc069d 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -54,11 +54,13 @@ static unsigned klee_is_symbolic(uintptr_t n);
 /* TODO(joe): Implement */
 static void klee_assume(uintptr_t condition);
 
-/* TODO(joe): Implement */
-static void klee_warning(const char *message);
+static void klee_warning(const char *message) {
+  DeepState_Log(DeepState_LogWarning, message);
+}
 
-/* TODO(joe): Implement */
-static void klee_warning_once(const char *message);
+static void klee_warning_once(const char *message) {
+  DeepState_Log(DeepState_LogWarning, message);
+}
 
 /* TODO(joe): Implement */
 static void klee_prefer_cex(void *object, uintptr_t condition);

From 6b95aab503f9f1f1971b913859c60d35b5beadae Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Fri, 23 Feb 2018 16:48:14 -0800
Subject: [PATCH 07/19] Impl `klee_silent_exit()`

---
 src/include/deepstate/Klee.h | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index 0cc069d..9baff4e 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -36,8 +36,9 @@ static int klee_range(int begin, int end, const char *name);
 /* TODO(joe): Implement */
 static int klee_int(const char *name);
 
-/* TODO(joe): Implement */
-DEEPSTATE_NORETURN static void klee_silent_exit(int status);
+DEEPSTATE_NORETURN static void klee_silent_exit(int status) {
+  exit(status);
+}
 
 /* TODO(joe): Implement */
 static size_t klee_get_obj_size(void *ptr);

From e33b9101829bba4fcb3b2a3ce462dea85fd4fb77 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 12:22:21 -0800
Subject: [PATCH 08/19] Add no-op impls for KLEE engine commands

These functions do not have a DeepState equivalent, nor do they impact
the semantics of the symbolic program to be executed.
---
 src/include/deepstate/Klee.h | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index 9baff4e..f90c62d 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -63,11 +63,13 @@ static void klee_warning_once(const char *message) {
   DeepState_Log(DeepState_LogWarning, message);
 }
 
-/* TODO(joe): Implement */
-static void klee_prefer_cex(void *object, uintptr_t condition);
+static void klee_prefer_cex(void *object, uintptr_t condition) {
+  /* KLEE engine command, no DeepState equivalent. */
+}
 
-/* TODO(joe): Implement */
-static void klee_posix_prefer_cex(void *object, uintptr_t condition);
+static void klee_posix_prefer_cex(void *object, uintptr_t condition) {
+  /* KLEE engine command, no DeepState equivalent. */
+}
 
 /* TODO(joe): Implement */
 static void klee_mark_global(void *object);
@@ -93,8 +95,9 @@ static KLEE_GET_VALUE(_i64, int64_t);
 /* TODO(joe): Implement */
 static void klee_check_memory_access(const void *address, size_t size);
 
-/* TODO(joe): Implement */
-static void klee_set_forking(unsigned enable);
+static void klee_set_forking(unsigned enable) {
+  /* KLEE engine command, no DeepState equivalent. */
+}
 
 /* TODO(joe): Implement */
 static void klee_alias_function(const char *fn_name, const char *new_fn_name);
@@ -105,11 +108,13 @@ static void klee_stack_trace(void);
 /* TODO(joe): Implement */
 static void klee_print_range(const char *name, int arg);
 
-/* TODO(joe): Implement */
-static void klee_open_merge(void);
+static void klee_open_merge(void) {
+  /* KLEE engine command, no DeepState equivalent. */
+}
 
-/* TODO(joe): Implement */
-static void klee_close_merge(void);
+static void klee_close_merge(void) {
+  /* KLEE engine command, no DeepState equivalent. */
+}
 
 DEEPSTATE_END_EXTERN_C
 

From 994d29b2d31cdcc389d9e3ffcbf4911c54e3f29f Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 12:47:13 -0800
Subject: [PATCH 09/19] Add no-op impls for KLEE-internal debugging functions

---
 src/include/deepstate/Klee.h | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index f90c62d..7c331a2 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -43,8 +43,10 @@ DEEPSTATE_NORETURN static void klee_silent_exit(int status) {
 /* TODO(joe): Implement */
 static size_t klee_get_obj_size(void *ptr);
 
-/* TODO(joe): Implement */
-static void klee_print_expr(const char *msg, ...);
+static void klee_print_expr(const char *msg, ...) {
+  /* KLEE debugging command, no DeepState equivalent. */
+  /* See impl in `runtime/Runtest/intrinsics.c`. */
+}
 
 /* TODO(joe): Implement */
 static uintptr_t klee_choose(uintptr_t n);
@@ -102,11 +104,13 @@ static void klee_set_forking(unsigned enable) {
 /* TODO(joe): Implement */
 static void klee_alias_function(const char *fn_name, const char *new_fn_name);
 
-/* TODO(joe): Implement */
-static void klee_stack_trace(void);
+static void klee_stack_trace(void) {
+  /* KLEE debugging command, no DeepState equivalent. */
+}
 
-/* TODO(joe): Implement */
-static void klee_print_range(const char *name, int arg);
+static void klee_print_range(const char *name, int arg) {
+  /* KLEE debugging command, no DeepState equivalent. */
+}
 
 static void klee_open_merge(void) {
   /* KLEE engine command, no DeepState equivalent. */

From 27b2a490ee101f7dc61cf0d2e369a1e31cd3ce9e Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 13:07:03 -0800
Subject: [PATCH 10/19] Comment out unsupported KLEE functions

We don't declare the functions to ensure compilation fails fast, not
linking. We keep the commented prototype for the sake of documentation,
instead of just deleting it. We may also eventually be able to impl the
functions if we extend the DeepState API.
---
 src/include/deepstate/Klee.h | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index 7c331a2..bc29ebd 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -23,8 +23,8 @@
 
 DEEPSTATE_BEGIN_EXTERN_C
 
-/* TODO(joe): Implement */
-static void klee_define_fixed_object(void *addr, size_t nbytes);
+/* Unsupported. */
+/* static void klee_define_fixed_object(void *addr, size_t nbytes); */
 
 static void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
   DeepState_SymbolizeData(addr, addr + nbytes);
@@ -40,8 +40,8 @@ DEEPSTATE_NORETURN static void klee_silent_exit(int status) {
   exit(status);
 }
 
-/* TODO(joe): Implement */
-static size_t klee_get_obj_size(void *ptr);
+/* Unsupported. */
+/* static size_t klee_get_obj_size(void *ptr); */
 
 static void klee_print_expr(const char *msg, ...) {
   /* KLEE debugging command, no DeepState equivalent. */
@@ -54,8 +54,8 @@ static uintptr_t klee_choose(uintptr_t n);
 /* TODO(joe): Implement */
 static unsigned klee_is_symbolic(uintptr_t n);
 
-/* TODO(joe): Implement */
-static void klee_assume(uintptr_t condition);
+/* Unsupported. */
+/* static void klee_assume(uintptr_t condition); */
 
 static void klee_warning(const char *message) {
   DeepState_Log(DeepState_LogWarning, message);
@@ -73,8 +73,8 @@ static void klee_posix_prefer_cex(void *object, uintptr_t condition) {
   /* KLEE engine command, no DeepState equivalent. */
 }
 
-/* TODO(joe): Implement */
-static void klee_mark_global(void *object);
+/* Unsupported. */
+/* static void klee_mark_global(void *object); */
 
 /* TODO(joe): Implement */
 static KLEE_GET_VALUE(f, float);
@@ -94,15 +94,16 @@ static KLEE_GET_VALUE(_i32, int32_t);
 /* TODO(joe): Implement */
 static KLEE_GET_VALUE(_i64, int64_t);
 
-/* TODO(joe): Implement */
-static void klee_check_memory_access(const void *address, size_t size);
+/* Unsupported. */
+/* static void klee_check_memory_access(const void *address, size_t size); */
 
 static void klee_set_forking(unsigned enable) {
   /* KLEE engine command, no DeepState equivalent. */
 }
 
-/* TODO(joe): Implement */
-static void klee_alias_function(const char *fn_name, const char *new_fn_name);
+/* Unsupported. */
+/* static void
+ * klee_alias_function(const char *fn_name, const char *new_fn_name); */
 
 static void klee_stack_trace(void) {
   /* KLEE debugging command, no DeepState equivalent. */

From 16ce8d6e008f006248b0da97e8bae7f832062fb5 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 13:22:42 -0800
Subject: [PATCH 11/19] Add decl, impl for `klee_abort()`

---
 src/include/deepstate/Klee.h | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index bc29ebd..d65a021 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -40,6 +40,10 @@ DEEPSTATE_NORETURN static void klee_silent_exit(int status) {
   exit(status);
 }
 
+DEEPSTATE_NORETURN static void klee_abort(void) {
+  abort();
+}
+
 /* Unsupported. */
 /* static size_t klee_get_obj_size(void *ptr); */
 

From a1aaeee8c848d38be9a846aea60765bc9c404d52 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 13:44:46 -0800
Subject: [PATCH 12/19] Use short-lived preprocessor def

---
 src/include/deepstate/Klee.h | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index d65a021..2d34f59 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -19,8 +19,6 @@
 
 #include <deepstate/DeepState.h>
 
-#define KLEE_GET_VALUE(suffix, type) type klee_get_value ## suffix(type expr)
-
 DEEPSTATE_BEGIN_EXTERN_C
 
 /* Unsupported. */
@@ -80,6 +78,8 @@ static void klee_posix_prefer_cex(void *object, uintptr_t condition) {
 /* Unsupported. */
 /* static void klee_mark_global(void *object); */
 
+#define KLEE_GET_VALUE(suffix, type) type klee_get_value ## suffix(type val)
+
 /* TODO(joe): Implement */
 static KLEE_GET_VALUE(f, float);
 
@@ -98,6 +98,8 @@ static KLEE_GET_VALUE(_i32, int32_t);
 /* TODO(joe): Implement */
 static KLEE_GET_VALUE(_i64, int64_t);
 
+#undef KLEE_GET_VALUE
+
 /* Unsupported. */
 /* static void klee_check_memory_access(const void *address, size_t size); */
 

From 63f22739f929c24f96a43d9c058453e553c7f462 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 14:04:28 -0800
Subject: [PATCH 13/19] Impl supported `klee_get_val` functions

We will extend the DeepState API to support the others.
---
 src/include/deepstate/Klee.h | 30 +++++++++++++++++-------------
 1 file changed, 17 insertions(+), 13 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index 2d34f59..9408f67 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -80,23 +80,27 @@ static void klee_posix_prefer_cex(void *object, uintptr_t condition) {
 
 #define KLEE_GET_VALUE(suffix, type) type klee_get_value ## suffix(type val)
 
-/* TODO(joe): Implement */
-static KLEE_GET_VALUE(f, float);
+/* Unsupported. */
+/* static KLEE_GET_VALUE(f, float); */
+
+/* Unsupported. */
+/* static KLEE_GET_VALUE(d, double); */
+
+static KLEE_GET_VALUE(l, long) {
+  DeepState_MinInt(val);
+}
+
+/* Unsupported. */
+/* static KLEE_GET_VALUE(ll, long long) */
 
 /* TODO(joe): Implement */
-static KLEE_GET_VALUE(d, double);
+static KLEE_GET_VALUE(_i32, int32_t) {
+  DeepState_MinInt(val);
+}
 
 /* TODO(joe): Implement */
-static KLEE_GET_VALUE(l, long);
-
-/* TODO(joe): Implement */
-static KLEE_GET_VALUE(ll, long long);
-
-/* TODO(joe): Implement */
-static KLEE_GET_VALUE(_i32, int32_t);
-
-/* TODO(joe): Implement */
-static KLEE_GET_VALUE(_i64, int64_t);
+/* Unsupported. */
+/* static KLEE_GET_VALUE(_i64, int64_t); */
 
 #undef KLEE_GET_VALUE
 

From 2ff08e5d706cfecc26dd05748aa0a933d2344667 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 14:20:57 -0800
Subject: [PATCH 14/19] Add impls for KLEE symbolic int functions

---
 src/include/deepstate/Klee.h | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index 9408f67..3c848d4 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -28,11 +28,13 @@ static void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
   DeepState_SymbolizeData(addr, addr + nbytes);
 }
 
-/* TODO(joe): Implement */
-static int klee_range(int begin, int end, const char *name);
+static int klee_range(int begin, int end, const char *name) {
+  return DeepState_IntInRange(begin, end);
+}
 
-/* TODO(joe): Implement */
-static int klee_int(const char *name);
+static int klee_int(const char *name) {
+  return DeepState_Int();
+}
 
 DEEPSTATE_NORETURN static void klee_silent_exit(int status) {
   exit(status);

From dc9c353244af5839f9204ac7d9be6d24cbb7c0c1 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 14:22:51 -0800
Subject: [PATCH 15/19] Comment out unsupported `klee_is_symbolic`

This takes a memory address as an argument, not a possibly-symbolic
value (which we do support). We probably need to extend the DeepState
API to support this robustly.
---
 src/include/deepstate/Klee.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index 3c848d4..3f90341 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -55,8 +55,8 @@ static void klee_print_expr(const char *msg, ...) {
 /* TODO(joe): Implement */
 static uintptr_t klee_choose(uintptr_t n);
 
-/* TODO(joe): Implement */
-static unsigned klee_is_symbolic(uintptr_t n);
+/* Unsupported. */
+/* static unsigned klee_is_symbolic(uintptr_t n); */
 
 /* Unsupported. */
 /* static void klee_assume(uintptr_t condition); */

From 2cb1bf002d7d91634c49ed5e5e05a6409bb539a5 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 14:38:26 -0800
Subject: [PATCH 16/19] Add impl for `klee_choose()`

---
 src/include/deepstate/Klee.h | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h
index 3f90341..2c8a4c5 100644
--- a/src/include/deepstate/Klee.h
+++ b/src/include/deepstate/Klee.h
@@ -52,8 +52,16 @@ static void klee_print_expr(const char *msg, ...) {
   /* See impl in `runtime/Runtest/intrinsics.c`. */
 }
 
-/* TODO(joe): Implement */
-static uintptr_t klee_choose(uintptr_t n);
+static uintptr_t klee_choose(uintptr_t n) {
+  uintptr_t out;
+  klee_make_symbolic(&out, sizeof(out), "klee_choose");
+
+  if (n <= out) {
+    klee_silent_exit(0);
+  }
+
+  return out;
+}
 
 /* Unsupported. */
 /* static unsigned klee_is_symbolic(uintptr_t n); */

From 376235808aaa1d55821d9079ea919833662eb60b Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 16:23:44 -0800
Subject: [PATCH 17/19] Internally support varying take-over symbols in
 Manticore executor

---
 bin/deepstate/main_manticore.py | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/bin/deepstate/main_manticore.py b/bin/deepstate/main_manticore.py
index 73036a1..6f38cf2 100644
--- a/bin/deepstate/main_manticore.py
+++ b/bin/deepstate/main_manticore.py
@@ -374,11 +374,12 @@ def run_tests(args, state, apis):
   exit(0)
 
 
-def main_takeover(m, args):
-  takeover_ea = find_symbol_ea(m, 'DeepState_TakeOver')
+def main_takeover(m, args, takeover_symbol):
+  takeover_ea = find_symbol_ea(m, takeover_symbol)
   if not takeover_ea:
-    L.critical("Cannot find symbol `DeepState_TakeOver` in binary `{}`".format(
-        args.binary))
+    L.critical("Cannot find symbol `{}` in binary `{}`".format(
+      takeover_symbol,
+      args.binary))
     return 1
 
   takeover_state = m._initial_state
@@ -438,7 +439,7 @@ def main():
   m._binary_obj = m._initial_state.platform.elf
 
   if args.take_over:
-    return main_takeover(m, args)
+    return main_takeover(m, args, 'DeepState_TakeOver')
   else:
     return main_unit_test(m, args)
 

From 96dafe6f4122ca05e8bbb00201faf8d29b5f3643 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 16:24:58 -0800
Subject: [PATCH 18/19] Fix wrapped indentation

---
 bin/deepstate/main_manticore.py | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/bin/deepstate/main_manticore.py b/bin/deepstate/main_manticore.py
index 6f38cf2..bad32f8 100644
--- a/bin/deepstate/main_manticore.py
+++ b/bin/deepstate/main_manticore.py
@@ -351,7 +351,7 @@ def run_test(state, apis, test):
     do_run_test(state, apis, test)
   except:
     L.error("Uncaught exception: {}\n{}".format(
-        sys.exc_info()[0], traceback.format_exc()))
+      sys.exc_info()[0], traceback.format_exc()))
 
 
 def run_tests(args, state, apis):
@@ -362,7 +362,7 @@ def run_tests(args, state, apis):
   tests = mc.find_test_cases()
 
   L.info("Running {} tests across {} workers".format(
-      len(tests), args.num_workers))
+    len(tests), args.num_workers))
 
   for test in tests:
     res = pool.apply_async(run_test, (state, apis, test))
@@ -403,7 +403,7 @@ def main_unit_test(m, args):
   setup_ea = find_symbol_ea(m, 'DeepState_Setup')
   if not setup_ea:
     L.critical("Cannot find symbol `DeepState_Setup` in binary `{}`".format(
-        args.binary))
+      args.binary))
     return 1
 
   setup_state = m._initial_state
@@ -429,7 +429,7 @@ def main():
     m = manticore.Manticore(args.binary)
   except Exception as e:
     L.critical("Cannot create Manticore instance on binary {}: {}".format(
-        args.binary, e))
+      args.binary, e))
     return 1
 
   m.verbosity(1)

From 35f73f24961a0cfd93e2976a1c4f89c77da95fb1 Mon Sep 17 00:00:00 2001
From: Joe Ranweiler <joe@lemma.co>
Date: Sat, 24 Feb 2018 17:06:51 -0800
Subject: [PATCH 19/19] Add KLEE support to Manticore executor

---
 bin/deepstate/main_manticore.py | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/bin/deepstate/main_manticore.py b/bin/deepstate/main_manticore.py
index bad32f8..dbab31a 100644
--- a/bin/deepstate/main_manticore.py
+++ b/bin/deepstate/main_manticore.py
@@ -309,7 +309,7 @@ def find_symbol_ea(m, name):
   return 0
 
 
-def do_run_test(state, apis, test):
+def do_run_test(state, apis, test, hook_test=False):
   """Run an individual test case."""
   state.cpu.PC = test.ea
   m = manticore.Manticore(state, sys.argv[1:])
@@ -338,23 +338,22 @@ def do_run_test(state, apis, test):
   m.add_hook(apis['ClearStream'], hook(hook_ClearStream))
   m.add_hook(apis['LogStream'], hook(hook_LogStream))
 
-  # Here we hook `DeepState_TakeOver()`, even if running unit tests.
-  # In that case, we simply will never hit this hooked function model.
-  m.add_hook(test.ea, hook(hook_TakeOver))
+  if hook_test:
+    m.add_hook(test.ea, hook(hook_TakeOver))
 
   m.subscribe('will_terminate_state', done_test)
   m.run()
 
 
-def run_test(state, apis, test):
+def run_test(state, apis, test, hook_test):
   try:
-    do_run_test(state, apis, test)
+    do_run_test(state, apis, test, hook_test)
   except:
     L.error("Uncaught exception: {}\n{}".format(
       sys.exc_info()[0], traceback.format_exc()))
 
 
-def run_tests(args, state, apis):
+def run_tests(state, apis, hook_test_ea):
   """Run all of the test cases."""
   pool = multiprocessing.Pool(processes=max(1, args.num_workers))
   results = []
@@ -395,7 +394,11 @@ def main_takeover(m, args, takeover_symbol):
   del mc
 
   fake_test = TestInfo(takeover_ea, '_takeover_test', '_takeover_file', 0)
-  m.add_hook(takeover_ea, lambda state: run_test(state, apis, fake_test))
+
+  hook_test = not args.klee
+  takeover_hook = lambda state: run_test(state, apis, fake_test, hook_test)
+  m.add_hook(takeover_ea, takeover_hook)
+
   m.run()
 
 
@@ -440,6 +443,8 @@ def main():
 
   if args.take_over:
     return main_takeover(m, args, 'DeepState_TakeOver')
+  elif args.klee:
+    return main_takeover(m, args, 'main')
   else:
     return main_unit_test(m, args)