Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Open
p-sawicki opened this issue Feb 22, 2024 · 5 comments · May be fixed by #4853
Open

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

p-sawicki opened this issue Feb 22, 2024 · 5 comments · May be fixed by #4853
Assignees
@fruffy
Labels
bug This behavior is unintended and should be fixed. p4tools Topics related to the P4Tools back end

Comments

@p-sawicki
Copy link
Contributor

p-sawicki commented Feb 22, 2024 •
edited
Loading

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;  }
@p-sawicki p-sawicki added bug This behavior is unintended and should be fixed. p4tools Topics related to the P4Tools back end labels Feb 22, 2024
@fruffy fruffy self-assigned this Feb 22, 2024
@fruffy
Copy link
Collaborator

fruffy commented Feb 22, 2024

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
Copy link
Collaborator

fruffy commented Aug 5, 2024 •
edited
Loading

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?

@fruffy fruffy linked a pull request Aug 5, 2024 that will close this issue
Open
@antoninbas
Copy link
Member

@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
Copy link
Contributor

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
Copy link
Collaborator

fruffy commented Aug 5, 2024

Added an implementation in this PR: #4853

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@fruffy fruffy

Labels
bug This behavior is unintended and should be fixed. p4tools Topics related to the P4Tools back end
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[P4Testgen] Set other headers also invalid when calling setInvalid on a union header. p4lang/p4c
4 participants
@jafingerhut @antoninbas @fruffy @p-sawicki