verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
73 stars 20 forks source link

GCL Compiler Updates #427

Closed ericthewry closed 1 year ago

ericthewry commented 1 year ago

My (too-)long running branch reflecting gritty bugfixes in the GCL compiler. Let me know what you think? @rudynicolop @hackedy ?

There are a few outstanding bugs that still need investigating.

hackedy commented 1 year ago

Huge. Massive. I will try to take a closer look tomorrow

ericthewry commented 1 year ago

Fixed #391 . For an example, observe that ingress for union-valid-bmv2.p4 becomes

control ingress(inout Headers h, inout Meta m, inout standard_metadata_t sm)  {
    action a() { }
    bool t'0;
    table t {
        key = {
            t'0 : exact;
        }
        actions = {
            a();
        }
        default_action = a();
    }
    apply {
        t'0 = h.u.isValid();
        t.apply();
    }
}

hackedy commented 1 year ago

Does the code in this branch handle de bruijn indices?