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 ::P4::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::StringLiteral *expression)
override;
142 void postorder(
const IR::Operation_Ternary *expression)
override;
143 void postorder(
const IR::Operation_Binary *expression)
override;
144 void postorder(
const IR::Operation_Relation *expression)
override;
145 void postorder(
const IR::Operation_Unary *expression)
override;
146 void postorder(
const IR::PathExpression *expression)
override;
147 void postorder(
const IR::Member *expression)
override;
148 bool preorder(
const IR::ArrayIndex *expression)
override;
149 void postorder(
const IR::ArrayIndex *expression)
override;
150 void postorder(
const IR::ListExpression *expression)
override;
151 void postorder(
const IR::StructExpression *expression)
override;
152 void postorder(
const IR::MethodCallExpression *expression)
override;
153 void checkResult(
const IR::Expression *expression,
const IR::Expression *result);
154 void setNonConstant(
const IR::Expression *expression);
158 : refMap(refMap), typeMap(typeMap), valueMap(valueMap) {
161 CHECK_NULL(valueMap);
167 SymbolicValue *evaluate(
const IR::Expression *expression,
bool leftValue);
170 auto r = ::P4::get(value, expression);
171 BUG_CHECK(r !=
nullptr,
"no evaluation for %1%", expression);
197class SymbolicException :
public SymbolicError {
199 const P4::StandardExceptions exc;
200 SymbolicException(
const IR::Node *errorPosition, P4::StandardExceptions exc)
201 : SymbolicError(errorPosition), exc(exc) {}
202 SymbolicValue *clone()
const override {
return new SymbolicException(errorPosition, exc); }
203 void dbprint(std::ostream &out)
const override { out <<
"Exception: " << exc; }
204 cstring message()
const override {
205 std::stringstream str;
211 DECLARE_TYPEINFO(SymbolicException, SymbolicError);
214class SymbolicStaticError :
public SymbolicError {
216 const std::string msg;
217 SymbolicStaticError(
const IR::Node *errorPosition, std::string_view message)
218 : SymbolicError(errorPosition), msg(message) {}
219 SymbolicValue *clone()
const override {
return new SymbolicStaticError(errorPosition, msg); }
220 void dbprint(std::ostream &out)
const override { out <<
"Error: " << msg; }
221 cstring message()
const override {
return msg; }
224 DECLARE_TYPEINFO(SymbolicStaticError, SymbolicError);
227class ScalarValue :
public SymbolicValue {
229 enum class ValueState {
236 ScalarValue(ScalarValue::ValueState state,
const IR::Type *type)
237 : SymbolicValue(type), state(state) {}
241 bool isUninitialized()
const {
return state == ValueState::Uninitialized; }
242 bool isUnknown()
const {
return state == ValueState::NotConstant; }
243 bool isKnown()
const {
return state == ValueState::Constant; }
244 bool isScalar()
const override {
return true; }
245 void dbprint(std::ostream &out)
const override {
246 if (isUninitialized())
247 out <<
"uninitialized";
248 else if (isUnknown())
251 static ValueState init(
bool uninit) {
252 return uninit ? ValueState::Uninitialized : ValueState::NotConstant;
254 void setAllUnknown()
override { state = ScalarValue::ValueState::NotConstant; }
255 ValueState mergeState(ValueState other)
const {
256 if (state == ValueState::Uninitialized && other == ValueState::Uninitialized)
257 return ValueState::Uninitialized;
258 if (state == ValueState::Constant && other == ValueState::Constant)
260 return ValueState::Constant;
261 return ValueState::NotConstant;
263 bool hasUninitializedParts()
const override {
return state == ValueState::Uninitialized; }
265 DECLARE_TYPEINFO(ScalarValue, SymbolicValue);
289class SymbolicBool final :
public ScalarValue {
292 explicit SymbolicBool(ScalarValue::ValueState state)
293 : ScalarValue(state, IR::Type_Boolean::get()), value(
false) {}
295 : ScalarValue(ScalarValue::ValueState::Uninitialized, IR::Type_Boolean::get()),
297 explicit SymbolicBool(
const IR::BoolLiteral *constant)
298 : ScalarValue(ScalarValue::ValueState::Constant, IR::Type_Boolean::get()),
299 value(constant->value) {}
300 SymbolicBool(
const SymbolicBool &other) =
default;
301 explicit SymbolicBool(
bool value)
302 : ScalarValue(ScalarValue::ValueState::Constant, IR::Type_Boolean::get()), value(value) {}
303 void dbprint(std::ostream &out)
const override {
304 ScalarValue::dbprint(out);
305 if (!isKnown())
return;
306 out << (value ?
"true" :
"false");
309 auto result =
new SymbolicBool();
310 result->state = state;
311 result->value = value;
318 DECLARE_TYPEINFO(SymbolicBool, ScalarValue);
321class SymbolicInteger final :
public ScalarValue {
323 const IR::Constant *constant;
324 explicit SymbolicInteger(
const IR::Type_Bits *type)
325 : ScalarValue(ScalarValue::ValueState::Uninitialized, type), constant(
nullptr) {}
326 SymbolicInteger(ScalarValue::ValueState state,
const IR::Type_Bits *type)
327 : ScalarValue(state, type), constant(
nullptr) {}
328 explicit SymbolicInteger(
const IR::Constant *constant)
329 : ScalarValue(ScalarValue::ValueState::Constant, constant->type), constant(constant) {
330 CHECK_NULL(constant);
332 SymbolicInteger(
const SymbolicInteger &other) =
default;
333 void dbprint(std::ostream &out)
const override {
334 ScalarValue::dbprint(out);
335 if (isKnown()) out << constant->value;
338 auto result =
new SymbolicInteger(type->to<IR::Type_Bits>());
339 result->state = state;
340 result->constant = constant;
347 DECLARE_TYPEINFO(SymbolicInteger, ScalarValue);
350class SymbolicString final :
public ScalarValue {
352 const IR::StringLiteral *string;
353 explicit SymbolicString(
const IR::Type_String *type)
354 : ScalarValue(ScalarValue::ValueState::Uninitialized, type), string(
nullptr) {}
355 SymbolicString(ScalarValue::ValueState state,
const IR::Type_String *type)
356 : ScalarValue(state, type), string(
nullptr) {}
357 explicit SymbolicString(
const IR::StringLiteral *
string)
358 : ScalarValue(ScalarValue::ValueState::Constant, string->type), string(
string) {
361 SymbolicString(
const SymbolicString &other) =
default;
362 void dbprint(std::ostream &out)
const override {
363 ScalarValue::dbprint(out);
364 if (isKnown()) out <<
string->value;
367 auto result =
new SymbolicString(type->to<IR::Type_String>());
368 result->state = state;
369 result->string = string;
376 DECLARE_TYPEINFO(SymbolicString, ScalarValue);
379class SymbolicVarbit final :
public ScalarValue {
381 explicit SymbolicVarbit(
const IR::Type_Varbits *type)
382 : ScalarValue(ScalarValue::ValueState::Uninitialized, type) {}
383 SymbolicVarbit(ScalarValue::ValueState state,
const IR::Type_Varbits *type)
384 : ScalarValue(state, type) {}
385 SymbolicVarbit(
const SymbolicVarbit &other) =
default;
386 void dbprint(std::ostream &out)
const override { ScalarValue::dbprint(out); }
388 return new SymbolicVarbit(state, type->to<IR::Type_Varbits>());
394 DECLARE_TYPEINFO(SymbolicVarbit, ScalarValue);
398class SymbolicEnum final :
public ScalarValue {
402 explicit SymbolicEnum(
const IR::Type *type)
403 : ScalarValue(ScalarValue::ValueState::Uninitialized, type) {}
404 SymbolicEnum(ScalarValue::ValueState state,
const IR::Type *type,
const IR::ID value)
405 : ScalarValue(state, type), value(value) {}
406 SymbolicEnum(
const IR::Type *type,
const IR::ID value)
407 : ScalarValue(ScalarValue::ValueState::Constant, type), value(value) {}
408 SymbolicEnum(
const SymbolicEnum &other) =
default;
409 void dbprint(std::ostream &out)
const override {
410 ScalarValue::dbprint(out);
411 if (isKnown()) out << value;
413 SymbolicValue *clone()
const override {
return new SymbolicEnum(state, type, value); }
418 DECLARE_TYPEINFO(SymbolicEnum, ScalarValue);
421class SymbolicStruct :
public SymbolicValue {
423 explicit SymbolicStruct(
const IR::Type_StructLike *type) : SymbolicValue(type) {
426 std::map<cstring, SymbolicValue *> fieldValue;
427 SymbolicStruct(
const IR::Type_StructLike *type,
bool uninitialized,
430 auto r = ::P4::get(fieldValue, field);
434 void set(
cstring field, SymbolicValue *value) {
436 fieldValue[field] = value;
438 void dbprint(std::ostream &out)
const override;
439 bool isScalar()
const override {
return false; }
440 SymbolicValue *clone()
const override;
441 void setAllUnknown()
override;
442 void assign(
const SymbolicValue *other)
override;
443 bool merge(
const SymbolicValue *other)
override;
444 bool equals(
const SymbolicValue *other)
const override;
445 bool hasUninitializedParts()
const override;
447 DECLARE_TYPEINFO(SymbolicStruct, SymbolicValue);
485class SymbolicArray final :
public SymbolicValue {
486 std::vector<SymbolicStruct *> values;
487 friend class AnyElement;
488 explicit SymbolicArray(
const IR::Type_Stack *type)
489 : SymbolicValue(type),
490 size(type->getSize()),
491 elemType(type->elementType->to<IR::Type_Header>()) {}
495 const IR::Type_Header *elemType;
496 SymbolicArray(
const IR::Type_Stack *stack,
bool uninitialized,
498 SymbolicValue *get(
const IR::Node *node,
size_t index)
const {
499 if (index >= values.size())
501 return values.at(index);
503 void shift(
int amount);
506 values[index] = value;
508 void dbprint(std::ostream &out)
const override;
509 SymbolicValue *clone()
const override;
510 SymbolicValue *next(
const IR::Node *node);
511 SymbolicValue *last(
const IR::Node *node);
512 SymbolicValue *lastIndex(
const IR::Node *node);
513 bool isScalar()
const override {
return false; }
514 void setAllUnknown()
override;
515 void assign(
const SymbolicValue *other)
override;
516 bool merge(
const SymbolicValue *other)
override;
517 bool equals(
const SymbolicValue *other)
const override;
518 bool hasUninitializedParts()
const override;
520 DECLARE_TYPEINFO(SymbolicArray, SymbolicValue);
524class AnyElement final :
public SymbolicHeader {
528 explicit AnyElement(
SymbolicArray *parent) : SymbolicHeader(parent->elemType), parent(parent) {
533 auto result =
new AnyElement(parent);
536 void setAllUnknown()
override { parent->setAllUnknown(); }
537 void assign(
const SymbolicValue *)
override { parent->setAllUnknown(); }
538 void dbprint(std::ostream &out)
const override { out <<
"Any element of " << parent; }
539 void setValid(
bool)
override { parent->setAllUnknown(); }
543 bool hasUninitializedParts()
const override { BUG(
"Should not be called"); }
545 DECLARE_TYPEINFO(AnyElement, SymbolicHeader);
548class SymbolicTuple final :
public SymbolicValue {
549 std::vector<SymbolicValue *> values;
552 explicit SymbolicTuple(
const IR::Type_Tuple *type) : SymbolicValue(type) {}
553 SymbolicTuple(
const IR::Type_Tuple *type,
bool uninitialized,
555 SymbolicValue *get(
size_t index)
const {
return values.at(index); }
556 void dbprint(std::ostream &out)
const override {
558 for (
auto f : values) {
559 if (!first) out <<
", ";
564 SymbolicValue *clone()
const override;
565 bool isScalar()
const override {
return false; }
566 void setAllUnknown()
override;
567 void assign(
const SymbolicValue *)
override { BUG(
"%1%: tuples are read-only",
this); }
568 void add(SymbolicValue *value) { values.push_back(value); }
569 bool merge(
const SymbolicValue *other)
override;
570 bool equals(
const SymbolicValue *other)
const override;
571 bool hasUninitializedParts()
const override;
573 DECLARE_TYPEINFO(SymbolicTuple, SymbolicValue);
577class SymbolicExtern :
public SymbolicValue {
579 explicit SymbolicExtern(
const IR::Type_Extern *type) : SymbolicValue(type) { CHECK_NULL(type); }
580 void dbprint(std::ostream &out)
const override { out <<
"instance of " << type; }
581 SymbolicValue *clone()
const override {
582 return new SymbolicExtern(type->to<IR::Type_Extern>());
584 bool isScalar()
const override {
return false; }
585 void setAllUnknown()
override { BUG(
"%1%: extern is read-only",
this); }
586 void assign(
const SymbolicValue *)
override { BUG(
"%1%: extern is read-only",
this); }
587 bool merge(
const SymbolicValue *)
override {
return false; }
588 bool equals(
const SymbolicValue *other)
const override;
589 bool hasUninitializedParts()
const override {
return false; }
591 DECLARE_TYPEINFO(SymbolicExtern, SymbolicValue);
595class SymbolicPacketIn final :
public SymbolicExtern {
600 unsigned minimumStreamOffset;
606 explicit SymbolicPacketIn(
const IR::Type_Extern *type)
607 : SymbolicExtern(type), minimumStreamOffset(0), conservative(
false) {}
608 void dbprint(std::ostream &out)
const override {
609 out <<
"packet_in; offset =" << minimumStreamOffset
610 << (conservative ?
" (conservative)" :
"");
613 auto result =
new SymbolicPacketIn(type->to<IR::Type_Extern>());
614 result->minimumStreamOffset = minimumStreamOffset;
615 result->conservative = conservative;
618 void setConservative() { conservative =
true; }
619 bool isConservative()
const {
return conservative; }
620 void advance(
unsigned width) { minimumStreamOffset += width; }
624 DECLARE_TYPEINFO(SymbolicPacketIn, SymbolicExtern);
TODO: this is not really specific to BMV2, it should reside somewhere else.
Definition applyOptionsPragmas.cpp:24