enum type declaration

[pataei]

• Petr4 allows inserting implicit cast for initializers while P4 spec doesn't state anything explicitly. However, P4 spec has examples that allow this.
• Petr4 doesn't check if an initializer fits into the bounds of its type, however, P4 spec states that: "Compiler implementations are expected to raise an error if the fixed-width integer representation for an enumeration entry falls outside the representation range of the underlying type."

Petr4 code

• The line let expr_typed = cast_expression env expr_ctx underlying_type expr in allows the implicit cast of initializers.
• To the best of my knowledge and investigation of the code, none of the helpers check if an integer is out of bound of its type.

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)

• Example of allowing implicit cast for initializers:

enum bit<8> FailingExample {
  first           = 1,
  second          = 2,
  third           = 3,
  unrepresentable = 300
}

• "Compiler implementations are expected to raise an error if the fixed-width integer representation for an enumeration entry falls outside the representation range of the underlying type."

Fixes

• [x] add implicit casts to rules in the enum declaration in spec and state it explicitly in P4 spec.
• [ ] add a helper that checks value out of bound in Petr4 implementation.

Side note on serializable enums

Note that Petr4 checks that the fixed-width integers have constant size by translating the underlying type from types.type.t to typed.type.t.

[pataei]

added to the casting issue on P4 spec repo.

[pataei]

Neither P4 spec nor Petr4 checks for enum fields to be distinct but I'd imagine a well-formed enum type must have distinct fields.

• [ ] add to P4 spec.
• [x] fix in Petr4.

[hackedy]

I think petr4 rejects enum field dups. E.g. running petr4 typecheck on this program

enum A {
  X,
  X
}

fails with a "constant already defined!" error about A.X. But if it's missing from the definition of type well-formedness we should probably add it to that.

[pataei]

Ahh! Then it must be checked where the constants are inserted. Checked and in fact, it was in insert_const helper function. Thanks Ryan!