implement saturating arithmetic

[cc10512]

P4 specification: http://github.com/p4lang/p4-spec/pull/609
Reference implementation proposal: https://github.com/p4lang/p4-spec/wiki/saturating#reference-implementation

[antoninbas]

@mbudiu-vmw I have been thinking about this a little bit. Because of the arithmetic engine of bmv2, which operates over arbitrary integers, it looks like I will need to introduce 2 new operations: an unsigned saturating cast ("usat_cast") and a signed saturating cast ("sat_cast"). In each case, the operands will be the expression to cast and the bitwidth of the type. For example:

If X and Y have type bit<8>, the expression X |+| Y will become for bmv2 (in pseudo JSON...):

usat_cast {
    add {
        X
        Y
    }
    8
}

If X and Y have type int<8>, the expression X |+| Y will become:

sat_cast {
    add {
        X
        Y
    }
    8
}

For the signed case, let's assume X is -127 and Y is -2. In arbitrary-precision arithmetic, the result is -129. If the operation was not saturating, the result would be 127 (if you remember, that's what the two_comp_mod operation would produce). For the saturating add, the result is -128.

Note that when sat_cast is used, there is no need for the compiler to add a two_comp_mod operation. Similarly, when usat_cast is used, there should be no need for a mod operation.

In pseudo-code:

unsat_cast(E, bw) {
    max = (1 << bw) - 1;
    min = 0;
    if (E > max) return max;
    if (E < min) return min;
    return E;
}

sat_cast(E, bw) {
    max = (1 << (bw - 1)) - 1;
    min = -(1 << (bw - 1));
    if (E > max) return max;
    if (E < min) return min;
    return E;
}

BTW, I thought about having a single saturating cast operation that would take the boundaries (min and max) instead of the bitwidth, but most operations in bmv2 have 2 operands and not 3.

Let me know what you think and if you think there would be any issues in the compiler side with this solution.

[mihaibudiu]

This looks pretty good.

[cc10512]

Are you using the multiprecision library? What do you do when the width is the same as the native type you use for computing E and the native type overflows (or wraps around)?

[antoninbas]

bmv2 never uses C++ native types for operations. E is computed using libgmp as well.

[cc10512]

+1