73    std::map<const IR::IDeclaration *, SymbolicValue *> map;
 
   76        for (
auto v : map) result->map.emplace(v.first, v.second->clone());
 
   82            if (filter(v.first, v.second)) result->map.emplace(v.first, v.second);
 
   92        return ::get(map, left);
 
   95    void dbprint(std::ostream &out)
 const {
 
   98            if (!first) out << std::endl;
 
   99            out << f.first << 
"=>" << f.second;
 
  105        BUG_CHECK(map.size() == other->map.size(), 
"Merging incompatible maps?");
 
  107            auto v = other->get(d.first);
 
  109            change = change || d.second->merge(v);
 
  113    bool equals(
const ValueMap *other)
 const {
 
  114        BUG_CHECK(map.size() == other->map.size(), 
"Incompatible maps compared");
 
  116            auto ov = other->get(v.first);
 
  118            if (!v.second->equals(ov)) 
return false;
 
 
  129    bool evaluatingLeftValue = 
false;
 
  131    std::map<const IR::Expression *, SymbolicValue *> value;
 
  134        LOG2(
"Symbolic evaluation of " << expression << 
" is " << v);
 
  135        value.emplace(expression, v);
 
  139    void postorder(
const IR::Constant *expression) 
override;
 
  140    void postorder(
const IR::BoolLiteral *expression) 
override;
 
  141    void postorder(
const IR::Operation_Ternary *expression) 
override;
 
  142    void postorder(
const IR::Operation_Binary *expression) 
override;
 
  143    void postorder(
const IR::Operation_Relation *expression) 
override;
 
  144    void postorder(
const IR::Operation_Unary *expression) 
override;
 
  145    void postorder(
const IR::PathExpression *expression) 
override;
 
  146    void postorder(
const IR::Member *expression) 
override;
 
  147    bool preorder(
const IR::ArrayIndex *expression) 
override;
 
  148    void postorder(
const IR::ArrayIndex *expression) 
override;
 
  149    void postorder(
const IR::ListExpression *expression) 
override;
 
  150    void postorder(
const IR::StructExpression *expression) 
override;
 
  151    void postorder(
const IR::MethodCallExpression *expression) 
override;
 
  152    void checkResult(
const IR::Expression *expression, 
const IR::Expression *result);
 
  153    void setNonConstant(
const IR::Expression *expression);
 
  157        : refMap(refMap), typeMap(typeMap), valueMap(valueMap) {
 
  160        CHECK_NULL(valueMap);
 
  166    SymbolicValue *evaluate(
const IR::Expression *expression, 
bool leftValue);
 
  169        auto r = ::get(value, expression);
 
  170        BUG_CHECK(r != 
nullptr, 
"no evaluation for %1%", expression);
 
 
  228    enum class ValueState {
 
  235    ScalarValue(ScalarValue::ValueState state, 
const IR::Type *type)
 
  240    bool isUninitialized()
 const { 
return state == ValueState::Uninitialized; }
 
  241    bool isUnknown()
 const { 
return state == ValueState::NotConstant; }
 
  242    bool isKnown()
 const { 
return state == ValueState::Constant; }
 
  243    bool isScalar()
 const override { 
return true; }
 
  244    void dbprint(std::ostream &out)
 const override {
 
  245        if (isUninitialized())
 
  246            out << 
"uninitialized";
 
  247        else if (isUnknown())
 
  250    static ValueState init(
bool uninit) {
 
  251        return uninit ? ValueState::Uninitialized : ValueState::NotConstant;
 
  253    void setAllUnknown()
 override { state = ScalarValue::ValueState::NotConstant; }
 
  254    ValueState mergeState(ValueState other)
 const {
 
  255        if (state == ValueState::Uninitialized && other == ValueState::Uninitialized)
 
  256            return ValueState::Uninitialized;
 
  257        if (state == ValueState::Constant && other == ValueState::Constant)
 
  259            return ValueState::Constant;
 
  260        return ValueState::NotConstant;
 
  262    bool hasUninitializedParts()
 const override { 
return state == ValueState::Uninitialized; }
 
 
  292        : 
ScalarValue(state, IR::Type_Boolean::get()), value(
false) {}
 
  294        : 
ScalarValue(ScalarValue::ValueState::Uninitialized, IR::Type_Boolean::get()),
 
  297        : 
ScalarValue(ScalarValue::ValueState::Constant, IR::Type_Boolean::get()),
 
  298          value(constant->value) {}
 
  301        : 
ScalarValue(ScalarValue::ValueState::Constant, IR::Type_Boolean::get()), value(value) {}
 
  302    void dbprint(std::ostream &out)
 const override {
 
  303        ScalarValue::dbprint(out);
 
  304        if (!isKnown()) 
return;
 
  305        out << (value ? 
"true" : 
"false");
 
  309        result->state = state;
 
  310        result->value = value;
 
 
  322    const IR::Constant *constant;
 
  324        : 
ScalarValue(ScalarValue::ValueState::Uninitialized, type), constant(
nullptr) {}
 
  325    SymbolicInteger(ScalarValue::ValueState state, 
const IR::Type_Bits *type)
 
  328        : 
ScalarValue(ScalarValue::ValueState::Constant, constant->type), constant(constant) {
 
  329        CHECK_NULL(constant);
 
  332    void dbprint(std::ostream &out)
 const override {
 
  333        ScalarValue::dbprint(out);
 
  334        if (isKnown()) out << constant->value;
 
  338        result->state = state;
 
  339        result->constant = constant;
 
 
  373        : 
ScalarValue(ScalarValue::ValueState::Uninitialized, type) {}
 
  377        : 
ScalarValue(ScalarValue::ValueState::Constant, type), value(value) {}
 
  379    void dbprint(std::ostream &out)
 const override {
 
  380        ScalarValue::dbprint(out);
 
  381        if (isKnown()) out << value;
 
 
  396    std::map<cstring, SymbolicValue *> fieldValue;
 
  397    SymbolicStruct(
const IR::Type_StructLike *type, 
bool uninitialized,
 
  400        auto r = ::get(fieldValue, field);
 
  406        fieldValue[field] = value;
 
  408    void dbprint(std::ostream &out) 
const override;
 
  409    bool isScalar()
 const override { 
return false; }
 
  411    void setAllUnknown() 
override;
 
  415    bool hasUninitializedParts() 
const override;
 
 
  570    unsigned minimumStreamOffset;
 
  577        : 
SymbolicExtern(type), minimumStreamOffset(0), conservative(
false) {}
 
  578    void dbprint(std::ostream &out)
 const override {
 
  579        out << 
"packet_in; offset =" << minimumStreamOffset
 
  580            << (conservative ? 
" (conservative)" : 
"");
 
  584        result->minimumStreamOffset = minimumStreamOffset;
 
  585        result->conservative = conservative;
 
  588    void setConservative() { conservative = 
true; }
 
  589    bool isConservative()
 const { 
return conservative; }
 
  590    void advance(
unsigned width) { minimumStreamOffset += width; }