verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
75 stars 21 forks source link

action partial applications are not type safe #394

Open hackedy opened 1 year ago

hackedy commented 1 year ago

The following slight modification of table2.p4 from the custom-stf-tests suite gets past the typechecker but causes a failure in the interpreter ~both on main and~ on poulet4.

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

header head {
    bit<8> v;
}

struct metadata { }

parser MyParser(packet_in packet,
                out head[13] hdr,
                inout metadata meta,
                inout standard_metadata_t standard_metadata) {
    state start {
        transition accept;
    }

}

control MyChecksum(inout head[13] hdr, inout metadata meta) {
    apply { }
}

control MyIngress(inout head[13] hdr,
                  inout metadata meta,
                  inout standard_metadata_t standard_metadata) {
    apply {
        standard_metadata.egress_spec = 1;

    }
}

control MyEgress(inout head[13] hdr,
                 inout metadata meta,
                 inout standard_metadata_t standard_metadata) {

  action a() { 
      hdr[0].v = 0;
      hdr[0].setValid();
  }

  action a_with_control_params(in bit<8> x) { 
      hdr[0].v = x;
      hdr[0].setValid();
  }

  table my_table {
    key = {standard_metadata.egress_spec : exact;
           standard_metadata.ingress_port : ternary;
          }

    actions = {a;
               a_with_control_params(0);
               a_with_control_params(1);
               }
    default_action = a();
    const entries = {
                     (9w0, 9w1 &&& 9w0) : a_with_control_params();
                     (0x02, 0x1181) : a_with_control_params();
                     (0x03, 0x1111) : a_with_control_params();
                     (0x04, 0x1211) : a_with_control_params();
                     (0x04, 0x1311) : a_with_control_params();
                     (0x06, _ )     : a_with_control_params();
                    }
      }

    apply {
        standard_metadata.egress_spec = 6;
        standard_metadata.ingress_port = 1;
        my_table.apply();
        exit;
    }

}

control MyDeparser(packet_out packet, in head[13] hdr) {
    apply {
        packet.emit(hdr[0]);
    }
}

V1Switch(
    MyParser(),
    MyChecksum(),
    MyIngress(),
    MyEgress(),
    MyChecksum(),
    MyDeparser()
    )
main;
hackedy commented 1 year ago

Oops, misinterpreted the error message. This does get stopped by the typechecker on main.

hackedy commented 1 year ago

I think the problem here is that unwrap_action_ref creates an expression with a "dummy type" in it and then get_arg_directions maps that dummy type to an empty list of parameters instead of raising an error. But I don't know what's going on with the typechecker.

hackedy commented 1 year ago

Oops, misinterpreted the error message. This does get stopped by the typechecker on main.

This doesn't appear to be true.