Parser Block

8.09-eval-parser.watsup defines the evaluation semantics for parser blocks.

The entrypoint for parser execution is Parser_apply, which is called by NanoSwitch_parse, a relation for architecture simulation:

rule NanoSwitch_parse:
  EC_0 |- parserDeclarationIR : transitionResult -| EC_1
  -- if argument* = [ _ID "packet_in", _ID "hdr" ]
  -- Parser_apply:
      EC_0 argument* |- parserDeclarationIR : transitionResult -| EC_1

NanoSwitch_parse constructs the argument list (packet_in and hdr) and hands off to Parser_apply, which runs the full parser state machine. The transitionResult it returns determines whether the packet proceeds to the control block or is dropped. Parser_apply is defined at the bottom of this section; the pieces it relies on are covered first.

Parser Local Declarations

Before the parser state machine runs, a parser may declare local variables. These are handled by ParserLocalDecl_eval:

rule ParserLocalDecl_eval:
  EC_0 |- variableDeclaration -| EC_1
  -- VarDecl_eval:
      BLOCK EC_0 |- variableDeclaration -| EC_1

In Nano-P4, the only form a parser local declaration can take is a variable declaration. The rule delegates to VarDecl_eval at BLOCK scope, mirroring ParserLocalDecl_ok from Section 3.7. The resulting binding is visible inside all parser states.

Multiple local declarations are sequenced by ParserLocalDecls_eval using the same nil/cons pattern seen throughout the spec, and ParserLocalDeclList_eval wraps the flattening step before delegating to it.

Parser Transitions

Each parser state ends with a transition statement naming the next state to enter.

parser Parser(packet_in pkt, out Header hdr) {
    state start {
        pkt.extract(hdr.nanonet);
        transition accept;
    }
}

The ParserTransition_eval relation reduces a transition statement to a transitionResult, which is one of ACCEPT, REJECT, or STATE nameIR.

relation ParserTransition_eval:
  evalContext |- transitionStatement : transitionResult
  hint(input %0 %1)

There are four rules:

rulegroup ParserTransition_eval {

  rule ParserTransition_eval/accept:
    EC |- TRANSITION (name ';') : ACCEPT
    -- if $id(name) = "accept"

  rule ParserTransition_eval/reject:
    EC |- TRANSITION (name ';') : REJECT
    -- if $id(name) = "reject"

  rule ParserTransition_eval/state:
    EC |- TRANSITION (name ';') : (STATE nameIR)
    -- if nameIR = $id(name)
    -- if nameIR =/= "accept" /\ nameIR =/= "reject"

  rule ParserTransition_eval/selectExpression:
    EC |- TRANSITION selectExpression : transitionResult
    -- ParserSelect_eval:
        EC |- selectExpression : transitionResult

}

The first three rules handle a plain transition name;. The name is resolved to a nameIR and compared against the reserved strings "accept" and "reject". If it matches either built-in sink, the result is ACCEPT or REJECT respectively. Otherwise it becomes STATE nameIR, signaling that execution should continue in the named user-defined state.

The fourth rule delegates a select expression to ParserSelect_eval, covered next.

Select Expressions

A select transition dispatches to different states based on the runtime value of an expression:

transition select(hdr.nanonet.packetType) {
    7w1 : parse_data;
    7w2 : reject;
}

There are two rules:

rulegroup ParserSelect_eval {

  rule ParserSelect_eval/match:
    EC |- selectExpression : transitionResult
    -- if SELECT `( expression `) `{ selectCaseList `} = selectExpression
    -- Expr_eval: LOCAL EC |- expression : value
    -- if selectCase* = $flatten_selectCaseList(selectCaseList)
    -- if (expression_case ':' name_case ';' = selectCase)*
    -- (Expr_eval: LOCAL EC |- expression_case : value_case)*
    -- if name_match = $match_case_value(value, (name_case, value_case)*)
    -- ParserTransition_eval:
        EC |- TRANSITION (name_match ';') : transitionResult

  rule ParserSelect_eval/no-match:
    EC |- selectExpression : REJECT
    -- if SELECT `( expression `) `{ selectCaseList `} = selectExpression
    -- Expr_eval: LOCAL EC |- expression : value
    -- if selectCase* = $flatten_selectCaseList(selectCaseList)
    -- if (expression_case ':' name_case ';' = selectCase)*
    -- (Expr_eval: LOCAL EC |- expression_case : value_case)*
    -- if eps = $match_case_value(value, (name_case, value_case)*)

}

Both rules evaluate the selector expression to value and evaluate all case label expressions to value_case*. The helper $match_case_value scans (name_case, value_case)* left to right and returns the name of the first case whose value matches value, or eps if no case matches.

ParserSelect_eval/match fires when a match is found: it delegates the matched name back to ParserTransition_eval, which then produces the final transitionResult (either ACCEPT, REJECT, or STATE nameIR).

ParserSelect_eval/no-match fires when $match_case_value returns eps. The result is unconditionally REJECT, reflecting the P4 specification rule that an unmatched select drops the packet.

Compare with ParserTransition_ok/expression from Section 3.7: where the static rule type-checks each case label and validates each target name, the dynamic rule evaluates case labels to values and uses $match_case_value to pick a branch at runtime.

Parser State Evaluation

ParserState_eval executes a single named state:

relation ParserState_eval:
  evalContext |- parserState : transitionResult -| evalContext
  hint(input %0 %1)

rule ParserState_eval:
  EC_0 |- parserState : transitionResult -| EC_1
  -- if STATE name `{ statementList transitionStatement `} = parserState
  -- if statement* = $flatten_statementList(statementList)
  -- Statements_eval:
      LOCAL EC_0 |- statement* -| EC_1
  -- ParserTransition_eval:
      EC_1 |- transitionStatement : transitionResult

The rule runs the statements inside the state at LOCAL scope, threading the context from EC_0 to EC_1, then evaluates the trailing transition statement under EC_1 to produce a transitionResult. The relation carries EC_1 out because statements inside the state may write to out or inout parameters visible in the caller’s context (the packet extraction call pkt.extract modifies hdr, for example).

Parser State Transitions

ParserState_eval produces a single-step result. To follow a chain of state transitions until the parser reaches ACCEPT or REJECT, the spec uses ParserState_trans:

rulegroup ParserState_trans {

  rule ParserState_trans/accept:
    EC_0 parserState* |- nameIR : ACCEPT -| EC_1
    -- if parserState_found = $find_parserState(parserState*, nameIR)
    -- ParserState_eval:
        EC_0 |- parserState_found : ACCEPT -| EC_1

  rule ParserState_trans/reject:
    EC_0 parserState* |- nameIR : REJECT -| EC_1
    -- if parserState_found = $find_parserState(parserState*, nameIR)
    -- ParserState_eval:
        EC_0 |- parserState_found : REJECT -| EC_1

  ;; ParserState_trans/state is left as the exercise for this section.

}

$find_parserState locates the state with the given name in the list. The two rules shown are base cases: if ParserState_eval immediately returns ACCEPT or REJECT, the recursion stops. There is a third, recursive rule that handles the case where a state transitions to another named state, which you will write in the exercise below. The full state list parserState* is passed through unchanged so that any state can transition to any other.

Parser Apply

Parser_apply ties everything together:

rule Parser_apply:
  EC_0 argument* |- parserDeclarationIR : transitionResult -| EC_1
  -- if PARSER nameIR
      `( parameterIR* `)
      `{ parserLocalDeclarationList parserStateList `} = parserDeclarationIR
  -- if EC_callee_0 = $inherit_e(GLOBAL, EC_0)
  -- Copy_in:
      GLOBAL EC_0 parameterIR*
        '@' BLOCK EC_callee_0 argument*
      ~> EC_callee_1 lvalue?*
  -- ParserLocalDeclList_eval:
      EC_callee_1 |- parserLocalDeclarationList -| EC_callee_2
  -- if parserState* = $flatten_parserStateList(parserStateList)
  -- ParserState_trans:
      EC_callee_2 parserState* |- "start" : transitionResult -| EC_callee_3
  -- Copy_out:
      GLOBAL EC_0 parameterIR*
        '@' BLOCK EC_callee_3 lvalue?*
      ~> EC_1

This follows the standard call-convention shape covered in detail in Section 5.5:

$inherit_e(GLOBAL, EC_0) creates a fresh callee context that shares the global layer of the caller but starts with an empty block frame.
Copy_in binds the call-site arguments to the parser’s parameters and records which caller l-values correspond to out and inout parameters (covered in Section 5.5).
The parser’s local declarations are evaluated in sequence, extending EC_callee_1 to EC_callee_2.
ParserState_trans runs the state machine starting from "start", threading the context through each state until ACCEPT or REJECT is reached.
Copy_out propagates any out and inout results back to the caller’s context EC_0, producing the final EC_1 (also covered in Section 5.5).

The transitionResult (ACCEPT or REJECT) is returned to the caller (NanoSwitch_parse) to decide whether to continue to the control block or drop the packet.

Exercise

Branch: exercise/5.6

Check out the exercise branch in the spec submodule:

git -C nano-p4/spec checkout exercise/5.6

Run the following test to observe the failure:

./nano-p4spectec eval nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/5.6.p4 -stf nano-p4/testdata/exercise/5.6.stf

The test should pass, but it fails. The third rule of ParserState_trans is missing from 8.09-eval-parser.watsup. Write it and add it back so the test passes.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main

Keyboard shortcuts

Mechanizing the Nano-P4 specification with P4-SpecTec