[m-dev.] proposal: specifying integer overflow behaviour, representations etc
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