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

ParsersUnroll pass produces semantically different IR #3537

Closed
kfcripps opened this issue Sep 26, 2022 · 1 comment
Closed

ParsersUnroll pass produces semantically different IR #3537

kfcripps opened this issue Sep 26, 2022 · 1 comment
Assignees
@VolodymyrPeschanenkoLitSoft
Labels
bug This behavior is unintended and should be fixed. fixed This topic is considered to be fixed.

Comments

@kfcripps
Copy link
Contributor

kfcripps commented Sep 26, 2022 •
edited
Loading

The following P4-16 code:

#include <core.p4>
#include <v1model.p4>

header h1_t {}
header h2_t {
    bit<16> f1;
}
header h3_t {
    bit<3> pad;
    bit<13> f2;
    bit<8> f3;
}
header h4_t {
    bit<8> f4;
}
header h5_t {}
header h6_t {
    bit<16> f5;
}

struct H {
    h1_t h1;
    h2_t h2;
    h3_t h3;
    h4_t h4;
    h5_t h5;
    h6_t h6;
};
struct M { };

parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) {
    state start {
        packet.extract<h1_t>(hdr.h1);
        packet.extract<h2_t>(hdr.h2);
        transition select(hdr.h2.f1) {
            16w0x800: parse_ipv4;
            16w0x86dd: parse_ipv6;
            default: accept;
        }
    }
    state parse_ipv4 {
        packet.extract<h3_t>(hdr.h3);
        transition select(hdr.h3.f2, hdr.h3.f3) {
            (13w0, 8w6): parse_tcp;
            (13w0, 8w17): parse_udp;
            default: accept;
        }
    }
    state parse_ipv6 {
        packet.extract<h4_t>(hdr.h4);
        transition select(hdr.h4.f4) {
            8w6: parse_tcp;
            8w17: parse_udp;
            default: accept;
        }
    }
    state parse_tcp {
        packet.extract<h5_t>(hdr.h5);
        transition accept;
    }
    state parse_udp {
        packet.extract<h6_t>(hdr.h6);
        transition select(hdr.h6.f5) {
            16w0xcafe: parse_ipv4;
            16w0xffff: reject;
            default: accept;
        }
    }
}

control Aux(inout M meta) {
    apply {
    }
}

control IngressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
    apply {
    }
}

control EgressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
    apply { }
}

control DeparserI(packet_out pk, in H hdr) {
    apply { }
}

control VerifyChecksumI(inout H hdr, inout M meta) {
    apply { }
}

control ComputeChecksumI(inout H hdr, inout M meta) {
    apply { }
}


V1Switch(ParserI(), VerifyChecksumI(), IngressI(), EgressI(),
         ComputeChecksumI(), DeparserI()) main;

when compiled using:

./build/p4test example.p4 --p4runtime-files out.json --arch v1model --target bmv2 --loopsUnroll --top4 ParsersUnroll

produces the following example-MidEnd_37_ParsersUnroll.p4 output:

#include <core.p4>
#define V1MODEL_VERSION 20180101
#include <v1model.p4>

header h1_t {
}

header h2_t {
    bit<16> f1;
}

header h3_t {
    bit<3>  pad;
    bit<13> f2;
    bit<8>  f3;
}

header h4_t {
    bit<8> f4;
}

header h5_t {
}

header h6_t {
    bit<16> f5;
}

struct H {
    h1_t h1;
    h2_t h2;
    h3_t h3;
    h4_t h4;
    h5_t h5;
    h6_t h6;
}

struct M {
}

parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) {
    state stateOutOfBound {
        verify(false, error.StackOutOfBounds);
        transition reject;
    }
    state parse_ipv4 {
        packet.extract<h3_t>(hdr.h3);
        transition select(hdr.h3.f2, hdr.h3.f3) {
            (13w0, 8w6): parse_tcp;
            (13w0, 8w17): parse_udp1;
            default: accept;
        }
    }
    state parse_ipv41 {
        packet.extract<h3_t>(hdr.h3);
        transition select(hdr.h3.f2, hdr.h3.f3) {
            (13w0, 8w6): parse_tcp;
            (13w0, 8w17): parse_udp2;
            default: accept;
        }
    }
    state parse_ipv6 {
        packet.extract<h4_t>(hdr.h4);
        transition select(hdr.h4.f4) {
            8w6: parse_tcp;
            8w17: parse_udp;
            default: accept;
        }
    }
    state parse_tcp {
        packet.extract<h5_t>(hdr.h5);
        transition accept;
    }
    state parse_udp {
        packet.extract<h6_t>(hdr.h6);
        transition select(hdr.h6.f5) {
            16w0xcafe: parse_ipv4;
            16w0xffff: reject;
            default: accept;
        }
    }
    state parse_udp1 {
        packet.extract<h6_t>(hdr.h6);
        transition select(hdr.h6.f5) {
            16w0xcafe: parse_ipv41;
            16w0xffff: reject;
            default: accept;
        }
    }
    state parse_udp2 {
        transition stateOutOfBound;
    }
    state start {
        packet.extract<h1_t>(hdr.h1);
        packet.extract<h2_t>(hdr.h2);
        transition select(hdr.h2.f1) {
            16w0x800: parse_ipv4;
            16w0x86dd: parse_ipv6;
            default: accept;
        }
    }
}

control IngressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
    apply {
    }
}

control EgressI(inout H hdr, inout M meta, inout standard_metadata_t smeta) {
    apply {
    }
}

control DeparserI(packet_out pk, in H hdr) {
    apply {
    }
}

control VerifyChecksumI(inout H hdr, inout M meta) {
    apply {
    }
}

control ComputeChecksumI(inout H hdr, inout M meta) {
    apply {
    }
}

V1Switch<H, M>(ParserI(), VerifyChecksumI(), IngressI(), EgressI(), ComputeChecksumI(), DeparserI()) main;

The transformation produces semantically different IR, as the following path is possible with the original parser: start -> parse_ipv4 -> parse_udp -> parse_ipv4 -> parse_udp -> accept - However, we now end up in the reject instead of accept state (via the path start -> parse_ipv4 -> parse_udp1 -> parse_ipv41 -> parse_udp2 -> stateOutOfBound -> reject) when parsing an identical packet.

This bug was introduced by #3503.
@kfcripps kfcripps mentioned this issue Sep 26, 2022
Merged
@mihaibudiu mihaibudiu added the bug This behavior is unintended and should be fixed. label Sep 26, 2022
Merged
@mihaibudiu mihaibudiu added the fixed This topic is considered to be fixed. label Sep 28, 2022
@fruffy
Copy link
Collaborator

fruffy commented Sep 29, 2022

Fixed by #3538.

@fruffy fruffy closed this as completed Sep 29, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@VolodymyrPeschanenkoLitSoft VolodymyrPeschanenkoLitSoft

Labels
bug This behavior is unintended and should be fixed. fixed This topic is considered to be fixed.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@fruffy @mihaibudiu @kfcripps @VolodymyrPeschanenkoLitSoft