Opt-out table return value

[QinshiWang]

In P4, tables are often considered free of return value, e.g.

tbl.apply();

But the P4 spec and our semantics describes a return value that is sometimes useful in a if/swtich statement, e.g.

if (ipv4_match.apply().hit) {
    // there was a hit
} else {
    // there was a miss
}
switch (dmac.apply().action_run) {
    Drop_action: { return; }
}

So even in the common case where the return value is ignored, the program logic requires the user to write down the return value. The return value itself is verbose, and I found a slightly better approach using existential quantifier.

Definition tbl_spec : func_spec :=
  WITH (* p *),
    PATH p
    MOD (Some []) []
    WITH,
      PRE
        (ARG []
        (MEM []
        (EXT [])))
      POST
        (EX retv,
        (ARG_RET [] retv
        (MEM []
        (EXT []))))%arg_ret_assr.

But this still requires the user to understand that there is a return value and remember to write it. The user also needs to handle the existential quantifier explicitly when calling this table.

step_call tbl_body.
{ entailer. }
Intros _.

Also, for a table with only one action, e.g.

action act_foo() {
}

table tbl_foo() {
  actions = {
      act_foo();
  }
  default_action = act_foo();
  size = 1;
}

applying the table is just the same as applying the action, so we expect them to have the same func spec. But the difference comes at the return value.

So there are two things we want to have

• a method to ignore tables' return values in func specs and call sites;
• the same func spec for an action and its single-action table.

I think the implementation can be making the meaning of ValBaseNull in return values as "any". This will directly solve the two bullet points. It does not break anything else, because ValBaseNull is now used for void functions, whose return values must be ignored.