fix undef handling in preconditions
MODIFY
ir/state.cpp
ir/state.cpp
@@ -22,20 +22,24 @@ const StateValue& State::exec(const Value &v) {
assert(undef_vars.empty());
auto val = v.toSMT(*this);
ENSURE(values_map.try_emplace(&v, (unsigned)values.size()).second);
- values.emplace_back(&v, ValTy(move(val), move(undef_vars)));
+ values.emplace_back(&v, ValTy(move(val), move(undef_vars)), false);
// cleanup potentially used temporary values due to undef rewriting
while (i_tmp_values > 0) {
tmp_values[--i_tmp_values] = StateValue();
}
- return values.back().second.first;
+ return get<1>(values.back()).first;
}
const StateValue& State::operator[](const Value &val) {
- auto &[sval, uvars] = values[values_map.at(&val)].second;
- if (uvars.empty())
+ auto &[var, val_uvars, used] = values[values_map.at(&val)];
+ auto &[sval, uvars] = val_uvars;
+ if (uvars.empty() || !used || disable_undef_rewrite) {
+ used = true;
+ undef_vars.insert(uvars.begin(), uvars.end());
return sval;
+ }
vector<pair<expr, expr>> repls;
for (auto &u : uvars) {
@@ -60,7 +64,7 @@ const StateValue& State::operator[](const Value &val) {
}
const State::ValTy& State::at(const Value &val) const {
- return values[values_map.at(&val)].second;
+ return get<1>(values[values_map.at(&val)]);
}
const expr* State::jumpCondFrom(const BasicBlock &bb) const {

MODIFY
ir/state.h
ir/state.h
#include <array>
#include <ostream>
#include <set>
+#include <tuple>
#include <unordered_map>
#include <unordered_set>
#include <utility>
@@ -31,15 +32,16 @@ public:
private:
const Function &f;
bool source;
+ bool disable_undef_rewrite = false;
smt::expr precondition = true;
smt::expr axioms = true;
const BasicBlock *current_bb;
std::set<smt::expr> quantified_vars;
- // var -> ((value, not_poison), undef_vars)
+ // var -> ((value, not_poison), undef_vars, already_used?)
std::unordered_map<const Value*, unsigned> values_map;
- std::vector<std::pair<const Value*, ValTy>> values;
+ std::vector<std::tuple<const Value*, ValTy, bool>> values;
// dst BB -> src BB -> (domain data, memory)
std::unordered_map<const BasicBlock*,
@@ -97,6 +99,8 @@ public:
auto& returnDomain() const { return return_domain; }
auto& returnVal() const { return return_val; }
+ void startParsingPre() { disable_undef_rewrite = true; }
+
// whether this is source or target program
bool isSource() const { return source; }

ADD
tests/unit/pre.opt
+Name: pre1
+Pre: WillNotOverflowSignedAdd(%x, %y)
+%r = add i4 %x, %y
+ =>
+%r = add nsw %x, %y

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -103,7 +103,8 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
s << " for " << *var;
s << "\n\nExample:\n";
- for (auto &[var, val] : src_state.getValues()) {
+ for (auto &[var, val, used] : src_state.getValues()) {
+ (void)used;
if (!dynamic_cast<const Input*>(var))
continue;
s << *var << " = ";
@@ -121,7 +122,8 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
}
}
- for (auto &[var, val] : st.getValues()) {
+ for (auto &[var, val, used] : st.getValues()) {
+ (void)used;
auto &name = var->getName();
if (name == var_name)
break;
@@ -233,6 +235,7 @@ static void check_refinement(Errors &errs, Transform &t,
expr axioms = src_state.getAxioms() && tgt_state.getAxioms();
// note that precondition->toSMT() may add stuff to getPre,
// so order here matters
+ src_state.startParsingPre();
expr pre = t.precondition ? t.precondition->toSMT(src_state) : true;
pre &= src_state.getPre() && tgt_state.getPre();
@@ -300,7 +303,8 @@ Errors TransformVerify::verify() const {
Errors errs;
if (check_each_var) {
- for (auto &[var, val] : src_state.getValues()) {
+ for (auto &[var, val, used] : src_state.getValues()) {
+ (void)used;
auto &name = var->getName();
if (name[0] != '%' || !dynamic_cast<const Instr*>(var))
continue;

fix undef handling in preconditions