Add KLEE support to Manticore executor

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)