p4-spec
p4-spec copied to clipboard
Add equality and inequality comparisons for Issue 960
- We added explicit equality and inequality comparisons for tuples, list expressions, and structure-valued expressions.
- We explained the recursive implicit casts applied when using list and structure-valued expressions. (Do we want to also mention this in the implicit cast section?)
- We elaborated the examples to illustrate these two points.
- We merged
8.15. Structure initializersinto8.12. Structure-valued expressionsand8.14. Operations on struct typesto reduce confusion and redundancy and to make the spec more organized. - We changed the title of section
8.12. Structure-valued expressionsinto8.12. Operations on structure-valued expressionsto make the spec more organized. - We renamed all usages of "structure initializer" with "structure-valued expressions" to be parallel to "list expressions" and to reduce confusion.
Fixes #960 Fixes #953
Note: There is a corner case not covered but this change. For more details, please see the issue report #960.
Hi @MollyDream, this is the ONF bot 🤖 I'm glad you want to contribute to our projects! However, before accepting your contribution, we need to ask you to sign a Contributor License Agreement (CLA). You can do it online, it will take only a few minutes:
✒️ 👉 https://cla.opennetworking.org
After signing, make sure to add your Github user ID MollyDream to the agreement.
For more information or help:" https://wiki.opennetworking.org/x/BgCUI
Can you please delete .DS_Store?
Example program from LDWG chat.
control C<G>(inout G G);
package P<G>(C<G> c);
header h {
bit<8> f;
}
header g {
bool b1;
bool b2;
bool b3;
bit<5> padding;
}
struct s {
bit<8> f;
}
control MyC(inout g my_g) {
h my_h;
s my_s;
tuple<bit<8>> my_t;
apply {
my_g.setValid();
my_g.b1 = { 8w1 } == my_h;
my_g.b2 = { 8w2 } == my_s;
my_g.b3 = { 8w3 } == my_t;
}
}
P(MyC()) main;
- Let's refactor or split this pull request to eliminate structure initializers.
- Regarding the comparison operations, we need to revise the spec to explain the rewriting that the compiler is doing, converting list expressions into structure-value expressions... this needs some thought because we don't have casts for structs and headers.
To summarize what we know at the current status, I am copying over the conclusion from here and here:
it seems tempting to summarize the allowed comparisons as:
- A list expression can be compared with a list expression, a structure-valued expression, a tuple, a struct, or a header for equality (==) or inequality (!=)
- A structure-valued expression can be compared with a list expression, a structure-valued expression, a struct, or a header for quality (==) or inequality (!=)
- Two tuples, two structs, and two headers can be compared for equality (==) or inequality (!=)
These are all true in the p4c compiler, except one corner case: A list expression can be compared with a structure-valued expression if and only if '(' typeRef ')' is explicit.
bool b11 = (S) { a = 1, b = 2 } == {1, 2}; // Good
// bool b12 = { a = 1, b = 2 } == {1, 2}; // Rejected by the BMV2 compiler
We should first examine if these comparisons allowed by p4c are reasonable.
If so, in order to explain the underlying "conversion" from a list expression to a structure-valued expression (which happens in p4c based on Nate's experiment in the last meeting), new types and casts need to be introduced. As a demonstration, in Petr4's type system, a list expression is of the list type and a structure-valued expression is of the record type. Such two types can only be created and used by the P4 compiler internally (similar to the function types in Section 7.2.8.2.)
Ideally, I would like to claim that casts from the list type to the record type, from the list type to the tuple type, and from the record type to the struct/header type are allowed. All nice and clean in explaning the comparisons and the initializations of tuples and structs/headers. But several changes need to happen in the p4c compiler and the spec:
- Since a structure-valued expression now has a well-defined type, and given that comparing two structure-valued expressions (without
'(' typeRef ')')are accepted in p4c,{ a = 1, b = 2 } == {1, 2}should also be allowed in p4c. - In these three new types of casts, the first one (from the list type to the record type) can be only implicit casts since the record type is only internal to the compiler; for the second cast (from the list type to the tuple type), it seems all reasonable to allow explicit casts, e.g.
(tuple<bit<32>, bool) { 10, false }should be allowed; for the last one (from the record type to the struct/header type), grammar needs to be adapted to recognize'(' typeRef ')' expressionas a cast.
I tried to implement this stuff in the compiler by desugaring these constructs by creating some new types for these expressions, but there are some difficulties. In particular, today struct types cannot have int fields, so the compiler has to infer appropriate widths for these integers. Also, the types for expressions that are compared to each other must be consistent. Not entirely trivial.
I created https://github.com/p4lang/p4-spec/pull/1019 which only makes the changes related to removing structure initializers.
@MollyDream do we close this in favor of @jafingerhut's more fine-grained PRs?
I only created one other PR which addressed removing structure initializers. My thinking was that this PR can now be updated to focus solely on any equality/inequality changes that might be desired. I do not know the details of what changes might be desired for equality/inequality purposes.
Ok. @MollyDream do you want to update this over the weekend? If so, we can add it to the list for Monday.
Closing this in favor of @jafingerhut's PRs.