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; }
TODO: this is not really specific to BMV2, it should reside somewhere else.
Definition applyOptionsPragmas.cpp:24