Implicit cast from int/bit<W> to int should be disallowed

[jaehyun1ee]

P4 inserts implicit casts from int to fixed-width types, but not the other way around.

However, tests issue2444.p4 and issue3283.p4 expects an implicit cast from fixed-width types to int.

// issue2444.p4

const int z2 = 2w3; // cast from bit<2> to int, should be (int) 2w3 instead
const int z3 = 2s3; // cast from int<2> to int, should be (int) 2s3 instead

// issue3283.p4

const int a = {1w1, 1w1} [0]; // should be (int) {1w1, 1w1}[0] instead
const tuple<bit, bit> c = {1w1, 1w1};
const int a1 = c[0]; // should be (int) c[0] instead

[vlstill]

While I think 8.11.2. Implicit casts is pretty clear on this, we might consider adding bit<N> -> int and int<N> -> int implicit casts to the spec as they are always safe (in the sense that they don't truncate the value; unlike the implicit cast int -> bit<N> which is allowed). Of course, this would only work on constants, as there are no non-constant int values.

The downside would be that something like int x = (65000 + 8w4) would be interpreted as int x = (int)((bit<8>)65000 + 8w4) which can be quite confusing because of the overflow!

[ChrisDodd]

I think there's a concern that allowing "loops" in possible implicit cast types could lead to issues when resolving overloading and typechecking, so if an implicit cast A -> B was allowed, an implicit cast B -> A should be disallowed. But that may be resolvable.

[jaehyun1ee]

@vlstill Hmm, but allowing both int -> int/bit<N> and int/bit<M> -> int would in turn allow any combination of implicit casts between int/bit<N> <-> int/bit<M>, which would likely lead to unexpected behavior in programs.

[vlstill]

@vlstill Hmm, but allowing both int -> int/bit<N> and int/bit<M> -> int would in turn allow any combination of implicit casts between int/bit<N> <-> int/bit<M>, which would likely lead to unexpected behavior in programs.

Good point, this would break constants completely :-/.

I don't see other way than to disable the implicit cast you reported, even at risk of breaking existing code.

In some future revision of P4, we might consider a different approach, where unsized constants are of generic integral type instead of int, and allow cast from fixed width to arbitrary width integers. This is what e.g. Haskell does, where e.g. 42 :: Num n => n, i.e. the constant can be any integer and based on the context in which is used it gets the appropriate concrete type.

In P4, that would looks somewhat like this:

int a = 42; // ok
bit<4> b = 42; // ok, no cast, just type specialization
bit<4> c = 4w42; // ok, no cast, no type specialization
int d = 4w42; // error, CHANGE from P4C, not spec, constant is bit<4>
bit<4> e = a; // error, CHANGE, a is `int`, which cannot be implicitly casted to bit<4>
bit<4> f = (bit<4>)a; // ok, CHANGE, explicit cast
int g = b; // ok, CHANGE, implicit cast

But we can't do that now without breaking code as currently e is allowed (I believe).

[ChrisDodd]

In some future revision of P4, we might consider a different approach, where unsized constants are of generic integral type instead of int

That is supposed to be what int is currently -- it is the generic integral type. So implicit casts from bit<N> to int should be disallowed, and I'm not sure why those testcases are not giving an error.

[ChrisDodd]

Looking at the discussion in #2444, it seems that it was decided to add implicit conversions from int/bit<W> to int, in a limited way (so as to still disallow int<N> <-> bit<M>). Doesn't look like anything got added to the spec at the time, however, so it is not terribly rigorous.

[jaehyun1ee]

Thank you @ChrisDodd for the pointer :) But to my understanding, it added implicit casts between bool and int types, so it isn't quite clear why int/bit<2> to int cast is allowed in the above program.

[ChrisDodd]

There's a one-line comment from Mihai that "perhaps that should be allowed", and that it would be added to the discussions for the LDWG. Unfortunately, it looks like note from meetings before 2023 are lost? -- the link at p4lang/p4-spec#904 just points at more recent notes.

[jafingerhut]

There's a one-line comment from Mihai that "perhaps that should be allowed", and that it would be added to the discussions for the LDWG. Unfortunately, it looks like note from meetings before 2023 are lost? -- the link at p4lang/p4-spec#904 just points at more recent notes.

There is a link near the beginning of the "recent meetings notes" doc to a google doc that contains notes from older meetings. That older Google doc does contain notes from the July 2020 meeting.

[vlstill]

There is not much in the document:

Issue p4-spec/#2444
The p4c implementation seems too flexible with respect to infinite-precision integer literals and boolean casts
The root cause is likely that constant folding does not pay attention to the int type
Action items: @mbudiu-vmw will draft a fix to the spec

I think the issue should be #2444 as p4-spec is nowhere near that number of issues.

Anyway, it is unfortunate, as pointed by @jaehyun1ee and @ChrisDodd, having the cast properly defined in both directions brings a lot of problems. It seems to me that the spec maybe only discussed the casts to bool, but the corresponding PR #2658 also allows the cast on integer constants. But it did so only on constants, by the means of constant folding, without changing type checker. (EDIT: Actually there is a type checker modification too). Sadly, constant folding runs even before type checking (!) which is a root of more cases where the P4C accepts code that should be rejected.

My guess is we will not fix this properly until we disentangle type checker from the requirement to see code after constant folding (see also #4634). And any fix will likely break some existing code, causing much inconvenience in the process.

[vlstill]

In some future revision of P4, we might consider a different approach, where unsized constants are of generic integral type instead of int

That is supposed to be what int is currently -- it is the generic integral type. So implicit casts from bit<N> to int should be disallowed, and I'm not sure why those testcases are not giving an error.

If we view int as having that intention, then yes, the current spec makes sense (and the compiler behavior is not correct). The disadvantage is that then it is quite easy to do complex operations on int (possibly involving variables) and then cast the result implicitly to a type that cannot represent it completely.

[vlstill]

The question is what to do with it now:

• revert Allow casts between int and bool #2658's part about constant folding integers and make breaking change to P4 code (we should bump at least minor version of the compiler in that case and declare it clearly in release notes)
• codify this behavior -- basically this is the bi-directional cast :-(

BTW. from quick testing it seems that the any-to-any worst case does not work in P4C, probably because it does not search for a proper chain of casts (as C or C++ compilers do), but for a single cast. I'm not sure what spec has to say about chaining casts.

const bit<4> foo = 4; // OK, wanted; in spec
const int bar = foo; // OK, not in spec
const int<5> baz = bar; // OK, kinda; in spec
const int<5> boo = foo; // ERROR

[jaehyun1ee]

Summarizing the discussion and looking back the previous issue #2444,

const int a =  2w1;
const bool b = (bool)a;

The second one (the code above) does look like a bug, but we may want to allow this one too - a would then be assigned the value 1, and not 2w1.

So the main intention of the following PR #2658 was to allow explicit int -> bool cast (when the int value is 0 or 1), but it also introduced an implicit int/bit<W> -> int cast. Explicit int -> bool cast was also introduced to the spec, while the latter, implicit int/bit<W> -> int cast wasn't. Yet, codifying implicit int/bit<W> -> int cast in the spec, in my opinion, would be undesirable since it introduces bi-directional implicit casts.

I am not familiar with the p4c internals, so I wonder if there is a way to disallow implicit int/bit<W> -> int cast within the frontend while retaining explicit int -> bool cast.