p4lang
Should identifiers declared with const be a local compile-time known value if their init expression is?
Originally when I created this issue, I thought that the spec did not say whether identifiers declared const were compile-time known values. Nate quickly pointed out that they are explicitly defined to be so. I then updated this issue to ask: if the initialization expression of an identifier declared const is local compile-time known, should the identifier also be considered local compile-time known?
The text of the original issue appears below:
My evidence:
- They are not in the list of compile-time known values in the specification.
- p4c gives a compile-time error for a program like this (full source code attached):
bit<8> n;
const bit<3> i = 0;
n[i:i] = 0; // <-- compiler error for this line
The error is:
$ mkdir -p tmp
$ p4test --dump tmp --top4 FrontEndLast,FrontEndDump,MidEndLast const-treated-as-compile-time-known-value1.p4
const-treated-as-compile-time-known-value1.p4(72): [--Werror=type-error] error: i: slice bit index values must be constants
n[i:i] = 1;
^
The language spec says about the initializer expression for an identifier declared const: "The initializer expression must be a compile-time known value." Thus it seems that one could consider the identifier as just another name for that compile-time known value.
const-treated-as-compile-time-known-value1.p4.txt
But they are?
https://github.com/p4lang/p4-spec/blob/main/p4-16/spec/P4-16-spec.mdk#L7750
The compiler should be fixed though.
On Fri, Jul 5, 2024 at 4:41 AM Andy Fingerhut @.***> wrote:
My evidence:
- They are not in the list of compile-time known values.
- p4c gives a compile-time error for a program like this (full source code attached):
bit<8> n; const bit<3> i = 0; n[i:i] = 0; // <-- compiler error for this line
The error is:
$ mkdir -p tmp $ p4test --dump tmp --top4 FrontEndLast,FrontEndDump,MidEndLast const-treated-as-compile-time-known-value1.p4 const-treated-as-compile-time-known-value1.p4(72): [--Werror=type-error] error: i: slice bit index values must be constants n[i:i] = 1; ^
The language spec says about the initializer expression for an identifier declared const: "The initializer expression must be a compile-time known value." Thus it seems that one could consider the identifier as just another name for that compile-time known value.
const-treated-as-compile-time-known-value1.p4.txt https://github.com/user-attachments/files/16104263/const-treated-as-compile-time-known-value1.p4.txt
— Reply to this email directly, view it on GitHub https://github.com/p4lang/p4-spec/issues/1290, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAOCFUQ22AR7CN4R2LBHV2TZKYBW5AVCNFSM6AAAAABKMMLSUKVHI2DSMVQWIX3LMV43ASLTON2WKOZSGM4TCNRWGYZDMMQ . You are receiving this because you are subscribed to this thread.Message ID: @.***>
Ugh. I do not know how I missed that. Then they are not allowed as slice indices by p4c because of a p4c limitation? Or because they are compile-time known, but not local compile-time known?
A question:
Today the spec says:
"The following are compile-time known values:
...
- Identifiers declared as constants using the const keyword."
Would it be reasonable to consider tightening it up slightly more, such that identifiers declared as constants using the const keyword are local compile-time known values, if and only if their initialization expression is local compile-time known, otherwise the identifier is only compile-time known?
I personally think this makes sense as a future enhancement to the spec and compiler.
I think that makes sense (it would allow us to give names to local compile-time known values, which is good). The one downside is that it could become increasingly hard to track down what breaks the "local" part of "local compile-time know" -- the fact that something is compile-time known is checked when assigning it as constant's initializer, but it being local compile time known is just implicitly inferred by the compiler.
Now after I read https://github.com/p4lang/p4-spec/issues/1291#issuecomment-2210562317 I rise this question.
Should a local-compile-time-know-ness be a type system property? It makes sense for compile-time-known-ness, so it should be the same for the local version in my opinion. That would probably require enforcing it with a different variable specifier than const. I'm not sure if it is a property of the type system now (but probably yes). The same problem with composition @jnfoster mentioned in #1291 arises here too:
control c(in hdr_t hdr)(bit<3> not_local_compile_time_know) {
apply {
bit<8> n;
const bit<3> i = 0 + not_local_compile_time_known;
n[i:i] = 0; // Now this should be an error!
}
}
Good point. I personally think it would be okay to not track local vs. non-local compile-time known value-ness in the syntax. Of course, internally, an implementation of P4's type system would need to keep track of this distinction. But the rules are simple and compositional, so I think it would be fine to let it be slightly implicit at the level of syntax.
It's true that a small change to an expression could break / make type checking (as in your example). But I personally think this is okay -- the full internal type of i changes depending on the expression that it is initialized with. So to type check the slice, we need to know that type.
@jnfoster Makes sense to me.
We might want to reconsider how we track constness in the implementation though, but that is a task for the compiler -- it might be worth making it actually part of the IR::Type instead of tracking it separately in P4::TypeMap.
Closing this issue, as I believe that the same changes made for https://github.com/p4lang/p4-spec/issues/1305 resolve this issue as well.