From 37cc4da62b6a8159fd73d5033aaf6d8f7cda3bfc Mon Sep 17 00:00:00 2001 From: fruffy Date: Tue, 30 Jul 2024 17:07:43 -0400 Subject: [PATCH] Make SymbolicVariable part of the core IR. Signed-off-by: fruffy --- backends/p4tools/p4tools.def | 21 --------------------- ir/expression.def | 21 +++++++++++++++++++++ 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/backends/p4tools/p4tools.def b/backends/p4tools/p4tools.def index 44d55d1db6..87bfd58217 100644 --- a/backends/p4tools/p4tools.def +++ b/backends/p4tools/p4tools.def @@ -130,27 +130,6 @@ class TaintExpression : Expression { dbprint { out << "TaintedExpression(" << type << ")"; } } -/// Signifies that a particular expression is a symbolic variable with a label. -/// These variables are intended to be consumed by SMT/SAT solvers. -class SymbolicVariable : Expression { -#noconstructor - - /// The label of the symbolic variable. - cstring label; - - /// A symbolic variable always has a type and no source info. - SymbolicVariable(Type type, cstring label) : Expression(type), label(label) {} - - /// Implements comparisons so that SymbolicVariables can be used as map keys. - bool operator<(const SymbolicVariable &other) const { - return label < other.label; - } - - toString { return "|" + label +"(" + type->toString() + ")|"; } - - dbprint { out << "|" + label +"(" << type << ")|"; } -} - /// This type replaces Type_Varbits and can store information about the current size class Extracted_Varbits : Type_Bits { public: diff --git a/ir/expression.def b/ir/expression.def index c6b61cd17a..7c6c0ccd63 100644 --- a/ir/expression.def +++ b/ir/expression.def @@ -611,4 +611,25 @@ class CompileTimeMethodCall : MethodCallExpression, CompileTimeValue { #nodbprint } +/// Signifies that a particular expression is a symbolic variable with a label. +/// These variables are intended to be consumed by SMT/SAT solvers. +class SymbolicVariable : Expression { +#noconstructor + + /// The label of the symbolic variable. + cstring label; + + /// A symbolic variable always has a type and no source info. + SymbolicVariable(Type type, cstring label) : Expression(type), label(label) {} + + /// Implements comparisons so that SymbolicVariables can be used as map keys. + bool operator<(const SymbolicVariable &other) const { + return label < other.label; + } + + toString { return "|" + label +"(" + type->toString() + ")|"; } + + dbprint { out << "|" + label +"(" << type << ")|"; } +} + /** @} *//* end group irdefs */