Control Block

8.10-eval-control.watsup defines the evaluation semantics for control blocks.

The entrypoint for control execution is Control_apply, which is called by NanoSwitch_filter, a relation for architecture simulation:

rule NanoSwitch_filter:
  EC_0 |- controlDeclarationIR -| EC_1
  -- if argument* = [ _ID "hdr", _ID "accept" ]
  -- Control_apply:
      EC_0 argument* |- controlDeclarationIR -| EC_1

NanoSwitch_filter constructs the argument list (hdr and accept) and hands off to Control_apply, which runs the control’s local declarations and apply block. Control_apply is defined at the bottom of this section; the pieces it relies on are covered first.

Control Local Declarations

A control block may declare local variables and tables before its apply block. These are handled by ControlLocalDecl_eval:

relation ControlLocalDecl_eval:
  evalContext |- controlLocalDeclaration -| evalContext
  hint(input %0 %1)

Unlike the parser case from Section 5.6, which only allows variable declarations as local declarations, a control local declaration can be either a variable declaration or a table declaration. There is one rule for each form.

ControlLocalDecl_eval/variableDeclaration delegates to VarDecl_eval at BLOCK scope, just as the parser does for its local variables:

rule ControlLocalDecl_eval/variableDeclaration:
  EC_0 |- variableDeclaration -| EC_1
  -- VarDecl_eval:
      BLOCK EC_0 |- variableDeclaration -| EC_1

ControlLocalDecl_eval/tableDeclaration does not evaluate any expressions. Instead, it converts the declared name to a nameIR and packages the table declaration into a tableValue of the form TABLE nameIR tableProperties. That value is inserted into the context with $add_var_e at BLOCK scope, making the table accessible by name within the apply block. You will write this rule in the exercise below.

Sequencing Local Declarations

Multiple local declarations are threaded left to right by ControlLocalDecls_eval, following the same nil/cons pattern used throughout the spec:

rulegroup ControlLocalDecls_eval {

  rule ControlLocalDecls_eval/nil:
    EC |- eps -| EC

  rule ControlLocalDecls_eval/cons:
    EC_0 |- controlLocalDeclaration_h :: controlLocalDeclaration_t* -| EC_2
    -- ControlLocalDecl_eval:
        EC_0 |- controlLocalDeclaration_h -| EC_1
    -- ControlLocalDecls_eval:
        EC_1 |- controlLocalDeclaration_t* -| EC_2

}

ControlLocalDeclList_eval is a thin wrapper that flattens the left-recursive syntax before delegating to ControlLocalDecls_eval:

rule ControlLocalDeclList_eval:
  EC_0 |- controlLocalDeclarationList -| EC_1
  -- if controlLocalDeclaration*
      = $flatten_controlLocalDeclarationList(controlLocalDeclarationList)
  -- ControlLocalDecls_eval:
      EC_0 |- controlLocalDeclaration* -| EC_1

The context produced by ControlLocalDeclList_eval is passed directly to Block_eval for the apply block, so all local variable and table bindings are visible inside apply.

Control Apply

Control_apply ties everything together:

rule Control_apply:
  EC_0 argument* |- controlDeclarationIR -| EC_1
  -- if CONTROL nameIR
      `( parameterIR* `)
      `{ controlLocalDeclarationList APPLY controlBody `} = controlDeclarationIR
  -- if EC_callee_0 = $inherit_e(GLOBAL, EC_0)
  -- Copy_in:
      GLOBAL EC_0 parameterIR*
        '@' BLOCK EC_callee_0 argument*
      ~> EC_callee_1 lvalue?*
  -- ControlLocalDeclList_eval:
      EC_callee_1 |- controlLocalDeclarationList -| EC_callee_2
  -- Block_eval:
      EC_callee_2 |- controlBody -| EC_callee_3
  -- Copy_out:
      GLOBAL EC_0 parameterIR*
        '@' BLOCK EC_callee_3 lvalue?*
      ~> EC_1

The structure mirrors Parser_apply from Section 5.6 and follows the standard call-convention shape (covered in detail in Section 5.5):

1. $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.
2. Copy_in binds the call-site arguments (hdr and accept) to the control’s parameters and records which caller l-values correspond to out and inout parameters.
3. The control’s local declarations are evaluated in sequence, extending EC_callee_1 to EC_callee_2. Variable bindings and table values become accessible inside apply.
4. Block_eval executes the apply block under EC_callee_2, threading the context through each statement in turn and producing EC_callee_3.
5. Copy_out propagates any out and inout results back to the caller’s context EC_0, producing the final EC_1.

Unlike Parser_apply, Control_apply produces no explicit result value. The control communicates its outcome entirely through the out parameter accept: Filter sets accept = true to pass the packet or accept = false to drop it.

Exercise

Branch: exercise/5.7

Check out the exercise branch in the spec submodule:

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

Run the following test to observe the failure:

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

The test should pass, but it fails. The ControlLocalDecl_eval/tableDeclaration rule is missing from 8.10-eval-control.watsup. Write it using the prose description in Control Local Declarations above, and verify that the test passes.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main