Adding serializable enums (or enums with backing types and specified representations).

p4-16/spec/P4-16-spec.mdk

@@ -5,7 +5,7 @@ Author: The P4 Language Consortium
 Heading depth: 5
 Pdf Latex: xelatex
 Document Class: [11pt]article
-Package: [top=1in, bottom=1.25in, left=1in, right=1in]{geometry}
+Package: [top=1in, bottom=1.25in, left=1in, right=1in]geometry
 Package: fancyhdr
 
 Tex Header:
@@ -2026,12 +2026,22 @@ An enumeration type is defined using the following syntax:
 ~ Begin P4Grammar
 enumDeclaration
     : optAnnotations ENUM name '{' identifierList '}'
+    | optAnnotations ENUM typeRef name '{' specifiedIdentifierList '}'
     ;
 
 identifierList
     : name
     | identifierList ',' name
     ;
+
+specifiedIdentifierList
+    : specifiedIdentifier
+    | specifiedIdentifierList ', ' specifiedIdentifier
+    ;
+
+specifiedIdentifier
+    : name '=' initializer
+    ;
 ~ End P4Grammar
 
 For example, the declaration
@@ -2043,10 +2053,55 @@ enum Suits { Clubs, Diamonds, Hearths, Spades }
 introduces a new enumeration type, which contains four
 constants---e.g., `Suits.Clubs`. An `enum` declaration
 introduces a new identifier in the current scope for naming the
-created type. The underlying representation of such values is not
+created type.  The underlying representation of the `Suits` enum is not
 specified, so their "size" in bits is not specified (it is
 target-specific).
 
+It is also possible to specify an `enum` with an underlying representation.
+This requires the programmer provide both the fixed-width integer type and an associated
+fixed-width integer value for each symbolic entry in the enumeration.  For example, the
+declaration
+
+~ Begin P4Example
+enum bit<16> EtherType {
+  VLAN      = 0x8100,
+  QINQ      = 0x9100,
+  MPLS      = 0x8847,
+  IPV4      = 0x0800,
+  IPV6      = 0x86dd
+  // ...
+}
+~ End P4Example
+
+introduces a new enumeration type, which contains five constants---e.g.,
+`EtherType.IPV4`.  This `enum` declaration specifies the fixed-width integer representation
+for each entry in the `enum` and provides an underlying type: `bit<16>`.
+This type of `enum` declaration can be thought of as declaring a new `bit<16>`
+type, where variables or fields of this type are expected to be unsigned 16-bit
+integer values, and the mapping of symbolic to numeric values defined by the
+`enum` are effectively constants defined as a part of this type.  In this way,
+an `enum` with an underlying type can be thought of as being a type derived
+from the underlying type carrying equality, assignment, and casts to/from the
+underlying type.
+
+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.
+
+For example, the declaration
+
+~ Begin P4Example
+enum bit<8> FailingExample {
+  first           = 1,
+  second          = 2,
+  third           = 3,
+  unrepresentable = 300
+}
+~ End P4Example
+
+would result in an error because the fixed-width integer value associated with
+`FailingExample.unrepresentable` cannot be represented as a `bit<8>` value.
+
 Annotations, represented by the non-terminal `optAnnotations`, are
 described in Section [#sec-annotations].
 
@@ -2278,14 +2333,17 @@ infinite-precision integer, without a width specified.
 | `error`        | error     | error   |  allowed |
 | `match_kind`   | error     | error   |  error   |
 | `bool`         | error     | error   |  allowed |
-| `enum`         | error     | error   |  allowed |
+| `enum`         | allowed[^enum_header]     | error   |  allowed |
 | `header`       | error     | allowed |  allowed |
 | header stack   | error     | error   |  allowed |
 | `header_union` | error     | error   |  allowed |
 | `struct`       | error     | error   |  allowed |
 | `tuple`        | error     | error   |  allowed |
 |----------------|-----------|---------|----------|
 
+[^enum_header]: an `enum` type used as a field in a `header` must specify a
+    underlying type and representation for `enum` elements.
+
 Rationale: `int` does not have precise storage requirements,
 unlike `bit<>` or `int<>` types. `match_kind`
 values are not useful to store in a variable, as they
@@ -2717,13 +2775,163 @@ X.v1  // reference to v1
 v1    // error - v1 is not in the top-level namespace
 ~ End P4Example
 
-Similar to errors, `enum` expressions only support equality (`==`)
-and inequality (`!=`) comparisons. Expressions whose type is an `enum`
+Similar to errors, `enum` expressions without a specified underlying type only support equality (`==`)
+and inequality (`!=`) comparisons. Expressions whose type is an `enum` without a specified underlying type
 cannot be cast to or from any other type.
 
-Note that if an `enum` value appears in the control-plane API, the
+An `enum` may also specify an underlying type, such as the following:
+
+~ Begin P4Example
+enum bit<8> E {
+  e1 = 0,
+  e2 = 1,
+  e3 = 2
+}
+~ End P4Example
+
+Note that each symbolic value in the enum must map to a unique fixed-width integer
+representation, for example the `enum` in the following example would result in
+error:
+
+~ Begin P4Example
+enum bit<8> Bad {
+  b1 = 0,
+  b2 = 1,  // Error: b2 and b3 both map to 1
+  b3 = 1,  // one must be changed.
+  b4 = 2
+}
+~ End P4Example
+
+An `enum` with an underlying type also supports explicit casts to and from the
+underlying type.  For instance, the following code:
+
+~ Begin P4Example
+bit<8> x;
+E a = E.e2;
+E b;
+
+x = (bit<8>) a; // sets x to 1
+b = (E) x;      // sets b to E.e2
+~ End P4Example
+
+casts `a`, which was initialized to `E.e2` to a `bit<8>`, using the specified
+fixed-width integer representation for `E.e2`, `1`.  The variable `b` is then set to the
+symbolic value `E.e2`, which corresponds to the fixed-width integer value `1`.
+
+Note that while it is always safe to cast from an `enum` to its fixed-width integer type,
+it may not be the case that every fixed-width integer value specified by the underlying type
+has a related symbol in the `enum`.  For instance, the following code:
+
+~ Begin P4Example
+bit<8> x = 5;
+E e = (E) x; // sets e to an unnamed value
+~ End P4Example
+
+sets `e` to an unnamed value, since there is no symbol corresponding to the
+fixed-width integer value `5`.  While the value of `e` is unspecified, it must not
+correspond to any symbol defined within enum `E`.  This is because casting from
+a fixed-width integer type to an `enum` type is required to obey the following semantics:
+
+Given an enum type $E$ with underlying type `bit<W>` and the set of mappings
+of $(s, n)$ where $S$ is the set of symbols ($s$) and $N$ is the set of fixed-width integer
+representations ($n$), the following properties must hold:
+
+1. if an integer $x \notin N$ then $\forall e \in S$, `(E)x != e`
+1. $\forall x \in [0, 2^W]$, `(bit<W>)(E)x == x`
+1. $\forall e \in S$, `(E)(bit<W>)e == e`
+
+For example, in the following code, the `else` clause of the `if/else if/else`
+block can be reached even though the matches on `x` are complete with respect
+to the symbols defined in `MyPartialEnum_t`:
+
+~ Begin P4Example
+enum bit<2> MyPartialEnum_t {
+    VALUE_A = 2w0,
+    VALUE_B = 2w1,
+    VALUE_C = 2w2
+}
+
+bit<2> y = < some value >;
+MyPartialEnum_t x = (MyPartialEnum_t)y;
+
+if (x == MyPartialEnum_t.VALUE_A) {
+    // some code here
+} else if (x == MyPartialEnum_t.VALUE_B) {
+    // some code here
+} else if (x == MyPartialEnum_t.VALUE_C) {
+    // some code here
+} else {
+    // A P4 compiler MUST ASSUME that this branch can be executed
+    // some code here
+}
+~ End P4Example
+
+Additionally, if an enumeration is used as a field of a header, we would expect
+the `transition select` to match `default` when the parsed integer value does
+not match one of the symbolic values of `EtherType` in the following example:
+
+~ Begin P4Example
+enum bit<16> EtherType {
+  VLAN      = 0x8100,
+  IPV4      = 0x0800,
+  IPV6      = 0x86dd
+}
+
+header ethernet {
+  ...
+  EtherType etherType;
+  ...
+}
+
+parser my_parser(...) {
+  state parse_ethernet {
+    packet.extract(hdr.ethernet);
+    transition select(hdr.ethernet.etherType) {
+      EtherType.VLAN : parse_vlan;
+      EtherType.IPV4 : parse_ipv4;
+      EtherType.IPV6: parse_ipv6;
+      default: reject;
+  }
+}
+~ End P4Example
+
+Any `enum` that contains an unspecifed value, whether as the result of a cast
+to an `enum` with an underlying type, parse into the field of an `enum` with an
+underlying type, or simply the declaration of any `enum` without a specified
+initial value might not be equal to any of the values defined for that
+type.  Such an unspecified value should still lead to predictable
+behavior in cases where any legal value would match, e.g. it should
+match in any of these situations:
+
+- If used in a `select` expression, it should match `default` or `_`
+  in a key set expression.
+- If used as a key with `match_kind` `ternary` in a table, it should
+  match a table entry where the field has all bit positions "don't
+  care".
+- If used as a key with `match_kind` `lpm` in a table, it should match
+  a table entry where the field has a prefix length of 0.
+
+Note that if an `enum` value lacking an underlying type appears in the control-plane API, the
 compiler must select a suitable serialization data type and
 representation.
+For `enum` values with an underlying type and representations, the compiler should
+use the specified underlying type as the serialization data type and
+representation.
+
+In addition to these operations a P4 implementation may choose to implement
+externs for explicitly checking that a fixed-width integer value corresponds to
+a symbolic representation within an `enum` or provide a checked conversion
+extern.
+
+~ Begin P4Example
+extern bool is_valid<Enum, Int>(Int x);
+extern Enum convert<Enum, Int>(Int x, Enum default);
+~ End P4Example
+
+The `is_valid` extern returns `true` for integer values that correspond to
+symbols in the supplied `Enum` type parameter.  The `convert` function returns
+either the symbolic value associated with `x` in `Enum` when one exists, or the
+provided `default`.
 
 ## Expressions on Booleans { #sec-bool-exprs }