[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.

3 files changed, 39 insertions, 8 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) {
diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h
index c41eace0..a3473f82 100644
--- a/lib/Solver/Z3Builder.h
+++ b/lib/Solver/Z3Builder.h
@@ -165,11 +165,11 @@ private:
   Z3SortHandle getBvSort(unsigned width);
   Z3SortHandle getArraySort(Z3SortHandle domainSort, Z3SortHandle rangeSort);
   bool autoClearConstructCache;
+  std::string z3LogInteractionFile;
 
 public:
   Z3_context ctx;
-
-  Z3Builder(bool autoClearConstructCache = true);
+  Z3Builder(bool autoClearConstructCache, const char *z3LogInteractionFile);
   ~Z3Builder();
 
   Z3ASTHandle getTrue();
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index c573011d..2b2e63b8 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -20,6 +20,12 @@
 #include "llvm/Support/raw_ostream.h"
 
 namespace {
+// NOTE: Very useful for debugging Z3 behaviour. These files can be given to
+// the z3 binary to replay all Z3 API calls using its `-log` option.
+llvm::cl::opt<std::string> Z3LogInteractionFile(
+    "debug-z3-log-api-interaction", llvm::cl::init(""),
+    llvm::cl::desc("Log API interaction with Z3 to the specified path"));
+
 llvm::cl::opt<std::string> Z3QueryDumpFile(
     "debug-z3-dump-queries", llvm::cl::init(""),
     llvm::cl::desc("Dump Z3's representation of the query to the specified path"));
@@ -80,8 +86,13 @@ public:
 };
 
 Z3SolverImpl::Z3SolverImpl()
-    : builder(new Z3Builder(/*autoClearConstructCache=*/false)), timeout(0.0),
-      runStatusCode(SOLVER_RUN_STATUS_FAILURE), dumpedQueriesFile(0) {
+    : builder(new Z3Builder(
+          /*autoClearConstructCache=*/false,
+          /*z3LogInteractionFileArg=*/Z3LogInteractionFile.size() > 0
+              ? Z3LogInteractionFile.c_str()
+              : NULL)),
+      timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE),
+      dumpedQueriesFile(0) {
   assert(builder && "unable to create Z3Builder");
   solverParameters = Z3_mk_params(builder->ctx);
   Z3_params_inc_ref(builder->ctx, solverParameters);