Errors in spec samples

[asl]

The spec contains some samples that cannot be compiled as of now. For example, https://p4.org/p4-spec/docs/p4-16-working-draft.html#sec-ops-on-hdrs mentions:

header H { bit<32> x; bit<32> y; }
H h;
h = {#};   // This make the header h become invalid
if (h == {#}) {     // This is equivalent to the condition !h.isValid()
    // ...
}

Whereas p4c produces:

header.p4(29): [--Werror=type-error] error: 'h = Invalid'
  h = {#}; // This make the header h become invalid
    ^
  ---- Actual error:
header.p4(23): Cannot cast implicitly type 'Unknown type' to type 'header H'
  header H { bit<32> x; bit<32> y; }
         ^
  ---- Originating from:
header.p4(29): Source expression 'Invalid' produces a result of type 'Unknown type' which cannot be assigned to a left-value with type 'header H'
    h = {#}; // This make the header h become invalid
        ^^^
header.p4(23)
  header H { bit<32> x; bit<32> y; }
         ^
header.p4(30): [--Werror=type-error] error: 'h' with type 'header H' cannot be compared to 'Invalid' with type 'Unknown type'
  if (h == {#}) { // This is equivalent to the condition !h.isValid()
      ^
header.p4(23)
header H { bit<32> x; bit<32> y; }
       ^
header.p4(30)
  if (h == {#}) { // This is equivalent to the condition !h.isValid()
           ^^^

I believe I saw other issues with examples as well.

[jafingerhut]

If I recall correctly (the git log on spec and p4c will tell for sure), Mihai Budiu wrote this section of the spec, and the p4c implementation for invalid headers.

He may have left comments in the p4c implementation indicating reasons why this does not work. I am guessing that if the line:

h = {#};

has an explicit cast added to it, like so:

h = (H) {#};

then there is no p4c compile-time error?

[jafingerhut]

I am guessing you considered this possibility as well, but this might be considered as a bug or limitation in the p4c implementation, rather than as a problem with the spec example.

[asl]

Let's view on the problem from slightly broader scope. Currently there is no set of P4 files that comprehensively cover all the aspects of the spec: the ones in p4c/testdata/p4_16_samples are just a pile of unstructured compiler tests, often duplicated and often mixing some language features with compiler issues / feature testcases). And P4C is the only publicly available P4 compiler, so it is certainly considered as a reference one.

Therefore, there is an expectation that P4C is able to compile examples from the spec. If not, it could be:

• Spec being incorrect and needs to be fixed;
• Reference compiler being incorrect and needs to be fixed;
• Both (e.g. when one could determine that the spec requirement could not be implemented unambiguously and therefore both spec and compiler should be aligned given the refined specification).

This is why I opened this issue as further resolution would be necessary:

• Is the spec incorrect and should be fixed?
• Is the type inference in P4C is not powerful enough to disambiguate this case. And if yes, is there any further action required? Still, it would be great to have a footnote in the spec telling that this is not something yet supported.

I checked everything in p4c/testdata/p4_16_samples and all the usage of # literal are in initializers. And always with explicit type cast, e.g.

h = (H){#};

Judging from p4lang/p4c#3667 (comment) it is something that likely was discussed on LDWG, so might be an oversight in spec?

[jafingerhut]

I agree with everything you wrote :-)

And thank you for digging further into the history of this. Very often, unless someone else reading the issue has the full context of what was done in the past in their heads right now, this kind of digging is needed when deciding between the alternatives of "spec needs updating", "p4c has a bug/limitation", or "both of those are true".

My first quick reaction for this issue is "it seems like a reasonable choice to update the spec examples to match what p4c is supporting". This quick reaction is not necessarily the prevailing view of all stakeholders.

[jafingerhut]

And if someone is interested in creating a set of test P4 programs that cover all of the code examples in the spec, and creating issues on the spec and/or p4c when there are discrepancies, that sounds like a useful project.

[asl]

I agree with everything you wrote :-)
My first quick reaction for this issue is "it seems like a reasonable choice to update the spec examples to match what p4c is supporting". This quick reaction is not necessarily the prevailing view of all stakeholders.

Right. Though if this was something discussed at the LDWG, it would be great to check what the resolution it was. Maybe this is something know, et.c

[jafingerhut]

I was likely there if it was discussed, but given it probably happened in late 2022 I have no memory of it. The meeting notes vary in their level of detail, but you are welcome to search through them to see if you can find any notes about it. Note that there were almost certainly multiple meetings discussing several different syntaxes for invalid headers, spread over time -- that I am certain of, so it might be challenging to find the one that addressed the distinction between whether the type of {#} should be automatically inferred by the compiler, or whether the developer must supply it explicitly, always.