Fix: Predication issue #2345

[anasyrmia]

This PR fixes issue #2345.

The issue was the incorrect order of assignment statements with a function like:
void dummy(inout Headers val) { }
...
action simple_action() {
if (h.eth_hdr.eth_type == 1) {
return;
}
h.eth_hdr.src_addr = 48w1;
// this serves as a barrier
dummy(h);
}

Predication output now looks like the folowing code:
@name("ingress.simple_action") action simple_action() {
hasReturned = false;
{
bool cond;
cond = h.eth_hdr.eth_type == 16w1;
hasReturned = (cond ? true : hasReturned);
}
{
bool cond_0;
cond_0 = !hasReturned;
h.eth_hdr.src_addr = (cond_0 ? 48w1 : h.eth_hdr.src_addr);
val_eth_hdr = (cond_0 ? h.eth_hdr : val_eth_hdr);
h.eth_hdr = (cond_0 ? val_eth_hdr : h.eth_hdr);
}
}

and before these changes were implemented these three lines were falsely aranged:

{
	val_eth_hdr = (cond_0 ? h.eth_hdr : val_eth_hdr);
}
h.eth_hdr.src_addr = (cond_0 ? 48w1 : h.eth_hdr.src_addr);
h.eth_hdr = (cond_0 ? val_eth_hdr : h.eth_hdr);

since h.eth_hdr.src_addr should be assigned to 1 bofore the function call.

The cause of the problem was the need to push a block with dependencies before liveAssignments. Which is now not an issue because all assignments are pushed on rv block from the same vector (liveAssigns), in preorder of if statements. In preorder of assignment statements, statements are pushed on liveAssigns in order they have on the input of predication pass.

The xor test was added since it first showed this problem. This test now also has a correct output. Also, some tests were added, which show adequate behavior when mixing nested if else-es and dependencies.

[mihaibudiu]

I am approving this PR, although I have to confess I don't understand the logic of the code anymore, but we need to fix this bug.
This is a case where I am relying fundamentally on Gauntlet and the Z3 verifier to ensure correctness.
@fruffy : I assume you will torture this logic further; your tool found the bug fixed here previously.

[mihaibudiu]

Could you use the find method instead?

[mihaibudiu]

use vector::insert?

[anasyrmia]

vector::insert can't be used in this case because rv is a BlockStatement pointer, not a vector. Function push_back is defined for BlockStatements. The only way insert could be used here is if it would be defined for BlockStatements.

[mihaibudiu]

your spelling of dependa/ent is inconsistent

[mihaibudiu]

I have filed #2565 to optimize such a pattern.

[anasyrmia]

I will try to handle this optimization.

[fruffy]

Gauntlet does not seem to have any issues with the tests. I will fuzz test until tomorrow and report back.

[mihaibudiu]

This test failed due to a network connectivity issue.

[fruffy]

Fuzz testing revealed an issue with header stacks:

The predication pass collapses

control ingress(inout Headers h) {
    @name("ingress.simple_action") action simple_action() {
        if (h.eth_hdr.src_addr != h.eth_hdr.dst_addr) {
            h.h[0].a = 8w2;
        } else {
            h.h[1].a = 8w1;
        }
    }
    apply {
        simple_action();
    }
}

into

control ingress(inout Headers h) {
    @name("ingress.simple_action") action simple_action() {
        {
            bool cond;
            cond = h.eth_hdr.src_addr != h.eth_hdr.dst_addr;
            h.h[1].a = (cond ? h.h[1].a : 8w1);
        }
    }
    apply {
        simple_action();
    }
}

2564.p4.txt
2564.stf.txt

@mbudiu-vmw That failure seems to happen a lot recently because of Travis rate limiting. Maybe the Travis config can be simplified a little. I will take a look.

[anasyrmia]

Thank you both for your replies.
I've implemented the requested changes regarding the code structure.
The problem with header stacks has been solved the following way:
The condition in if block on the line 203 is what originally caused the problem. This if block is used to remove the statement in liveAssigns vector, in order to not duplicate some assignments. If the code looks something like this (this is just a pseudocode):

bool a = true;
if (a) {
hdr.x = hdr.x + 1;
}
else {
hdr.x = hdr.x + 2;
}

Without the if block on line 203 the output of predication would look like:

hdr.x = a ? hdr.x + 1 : hdr.x;
hdr.x = a ? hdr.x + 1 : hdr.x + 2;

Which is wrong because it adds 1 to hdr.x twice in case 'a' is true.
This code segment checks if statement->left is the same in if block and in else block of p4 code. If it is the same, it removes the first and only keeps the second statement (hdr.x = a ? hdr.x + 1 : hdr.x + 2; in this example).

The condition wasn't correct, so some assignments were falsely removed (in 2564.p4 test the line: h.h[0].a = (cond ? 8w2 : h.h[0].a);). In this example the condition didn't see the difference between h.h[0].a and h.h[1].a because toString() function converted the left sides of both statements to [].a. Now that the condition consists of the comparison of lvalue_names of these headers, this if block won't effect these statements, since their lvlaue_names differ.

[mihaibudiu]

In general, you should not depend on toString(), it is designed for human consumption, not for compiler internals.
Please add a test with arrays.

[anasyrmia]

Thank you for pointing that out. Since I replaced the condition with the comparison of lvalue_names there are no more toString function calls in the solution.
Also, I added the test for header stacks.
Let me know if there is anything else regarding this solution that needs fixing.