introduce AggregateType and do a big code refactoring
further testing undergoing
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -82,16 +82,14 @@ AggregateConst::AggregateConst(Type &type, vector<Value*> &&vals)
: Constant(type, agg_const_str(vals)), vals(move(vals)) {}
StateValue AggregateConst::toSMT(State &s) const {
- expr v;
+ StateValue v;
bool first = true;
for (auto val : vals) {
- auto [vv, vnp] = val->toSMT(s);
- assert(vnp.isTrue());
- vv = val->getType().toBV(vv);
- v = first ? vv : v.concat(vv);
+ auto vv = val->getType().toBV(val->toSMT(s));
+ v = first ? move(vv) : v.concat(vv);
first = false;
}
- return { move(v), true };
+ return v;
}
pair<expr, expr> AggregateConst::toSMT_cnst() const {

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -153,6 +153,16 @@ static expr fm_poison(const expr &a, const expr &b, const expr &val,
return ret;
}
+static expr mk_poison_agg(expr &poison, unsigned agg_size) {
+ assert(agg_size > 0);
+ expr p = poison.toBVBool();
+ expr r = p;
+ for (unsigned i = 1; i != agg_size; ++i) {
+ r = r.concat(p);
+ }
+ return r;
+}
+
StateValue BinOp::toSMT(State &s) const {
auto &[a, ap] = s[*lhs];
auto &[b, bp] = s[*rhs];
@@ -278,31 +288,37 @@ StateValue BinOp::toSMT(State &s) const {
case SAdd_Overflow:
val = a + b;
val = val.concat((!a.add_no_soverflow(b)).toBVBool());
+ not_poison = mk_poison_agg(not_poison, 2);
break;
case UAdd_Overflow:
val = a + b;
val = val.concat((!a.add_no_uoverflow(b)).toBVBool());
+ not_poison = mk_poison_agg(not_poison, 2);
break;
case SSub_Overflow:
val = a - b;
val = val.concat((!a.sub_no_soverflow(b)).toBVBool());
+ not_poison = mk_poison_agg(not_poison, 2);
break;
case USub_Overflow:
val = a - b;
val = val.concat((!a.sub_no_uoverflow(b)).toBVBool());
+ not_poison = mk_poison_agg(not_poison, 2);
break;
case SMul_Overflow:
val = a * b;
val = val.concat((!a.mul_no_soverflow(b)).toBVBool());
+ not_poison = mk_poison_agg(not_poison, 2);
break;
case UMul_Overflow:
val = a * b;
val = val.concat((!a.mul_no_uoverflow(b)).toBVBool());
+ not_poison = mk_poison_agg(not_poison, 2);
break;
case FAdd:
@@ -664,37 +680,34 @@ void ExtractValue::print(ostream &os) const {
}
StateValue ExtractValue::toSMT(State &s) const {
- auto [v, p] = s[*val];
+ auto v = s[*val];
- // TODO: add support for array type
Type *type = &val->getType();
for (auto idx : idxs) {
- auto st = type->getAsStructType();
- v = st->extract(v, idx);
- type = &st->getChild(idx);
+ auto ty = type->getAsAggregateType();
+ v = ty->extract(v, idx);
+ type = &ty->getChild(idx);
}
-
- return { move(v), move(p) };
+ return v;
}
expr ExtractValue::getTypeConstraints(const Function &f) const {
auto c = Value::getTypeConstraints() &&
val->getType().enforceAggregateType();
- // TODO: add support for arrays
Type *type = &val->getType();
unsigned i = 0;
for (auto idx : idxs) {
- auto st = type->getAsStructType();
- if (!st) {
+ auto ty = type->getAsAggregateType();
+ if (!ty) {
c = false;
break;
}
- type = &st->getChild(idx);
+ type = &ty->getChild(idx);
- c &= st->numElements().ugt(idx);
+ c &= ty->numElements().ugt(idx);
if (++i == idxs.size())
- c &= st->getChild(idx) == getType();
+ c &= ty->getChild(idx) == getType();
}
return c;
}

MODIFY
ir/state_value.cpp
ir/state_value.cpp
@@ -14,6 +14,10 @@ StateValue StateValue::mkIf(const expr &cond, const StateValue &then,
expr::mkIf(cond, then.non_poison, els.non_poison) };
}
+StateValue StateValue::concat(const StateValue &other) const {
+ return { value.concat(other.value), non_poison.concat(other.non_poison) };
+}
+
bool StateValue::eq(const StateValue &other) const {
return value.eq(other.value) && non_poison.eq(other.non_poison);
}

MODIFY
ir/state_value.h
ir/state_value.h
@@ -20,6 +20,7 @@ struct StateValue {
static StateValue mkIf(const smt::expr &cond, const StateValue &then,
const StateValue &els);
+ StateValue concat(const StateValue &other) const;
smt::expr both() const { return value && non_poison; }
bool eq(const StateValue &other) const;

MODIFY
ir/type.cpp
ir/type.cpp
@@ -142,18 +142,40 @@ expr Type::enforceFloatType() const {
return false;
}
-const StructType* Type::getAsStructType() const {
+const FloatType* Type::getAsFloatType() const {
return nullptr;
}
-const FloatType* Type::getAsFloatType() const {
+const AggregateType* Type::getAsAggregateType() const {
+ return nullptr;
+}
+
+const StructType* Type::getAsStructType() const {
return nullptr;
}
+expr Type::map_reduce(expr(*map)(const StateValue&, const StateValue&),
+ expr(*reduce)(const set<expr> &),
+ const StateValue &a, const StateValue &b) const {
+ return map(a, b);
+}
+
expr Type::toBV(expr e) const {
return e;
}
+StateValue Type::toBV(StateValue v) const {
+ return { toBV(v.value), v.non_poison.toBVBool() };
+}
+
+expr Type::fromBV(expr e) const {
+ return e;
+}
+
+StateValue Type::fromBV(StateValue v) const {
+ return { fromBV(v.value), v.non_poison == 1 };
+}
+
ostream& operator<<(ostream &os, const Type &t) {
t.print(os);
return os;
@@ -291,6 +313,10 @@ expr FloatType::toBV(expr e) const {
return e.float2BV();
}
+expr FloatType::fromBV(expr e) const {
+ return e.BV2float(getDummyValue());
+}
+
expr FloatType::sizeVar() const {
return defined ? expr::mkUInt(getFpType(), var_bw_bits) : Type::sizeVar();
}
@@ -449,313 +475,252 @@ void PtrType::print(ostream &os) const {
}
-unsigned ArrayType::bits() const {
- // TODO
- return 0;
-}
-
-expr ArrayType::getDummyValue() const {
- // TODO
- return {};
-}
-
-expr ArrayType::getTypeConstraints() const {
- // TODO
- return false;
-}
-
-expr ArrayType::operator==(const ArrayType &rhs) const {
- // TODO
- return false;
-}
-
-expr ArrayType::sameType(const ArrayType &rhs) const {
- // TODO
- return false;
-}
+AggregateType::AggregateType(string &&name, bool symbolic)
+ : Type(string(name)) {
+ if (!symbolic)
+ return;
-void ArrayType::fixup(const Model &m) {
- // TODO
-}
+ // create symbolic type with a finite number of children
+ unsigned num = 4;
+ sym.resize(num);
+ children.resize(num);
-expr ArrayType::enforceAggregateType(vector<Type*> *element_types) const {
- // TODO
- return true;
+ // FIXME: limitation below is for vectors; what about structs and arrays?
+ for (unsigned i = 0; i < num; ++i) {
+ sym[i] = make_unique<SymbolicType>("v_" + name,
+ (1 << SymbolicType::Int) |
+ (1 << SymbolicType::Float) |
+ (1 << SymbolicType::Ptr));
+ children[i] = sym[i].get();
}
-
-pair<expr, vector<expr>> ArrayType::mkInput(State &s, const char *name) const {
- // TODO
- return {};
}
-void ArrayType::printVal(ostream &os, State &s, const expr &e) const {
- // TODO
+expr AggregateType::numElements() const {
+ return defined ? expr::mkUInt(elements, var_vector_elements) :
+ var("elements", var_vector_elements);
}
-void ArrayType::print(ostream &os) const {
- os << "TODO";
+StateValue AggregateType::extract(const StateValue &val, unsigned index) const {
+ unsigned total_till_now = 0;
+ for (unsigned i = 0; i < index; ++i) {
+ total_till_now += children[i]->bits();
}
+ unsigned high = val.value.bits() - total_till_now;
+ unsigned poison_idx = children.size() - index - 1;
-
-VectorType::VectorType(string &&name, unsigned elements, Type &elementTy)
- : Type(move(name)), elementTy(elementTy), elements(elements), defined(true) {
- assert(elements != 0);
+ return children[index]->fromBV({
+ val.value.extract(high - 1, high - children[index]->bits()),
+ val.non_poison.extract(poison_idx, poison_idx) });
}
-VectorType::VectorType(string &&name)
- : Type(string(name)),
- sym(make_unique<SymbolicType>("v_" + name, (1 << SymbolicType::Int) |
- (1 << SymbolicType::Float) |
- (1 << SymbolicType::Ptr))),
- elementTy(*sym.get()), elements(0) {}
-
-expr VectorType::numElements() const {
- return defined ? expr::mkUInt(elements, var_vector_elements) :
- var("elements", var_vector_elements);
+StateValue AggregateType::extract(const StateValue &val,
+ const expr &index) const {
+ auto &elementTy = *children[0];
+ for (unsigned i = 1; i < elements; ++i) {
+ assert(elementTy.bits() == children[i]->bits());
}
-
-expr VectorType::extract(const expr &val, const expr &index) const {
unsigned bw_elem = elementTy.bits();
- unsigned bw_val = val.bits();
- expr v = val << (index.zextOrTrunc(bw_val) * expr::mkUInt(bw_elem, bw_val));
- v = v.extract(elements * bw_elem - 1, (elements - 1) * bw_elem);
- return elementTy.isFloatType() ? v.BV2float(elementTy.getDummyValue()) : v;
+ unsigned bw_val = val.value.bits();
+ expr idx = index.zextOrTrunc(bw_val);
+ expr v = val.value << (idx * expr::mkUInt(bw_elem, bw_val));
+ return elementTy.fromBV({
+ v.extract(elements * bw_elem - 1, (elements - 1) * bw_elem),
+ (val.non_poison << idx).extract(elements-1, elements-1) });
}
-unsigned VectorType::bits() const {
- return elements * elementTy.bits();
+unsigned AggregateType::bits() const {
+ unsigned bw = 0;
+ for (unsigned i = 0; i < elements; ++i) {
+ bw += children[i]->bits();
+ }
+ return bw;
}
-expr VectorType::getDummyValue() const {
- expr element = elementTy.toBV(elementTy.getDummyValue());
+expr AggregateType::getDummyValue() const {
+ if (elements == 0)
+ return expr::mkUInt(0, 1);
- expr ret = element;
- for (unsigned i = 1; i < elements; ++i) {
- ret = ret.concat(element);
+ expr ret;
+ for (unsigned i = 0; i < elements; ++i) {
+ auto v = children[i]->toBV(children[i]->getDummyValue());
+ ret = i == 0 ? move(v) : ret.concat(v);
}
return ret;
}
-expr VectorType::getTypeConstraints() const {
- expr elems = numElements();
- expr r = elementTy.getTypeConstraints() &&
- (elementTy.enforceIntType() ||
- elementTy.enforceFloatType() ||
- elementTy.enforcePtrType()) &&
- elems != 0;
+expr AggregateType::getTypeConstraints() const {
+ expr r(true), elems = numElements();
+ for (unsigned i = 0, e = children.size(); i != e; ++i) {
+ r &= elems.ugt(i).implies(children[i]->getTypeConstraints());
+ }
if (!defined)
r &= elems.ule(4);
return r;
}
-expr VectorType::operator==(const VectorType &rhs) const {
- return numElements() == rhs.numElements() && elementTy == rhs.elementTy;
+expr AggregateType::operator==(const AggregateType &rhs) const {
+ expr elems = numElements();
+ expr res = elems == rhs.numElements();
+ for (unsigned i = 0, e = min(children.size(), rhs.children.size());
+ i != e; ++i) {
+ res &= elems.ugt(i).implies(*children[i] == *rhs.children[i]);
+ }
+ return res;
}
-expr VectorType::sameType(const VectorType &rhs) const {
- return numElements() == rhs.numElements() &&
- elementTy.sameType(rhs.elementTy);
+expr AggregateType::sameType(const AggregateType &rhs) const {
+ expr elems = numElements();
+ expr res = elems == rhs.numElements();
+ for (unsigned i = 0, e = min(children.size(), rhs.children.size());
+ i != e; ++i) {
+ res &= elems.ugt(i).implies(children[i]->sameType(*rhs.children[i]));
+ }
+ return res;
}
-void VectorType::fixup(const Model &m) {
- elementTy.fixup(m);
+void AggregateType::fixup(const Model &m) {
if (!defined)
elements = m.getUInt(numElements());
-}
-expr VectorType::enforceIntOrVectorType() const {
- return elementTy.enforceIntType();
+ for (unsigned i = 0; i < elements; ++i) {
+ children[i]->fixup(m);
}
-
-expr VectorType::enforceIntOrPtrOrVectorType() const {
- return elementTy.enforceIntOrPtrType();
}
-expr VectorType::enforceAggregateType(vector<Type*> *element_types) const {
+expr AggregateType::enforceAggregateType(vector<Type*> *element_types) const {
if (!element_types)
return true;
+ if (children.size() < element_types->size())
+ return false;
+
expr r = numElements() == element_types->size();
- for (auto ty : *element_types) {
- r &= *ty == elementTy;
+ for (unsigned i = 0, e = element_types->size(); i != e; ++i) {
+ r &= *children[i] == *(*element_types)[i];
}
return r;
}
-pair<expr, vector<expr>> VectorType::mkInput(State &s, const char *name) const {
+pair<expr, vector<expr>>
+ AggregateType::mkInput(State &s, const char *name) const {
expr val;
- vector<expr> vect;
+ vector<expr> vars;
for (unsigned i = 0; i < elements; ++i) {
- auto name_i = string(name) + '#' + to_string(i);
- auto [val_i, vect_i] = elementTy.mkInput(s, name_i.c_str());
- vect.insert(vect.end(), vect_i.begin(), vect_i.end());
-
- val_i = elementTy.toBV(val_i);
- val = i == 0 ? move(val_i) : val.concat(val_i);
+ string c_name = string(name) + "#" + to_string(i);
+ auto [v, vs] = children[i]->mkInput(s, c_name.c_str());
+ v = children[i]->toBV(v);
+ val = i == 0 ? move(v) : val.concat(v);
+ vars.insert(vars.end(), vs.begin(), vs.end());
}
- return { move(val), move(vect) };
+ return { move(val), move(vars) };
}
-void VectorType::printVal(ostream &os, State &s, const expr &e) const {
- os << '<';
+void AggregateType::printVal(ostream &os, State &s, const expr &e) const {
+ os << (dynamic_cast<const StructType*>(this) ? "{ " : "< ");
+ // FIXME: poison
+ auto tmp_e = StateValue(expr(e), expr::mkUInt(0, elements));
for (unsigned i = 0; i < elements; ++i) {
if (i != 0)
os << ", ";
- elementTy.printVal(os, s, extract(e, expr::mkUInt(i, 8)).simplify());
+ children[i]->printVal(os, s, extract(tmp_e, i).value.simplify());
}
- os << '>';
+ os << (dynamic_cast<const StructType*>(this) ? " }" : " >");
}
-void VectorType::print(ostream &os) const {
- if (elements)
- os << '<' << elements << " x " << elementTy << '>';
+const AggregateType* AggregateType::getAsAggregateType() const {
+ return this;
}
-
-unsigned StructType::bits() const {
- unsigned res = 0;
- for (auto c : children) {
- res += c->bits();
+expr AggregateType::map_reduce(expr(*map)(const StateValue&, const StateValue&),
+ expr(*reduce)(const set<expr>&),
+ const StateValue &a, const StateValue &b) const {
+ set<expr> r;
+ for (unsigned i = 0; i < elements; ++i) {
+ r.insert(map(extract(a, i), extract(b, i)));
}
- return res;
+ return reduce(r);
}
-expr StructType::getDummyValue() const {
- if (children.empty())
- return expr::mkUInt(0, 1);
- expr res;
- bool first = true;
- for (auto c : children) {
- if (first) {
- res = c->getDummyValue();
- first = false;
- } else {
- res = res.concat(c->getDummyValue());
- }
- }
- return res;
+expr ArrayType::getTypeConstraints() const {
+ // TODO
+ return false;
}
-expr StructType::getTypeConstraints() const {
- expr res(true);
- for (auto c : children) {
- res &= c->getTypeConstraints();
- }
- return res;
+void ArrayType::print(ostream &os) const {
+ os << "TODO";
}
-expr StructType::operator==(const StructType &rhs) const {
- if (children.size() != rhs.children.size())
- return false;
- expr res(true);
- for (unsigned i = 0, e = children.size(); i != e; ++i) {
- res &= *children[i] == *rhs.children[i];
+VectorType::VectorType(string &&name, unsigned elements, Type &elementTy)
+ : AggregateType(move(name), false) {
+ assert(elements != 0);
+ this->elements = elements;
+ defined = true;
+
+ for (unsigned i = 0; i < elements; ++i) {
+ children.emplace_back(&elementTy);
}
- return res;
}
-expr StructType::sameType(const StructType &rhs) const {
- if (children.size() != rhs.children.size())
- return false;
+expr VectorType::getTypeConstraints() const {
+ auto &elementTy = *children[0];
+ expr r = AggregateType::getTypeConstraints() &&
+ (elementTy.enforceIntType() ||
+ elementTy.enforceFloatType() ||
+ elementTy.enforcePtrType()) &&
+ numElements() != 0;
- expr res(true);
- for (unsigned i = 0, e = children.size(); i != e; ++i) {
- res &= children[i]->sameType(*rhs.children[i]);
- }
- return res;
+ // all elements have the same type
+ for (unsigned i = 1, e = children.size(); i != e; ++i) {
+ r &= numElements().ugt(i).implies(elementTy == *children[i]);
}
-void StructType::fixup(const Model &m) {
- for (auto c : children) {
- c->fixup(m);
- }
+ return r;
}
-expr StructType::enforceStructType() const {
- return true;
+expr VectorType::enforceIntOrVectorType() const {
+ return children[0]->enforceIntType();
}
-expr StructType::enforceAggregateType(vector<Type*> *element_types) const {
- if (!element_types)
- return true;
-
- // TODO: support symbolic structs
- if (children.size() != element_types->size())
- return false;
-
- expr r(true);
- for (unsigned i = 0, e = children.size(); i != e; ++i) {
- r &= *children[i] == *(*element_types)[i];
- }
- return r;
+expr VectorType::enforceIntOrPtrOrVectorType() const {
+ return children[0]->enforceIntOrPtrType();
}
-const StructType* StructType::getAsStructType() const {
- return this;
+void VectorType::print(ostream &os) const {
+ if (elements)
+ os << '<' << elements << " x " << *children[0] << '>';
}
-pair<expr, vector<expr>> StructType::mkInput(State &s, const char *name) const {
- expr val;
- vector<expr> vars;
- unsigned num = 0;
- for (auto c : children) {
- string c_name = string(name) + "#" + to_string(num);
- auto [v, vs] = c->mkInput(s, c_name.c_str());
- val = num == 0 ? v : val.concat(v);
- vars.insert(vars.end(), vs.begin(), vs.end());
- ++num;
- }
- return { move(val), move(vars) };
+StructType::StructType(string &&name, vector<Type*> &&children)
+ : AggregateType(move(name), move(children)) {
+ elements = this->children.size();
+ defined = true;
}
-void StructType::printVal(ostream &os, State &s, const expr &val) const {
- os << "{ ";
- bool first = true;
- for (size_t i = 0, e = children.size(); i != e; ++i) {
- if (!first)
- os << ", ";
- getChild(i).printVal(os, s, extract(val, i).simplify());
- first = false;
+expr StructType::enforceStructType() const {
+ return true;
}
- os << " }";
+
+const StructType* StructType::getAsStructType() const {
+ return this;
}
void StructType::print(ostream &os) const {
+ if (!elements)
+ return;
+
os << '{';
- bool first = true;
- for (auto c : children) {
- if (!first)
+ for (unsigned i = 0; i < elements; ++i) {
+ if (i != 0)
os << ", ";
- first = false;
- c->print(os);
+ children[i]->print(os);
}
os << '}';
}
-smt::expr StructType::numElements() const {
- // TODO: fix symbolic struct type
- return expr::mkUInt(children.size(), 8);
-}
-
-Type& StructType::getChild(unsigned index) const {
- // TODO: fix symbolic struct type
- return *children[index];
-}
-
-expr StructType::extract(const expr &struct_val, unsigned index) const {
- unsigned total_till_now = 0;
- assert(index < children.size());
- for (unsigned i = 0; i <= index; ++i) {
- total_till_now += children[i]->bits();
- }
- unsigned low = struct_val.bits() - total_till_now;
- return struct_val.extract(low + children[index]->bits() - 1, low);
-}
-
SymbolicType::SymbolicType(string &&name)
: Type(string(name)), i(string(name)), f(string(name)), p(string(name)),
@@ -940,12 +905,17 @@ expr SymbolicType::enforceFloatType() const {
return isFloat();
}
-const StructType* SymbolicType::getAsStructType() const {
+const FloatType* SymbolicType::getAsFloatType() const {
+ return &*f;
+}
+
+const AggregateType* SymbolicType::getAsAggregateType() const {
+ // TODO: needs a proxy or something
return &*s;
}
-const FloatType* SymbolicType::getAsFloatType() const {
- return &*f;
+const StructType* SymbolicType::getAsStructType() const {
+ return &*s;
}
pair<expr, vector<expr>>

MODIFY
ir/type.h
ir/type.h
@@ -15,10 +15,13 @@ namespace smt { class Model; }
namespace IR {
+class AggregateType;
class FloatType;
class StructType;
+class SymbolicType;
class VoidType;
class State;
+class StateValue;
class Type {
protected:
@@ -60,10 +63,19 @@ public:
std::vector<Type*> *element_types = nullptr) const;
virtual smt::expr enforceFloatType() const;
- virtual const StructType* getAsStructType() const;
virtual const FloatType* getAsFloatType() const;
+ virtual const AggregateType* getAsAggregateType() const;
+ virtual const StructType* getAsStructType() const;
+
+ virtual smt::expr map_reduce(
+ smt::expr(*map)(const IR::StateValue&, const IR::StateValue&),
+ smt::expr(*reduce)(const std::set<smt::expr>&),
+ const IR::StateValue &a, const IR::StateValue &b) const;
virtual smt::expr toBV(smt::expr e) const;
+ IR::StateValue toBV(IR::StateValue v) const;
+ virtual smt::expr fromBV(smt::expr e) const;
+ IR::StateValue fromBV(IR::StateValue v) const;
virtual std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const = 0;
@@ -147,6 +159,7 @@ public:
smt::expr enforceFloatType() const override;
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, 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;
@@ -180,82 +193,73 @@ public:
};
-class ArrayType final : public Type {
+// don't create these directly; use vectors, arrays, or structs
+class AggregateType : public Type {
+protected:
+ std::vector<Type*> children;
+ std::vector<std::unique_ptr<SymbolicType>> sym;
+ unsigned elements;
+ bool defined = false;
+
+ AggregateType(std::string &&name, bool symbolic = true);
+ AggregateType(std::string &&name, std::vector<Type*> &&children)
+ : Type(std::move(name)), children(std::move(children)) {}
+
public:
- ArrayType(std::string &&name) : Type(std::move(name)) {}
+ smt::expr numElements() const;
+ IR::StateValue extract(const IR::StateValue &val, unsigned index) const;
+ IR::StateValue extract(const IR::StateValue &val,
+ const smt::expr &index) const;
+ Type& getChild(unsigned index) const { return *children[index]; }
+
unsigned bits() const override;
smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
- smt::expr operator==(const ArrayType &rhs) const;
- smt::expr sameType(const ArrayType &rhs) const;
+ smt::expr operator==(const AggregateType &rhs) const;
+ smt::expr sameType(const AggregateType &rhs) const;
void fixup(const smt::Model &m) override;
smt::expr enforceAggregateType(
std::vector<Type *> *element_types) 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;
- void print(std::ostream &os) const override;
+ const AggregateType* getAsAggregateType() const override;
+
+ smt::expr map_reduce(
+ smt::expr(*map)(const IR::StateValue&, const IR::StateValue&),
+ smt::expr(*reduce)(const std::set<smt::expr>&),
+ const IR::StateValue &a, const IR::StateValue &b) const override;
};
-class SymbolicType;
+class ArrayType final : public AggregateType {
+public:
+ ArrayType(std::string &&name) : AggregateType(std::move(name)) {}
+ smt::expr getTypeConstraints() const override;
+ void print(std::ostream &os) const override;
+};
-class VectorType final : public Type {
- std::unique_ptr<SymbolicType> sym;
- Type &elementTy;
- unsigned elements;
- bool defined = false;
+
+class VectorType final : public AggregateType {
public:
+ VectorType(std::string &&name) : AggregateType(std::move(name)) {}
VectorType(std::string &&name, unsigned elements, Type &elementTy);
- VectorType(std::string &&name);
-
- smt::expr numElements() const;
- smt::expr extract(const smt::expr &val, const smt::expr &index) const;
- unsigned bits() const override;
- smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
- smt::expr operator==(const VectorType &rhs) const;
- smt::expr sameType(const VectorType &rhs) const;
- void fixup(const smt::Model &m) override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
- smt::expr enforceAggregateType(
- std::vector<Type*> *element_types) 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;
void print(std::ostream &os) const override;
};
-class StructType final : public Type {
- const std::vector<Type*> children;
-
+class StructType final : public AggregateType {
public:
- StructType(std::string &&name) : Type(std::move(name)) {}
- StructType(std::string &&name, std::vector<Type*> &&children)
- : Type(std::move(name)), children(std::move(children)) {}
+ StructType(std::string &&name) : AggregateType(std::move(name)) {}
+ StructType(std::string &&name, std::vector<Type*> &&children);
- unsigned bits() const override;
- smt::expr getDummyValue() const override;
- smt::expr getTypeConstraints() const override;
- smt::expr operator==(const StructType &rhs) const;
- smt::expr sameType(const StructType &rhs) const;
- void fixup(const smt::Model &m) override;
smt::expr enforceStructType() const override;
- smt::expr enforceAggregateType(
- std::vector<Type*> *element_types) const override;
const StructType* getAsStructType() 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;
void print(std::ostream &os) const override;
-
- smt::expr numElements() const;
- Type& getChild(unsigned index) const;
- // Extracts the type located at \p index from \p struct_val
- smt::expr extract(const smt::expr &struct_val, unsigned index) const;
};
@@ -294,8 +298,9 @@ public:
smt::expr enforceAggregateType(
std::vector<Type*> *element_types) const override;
smt::expr enforceFloatType() const override;
- const StructType* getAsStructType() const override;
const FloatType* getAsFloatType() const override;
+ const AggregateType* getAsAggregateType() const override;
+ const StructType* getAsStructType() 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
@@ -157,9 +157,9 @@ static expr preprocess(Transform &t, const set<expr> &qvars,
auto var = static_cast<const Input &>(i).getTyVar();
if (config::disable_undef_input)
- e &= var != expr::mkUInt(1, 2);
+ e &= var != 1;
if (config::disable_poison_input)
- e &= var.extract(1, 1) == expr::mkUInt(0, 1);
+ e &= var.extract(1, 1) == 0;
}
if (qvars.empty() || e.isFalse())
@@ -231,18 +231,26 @@ static void check_refinement(Errors &errs, Transform &t,
expr pre = src_state.getPre() && tgt_state.getPre();
+ 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);
+
Solver::check({
{ pre && preprocess(t, qvars, ap.second, dom_a.notImplies(dom_b)),
[&](const Result &r) {
err(r, false, "Source is more defined than target");
}},
- { pre && preprocess(t, qvars, ap.second,
- dom_a && a.non_poison.notImplies(b.non_poison)),
+ { pre && preprocess(t, qvars, ap.second, dom_a && poison_cnstr),
[&](const Result &r) {
err(r, true, "Target is more poisonous than source");
}},
- { pre && preprocess(t, qvars, ap.second,
- dom_a && a.non_poison && a.value != b.value),
+ { pre && preprocess(t, qvars, ap.second, dom_a && value_cnstr),
[&](const Result &r) {
err(r, true, "Value mismatch");
}}

introduce AggregateType and do a big code refactoring
further testing undergoing