Expressions and L-values

8.03-eval-expression.watsup and 8.04-eval-lvalue.watsup define the Expr_eval, Lvalue_eval, and Lvalue_write relations.

relation Expr_eval:
  scope evalContext |- expression : value
  hint(input %0 %1 %2)

Read scope EC |- e : v as: “under context EC at scope scope, expression e evaluates to value v.”

The structure mirrors Expr_ok from Section 3.3 almost rule-for-rule with one key difference: where Expr_ok produces a typeIR, Expr_eval produces a value.

Literals

Boolean and integer literals evaluate to themselves:

rule Expr_eval/true:
  scope EC |- TRUE : _B true

rule Expr_eval/false:
  scope EC |- FALSE : _B false

rule Expr_eval/integerLiteral:
  scope EC |- integerLiteral : integerLiteral

Integer literals are already values in the syntax (w W i or w S i), so the rule is a no-op: the literal on the right of |- is identical to the one on the left.

Reference Expressions

rule Expr_eval/referenceExpression:
  scope EC |- name : value
  -- if nameIR = $id(name)
  -- if value = $find_var_e(scope, EC, nameIR)

The rule converts name to nameIR and looks up the current value in the evaluation context. Compare with Expr_ok/referenceExpression, which calls $find_var_t to get a type instead.

Unary and Binary Expressions

rule Expr_eval/unaryExpression:
  scope EC |- unop expression : value'
  -- Expr_eval: scope EC |- expression : value
  -- if value' = $un_op(unop, value)

rule Expr_eval/binaryExpression:
  scope EC |- expression_l binop expression_r : value
  -- Expr_eval: scope EC |- expression_l : value_l
  -- Expr_eval: scope EC |- expression_r : value_r
  -- if value = $bin_op(binop, value_l, value_r)

Both rules delegate the actual computation to helpers defined in 3.1-operations.watsup: $un_op for unary operators and $bin_op for binary operators. These helpers are defined exhaustively for every operator and value type combination. For example, unsigned addition converts both operands to raw integers, adds them, and wraps the result back into a fixed-width bitstring:

def $bin_op('+', w W i_l, w W i_r) = w W i'
  -- if i_l' = $bitstr_to_int(w, i_l)
  -- if i_r' = $bitstr_to_int(w, i_r)
  -- if i'   = $int_to_bitstr(w, $(i_l' + i_r'))

The static semantics already ensures that both operands have the same type, so $bin_op never has to handle mismatched widths at runtime.

Member Access

rule Expr_eval/struct:
  scope EC |- memberAccessBase '.' member : value_member
  -- Expr_eval: scope EC |- memberAccessBase : value_base
  -- if STRUCT typeId `{ fieldValue* `} = value_base
  -- if (value_field nameIR_field ';' = fieldValue)*
  -- if nameIR = $id(member)
  -- if value_member
      = $assoc_<nameIR, value>(nameIR, (nameIR_field, value_field)*)

rule Expr_eval/header:
  scope EC |- memberAccessBase '.' member : value_member
  -- Expr_eval: scope EC |- memberAccessBase : value_base
  -- if HEADER typeId `{ fieldValue* `} = value_base
  -- if (value_field nameIR_field ';' = fieldValue)*
  -- if nameIR = $id(member)
  -- if value_member
      = $assoc_<nameIR, value>(nameIR, (nameIR_field, value_field)*)

Where Expr_ok/struct destructures the type STRUCT _ `{ (typeIR id ';')* `} to find the field’s type, Expr_eval/struct destructures the value STRUCT typeId `{ fieldValue* `} to find the field’s current value. The $assoc_ call performs a linear scan of the (nameIR_field, value_field)* pairs to return the value associated with nameIR.

Parenthesized Expressions

rule Expr_eval/parenthesizedExpression:
  scope EC |- `( expression `) : value
  -- Expr_eval: scope EC |- expression : value

Parentheses are transparent at runtime, just as they are during type checking.

Reading L-values: Lvalue_eval

relation Lvalue_eval:
  scope evalContext |- lvalue : value
  hint(input %0 %1 %2)

An l-value is a location that can appear on the left of an assignment. Reading one is straightforward: convert it to the equivalent expression and delegate to Expr_eval:

rule Lvalue_eval:
  scope EC |- lvalue : value
  -- if expression = $expression_of_lvalue(lvalue)
  -- Expr_eval:
      scope EC |- expression : value

$expression_of_lvalue is a syntactic helper that turns a lvalue into an expression of the same shape. Every l-value form has a corresponding expression form, so the conversion is always total.

Writing L-values: Lvalue_write

Writing is more involved: the interpreter finds the variable that owns the location, updates its stored value, and threads the updated context forward.

relation Lvalue_write:
  scope evalContext |- lvalue := value -| evalContext
  hint(input %0 %1 %2 %3)

Simple Variable

rule Lvalue_write/referenceExpression:
  scope EC_0 |- referenceExpression := value -| EC_1
  -- if nameIR = $id(referenceExpression)
  -- if EC_1 = $update_var_e(scope, EC_0, nameIR, value)

A bare name resolves to a nameIR and calls $update_var_e, which walks the frame stack to find the frame that owns nameIR and overwrites the binding there. The frame walk was covered in Section 5.1.

Member Access

Both rules for struct and header member access follow the same read-modify-write pattern: read the current value of the base l-value, update the relevant field inside it, reconstruct the whole-aggregate value, and write it back recursively. The recursion handles nested member access naturally. These rules are left as the exercise for this section.

$update_fieldValue is a small helper that scans the field list and replaces the value associated with the given nameIR:

dec $update_fieldValue(fieldValue*, nameIR, value) : fieldValue*

def $update_fieldValue(eps, nameIR, value) = eps
def $update_fieldValue(
    (value_field_h nameIR_field_h ';') :: fieldValue_t*,
    nameIR, value)
  = (value nameIR ';') :: fieldValue_t*
  -- if nameIR_field_h = nameIR
def $update_fieldValue(
    (value_field_h nameIR_field_h ';') :: fieldValue_t*,
    nameIR, value)
  = (value_field_h nameIR_field_h ';') ::
      $update_fieldValue(fieldValue_t*, nameIR, value)
  -- if nameIR_field_h =/= nameIR

The first clause handles an empty list. The second replaces the head when its name matches. The third skips the head and recurses when names differ.

Parenthesized L-value

rule Lvalue_write/parenthesized:
  scope EC_0 |- (`( lvalue `)) := value -| EC_1
  -- Lvalue_write:
      scope EC_0 |- lvalue := value -| EC_1

Parentheses are transparent for writing, just as they are for reading.

Exercise

Branch: exercise/5.3

Check out the exercise branch in the spec submodule:

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

Run the following test to observe the failure:

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

The test program writes to a nested member l-value and reads the result back. It should pass, but the interpreter gets stuck. Two rules have been omitted from 8.04-eval-lvalue.watsup. Write them by analogy with each other and with Lvalue_write/referenceExpression.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main