SMT: add functionality to log all interactions with Z3
MODIFY
smt/ctx.cpp
smt/ctx.cpp
@@ -39,6 +39,7 @@ void context::init() {
}
void context::destroy() {
+ Z3_close_log();
Z3_del_context(ctx);
}

MODIFY
smt/smt.cpp
smt/smt.cpp
#include "smt/smt.h"
#include "smt/ctx.h"
#include "smt/solver.h"
+#include "util/version.h"
#include <cstdint>
+#include <string>
#include <z3.h>
+using namespace util;
using namespace std;
namespace smt {
@@ -62,4 +65,10 @@ bool hit_half_memory_limit() {
return Z3_get_estimated_alloc_size() >= (z3_memory_limit / 2);
}
+void start_logging() {
+ Z3_open_log("z3_log.txt");
+ string str = string("Alive2 ") + alive_version;
+ Z3_append_log(str.c_str());
+}
+
}

MODIFY
smt/smt.h
smt/smt.h
@@ -25,4 +25,6 @@ void set_memory_limit(uint64_t limit);
bool hit_memory_limit();
bool hit_half_memory_limit();
+void start_logging();
+
}

MODIFY
tools/alive-tv.cpp
tools/alive-tv.cpp
@@ -67,6 +67,10 @@ static llvm::cl::opt<bool> opt_smt_verbose(
"smt-verbose", llvm::cl::desc("SMT verbose mode"),
llvm::cl::cat(opt_alive), llvm::cl::init(false));
+static llvm::cl::opt<bool> opt_smt_log(
+ "smt-log", llvm::cl::desc("Log interactions with the SMT solver"),
+ llvm::cl::cat(opt_alive), llvm::cl::init(false));
+
static llvm::cl::opt<bool> opt_smt_skip(
"skip-smt", llvm::cl::desc("Skip all SMT queries"),
llvm::cl::cat(opt_alive), llvm::cl::init(false));
@@ -420,6 +424,9 @@ convenient way to demonstrate an existing optimizer bug.
config::disable_poison_input = opt_disable_poison;
config::debug = opt_debug;
+ if (opt_smt_log)
+ smt::start_logging();
+
// optionally, redirect cout and cerr to user-specified file
if (!opt_outputfile.empty()) {
OutFile.open(opt_outputfile);

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -31,10 +31,12 @@ static void show_help() {
" -smt-to:x\t\tTimeout for SMT queries in ms\n"
" -max-mem:x\t\tMax memory consumption in MB (aprox)\n"
" -smt-verbose\t\tPrint all SMT queries\n"
+ " -tactic-verbose\tDebug SMT tactics\n"
+ " -smt-log\t\tLog interactions with the SMT solver\n"
" -skip-smt\t\tSkip all SMT queries\n"
" -disable-poison-input\tAssume input variables can never be poison\n"
" -disable-undef-input\tAssume input variables can never be undef\n"
- " -h / --help / -v / --version\t\tShow this help\n";
+ " -h / --help / -v / --version\tShow this help\n";
}
@@ -64,6 +66,8 @@ int main(int argc, char **argv) {
smt::solver_print_queries(true);
else if (arg == "-tactic-verbose")
smt::solver_tactic_verbose(true);
+ else if (arg == "-smt-log")
+ smt::start_logging();
else if (arg == "-skip-smt")
config::skip_smt = true;
else if (arg == "-disable-undef-input")

MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -80,6 +80,10 @@ llvm::cl::opt<bool> opt_tactic_verbose(
"tv-tactic-verbose", llvm::cl::desc("Alive: SMT Tactic verbose mode"),
llvm::cl::init(false));
+llvm::cl::opt<bool> opt_smt_log(
+ "tv-smt-log", llvm::cl::desc("Alive: log interactions with the SMT solver"),
+ llvm::cl::init(false));
+
llvm::cl::opt<bool> opt_print_dot(
"tv-dot", llvm::cl::desc("Alive: print .dot file with CFG of each function"),
llvm::cl::init(false));
@@ -266,6 +270,9 @@ struct TVPass final : public llvm::FunctionPass {
config::debug = opt_debug;
llvm_util::omit_array_size = opt_omit_array_size;
+ if (opt_smt_log)
+ smt::start_logging();
+
llvm_util_init.emplace(*out, module.getDataLayout());
smt_init.emplace();
return false;

SMT: add functionality to log all interactions with Z3 (#492)