From patchwork Tue Oct 26 13:05:45 2010 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 69247 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 40E99B70D2 for ; Wed, 27 Oct 2010 00:06:16 +1100 (EST) Received: (qmail 19265 invoked by alias); 26 Oct 2010 13:06:08 -0000 Received: (qmail 19247 invoked by uid 22791); 26 Oct 2010 13:06:04 -0000 X-SWARE-Spam-Status: No, hits=-1.8 required=5.0 tests=AWL, BAYES_00, T_RP_MATCHES_RCVD X-Spam-Check-By: sourceware.org Received: from mel.act-europe.fr (HELO mel.act-europe.fr) (194.98.77.210) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Tue, 26 Oct 2010 13:05:48 +0000 Received: from localhost (localhost [127.0.0.1]) by filtered-smtp.eu.adacore.com (Postfix) with ESMTP id 3AACECB02EF; Tue, 26 Oct 2010 15:05:46 +0200 (CEST) Received: from mel.act-europe.fr ([127.0.0.1]) by localhost (smtp.eu.adacore.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id b5vDzhufRmF5; Tue, 26 Oct 2010 15:05:46 +0200 (CEST) Received: from saumur.act-europe.fr (saumur.act-europe.fr [10.10.0.183]) by mel.act-europe.fr (Postfix) with ESMTP id 26B5FCB02ED; Tue, 26 Oct 2010 15:05:46 +0200 (CEST) Received: by saumur.act-europe.fr (Postfix, from userid 525) id 0652FD9BB4; Tue, 26 Oct 2010 15:05:45 +0200 (CEST) Date: Tue, 26 Oct 2010 15:05:45 +0200 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Quantified expressions in pre/postconditions and other contexts Message-ID: <20101026130545.GA5227@adacore.com> Mime-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.9i X-IsSubscribed: yes 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 Quantified expressions over arrays typically include indexed expressions over implicit or explicit ranges. The range checks and other code resulting from expansion of the condition in a quantified expression must be inserted at the proper places in the tree. This patch generalizes the mechanism that handles discrete ranges, which previously only appeared in loops and type declarations. With this patch quantified expressions are handled properly when they appear within preconditions and Assert statements. The following must compile quietly; gcc -c -gnat12 -gnata ex1.adb --- package Ex1 is type Extended_Index is range 0 .. 10_000; subtype Index is Extended_Index range 1 .. Extended_Index'Last; type Arr is array (Index range <>) of Natural; function Find_Array (A : Arr; Query : Natural) return Extended_Index with Pre => (for some J in A'Range => (A (J) = Query)), Post => A (Find_Array'Result) = Query; end Ex1; --- package body Ex1 is function Find_Array (A : Arr; Query : Natural) return Extended_Index is Result : Extended_Index := 0; begin for Cur in Index range A'Range loop if A (Cur) = Query then Result := Cur; exit; end if; pragma Assert (for all J in Index range A'First .. Cur => (A (J) /= Query)); end loop; return Result; end Find_Array; end Ex1; Tested on x86_64-pc-linux-gnu, committed on trunk 2010-10-26 Ed Schonberg * sem_ch3.adb (Process_Range_In_Decl): If the range is part of a quantified expression, the insertion point for range checks will be arbitrarily far in the tree. * sem_ch5.adb (One_Bound): Use Insert_Actions for the declaration of the temporary that holds the value of the bounds. * sem_res.adb (Resolve_Quantified_Expressions): Disable expansion of condition until the full expression is expanded. Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 165953) +++ sem_ch3.adb (working copy) @@ -17627,10 +17627,10 @@ package body Sem_Ch3 is Check_List : List_Id := Empty_List; R_Check_Off : Boolean := False) is - Lo, Hi : Node_Id; - R_Checks : Check_Result; - Type_Decl : Node_Id; - Def_Id : Entity_Id; + Lo, Hi : Node_Id; + R_Checks : Check_Result; + Insert_Node : Node_Id; + Def_Id : Entity_Id; begin Analyze_And_Resolve (R, Base_Type (T)); @@ -17738,32 +17738,43 @@ package body Sem_Ch3 is if not R_Check_Off then R_Checks := Get_Range_Checks (R, T); - -- Look up tree to find an appropriate insertion point. - -- This seems really junk code, and very brittle, couldn't - -- we just use an insert actions call of some kind ??? - - Type_Decl := Parent (R); - while Present (Type_Decl) and then not - (Nkind_In (Type_Decl, N_Full_Type_Declaration, - N_Subtype_Declaration, - N_Loop_Statement, - N_Task_Type_Declaration) - or else - Nkind_In (Type_Decl, N_Single_Task_Declaration, - N_Protected_Type_Declaration, - N_Single_Protected_Declaration)) - loop - Type_Decl := Parent (Type_Decl); + -- Look up tree to find an appropriate insertion point. We + -- can't just use insert_actions because later processing + -- depends on the insertion node. Prior to Ada2012 the + -- insertion point could only be a declaration or a loop, but + -- quantified expressions can appear within any context in an + -- expression, and the insertion point can be any statement, + -- pragma, or declaration. + + Insert_Node := Parent (R); + while Present (Insert_Node) loop + exit when + Nkind (Insert_Node) in N_Declaration + and then + not Nkind_In + (Insert_Node, N_Component_Declaration, + N_Loop_Parameter_Specification, + N_Function_Specification, + N_Procedure_Specification); + + exit when Nkind (Insert_Node) in N_Later_Decl_Item + or else Nkind (Insert_Node) in + N_Statement_Other_Than_Procedure_Call + or else Nkind_In (Insert_Node, N_Procedure_Call_Statement, + N_Pragma); + + Insert_Node := Parent (Insert_Node); end loop; -- Why would Type_Decl not be present??? Without this test, -- short regression tests fail. - if Present (Type_Decl) then + if Present (Insert_Node) then - -- Case of loop statement (more comments ???) + -- Case of loop statement. Verify that the range is part + -- of the subtype indication of the iteration scheme. - if Nkind (Type_Decl) = N_Loop_Statement then + if Nkind (Insert_Node) = N_Loop_Statement then declare Indic : Node_Id; @@ -17780,18 +17791,20 @@ package body Sem_Ch3 is Insert_Range_Checks (R_Checks, - Type_Decl, + Insert_Node, Def_Id, - Sloc (Type_Decl), + Sloc (Insert_Node), R, Do_Before => True); end if; end; - -- All other cases (more comments ???) + -- Insertion before a declaration. If the declaration + -- includes discriminants, the list of applicable checks + -- is given by the caller. - else - Def_Id := Defining_Identifier (Type_Decl); + elsif Nkind (Insert_Node) in N_Declaration then + Def_Id := Defining_Identifier (Insert_Node); if (Ekind (Def_Id) = E_Record_Type and then Depends_On_Discriminant (R)) @@ -17800,18 +17813,29 @@ package body Sem_Ch3 is and then Has_Discriminants (Def_Id)) then Append_Range_Checks - (R_Checks, Check_List, Def_Id, Sloc (Type_Decl), R); + (R_Checks, + Check_List, Def_Id, Sloc (Insert_Node), R); else Insert_Range_Checks - (R_Checks, Type_Decl, Def_Id, Sloc (Type_Decl), R); + (R_Checks, + Insert_Node, Def_Id, Sloc (Insert_Node), R); end if; + + -- Insertion before a statement. Range appears in the + -- context of a quantified expression. Insertion will + -- take place when expression is expanded. + + else + null; end if; end if; end if; end if; + -- Case of other than an explicit N_Range node + elsif Expander_Active then Get_Index_Bounds (R, Lo, Hi); Force_Evaluation (Lo); Index: sem_ch5.adb =================================================================== --- sem_ch5.adb (revision 165944) +++ sem_ch5.adb (working copy) @@ -1538,8 +1538,11 @@ package body Sem_Ch5 is Object_Definition => New_Occurrence_Of (Typ, Loc), Expression => Relocate_Node (Original_Bound)); - Insert_Before (Parent (N), Decl); - Analyze (Decl); + -- Insert declaration at proper place. If loop comes from an + -- enclosing quantified expression, the insertion point is + -- arbitrarily far up in the tree. + + Insert_Action (Parent (N), Decl); Rewrite (Original_Bound, New_Occurrence_Of (Id, Loc)); return Expression (Decl); end if; Index: sem_res.adb =================================================================== --- sem_res.adb (revision 165950) +++ sem_res.adb (working copy) @@ -7809,9 +7809,13 @@ package body Sem_Res is procedure Resolve_Quantified_Expression (N : Node_Id; Typ : Entity_Id) is begin -- The loop structure is already resolved during its analysis, only the - -- resolution of the condition needs to be done. + -- resolution of the condition needs to be done. Expansion is disabled + -- so that checks and other generated code are inserted in the tree + -- after expression has been rewritten as a loop. + Expander_Mode_Save_And_Set (False); Resolve (Condition (N), Typ); + Expander_Mode_Restore; end Resolve_Quantified_Expression; -------------------