Fixing bug in ParserUnroll for infinite loops without header stacks

[VolodymyrPeschanenkoLitSoft]

These changes allow leaving as is the infinite loops for programs without extraction of the header stack (#3537)

[fruffy]

Does this also fix issue281?

[kfcripps]

This does fix the specific case described in #3537, but ParsersUnroll still produces semantically different IR for the following case:

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

header header_h {
    bit<8> field_1;
    bit<8> field_2;
}

struct M {
    bit<8> field_1;
    bit<8> field_2;
}

struct H {
    header_h hdr_1;
    header_h hdr_2;
    header_h hdr_3;
};

parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) {
    bit<8> local_1;

    state start {
        transition state_2;
    }

    state state_2 {
        packet.extract(hdr.hdr_1);
        local_1 = hdr.hdr_1.field_1;
        transition state_3;
    }

    state state_3 {
        transition state_4;
    }

    state state_4 {
        transition select(local_1) {
            1: state_end;
            2: state_5;
        }
    }

    state state_5 {
        transition state_6;
    }

    state state_6 {
        local_1 = local_1 + 1;
        transition state_7;
    }

    state state_7 {
        transition state_4;
    }

    state state_end {
        transition 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;

The following is produced:

#define V1MODEL_VERSION 20180101
#include <v1model.p4>

header header_h {
    bit<8> field_1;
    bit<8> field_2;
}

struct M {
    bit<8> field_1;
    bit<8> field_2;
}

struct H {
    header_h hdr_1;
    header_h hdr_2;
    header_h hdr_3;
}

parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) {
    @name("ParserI.local_1") bit<8> local;
    state stateOutOfBound {
        verify(false, error.StackOutOfBounds);
        transition reject;
    }
    state noMatch {
        verify(false, error.NoMatch);
        transition reject;
    }
    state start {
        packet.extract<header_h>(hdr.hdr_1);
        local = hdr.hdr_1.field_1;
        transition state_4;
    }
    state state_4 {
        transition select(local) {
            8w1: state_end;
            8w2: state_5;
            default: noMatch;
        }
    }
    state state_41 {
        transition stateOutOfBound;
    }
    state state_5 {
        local = local + 8w1;
        transition state_41;
    }
    state state_end {
        transition 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;

using:

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

[kfcripps]

Here is yet another example for which this transformation produces semantically different IR:

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

struct H { }

struct M { }

parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) {
    state start {
        transition s0;
    }

    state s0 {
        transition s1;
    }

    state s1 {
        packet.advance(16);
        transition select(packet.lookahead<bit<16>>()) {
            0 : s1;
            default : s2;
        }
    }

    state s2 {
        transition s3;
    }

    state s3 {
        packet.advance(16);
        transition select(packet.lookahead<bit<16>>()) {
            0 : s1;
            1 : s2;
            default : s4;
        }
    }

    state s4 {
        transition 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;

This produces:

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

struct H {
}

struct M {
}

parser ParserI(packet_in packet, out H hdr, inout M meta, inout standard_metadata_t smeta) {
    @name("ParserI.tmp_0") bit<16> tmp_0;
    @name("ParserI.tmp_2") bit<16> tmp_2;
    state stateOutOfBound {
        verify(false, error.StackOutOfBounds);
        transition reject;
    }
    state s1 {
        packet.advance(32w16);
        tmp_0 = packet.lookahead<bit<16>>();
        transition select(tmp_0) {
            16w0: s11;
            default: s2;
        }
    }
    state s11 {
        transition stateOutOfBound;
    }
    state s12 {
        transition stateOutOfBound;
    }
    state s2 {
        packet.advance(32w16);
        tmp_2 = packet.lookahead<bit<16>>();
        transition select(tmp_2) {
            16w0: s12;
            16w1: s21;
            default: s4;
        }
    }
    state s21 {
        transition stateOutOfBound;
    }
    state s4 {
        transition accept;
    }
    state start {
        transition s1;
    }
}

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;

because the pass does not consider that packet_in::advance() advances the packet offset.

I am a little concerned that this pass may be overly liberal in classifying loops as infinite loops. Other backends may define externs similar to packet_in::advance() that may advance the packet cursor without this pass knowing about it, and as a result ParsersUnroll will end up incorrectly classifying non-infinite loops as infinite.

[VolodymyrPeschanenkoLitSoft]

Does this also fix issue281?

Yes, It does

[VolodymyrPeschanenkoLitSoft]

@kfcripps, Thanks for another example. I added it to the test suite of the ParserUnroll.

[kfcripps]

@VolodymyrPeschanenkoLitSoft This PR seems to fix the problems I have been experiencing, thank you.

[mihaibudiu]

Fixes #3537

[kfcripps]

I noticed that when I build test testdata/p4_16_samples/parser-unroll-issue3537-1.p4, the following warning is emitted:

[--Wwarn=invalid] warning: Parser cycle without extracting any bytes:
Parser ParserI state chain: start, s1, s2, s2

Why is this warning printed here? Why do I care that I have a parser cycle that doesn't extract any bytes? In the case of this example, I only want to advance the packet cursor without extracting any headers, so I'm not sure what I can do to get rid of this warning.

[mihaibudiu]

@kfcripps if you think this is a problem you should probably file a new issue, this comment will get lost attached to a closed PR.
It may be that the "advance" call is not accounted in the code that checks whether the packet pointer has been advanced.
In general you can silence warnings with the @noWarn annotation, which in this case you should attach to the parser that contains the cycle.