| 31 | using util::config::dbg; |
| 32 | |
| 33 | static void print_single_varval(ostream &os, State &st, const Model &m, |
| 34 | const Value *var, const Type &type, |
| 35 | const StateValue &val, unsigned child) { |
| 36 | if (dynamic_cast<const VoidType*>(&type)) { |
| 37 | os << "void"; |
| 38 | return; |
| 39 | } |
| 40 | |
| 41 | if (!val.isValid()) { |
| 42 | os << "(invalid expr)"; |
| 43 | return; |
| 44 | } |
| 45 | |
| 46 | // Best effort detection of poison if model is partial |
| 47 | if (auto v = m.eval(val.non_poison); |
| 48 | (v.isFalse() || check_expr(!v, "val_is_poison").isSat())) { |
| 49 | os << "poison"; |
| 50 | return; |
| 51 | } |
| 52 | |
| 53 | if (auto *in = dynamic_cast<const Input*>(var)) { |
| 54 | auto var = in->getUndefVar(type, child); |
| 55 | if (var.isValid() && m.eval(var).isAllOnes()) { |
| 56 | os << "undef"; |
| 57 | return; |
| 58 | } |
| 59 | } |
| 60 | |
| 61 | // TODO: detect undef bits (total or partial) with an SMT query |
| 62 | |
| 63 | expr partial = m.eval(val.value); |
| 64 | vector<pair<expr,expr>> repls; |
| 65 | for (auto &var : partial.vars()) { |
| 66 | repls.emplace_back(var, expr::some(var)); |
| 67 | } |
| 68 | |
| 69 | expr full = partial.subst_simplify(repls); |
| 70 | if (!full.isConst()) |
| 71 | full = m.eval(full, true); |
| 72 | type.printVal(os, st, full); |
| 73 | |
| 74 | if (dynamic_cast<const PtrType*>(&type)) { |
| 75 | Pointer ptr(st.returnMemory(), std::move(full)); |
| 76 | auto addr = m.eval(ptr.getAddress()); |
| 77 | if (addr.isConst() && !ptr.isNull().isTrue()) { |
| 78 | os << " / Address="; |
| 79 | addr.printHexadecimal(os); |
| 80 | } |
| 81 | } |
| 82 | |
| 83 | // undef variables may not have a model since each read uses a copy |
| 84 | // TODO: add intervals of possible values for ints at least? |
| 85 | for (auto &var : partial.vars()) { |
| 86 | if (var.fn_name().starts_with("undef!")) { |
| 87 | os << "\t[based on undef]"; |
| 88 | break; |
| 89 | } |
| 90 | } |
no test coverage detected