Writes to a header field implicitly read the header valid bit

[mihaibudiu]

Fixes #2890

[mihaibudiu]

@fruffy this is a subtle issue of semantics that you may want to revise in Gauntlet too.
So essentially if you have a header H and a variable H x, the assignment x.a = 1 in fact in a surreptitious way looks at the valid bit of x: the x is not valid, then the assignment may actually do nothing. So any prior statement that sets the valid bit of x is actually live. This shows up in examples like:
x.a = 1; r = x.a;. Here you would think that you can copy-propagate the 1 into r, but this is true only of x is known to be valid.

[mihaibudiu]

The fix is in the def-use analysis: when someone assigns to x.a we mark the valid bit of the enclosing header (if any) as being read by the instruction that makes the assignment.

[fruffy]

How does this relate to #2323? The discussion in this issue prompted me to implicitly propagate in Gauntlet, too

[fruffy]

We should probably find a way to fail tests if they are missing their reference file, so that they do not have to be added in later pull requests.

[mihaibudiu]

I will file a new issue for that.

[mihaibudiu]

#2892

[fruffy]

For example, looking at the copy propagation of programs such as header-bmv2.p4

control ingress(inout Headers h, inout Meta m, inout standard_metadata_t sm) {
    @name("ingress.c.tmp") hdr c_tmp;
    apply {
        c_tmp.setInvalid();
        c_tmp.f = h.h.f + 32w1;
        h.h.f = c_tmp.f;
        sm.egress_spec = 9w0;
    }
}

control ingress(inout Headers h, inout Meta m, inout standard_metadata_t sm) {
    @name("ingress.c.tmp") hdr c_tmp;
    apply {
        c_tmp.setInvalid();
        c_tmp.f = h.h.f + 32w1;
        h.h.f = h.h.f + 32w1;
        sm.egress_spec = 9w0;
    }
}

This is still acceptable behavior, right? Since h.h.f is reading from an uninitialized variable.

[mihaibudiu]

How does this relate to #2323? The discussion in this issue prompted me to implicitly propagate in Gauntlet, too

I think propagating through invalid header field is a legal behavior. The result is undefined anyway, and this is as undefined as anything else.

But I also think that here we are fixing a true bug; the programs before and after were not equivalent.

[mihaibudiu]

Yes, the copy propagation does something that is acceptable. Both the input and output programs have the same undefined behaviors.
What is not acceptable is to make the program less defined. Removing a setValid converts a program with defined behavior into an a program with undefined behavior.

[mihaibudiu]

This upcoming PR will help catch many undefined programs: #2881
The number of warning it is producing shows that this is a very useful analysis.

[fruffy]

Sounds good. I tightened the semantics of Gauntlet accordingly. It reports a lot more issues with undefined behavior now, but those are all benign. The only real issue that is detected is fixed with this pull request. Once it is merged in I will update the tool.