[P4Testgen] incorrect handling of setInvalid() called on headers in unions

[p-sawicki]

The spec specifies that calling setInvalid() on any header inside a header union should invalidate all headers in that union:

u.hi.setInvalid(): if the valid bit for any member header of u is true then sets it to false, which implies that it is unspecified what value reading any member header of u will return.

However, Testgen doesn't expect all the headers to be invalidated, only the one on which setInvalid() is called.

Example source code:

#include <v1model.p4>

header opt_t {
    bit<8> opt;
}

header ethernet_t {
    bit<48> dst_addr;
    bit<48> src_addr;
    bit<16> eth_type;
}

header H {
    bit<8> a;
    bit<8> a1;
    bit<8> b;
}

header_union U {
    ethernet_t e;
    H h;
}

struct Headers {
    opt_t opt;
    U u;
}

struct Meta {}

parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) {
    state start {
        pkt.extract(h.opt);
        transition select(h.opt.opt) {
            0x0: parse_e;
            0x1: parse_h;
            default: accept;
        }
    }

    state parse_e {
        pkt.extract(h.u.e);
        transition accept;
    }

    state parse_h {
        pkt.extract(h.u.h);
        transition accept;
    }
}

control vrfy(inout Headers h, inout Meta meta) {
    apply { }
}

control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) {
    apply {
        h.u.e.setInvalid();
    }
}

control egress(inout Headers h, inout Meta m, inout standard_metadata_t s) {
    apply { }
}

control update(inout Headers h, inout Meta m) {
    apply { }
}

control deparser(packet_out pkt, in Headers h) {
    apply {
        pkt.emit(h);
    }
}

V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main;

Command:

./p4testgen --target bmv2 --test-backend stf main.p4 --max-tests 0

Output (main_3.stf):

# p4testgen seed: none
# Date generated: 2024-02-22-03:05:10.778
# Current node coverage: 0
# Traces
# [P4Testgen MethodCall]: *.copy_in("p");
# [Parser] p
# [State] start
# [MethodCall]: pkt.extract<opt_t>(h.opt);
# [ExtractSuccess] h.opt@0 | Condition: |*packetLen_bits(bit<32>)| >= 8; | Extract Size: 8 -> h.opt.opt = 0x01
# [State] parse_h
# [MethodCall]: pkt.extract<H>(h.u.h);
# [ExtractSuccess] h.u.h@8 | Condition: |*packetLen_bits(bit<32>)| >= 32; | Extract Size: 24 -> h.u.h.a = 0x00 | h.u.h.a1 = 0x00 | h.u.h.b = 0x00
# [State] accept
# [P4Testgen MethodCall]: *.copy_out("p");
# [P4Testgen MethodCall]: *.copy_in("vrfy");
# [Control vrfy start]
# [P4Testgen MethodCall]: *.copy_out("vrfy");
# [P4Testgen MethodCall]: *.copy_in("ingress");
# [Control ingress start]
# [MethodCall]: h.u.e.setInvalid();
# [P4Testgen MethodCall]: *.copy_out("ingress");
# [P4Testgen AssignmentStatement]: *standard_metadata.egress_port = 0;
# [P4Testgen If Statement]: 0 != 0; Condition: 0 != 0; Result: false
# [P4Testgen MethodCall]: *.copy_in("egress");
# [Control egress start]
# [P4Testgen MethodCall]: *.copy_out("egress");
# [P4Testgen MethodCall]: *.copy_in("update");
# [Control update start]
# [P4Testgen MethodCall]: *.copy_out("update");
# [P4Testgen MethodCall]: *.copy_in("deparser");
# [Control deparser start]
# [MethodCall]: pkt.emit<opt_t>(h.opt);
# [Emit]: {$headerValid:1;;    opt:1;  }
# [MethodCall]: pkt.emit<ethernet_t>(h.u.e);
# [Invalid emit: { dst_addr = TaintedExpression(bit<48>), src_addr = TaintedExpression(bit<48>), eth_type = TaintedExpression(bit<16>) }]
# [MethodCall]: pkt.emit<H>(h.u.h);
# [Emit]: {$headerValid:1;;    a:0;  a1:0;  b:0;  }
# [P4Testgen MethodCall]: *.copy_out("deparser");
# [P4Testgen MethodCall]: *.prepend_emit_buffer();
# [Prepending the emit buffer to the program packet]
# [P4Testgen If Statement]: 511 == 0; Condition: 511 == 0; Result: false
# [P4Testgen MethodCall]: *.invoke_traffic_manager();


packet 0 01000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
expect 0 01000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000$

This emit should be invalid:

# [MethodCall]: pkt.emit<H>(h.u.h);
# [Emit]: {$headerValid:1;;    a:0;  a1:0;  b:0;  }

[fruffy]

Yeah... we have always punted this specification detail. Support for header unions and varbits is brittle. Let me see whether there is an easy way to implement it

[fruffy]

Actually, the reason this might be modeled incorrectly is that BMv2 also has the same behavior. The test, as written, passes. If I add code to set other headers invalid I am seeing mismatches.

@antoninbas Does BMv2 model this behavior? It looks like remove_header doesn't account for unions either?

[antoninbas]

@antoninbas The best way to handle this as of now would be for the backend to generate a remove_header call for every header that constitutes the union.

[jafingerhut]

Agreed with Antonin's assessment. The bug is in the combination of the behavior of the p4c BMv2 back end, combined with BMv2. Modifications to either (or both) of them could correct the issue.

[fruffy]

Added an implementation in this PR: #4853