Tricky case with uninitialized values...

[jnfoster]

Consider the following program.

control C(inout bit<8> z);
package DummySwitch(C c);

void f(out bit<8> x) { return; }
control MyC(inout bit<8> z) {
  bit<8> y = 0;
  apply {
    f(y);
    if(y - y == 0) {
      z = 1;    
    } else {
      z = 2;
    } 
  }
}

DummySwitch(MyC()) main;

According to the spec, what are the possible final values of z after MyC is executed?

[fruffy-bfn]

It looks to me like it is related to this case #891. The compiler is free to reduce this to z=1; since we are narrowing from undefined behavior. I guess the question is whether to even consider this undefined behavior since we are dealing with a variable that is not read from a header?
Edit: https://github.com/jafingerhut/p4-guide/blob/master/formal-verification/README.md#reading-fields-of-a-header

[jfingerh]

Here is my understanding from version 1.2.1 of the P4_16 language spec.

Any call to f() says that its direction out parameter x need not be initialized to any predictable value. This from Section 6.7. "Calling convention: call by copy in/copy out". In particular, there is a list of bullet points defining the initial value for direction out parameters, and the last one applies to parameter x's type: "If a direction out parameter has any other type, e.g. bit, an implementation need not initialize it to any predictable value."

It seems to me that if you want to capture the maximum amount of undefined-ness allowed by the spec, the answer to the question hinges on whether y is assigned a value during copy-out during the call f(y).

(1) If it is, then we do not know what its value is, but it is some legal value of type bit<8> that does not change from one read to the next. Then the language spec indicates that y-y must evaluates to 0, and the 'then' branch of the if must be taken.

(2) If there is no assignment to y during copy-out, then that doesn't seem to make sense. copy-out is defined to copy some value, even if you cannot predict what value that will be.

So my belief is that the final state z=1 is what the current language spec requires.

Here are a couple of small variations to the program that seem to allow more kinds of behaviors, though, and they are such small variations that I would not be surprised if most compiler writers would not try to preserve the maximum undefined-ness, and instead make transformations that reduce the number of possible final states.

Variant program B:

control C(inout bit<8> z);
package DummySwitch(C c);

control MyC(inout bit<8> z) {
  bit<8> y;
  apply {
    if(y - y == 0) {
      z = 1;    
    } else {
      z = 2;
    } 
  }
}

DummySwitch(MyC()) main;

In variant program B, y has never been initialized at the time the expression y-y is evaluated, so the spec allows each read of y to potentially evaluate to a different value of type bit<8>. Thus an implementation is allowed to end with z equal to either 1 or 2, based on arbitrary criteria.

Variant program C:

control C(inout bit<8> z);
package DummySwitch(C c);

control MyC(inout bit<8> z) {
  bit<8> x;
  bit<8> y;
  apply {
    y = x;
    if(y - y == 0) {
      z = 1;    
    } else {
      z = 2;
    } 
  }
}

DummySwitch(MyC()) main;

In variant program C, x is never initialized, so when we evaluate y = x;, the spec does not define which value is assigned to y, but some value of type bit<8> is assigned to y, so y is no longer uninitialized. Therefore y-y must evaluate to 0, because each evaluation of y should evaluate to the same value, repeatedly, even though the spec doesn't determine what y's value will be.

This is something I puzzled over earlier when thinking about some other P4_16 corner case, and perhaps we don't want future versions of the spec to have such weird cases in it for such similar programs.

Note: I consider all three of these programs to be poor examples of software engineering, and a good P4 compiler and/or lint-like tool should point out the use of uninitialized values.

I do not have an example off-hand of a P4_16 program that raises these questions that I would consider safely written, but I don't have any convincing argument that there are no such programs. The closest thing I can think of there would be using one or more fields in an invalid header as a table key field, but there the language spec has some explicit words that if you attempt to match such a value as a ternary field, it should always predictably match a ternary table entry where that field is completely wildcard in all bit positions. See a mention of "ternary" in Section 8.22. "Reading uninitialized values and writing fields of invalid headers".

[fruffy-bfn]

FunctionInlining does convert the P4 program into case B, meaning it could be possible that undefined behavior is produced from a well-defined program. However, because StrengthReduction(?) and other preceding passes simplify the expression first, the well-defined behavior is preserved. Just a note.

Edit: Actually, taking a closer look: The copy semantics are preserved, a second variable is introduced. So there is no issue in this case. LocalCopyPropagation on the other hand, eliminates the second variable and the copy assignment. Leading, once again, to undefined behavior.

[jnfoster]

In the interest of tidying up the set of active issues on the P4 specification repository, I'm marking this as "stalled" and closing it. Of course, we can always re-open it in the future if there is interest in resurrecting it.