verified-network-toolchain / petr4

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

Poulet4 supports directionless parameters #300

Open QinshiWang opened 2 years ago

QinshiWang commented 2 years ago

P4 allows using directionless parameters to pass (compile-time known) objects to functions. For example,

void count(direct_counter c, bool flag) {
    if(flag)
        c.count();
}

This is supported by the Petr4 interpreter, but not by the poulet4 semantics. Poulet4 supports a special treatment for packet_in and packet_out by converting them to constructor parameters with hard-coded object references. For other kinds of directionless parameters, we support value parameters (e.g. mathematical integer and string), but not objects. We can do that by unrolling.

In general, I would like to ask for opinions.

QinshiWang commented 2 years ago

@andrew-appel