P4C
The P4 Compiler
|
Implements small-step operational semantics for expressions. More...
#include <expr_stepper.h>
Classes | |
class | ExternMethodImpls |
Encapsulates a set of extern method implementations. More... | |
struct | PacketCursorAdvanceInfo |
Public Member Functions | |
ExprStepper (const ExprStepper &)=default | |
ExprStepper (ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo) | |
ExprStepper (ExprStepper &&)=default | |
ExprStepper & | operator= (const ExprStepper &)=delete |
ExprStepper & | operator= (ExprStepper &&)=delete |
bool | preorder (const IR::ArrayIndex *arr) override |
bool | preorder (const IR::BaseListExpression *listExpression) override |
bool | preorder (const IR::BoolLiteral *boolLiteral) override |
bool | preorder (const IR::Constant *constant) override |
bool | preorder (const IR::Member *member) override |
bool | preorder (const IR::MethodCallExpression *call) override |
bool | preorder (const IR::Mux *mux) override |
bool | preorder (const IR::Operation_Binary *binary) override |
bool | preorder (const IR::Operation_Unary *unary) override |
bool | preorder (const IR::P4Table *table) override |
bool | preorder (const IR::P4ValueSet *valueSet) override |
bool | preorder (const IR::PathExpression *pathExpression) override |
bool | preorder (const IR::SelectExpression *selectExpression) override |
bool | preorder (const IR::Slice *slice) override |
bool | preorder (const IR::StructExpression *structExpression) override |
Public Member Functions inherited from P4::P4Tools::P4Testgen::AbstractStepper | |
AbstractStepper (ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo) | |
bool | preorder (const IR::Node *) override |
Provides generic handling of unsupported nodes. | |
Result | step (const IR::Node *) |
Public Member Functions inherited from P4::Inspector | |
const IR::Node * | apply_visitor (const IR::Node *, const char *name=0) override |
profile_t | init_apply (const IR::Node *root) override |
virtual void | loop_revisit (const IR::Node *) |
virtual void | postorder (const IR::Node *) |
virtual void | revisit (const IR::Node *) |
void | revisit_visited () |
bool | visit_in_progress (const IR::Node *n) const |
void | visitAgain () const override |
void | visitOnce () const override |
Public Member Functions inherited from P4::Visitor | |
virtual bool | check_global (cstring) |
virtual void | clear_globals () |
virtual Visitor * | clone () const |
virtual ControlFlowVisitor * | controlFlowVisitor () |
virtual void | end_apply () |
virtual void | end_apply (const IR::Node *root) |
virtual void | erase_global (cstring) |
template<class T > | |
const T * | findContext () const |
template<class T > | |
const T * | findContext (const Context *&c) const |
template<class T > | |
const T * | findOrigCtxt () const |
template<class T > | |
const T * | findOrigCtxt (const Context *&c) const |
virtual Visitor & | flow_clone () |
virtual void | flow_merge (Visitor &) |
virtual bool | flow_merge_closure (Visitor &) |
virtual void | flow_merge_global_from (cstring) |
virtual void | flow_merge_global_to (cstring) |
const Context * | getChildContext () const |
int | getChildrenVisited () const |
const Context * | getContext () const |
int | getContextDepth () const |
const IR::Node * | getCurrentNode () const |
template<class T > | |
const T * | getCurrentNode () const |
const IR::Node * | getOriginal () const |
template<class T > | |
const T * | getOriginal () const |
template<class T > | |
const T * | getParent () const |
virtual bool | has_flow_joins () const |
profile_t | init_apply (const IR::Node *root, const Context *parent_context) |
bool | isInContext (const IR::Node *n) const |
virtual const char * | name () const |
template<class T > | |
void | parallel_visit (const IR::Vector< T > &v, const char *name, int cidx) |
template<class T > | |
void | parallel_visit (const IR::Vector< T > &v, const char *name=0) |
template<class T > | |
void | parallel_visit (IR::Vector< T > &v, const char *name, int cidx) |
template<class T > | |
void | parallel_visit (IR::Vector< T > &v, const char *name=0) |
void | print_context () const |
const Visitor & | setCalledBy (const Visitor *visitor) |
void | setName (const char *name) |
void | visit (const IR::Node &n, const char *name, int cidx) |
void | visit (const IR::Node &n, const char *name=0) |
void | visit (const IR::Node *&n, const char *name, int cidx) |
void | visit (const IR::Node *&n, const char *name=0) |
void | visit (const IR::Node *const &n, const char *name, int cidx) |
void | visit (const IR::Node *const &n, const char *name=0) |
void | visit (IR::Node &n, const char *name, int cidx) |
void | visit (IR::Node &n, const char *name=0) |
void | visit (IR::Node *&, const char *=0, int=0) |
template<class T , typename = std::enable_if_t<Util::has_SourceInfo_v<T> && !std::is_pointer_v<T>>, class... Args> | |
void | warn (const int kind, const char *format, const T &node, Args &&...args) |
The const ref variant of the above. | |
template<class T , typename = std::enable_if_t<Util::has_SourceInfo_v<T>>, class... Args> | |
void | warn (const int kind, const char *format, const T *node, Args &&...args) |
bool | warning_enabled (int warning_kind) const |
Static Public Attributes | |
static const ExprStepper::ExternMethodImpls< ExprStepper > | CORE_EXTERN_METHOD_IMPLS |
Provides implementations of all known extern methods built into P4 core. | |
static const ExprStepper::ExternMethodImpls< ExprStepper > | INTERNAL_EXTERN_METHOD_IMPLS |
Definitions of internal helper functions. | |
Protected Member Functions | |
virtual PacketCursorAdvanceInfo | calculateAdvanceExpression (const ExecutionState &state, const IR::Expression *advanceExpr, const IR::Expression *restrictions) const |
virtual PacketCursorAdvanceInfo | calculateSuccessfulParserAdvance (const ExecutionState &state, int advanceSize) const |
void | evalActionCall (const IR::P4Action *action, const IR::MethodCallExpression *call) |
virtual void | evalExternMethodCall (const ExternInfo &externInfo) |
void | evalInternalExternMethodCall (const ExternInfo &externInfo) |
void | generateCopyIn (ExecutionState &nextState, const IR::StateVariable &targetPath, const IR::StateVariable &srcPath, cstring dir, bool forceTaint) const |
TODO: Consolidate this into the copy_in_out extern. | |
void | handleHitMissActionRun (const IR::Member *member) |
bool | resolveMethodCallArguments (const IR::MethodCallExpression *call) |
virtual void | stepNoMatch (std::string traceLog, const IR::Expression *condition=nullptr) |
Protected Member Functions inherited from P4::P4Tools::P4Testgen::AbstractStepper | |
void | declareBaseType (ExecutionState &nextState, const IR::StateVariable ¶mPath, const IR::Type_Base *baseType) const |
void | declareStructLike (ExecutionState &nextState, const IR::StateVariable &parentExpr, bool forceTaint=false) const |
const IR::Literal * | evaluateExpression (const IR::Expression *expr, std::optional< const IR::Expression * > cond) const |
virtual std::string | getClassName ()=0 |
virtual const ProgramInfo & | getProgramInfo () const |
void | logStep (const IR::Node *node) |
Helper function for debugging execution of small stepper. | |
void | setHeaderValidity (const IR::StateVariable &headerRef, bool validity, ExecutionState &state) |
void | setTargetUninitialized (ExecutionState &nextState, const IR::StateVariable &ref, bool forceTaint) const |
bool | stepGetHeaderValidity (const IR::StateVariable &headerRef) |
bool | stepSetHeaderValidity (const IR::StateVariable &headerRef, bool validity) |
bool | stepStackPushPopFront (const IR::Expression *stackRef, const IR::Vector< IR::Argument > *args, bool isPush=true) |
bool | stepSymbolicValue (const IR::Node *) |
bool | stepToException (Continuation::Exception) |
Protected Member Functions inherited from P4::Visitor | |
virtual void | init_join_flows (const IR::Node *) |
virtual bool | join_flows (const IR::Node *) |
virtual void | post_join_flows (const IR::Node *, const IR::Node *) |
void | visit_children (const IR::Node *, std::function< void()> fn) |
Static Protected Member Functions | |
static std::vector< std::pair< IR::StateVariable, const IR::Expression * > > | setFields (ExecutionState &nextState, const std::vector< IR::StateVariable > &flatFields, int varBitFieldSize) |
Static Protected Member Functions inherited from P4::P4Tools::P4Testgen::AbstractStepper | |
static void | checkMemberInvariant (const IR::Node *node) |
static bool | stepToListSubexpr (const IR::BaseListExpression *subexpr, SmallStepEvaluator::Result &result, const ExecutionState &state, std::function< const Continuation::Command(const IR::BaseListExpression *)> rebuildCmd) |
static bool | stepToStructSubexpr (const IR::StructExpression *subexpr, SmallStepEvaluator::Result &result, const ExecutionState &state, std::function< const Continuation::Command(const IR::StructExpression *)> rebuildCmd) |
static bool | stepToSubexpr (const IR::Expression *subexpr, SmallStepEvaluator::Result &result, const ExecutionState &state, std::function< const Continuation::Command(const Continuation::Parameter *)> rebuildCmd) |
Additional Inherited Members | |
Public Types inherited from P4::P4Tools::P4Testgen::AbstractStepper | |
using | Branch = SmallStepEvaluator::Branch |
using | Result = SmallStepEvaluator::Result |
Public Types inherited from P4::Visitor | |
typedef Visitor_Context | Context |
Static Public Member Functions inherited from P4::Visitor | |
static cstring | demangle (const char *) |
static bool | warning_enabled (const Visitor *visitor, int warning_kind) |
Public Attributes inherited from P4::Visitor | |
const Visitor * | called_by = nullptr |
cstring | internalName |
SplitFlowVisit_base *& | split_link |
SplitFlowVisit_base * | split_link_mem = nullptr |
Protected Attributes inherited from P4::P4Tools::P4Testgen::AbstractStepper | |
const ProgramInfo & | programInfo |
Target-specific information about the P4 program being evaluated. | |
Result | result |
The output of the evaluation. | |
AbstractSolver & | solver |
The solver backing the state being executed. | |
ExecutionState & | state |
The state being evaluated. | |
Protected Attributes inherited from P4::Visitor | |
bool | dontForwardChildrenBeforePreorder = false |
bool | joinFlows = false |
bool | visitDagOnce = true |
Implements small-step operational semantics for expressions.
struct P4::P4Tools::P4Testgen::ExprStepper::PacketCursorAdvanceInfo |
Contains information that is useful for externs that advance the parser cursor. For example, advance, extract, or lookahead.
|
protectedvirtual |
Calculates the conditions that need to be satisfied for a successful parser advance. This assumes that the advance amount is a run-time value. We need to pick a satisfying value assignment for a reject or advance of the parser. Targets may override this function with custom behavior.
|
protectedvirtual |
Calculates the conditions that need to be satisfied for a successful parser advance. This assumes that the advance amount is known already and a compile-time constant. Targets may override this function with custom behavior.
|
protected |
Evaluates a call to an action. This usually only happens when a table is invoked or when action is directly invoked from a control. In other cases, actions should be inlined. When the action call is evaluated, we use symbolic variables to pass arguments across execution boundaries. These variables persist until the end of program execution.
action | the action declaration that is being referenced. |
call | the actual method call containing the arguments. |
|
protectedvirtual |
Evaluates a call to an extern method. Upon return, the given result will be augmented with the successor states resulting from evaluating the call.
call | the original method call expression, can be used for stepInto calls. |
receiver | a symbolic value representing the object on which the method is being called. |
name | the name of the method being called. |
args | the list of arguments being passed to method. |
state | the state in which the call is being made, with the call at the top of the current continuation body. TODO(fruffy): Move this call out of the expression stepper. The location is confusing. |
Reimplemented in P4::P4Tools::P4Testgen::Bmv2::Bmv2V1ModelExprStepper, P4::P4Tools::P4Testgen::EBPF::EBPFExprStepper, P4::P4Tools::P4Testgen::Pna::PnaDpdkExprStepper, and P4::P4Tools::P4Testgen::Pna::SharedPnaExprStepper.
|
protected |
Evaluates a call to an extern method that only exists in the interpreter. These are helper functions used to execute custom operations and specific control flow. They do not exist as P4 code or call.
call | the original method call expression, can be used for stepInto calls. |
receiver | a symbolic value representing the object on which the method is being called. |
name | the name of the method being called. |
args | the list of arguments being passed to method. |
state | the state in which the call is being made, with the call at the top of the current continuation body. TODO(fruffy): Move this call out of the expression stepper. The location is confusing. |
|
protected |
This function call is used in member expressions to cleanly resolve hit, miss, and action run expressions. These are return values of a table.apply() call, and fairly special in P4. We have to use this rewrite to execute the table, and then return the corresponding values for hit, miss and action_run after that.
|
override |
This is a special function that handles the case where structure include P4ValueSet. Returns an updated structure, replacing P4ValueSet with a list of P4ValueSet components, splitting the list into separate keys if possible
|
protected |
Resolve all arguments to the method call by stepping into each argument that is not yet symbolic or a pure reference (represented as Out direction).
|
staticprotected |
Iterate over the fields in
flatFields | and set the corresponding values in |
nextState. | If there is a varbit, assign the |
varbitFieldSize | as size to it. |
|
protectedvirtual |
Takes a step to reflect a "select" expression failing to match. If condition is given, this will create a new state that is guarded by the given condition. The default implementation raises Continuation::Exception::NoMatch.