-
Notifications
You must be signed in to change notification settings - Fork 441
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
default
expression is accepted in select case expressions with multiple components
#4733
Comments
I may be missing some subtle thing that makes this program's behavior not defined according to the spec, so feel free to point out any aspect of the below that seems wrong:
What am I missing? |
Here is a small test program that runs on BMv2, based on your code but with small changes to enable it to compile and run on BMv2 (e.g. make header type |
@jafingerhut My point is that it seems like an oversight in the spec (I don't see any mention of this in either direction) and/or in the compiler that e.g.
which makes me think that some switch case validation is missing from the compiler. Also, I wonder what would be generated for:
for the BMV2 backend. If you are saying that a switch case label of |
At least according to the specification this seems valid to me? A |
If you want to guarantee in the compiler that you always detect select branches that are unmatchable, in general you will need a satisfiability solver to do it. You can get it with Z3 off the shelf, of course, and if someone wants to implement that, be my guest. The compiler does treat (default, default) the same as default, as far as I can tell from simple experiments. If you have evidence of a bug in this area, definitely good to have a test program that exhibits it. |
There was a pass in the works to remove or simplify overlapping matches but it was never finished: |
@jafingerhut Sure, below are two examples which exhibit different behavior when using The following P4 program:
produces the following warnings:
and the following program produces no warnings or errors:
|
@jafingerhut Skimming through the code, I see some examples where we are only checking whether the switch case label expression, rather than its components (if it is a list expression) is a
The above is not an exhaustive list of places that I noticed this. |
@kfcripps Thanks for pointing those out. My main worry is if the final IR output by the compiler is functionally different from each other, not whether the IR is 100% the same, since obviously many different IR data structures can be functionally equivalent. I realize it is not ideal if the warnings are different, but I have to admit that bothers me less. |
I would guess that if you really wanted all of the select expressions that are equivalent to |
The way I teach P4 programming is to only use |
Yeah, that's why I said that the fact that the compiler accepts this "seemed odd." Maybe this deserves an issue in https://github.com/p4lang/p4-spec as well? Regardless of whether this is allowed by the language or not, I think changes to the compiler are likely needed to either treat e.g.
@jafingerhut The warning itself is not a big deal. It just makes me suspicious that the compiler could be processing e.g. |
The construct |
I would urge us not to create backwards incompatibility without a really, really good reason. |
The following P4 program:
compiles successfully, which seems odd, but I'm not sure what the expected behavior is per the spec.
The text was updated successfully, but these errors were encountered: