Control Block

This section covers 5.10-typing-control.watsup, which type-checks the body of a control declaration.

Recall from Section 3.6 that Decl_ok/controlDeclaration decomposes a control declaration into three parts and delegates each to a separate relation:

rule Decl_ok/controlDeclaration:
  TC_0 |- controlDeclaration -| TC_2
  -- if CONTROL name
      `( parameterList `)
      `{ controlLocalDeclarationList APPLY controlBody `} = controlDeclaration
  -- ParameterList_ok: BLOCK TC_0 |- parameterList : parameterIR* -| TC_body
  -- ControlLocalDeclList_ok: TC_body |- controlLocalDeclarationList -| TC_1
  -- Block_ok: TC_1 |- controlBody
  -- if callableId = $id(name)
  -- if callableTypeDef = CONTROL parameterIR*
  -- if TC_2 = $add_callableDef_t(TC_0, callableId, callableTypeDef)

The parameter list is handled by ParameterList_ok (covered in Section 3.5), and the apply block is handled by Block_ok (covered in Section 3.4). The remaining relation, ControlLocalDeclList_ok, is defined in 5.10-typing-control.watsup and is covered here.

Control Local Declarations

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

relation ControlLocalDecl_ok:
  typingContext |- controlLocalDeclaration -| typingContext
  hint(input %0 %1)

Unlike the parser case, which only allows variable declarations as local declarations, a control local declaration can be either a variable declaration or a table declaration. The ControlLocalDecl_ok rulegroup has one rule for each form:

rule ControlLocalDecl_ok/variableDeclaration:
  TC_0 |- variableDeclaration -| TC_1
  -- VarDecl_ok: BLOCK TC_0 |- variableDeclaration -| TC_1

rule ControlLocalDecl_ok/tableDeclaration:
  TC_0 |- tableDeclaration -| TC_1
  -- TableDecl_ok: TC_0 |- tableDeclaration -| TC_1

Both rules simply delegate to the appropriate specialized relation:

• VarDecl_ok handles variable declarations at BLOCK scope (see Section 3.4).
• TableDecl_ok handles table declarations (covered in Section 3.9).

Both produce an updated context TC_1 with the new binding, making the declared name visible to subsequent local declarations and the apply block.

Sequencing Local Declarations

Multiple local declarations are threaded left to right by ControlLocalDecls_ok, which follows the same nil/cons pattern used throughout the spec. The empty sequence leaves the context unchanged. A non-empty sequence checks the head declaration under the current context, obtains an updated context, and then checks the tail under that updated context, threading bindings left to right.

ControlLocalDeclList_ok is a thin wrapper that flattens the left-recursive syntax before delegating to ControlLocalDecls_ok:

rule ControlLocalDeclList_ok:
  TC_0 |- controlLocalDeclarationList -| TC_1
  -- if controlLocalDeclaration*
      = $flatten_controlLocalDeclarationList(controlLocalDeclarationList)
  -- ControlLocalDecls_ok: TC_0 |- controlLocalDeclaration* -| TC_1

The context TC_1 produced by ControlLocalDeclList_ok is the context passed to Block_ok for the apply block, so all local variable and table bindings are visible inside apply.

Exercise

Branch: exercise/3.8

Check out the exercise branch in the spec submodule:

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

Run the following test to observe the failure:

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.8.p4

The test program defines a control with a table local declaration. The checker should accept it, but it does not.

The two rules for ControlLocalDecls_ok have been omitted from 5.10-typing-control.watsup. Fill them in using the prose description in Sequencing Local Declarations above. The relation signature is already declared:

relation ControlLocalDecls_ok:
  typingContext |- controlLocalDeclaration* -| typingContext
  hint(input %0 %1)

Once the rules are in place:

./nano-p4spectec check nano-p4/spec \
    -i nano-p4/include \
    -p nano-p4/testdata/exercise/3.8.p4
# should pass!

When you are done, restore the original branch:

git -C nano-p4/spec checkout main