improve cex printing for aggregate types
MODIFY
ir/type.cpp
ir/type.cpp
@@ -110,6 +110,22 @@ bool Type::isPtrType() const {
return false;
}
+bool Type::isArrayType() const {
+ return false;
+}
+
+bool Type::isStructType() const {
+ return false;
+}
+
+bool Type::isVectorType() const {
+ return false;
+}
+
+bool Type::isAggregateType() const {
+ return isArrayType() || isStructType() || isVectorType();
+}
+
expr Type::enforceIntType(unsigned bits) const {
return false;
}
@@ -154,12 +170,6 @@ 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;
}
@@ -664,37 +674,23 @@ AggregateType::mkInput(State &s, const char *name) const {
}
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 << ", ";
- children[i]->printVal(os, s, extract(tmp_e, i).value.simplify());
- }
- os << (dynamic_cast<const StructType*>(this) ? " }" : " >");
+ UNREACHABLE();
}
const AggregateType* AggregateType::getAsAggregateType() const {
return this;
}
-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 reduce(r);
-}
-
expr ArrayType::getTypeConstraints() const {
// TODO
return false;
}
+bool ArrayType::isArrayType() const {
+ return true;
+}
+
void ArrayType::print(ostream &os) const {
os << "TODO";
}
@@ -727,6 +723,10 @@ expr VectorType::getTypeConstraints() const {
return r;
}
+bool VectorType::isVectorType() const {
+ return true;
+}
+
expr VectorType::enforceIntOrVectorType() const {
return children[0]->enforceIntType();
}
@@ -747,6 +747,10 @@ StructType::StructType(string &&name, vector<Type*> &&children)
defined = true;
}
+bool StructType::isStructType() const {
+ return true;
+}
+
expr StructType::enforceStructType() const {
return true;
}
@@ -920,6 +924,18 @@ bool SymbolicType::isPtrType() const {
return typ == Ptr;
}
+bool SymbolicType::isArrayType() const {
+ return typ == Array;
+}
+
+bool SymbolicType::isVectorType() const {
+ return typ == Vector;
+}
+
+bool SymbolicType::isStructType() const {
+ return typ == Struct;
+}
+
expr SymbolicType::enforceIntType(unsigned bits) const {
return isInt() && (i ? i->enforceIntType(bits) : false);
}

MODIFY
ir/type.h
ir/type.h
@@ -53,6 +53,10 @@ public:
virtual bool isIntType() const;
virtual bool isFloatType() const;
virtual bool isPtrType() const;
+ virtual bool isArrayType() const;
+ virtual bool isStructType() const;
+ virtual bool isVectorType() const;
+ bool isAggregateType() const;
virtual smt::expr enforceIntType(unsigned bits = 0) const;
virtual smt::expr enforceIntOrVectorType() const;
@@ -68,11 +72,6 @@ public:
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;
@@ -220,6 +219,8 @@ protected:
public:
smt::expr numElements() const;
+ unsigned numElementsConst() const { return elements; }
+
StateValue aggregateVals(const std::vector<StateValue> &vals) const;
IR::StateValue extract(const IR::StateValue &val, unsigned index) const;
IR::StateValue extract(const IR::StateValue &val,
@@ -240,11 +241,6 @@ public:
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) 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;
};
@@ -252,6 +248,7 @@ class ArrayType final : public AggregateType {
public:
ArrayType(std::string &&name) : AggregateType(std::move(name)) {}
smt::expr getTypeConstraints() const override;
+ bool isArrayType() const override;
void print(std::ostream &os) const override;
};
@@ -262,6 +259,7 @@ public:
VectorType(std::string &&name, unsigned elements, Type &elementTy);
smt::expr getTypeConstraints() const override;
+ bool isVectorType() const override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
void print(std::ostream &os) const override;
@@ -273,6 +271,7 @@ public:
StructType(std::string &&name) : AggregateType(std::move(name)) {}
StructType(std::string &&name, std::vector<Type*> &&children);
+ bool isStructType() const override;
smt::expr enforceStructType() const override;
const StructType* getAsStructType() const override;
void print(std::ostream &os) const override;
@@ -306,6 +305,9 @@ public:
bool isIntType() const override;
bool isFloatType() const override;
bool isPtrType() const override;
+ bool isArrayType() const override;
+ bool isStructType() const override;
+ bool isVectorType() const override;
smt::expr enforceIntType(unsigned bits = 0) const override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -29,7 +29,7 @@ static bool is_undef(const expr &e) {
return s.check().isUnsat();
}
-static void print_varval(ostream &s, State &st, const Model &m,
+static void print_single_varval(ostream &os, State &st, const Model &m,
const Value *var, const Type &type,
const StateValue &val) {
// if the model is partial, we don't know for sure if it's poison or not
@@ -37,7 +37,7 @@ static void print_varval(ostream &s, State &st, const Model &m,
// however, cexs are usually triggered by the worst case, which is poison
if (auto v = m.eval(val.non_poison);
(!v.isConst() || v.isFalse())) {
- s << "poison";
+ os << "poison";
return;
}
@@ -45,7 +45,7 @@ static void print_varval(ostream &s, State &st, const Model &m,
uint64_t n;
ENSURE(m[in->getTyVar()].isUInt(n));
if (n == 1) {
- s << "undef";
+ os << "undef";
return;
}
assert(n == 0);
@@ -53,11 +53,11 @@ static void print_varval(ostream &s, State &st, const Model &m,
expr partial = m.eval(val.value);
if (is_undef(partial)) {
- s << "undef";
+ os << "undef";
return;
}
- type.printVal(s, st, m.eval(val.value, true));
+ type.printVal(os, st, m.eval(val.value, true));
// undef variables may not have a model since each read uses a copy
// TODO: add intervals of possible values for ints at least?
@@ -72,10 +72,28 @@ static void print_varval(ostream &s, State &st, const Model &m,
found_undef |= string_view(name).substr(0, 6) == "undef_";
}
if (found_undef)
- s << "\t[based on undef value]";
+ os << "\t[based on undef value]";
}
}
+static void print_varval(ostream &os, State &st, const Model &m,
+ const Value *var, const Type &type,
+ const StateValue &val) {
+ if (!type.isAggregateType()) {
+ print_single_varval(os, st, m, var, type, val);
+ return;
+ }
+
+ os << (type.isStructType() ? "{ " : "< ");
+ auto agg = type.getAsAggregateType();
+ for (unsigned i = 0, e = agg->numElementsConst(); i < e; ++i) {
+ if (i != 0)
+ os << ", ";
+ print_varval(os, st, m, var, agg->getChild(i), agg->extract(val, i));
+ }
+ os << (type.isStructType() ? " }" : " >");
+}
+
static void error(Errors &errs, State &src_state, State &tgt_state,
const Result &r, bool print_var, const Value *var,

improve cex printing for aggregate types