add smtllib benchmark dumping functionality
MODIFY
CMakeLists.txt
CMakeLists.txt
@@ -133,6 +133,7 @@ set(UTIL_SRCS
util/parallel_fifo.cpp
util/parallel_null.cpp
util/parallel_unrestricted.cpp
+ util/random.cpp
util/sort.cpp
util/stopwatch.cpp
util/symexec.cpp

MODIFY
smt/solver.cpp
smt/solver.cpp
#include "smt/ctx.h"
#include "util/compiler.h"
#include "util/config.h"
+#include "util/file.h"
#include <cassert>
+#include <fstream>
#include <iomanip>
#include <iostream>
#include <optional>
@@ -297,6 +299,23 @@ Result Solver::check() const {
return Result::SKIP;
}
+ if (!config::smt_benchmark_dir.empty()) {
+ const char *banner =
+ R"(Alive2 compiler optimization refinement query
+; More info in "Alive2: Bounded Translation Validation for LLVM", PLDI'21.)";
+ expr fml = assertions();
+ if (!fml.isTrue()) {
+ auto str = Z3_benchmark_to_smtlib_string(ctx(), banner, nullptr, nullptr,
+ nullptr, 0, nullptr, fml());
+ ofstream file(get_random_filename(config::smt_benchmark_dir, "smt2"));
+ if (!file.is_open()) {
+ cerr << "Alive2: Couldn't open smtlib benchmark file!" << endl;
+ exit(1);
+ }
+ file << str;
+ }
+ }
+
++num_queries;
if (print_queries)
cout << "\nSMT query:\n" << Z3_solver_to_string(ctx(), s) << endl;

MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -114,6 +114,12 @@ llvm::cl::opt<bool>
llvm::cl::desc("Alive: log interactions with the SMT solver"),
llvm::cl::cat(TVOptions), llvm::cl::init(false));
+llvm::cl::opt<string>
+ opt_smt_bench_dir("tv-smt-bench",
+ llvm::cl::desc("Alive: dump smtlib benchmarks"),
+ llvm::cl::cat(TVOptions),
+ llvm::cl::value_desc("directory"));
+
llvm::cl::opt<bool> opt_print_dot(
"tv-dot",
llvm::cl::desc("Alive: print .dot files of each function"),
@@ -496,6 +502,7 @@ struct TVLegacyPass final : public llvm::ModulePass {
smt::set_random_seed(to_string(opt_smt_random_seed));
smt::set_memory_limit(opt_max_mem * 1024 * 1024);
config::skip_smt = opt_smt_skip;
+ config::smt_benchmark_dir = opt_smt_bench_dir;
config::symexec_print_each_value = opt_se_verbose;
config::disable_undef_input = opt_disable_undef_input;

MODIFY
util/config.cpp
util/config.cpp
@@ -12,6 +12,7 @@ namespace util::config {
bool symexec_print_each_value = false;
bool skip_smt = false;
+string smt_benchmark_dir;
bool disable_poison_input = false;
bool disable_undef_input = false;
bool debug = false;

MODIFY
util/config.h
util/config.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include <string>
#include <ostream>
namespace util::config {
@@ -11,6 +12,9 @@ extern bool symexec_print_each_value;
extern bool skip_smt;
+// don't dumo if empty
+extern std::string smt_benchmark_dir;
+
extern bool disable_poison_input;
extern bool disable_undef_input;

MODIFY
util/file.cpp
util/file.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "util/file.h"
+#include "util/random.h"
#include <cstring>
+#include <filesystem>
#include <fstream>
using namespace std;
+namespace fs = std::filesystem;
namespace util {
@@ -26,4 +29,15 @@ file_reader::~file_reader() {
delete[] buf;
}
+
+string get_random_filename(const string &dir, const char *extension) {
+ // there's a low probability of race here
+ auto newname = [&]() { return get_random_str(12) + '.' + extension; };
+ fs::path path = fs::path(dir) / newname();
+ while (fs::exists(path)) {
+ path.replace_filename(newname());
+ }
+ return path;
+}
+
}

MODIFY
util/file.h
util/file.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
-#include <memory>
+#include <string>
#include <string_view>
namespace util {
@@ -23,4 +23,6 @@ public:
struct FileIOException {};
+std::string get_random_filename(const std::string &dir, const char *extension);
+
}

ADD
util/random.cpp
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "util/random.h"
+#include <random>
+
+using namespace std;
+
+static default_random_engine re;
+
+static void seed() {
+ static bool seeded = false;
+ if (!seeded) {
+ random_device rd;
+ re.seed(rd());
+ seeded = true;
+ }
+}
+
+static const char chars[] = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789";
+
+namespace util {
+
+string get_random_str(unsigned num_chars) {
+ seed();
+ uniform_int_distribution<unsigned> rand(0, sizeof(chars)-2);
+ string s;
+ for (unsigned i = 0; i < num_chars; ++i) {
+ s += chars[rand(re)];
+ }
+ return s;
+}
+
+}

ADD
util/random.h
+#pragma once
+
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include <string>
+
+namespace util {
+
+std::string get_random_str(unsigned num_chars);
+
+}

add smtllib benchmark dumping functionality