From patchwork Thu Feb 6 10:04:54 2014 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 317406 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]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 225322C0096 for ; Thu, 6 Feb 2014 21:05:11 +1100 (EST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=vwtioPjbsjb1Xo/lwdk6yhTh4XvNzd5RewOZfLLF10SSzc6boJ 3I4MAG3Jie2WkEerQejlQoVll7IQ6xcBIlI7vAelZ54GUuAP9elnWW+Bside/iMA 6QzA3wt8t6D/PF/wzrEFXNY0REsdb4rlT8GAqFSXn2gpKSClkSknabBHM= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=UvfAjw2JSzhoFixRBn7+iYNkfWk=; b=y6lqGMxRZkntvs5PUvTG NQSBL1+V+vnrAxI7btRTFMwuNfM0QrJSQ7JUBG9dKtu378IdZZmUYWhjDVP4by4X EPHmEiGu52igNNZ1m3TSRyJ7GcR7/EPn59IM1EXMmS5SsuIfYdeK0gnaSvbhpO5w yh/vG30Bc80u6WzZwr8qMyY= Received: (qmail 3702 invoked by alias); 6 Feb 2014 10:04:58 -0000 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 Received: (qmail 3625 invoked by uid 89); 6 Feb 2014 10:04:57 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham version=3.3.2 X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with (AES256-SHA encrypted) ESMTPS; Thu, 06 Feb 2014 10:04:56 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 39E49116690; Thu, 6 Feb 2014 05:04:54 -0500 (EST) 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 UNwqOOf8RQTE; Thu, 6 Feb 2014 05:04:54 -0500 (EST) Received: from kwai.gnat.com (unknown [IPv6:2620:20:4000:0:a6ba:dbff:fe26:1f63]) by rock.gnat.com (Postfix) with ESMTP id 29DF611668F; Thu, 6 Feb 2014 05:04:54 -0500 (EST) Received: by kwai.gnat.com (Postfix, from userid 4192) id 29B669198B; Thu, 6 Feb 2014 05:04:54 -0500 (EST) Date: Thu, 6 Feb 2014 05:04:54 -0500 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Order of evaluation between precondition and 'Old Message-ID: <20140206100454.GA1231@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.21 (2010-09-15) This patch modifies the expansion of attribute 'Old to insert the generated temporary that captures the value of the prefix before routine _Postconditions. As a result, the precondition of a subprogram will be evaluated first, before any postcondition-related code is executed. ------------ -- Source -- ------------ -- evaluation_order.adb procedure Evaluation_Order is subtype Idx is Integer range 1 .. 10; type Arr is array (Integer range <>) of Integer; procedure Swap (A : in out Arr; X, Y : Idx) with Pre => X in A'Range and Y in A'Range, Post => A(X) = A(Y)'Old and A(Y) = A(X)'Old; procedure Swap (A : in out Arr; X, Y : Idx) is begin null; end Swap; A : Arr (1 .. 2) := (1 => 1, others => 0); begin Swap (A, 1, 3); end Evaluation_Order; ---------------------------- -- Compilation and output -- ---------------------------- $ gnatmake -q -gnata evaluation_order.adb $ ./evaluation_order raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from evaluation_order.adb:6 Tested on x86_64-pc-linux-gnu, committed on trunk 2014-02-06 Hristian Kirtchev * exp_attr.adb (Expand_N_Attribute_Reference): Alphabetize variables. Rename variabme Tnn to Temp. Do not create a temporary if assertions are disabled. Find enclosing routine _Postconditions and insert the temporary that captures the value of the prefix before the routine. * exp_ch6.adb (Build_Postconditions_Procedure): Insert the generated _Postconditions routine before the first source declaration of the related subprogram. (Insert_After_Last_Declaration): Removed. (Insert_Before_First_Source_Declaration): New routine. Index: exp_attr.adb =================================================================== --- exp_attr.adb (revision 207533) +++ exp_attr.adb (working copy) @@ -3806,9 +3806,9 @@ --------- when Attribute_Old => Old : declare - Tnn : constant Entity_Id := Make_Temporary (Loc, 'T', Pref); + Asn_Stm : Node_Id; Subp : Node_Id; - Asn_Stm : Node_Id; + Temp : Entity_Id; begin -- If assertions are disabled, no need to create the declaration @@ -3818,42 +3818,47 @@ return; end if; - -- Find the nearest subprogram body, ignoring _Preconditions + Temp := Make_Temporary (Loc, 'T', Pref); + -- Climb the parent chain looking for subprogram _Postconditions + Subp := N; - loop + while Present (Subp) loop + exit when Nkind (Subp) = N_Subprogram_Body + and then Chars (Defining_Entity (Subp)) = Name_uPostconditions; + Subp := Parent (Subp); - exit when Nkind (Subp) = N_Subprogram_Body - and then Chars (Defining_Entity (Subp)) /= Name_uPostconditions; end loop; - -- Insert the initialized object declaration at the start of the - -- subprogram's declarations. + -- 'Old can only appear in a postcondition, the generated body of + -- _Postconditions must be in the tree. + pragma Assert (Present (Subp)); + + -- Generate: + -- Temp : constant := ; + Asn_Stm := Make_Object_Declaration (Loc, - Defining_Identifier => Tnn, + Defining_Identifier => Temp, Constant_Present => True, Object_Definition => New_Occurrence_Of (Etype (N), Loc), Expression => Pref); - -- Push the subprogram's scope, so that the object will be analyzed - -- in that context (rather than the context of the Precondition - -- subprogram) and will have its Scope set properly. + -- Push the scope of the related subprogram where _Postcondition + -- resides as this ensures that the object will be analyzed in the + -- proper context. - if Present (Corresponding_Spec (Subp)) then - Push_Scope (Corresponding_Spec (Subp)); - else - Push_Scope (Defining_Entity (Subp)); - end if; + Push_Scope (Scope (Defining_Entity (Subp))); - if Is_Empty_List (Declarations (Subp)) then - Set_Declarations (Subp, New_List (Asn_Stm)); - Analyze (Asn_Stm); - else - Insert_Action (First (Declarations (Subp)), Asn_Stm); - end if; + -- The object declaration is inserted before the body of subprogram + -- _Postconditions. This ensures that any precondition-like actions + -- are still executed before any parameter values are captured and + -- the multiple 'Old occurrences appear in order of declaration. + Insert_Before_And_Analyze (Subp, Asn_Stm); + Pop_Scope; + -- Ensure that the prefix of attribute 'Old is valid. The check must -- be inserted after the expansion of the attribute has taken place -- to reflect the new placement of the prefix. @@ -3862,9 +3867,7 @@ Ensure_Valid (Pref); end if; - Pop_Scope; - - Rewrite (N, New_Occurrence_Of (Tnn, Loc)); + Rewrite (N, New_Occurrence_Of (Temp, Loc)); end Old; ---------------------- Index: exp_ch6.adb =================================================================== --- exp_ch6.adb (revision 207536) +++ exp_ch6.adb (working copy) @@ -8911,27 +8911,47 @@ Stmts : List_Id; Result : Entity_Id) is - procedure Insert_After_Last_Declaration (Stmt : Node_Id); - -- Insert node Stmt after the last declaration of the subprogram body + procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id); + -- Insert node Stmt before the first source declaration of the + -- related subprogram's body. If no such declaration exists, Stmt + -- becomes the last declaration. - ----------------------------------- - -- Insert_After_Last_Declaration -- - ----------------------------------- + -------------------------------------------- + -- Insert_Before_First_Source_Declaration -- + -------------------------------------------- - procedure Insert_After_Last_Declaration (Stmt : Node_Id) is - Decls : List_Id := Declarations (N); + procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is + Decls : constant List_Id := Declarations (N); + Decl : Node_Id; begin + -- Inspect the declarations of the related subprogram body looking + -- for the first source declaration. + + if Present (Decls) then + Decl := First (Decls); + while Present (Decl) loop + if Comes_From_Source (Decl) then + Insert_Before (Decl, Stmt); + return; + end if; + + Next (Decl); + end loop; + + -- If we get there, then the subprogram body lacks any source + -- declarations. The body of _Postconditions now acts as the + -- last declaration. + + Append (Stmt, Decls); + -- Ensure that the body has a declaration list - if No (Decls) then - Decls := New_List; - Set_Declarations (N, Decls); + else + Set_Declarations (N, New_List (Stmt)); end if; + end Insert_Before_First_Source_Declaration; - Append_To (Decls, Stmt); - end Insert_After_Last_Declaration; - -- Local variables Loc : constant Source_Ptr := Sloc (N); @@ -8965,9 +8985,9 @@ New_Reference_To (Etype (Result), Loc))); end if; - -- Insert _Postconditions after the last declaration of the body. - -- This ensures that the body will not cause any premature freezing - -- as it may mention types: + -- Insert _Postconditions before the first source declaration of the + -- body. This ensures that the body will not cause any premature + -- freezing as it may mention types: -- procedure Proc (Obj : Array_Typ) is -- procedure _postconditions is @@ -8983,7 +9003,7 @@ -- order reference. The body of _Postconditions must be placed after -- the declaration of Temp to preserve correct visibility. - Insert_After_Last_Declaration ( + Insert_Before_First_Source_Declaration ( Make_Subprogram_Body (Loc, Specification => Make_Procedure_Specification (Loc,