From: Pierre-Marie de Rodat <derodat@adacore.com>
To: gcc-patches@gcc.gnu.org
Cc: Yannick Moy <moy@adacore.com>
Subject: [Ada] Fix possible suppressed overflows in arithmetic run-time
Date: Tue, 17 Sep 2019 08:07:00 -0000 [thread overview]
Message-ID: <20190917080634.GA37596@adacore.com> (raw)
[-- Attachment #1: Type: text/plain, Size: 1007 bytes --]
Function Double_Divide computes the division of its parameters
(X / (Y*Z)) in a way that avoids overflows on signed integers, except in
two specific cases, when X = -2**63, abs(Y) = abs(Z) = 1 (leading to an
overflow in -To_Int(Qu)) and when X = -2**63 and Y*Z is large enough
that Qu=0 and so the remainder Ru=2**63 (leading to an overflow in
-To_Int(Ru)), for example with Y = Z = 2**32-1.
This fix avoids the overflow by applying "-" on the unsigned value
before the conversion to signed integer.
The issue cannot manifest as an overflow check failure in our runtime,
as overflow checks are suppressed by using pragma Suppress at the start
of the file. Assuming a machine implements wraparound semantics here,
the result was correct even with the suppressed overflow.
As a result, there can be no test showing the difference.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-09-17 Yannick Moy <moy@adacore.com>
gcc/ada/
* libgnat/s-arit64.adb (Double_Divide): Fix two possible
overflows.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 606 bytes --]
--- gcc/ada/libgnat/s-arit64.adb
+++ gcc/ada/libgnat/s-arit64.adb
@@ -204,9 +204,13 @@ package body System.Arith_64 is
-- Case of dividend (X) sign negative
+ -- We perform the unary minus operation on the unsigned value
+ -- before conversion to signed, to avoid a possible overflow for
+ -- value -2**63, both for computing R and Q.
+
else
- R := -To_Int (Ru);
- Q := (if Den_Pos then -To_Int (Qu) else To_Int (Qu));
+ R := To_Int (-Ru);
+ Q := (if Den_Pos then To_Int (-Qu) else To_Int (Qu));
end if;
end Double_Divide;
reply other threads:[~2019-09-17 8:07 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20190917080634.GA37596@adacore.com \
--to=derodat@adacore.com \
--cc=gcc-patches@gcc.gnu.org \
--cc=moy@adacore.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).