verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
74 stars 20 forks source link

Conditionals and constants #379

Open jnfoster opened 1 year ago

jnfoster commented 1 year ago

Andrew Pinski raised this issue on p4c https://github.com/p4lang/p4c/issues/3699

Petr4 currently rejects the program with this error message.

Conditional expressions may not have arbitrary width integer type

However, the language specification (Section 8.5.1) is more permissive:

The first sub-expression e1 must have Boolean type and the second and third sub-expressions must have the same type, which cannot both be arbitrary-precision integers unless the condition itself can be evaluated at compilation time. This restriction is designed to ensure that the width of the result of the conditional expression can be inferred statically at compile time.

We should fix this.