p4-spec icon indicating copy to clipboard operation
p4-spec copied to clipboard

Add equality and inequality comparisons for Issue 960

Open MollyDream opened this issue 4 years ago • 10 comments

  • 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 initializers into 8.12. Structure-valued expressions and 8.14. Operations on struct types to reduce confusion and redundancy and to make the spec more organized.
  • We changed the title of section 8.12. Structure-valued expressions into 8.12. Operations on structure-valued expressions to 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.

MollyDream avatar Dec 01 '21 21:12 MollyDream

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

onf-cla-manager[bot] avatar Dec 01 '21 21:12 onf-cla-manager[bot]

Can you please delete .DS_Store?

mihaibudiu avatar Dec 01 '21 21:12 mihaibudiu

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;

jnfoster avatar Jan 24 '22 22:01 jnfoster

  • 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.

jnfoster avatar Jan 24 '22 22:01 jnfoster

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 ')' expression as a cast.

MollyDream avatar Feb 07 '22 17:02 MollyDream

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.

mihaibudiu avatar Feb 07 '22 17:02 mihaibudiu

I created https://github.com/p4lang/p4-spec/pull/1019 which only makes the changes related to removing structure initializers.

jafingerhut avatar Feb 24 '22 21:02 jafingerhut

@MollyDream do we close this in favor of @jafingerhut's more fine-grained PRs?

jnfoster avatar Apr 01 '22 18:04 jnfoster

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.

jfingerh avatar Apr 01 '22 19:04 jfingerh

Ok. @MollyDream do you want to update this over the weekend? If so, we can add it to the list for Monday.

jnfoster avatar Apr 01 '22 19:04 jnfoster

Closing this in favor of @jafingerhut's PRs.

jnfoster avatar Nov 11 '23 13:11 jnfoster