From patchwork Fri Oct 5 14:26:44 2012 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 189493 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) by ozlabs.org (Postfix) with SMTP id EFE392C0080 for ; Sat, 6 Oct 2012 00:27:00 +1000 (EST) Comment: DKIM? See http://www.dkim.org DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d=gcc.gnu.org; s=default; x=1350052021; h=Comment: DomainKey-Signature:Received:Received:Received:Received:Received: Received:Received:Date:From:To:Cc:Subject:Message-ID: MIME-Version:Content-Type:Content-Disposition:User-Agent: Mailing-List:Precedence:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:Sender:Delivered-To; bh=f6ftY9bJDAqQQm/Ht2Sl /t6tpKY=; b=Q2WtmsY0PyUiNoQwebTIUlRiBNSnf+vq5tu4SOT+X6L/Mri38Ail bB5fi029/07RDmZzG8A1sPCQCUKaIOON5HAxtTVdVZ3tQJR6SllkarKCPzaFCTjS maQqyRzDMXTDImZ1Yh0R4v+Zv4+wuRCxZlDWpIW3oc0H1wDqHHy7CfM= Comment: DomainKeys? See http://antispam.yahoo.com/domainkeys DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=default; d=gcc.gnu.org; h=Received:Received:X-SWARE-Spam-Status:X-Spam-Check-By:Received:Received:Received:Received:Received:Date:From:To:Cc:Subject:Message-ID:MIME-Version:Content-Type:Content-Disposition:User-Agent:Mailing-List:Precedence:List-Id:List-Unsubscribe:List-Archive:List-Post:List-Help:Sender:Delivered-To; b=fy8VvyFzJJm4plblG8dR2eBbHHfRvaVXLPtd9EPtZvxhR69WE+MJWTbPeQ3wZN StdFxLlhwg+4V4P4ov36tN/RwasSLhW+T0VgfYTzLI8N3tvc5GsqDqX/wCnTgUm5 wcbUOUH3u7BxX6cllWh7aH7t302xKrNtR+Z+FqhI7tosk=; Received: (qmail 4238 invoked by alias); 5 Oct 2012 14:26:52 -0000 Received: (qmail 4198 invoked by uid 22791); 5 Oct 2012 14:26:51 -0000 X-SWARE-Spam-Status: No, hits=-1.9 required=5.0 tests=AWL, BAYES_00, RCVD_IN_HOSTKARMA_NO X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Fri, 05 Oct 2012 14:26:45 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id BFA111C7D5A; Fri, 5 Oct 2012 10:26:44 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id yH2C2xVvXtUB; Fri, 5 Oct 2012 10:26:44 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 9B75E1C7D27; Fri, 5 Oct 2012 10:26:44 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 99D30919E3; Fri, 5 Oct 2012 10:26:44 -0400 (EDT) Date: Fri, 5 Oct 2012 10:26:44 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Fix static computation of bounds using -gnato2 or -gnato3 Message-ID: <20121005142644.GA8783@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org The code for statically computing bounds for division and exponent was incorrect in some cases, possibly leading to wrong results when -gnato2 or -gnato3 was used. The code for mod and rem was not using optimal bounds, with possible minor consequences on efficiency of the generated code with -gnato2 or -gnato3. Tested on x86_64-pc-linux-gnu, committed on trunk 2012-10-05 Yannick Moy * checks.adb (Minimize_Eliminate_Overflow_Checks): Correct code for the division operation and exponent operation. Adjust bound for the mod and rem operations. Index: checks.adb =================================================================== --- checks.adb (revision 192125) +++ checks.adb (working copy) @@ -1209,7 +1209,7 @@ -- Here we know the result is Long_Long_Integer'Base, of that it has -- been rewritten because the parent operation is a conversion. See - -- Conversion_Optimization.Apply_Arithmetic_Overflow_Checked_Suppressed. + -- Apply_Arithmetic_Overflow_Checked_Suppressed.Conversion_Optimization. else pragma Assert @@ -7087,148 +7087,81 @@ when N_Op_Divide => - -- Following seems awfully complex, can it be simplified ??? + -- If the right operand can only be zero, set 0..0 - Hi := No_Uint; - Lo := No_Uint; + if Rlo = 0 and then Rhi = 0 then + Lo := Uint_0; + Hi := Uint_0; - declare - S : Uint; + -- Possible bounds of division must come from dividing end + -- values of the input ranges (four possibilities), provided + -- zero is not included in the possible values of the right + -- operand. - begin - -- First work on finding big absolute result values. These - -- come from dividing large numbers (which we have in Llo - -- and Lhi) by small values, which we need to figure out. + -- Otherwise, we just consider two intervals of values for + -- the right operand: the interval of negative values (up to + -- -1) and the interval of positive values (starting at 1). + -- Since division by 1 is the identity, and division by -1 + -- is negation, we get all possible bounds of division in that + -- case by considering: + -- - all values from the division of end values of input + -- ranges; + -- - the end values of the left operand; + -- - the negation of the end values of the left operand. - -- Case where right operand can be positive + else + declare + Mrk : constant Uintp.Save_Mark := Mark; + -- Mark so we can release the RR and Ev values - if Rhi > 0 then + Ev1 : Uint; + Ev2 : Uint; + Ev3 : Uint; + Ev4 : Uint; - -- Find smallest positive divisor + begin + -- Discard extreme values of zero for the divisor, since + -- they will simply result in an exception in any case. - if Rlo > 0 then - S := Rlo; - else - S := Uint_1; + if Rlo = 0 then + Rlo := Uint_1; + elsif Rhi = 0 then + Rhi := -Uint_1; end if; - -- Big negative value divided by small positive value - -- generates a candidate for lowest possible result. + -- Compute possible bounds coming from dividing end + -- values of the input ranges. - if Llo < 0 then - Min (Lo, Llo / S); - end if; + Ev1 := Llo / Rlo; + Ev2 := Llo / Rhi; + Ev3 := Lhi / Rlo; + Ev4 := Lhi / Rhi; - -- Big positive value divided by small positive value - -- generates a candidate for highest possible result. + Lo := UI_Min (UI_Min (Ev1, Ev2), UI_Min (Ev3, Ev4)); + Hi := UI_Max (UI_Max (Ev1, Ev2), UI_Max (Ev3, Ev4)); - if Lhi > 0 then - Max (Hi, Lhi / S); - end if; - end if; + -- If the right operand can be both negative or positive, + -- include the end values of the left operand in the + -- extreme values, as well as their negation. - -- Case where right operand can be negative + if Rlo < 0 and then Rhi > 0 then + Ev1 := Llo; + Ev2 := -Llo; + Ev3 := Lhi; + Ev4 := -Lhi; - if Rlo < 0 then - - -- Find smallest absolute value negative divisor - - if Rhi < 0 then - S := Rhi; - else - S := -Uint_1; + Min (Lo, + UI_Min (UI_Min (Ev1, Ev2), UI_Min (Ev3, Ev4))); + Max (Hi, + UI_Max (UI_Max (Ev1, Ev2), UI_Max (Ev3, Ev4))); end if; - -- Big negative value divided by small negative value - -- generates a candidate for largest possible result. + -- Release the RR and Ev values - if Llo < 0 then - Max (Hi, Llo / S); - end if; + Release_And_Save (Mrk, Lo, Hi); + end; + end if; - -- Big positive value divided by small negative value - -- generates a candidate for lowest possible result. - - if Lhi > 0 then - Min (Lo, Lhi / S); - end if; - end if; - - -- Now work on finding small absolute result values. These - -- come from dividing small numbers, which we need to figure - -- out, by large values (which we have in Rlo, Rhi). - - -- Case where left operand can be positive - - if Lhi > 0 then - - -- Find smallest positive dividend - - if Llo > 0 then - S := Llo; - else - S := Uint_1; - end if; - - -- Small positive values divided by large negative values - -- generate candidates for low results. - - if Rlo < 0 then - Min (Lo, S / Rlo); - end if; - - -- Small positive values divided by large positive values - -- generate candidates for high results. - - if Rhi > 0 then - Max (Hi, S / Rhi); - end if; - end if; - - -- Case where left operand can be negative - - if Llo < 0 then - - -- Find smallest absolute value negative dividend - - if Lhi < 0 then - S := Lhi; - else - S := -Uint_1; - end if; - - -- Small negative value divided by large negative value - -- generates a candidate for highest possible result. - - if Rlo < 0 then - Max (Hi, Rlo / S); - end if; - - -- Small negative value divided by large positive value - -- generates a candidate for lowest possible result. - - if Rhi > 0 then - Min (Lo, Rhi / S); - end if; - end if; - - -- Finally, if neither Lo or Hi set (happens if the right - -- operand is always zero for example), then set 0 .. 0. - - if Lo = No_Uint and then Hi = No_Uint then - Lo := Uint_0; - Hi := Uint_0; - - -- If one bound set and not the other copy - - elsif Lo = No_Uint then - Lo := Hi; - - elsif Hi = No_Uint then - Hi := Lo; - end if; - end; - -- Exponentiation when N_Op_Expon => @@ -7264,14 +7197,15 @@ else -- High bound comes either from exponentiation of largest - -- positive value to largest exponent value, or from the - -- exponentiation of most negative value to an odd exponent. + -- positive value to largest exponent value, or from + -- the exponentiation of most negative value to an + -- even exponent. declare Hi1, Hi2 : Uint; begin - if Lhi >= 0 then + if Lhi > 0 then Hi1 := Lhi ** Rhi; else Hi1 := Uint_0; @@ -7279,9 +7213,9 @@ if Llo < 0 then if Rhi mod 2 = 0 then - Hi2 := Llo ** (Rhi - 1); - else Hi2 := Llo ** Rhi; + else + Hi2 := Llo ** (Rhi - 1); end if; else Hi2 := Uint_0; @@ -7316,7 +7250,7 @@ when N_Op_Mod => declare - Maxabs : constant Uint := UI_Max (abs Rlo, abs Rhi); + Maxabs : constant Uint := UI_Max (abs Rlo, abs Rhi) - 1; -- This is the maximum absolute value of the result begin @@ -7371,9 +7305,10 @@ when N_Op_Rem => declare - Maxabs : constant Uint := UI_Max (abs Rlo, abs Rhi); + Maxabs : constant Uint := UI_Max (abs Rlo, abs Rhi) - 1; -- This is the maximum absolute value of the result. Note - -- that the result range does not depend on the sign of B. + -- that the result range does not depend on the sign of the + -- right operand. begin Lo := Uint_0;