Parameters and Arguments

Three spec files cover the static semantics of function-like calls in Nano-P4: how parameter lists are elaborated, how argument expressions are typed, and how the two sides are matched at a call site: 5.06-typing-parameter.watsup, 5.07-typing-argument.watsup, and 5.13-typing-call-convention.watsup.

Parameters

Parameter_ok

A single parameter is checked by Parameter_ok:

relation Parameter_ok:
  scope typingContext |- parameter : parameterIR -| typingContext
  hint(input %0 %1 %2)

The relation takes an incoming context and produces an outgoing one: each parameter adds a new variable binding visible to subsequent parameters.

rule Parameter_ok:
  scope TC_0 |- direction type name : parameterIR -| TC_1
  -- Type_ok: TC_0 |- type ~> typeIR
  -- if nameIR = $id(name)
  -- if parameterIR = direction typeIR nameIR
  -- if varTypeIR = direction typeIR
  -- if TC_1 = $add_var_t(scope, TC_0, nameIR, varTypeIR)

The rule elaborates the declared type, packages the result into a parameterIR triple of (direction, typeIR, nameIR), and extends the context with the new variable. Unlike local variables (which are unconditionally INOUT), a parameter’s direction comes directly from its declaration and is stored as-is.

Parameters_ok and ParameterList_ok

Multiple parameters are threaded left to right, exactly like statements in Section 3.4:

rule Parameters_ok/nil:
  scope TC |- eps : eps -| TC

rule Parameters_ok/cons:
  scope TC_0 |- parameter_h :: parameter_t* : parameterIR_h :: parameterIR_t* -| TC_2
  -- Parameter_ok: scope TC_0 |- parameter_h : parameterIR_h -| TC_1
  -- Parameters_ok: scope TC_1 |- parameter_t* : parameterIR_t* -| TC_2

ParameterList_ok is a thin wrapper that flattens the left-recursive syntax before delegating to Parameters_ok, and also enforces that no two parameters share the same name:

rule ParameterList_ok:
  scope TC_0 |- parameterList : parameterIR* -| TC_1
  -- if parameter* = $flatten_parameterList(parameterList)
  -- Parameters_ok: scope TC_0 |- parameter* : parameterIR* -| TC_1
  -- if $distinct_params(parameterIR*)

$distinct_params extracts the name fields from each parameterIR and checks them for uniqueness using the standard-library predicate $distinct_.

Helper predicates

Two helper predicates guard parameter lists in declaration rules (covered in Section 3.6):

dec $is_object_typeIR(typeIR) : bool
dec $no_object_params(parameterIR*) : bool

$is_object_typeIR returns true for parser, control, and package object types. $no_object_params confirms that no parameter in a list has an object type. This enforces the Nano-P4 restriction that actions and controls may not take other programmable-block objects as parameters.

Arguments

Argument_ok

An argument is a call-site expression paired with its elaborated type:

relation Argument_ok:
  scope typingContext |- argument : argumentIR
  hint(input %0 %1 %2)

rule Argument_ok:
  scope TC |- expression : argumentIR
  -- Expr_ok: scope TC |- expression : typeIR
  -- if argumentIR = expression '#' typeIR

The rule type-checks the expression and bundles it with its type into an argumentIR pair expression '#' typeIR. The expression itself is kept because the call-convention check below needs to inspect it structurally.

ArgumentList_ok

rule ArgumentList_ok:
  scope TC |- argumentList : argumentIR*
  -- if argument* = $flatten_argumentList(argumentList)
  -- (Argument_ok: scope TC |- argument : argumentIR)*

The iteration premise (Argument_ok: ...)* checks each argument independently under the same context TC. Unlike parameters, arguments do not bind anything, so there is no threading.

Call Convention

Call_convention_ok pairs up a parameter list parameterIR* with an argument list argumentIR* and performs a pairwise check.

rule Call_convention_ok/nil:
  eps '@' eps

rule Call_convention_ok/cons:
  (parameterIR_h :: parameterIR_t*) '@' (argumentIR_h :: argumentIR_t*)
  -- Call_convention_arg_ok: parameterIR_h '@' argumentIR_h
  -- Call_convention_ok:     parameterIR_t* '@' argumentIR_t*

The structural recursion over the two lists in lockstep requires equal lengths: there is no wildcard rule for mismatched lengths, so an arity mismatch has no applicable rule and the check fails.

Each pair is checked by Call_convention_arg_ok, which has three cases based on the parameter’s direction:

rule Call_convention_arg_ok/empty:
  parameterIR '@' argumentIR
  -- if _EMPTY typeIR_param _ = parameterIR
  -- if expression_arg '#' typeIR_arg = argumentIR
  -- Type_eq: typeIR_param ~~ typeIR_arg

rule Call_convention_arg_ok/in:
  parameterIR '@' argumentIR
  -- if IN typeIR_param _ = parameterIR
  -- if expression_arg '#' typeIR_arg = argumentIR
  -- Type_eq: typeIR_param ~~ typeIR_arg

rule Call_convention_arg_ok/out-inout:
  parameterIR '@' argumentIR
  ---- ;; Left for exercise!

EMPTY and IN parameters only require a type match.

OUT and INOUT parameters additionally require the argument expression to be an l-value, enforced by $expression_is_lvalue. This rule is left for you as exercise for this section.

Exercise

Branch: exercise/3.5

Check out the exercise branch in the spec submodule:

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

Run the following test to observe the failure:

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

The test program passes a literal integer to an OUT parameter. The checker should reject this, but it does not.

The Call_convention_arg_ok/out-inout rule in 5.13-typing-call-convention.watsup has been omitted entirely. Write the rule from scratch. There are three tests for this exercise: 3.5.p4, 3.5.1.p4, 3.5.2.p4. The latter two tests are negative tests, so they must be rejected by the typechecker.

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

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.5.1.p4
# should fail!

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.5.2.p4
# should fail!

When you are done, restore the original branch:

git -C nano-p4/spec checkout main