fix non-undef/poison axioms for input vars
MODIFY
ir/value.cpp
ir/value.cpp
@@ -215,6 +215,12 @@ StateValue Input::toSMT(State &s) const {
bool never_poison = config::disable_poison_input || has_byval || has_deref ||
has_nonnull || has_noundef;
+ if (never_undef) {
+ s.addAxiom(never_poison ? type == 0 : type.extract(0, 0) == 0);
+ } else if (never_poison) {
+ s.addAxiom(type.extract(1, 1) == 0);
+ }
+
// TODO: element-wise poison/undef control
return { move(val),
never_poison

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -54,9 +54,6 @@ static void print_single_varval(ostream &os, State &st, const Model &m,
if (n == 1) {
os << "undef";
return;
- } else if (n == 2) {
- os << "poison";
- return;
}
assert(n == 0);
}
@@ -293,22 +290,6 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
AndExpr axioms = src_state.getAxioms();
axioms.add(tgt_state.getAxioms());
- // restrict type variable from taking disabled values
- if (config::disable_undef_input || config::disable_poison_input) {
- for (auto &i : t.src.getInputs()) {
- if (auto in = dynamic_cast<const Input*>(&i)) {
- auto var = in->getTyVar();
- if (config::disable_undef_input) {
- if (config::disable_poison_input)
- axioms.add(var == 0);
- else
- axioms.add(var != 1);
- } else if (config::disable_poison_input)
- axioms.add(var.extract(1, 1) == 0);
- }
- }
- }
-
// note that precondition->toSMT() may add stuff to getPre,
// so order here matters
// FIXME: broken handling of transformation precondition

fix non-undef/poison axioms for input vars