&& and || should short-circuit

[hackedy]

In the P4light and P4cub semantics both operands of short-circuiting operators like && and || are always evaluated, which disagrees with the spec. The spec calls for short-circuiting. Maybe we can desugar them to ternary operators, which appear to do the right thing?

8.1. Expression evaluation order

Given a compound expression, the order in which sub-expressions are evaluated is important when the sub-expressions have side-effects. P4 expressions are evaluated as follows:

• Boolean operators && and || use short-circuit evaluation—i.e., the second operand is only evaluated if necessary.
• The conditional operator e1 ? e2 : e3 evaluates e1, and then either evaluates e2 or e3.
• All other expressions are evaluated left-to-right as they appear in the source program.

[hackedy]

u && v   ==>   u ?    v : false
u || v   ==>   u ? true : v

[hackedy]

re: ternary operators, I spoke too soon. In SimplExpr:

    | ExpTernary cond tru fls =>
      let '(l1, e1, n1) := transform_exp nameIdx cond in
      let '(l2, e2, n2) := transform_exp n1 tru in
      let '(l3, e3, n3) := transform_exp n2 fls in
      (* Qinshi: This is incorrect. l2/l3 is only evaluated when the boolean is true/false. *)
      (l1 ++ l2 ++ l3, MkExpression tag (ExpTernary e1 e2 e3) typ dir, n3)

[hackedy]

Parisa and I think that to fix this we have to add conditionals to P4light and P4cub declarations. To see why, imagine lifting function calls out of expressions in the following example, which should assign 0 to hdr.

bit<8> f(inout bit<8> y) { y = 0; return 0; }
bit<8> g(inout bit<8> y) { y = 1; return 1; }

control MyIngress(inout bit<8> hdr,
                  inout metadata meta,
                  inout standard_metadata_t standard_metadata) {
  bit<8> y = 0xFF;
  bit<8> z = true ? f(y) : g(y);
  apply {
    hdr = y;
  }
}

@QinshiWang @rudynicolop your thoughts?

[rudynicolop]

I'm not sure how else one would do it. Maybe by creating a new function for these cases and calling that here?

For this example I'm not sure because function calls aren't allowed in the top level of control declarations?

[hackedy]

Both p4c and petr4 accept this program and the spec does not explicitly disallow it, so I think it's legal. There's also this note which is about extern functions but seems applicable.

One way that an extern can be called from the top level of a parser or control is in an initializer expression for a declared variable, e.g. bit<32> x = rand.get();.