introduce per-type value refinement
refinement of floats changed to allow NaN -> something else
MODIFY
ir/type.cpp
ir/type.cpp
@@ -206,6 +206,11 @@ void VoidType::fixup(const Model &m) {
// do nothing
}
+pair<expr, expr>
+VoidType::refines(const StateValue &src, const StateValue &tgt) const {
+ UNREACHABLE();
+}
+
pair<expr, vector<expr>> VoidType::mkInput(State &s, const char *name) const {
UNREACHABLE();
}
@@ -269,6 +274,13 @@ expr IntType::enforceIntOrPtrOrVectorType() const {
return true;
}
+pair<expr, expr>
+IntType::refines(const StateValue &src, const StateValue &tgt) const {
+ return { src.non_poison.implies(tgt.non_poison),
+ // TODO: test if perf improves with && tgt.non_poison below
+ src.non_poison.implies(src.value == tgt.value) };
+}
+
pair<expr, vector<expr>> IntType::mkInput(State &s, const char *name) const {
auto var = expr::mkVar(name, bits());
return { var, { var } };
@@ -362,6 +374,14 @@ expr FloatType::enforceFloatType() const {
return true;
}
+pair<expr, expr>
+FloatType::refines(const StateValue &src, const StateValue &tgt) const {
+ return
+ { src.non_poison.implies(tgt.non_poison),
+ // TODO: test if perf improves with && tgt.non_poison below
+ (src.non_poison && !src.value.isNaN()).implies(src.value == tgt.value) };
+}
+
pair<expr, vector<expr>> FloatType::mkInput(State &s, const char *name) const {
expr var;
switch (fpType) {
@@ -374,6 +394,8 @@ pair<expr, vector<expr>> FloatType::mkInput(State &s, const char *name) const {
}
void FloatType::printVal(ostream &os, State &s, const expr &e) const {
+ e.float2BV().printHexadecimal(os);
+ os << " (";
if (e.isNaN().simplify().isTrue()) {
os << "NaN";
} else if (e.isFPZero().simplify().isTrue()) {
@@ -381,9 +403,9 @@ void FloatType::printVal(ostream &os, State &s, const expr &e) const {
} else if (e.isInf().simplify().isTrue()) {
os << (e.isFPNeg().simplify().isTrue() ? "-oo" : "+oo");
} else {
- e.float2BV().printHexadecimal(os);
- os << " (" << e.float2Real().simplify().numeral_string() << ')';
+ os << e.float2Real().simplify().numeral_string();
}
+ os << ')';
}
void FloatType::print(ostream &os) const {
@@ -454,6 +476,13 @@ expr PtrType::enforcePtrType() const {
return true;
}
+pair<expr, expr>
+PtrType::refines(const StateValue &src, const StateValue &tgt) const {
+ return { src.non_poison.implies(tgt.non_poison),
+ // TODO: test if perf improves with && tgt.non_poison below
+ src.non_poison.implies(src.value == tgt.value) };
+}
+
pair<expr, vector<expr>> PtrType::mkInput(State &s, const char *name) const {
return s.getMemory().mkInput(name);
}
@@ -605,6 +634,17 @@ expr AggregateType::enforceAggregateType(vector<Type*> *element_types) const {
return r;
}
+pair<expr, expr>
+AggregateType::refines(const StateValue &src, const StateValue &tgt) const {
+ set<expr> poison, value;
+ for (unsigned i = 0; i < elements; ++i) {
+ auto [p, v] = children[i]->refines(extract(src, i), extract(tgt, i));
+ poison.insert(p);
+ value.insert(v);
+ }
+ return { expr::mk_and(poison), expr::mk_and(value) };
+}
+
pair<expr, vector<expr>>
AggregateType::mkInput(State &s, const char *name) const {
expr val;
@@ -922,6 +962,20 @@ const StructType* SymbolicType::getAsStructType() const {
return &*s;
}
+pair<expr, expr>
+SymbolicType::refines(const StateValue &src, const StateValue &tgt) const {
+ switch (typ) {
+ case Int: return i->refines(src, tgt);
+ case Float: return f->refines(src, tgt);
+ case Ptr: return p->refines(src, tgt);
+ case Array: return a->refines(src, tgt);
+ case Vector: return v->refines(src, tgt);
+ case Struct: return s->refines(src, tgt);
+ case Undefined: UNREACHABLE();
+ }
+ UNREACHABLE();
+}
+
pair<expr, vector<expr>>
SymbolicType::mkInput(State &st, const char *name) const {
switch (typ) {

MODIFY
ir/type.h
ir/type.h
#include <optional>
#include <ostream>
#include <string>
+#include <utility>
#include <vector>
namespace smt { class Model; }
@@ -77,6 +78,10 @@ public:
virtual smt::expr fromBV(smt::expr e) const;
IR::StateValue fromBV(IR::StateValue v) const;
+ // returns pair of refinement constraints for <poison, !poison && value>
+ virtual std::pair<smt::expr, smt::expr>
+ refines(const IR::StateValue &src, const IR::StateValue &tgt) const = 0;
+
virtual std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const = 0;
virtual void printVal(std::ostream &os, State &s,
@@ -99,6 +104,8 @@ public:
smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
void fixup(const smt::Model &m) override;
+ std::pair<smt::expr, smt::expr>
+ refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -126,6 +133,8 @@ public:
smt::expr enforceIntType(unsigned bits = 0) const override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
+ std::pair<smt::expr, smt::expr>
+ refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -160,6 +169,8 @@ public:
const FloatType* getAsFloatType() const override;
smt::expr toBV(smt::expr e) const override;
smt::expr fromBV(smt::expr e) const override;
+ std::pair<smt::expr, smt::expr>
+ refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -186,6 +197,8 @@ public:
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
smt::expr enforcePtrType() const override;
+ std::pair<smt::expr, smt::expr>
+ refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -221,6 +234,8 @@ public:
void fixup(const smt::Model &m) override;
smt::expr enforceAggregateType(
std::vector<Type *> *element_types) const override;
+ std::pair<smt::expr, smt::expr>
+ refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -302,6 +317,8 @@ public:
const FloatType* getAsFloatType() const override;
const AggregateType* getAsAggregateType() const override;
const StructType* getAsStructType() const override;
+ std::pair<smt::expr, smt::expr>
+ refines(const IR::StateValue &a, const IR::StateValue &b) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -244,26 +244,18 @@ static void check_refinement(Errors &errs, Transform &t,
return;
}
- expr poison_cnstr = type.map_reduce(
- [](const StateValue &a, const StateValue &b) {
- return a.non_poison.notImplies(b.non_poison);
- }, &expr::mk_or, a, b);
-
- expr value_cnstr = type.map_reduce(
- [](const StateValue &a, const StateValue &b) {
- return a.non_poison && a.value != b.value;
- }, &expr::mk_or, a, b);
+ auto [poison_cnstr, value_cnstr] = type.refines(a, b);
Solver::check({
{ axioms && preprocess(t, qvars, uvars, pre && dom_a.notImplies(dom_b)),
[&](const Result &r) {
err(r, false, "Source is more defined than target");
}},
- { axioms && preprocess(t, qvars, uvars, pre && dom_a && poison_cnstr),
+ { axioms && preprocess(t, qvars, uvars, pre && dom_a && !poison_cnstr),
[&](const Result &r) {
err(r, true, "Target is more poisonous than source");
}},
- { axioms && preprocess(t, qvars, uvars, pre && dom_a && value_cnstr),
+ { axioms && preprocess(t, qvars, uvars, pre && dom_a && !value_cnstr),
[&](const Result &r) {
err(r, true, "Value mismatch");
}}

introduce per-type value refinement
refinement of floats changed to allow NaN -> something else