don't crash when printing cexs with invalid exprs
MODIFY
ir/state_value.cpp
ir/state_value.cpp
@@ -29,6 +29,10 @@ StateValue StateValue::concat(const StateValue &other) const {
return { value.concat(other.value), non_poison.concat(other.non_poison) };
}
+bool StateValue::isValid() const {
+ return value.isValid() && non_poison.isValid();
+}
+
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
@@ -26,6 +26,7 @@ struct StateValue {
StateValue zextOrTrunc(unsigned tobw) const;
StateValue concat(const StateValue &other) const;
+ bool isValid() const;
smt::expr both() const { return value && non_poison; }
bool eq(const StateValue &other) const;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -32,6 +32,11 @@ static bool is_undef(const expr &e) {
static void print_single_varval(ostream &os, State &st, const Model &m,
const Value *var, const Type &type,
const StateValue &val) {
+ if (!val.isValid()) {
+ os << "(invalid expr)";
+ return;
+ }
+
// 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

don't crash when printing cexs with invalid exprs