TV: now working for single-BB, binops only functions
run with: opt -load=tv/tv.so -S foo.ll -tv -instcombine -tv
MODIFY
ir/function.h
ir/function.h
@@ -64,9 +64,12 @@ public:
const IR::Type& getType() const { return type ? *type : Type::voidTy; }
void setType(IR::Type &t) { type = &t; }
+ const std::string& getName() const { return name; }
+
smt::expr getTypeConstraints() const;
void fixupTypes(const smt::Model &m);
+ const BasicBlock& getFirstBB() const { return *BB_order[0]; }
BasicBlock& getBB(std::string_view name);
const BasicBlock& getBB(std::string_view name) const;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -22,7 +22,7 @@ ostream& operator<<(ostream &os, const StateValue &val) {
}
State::State(const Function &f) : f(f) {
- domain_bbs.emplace(&f.getBB(""), true);
+ domain_bbs.emplace(&f.getFirstBB(), true);
}
const StateValue& State::exec(const Value &v) {

MODIFY
tv/tv.cpp
tv/tv.cpp
#include "tools/transform.h"
#include "util/config.h"
#include "llvm/IR/Function.h"
+#include "llvm/IR/Operator.h"
#include "llvm/Pass.h"
#include "llvm/Support/raw_ostream.h"
#include <array>
@@ -19,18 +20,27 @@ using namespace IR;
using namespace tools;
using namespace util;
using namespace std;
-using llvm::cast, llvm::errs;
+using llvm::cast, llvm::dyn_cast, llvm::isa, llvm::errs;
namespace {
+#if 0
string_view s(llvm::StringRef str) {
return { str.data(), str.size() };
}
+#endif
smt::smt_initializer smt_init;
+TransformPrintOpts print_opts;
array<unique_ptr<IntType>, 65> int_types;
unordered_map<string, Function> fns;
unordered_map<const llvm::Value*, Value*> identifiers;
+Function *current_fn;
+
+// cache Value*'s names
+unordered_map<const llvm::Value*, std::string> value_names;
+unsigned value_id_counter; // for %0, %1, etc..
+
struct alive_init {
alive_init() {
@@ -42,6 +52,23 @@ struct alive_init {
}
} alive_init;
+void reset_state() {
+ identifiers.clear();
+ current_fn = nullptr;
+ value_names.clear();
+ value_id_counter = 0;
+}
+
+
+string value_name(const llvm::Value &v) {
+ auto &name = value_names[&v];
+ if (!name.empty())
+ return name;
+
+ if (!v.getName().empty())
+ return name = '%' + v.getName().str();
+ return name = '%' + to_string(value_id_counter++);
+}
Type* llvm_type2alive(const llvm::Type *ty) {
switch (ty->getTypeID()) {
@@ -58,24 +85,74 @@ Type* llvm_type2alive(const llvm::Type *ty) {
}
+Value* get_operand(llvm::Value *v) {
+ if (isa<llvm::Instruction>(v) || isa<llvm::Argument>(v))
+ return identifiers[v];
+
+ auto ty = llvm_type2alive(v->getType());
+ if (!ty)
+ return nullptr;
+
+ if (auto cnst = dyn_cast<llvm::ConstantInt>(v)) {
+ auto c = make_unique<IntConst>(*ty, cnst->getZExtValue());
+ auto ret = c.get();
+ current_fn->addConstant(move(c));
+ return ret;
+ }
+
+ if (isa<llvm::UndefValue>(v)) {
+ auto val = make_unique<UndefValue>(*ty);
+ auto ret = val.get();
+ current_fn->addUndef(move(val));
+ return ret;
+ }
+
+ return nullptr;
+}
+
+
+const unordered_map<unsigned, BinOp::Op> llvm_binop2alive = {
+#define LLVM_BINOP(x, y) { x, y },
+#include "tv/tv.h"
+#undef LLVM_BINOP
+};
+
unique_ptr<Instr> llvm_instr2alive(const llvm::Instruction &i) {
switch (i.getOpcode()) {
- case llvm::Instruction::Add:
- case llvm::Instruction::Sub:
- case llvm::Instruction::Mul:
- case llvm::Instruction::Shl:
+#define LLVM_BINOP(x, y) case x:
+#include "tv/tv.h"
+#undef LLVM_BINOP
{
auto ty = llvm_type2alive(i.getType());
- // FIXME: what about const operands?
- auto op1 = identifiers[i.getOperand(0)];
- auto op2 = identifiers[i.getOperand(1)];
+ auto op1 = get_operand(i.getOperand(0));
+ auto op2 = get_operand(i.getOperand(1));
if (!ty || !op1 || !op2)
goto err;
- // FIXME
- auto op = make_unique<BinOp>(*ty, i.getName().str(), *op1, *op2, BinOp::Add);
+
+ auto alive_op = llvm_binop2alive.at(i.getOpcode());
+
+ unsigned flags = BinOp::None;
+ if (isa<llvm::OverflowingBinaryOperator>(i) && i.hasNoSignedWrap())
+ flags |= BinOp::NSW;
+ if (isa<llvm::OverflowingBinaryOperator>(i) && i.hasNoUnsignedWrap())
+ flags |= BinOp::NUW;
+ if (isa<llvm::PossiblyExactOperator>(i) && i.isExact())
+ flags = BinOp::Exact;
+
+ auto op = make_unique<BinOp>(*ty, value_name(i), *op1, *op2, alive_op,
+ (BinOp::Flags)flags);
+
identifiers.emplace(&i, op.get());
return op;
}
+ case llvm::Instruction::Ret:
+ {
+ auto ty = llvm_type2alive(i.getType());
+ auto op = get_operand(i.getOperand(0));
+ if (!ty || !op)
+ goto err;
+ return make_unique<Return>(*ty, *op);
+ }
default:
break;
}
@@ -86,25 +163,26 @@ err:
optional<Function> llvm2alive(const llvm::Function &f) {
- identifiers.clear();
+ reset_state();
auto type = llvm_type2alive(f.getReturnType());
if (!type)
return {};
Function Fn(*type, f.getName());
+ current_fn = &Fn;
for (auto &arg : f.args()) {
auto ty = llvm_type2alive(arg.getType());
if (!ty)
return {};
- auto val = make_unique<Input>(*ty, arg.getName().str());
+ auto val = make_unique<Input>(*ty, value_name(arg));
identifiers.emplace(&arg, val.get());
Fn.addInput(move(val));
}
for (auto &bb : f) {
- auto &BB = Fn.getBB(s(bb.getName()));
+ auto &BB = Fn.getBB(value_name(bb));
for (auto &i : bb) {
if (auto I = llvm_instr2alive(i))
BB.addIntr(move(I));
@@ -120,22 +198,37 @@ optional<Function> llvm2alive(const llvm::Function &f) {
struct TVPass : public llvm::FunctionPass {
static char ID;
- //TransformPrintOpts print_opts;
bool FatalErrors = true;
TVPass() : FunctionPass(ID) {}
bool runOnFunction(llvm::Function &F) override {
auto fn = llvm2alive(F);
- if (fn)
- fn->print(cout);
+ if (!fn) {
+ fns.erase(F.getName());
+ return false;
+ }
+ auto [old_fn, inserted] = fns.try_emplace(fn->getName(), move(*fn));
+ if (inserted)
+ return false;
+
+ Transform t;
+ t.src = move(old_fn->second);
+ t.tgt = move(*fn);
+ TransformVerify verifier(t, false);
+ t.print(cout, print_opts);
- //outs() << "verifying " << F.getName() << '\n';
- if (/* !V->verify(F)*/ false && FatalErrors) {
- //errs() << "in function " << F.getName() << '\n';
- //report_fatal_error("Broken function found, compilation aborted!");
+ if (Errors errs = verifier.verify()) {
+ if (FatalErrors)
+ llvm::report_fatal_error("[Alive2] Transform doesn't verify!");
+ else
+ cout << "Transformation doesn't verify!\n\n";
+ } else {
+ cout << "Transformation seems to be correct!\n\n";
}
+
+ old_fn->second = move(t.tgt);
return false;
}

ADD
tv/tv.h
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#ifndef LLVM_BINOP
+# define LLVM_BINOP(x,y)
+#endif
+
+LLVM_BINOP(llvm::Instruction::Add, BinOp::Add)
+LLVM_BINOP(llvm::Instruction::Sub, BinOp::Sub)
+LLVM_BINOP(llvm::Instruction::Mul, BinOp::Mul)
+LLVM_BINOP(llvm::Instruction::SDiv, BinOp::SDiv)
+LLVM_BINOP(llvm::Instruction::UDiv, BinOp::UDiv)
+LLVM_BINOP(llvm::Instruction::SRem, BinOp::SRem)
+LLVM_BINOP(llvm::Instruction::URem, BinOp::URem)
+LLVM_BINOP(llvm::Instruction::Shl, BinOp::Shl)
+LLVM_BINOP(llvm::Instruction::AShr, BinOp::AShr)
+LLVM_BINOP(llvm::Instruction::LShr, BinOp::LShr)
+LLVM_BINOP(llvm::Instruction::And, BinOp::And)
+LLVM_BINOP(llvm::Instruction::Or, BinOp::Or)
+LLVM_BINOP(llvm::Instruction::Xor , BinOp::Xor)

TV: now working for single-BB, binops only functions
run with: opt -load=tv/tv.so -S foo.ll -tv -instcombine -tv