Tables

8.11-eval-table.watsup defines the evaluation semantics for table lookups.

Recall from Section 5.7 that when a control’s local declaration list is evaluated, each table declaration is packaged into a tableValue of the form TABLE nameIR tableProperties and stored in the block frame. When the apply block later calls tbl.apply(), Callee_eval/table retrieves that value and constructs a tableApplyMethodCallee:

rule Callee_eval/table:
  scope EC |- lvalue_base '.' member : tableApplyMethodCallee
  -- Lvalue_eval:
      scope EC |- lvalue_base : tableValue
  -- if TABLE nameIR tableProperties = tableValue
  -- if tableApplyMethodCallee = TABLE nameIR '.' APPLY `{ tableProperties `}

Call_eval/tableApplyMethodCallee then drives Table_eval with those properties:

rule Call_eval/tableApplyMethodCallee:
  scope EC_0 |- tableApplyMethodCallee `( argument* `) -| EC_1
    -- if TABLE typeId '.' APPLY `{ tableProperties `} = tableApplyMethodCallee
    -- if EC_callee_0 = $inherit_e(BLOCK, EC_0)
    -- Table_eval:
        EC_callee_0 |- tableProperties -| EC_callee_1
    -- if EC_1 = EC_0[ .GLOBAL = EC_callee_1.GLOBAL ]
                     [ .BLOCK = EC_callee_1.BLOCK ]

Table_eval runs in a callee context inherited from the BLOCK frame of the caller (unlike parser and control invocations, which inherit from GLOBAL), and its effects are merged back into both the global and block layers of the caller’s context.

The relations that make up Table_eval are covered below.

Table Key

TableKey_eval evaluates the table’s key expression to a concrete value:

relation TableKey_eval:
  evalContext |- tableKey : value
  hint(input %0 %1)

rule TableKey_eval:
  EC |- `{ expression ':' name ';' `} : value
  -- Expr_eval:
      LOCAL EC |- expression : value

The match kind name (name) is ignored at evaluation time; it was only needed during type checking to validate that the match kind is declared (the only key match policy in Nano-P4 is exact). Only the expression matters here, and it is evaluated at LOCAL scope to produce the runtime key value.

Compare with TableKey_ok from Section 3.9: the static rule type-checks the expression and validates the match kind name; the dynamic rule simply evaluates the expression.

Table Entry Matching

TableMatch_eval takes the key value and the list of constant entries, finds the first matching entry, and executes its action:

relation TableMatch_eval:
  evalContext value |- tableEntry* -| evalContext
  hint(input %0 %1 %2)

Matching relies on the helper $match_entry_value, which walks the list of (tableActionReference, value) pairs and returns the tableActionReference of the first pair whose value equals the key, or eps if no entry matches. Its declaration is:

dec $match_entry_value(value, (tableActionReference, value)*)
  : tableActionReference?

The three def clauses that implement it are left as the exercise for this section.

There are three rules in the TableMatch_eval rulegroup. The first handles the case where $match_entry_value returns eps (no entry matched the key) and leaves the context unchanged. The other two handle a successful match and differ only in whether the matched action reference carries an argument list:

rulegroup TableMatch_eval {

  rule TableMatch_eval/no-match:
    EC value_tableKey |- tableEntry* -| EC
    -- if (`( expression_entry `) ':' tableActionReference_entry ';' = tableEntry)*
    -- (Expr_eval: BLOCK EC |- expression_entry : value_entry)*
    -- if eps
        = $match_entry_value(
            value_tableKey,
            (tableActionReference_entry, value_entry)*
          )

  rule TableMatch_eval/match-no-argumentList:
    EC_0 value_tableKey |- tableEntry* -| EC_1
    -- if (`( expression_entry `) ':' tableActionReference_entry ';' = tableEntry)*
    -- (Expr_eval: BLOCK EC_0 |- expression_entry : value_entry)*
    -- if name
        = $match_entry_value(
            value_tableKey,
            (tableActionReference_entry, value_entry)*
          )
    -- Statement_eval:
        BLOCK EC_0 |- name `( _EMPTY `) ';' -| EC_1

  rule TableMatch_eval/match-argumentList:
    EC_0 value_tableKey |- tableEntry* -| EC_1
    -- if (`( expression_entry `) ':' tableActionReference_entry ';' = tableEntry)*
    -- (Expr_eval: BLOCK EC_0 |- expression_entry : value_entry)*
    -- if name `( argumentList `)
        = $match_entry_value(
            value_tableKey,
            (tableActionReference_entry, value_entry)*
          )
    -- Statement_eval:
        BLOCK EC_0 |- name `( argumentList `) ';' -| EC_1

}

Both rules evaluate all entry key expressions to value_entry*, then call $match_entry_value to find the matching action reference, and pattern-match on its shape:

• match-no-argumentList fires when the reference is a bare name. It synthesizes a call statement name ( EMPTY ) ; and delegates to Statement_eval.
• match-argumentList fires when the reference carries an argument list. It synthesizes name ( argumentList ) ; and delegates to Statement_eval.

In both cases the action is dispatched as an ordinary call statement, so Statement_eval routes it through Callee_eval and Call_eval exactly as any other action call would be.

Table Evaluation

Table_eval orchestrates the key lookup and entry matching:

rule Table_eval/no-entries:
  EC |- tableKeyProperty tableActionsProperty -| EC

rule Table_eval/no-match:
  EC_0 |- (KEY '=' tableKey)
        (ACTIONS '=' `{ tableActionList `})
        (CONST ENTRIES '=' `{ tableEntryList `}) -| EC_1
  -- TableKey_eval: EC_0 |- tableKey : value_tableKey
  -- if tableEntry* = $flatten_tableEntryList(tableEntryList)
  -- TableMatch_eval: EC_0 value_tableKey |- tableEntry* -| EC_1

Table_eval/no-entries handles a table declared without const entries. No key is evaluated and no action is dispatched; the context passes through unchanged.

Table_eval/entries handles a table with const entries: it evaluates the key, flattens the entry list, and delegates to TableMatch_eval.

Note that the tableActionsProperty is not used at runtime. The actions list was needed at type-checking time to validate which actions are reachable and to register their parameter signatures; at evaluation time the action is dispatched directly by name from within TableMatch_eval.

Exercise

Branch: exercise/5.8

Check out the exercise branch in the spec submodule:

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

Run the following test to observe the failure:

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

The test should pass, but it fails. The three def clauses of $match_entry_value are missing from 8.11-eval-table.watsup. Write them using the prose description in Table Entry Matching above, and verify that the test passes.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main