make alive-exec work for very simple IRs
MODIFY
tools/alive-exec.cpp
tools/alive-exec.cpp
#include "llvm_util/llvm2alive.h"
#include "ir/memory.h"
+#include "smt/expr.h"
#include "smt/smt.h"
+#include "smt/solver.h"
#include "tools/transform.h"
#include "util/config.h"
#include "util/version.h"
#include <iostream>
#include <utility>
+using namespace llvm_util;
+using namespace smt;
using namespace tools;
using namespace util;
using namespace std;
-using namespace llvm_util;
static llvm::cl::OptionCategory opt_alive("Alive options");
@@ -81,14 +84,9 @@ static llvm::cl::list<std::string> opt_funcs(
llvm::cl::ZeroOrMore, llvm::cl::value_desc("function name"),
llvm::cl::CommaSeparated, llvm::cl::cat(opt_alive));
-static llvm::cl::opt<unsigned> opt_src_unrolling_factor(
- "src-unroll",
- llvm::cl::desc("Unrolling factor for src function (default=0)"),
- llvm::cl::cat(opt_alive), llvm::cl::init(0));
-
-static llvm::cl::opt<unsigned> opt_tgt_unrolling_factor(
- "tgt-unroll",
- llvm::cl::desc("Unrolling factor for tgt function (default=0)"),
+static llvm::cl::opt<unsigned> opt_unrolling_factor(
+ "unroll",
+ llvm::cl::desc("Unrolling factor (default=0)"),
llvm::cl::cat(opt_alive), llvm::cl::init(0));
static llvm::cl::opt<bool> opt_tactic_verbose(
@@ -150,25 +148,98 @@ static std::unique_ptr<llvm::Module> openInputFile(llvm::LLVMContext &Context,
static optional<smt::smt_initializer> smt_init;
-static void execFunction(llvm::Function &F, llvm::Triple &targetTriple,
+static void execFunction(llvm::Function &F, llvm::Triple &triple,
unsigned &successCount, unsigned &errorCount) {
- omit_array_size = opt_omit_array_size;
-
- auto Func = llvm2alive(F, llvm::TargetLibraryInfoWrapperPass(targetTriple)
- .getTLI(F));
+ auto Func = llvm2alive(F,
+ llvm::TargetLibraryInfoWrapperPass(triple).getTLI(F));
if (!Func) {
cerr << "ERROR: Could not translate '" << F.getName().str()
<< "' to Alive IR\n";
++errorCount;
return;
}
- Func->unroll(opt_src_unrolling_factor);
+ Func->unroll(opt_unrolling_factor);
- smt_init->reset();
+ Transform t;
+ t.src = move(*Func);
+ t.tgt = *llvm2alive(F,
+ llvm::TargetLibraryInfoWrapperPass(triple).getTLI(F));
+ t.preprocess();
+ TransformVerify verifier(t, false);
+ if (!opt_succinct)
+ t.src.print(cout << "\n----------------------------------------\n");
- // FIXME Nuno add execution logic here
- cout << "executing: " << F.getName().str() << "\n";
+ {
+ auto types = verifier.getTypings();
+ if (!types) {
+ cerr << "Transformation doesn't verify!\n"
+ "ERROR: program doesn't type check!\n\n";
+ ++errorCount;
+ return;
+ }
+ assert(types.hasSingleTyping());
+ }
+
+ smt_init->reset();
+ try {
+ auto p = verifier.exec();
+ auto &state = p.first;
+
+ auto ret_domain = state.returnDomain()();
+ auto [ret_val, ret_undefs] = state.returnVal();
+ auto ret = expr::mkVar("ret_val", ret_val.value);
+ auto ret_np = expr::mkVar("ret_np", ret_val.non_poison);
+
+ Solver s;
+ s.add(ret_domain);
+ s.add(ret == ret_val.value);
+ s.add(ret_np == ret_val.non_poison);
+ auto r = s.check();
+ if (r.isUnsat()) {
+ cout << "ERROR: Function doesn't reach a return statement\n";
+ ++errorCount;
+ return;
+ }
+ if (r.isInvalid()) {
+ cout << "ERROR: invalid expression\n";
+ ++errorCount;
+ return;
+ }
+ if (r.isError()) {
+ cout << "ERROR: Error in SMT solver: " << r.getReason() << '\n';
+ ++errorCount;
+ return;
+ }
+ if (r.isTimeout()) {
+ cout << "ERROR: SMT solver timedout\n";
+ ++errorCount;
+ return;
+ }
+ if (r.isSkip()) {
+ cout << "ERROR: SMT queries disabled";
+ ++errorCount;
+ return;
+ }
+ if (r.isSat()) {
+ auto &m = r.getModel();
+ cout << "Return value: ";
+ // TODO: add support for aggregates
+ if (m[ret_np].isFalse()) {
+ cout << "poison\n\n";
+ } else {
+ t.src.getType().printVal(cout, state, m[ret]);
+ cout << "\n\n";
+ }
++successCount;
+ return;
+ }
+ UNREACHABLE();
+
+ } catch (const AliveException &e) {
+ cout << "ERROR: " << e.msg << '\n';
+ ++errorCount;
+ return;
+ }
}
static ofstream OutFile;
@@ -235,6 +306,7 @@ will attempt to execute every function in the bitcode file.
auto targetTriple = llvm::Triple(M.get()->getTargetTriple());
llvm_util::initializer llvm_util_init(cerr, DL);
+ omit_array_size = opt_omit_array_size;
smt_init.emplace();
unsigned successCount = 0, errorCount = 0;

MODIFY
tools/alive-tv.cpp
tools/alive-tv.cpp
@@ -283,8 +283,6 @@ static void compareFunctions(llvm::Function &F1, llvm::Function &F2,
TransformPrintOpts print_opts;
- omit_array_size = opt_omit_array_size;
-
auto Func1 = llvm2alive(F1, llvm::TargetLibraryInfoWrapperPass(targetTriple)
.getTLI(F1));
if (!Func1) {
@@ -461,6 +459,7 @@ convenient way to demonstrate an existing optimizer bug.
auto targetTriple = llvm::Triple(M1.get()->getTargetTriple());
llvm_util::initializer llvm_util_init(cerr, DL);
+ omit_array_size = opt_omit_array_size;
smt_init.emplace();
unsigned goodCount = 0, badCount = 0, errorCount = 0;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -883,6 +883,25 @@ TransformVerify::TransformVerify(Transform &t, bool check_each_var) :
}
}
+pair<State, State> TransformVerify::exec() const {
+ StopWatch symexec_watch;
+ t.tgt.syncDataWithSrc(t.src);
+ calculateAndInitConstants(t);
+ State::resetGlobals();
+
+ State src_state(t.src, true), tgt_state(t.tgt, false);
+ sym_exec(src_state);
+ tgt_state.syncSEdataWithSrc(src_state);
+ sym_exec(tgt_state);
+ src_state.mkAxioms(tgt_state);
+
+ symexec_watch.stop();
+ if (symexec_watch.seconds() > 5) {
+ cerr << "WARNING: slow vcgen! Took " << symexec_watch << '\n';
+ }
+ return { move(src_state), move(tgt_state) };
+}
+
Errors TransformVerify::verify() const {
if (t.src.getFnAttrs() != t.tgt.getFnAttrs() ||
!t.src.hasSameInputs(t.tgt)) {
@@ -890,12 +909,6 @@ Errors TransformVerify::verify() const {
"between src and tgt", false };
}
- try {
- t.tgt.syncDataWithSrc(t.src);
- } catch (AliveException &ae) {
- return Errors(move(ae));
- }
-
// Check sizes of global variables
auto globals_tgt = t.tgt.getGlobalVars();
auto globals_src = t.src.getGlobalVars();
@@ -926,26 +939,9 @@ Errors TransformVerify::verify() const {
}
}
- StopWatch symexec_watch;
- calculateAndInitConstants(t);
- State::resetGlobals();
- State src_state(t.src, true), tgt_state(t.tgt, false);
-
- try {
- sym_exec(src_state);
- tgt_state.syncSEdataWithSrc(src_state);
- sym_exec(tgt_state);
- src_state.mkAxioms(tgt_state);
- } catch (AliveException e) {
- return move(e);
- }
-
- symexec_watch.stop();
- if (symexec_watch.seconds() > 5) {
- cerr << "WARNING: slow vcgen! Took " << symexec_watch << '\n';
- }
-
Errors errs;
+ try {
+ auto [src_state, tgt_state] = exec();
if (check_each_var) {
for (auto &[var, val, used] : src_state.getValues()) {
@@ -970,7 +966,9 @@ Errors TransformVerify::verify() const {
tgt_state.returnDomain()(), tgt_state.functionDomain()(),
tgt_state.returnVal(),
check_each_var);
-
+ } catch (AliveException e) {
+ return move(e);
+ }
return errs;
}

MODIFY
tools/transform.h
tools/transform.h
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/function.h"
+#include "ir/state.h"
#include "smt/solver.h"
#include "util/errors.h"
#include <string>
@@ -52,6 +53,7 @@ class TransformVerify {
public:
TransformVerify(Transform &t, bool check_each_var);
+ std::pair<IR::State, IR::State> exec() const;
util::Errors verify() const;
TypingAssignments getTypings() const;
void fixupTypes(const TypingAssignments &ty);

make alive-exec work for very simple IRs