TV: add command line LLVM options to 'opt'
MODIFY
smt/smt.cpp
smt/smt.cpp
#include <cstdint>
#include <z3.h>
+using namespace std;
+
namespace smt {
smt_initializer::smt_initializer() {
@@ -35,14 +37,14 @@ void smt_initializer::destroy() {
}
-static const char *query_timeout = "10000";
+static string query_timeout = "10000";
-void set_query_timeout(const char *ms) {
- query_timeout = ms;
+void set_query_timeout(string ms) {
+ query_timeout = move(ms);
}
const char* get_query_timeout() {
- return query_timeout;
+ return query_timeout.c_str();
}

MODIFY
smt/smt.h
smt/smt.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include <string>
+
namespace smt {
struct smt_initializer {
@@ -16,7 +18,7 @@ private:
};
-void set_query_timeout(const char *ms);
+void set_query_timeout(std::string ms);
const char* get_query_timeout();
bool hit_memory_limit();

MODIFY
smt/solver.cpp
smt/solver.cpp
#include <cassert>
#include <iomanip>
#include <iostream>
+#include <optional>
#include <utility>
#include <vector>
#include <z3.h>
@@ -42,7 +43,6 @@ protected:
}
public:
- Tactic() = default;
Tactic(const char *name) : Tactic(Z3_mk_tactic(ctx(), name)) {
this->name = name;
}
@@ -72,18 +72,17 @@ class MultiTactic final : public Tactic {
Z3_goal goal = nullptr;
public:
- MultiTactic() : Tactic() {}
-
- MultiTactic(initializer_list<Tactic> ts) : Tactic("skip") {
+ MultiTactic(initializer_list<const char*> ts) : Tactic("skip") {
if (tactic_verbose) {
goal = Z3_mk_goal(ctx(), true, false, false);
Z3_goal_inc_ref(ctx(), goal);
}
for (auto I = ts.begin(), E = ts.end(); I != E; ++I) {
- *this = mkThen(*this, *I);
+ Tactic t(*I);
+ *this = mkThen(*this, t);
if (tactic_verbose)
- tactics.emplace_back(move(const_cast<Tactic&>(*I)));
+ tactics.emplace_back(move(t));
}
}
@@ -92,12 +91,6 @@ public:
Z3_goal_dec_ref(ctx(), goal);
}
- void operator=(MultiTactic &&other) {
- *this = move(static_cast<Tactic&&>(other));
- tactics = move(other.tactics);
- swap(goal, other.goal);
- }
-
void operator=(Tactic &&other) {
static_cast<Tactic&>(*this) = move(other);
}
@@ -123,7 +116,7 @@ public:
Tactic to(Z3_tactic_try_for(ctx(), t.t, 5000));
auto r = Z3_tactic_apply(ctx(), to.t, goal);
Z3_apply_result_inc_ref(ctx(), r);
- reset();
+ reset_solver();
for (unsigned i = 0, e = Z3_apply_result_get_num_subgoals(ctx(), r);
i != e; ++i) {
@@ -144,14 +137,14 @@ public:
}
}
- void reset() {
+ void reset_solver() {
if (tactic_verbose)
Z3_goal_reset(ctx(), goal);
}
};
}
-static MultiTactic tactic;
+static optional<MultiTactic> tactic;
namespace smt {
@@ -217,7 +210,7 @@ void solver_tactic_verbose(bool yes) {
}
Solver::Solver() {
- s = Z3_mk_solver_from_tactic(ctx(), tactic.t);
+ s = Z3_mk_solver_from_tactic(ctx(), tactic->t);
Z3_solver_inc_ref(ctx(), s);
}
@@ -229,7 +222,7 @@ void Solver::add(const expr &e) {
if (e.isValid()) {
auto ast = e();
Z3_solver_assert(ctx(), s, ast);
- tactic.add(ast);
+ tactic->add(ast);
} else {
valid = false;
}
@@ -250,7 +243,7 @@ SolverPop Solver::push() {
void Solver::reset() {
Z3_solver_reset(ctx(), s);
- tactic.reset();
+ tactic->reset_solver();
}
Result Solver::check() const {
@@ -268,7 +261,7 @@ Result Solver::check() const {
if (print_queries)
cout << "\nSMT query:\n" << Z3_solver_to_string(ctx(), s);
- tactic.check();
+ tactic->check();
switch (Z3_solver_check(ctx(), s)) {
case Z3_L_FALSE:
@@ -339,7 +332,7 @@ EnableSMTQueriesTMP::~EnableSMTQueriesTMP() {
void solver_init() {
- tactic = {
+ tactic.emplace({
"simplify",
"propagate-values",
"simplify",
@@ -350,11 +343,11 @@ void solver_init() {
"qe-light",
"simplify",
"smt"
- };
+ });
}
void solver_destroy() {
- tactic = MultiTactic();
+ tactic.reset();
}
}

MODIFY
tv/tv.cpp
tv/tv.cpp
#include "llvm/IR/InstVisitor.h"
#include "llvm/IR/Operator.h"
#include "llvm/Pass.h"
+#include "llvm/Support/CommandLine.h"
#include "llvm/Support/raw_ostream.h"
#include <iostream>
#include <optional>
@@ -25,13 +26,37 @@ using llvm::LLVMContext;
namespace {
+llvm::cl::opt<unsigned> opt_smt_to(
+ "tv-smt-to", llvm::cl::desc("Alive: timeout for SMT queries"),
+ llvm::cl::init(1000), llvm::cl::value_desc("ms"));
+
+llvm::cl::opt<bool> opt_se_verbose(
+ "tv-se-verbose", llvm::cl::desc("Alive: symbolic execution verbose mode"),
+ llvm::cl::init(false));
+
+llvm::cl::opt<bool> opt_smt_stats(
+ "tv-smt-stats", llvm::cl::desc("Alive: show SMT statistics"),
+ llvm::cl::init(false));
+
+llvm::cl::opt<bool> opt_smt_skip(
+ "tv-smt-skip", llvm::cl::desc("Alive: skip SMT queries"),
+ llvm::cl::init(false));
+
+llvm::cl::opt<bool> opt_smt_verbose(
+ "tv-smt-verbose", llvm::cl::desc("Alive: SMT verbose mode"),
+ llvm::cl::init(false));
+
+llvm::cl::opt<bool> opt_tactic_verbose(
+ "tv-tactic-verbose", llvm::cl::desc("Alive: SMT Tactic verbose mode"),
+ llvm::cl::init(false));
+
#if 0
string_view s(llvm::StringRef str) {
return { str.data(), str.size() };
}
#endif
-smt::smt_initializer smt_init;
+optional<smt::smt_initializer> smt_init;
TransformPrintOpts print_opts;
vector<unique_ptr<IntType>> int_types;
unordered_map<string, Function> fns;
@@ -485,7 +510,7 @@ struct TVPass : public llvm::FunctionPass {
if (inserted)
return false;
- smt_init.reset();
+ smt_init->reset();
Transform t;
t.src = move(old_fn->second);
t.tgt = move(*fn);
@@ -504,8 +529,29 @@ struct TVPass : public llvm::FunctionPass {
return false;
}
+ bool doInitialization(llvm::Module&) override {
+ static bool done = false;
+ if (done)
+ return false;
+ done = true;
+
+ smt::solver_print_queries(opt_smt_verbose);
+ smt::solver_tactic_verbose(opt_tactic_verbose);
+ smt::set_query_timeout(to_string(opt_smt_to));
+ config::skip_smt = opt_smt_skip;
+ config::symexec_print_each_value = opt_se_verbose;
+
+ smt_init.emplace();
+ return false;
+ }
+
bool doFinalization(llvm::Module&) override {
+ static bool showed_stats = false;
+ if (opt_smt_stats && !showed_stats) {
smt::solver_print_stats(cerr);
+ showed_stats = true;
+ }
+ smt_init.reset();
return false;
}

TV: add command line LLVM options to 'opt'