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

[Julien Fischer]

On Sun, 15 Apr 2018, Peter Wang wrote:

> On Sat, 14 Apr 2018 08:56:48 -0400 (EDT), Julien Fischer <jfischer at opturion.com> wrote:

>>
>>     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.

Let me reword that: what I'm doing here is defining what happens when a
a signed integer overflow occurs for an operation and we are not
checking / trapping that overflow.  In that case we define the result to
wrap around.  (Similar to what happens in C# in an unchecked context.)

This does not preclude the implmentation from doing overflow checking /
trapping, it just defines what happens when it doesn't.  (The question
is of the implementation supports overflow checking is a separate one,
which I'm not addressing here.)

>> 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.

Is that an objection?  (Obviously, in the presence of the above signed
integer overflow becomes defined.)

Julien.