Skip to content

Commit

Permalink
Make SymbolicVariable part of the core IR.
Browse files Browse the repository at this point in the history
Signed-off-by: fruffy <[email protected]>
  • Loading branch information
fruffy committed Jul 31, 2024
1 parent fcaf633 commit 37cc4da
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 21 deletions.
21 changes: 0 additions & 21 deletions backends/p4tools/p4tools.def
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
21 changes: 21 additions & 0 deletions ir/expression.def
Original file line number Diff line number Diff line change
Expand Up @@ -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 */

0 comments on commit 37cc4da

Please sign in to comment.