[Z3] Implement API logging.

Add `-debug-z3-log-api-interaction` option to allow Z3 API calls to be
logged to a file. The files logged by this option can be replayed by the
`z3` binary (using its `-log` option). This is incredibly useful because
it allows to exactly replay Z3's behaviour outside of KLEE.

1 files changed, 24 insertions, 4 deletions

diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index a1448415..11f6193d 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -10,11 +10,12 @@
 #ifdef ENABLE_Z3
 #include "Z3Builder.h"
 
+#include "ConstantDivision.h"
 #include "klee/Expr.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Solver.h"
-#include "klee/util/Bits.h"
-#include "ConstantDivision.h"
 #include "klee/SolverStats.h"
+#include "klee/util/Bits.h"
 
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/CommandLine.h"
@@ -26,6 +27,9 @@ llvm::cl::opt<bool> UseConstructHashZ3(
     "use-construct-hash-z3",
     llvm::cl::desc("Use hash-consing during Z3 query construction."),
     llvm::cl::init(true));
+
+// FIXME: This should be std::atomic<bool>. Need C++11 for that.
+bool Z3InterationLogOpen = false;
 }
 
 namespace klee {
@@ -57,6 +61,9 @@ void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) {
   }
   llvm::errs() << "Error: Incorrect use of Z3. [" << ec << "] " << errorMsg
                << "\n";
+  // NOTE: The current implementation of `Z3_close_log()` can be safely
+  // called even if the log isn't open.
+  Z3_close_log();
   abort();
 }
 
@@ -67,8 +74,17 @@ void Z3ArrayExprHash::clear() {
   _array_hash.clear();
 }
 
-Z3Builder::Z3Builder(bool autoClearConstructCache)
-    : autoClearConstructCache(autoClearConstructCache) {
+Z3Builder::Z3Builder(bool autoClearConstructCache, const char* z3LogInteractionFileArg)
+    : autoClearConstructCache(autoClearConstructCache), z3LogInteractionFile("") {
+  if (z3LogInteractionFileArg)
+    this->z3LogInteractionFile = std::string(z3LogInteractionFileArg);
+  if (z3LogInteractionFile.length() > 0) {
+    klee_message("Logging Z3 API interaction to \"%s\"",
+                 z3LogInteractionFile.c_str());
+    assert(!Z3InterationLogOpen && "interaction log should not already be open");
+    Z3_open_log(z3LogInteractionFile.c_str());
+    Z3InterationLogOpen = true;
+  }
   // FIXME: Should probably let the client pass in a Z3_config instead
   Z3_config cfg = Z3_mk_config();
   // It is very important that we ask Z3 to let us manage memory so that
@@ -87,6 +103,10 @@ Z3Builder::~Z3Builder() {
   clearConstructCache();
   _arr_hash.clear();
   Z3_del_context(ctx);
+  if (z3LogInteractionFile.length() > 0) {
+    Z3_close_log();
+    Z3InterationLogOpen = false;
+  }
 }
 
 Z3SortHandle Z3Builder::getBvSort(unsigned width) {