[m-dev.] proposal: specifying integer overflow behaviour, representations etc

[Peter Wang]

On Sat, 14 Apr 2018 08:56:48 -0400 (EDT), Julien Fischer <jfischer at opturion.com> wrote:
> 
> Hi all,
> 
> Below are four proposed changes to the language and one to the implementation.
> I would like a yes or no on these before I do any further work adding them
> to the reference manual / implement the change.
> 
> The proposed language changes are:
> 
>     1. Mercury's builtin signed integer types must use two's complement
>        representation.

Ok.

> 
>     2. The minimum width of the builtin types int and uint is 32 bits.

Ok.

> 
>     3. On overflow, operations on Mercury's builtin unsigned integer types will
>        produce a value that is congruent modulo 2^n to the true mathematical
>        result of the operation (i.e. it will wrap around).  n being the width
>        of the integer.

Ok.

> 
>     4. On overflow, operations on Mercury's builtin signed integer types will produce
>        a result that is the low-order bits of the true two's complement result (i.e
>        it will wrap around).
> 

Ok if overflow checking can be enabled:

> For 3 and 4, the behaviour specified above is the behaviour to be required when
> the implementation does *not* check for overflow.
>

It does seem a bit strange to specify behaviour but also say that a
correct program cannot depend on it.

> The only thing that needs to change in the implementation is that we do not
> technically have (4) for the C backends.  In order to get it, we either need to
> compile with GCC's -fwrapv option enabled (or the equivalent for  other C
> compilers), or change the code generator so that the following Mercury
> 
>     X : int + Y : int
> 
> gets compiled into the following C:
> 
>     (MR_Integer)((MR_Unsigned)X + (MR_Unsigned)Y)
> 
> Similarly, for subtraction and multiplication.  The latter is my preferred
> option as I'm not sure if all of the C compilers have an equivalent to the
> -fwrapv option and it is more user-proof in any case.

Me too.

This will prevent the use of UndefinedBehaviorSanitizer to check for
integer overflow in Mercury code, until an overflow checking option is
added to the Mercury compiler. I haven't used UBSan seriously yet though.

Peter