p4lang / p4-spec

Apache License 2.0
178 stars 80 forks source link

Allow division and modulo on fixed-width integers #1327

Open vlstill opened 2 weeks ago

vlstill commented 2 weeks ago

Currently, the P416 spec v1.2.5 only defines / and % operation (division and modulo) for arbitrary-width integers (int): see 8.8. Operations on arbitrary-precision integers.

However, the P4C reference compiler allows these operations also on bit<N> type (fixed-width unsigned), and can perform constant folding and even strength reduction of them. For that reason, the user can write a code like this:

my_hdr1.fld_a = my_hdr0.fld_b / 16;

and the code is strength-reduced to

my_hdr1.fld_a = my_hdr0.fld_b >> 4;

and compiles just fine. Indeed, if the target does not invoke P4::CompileTimeOperations midend pass, or otherwise prohibit these operations, and it implements proper code-generation for them, the target may choose to allow fully-runtime division and modulo. Of course, such an operation may not be available on all targets.


I think a more reasonably way to specify this is to allow division and modulo on bit<N> type, and to explicitly state in spec that on certain targets, only division/modulo by a constant (possibly a power-of-two constant) may be allowed. I don't see any strong reason to prohibit targets from supporting these ops.

Furthermore, for the sake of symmetry and elimination of exceptions, I would like to extend these operations on int<N> type too. Here, however, we need to define precisely how division modulo should behave for negative numbers as different languages have different behavior. I am not sure if there is one definition which is considered better.

jonathan-dilorenzo commented 2 weeks ago

Discussed in the P4-LDWG, we decided that there are 3 levels of this:

  1. Allow only constant folded away bit divisions and modulo.
  2. Allow any bit divisions and modulo, noting that targets may restrict this behavior arbitrarily. Suggestion from P4 LDWG is to send a PR to support this.
  3. Allow int modulo and division as well.