Specify semantics for the modulus (%) operator

Minres / CoreDSL

Xtext project to parse CoreDSL files

Apache License 2.0

14 stars 2 forks source link

Specify semantics for the modulus (%) operator #25

Closed jopperm closed 1 year ago

jopperm commented 2 years ago

From the wiki-spec: https://github.com/Minres/CoreDSL/wiki/Expressions#modulus

Specify concrete semantics for this operation (as modulo is always contentious), and check the u1 % s2 case as it may yield an (invalid!) unsigned<0> type.

jopperm commented 1 year ago

Done. (diff)

For future reference, given a % b:

The sign of a determines the sign of the expression.
If a is positive, the result is in the range [0, min(a, |b|-1)]
If a is negative, the result is in the range [max(a, -|b|+1), 0]
Example why we have (w2 +1) in the rule for the signed<w1> % unsigned<u2> case:
```
signed<6>   a = -28;
unsigned<4> b = 15;
a % b == -13 ∉ signed<4>
```