Call & Convention

8.13-eval-call.watsup and 8.14-eval-convention.watsup together define how call sites are resolved and how arguments are passed to and from callees.

Recall from Section 5.4 that a call statement resolves to:

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

Callee_eval resolves the call target to a typed callee value; Call_eval then takes that value and executes the call. This section explains both.

Callee Resolution

Before a call can execute, the spec needs to know what kind of thing is being called. A call target is either an actionCallee, an externMethodCallee, or a tableApplyMethodCallee. The callee type captures that information:

syntax actionCallee =
  ACTION callableId `( parameterIR* `) blockStatement

syntax externMethodCallee =
  EXTERN_METHOD lvalue '.' callableId `( parameterIR* `)

syntax tableApplyMethodCallee =
  TABLE nameIR '.' APPLY `{ tableProperties `}

syntax callee =
  | actionCallee
  | externMethodCallee
  | tableApplyMethodCallee

Each variant bundles everything Call_eval will need to execute the call.

Callee_eval inspects the call target and produces the appropriate variant:

relation Callee_eval:
  scope evalContext |- lvalue : callee
  hint(input %0 %1 %2)

Action callee

rule Callee_eval/action:
  scope EC |- referenceExpression : actionCallee
  -- if callableId = $id(referenceExpression)
  -- if actionDeclarationIR = $find_callableDef_e(EC, callableId)
  -- if ACTION _ `( parameterIR* `) blockStatement = actionDeclarationIR
  -- if actionCallee = ACTION callableId `( parameterIR* `) blockStatement

A bare name is resolved to a callableId and looked up in the callable environment with $find_callableDef_e. The result must be an ACTION declaration, from which the parameter list and body block are extracted and bundled into an actionCallee.

Extern method callee

rule Callee_eval/extern:
  scope EC |- lvalue_base '.' member : externMethodCallee
  -- Lvalue_eval:
      scope EC |- lvalue_base : packetValue
  -- if PACKET typeId objectState = packetValue
  -- if callableId = $id(member)
  -- if EXTERN _ externMethodTypeDefEnv = $find_typeDef_e(EC, typeId)
  -- if VOID _ `( parameterIR* `)
      = $find_map<callableId, externMethodTypeDefIR>(
          externMethodTypeDefEnv,
          callableId
        )
  -- if externMethodCallee
      = EXTERN_METHOD lvalue_base '.' callableId `( parameterIR* `)

In Nano-P4, the only extern type is packet_in and the only object of that type is pkt, so in practice base is always pkt and method is always extract. Therefore, Lvalue_eval evaluates base to a packetValue of the form PACKET typeId objectState, and typeId is used to look up the extern type definition (containing the method signatures) in the context.

The method is then found in the extern type’s method environment by callableId. The result is an externMethodCallee carrying the base l-value (needed to write the updated packet state back after the call) and the method’s parameter list.

Table apply callee

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 `}

A member access tbl.apply resolves tbl to a tableValue (stored in the block frame by ControlLocalDecl_eval/tableDeclaration, see Section 5.7) and packages its properties into a tableApplyMethodCallee. The member name itself is not checked here: the static type checker already verified that the only method on a table value is apply.

Call Execution

Call_eval dispatches on the callee variant produced by Callee_eval.

relation Call_eval:
  scope evalContext |- callee `( argument* `) -| evalContext
  hint(input %0 %1 %2 %3)

Action call

rule Call_eval/actionCallee:
  scope EC_0 |- actionCallee `( argument* `) -| EC_1
  -- if ACTION callableId `( parameterIR* `) blockStatement = actionCallee
  -- if EC_callee_0 = $inherit_e(GLOBAL, EC_0)
  -- Copy_in:
      scope EC_0 parameterIR*
        '@' LOCAL EC_callee_0 argument*
      ~> EC_callee_1 lvalue?*
  -- Block_eval:
      EC_callee_1 |- blockStatement -| EC_callee_2
  -- Copy_out:
      scope EC_0 parameterIR*
        '@' LOCAL EC_callee_2 lvalue?*
      ~> EC_1

The caller’s scope and context EC_0 are used for both argument evaluation and the eventual write-back. $inherit_e(GLOBAL, EC_0) produces a fresh callee context that shares the global frame of the caller but starts with empty block and local frames. Copy_in binds each argument to the matching parameter in the callee context and records which caller l-values need to be updated after the call. Block_eval runs the action body. Copy_out writes the final values of out and inout parameters back to the caller.

Extern method call

rule Call_eval/externMethodCallee:
  scope EC_0 |- externMethodCallee `( argument* `) -| EC_2
    -- if EXTERN_METHOD lvalue_extern '.' callableId `( parameterIR* `)
        = externMethodCallee
    -- Lvalue_eval:
        scope EC_0 |- lvalue_extern : value_extern
    -- if EC_callee_0 = $inherit_e(GLOBAL, EC_0)
    -- Copy_in:
        scope EC_0 parameterIR*
          '@' LOCAL EC_callee_0 argument*
        ~> EC_callee_1 lvalue?*
    -- if (_ _ nameIR = parameterIR)*
    -- ExternMethodCall_eval:
        EC_callee_1 |- value_extern '.' callableId `( nameIR* `)
                    : value_extern' -| EC_callee_2
    -- Copy_out:
        scope EC_0 parameterIR*
          '@' LOCAL EC_callee_2 lvalue?*
        ~> EC_1
    -- Lvalue_write:
        scope EC_1 |- lvalue_extern := value_extern' -| EC_2

Extern method calls follow the same Copy_in / body / Copy_out shape as action calls. The key differences are:

• The extern object’s current value is read with Lvalue_eval before the call.
• The body is dispatched through ExternMethodCall_eval, an extern relation whose implementation is outside the spec (it handles built-in operations like pkt.extract). It receives the current extern value and the bound parameter names, and returns an updated extern value value_extern'.
• After Copy_out writes back any directional parameters, Lvalue_write stores the updated extern value back to lvalue_extern, so the caller’s view of the extern object reflects whatever the method did to it.

Table apply call

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 apply does not use Copy_in / Copy_out because a table invocation has no declared parameter list. Instead, $inherit_e(BLOCK, EC_0) creates a callee context that shares both the global and block frames of the caller (so the table can read hdr and write to pass), with only the local frame reset. After Table_eval runs, the caller’s global and block layers are updated from the callee context so that any writes made during table execution are visible.

Copy-in

P4’s parameter passing is not simple value-passing. Each parameter has a direction that controls the behavior of both what the callee receives at entry and what the caller gets back at exit. Copy-in and copy-out implement this two-phase handoff.

At the call site, copy-in initializes each callee parameter from the corresponding argument. For in and directionless parameters, this is a straightforward value copy. For out parameters the argument is not read. Instead, the callee starts with a default value regardless of what the caller had. For inout the current value is copied in just like in, but the argument location is also recorded so that copy-out can write back to it.

Copy_in processes the parameter and argument lists in lock-step, delegating each pair to Copy_in_arg. It follows the standard nil/cons pattern.

The per-argument rule Copy_in_arg has three cases depending on the parameter direction:

rulegroup Copy_in_arg {

  rule Copy_in_arg/directionless-in:
      scope_caller EC_caller (direction _ nameIR)
      '@' scope_callee EC_callee argument
    ~> EC_callee' eps
    -- if direction = _EMPTY \/ direction = IN
    -- Expr_eval:
        scope_caller EC_caller |- argument : value
    -- if EC_callee' = $add_var_e(scope_callee, EC_callee, nameIR, value)

  rule Copy_in_arg/out:
      scope_caller EC_caller (OUT typeIR nameIR)
      '@' scope_callee EC_callee argument
    ~> EC_callee' lvalue
    -- if value = $default(typeIR)
    -- if EC_callee' = $add_var_e(scope_callee, EC_callee, nameIR, value)
    -- if lvalue = $lvalue_of_expression(argument)

  rule Copy_in_arg/inout:
    scope_caller EC_caller (INOUT typeIR nameIR)
      '@' scope_callee EC_callee argument
    ~> EC_callee' lvalue
    -- Expr_eval:
        scope_caller EC_caller |- argument : value
    -- if EC_callee' = $add_var_e(scope_callee, EC_callee, nameIR, value)
    -- if lvalue = $lvalue_of_expression(argument)

}

_EMPTY / IN: The argument is evaluated in the caller’s context and copied into the callee. No write-back is needed, so eps is returned as the l-value placeholder.

OUT: The callee parameter is initialized to the default value for its type ($default(typeIR)), which is zero for bit-vectors and integers, false for booleans, and zeroed structs and headers. The argument expression is not evaluated, since its value is irrelevant. Instead, $lvalue_of_expression converts the argument expression into an l-value that Copy_out will later write the final value to.

INOUT: Combines both: the current caller value is copied in, and the argument expression is also remembered as an l-value for write-back.

Copy-out

Once the callee body has finished executing, copy-out propagates results back to the caller. For in and directionless parameters, nothing is written back and the copy is discarded. For out and inout parameters the final value of the callee’s local variable is read and written to the l-value that copy-in recorded from the argument expression.

Copy_out mirrors Copy_in, processing pairs with Copy_out_arg:

rulegroup Copy_out_arg {

  rule Copy_out_arg/directionless-in:
    scope_caller EC_caller (direction _ _)
      '@' scope_callee EC_callee eps
    ~> EC_caller
    -- if direction = IN \/ direction = _EMPTY

  ;; Copy_out_arg/out-inout is left as the exercise for this section.

}

_EMPTY / IN: The l-value placeholder is eps, so nothing is written back. The caller’s context is returned unchanged.

OUT / INOUT: The final value of the parameter is read from the callee context with $find_var_e, then written to the caller l-value that was recorded during Copy_in. This is how an action’s writes to an out or inout parameter propagate back to the variable the caller passed in. You will write this rule in the exercise below.

Exercise

Branch: exercise/5.5

Check out the exercise branch in the spec submodule:

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

Run the following test to observe the failure:

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

The test should pass, but it fails. The Copy_out_arg/out-inout rule is missing from 8.14-eval-convention.watsup. It handles the write-back of out and inout parameters to the caller. Write it using the prose description in Copy-out above, and verify that the test passes.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main