Statements

8.05-eval-statement.watsup defines the Statement_eval relation:

relation Statement_eval:
  scope evalContext |- statement -| evalContext
  hint(input %0 %1 %2)

Read scope EC_0 |- s -| EC_1 as: “under context EC_0 at scope scope, statement s executes and produces context EC_1.”

This threading pattern mirrors Statement_ok from Section 3.4, but the context now carries values instead of types.

Empty Statement

rule Statement_eval/emptyStatement:
  scope EC |- emptyStatement -| EC

An empty statement is a no-op: it returns the incoming context unchanged.

Variable Declaration

rule VarDecl_eval:
  scope EC_0 |- type name ('=' expression) ';' -| EC_1
  -- Expr_eval:
      scope EC_0 |- expression : value
  -- if nameIR = $id(name)
  -- if EC_1 = $add_var_e(scope, EC_0, nameIR, value)

rule Statement_eval/variableDeclaration:
  scope EC_0 |- variableDeclaration -| EC_1
  -- VarDecl_eval: scope EC_0 |- variableDeclaration -| EC_1

VarDecl_eval evaluates the initializer expression to a value, converts the declared name to nameIR, and inserts the binding into the context with $add_var_e. The declared type annotation is not used at evaluation time; the static semantics already guarantees that the value has the right type.

Assignment Statement

rule Statement_eval/assignmentStatement:
  scope EC_0 |- lvalue '=' expression ';' -| EC_1
  -- Expr_eval:
      scope EC_0 |- expression : value
  -- Lvalue_write:
      scope EC_0 |- lvalue := value -| EC_1

Assignment evaluates the right-hand side to a value, then delegates the write to Lvalue_write. The updated context EC_1 carries the new binding. Note that both Expr_eval and Lvalue_write receive EC_0: the right-hand side is evaluated in the context before the write, which is the usual sequential evaluation order.

Call Statement

rule Statement_eval/callStatement:
  scope EC_0 |- lvalue `( argumentList `) ';' -| EC_1
  -- Callee_eval:
      scope EC_0 |- lvalue : callee
  -- if argument* = $flatten_argumentList(argumentList)
  -- Call_eval:
      scope EC_0 |- callee `( argument* `) -| EC_1

A call statement first resolves the callee name to a callee value via Callee_eval, flattens the argument list, then hands off to Call_eval. Call_eval handles binding arguments to parameters, executing the body, and propagating any out or inout writes back to the caller’s context. Both relations are covered in detail in Section 5.5: Call Convention.

Block Statement

rule Statement_eval/blockStatement:
  scope EC_0 |- blockStatement -| EC_3
  -- if EC_1 = $enter_e(EC_0)
  -- Block_eval:
      EC_1 |- blockStatement -| EC_2
  -- if EC_3 = $exit_e(EC_2)

A block pushes a fresh frame onto the local stack with $enter_e, evaluates the body under the extended context, then pops the frame with $exit_e. Any variables declared inside the block are discarded when the block exits. This is the runtime counterpart of Statement_ok/blockStatement from Section 3.4.

The helper relations that thread statements through a block are:

rule Block_eval:
  EC_0 |- `{ statementList `} -| EC_1
  -- if statement* = $flatten_statementList(statementList)
  -- Statements_eval:
      LOCAL EC_0 |- statement* -| EC_1

rule Statements_eval/nil:
  scope EC |- eps -| EC

rule Statements_eval/cons:
  scope EC_0 |- statement_h :: statement_t* -| EC_2
  -- Statement_eval:
      scope EC_0 |- statement_h -| EC_1
  -- Statements_eval:
      scope EC_1 |- statement_t* -| EC_2

Block_eval flattens the statement list and passes it to Statements_eval at LOCAL scope. Statements_eval threads the context left to right through each statement in sequence, just like Statements_ok in the type checker.

Conditional Statement

The two rules for conditionalStatement form a rulegroup. One rule fires when the condition evaluates to _B true and runs the then-branch block; the other fires when the condition evaluates to _B false and runs the else-branch block. Neither branch receives the other’s local declarations: each Block_eval call manages its own frame push and pop.

Compare with Statement_ok/conditionalStatement from Section 3.4, where both branches are checked under the same incoming context. At evaluation time, exactly one branch executes depending on the runtime value of the condition.

Exercise

Branch: exercise/5.4

Check out the exercise branch in the spec submodule:

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

Run the following test to observe the failure:

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

The test should pass, but it fails. The rules for Statement_eval/conditionalStatement are missing. Write them yourself, and verify that 5.4.p4 passes.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main