P4 doesn't state insertion of implicit cast on the RHS of assignments

[pataei]

P4 spec has lots of examples in various subsections of needing to cast the RHS of assignment, however, it never discusses it explicitly. Even worse, it doesn't mention anything in section 12.1 (asssignment statement).

On the other hand, Petr4 clearly inserts implicit casts when needed on the RHS of an assignment.

Petr4 code

The line let rhs_typed = cast_expression env expr_ctx lhs_typed.typ rhs in is responsible for the potential insertion of casts.

type_assignment env ctx lhs rhs =
  let open Expression in 
  let open Prog.Statement in
  let expr_ctx = ExprContext.of_stmt_context ctx in
  let lhs_typed = type_expression env expr_ctx lhs in
  if not @@ is_lvalue env lhs_typed
  then raise_s [%message "Must be an lvalue"
                   ~lhs:(lhs:Types.Expression.t)]
  else
    let rhs_typed = cast_expression env expr_ctx lhs_typed.typ rhs in
    ignore (assert_same_type env (tags lhs) (tags rhs)
              lhs_typed.typ rhs_typed.typ);
    { stmt = Assignment { lhs = lhs_typed; rhs = rhs_typed; tags = Info.merge (tags lhs) (tags rhs) };
      typ = StmType.Unit },
    env

P4 spec (v1.2.3)

Section 12.1 (asssignment statement): "An assignment, written with the = sign, first evaluates its left sub-expression to an l-value, then evaluates its right sub-expression to a value, and finally copies the value into the l-value. Derived types (e.g. structs) are copied recursively, and all components of headers are copied, including “validity” bits. Assignment is not defined for extern values."

Examples taken from P4 spec that illustrate the need to insert an implicit cast on the RHS of an assignment:

Section 8.12: "A list may be used to initialize a structure if the list has the same number of elements as fields in the structure. The effect of such an initializer is to assign the nth element of the list to the nth field in the structure:

struct S {
    bit<32> a;
    bit<32> b;
}
const S x = { 10, 20 }; //a = 10, b = 20

Section 8.13: "For a structure-valued expression typeRef is the name of a struct or header type. The typeRef can be omitted if it can be inferred from context, e.g., when initializing a variable with a struct type. The following example shows a structure-valued expression used in an equality comparison expression:"

struct S {
    bit<32> a;
    bit<32> b;
}

S s;

// Compare s with a structure-valued expression
bool b = s == (S) { a = 1, b = 2 };

P4 spec doesn't even consider such conversions as casts (or at least, it doesn't phrase them as casts), instead, it states them as automatic conversions. Furthermore, it doesn't include them in the list of explicit/implicit casts.

For reference, the following is the legal list of P4's explicit casts:

• bit<1> ↔ bool: converts the value 0 to false, the value 1 to true, and vice versa.
• int → bool: only if the int value is 0 (converted to false) or 1 (converted to true)
• int → bit: preserves all bits unchanged and reinterprets negative values as positive values
• bit → int: preserves all bits unchanged and reinterprets values whose most-significant bit is 1 as negative values
• bit → bit: truncates the value if W > X, and otherwise (i.e., if W <= X) pads the value with zero bits.
• int → int: truncates the value if W > X, and otherwise (i.e., if W < X) extends it with the sign bit.
• bit → int: preserves the value unchanged but converts it to an unlimited-precision integer; the result is always non-negative
• int → int: preserves the value unchanged but converts it to an unlimited-precision integer; the result may be negative
• int → bit: converts the integer value into a sufficiently large two's complement bit string to avoid information loss, and then truncates the result to W bits. The compiler should emit a warning on overflow or on conversion of negative value.
• int → int: converts the integer value into a sufficiently-large two's complement bit string to avoid information loss, and then truncates the result to W bits. The compiler should emit a warning on overflow.
• casts between two types that are introduced by typedef and are equivalent to one of the above combinations.
• casts between a typedef and the original type.
• casts between a type introduced by type and the original type.
• casts between an enum with an explicit type and its underlying type

@jnfoster is my understanding correct that these are indeed examples of inserting implicit casts? And if so, just out of curiosity, is there a specific reason why P4 spec doesn't consider them as casts?

Also, for reference, the typing rules for assignment in our formalization are:

Quick fix

Add the followings to P4 spec PR:

• [ ] casts discussed in issue #380
• [x] assignment sometimes may require inserting an implicit cast in section 12.1

[jnfoster]

I'm not sure I fully understand the question here. But there are two things going on:

• The P4 type checker sometimes inserts implicit casts.
• There are a set of explicit casts that the programmer is allowed to insert. I think these two categories are meant to be compatible (every implicit cast is also a legal explicit cast) but it's possible the spec has drifted.

I think "automatic conversion" means "implicit cast." We should edit the spec to use consistent terminology.

[pataei]

added to the casting issue on P4 spec repo.