stub transform preprocessor to remove unneeded instructions
MODIFY
ir/function.cpp
ir/function.cpp
@@ -29,6 +29,15 @@ void BasicBlock::addInstr(unique_ptr<Instr> &&i) {
m_instrs.push_back(move(i));
}
+void BasicBlock::delInstr(Instr *i) {
+ for (auto I = m_instrs.begin(), E = m_instrs.end(); I != E; ++I) {
+ if (I->get() == i) {
+ m_instrs.erase(I);
+ return;
+ }
+ }
+}
+
unique_ptr<BasicBlock> BasicBlock::dup(const string &suffix) const {
auto newbb = make_unique<BasicBlock>(name + suffix);
for (auto &i : instrs()) {
@@ -191,6 +200,17 @@ void Function::instr_iterator::operator++(void) {
next_bb();
}
+multimap<Value*, Value*> Function::getUsers() const {
+ multimap<Value*, Value*> users;
+ for (auto &i : instrs()) {
+ for (auto op : i.operands()) {
+ users.emplace(op, const_cast<Instr*>(&i));
+ }
+ }
+ // TODO: missing, e.g., global var users
+ return users;
+}
+
void Function::print(ostream &os, bool print_header) const {
{
const auto &gvars = getGlobalVars();

MODIFY
ir/function.h
ir/function.h
@@ -37,6 +37,7 @@ public:
void fixupTypes(const smt::Model &m);
void addInstr(std::unique_ptr<Instr> &&i);
+ void delInstr(Instr *i);
util::const_strip_unique_ptr<decltype(m_instrs)> instrs() const {
return m_instrs;
@@ -88,6 +89,7 @@ public:
void fixupTypes(const smt::Model &m);
const BasicBlock& getFirstBB() const { return *BB_order[0]; }
+ BasicBlock& getFirstBB() { return *BB_order[0]; }
BasicBlock& getBB(std::string_view name, bool push_front = false);
const BasicBlock& getBB(std::string_view name) const;
const BasicBlock* getBBIfExists(std::string_view name) const;
@@ -150,6 +152,8 @@ public:
instr_helper instrs() { return *this; }
instr_helper instrs() const { return *this; }
+ std::multimap<Value*, Value*> getUsers() const;
+
void print(std::ostream &os, bool print_header = true) const;
friend std::ostream &operator<<(std::ostream &os, const Function &f);
};

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -3008,6 +3008,11 @@ Value* isNoOp(const Value &v) {
if (auto gep = dynamic_cast<const GEP*>(&v))
return gep->getMaxGEPOffset() == 0 ? &gep->getPtr() : nullptr;
+ if (auto unop = dynamic_cast<const UnaryOp*>(&v)) {
+ if (unop->getOp() == UnaryOp::Copy)
+ return &unop->getValue();
+ }
+
return nullptr;
}
}

MODIFY
ir/instr.h
ir/instr.h
@@ -85,6 +85,8 @@ public:
FastMathFlags fmath = {})
: Instr(type, std::move(name)), val(&val), op(op), fmath(fmath) {}
+ Op getOp() const { return op; }
+ Value& getValue() const { return *val; }
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;
void print(std::ostream &os) const override;

MODIFY
tools/alive-tv.cpp
tools/alive-tv.cpp
@@ -273,6 +273,7 @@ static void compareFunctions(llvm::Function &F1, llvm::Function &F2,
Transform t;
t.src = move(*Func1);
t.tgt = move(*Func2);
+ t.preprocess();
TransformVerify verifier(t, false);
if (!opt_succinct)
t.print(cout, print_opts);

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -107,6 +107,7 @@ int main(int argc, char **argv) {
continue;
}
+ t.preprocess();
t.print(cout, print_opts);
cout << '\n';

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -331,7 +331,8 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
auto src_mem = src_state.returnMemory();
auto tgt_mem = tgt_state.returnMemory();
- auto [memory_cnstr0, ptr_refinement0] = src_mem.refined(tgt_mem, false);
+ // TODO: checking of constant global vars disabled
+ auto [memory_cnstr0, ptr_refinement0] = src_mem.refined(tgt_mem, true);
auto &ptr_refinement = ptr_refinement0;
auto memory_cnstr = memory_cnstr0.isTrue() ? memory_cnstr0
: value_cnstr && memory_cnstr0;
@@ -896,6 +897,69 @@ void TransformVerify::fixupTypes(const TypingAssignments &ty) {
t.tgt.fixupTypes(ty.r.getModel());
}
+void Transform::preprocess() {
+ // remove store of initializers to global variables that aren't needed to
+ // verify the transformation
+ vector<Value*> worklist;
+ set<const Value*> seen;
+
+ for (auto fn : { &src, &tgt }) {
+ auto &bb = fn->getFirstBB();
+ if (bb.getName() != "#init")
+ continue;
+
+ vector<Instr*> to_remove;
+ auto users = fn->getUsers();
+
+ for (auto &i : bb.instrs()) {
+ if (!dynamic_cast<const Store*>(&i))
+ continue;
+ auto ops = i.operands();
+ auto val = ops[0];
+ auto gvar = ops[1];
+ worklist.emplace_back(gvar);
+ seen.emplace(&i);
+
+ bool needed = false;
+ while (!worklist.empty()) {
+ auto user = worklist.back();
+ worklist.pop_back();
+ if (!seen.emplace(user).second)
+ continue;
+
+ if (user == gvar ||
+ isNoOp(*user) ||
+ dynamic_cast<Phi*>(user) ||
+ dynamic_cast<Return*>(user) ||
+ dynamic_cast<Select*>(user)) {
+ for (auto p = users.equal_range(user); p.first != p.second;
+ ++p.first)
+ worklist.emplace_back(p.first->second);
+ }
+ else if (dynamic_cast<FnCall*>(user)) {
+ // OK
+ } else {
+ needed = true;
+ break;
+ }
+ }
+
+ worklist.clear();
+ seen.clear();
+
+ if (!needed) {
+ to_remove.emplace_back(const_cast<Instr*>(&i));
+ //TODO: check src & target have same initializer
+ (void)val;
+ }
+ }
+
+ for (auto i : to_remove) {
+ bb.delInstr(i);
+ }
+ }
+}
+
void Transform::print(ostream &os, const TransformPrintOpts &opt) const {
os << "\n----------------------------------------\n";
if (!name.empty())

MODIFY
tools/transform.h
tools/transform.h
@@ -22,6 +22,7 @@ struct Transform {
IR::Function src, tgt;
IR::Predicate *precondition = nullptr;
+ void preprocess();
void print(std::ostream &os, const TransformPrintOpts &opt) const;
friend std::ostream& operator<<(std::ostream &os, const Transform &t);
};

MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -179,6 +179,7 @@ struct TVPass final : public llvm::FunctionPass {
Transform t;
t.src = move(old_fn);
t.tgt = move(I->second.first);
+ t.preprocess();
TransformVerify verifier(t, false);
t.print(*out, print_opts);

stub transform preprocessor to remove unneeded instructions