preprocess: only remove initializers when possible to remove forom both transforms
this allows memories to remain syntactically equal
MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -107,7 +107,6 @@ int main(int argc, char **argv) {
continue;
}
- t.preprocess();
t.print(cout, print_opts);
cout << '\n';

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -331,8 +331,7 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
auto src_mem = src_state.returnMemory();
auto tgt_mem = tgt_state.returnMemory();
- // TODO: checking of constant global vars disabled
- auto [memory_cnstr0, ptr_refinement0] = src_mem.refined(tgt_mem, true);
+ auto [memory_cnstr0, ptr_refinement0] = src_mem.refined(tgt_mem, false);
auto &ptr_refinement = ptr_refinement0;
auto memory_cnstr = memory_cnstr0.isTrue() ? memory_cnstr0
: value_cnstr && memory_cnstr0;
@@ -897,31 +896,25 @@ 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;
- vector<Instr*> to_remove;
- set<const Value*> seen;
-
- for (auto fn : { &src, &tgt }) {
- auto &bb = fn->getFirstBB();
+static map<string_view, Instr*> can_remove_init(Function &fn) {
+ map<string_view, Instr*> to_remove;
+ auto &bb = fn.getFirstBB();
if (bb.getName() != "#init")
- continue;
+ return to_remove;
- auto users = fn->getUsers();
+ vector<Value*> worklist;
+ set<const Value*> seen;
+ 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];
+ auto gvar = i.operands()[1];
worklist.emplace_back(gvar);
seen.emplace(&i);
bool needed = false;
- while (!worklist.empty()) {
+ do {
auto user = worklist.back();
worklist.pop_back();
if (!seen.emplace(user).second)
@@ -931,8 +924,7 @@ void Transform::preprocess() {
isNoOp(*user) ||
dynamic_cast<Phi*>(user) ||
dynamic_cast<Select*>(user)) {
- for (auto p = users.equal_range(user); p.first != p.second;
- ++p.first)
+ 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) ||
@@ -942,26 +934,38 @@ void Transform::preprocess() {
needed = true;
break;
}
- }
+ } while (!worklist.empty());
worklist.clear();
seen.clear();
- if (!needed) {
- to_remove.emplace_back(const_cast<Instr*>(&i));
- //TODO: check src & target have same initializer
- (void)val;
+ if (!needed)
+ to_remove.emplace(gvar->getName(), const_cast<Instr*>(&i));
}
+ return to_remove;
}
- for (auto i : to_remove) {
- bb.delInstr(i);
+void Transform::preprocess() {
+ // remove store of initializers to global variables that aren't needed to
+ // verify the transformation
+ // We only remove inits if it's possible to remove from both programs to keep
+ // memories syntactically equal
+ auto remove_init_tgt = can_remove_init(tgt);
+ for (auto &[name, isrc] : can_remove_init(src)) {
+ auto Itgt = remove_init_tgt.find(name);
+ if (Itgt == remove_init_tgt.end())
+ continue;
+ src.getFirstBB().delInstr(isrc);
+ tgt.getFirstBB().delInstr(Itgt->second);
+ // TODO: check that tgt init refines that of src
}
- to_remove.clear();
+ // remove side-effect free instructions without users
+ vector<Instr*> to_remove;
+ for (auto fn : { &src, &tgt }) {
bool changed;
do {
- users = fn->getUsers();
+ auto users = fn->getUsers();
changed = false;
for (auto bb : fn->getBBs()) {

preprocess: only remove initializers when possible to remove forom both transforms
this allows memories to remain syntactically equal