add model printing for pointers
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -149,8 +149,12 @@ void Pointer::is_dereferenceable(unsigned bytes, unsigned align) {
}
ostream& operator<<(ostream &os, const Pointer &p) {
- // TODO
- return os << p.p;
+ os << "pointer(" << (p.is_local().simplify().isTrue() ? "local" : "non-local")
+ << ", block_id=";
+ p.get_bid().simplify().printUnsigned(os);
+ os << ", offset=";
+ p.get_offset().simplify().printSigned(os);
+ return os << ')';
}

MODIFY
ir/type.cpp
ir/type.cpp
@@ -179,7 +179,7 @@ pair<expr, vector<expr>> VoidType::mkInput(State &s, const char *name) const {
UNREACHABLE();
}
-void VoidType::printVal(ostream &os, const expr &e) const {
+void VoidType::printVal(ostream &os, State &s, const expr &e) const {
UNREACHABLE();
}
@@ -243,7 +243,7 @@ pair<expr, vector<expr>> IntType::mkInput(State &s, const char *name) const {
return { var, { var } };
}
-void IntType::printVal(ostream &os, const expr &e) const {
+void IntType::printVal(ostream &os, State &s, const expr &e) const {
e.printHexadecimal(os);
os << " (";
e.printUnsigned(os);
@@ -339,7 +339,7 @@ pair<expr, vector<expr>> FloatType::mkInput(State &s, const char *name) const {
return { var, { var } };
}
-void FloatType::printVal(ostream &os, const expr &e) const {
+void FloatType::printVal(ostream &os, State &s, const expr &e) const {
if (e.isNaN().simplify().isTrue()) {
os << "NaN";
} else if (e.isInf().simplify().isTrue()) {
@@ -422,9 +422,8 @@ pair<expr, vector<expr>> PtrType::mkInput(State &s, const char *name) const {
return s.getMemory().mkInput(name);
}
-void PtrType::printVal(ostream &os, const expr &e) const {
- // TODO
- os << e;
+void PtrType::printVal(ostream &os, State &s, const expr &e) const {
+ os << Pointer(s.getMemory(), e);
}
void PtrType::print(ostream &os) const {
@@ -473,7 +472,7 @@ pair<expr, vector<expr>> ArrayType::mkInput(State &s, const char *name) const {
return {};
}
-void ArrayType::printVal(ostream &os, const expr &e) const {
+void ArrayType::printVal(ostream &os, State &s, const expr &e) const {
// TODO
}
@@ -526,7 +525,7 @@ pair<expr, vector<expr>> VectorType::mkInput(State &s, const char *name) const {
return {};
}
-void VectorType::printVal(ostream &os, const expr &e) const {
+void VectorType::printVal(ostream &os, State &s, const expr &e) const {
// TODO
}
@@ -624,13 +623,13 @@ pair<expr, vector<expr>> StructType::mkInput(State &s, const char *name) const {
return { move(val), move(vars) };
}
-void StructType::printVal(ostream &os, const expr &val) const {
+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, extract(val, i).simplify());
+ getChild(i).printVal(os, s, extract(val, i).simplify());
first = false;
}
os << " }";
@@ -854,14 +853,14 @@ pair<expr, vector<expr>>
UNREACHABLE();
}
-void SymbolicType::printVal(ostream &os, const expr &e) const {
+void SymbolicType::printVal(ostream &os, State &st, const expr &e) const {
switch (typ) {
- case Int: i.printVal(os, e); break;
- case Float: f.printVal(os, e); break;
- case Ptr: p.printVal(os, e); break;
- case Array: a.printVal(os, e); break;
- case Vector: v.printVal(os, e); break;
- case Struct: s.printVal(os, e); break;
+ case Int: i.printVal(os, st, e); break;
+ case Float: f.printVal(os, st, e); break;
+ case Ptr: p.printVal(os, st, e); break;
+ case Array: a.printVal(os, st, e); break;
+ case Vector: v.printVal(os, st, e); break;
+ case Struct: s.printVal(os, st, e); break;
case Undefined: UNREACHABLE();
}
}

MODIFY
ir/type.h
ir/type.h
@@ -62,7 +62,8 @@ public:
virtual std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const = 0;
- virtual void printVal(std::ostream &os, const smt::expr &e) const = 0;
+ virtual void printVal(std::ostream &os, State &s,
+ const smt::expr &e) const = 0;
virtual void print(std::ostream &os) const = 0;
friend std::ostream& operator<<(std::ostream &os, const Type &t);
@@ -83,7 +84,7 @@ public:
void fixup(const smt::Model &m) override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
- void printVal(std::ostream &os, const smt::expr &e) const override;
+ void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -110,7 +111,7 @@ public:
smt::expr enforceIntOrPtrOrVectorType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
- void printVal(std::ostream &os, const smt::expr &e) const override;
+ void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -142,7 +143,7 @@ public:
const FloatType* getAsFloatType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
- void printVal(std::ostream &os, const smt::expr &e) const override;
+ void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -168,7 +169,7 @@ public:
smt::expr enforcePtrType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
- void printVal(std::ostream &os, const smt::expr &e) const override;
+ void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -185,7 +186,7 @@ public:
smt::expr enforceAggregateType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
- void printVal(std::ostream &os, const smt::expr &e) const override;
+ void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -203,7 +204,7 @@ public:
smt::expr enforceIntOrPtrOrVectorType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
- void printVal(std::ostream &os, const smt::expr &e) const override;
+ void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -227,7 +228,7 @@ public:
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, const smt::expr &e) 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;
@@ -273,7 +274,7 @@ public:
const FloatType* getAsFloatType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
- void printVal(std::ostream &os, const smt::expr &e) const override;
+ void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -26,8 +26,9 @@ static bool is_undef(const expr &e) {
return s.check().isUnsat();
}
-static void print_varval(ostream &s, const Model &m, const Value *var,
- const Type &type, const StateValue &val) {
+static void print_varval(ostream &s, 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
// this happens if the poison constraint depends on an undef
// however, cexs are usually triggered by the worst case, which is poison
@@ -53,7 +54,7 @@ static void print_varval(ostream &s, const Model &m, const Value *var,
return;
}
- type.printVal(s, m.eval(val.value, true));
+ type.printVal(s, 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?
@@ -93,23 +94,21 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
if (!dynamic_cast<const Input*>(var))
continue;
s << *var << " = ";
- print_varval(s, m, var, var->getType(), val.first);
+ print_varval(s, src_state, m, var, var->getType(), val.first);
s << '\n';
}
set<string> seen_vars;
- bool source = true;
- for (auto &vs : { src_state.getValues(), tgt_state.getValues() }) {
+ for (auto &st : { src_state, tgt_state }) {
if (!check_each_var) {
- if (source) {
+ if (st.isSource()) {
s << "\nSource:\n";
- source = false;
} else {
s << "\nTarget:\n";
}
}
- for (auto &[var, val] : vs) {
+ for (auto &[var, val] : st.getValues()) {
auto &name = var->getName();
if (name == var_name)
break;
@@ -120,16 +119,17 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
continue;
s << *var << " = ";
- print_varval(s, m, var, var->getType(), val.first);
+ print_varval(s, const_cast<State&>(st), m, var, var->getType(),
+ val.first);
s << '\n';
}
}
if (print_var) {
s << "Source value: ";
- print_varval(s, m, var, type, src);
+ print_varval(s, src_state, m, var, type, src);
s << "\nTarget value: ";
- print_varval(s, m, var, type, tgt);
+ print_varval(s, tgt_state, m, var, type, tgt);
}
errs.add(s.str());

add model printing for pointers