From 33ee2b46a9d2f2caa7ec83d4342ab8af36851b20 Mon Sep 17 00:00:00 2001 From: Andy Keep Date: Wed, 2 May 2018 18:08:03 -0400 Subject: [PATCH 1/7] Adding enums with backing types. --- p4-16/spec/P4-16-spec.mdk | 111 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 106 insertions(+), 5 deletions(-) diff --git a/p4-16/spec/P4-16-spec.mdk b/p4-16/spec/P4-16-spec.mdk index e6e66e479c..319cff0587 100644 --- a/p4-16/spec/P4-16-spec.mdk +++ b/p4-16/spec/P4-16-spec.mdk @@ -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,47 @@ 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 numeric type and an associated +numeric 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 numeric representation +for each entry in the `enum` and provides a backing type: `bit<16>`. +Implementations are expected to raise an error if the numeric representation +for an enumeration entry falls outside the representation range of the backing +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 numeric 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,7 +2325,7 @@ 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 | @@ -2286,6 +2333,9 @@ infinite-precision integer, without a width specified. | `tuple` | error | error | allowed | |----------------|-----------|---------|----------| +[^enum_header]: an `enum` type used as a field in a `header` must specify a + backing 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 +2767,64 @@ 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 backing type only support equality (`==`) +and inequality (`!=`) comparisons. Expressions whose type is an `enum` without a specified backing 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` that specifies a backing type, such as the following: + +~ Begin P4Example +enum bit<8> E { + e1 = 0, + e2 = 1, + e3 = 2 +} +~ End P4Example + +also supports explicit casts to and from the backing type. For instance, the +following code: + +~ Begin P4Example +bit<8> x; +E e1 = E.e2; +E e2; + +x = (bit<8>) e1; // sets x to 1 +e2 = (E) x; // sets e to E.e2 +~ End P4Example + +casts `e1`, which was initialized to `E.e2` to a `bit<8>`, using the specified +numeric representation for `E.e2`, `1`. The variable `e2` is then set to the +symbolic value `E.e2`, which corresponds to the numeric value `1`. + +Note that while it is always safe to cast from an `enum` to its numeric type, +it may not be th case that every numeric value specified by the backing 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 unspecified value +~ End P4Example + +sets `e` to an unknown value, since there is no symbol corresponding to the +numeric 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 numeric type to an `enum` type is required obey the following semantics: + +Given an enum type $E$ with underlying type `bit` and the set of mappings +of $(s, n)$ where $S$ is the set of symbols ($s$) and $N$ is the set of numeric +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)(E)x == x` +1. $\forall e \in S$, `(E)(bit)e == e` + +Note that if an `enum` value lacking a backing representation appears in the control-plane API, the compiler must select a suitable serialization data type and representation. +For `enum` values with a backing type and representations, the compiler should +use the specified backing type as the serialization data type and +representation. ## Expressions on Booleans { #sec-bool-exprs } From 34c7fc118a59634ceb8120a56a2751e3a6d32adc Mon Sep 17 00:00:00 2001 From: Andy Keep Date: Fri, 4 May 2018 11:11:28 -0400 Subject: [PATCH 2/7] Addressed the resolved issues in pull request #615 --- p4-16/spec/P4-16-spec.mdk | 86 ++++++++++++++++++++++++++------------- 1 file changed, 57 insertions(+), 29 deletions(-) diff --git a/p4-16/spec/P4-16-spec.mdk b/p4-16/spec/P4-16-spec.mdk index 319cff0587..ea93f148d7 100644 --- a/p4-16/spec/P4-16-spec.mdk +++ b/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: @@ -2058,8 +2058,8 @@ 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 numeric type and an associated -numeric value for each symbolic entry in the enumeration. For example, the +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 @@ -2074,10 +2074,10 @@ enum bit<16> EtherType { ~ End P4Example introduces a new enumeration type, which contains five constants---e.g., -`EtherType.IPV4`. This `enum` declaration specifies the numeric representation -for each entry in the `enum` and provides a backing type: `bit<16>`. -Implementations are expected to raise an error if the numeric representation -for an enumeration entry falls outside the representation range of the backing +`EtherType.IPV4`. This `enum` declaration specifies the fixed-width integer representation +for each entry in the `enum` and provides an underlying type: `bit<16>`. +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 @@ -2091,7 +2091,7 @@ enum bit<8> FailingExample { } ~ End P4Example -would result in an error because the numeric value associated with +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 @@ -2334,7 +2334,7 @@ infinite-precision integer, without a width specified. |----------------|-----------|---------|----------| [^enum_header]: an `enum` type used as a field in a `header` must specify a - backing type and representation for `enum` elements. + underlying type and representation for `enum` elements. Rationale: `int` does not have precise storage requirements, unlike `bit<>` or `int<>` types. `match_kind` @@ -2767,11 +2767,11 @@ X.v1 // reference to v1 v1 // error - v1 is not in the top-level namespace ~ End P4Example -Similar to errors, `enum` expressions without a specified backing type only support equality (`==`) -and inequality (`!=`) comparisons. Expressions whose type is an `enum` without a specified backing type +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. -An `enum` that specifies a backing type, such as the following: +An `enum` may also specify an underlying type, such as the following: ~ Begin P4Example enum bit<8> E { @@ -2781,24 +2781,37 @@ enum bit<8> E { } ~ End P4Example -also supports explicit casts to and from the backing type. For instance, the -following code: +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 e1 = E.e2; -E e2; +E a = E.e2; +E b; -x = (bit<8>) e1; // sets x to 1 -e2 = (E) x; // sets e to E.e2 +x = (bit<8>) a; // sets x to 1 +b = (E) x; // sets e to E.e2 ~ End P4Example -casts `e1`, which was initialized to `E.e2` to a `bit<8>`, using the specified -numeric representation for `E.e2`, `1`. The variable `e2` is then set to the -symbolic value `E.e2`, which corresponds to the numeric value `1`. +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 numeric type, -it may not be th case that every numeric value specified by the backing type +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 @@ -2807,25 +2820,40 @@ E e = (E) x; // sets e to an unspecified value ~ End P4Example sets `e` to an unknown value, since there is no symbol corresponding to the -numeric value `5`. While the value of `e` is unspecified, it must not +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 numeric type to an `enum` type is required obey the following semantics: +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` and the set of mappings -of $(s, n)$ where $S$ is the set of symbols ($s$) and $N$ is the set of numeric +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)(E)x == x` 1. $\forall e \in S$, `(E)(bit)e == e` -Note that if an `enum` value lacking a backing representation appears in the control-plane API, the +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 a backing type and representations, the compiler should -use the specified backing type as the serialization data type and +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(Int x); +extern Enum convert(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 } The following operations are provided on Boolean expressions: From 8b0a64c9c3df03227cda6f8de534bab80d47f30c Mon Sep 17 00:00:00 2001 From: Andy Keep Date: Mon, 7 May 2018 14:03:55 -0400 Subject: [PATCH 3/7] Added examples to the rules on enum, and tried to address @mbudiu-vmw's request to make the enum with underlying type more like a newtype based on the underlying type. --- p4-16/spec/P4-16-spec.mdk | 79 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) diff --git a/p4-16/spec/P4-16-spec.mdk b/p4-16/spec/P4-16-spec.mdk index ea93f148d7..2e93832ecf 100644 --- a/p4-16/spec/P4-16-spec.mdk +++ b/p4-16/spec/P4-16-spec.mdk @@ -2076,6 +2076,14 @@ enum bit<16> EtherType { 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. @@ -2832,6 +2840,77 @@ representations ($n$), the following properties must hold: 1. $\forall x \in [0, 2^W]$, `(bit)(E)x == x` 1. $\forall e \in S$, `(E)(bit)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. From 83b1efade68f63520276aaba087d1a318bb0c776 Mon Sep 17 00:00:00 2001 From: Andy Keep Date: Mon, 7 May 2018 16:51:46 -0400 Subject: [PATCH 4/7] Fixing unknown to unnamed and the set e comment to set b that Andy asked for --- p4-16/spec/P4-16-spec.mdk | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/p4-16/spec/P4-16-spec.mdk b/p4-16/spec/P4-16-spec.mdk index 2e93832ecf..0d24495746 100644 --- a/p4-16/spec/P4-16-spec.mdk +++ b/p4-16/spec/P4-16-spec.mdk @@ -2811,7 +2811,7 @@ E a = E.e2; E b; x = (bit<8>) a; // sets x to 1 -b = (E) x; // sets e to E.e2 +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 @@ -2824,10 +2824,10 @@ 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 unspecified value +E e = (E) x; // sets e to an unnamed value ~ End P4Example -sets `e` to an unknown value, since there is no symbol corresponding to the +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: From 4e90588254828a7c11855d02c553b325d805dc10 Mon Sep 17 00:00:00 2001 From: Andy Keep Date: Thu, 10 May 2018 11:14:08 -0400 Subject: [PATCH 5/7] Revisions to cover (most) of the comments from Mihai and James --- p4-16/spec/P4-16-spec.mdk | 56 +++++++++++++++------------------------ p4-16/spec/grammar.mdk | 10 +++++++ 2 files changed, 32 insertions(+), 34 deletions(-) diff --git a/p4-16/spec/P4-16-spec.mdk b/p4-16/spec/P4-16-spec.mdk index 0d24495746..1fbb0cc5bc 100644 --- a/p4-16/spec/P4-16-spec.mdk +++ b/p4-16/spec/P4-16-spec.mdk @@ -2099,8 +2099,10 @@ enum bit<8> FailingExample { } ~ End P4Example -would result in an error because the fixed-width integer value associated with +would raise an error because `300`, the value associated with `FailingExample.unrepresentable` cannot be represented as a `bit<8>` value. + +The `initializer` expression must be a compile-time known value. Annotations, represented by the non-terminal `optAnnotations`, are described in Section [#sec-annotations]. @@ -2789,15 +2791,26 @@ enum bit<8> E { } ~ 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: +More than one symbolic value in an `enum` may map to the same fixed-with +integer value. ~ Begin P4Example -enum bit<8> Bad { +enum bit<8> NonUnique { b1 = 0, - b2 = 1, // Error: b2 and b3 both map to 1 - b3 = 1, // one must be changed. + b2 = 1, // Note, both b2 and b3 map to the same value. + b3 = 1, + b4 = 2 +} +~ End P4Example + +Additionally, within an `enum` declaration, earlier symbols may be referred to in later +symbol declarations, so `NonUnique` could also be defined as follows. + +~ Begin P4Example +enum bit<8> NonUnique { + b1 = 0, + b2 = 1, // Note, both b2 and b3 map to the same value. + b3 = b2, b4 = 2 } ~ End P4Example @@ -2828,17 +2841,7 @@ 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` 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)(E)x == x` -1. $\forall e \in S$, `(E)(bit)e == e` +fixed-width integer value `5`. 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 @@ -2895,7 +2898,7 @@ parser my_parser(...) { } ~ End P4Example -Any `enum` that contains an unspecifed value, whether as the result of a cast +Any `enum` that contains an unnamed 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 @@ -2918,21 +2921,6 @@ For `enum` values with an underlying type and representations, the compiler shou 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(Int x); -extern Enum convert(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 } The following operations are provided on Boolean expressions: diff --git a/p4-16/spec/grammar.mdk b/p4-16/spec/grammar.mdk index b0fb527f5e..df68e66f56 100644 --- a/p4-16/spec/grammar.mdk +++ b/p4-16/spec/grammar.mdk @@ -334,6 +334,7 @@ structField enumDeclaration : optAnnotations ENUM name '{' identifierList '}' + | optAnnotations ENUM typeRef name '{' specifiedIdentifierList '}' ; errorDeclaration @@ -349,6 +350,15 @@ identifierList | identifierList ',' name ; +specifiedIdentifierList + : specifiedIdentifier + | specifiedIdentifierList ', ' specifiedIdentifier + ; + +specifiedIdentifier + : name '=' initializer + ; + typedefDeclaration : optAnnotations TYPEDEF typeRef name ';' | optAnnotations TYPEDEF derivedTypeDeclaration name ';' From e5be6fa017fff14aff26bb8aba75d9795e95a330 Mon Sep 17 00:00:00 2001 From: Andy Keep Date: Mon, 21 May 2018 10:06:07 -0400 Subject: [PATCH 6/7] addressing latest round of change requests --- p4-16/spec/P4-16-spec.mdk | 22 +++++----------------- 1 file changed, 5 insertions(+), 17 deletions(-) diff --git a/p4-16/spec/P4-16-spec.mdk b/p4-16/spec/P4-16-spec.mdk index 1fbb0cc5bc..e0d3fa6084 100644 --- a/p4-16/spec/P4-16-spec.mdk +++ b/p4-16/spec/P4-16-spec.mdk @@ -2803,18 +2803,6 @@ enum bit<8> NonUnique { } ~ End P4Example -Additionally, within an `enum` declaration, earlier symbols may be referred to in later -symbol declarations, so `NonUnique` could also be defined as follows. - -~ Begin P4Example -enum bit<8> NonUnique { - b1 = 0, - b2 = 1, // Note, both b2 and b3 map to the same value. - b3 = b2, - 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: @@ -2832,8 +2820,8 @@ fixed-width integer representation for `E.e2`, `1`. The variable `b` is then se 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: +and vice versa, there may be cases where casting a fixed-width integer value to +its related `enum` type produces an unnamed value. ~ Begin P4Example bit<8> x = 5; @@ -2898,11 +2886,11 @@ parser my_parser(...) { } ~ End P4Example -Any `enum` that contains an unnamed value, whether as the result of a cast +Any variable with an `enum` type that contains an unnamed 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 +initial value will not be equal to any of the values defined for that +type. Such an unnamed 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: From 8b9f2af29fee059f5d9c12ed5438d54d66a29813 Mon Sep 17 00:00:00 2001 From: Andy Keep Date: Mon, 21 May 2018 16:55:02 -0400 Subject: [PATCH 7/7] Updated explicitly require a bit type for the serializable enum. --- p4-16/spec/P4-16-spec.mdk | 20 ++++++++++---------- p4-16/spec/grammar.mdk | 2 +- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/p4-16/spec/P4-16-spec.mdk b/p4-16/spec/P4-16-spec.mdk index e0d3fa6084..2922fa5ebe 100644 --- a/p4-16/spec/P4-16-spec.mdk +++ b/p4-16/spec/P4-16-spec.mdk @@ -2026,7 +2026,7 @@ An enumeration type is defined using the following syntax: ~ Begin P4Grammar enumDeclaration : optAnnotations ENUM name '{' identifierList '}' - | optAnnotations ENUM typeRef name '{' specifiedIdentifierList '}' + | optAnnotations ENUM BIT '<' INTEGER '>' name '{' specifiedIdentifierList '}' ; identifierList @@ -2058,8 +2058,8 @@ 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 +This requires the programmer provide both the fixed-width unsigned integer type and an associated +fixed-width unsigned integer value for each symbolic entry in the enumeration. For example, the declaration ~ Begin P4Example @@ -2074,7 +2074,7 @@ enum bit<16> EtherType { ~ End P4Example introduces a new enumeration type, which contains five constants---e.g., -`EtherType.IPV4`. This `enum` declaration specifies the fixed-width integer representation +`EtherType.IPV4`. This `enum` declaration specifies the fixed-width unsigned 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 @@ -2084,7 +2084,7 @@ 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 +Compiler implementations are expected to raise an error if the fixed-width unsigned integer representation for an enumeration entry falls outside the representation range of the underlying type. @@ -2816,11 +2816,11 @@ 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`. +fixed-width unsigned integer representation for `E.e2`, `1`. The variable `b` is then set to the +symbolic value `E.e2`, which corresponds to the fixed-width unsigned integer value `1`. -Note that while it is always safe to cast from an `enum` to its fixed-width integer type, -and vice versa, there may be cases where casting a fixed-width integer value to +Note that while it is always safe to cast from an `enum` to its fixed-width unsigned integer type, +and vice versa, there may be cases where casting a fixed-width unsigned integer value to its related `enum` type produces an unnamed value. ~ Begin P4Example @@ -2829,7 +2829,7 @@ 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`. +fixed-width unsigned integer value `5`. 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 diff --git a/p4-16/spec/grammar.mdk b/p4-16/spec/grammar.mdk index df68e66f56..ccfac946ee 100644 --- a/p4-16/spec/grammar.mdk +++ b/p4-16/spec/grammar.mdk @@ -334,7 +334,7 @@ structField enumDeclaration : optAnnotations ENUM name '{' identifierList '}' - | optAnnotations ENUM typeRef name '{' specifiedIdentifierList '}' + | optAnnotations ENUM BIT '<' INTEGER '>' name '{' specifiedIdentifierList '}' ; errorDeclaration