From patchwork Mon Oct 14 13:23:58 2013 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 283220 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 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (Client did not present a certificate) by ozlabs.org (Postfix) with ESMTPS id AADA02C00B6 for ; Tue, 15 Oct 2013 00:24:09 +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=atDg+PtmH+ZjxASvYg32cRmBT6XAA/X74Om+z0R9fjmouO9IXE nOXr+MV6rPxPnjacJvUmwZI2SGEWL+Jd7cgPjz6TZCTCLX0pV52GqvZqxHpXfQx8 wAToQg1Gg/FO58kFkOgdRcuLXV8xjcOq0dfGWhA+SnjUwzOFGDtWE3SlE= 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=MeCOu6ZPO7bk1jlf54GnxlBVkBM=; b=LM2GiMIjb6jB9RrRfmJ3 Zl2dy7LYAXXPjvUaVggltQNa5B4Pfyoq/vVjvD6S8zviNFrcYIXyftWCYADTKavE YUVgxt73YKfoA3ooQ8aPXOm+rJFRtRN4eLW2d40WJTlsP+I50kP0nekFJGlir5H8 u64N3F7RWwwic6MUWO5NVK0= Received: (qmail 26524 invoked by alias); 14 Oct 2013 13:24:03 -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 26512 invoked by uid 89); 14 Oct 2013 13:24:02 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No 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; Mon, 14 Oct 2013 13:24:01 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 424F811648D; Mon, 14 Oct 2013 09:24:21 -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 f+wz51V0q0Hd; Mon, 14 Oct 2013 09:24:21 -0400 (EDT) Received: from kwai.gnat.com (unknown [IPv6:2620:20:4000:0:a6ba:dbff:fe26:1f63]) by rock.gnat.com (Postfix) with ESMTP id 2FD8511645A; Mon, 14 Oct 2013 09:24:21 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id C40B23FB31; Mon, 14 Oct 2013 09:23:58 -0400 (EDT) Date: Mon, 14 Oct 2013 09:23:58 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] State refinement constituent uninstall Message-ID: <20131014132358.GA9939@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) This patch hides the refinement constituents of all abstract states with visible refinement at the end of the package body declarations. Tested on x86_64-pc-linux-gnu, committed on trunk 2013-10-14 Hristian Kirtchev * einfo.adb: Flag 263 is now known as Has_Visible_Refinement. (Has_Non_Null_Refinement): New routine. (Has_Null_Refinement): The routine is now synthesized. (Has_Visible_Refinement): New routine. (Set_Has_Visible_Refinement): New routine. (Write_Entity_Flags): Remove the output for Has_Null_Refinement. Add output for Has_Visible_Refinement. * einfo.ads: Update the occurrences of Has_Non_Null_Refinement, Has_Null_Refinement and Has_Visible_Refinement in entities. (Has_Non_Null_Refinement): New synthesized attribute. (Has_Null_Refinement): This attribute is now synthesized. (Has_Visible_Refinement): New routine with corresponding pragma Inline. (Set_Has_Visible_Refinement): New routine with corresponding pragma Inline. * sem_ch3.adb (Analyze_Declarations): Add new local variable In_Package_Body. Remove state refinements from visibility at the end of the package body declarations. (Remove_Visible_Refinements): New routine. * sem_prag.adb (Analyze_Constituent): Collect a null constituent and mark the state as having visible refinement. (Analyze_Global_Item): Use attribute Has_Visible_Refinement to detect a state with visible refinement. (Analyze_Input_Output): Use attribute Has_Visible_Refinement to detect a state with visible refinement. (Check_Dependency_Clause): Use attribute Has_Non_Null_Refinement rather than checking the contents of list Refinement_Constituents. (Check_In_Out_States): Use attribute Has_Non_Null_Refinement rather than checking the contents of list Refinement_Constituents. (Check_Input_States): Use attribute Has_Non_Null_Refinement rather than checking the contents of list Refinement_Constituents. (Check_Matching_Constituent): Mark a state as having visible refinement. (Check_Output_States): Use attribute Has_Non_Null_Refinement rather than checking the contents of list Refinement_Constituents. (Check_Refined_Global_Item): Use attribute Has_Visible_Refinement to detect a state with visible refinement. (Is_Matching_Input): Use attribute Has_Non_Null_Refinement rather than checking the contents of list Refinement_Constituents. * sem_util.adb (Is_Refined_State): Use attribute Has_Visible_Refinement to detect a state with visible refinement. Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 203531) +++ sem_ch3.adb (working copy) @@ -2067,6 +2067,11 @@ -- (They have the sloc of the label as found in the source, and that -- is ahead of the current declarative part). + procedure Remove_Visible_Refinements (Spec_Id : Entity_Id); + -- Spec_Id is the entity of a package that may define abstract states. + -- If the states have visible refinement, remove the visibility of each + -- constituent at the end of the package body declarations. + ----------------- -- Adjust_Decl -- ----------------- @@ -2080,6 +2085,24 @@ end loop; end Adjust_Decl; + -------------------------------- + -- Remove_Visible_Refinements -- + -------------------------------- + + procedure Remove_Visible_Refinements (Spec_Id : Entity_Id) is + State_Elmt : Elmt_Id; + + begin + if Present (Abstract_States (Spec_Id)) then + State_Elmt := First_Elmt (Abstract_States (Spec_Id)); + while Present (State_Elmt) loop + Set_Has_Visible_Refinement (Node (State_Elmt), False); + + Next_Elmt (State_Elmt); + end loop; + end if; + end Remove_Visible_Refinements; + -- Local variables Body_Id : Entity_Id; @@ -2089,6 +2112,9 @@ Prag : Node_Id; Spec_Id : Entity_Id; + In_Package_Body : Boolean := False; + -- Flag set when the current declaration list belongs to a package body + -- Start of processing for Analyze_Declarations begin @@ -2220,6 +2246,8 @@ -- Refined_Global because the last two may mention constituents. elsif Nkind (Context) = N_Package_Body then + In_Package_Body := True; + Body_Id := Defining_Entity (Context); Spec_Id := Corresponding_Spec (Context); Prag := Get_Pragma (Body_Id, Pragma_Refined_State); @@ -2256,6 +2284,14 @@ Next (Decl); end loop; + + -- State refinements are visible upto the end the of the package body + -- declarations. Hide the refinements from visibility to restore the + -- original state conditions. + + if In_Package_Body then + Remove_Visible_Refinements (Spec_Id); + end if; end Analyze_Declarations; ----------------------------------- Index: einfo.adb =================================================================== --- einfo.adb (revision 203527) +++ einfo.adb (working copy) @@ -551,7 +551,7 @@ -- Has_Delayed_Rep_Aspects Flag261 -- May_Inherit_Delayed_Rep_Aspects Flag262 - -- Has_Null_Refinement Flag263 + -- Has_Visible_Refinement Flag263 -- (unused) Flag264 -- (unused) Flag265 @@ -1483,12 +1483,6 @@ return Flag75 (Implementation_Base_Type (Id)); end Has_Non_Standard_Rep; - function Has_Null_Refinement (Id : E) return B is - begin - pragma Assert (Ekind (Id) = E_Abstract_State); - return Flag263 (Id); - end Has_Null_Refinement; - function Has_Object_Size_Clause (Id : E) return B is begin pragma Assert (Is_Type (Id)); @@ -1716,6 +1710,12 @@ return Flag215 (Id); end Has_Up_Level_Access; + function Has_Visible_Refinement (Id : E) return B is + begin + pragma Assert (Ekind (Id) = E_Abstract_State); + return Flag263 (Id); + end Has_Visible_Refinement; + function Has_Volatile_Components (Id : E) return B is begin return Flag87 (Implementation_Base_Type (Id)); @@ -4110,12 +4110,6 @@ Set_Flag75 (Id, V); end Set_Has_Non_Standard_Rep; - procedure Set_Has_Null_Refinement (Id : E; V : B := True) is - begin - pragma Assert (Ekind (Id) = E_Abstract_State); - Set_Flag263 (Id, V); - end Set_Has_Null_Refinement; - procedure Set_Has_Object_Size_Clause (Id : E; V : B := True) is begin pragma Assert (Is_Type (Id)); @@ -4343,6 +4337,12 @@ Set_Flag72 (Id, V); end Set_Has_Unknown_Discriminants; + procedure Set_Has_Visible_Refinement (Id : E; V : B := True) is + begin + pragma Assert (Ekind (Id) = E_Abstract_State); + Set_Flag263 (Id, V); + end Set_Has_Visible_Refinement; + procedure Set_Has_Volatile_Components (Id : E; V : B := True) is begin pragma Assert (not Is_Type (Id) or else Is_Base_Type (Id)); @@ -6472,6 +6472,29 @@ end Has_Interrupt_Handler; ----------------------------- + -- Has_Non_Null_Refinement -- + ----------------------------- + + function Has_Non_Null_Refinement (Id : E) return B is + begin + -- "Refinement" is a concept applicable only to abstract states + + pragma Assert (Ekind (Id) = E_Abstract_State); + + if Has_Visible_Refinement (Id) then + pragma Assert (Present (Refinement_Constituents (Id))); + + -- For a refinement to be non-null, the first constituent must be + -- anything other than null. + + return + Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) /= N_Null; + end if; + + return False; + end Has_Non_Null_Refinement; + + ----------------------------- -- Has_Null_Abstract_State -- ----------------------------- @@ -6484,6 +6507,29 @@ and then Is_Null_State (Node (First_Elmt (Abstract_States (Id)))); end Has_Null_Abstract_State; + ------------------------- + -- Has_Null_Refinement -- + ------------------------- + + function Has_Null_Refinement (Id : E) return B is + begin + -- "Refinement" is a concept applicable only to abstract states + + pragma Assert (Ekind (Id) = E_Abstract_State); + + if Has_Visible_Refinement (Id) then + pragma Assert (Present (Refinement_Constituents (Id))); + + -- For a refinement to be null, the state's sole constituent must be + -- a null. + + return + Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) = N_Null; + end if; + + return False; + end Has_Null_Refinement; + -------------------- -- Has_Unmodified -- -------------------- @@ -7969,7 +8015,6 @@ W ("Has_Missing_Return", Flag142 (Id)); W ("Has_Nested_Block_With_Handler", Flag101 (Id)); W ("Has_Non_Standard_Rep", Flag75 (Id)); - W ("Has_Null_Refinement", Flag263 (Id)); W ("Has_Object_Size_Clause", Flag172 (Id)); W ("Has_Per_Object_Constraint", Flag154 (Id)); W ("Has_Postconditions", Flag240 (Id)); @@ -8011,6 +8056,7 @@ W ("Has_Unchecked_Union", Flag123 (Id)); W ("Has_Unknown_Discriminants", Flag72 (Id)); W ("Has_Up_Level_Access", Flag215 (Id)); + W ("Has_Visible_Refinement", Flag263 (Id)); W ("Has_Volatile_Components", Flag87 (Id)); W ("Has_Xref_Entry", Flag182 (Id)); W ("In_Package_Body", Flag48 (Id)); Index: einfo.ads =================================================================== --- einfo.ads (revision 203527) +++ einfo.ads (working copy) @@ -1636,6 +1636,10 @@ -- optimizations to ensure that they are consistent with exceptions. -- See documentation in Gigi for further details. +-- Has_Non_Null_Refinement (synth) +-- Defined in E_Abstract_State entities. True if the state has at least +-- one variable or state constituent in aspect/pragma Refined_State. + -- Has_Non_Standard_Rep (Flag75) [implementation base type only] -- Defined in all type entities. Set when some representation clause -- or pragma causes the representation of the item to be significantly @@ -1650,8 +1654,8 @@ -- Defined in package entities. True if the package is subject to a null -- Abstract_State aspect/pragma. --- Has_Null_Refinement (Flag263) --- Defined in E_Abstract_State entities. Set if the state has a null +-- Has_Null_Refinement (synth) +-- Defined in E_Abstract_State entities. True if the state has a null -- refinement in aspect/pragma Refined_State. -- Has_Object_Size_Clause (Flag172) @@ -1913,6 +1917,11 @@ -- VM_Target /= No_VM, for efficiency, since only the .NET back-end -- makes use of it to generate proper code for up-level references. +-- Has_Visible_Refinement (Flag263) +-- Defined in E_Abstract_State entities. Set when a state has at least +-- one refinement constituent and analysis is in the region between +-- pragma Refined_State and the end of the package body declarations. + -- Has_Volatile_Components (Flag87) [implementation base type only] -- Defined in all types and objects. Set only for an array type or array -- object if a valid pragma Volatile_Components or a valid pragma @@ -5108,7 +5117,9 @@ -- E_Abstract_State -- Refinement_Constituents (Elist8) -- Refined_State (Node10) - -- Has_Null_Refinement (Flag263) + -- Has_Visible_Refinement (Flag263) + -- Has_Non_Null_Refinement (synth) + -- Has_Null_Refinement (synth) -- Is_External_State (synth) -- Is_Input_Only_State (synth) -- Is_Null_State (synth) @@ -6349,7 +6360,6 @@ function Has_Missing_Return (Id : E) return B; function Has_Nested_Block_With_Handler (Id : E) return B; function Has_Non_Standard_Rep (Id : E) return B; - function Has_Null_Refinement (Id : E) return B; function Has_Object_Size_Clause (Id : E) return B; function Has_Per_Object_Constraint (Id : E) return B; function Has_Postconditions (Id : E) return B; @@ -6391,6 +6401,7 @@ function Has_Unchecked_Union (Id : E) return B; function Has_Unknown_Discriminants (Id : E) return B; function Has_Up_Level_Access (Id : E) return B; + function Has_Visible_Refinement (Id : E) return B; function Has_Volatile_Components (Id : E) return B; function Has_Xref_Entry (Id : E) return B; function Hiding_Loop_Variable (Id : E) return E; @@ -6696,7 +6707,9 @@ function Has_Attach_Handler (Id : E) return B; function Has_Entries (Id : E) return B; function Has_Foreign_Convention (Id : E) return B; + function Has_Non_Null_Refinement (Id : E) return B; function Has_Null_Abstract_State (Id : E) return B; + function Has_Null_Refinement (Id : E) return B; function Implementation_Base_Type (Id : E) return E; function Is_Base_Type (Id : E) return B; function Is_Boolean_Type (Id : E) return B; @@ -6963,7 +6976,6 @@ procedure Set_Has_Missing_Return (Id : E; V : B := True); procedure Set_Has_Nested_Block_With_Handler (Id : E; V : B := True); procedure Set_Has_Non_Standard_Rep (Id : E; V : B := True); - procedure Set_Has_Null_Refinement (Id : E; V : B := True); procedure Set_Has_Object_Size_Clause (Id : E; V : B := True); procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True); procedure Set_Has_Postconditions (Id : E; V : B := True); @@ -7005,6 +7017,7 @@ procedure Set_Has_Unchecked_Union (Id : E; V : B := True); procedure Set_Has_Unknown_Discriminants (Id : E; V : B := True); procedure Set_Has_Up_Level_Access (Id : E; V : B := True); + procedure Set_Has_Visible_Refinement (Id : E; V : B := True); procedure Set_Has_Volatile_Components (Id : E; V : B := True); procedure Set_Has_Xref_Entry (Id : E; V : B := True); procedure Set_Hiding_Loop_Variable (Id : E; V : E); @@ -7679,7 +7692,6 @@ pragma Inline (Has_Missing_Return); pragma Inline (Has_Nested_Block_With_Handler); pragma Inline (Has_Non_Standard_Rep); - pragma Inline (Has_Null_Refinement); pragma Inline (Has_Object_Size_Clause); pragma Inline (Has_Per_Object_Constraint); pragma Inline (Has_Postconditions); @@ -7721,6 +7733,7 @@ pragma Inline (Has_Unchecked_Union); pragma Inline (Has_Unknown_Discriminants); pragma Inline (Has_Up_Level_Access); + pragma Inline (Has_Visible_Refinement); pragma Inline (Has_Volatile_Components); pragma Inline (Has_Xref_Entry); pragma Inline (Hiding_Loop_Variable); @@ -8140,7 +8153,6 @@ pragma Inline (Set_Has_Missing_Return); pragma Inline (Set_Has_Nested_Block_With_Handler); pragma Inline (Set_Has_Non_Standard_Rep); - pragma Inline (Set_Has_Null_Refinement); pragma Inline (Set_Has_Object_Size_Clause); pragma Inline (Set_Has_Per_Object_Constraint); pragma Inline (Set_Has_Postconditions); @@ -8182,6 +8194,7 @@ pragma Inline (Set_Has_Unchecked_Union); pragma Inline (Set_Has_Unknown_Discriminants); pragma Inline (Set_Has_Up_Level_Access); + pragma Inline (Set_Has_Visible_Refinement); pragma Inline (Set_Has_Volatile_Components); pragma Inline (Set_Has_Xref_Entry); pragma Inline (Set_Hiding_Loop_Variable); Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 203545) +++ sem_prag.adb (working copy) @@ -798,9 +798,7 @@ -- appear in pragma [Refined_]Global as its place must -- be taken by some of its constituents. - elsif not Is_Empty_Elmt_List - (Refinement_Constituents (Item_Id)) - then + elsif Has_Visible_Refinement (Item_Id) then Error_Msg_NE ("cannot mention state & in global refinement, " & "use its constituents instead", Item, Item_Id); @@ -1625,9 +1623,7 @@ -- in pragma [Refined_]Global as its place must be taken by -- some of its constituents. - elsif not Is_Empty_Elmt_List - (Refinement_Constituents (Item_Id)) - then + elsif Has_Visible_Refinement (Item_Id) then Error_Msg_NE ("cannot mention state & in global refinement, use its " & "constituents instead", Item, Item_Id); @@ -19677,9 +19673,7 @@ -- Depends => ( => State) -- Refined_Depends => ( => (C1, C2)) - elsif not Is_Empty_Elmt_List - (Refinement_Constituents (Dep_Id)) - then + elsif Has_Non_Null_Refinement (Dep_Id) then Has_Refined_State := True; if Is_Entity_Name (Ref_Input) then @@ -20033,9 +20027,7 @@ -- Refined_Depends => (C1 => , -- C2 => ) - elsif not Is_Empty_Elmt_List - (Refinement_Constituents (Dep_Id)) - then + elsif Has_Non_Null_Refinement (Dep_Id) then Has_Refined_State := True; -- Store the entities of all output constituents of an @@ -20452,8 +20444,7 @@ -- Ensure that one of the three coverage variants is satisfied if Ekind (Item_Id) = E_Abstract_State - and then not Is_Empty_Elmt_List - (Refinement_Constituents (Item_Id)) + and then Has_Non_Null_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; @@ -20536,8 +20527,7 @@ -- is of mode Input. if Ekind (Item_Id) = E_Abstract_State - and then not Is_Empty_Elmt_List - (Refinement_Constituents (Item_Id)) + and then Has_Non_Null_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; @@ -20607,8 +20597,7 @@ -- have mode Output. if Ekind (Item_Id) = E_Abstract_State - and then not Is_Empty_Elmt_List - (Refinement_Constituents (Item_Id)) + and then Has_Non_Null_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; @@ -20730,8 +20719,7 @@ -- occurrences in Global and Refined_Global match. if No (Refined_State (Item_Id)) - and then Is_Empty_Elmt_List - (Refinement_Constituents (Item_Id)) + and then not Has_Visible_Refinement (Item_Id) then Check_Matching_Modes (Item_Id); end if; @@ -21088,13 +21076,20 @@ Add_Item (Constit_Id, Constituents_Seen); Remove_Elmt (Hidden_States, State_Elmt); - -- Establish a relation between the refined state and its - -- constituent. + -- Collect the constituent in the list of refinement + -- items. Establish a relation between the refined state + -- and its constituent. Append_Elmt (Constit_Id, Refinement_Constituents (State_Id)); Set_Refined_State (Constit_Id, State_Id); + -- The state has at least one legal constituent, mark the + -- start of the refinement region. The region ends when + -- the body declarations end (see Analyze_Declarations). + + Set_Has_Visible_Refinement (State_Id); + return; end if; @@ -21129,11 +21124,18 @@ Error_Msg_N ("cannot mix null and non-null constituents", Constit); - -- Mark the related state as having a null refinement - else Null_Seen := True; - Set_Has_Null_Refinement (State_Id); + + -- Collect the constituent in the list of refinement items + + Append_Elmt (Constit, Refinement_Constituents (State_Id)); + + -- The state has at least one legal constituent, mark the + -- start of the refinement region. The region ends when the + -- body declarations end (see Analyze_Declarations). + + Set_Has_Visible_Refinement (State_Id); end if; -- Non-null constituents @@ -21717,12 +21719,15 @@ if Ekind (Item_Id) = E_Abstract_State then if Has_Null_Refinement (Item_Id) then Has_Null_State := True; - elsif Mode = Name_Input then - Has_In_State := True; - elsif Mode = Name_In_Out then - Has_In_Out_State := True; - elsif Mode = Name_Output then - Has_Out_State := True; + + elsif Has_Non_Null_Refinement (Item_Id) then + if Mode = Name_Input then + Has_In_State := True; + elsif Mode = Name_In_Out then + Has_In_Out_State := True; + elsif Mode = Name_Output then + Has_Out_State := True; + end if; end if; end if; Index: sem_util.adb =================================================================== --- sem_util.adb (revision 203532) +++ sem_util.adb (working copy) @@ -3418,8 +3418,7 @@ return Ekind (Item_Id) = E_Abstract_State - and then not Is_Empty_Elmt_List - (Refinement_Constituents (Item_Id)); + and then Has_Visible_Refinement (Item_Id); end if; end Is_Refined_State;