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

Julien Fischer jfischer at opturion.com
Sun Apr 15 16:49:44 AEST 2018

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


More information about the developers mailing list