A wider range of serializable enums are well-formed in Petr4 compared to p4 spec

[pataei]

Petr4 defines a wider range of enum as well-formed compared to P4 spec. Specifically, Petr4 only checks that the underlying type is well-formed whereas P4 spec states that the underlying type can only be one of bit<w>, int<w>, or a type name defined by typedef where the base type is a fixed-length (signed or unsigned) integer. Note that Petr4 does check this when a serializable enum is being defined.

Petr4 code

The following is the related block of code for checking if a type is well-formed:

is_well_formed_type env (typ: Typed.Type.t) : bool =
  match saturate_type env typ with
 | ...
 | Enum {typ; _} ->
    begin match typ with
    | None -> true
    | Some typ -> is_well_formed_type env typ
    end
 | ...

The following is the block of code for declaring a serializable enum, however, even here Petr4 doesn't check that the argument passed to the underlying type is constant, that is, Petr4 allows bit<exp> as the underlying type whereas P4 spec only allows bit<w>:

and type_serializable_enum env ctx tags annotations underlying_type (name: P4String.t) (members: (P4String.t * Expression.t) list) =
  let expr_ctx = ExprContext.of_decl_context ctx in
  let underlying_type =
    underlying_type
    |> translate_type env []
    |> saturate_type env
  in
  let underlying_type =
    match underlying_type with
    | Int _ | Bit _ -> underlying_type
    | _ -> raise_mismatch tags "fixed width numeric type for enum" underlying_type
  in
  let member_names = List.map ~f:(fun member -> (fst member).string) members in
  let enum_type: Typed.Type.t =
    Enum { name = name.string; typ = Some underlying_type; members = member_names }
  in
  let add_member (env, members_typed) ((member: P4String.t) , expr) =
    let member_name = QualifiedName {prefix = []; tags = member.tags; name={tags = name.tags; string = name.string ^ "." ^ member.string}} in
    let expr_typed = cast_expression env expr_ctx underlying_type expr in
    match compile_time_eval_expr env expr_typed with
    | Some value ->
       env
       |> CheckerEnv.insert_type_of member_name enum_type
       |> CheckerEnv.insert_const member_name
            (VEnumField { typ_name = name.string;
                          enum_name = member.string }),
       members_typed @ [ member, expr_typed ]
    | None -> failwith "could not evaluate enum member"
  in
  let env = CheckerEnv.insert_type (QualifiedName {prefix=[]; name; tags = name.tags}) enum_type env in
  let env, member_names = List.fold_left ~f:add_member ~init:(env, []) members in
  let enum_typed =
    Prog.Declaration.SerializableEnum { annotations; typ=enum_type; name; members = member_names; tags } in
  enum_typed, env

P4 spec (v1.2.3)

Enumeration types states that: "The symbol typeRef in the grammar above must be one of the following types:

• an unsigned integer, i.e. bit for some constant W.
• a signed integer, i.e. int for some constant W.
• a type name declared via typedef, where the base type of that type is either one of the types listed above, or another typedef name that meets these conditions. For example, the declaration"

Quick fix

Add the check of assert_runtime_numeric and define a helper such as is_constant that checks that exp in bit<exp> or int<exp> is a constant.

[pataei]

• [ ] @pataei check this with examples.

[pataei]

discussed this with Ryan and we're wondering why P4 limits the underlying type of an enum to bit<W> and int<W>, instead of limiting them to be int<exp> or ibt<exp> and requiring exp to be compile-time-known. @jnfoster do you know?

[pataei]

This isn't the only place where P4 spec is more restrictive for fixed-length integers. See #397