From patchwork Wed Aug 31 08:54:45 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 112469 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 643F3B6F7F for ; Wed, 31 Aug 2011 18:55:07 +1000 (EST) Received: (qmail 19052 invoked by alias); 31 Aug 2011 08:55:05 -0000 Received: (qmail 18991 invoked by uid 22791); 31 Aug 2011 08:55:02 -0000 X-SWARE-Spam-Status: No, hits=-1.8 required=5.0 tests=AWL,BAYES_00 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; Wed, 31 Aug 2011 08:54:47 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id C672A2BAFB1; Wed, 31 Aug 2011 04:54:46 -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 6wWiC5vyg61V; Wed, 31 Aug 2011 04:54:46 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id AB9AB2BAFD0; Wed, 31 Aug 2011 04:54:45 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 9C6A53FEE8; Wed, 31 Aug 2011 04:54:45 -0400 (EDT) Date: Wed, 31 Aug 2011 04:54:45 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Crash on quantified expressions containing 'Old in postconditions Message-ID: <20110831085445.GA1121@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 attribute reference 'Old ppears within a postcondition, but refers to an entity in the enclosing subprogram. If the prefix is a component of a formal its expansion might generate actual subtypes that may be referenced in an inner context, and which must be elaborated within the subprogram itself. As a result we create a declaration for the prefix, insert it in the enclosing subprogram itself and expand it at once. This is properly an expansion activity but it has to be performed now to prevent out-of-order issues in the back-end. the following commands gnatmake -q -gnat12 -gnata my_test my_test must yield: Max = 9 Min = 0 Average = 4 Find 0 in T1 4 Find 9 in T2 4 --- with Simple_Unc_Arrays; use Simple_Unc_Arrays; with Ada.Text_IO; use Ada.Text_IO; procedure My_Test is T1 : Table := (10, (5, 1, 3, 0, 9, 8, 2, 7, 4, 6)); T2 : Table := (10, (4, 8, 6, 9, 0, 1, 7, 2, 5, 3)); T3 : Table (10); begin Put_Line ("Max = " & Max (T1)'img); Put_Line ("Min = " & Min (T1)'img ); Put_Line ("Average = " & Average (T1)'img); Put_Line ("Find 0 in T1 " & Search (T1, 0)'img); Put_Line ("Find 9 in T2 " & Search (T2, 9)'img); T3 := Add (T1, T2); pragma Assert (for all I in 1 .. T3.Last => T3.V (I) = 9); T3 := Bubble_Sort (T1); Quick_Sort (T1); pragma Assert (T1 = T3); end; --- package Simple_Unc_Arrays is -- This should be a generic parameter type Value is new Integer; -- should be range <>; -- This is declaring arrays with a fixed first bound of 1 type Values is array (Positive range <>) of Value; type Table (Last : Natural) is record V : Values (1 .. Last); end record; --------- -- Add -- --------- function Add (A, B : Table) return Table with Pre => Same_Range (A, B), Post => Same_Range (Add'Result, A) and then (for all J in 1 .. A.Last => (Add'Result.V (J) = A.V (J) + B.V (J))); ------------- -- Reverse -- ------------- Procedure Inverse (A : in out Table) with Post => (for all J in 1 .. A.Last => (A.V (J) = A.V'Old (A.Last - J + 1))); -- Reverses the content of A --------- -- Min -- --------- function Min (A : Table) return Value with Pre => not Empty (A), Post => (for all J in 1 .. A.Last => Min'Result <= A.V (J)) and then (for some J in 1 .. A.Last => Min'Result = A.V (J)); -- Returns the minimum value occurring in A --------- -- Max -- --------- function Max (A : Table) return Value with Pre => not Empty (A), Post => (for all J in 1 .. A.Last => Max'Result >= A.V (J)) and then (for some J in 1 .. A.Last => Max'Result = A.V (J)); -- Returns the maximun value occurring in A ------------- -- Average -- ------------- function Average (A : Table) return Value with Pre => not Empty (A), Post => Min (A) <= Average'Result and then Max (A) >= Average'Result; -- Returns the average value in A. Here, the given postcondition does not -- describe completely the value returned. ------------ -- Search -- ------------ function Search (A : Table; V : Value) return Natural with Post => (Search'Result = 0 and then Not_In (A, V, 1 ,A.Last)) or else (A.V (Search'Result) = V and then Not_In (A, V, 1, Search'Result-1)); -- Returns the first index at which value V occurs in array A, or else 0 ----------------- -- Bubble_Sort -- ----------------- function Bubble_Sort (A: Table) return Table with Post => (for all J in 1 .. A.Last - 1 => Bubble_Sort'Result.V (J) <= Bubble_Sort'Result.V (J+1)) and then (for all J in 1 .. A.Last => (for some K in 1 .. A.Last => A.V (J) = Bubble_Sort'Result.V (K))); -- Sorts an array in increasing order by using bubble sort ---------------- -- Quick_Sort -- ---------------- Procedure Quick_Sort (A: in out Table); -- with Post => (for all J in 1 .. A.Last - 1 => A.V (J) <= A.V (J+1)) -- and then (for all J in 1 .. A.Last => -- (for some K in 1 .. A.Last => A.V'Old (J) = A.V (K))); -- Sorts an array in increasing order by using quick sort ----------------- -- utililities -- ----------------- function Empty (A : Table) return Boolean is (1 > A.Last); function Same_Range (A, B : Table) return Boolean is (A.Last = B.Last); function Not_In (A : Table; V : Value; Low : Positive; Up : Natural) return Boolean is (Up > A.Last or else (for all J in Low .. Up => A.V (J) /= V)); procedure Swap (V, W : in out Value) with Post => (V = W'Old and then W = V'Old); -- Swaps two values V and W end Simple_Unc_Arrays; --- package body Simple_Unc_Arrays is --------- -- Add -- --------- function Add (A, B : Table) return Table is begin return C : Table (A.Last) do for I in 1 .. A.Last loop pragma Assert ((for all J in 1 .. I-1 => C.V (J) = A.V (J) + B.V (J)) -- and then (for all K in I .. A.Last => C.V (K) = C.V'old (K))); ); C.V (I) := A.V (I) + B.V (I); end loop; end return; end Add; ------------- -- Reverse -- ------------- procedure Inverse (A : in out Table) is Low : Positive := 1; High : Natural := A.Last; begin while Low < High loop pragma Assert (for all J in 1 .. Low - 1 => (A.V (J) = A.V'Old (A.Last - J + 1)) and then (for all J in Low -1 .. A.Last => (A.V (J) = A.V'Old (J))) ); Swap (A.V (Low), A.V (High)); Low := Low + 1; High := High - 1; end loop; end Inverse; --------- -- Min -- --------- function Min (A : Table) return Value is Res : Value := A.V (1); begin for I in 2 .. A.Last loop pragma Assert (for all J in 1 .. I - 1 => Res <= A.V (J)); if Res > A.V (I) then Res := A.V (I); end if; end loop; return Res; end Min; --------- -- Max -- --------- function Max (A : Table) return Value is begin return Res : Value := A.V (1) do for I in 2 .. A.Last loop pragma Assert (for all J in 1 .. I - 1 => Res >= A.V (J)); if Res < A.V (I) then Res := A.V (I); end if; end loop; end return; end Max; ------------- -- Average -- ------------- function Average (A : Table) return Value is Sum : Value := 0; begin for I in 1 .. A.Last loop Sum := Sum + A.V (I); end loop; return Sum / Value (A.Last); end Average; ------------ -- Search -- ------------ function Search (A : Table; V : Value) return Natural is Pos : Natural := 0; begin for I in A.V'range loop pragma Assert (for all J in 1 .. I - 1 => A.V (J) /= V); if A.V (I) = V then Pos := I; exit; end if; end loop; return Pos; end Search; ----------------- -- Bubble_Sort -- ----------------- function Bubble_Sort (A: Table) return Table is Bull : Boolean := True; Res : Table := A; begin while Bull loop Bull := False; for I in 1 .. Res.Last - 1 loop if Res.V (I + 1) < Res.V (I) then Swap (Res.V (I), Res.V (I+1)); Bull := True; end if; end loop; end loop; return Res; end Bubble_Sort; ---------------- -- Quick_Sort -- ---------------- procedure Quick_Sort (A : in out Table) is procedure Q_S (First, Last : Natural); -- for the recursive call procedure Q_S (First, Last : Natural) is Pivot_Index, Right, Left : Natural; Pivot_Value: Value; begin if First < Last then Pivot_Index := (First + Last + 1) / 2; Pivot_Value := A.V (Pivot_Index); Left := First; Right := Last; loop while Left < Last and then A.V (Left) < Pivot_Value loop Left := Left + 1; end loop; while Right > First and then A.V (Right) > Pivot_Value loop Right := Right - 1; end loop; exit when Left >= Right; Swap (A.V (Left), A.V (Right)); end loop; if Right > First then Q_S (First, Right - 1); end if; if Left < Last then Q_S (Left, Last); end if; end if; end Q_S; begin Q_S (1, A.Last); end Quick_Sort; procedure Swap (V, W : in out Value) is Tmp : Value; begin Tmp := V; V := W; W := Tmp; end Swap; end Simple_Unc_Arrays; Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-31 Ed Schonberg * sem_attr.adb (Analyze_Attribute, case 'Old): If prefix may be a discriminated component of an actual, expand at once to prevent ouf-of-order references with generated subtypes. Index: sem_attr.adb =================================================================== --- sem_attr.adb (revision 178358) +++ sem_attr.adb (working copy) @@ -1939,7 +1939,7 @@ -- Analyze prefix and exit if error in analysis. If the prefix is an -- incomplete type, use full view if available. Note that there are -- some attributes for which we do not analyze the prefix, since the - -- prefix is not a normal name. + -- prefix is not a normal name, or else needs special handling. if Aname /= Name_Elab_Body and then @@ -1950,6 +1950,8 @@ Aname /= Name_UET_Address and then Aname /= Name_Enabled + and then + Aname /= Name_Old then Analyze (P); P_Type := Etype (P); @@ -3772,6 +3774,12 @@ end if; Check_E0; + + -- Prefix has not been analyzed yet, and its full analysis will take + -- place during expansion (see below). + + Preanalyze_And_Resolve (P); + P_Type := Etype (P); Set_Etype (N, P_Type); if No (Current_Subprogram) then @@ -3852,6 +3860,24 @@ end if; end Check_Local; + -- The attribute ppears within a pre/postcondition, but refers to + -- an entity in the enclosing subprogram. If it is a component of a + -- formal its expansion might generate actual subtypes that may be + -- referenced in an inner context, and which must be elaborated + -- within the subprogram itself. As a result we create a declaration + -- for it and insert it at the start of the enclosing subprogram + -- This is properly an expansion activity but it has to be performed + -- now to prevent out-of-order issues. + + if Nkind (P) = N_Selected_Component + and then Has_Discriminants (Etype (Prefix (P))) + then + P_Type := Base_Type (P_Type); + Set_Etype (N, P_Type); + Set_Etype (P, P_Type); + Expand (N); + end if; + ------------ -- Output -- ------------