From 05f1a54316f9516defe5ab54e0be66b1821596a1 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Wed, 12 Oct 2016 16:37:35 +0200 Subject: [PATCH] [multiple changes] 2016-10-12 Yannick Moy * einfo.adb, einfo.ads (Partial_Refinement_Constituents): Take into account constituents that are themselves abstract states with full or partial refinement visible. * sem_prag.adb (Find_Encapsulating_State): Move function to library-level, to share between subprograms. (Analyze_Refined_Global_In_Decl_Part): Use Find_Encapsulating_State to get relevant encapsulating state. 2016-10-12 Arnaud Charlet * gnat1drv.adb: Fix minor typo. From-SVN: r241052 --- gcc/ada/ChangeLog | 14 +++++ gcc/ada/einfo.adb | 68 +++++++++++++++++++-- gcc/ada/einfo.ads | 8 ++- gcc/ada/gnat1drv.adb | 2 +- gcc/ada/sem_prag.adb | 169 ++++++++++++++++++++++++++------------------------- 5 files changed, 169 insertions(+), 92 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index efbe1d2..8809033 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,19 @@ 2016-10-12 Yannick Moy + * einfo.adb, einfo.ads (Partial_Refinement_Constituents): Take + into account constituents that are themselves abstract states + with full or partial refinement visible. + * sem_prag.adb (Find_Encapsulating_State): Move function + to library-level, to share between subprograms. + (Analyze_Refined_Global_In_Decl_Part): Use + Find_Encapsulating_State to get relevant encapsulating state. + +2016-10-12 Arnaud Charlet + + * gnat1drv.adb: Fix minor typo. + +2016-10-12 Yannick Moy + * sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Adapt checking for optional refinement of abstract state with partial visible refinement. diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 83eddf3..2cfb332 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -8407,19 +8407,79 @@ package body Einfo is ------------------------------------- function Partial_Refinement_Constituents (Id : E) return L is - Constits : Elist_Id; + Constits : Elist_Id := No_Elist; + + procedure Add_Usable_Constituents (Item : E); + -- Add global item Item and/or its constituents to list Constits when + -- they can be used in a global refinement within the current scope. The + -- criteria are: + -- 1) If Item is an abstract state with full refinement visible, add + -- its constituents. + -- 2) If Item is an abstract state with only partial refinement + -- visible, add both Item and its constituents. + -- 3) If Item is an abstract state without a visible refinement, add + -- it. + -- 4) If Id is not an abstract state, add it. + + procedure Add_Usable_Constituents (List : Elist_Id); + -- Apply Add_Usable_Constituents to every constituent in List + + ----------------------------- + -- Add_Usable_Constituents -- + ----------------------------- + + procedure Add_Usable_Constituents (Item : E) is + begin + if Ekind (Item) = E_Abstract_State then + if Has_Visible_Refinement (Item) then + Add_Usable_Constituents (Refinement_Constituents (Item)); + + elsif Has_Partial_Visible_Refinement (Item) then + Append_New_Elmt (Item, Constits); + Add_Usable_Constituents (Part_Of_Constituents (Item)); + + else + Append_New_Elmt (Item, Constits); + end if; + + else + Append_New_Elmt (Item, Constits); + end if; + end Add_Usable_Constituents; + + procedure Add_Usable_Constituents (List : Elist_Id) is + Constit_Elmt : Elmt_Id; + begin + if Present (List) then + Constit_Elmt := First_Elmt (List); + while Present (Constit_Elmt) loop + Add_Usable_Constituents (Node (Constit_Elmt)); + Next_Elmt (Constit_Elmt); + end loop; + end if; + end Add_Usable_Constituents; + + -- Start of processing for Partial_Refinement_Constituents begin -- "Refinement" is a concept applicable only to abstract states pragma Assert (Ekind (Id) = E_Abstract_State); - Constits := Refinement_Constituents (Id); + + if Has_Visible_Refinement (Id) then + Constits := Refinement_Constituents (Id); -- A refinement may be partially visible when objects declared in the -- private part of a package are subject to a Part_Of indicator. - if No (Constits) then - Constits := Part_Of_Constituents (Id); + elsif Has_Partial_Visible_Refinement (Id) then + Add_Usable_Constituents (Part_Of_Constituents (Id)); + + -- Function should only be called when full or partial refinement is + -- visible. + + else + raise Program_Error; end if; return Constits; diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 9ffc2a8..f62942c 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -3793,9 +3793,11 @@ package Einfo is -- way this is stored is as an element of the Subprograms_For_Type field. -- Partial_Refinement_Constituents (synthesized) --- Present in abstract state entities. Contains the constituents that --- refine the state in its private part, in other words, all the hidden --- states that indicate this abstract state in a Part_Of aspect/pragma. +-- Defined in abstract state entities. Returns the constituents that +-- refine the state in the current scope, which are allowed in a global +-- refinement in this scope. These consist in those constituents that are +-- abstract states with no or only partial refinement visible, and those +-- that are not themselves abstract states. -- Partial_View_Has_Unknown_Discr (Flag280) -- Present in all types. Set to Indicate that the partial view of a type diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index acb79a5..fa08414 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -343,7 +343,7 @@ procedure Gnat1drv is -- of compiler warnings, but these are being turned off by default, -- and CodePeer generates better messages (referencing original -- variables) this way. - -- Do this only is -gnatws is set (the default with -gnatcC), so that + -- Do this only if -gnatws is set (the default with -gnatcC), so that -- if warnings are enabled, we'll get better messages from GNAT. if Warning_Mode = Suppress then diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 3b0c6c6..649eb62 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -258,6 +258,13 @@ package body Sem_Prag is -- Subsidiary to all Find_Related_xxx routines. Emit an error on pragma -- Prag that duplicates previous pragma Prev. + function Find_Encapsulating_State + (States : Elist_Id; + Constit_Id : Entity_Id) return Entity_Id; + -- Given the entity of a constituent Constit_Id, find the corresponding + -- encapsulating state which appears in States. The routine returns Empty + -- is no such state is found. + function Find_Related_Context (Prag : Node_Id; Do_Checks : Boolean := False) return Node_Id; @@ -24545,6 +24552,12 @@ package body Sem_Prag is -- These list contain the entities of all Input, In_Out, Output and -- Proof_In items defined in the corresponding Global pragma. + Repeat_Items : Elist_Id := No_Elist; + -- A list of all global items without full visible refinement found + -- in pragma Global. These states should be repeated in the global + -- refinement (SPARK RM 7.2.4(3c)) unless they have a partial visible + -- refinement, in which case they may be repeated (SPARK RM 7.2.4(3d)). + Spec_Id : Entity_Id; -- The entity of the subprogram subject to pragma Refined_Global @@ -24552,12 +24565,6 @@ package body Sem_Prag is -- A list of all states with full or partial visible refinement found in -- pragma Global. - Repeat_Items : Elist_Id := No_Elist; - -- A list of all global items without full visible refinement found - -- in pragma Global. These states should be repeated in the global - -- refinement (SPARK RM 7.2.4(3c)) unless they have a partial visible - -- refinement, in which case they may be repeated (SPARK RM 7.2.4(3d)). - procedure Check_In_Out_States; -- Determine whether the corresponding Global pragma mentions In_Out -- states with visible refinement and if so, ensure that one of the @@ -24616,8 +24623,8 @@ package body Sem_Prag is -- In_Out_Constits and Out_Constits of valid constituents. procedure Present_Then_Remove (List : Elist_Id; Item : Entity_Id); - -- Same as function Present_Then_Remove, but do not report presence of - -- Item in List. + -- Same as function Present_Then_Remove, but do not report the presence + -- of Item in List. procedure Report_Extra_Constituents; -- Emit an error for each constituent found in lists In_Constits, @@ -24715,12 +24722,12 @@ package body Sem_Prag is N, State_Id); end if; - -- The state lacks a completion. When full refinement is - -- visible, always emit an error (SPARK RM 7.2.4(3a)). When only - -- partial refinement is visible, emit an error if the abstract - -- state itself is not utilized (SPARK RM 7.2.4(3d)). In the - -- case where both are utilized, an error will be issued in - -- Check_State_And_Constituent_Use. + -- The state lacks a completion. When full refinement is visible, + -- always emit an error (SPARK RM 7.2.4(3a)). When only partial + -- refinement is visible, emit an error if the abstract state + -- itself is not utilized (SPARK RM 7.2.4(3d)). In the case where + -- both are utilized, Check_State_And_Constituent_Use. will issue + -- the error. elsif not Input_Seen and then not In_Out_Seen @@ -24836,17 +24843,16 @@ package body Sem_Prag is end loop; end if; - -- Not one of the constituents appeared as Input. When full - -- refinement is visible, always emit an error (SPARK RM - -- 7.2.4(3a)). When only partial refinement is visible, emit an + -- Not one of the constituents appeared as Input. Always emit an + -- error when the full refinement is visible (SPARK RM 7.2.4(3a)). + -- When only partial refinement is visible, emit an -- error if the abstract state itself is not utilized (SPARK RM -- 7.2.4(3d)). In the case where both are utilized, an error will -- be issued in Check_State_And_Constituent_Use. if not In_Seen and then (Has_Visible_Refinement (State_Id) - or else - Contains (Repeat_Items, State_Id)) + or else Contains (Repeat_Items, State_Id)) then SPARK_Msg_NE ("global refinement of state & must include at least one " @@ -24910,10 +24916,10 @@ package body Sem_Prag is procedure Check_Constituent_Usage (State_Id : Entity_Id) is Constits : constant Elist_Id := Partial_Refinement_Constituents (State_Id); - Constit_Elmt : Elmt_Id; - Constit_Id : Entity_Id; Only_Partial : constant Boolean := not Has_Visible_Refinement (State_Id); + Constit_Elmt : Elmt_Id; + Constit_Id : Entity_Id; Posted : Boolean := False; begin @@ -24922,9 +24928,9 @@ package body Sem_Prag is while Present (Constit_Elmt) loop Constit_Id := Node (Constit_Elmt); - -- Issue an error when a constituent of State_Id is - -- utilized, and State_Id has only partial visible - -- refinement (SPARK RM 7.2.4(3d)). + -- Issue an error when a constituent of State_Id is utilized + -- and State_Id has only partial visible refinement + -- (SPARK RM 7.2.4(3d)). if Only_Partial then if Present_Then_Remove (Out_Constits, Constit_Id) @@ -24936,8 +24942,8 @@ package body Sem_Prag is then Error_Msg_Name_1 := Chars (State_Id); SPARK_Msg_NE - ("constituent & of state % cannot be used in " - & "global refinement", N, Constit_Id); + ("constituent & of state % cannot be used in global " + & "refinement", N, Constit_Id); Error_Msg_Name_1 := Chars (State_Id); SPARK_Msg_N ("\use state % instead", N); end if; @@ -25000,9 +25006,9 @@ package body Sem_Prag is Item_Id := Node (Item_Elmt); -- When full refinement is visible, ensure that all of the - -- constituents are utilized and they have mode Output. - -- When only partial refinement is visible, ensure that - -- no constituent is utilized. + -- constituents are utilized and they have mode Output. When + -- only partial refinement is visible, ensure that no + -- constituent is utilized. if Ekind (Item_Id) = E_Abstract_State and then Has_Non_Null_Visible_Refinement (Item_Id) @@ -25066,17 +25072,16 @@ package body Sem_Prag is end loop; end if; - -- Not one of the constituents appeared as Proof_In. When - -- full refinement is visible, always emit an error (SPARK RM - -- 7.2.4(3a)). When only partial refinement is visible, emit an - -- error if the abstract state itself is not utilized (SPARK RM - -- 7.2.4(3d)). In the case where both are utilized, an error will - -- be issued in Check_State_And_Constituent_Use. + -- Not one of the constituents appeared as Proof_In. Always emit + -- an error when full refinement is visible (SPARK RM 7.2.4(3a)). + -- When only partial refinement is visible, emit an error if the + -- abstract state itself is not utilized (SPARK RM 7.2.4(3d)). In + -- the case where both are utilized, an error will be issued by + -- Check_State_And_Constituent_Use. if not Proof_In_Seen and then (Has_Visible_Refinement (State_Id) - or else - Contains (Repeat_Items, State_Id)) + or else Contains (Repeat_Items, State_Id)) then SPARK_Msg_NE ("global refinement of state & must include at least one " @@ -25165,15 +25170,19 @@ package body Sem_Prag is SPARK_Msg_N ("\expected mode %, found mode %", Item); end Inconsistent_Mode_Error; + -- Local variables + Enc_State : Entity_Id := Empty; -- Encapsulating state for constituent, Empty otherwise -- Start of processing for Check_Refined_Global_Item begin - if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable) + if Ekind_In (Item_Id, E_Abstract_State, + E_Constant, + E_Variable) then - Enc_State := Encapsulating_State (Item_Id); + Enc_State := Find_Encapsulating_State (States, Item_Id); end if; -- When the state or object acts as a constituent of another @@ -25184,8 +25193,7 @@ package body Sem_Prag is if Present (Enc_State) and then (Has_Visible_Refinement (Enc_State) - or else - Has_Partial_Visible_Refinement (Enc_State)) + or else Has_Partial_Visible_Refinement (Enc_State)) and then Contains (States, Enc_State) then -- If the state has only partial visible refinement, remove it @@ -25360,8 +25368,8 @@ package body Sem_Prag is end if; -- Record global items without full visible refinement found in - -- pragma Global, which should (SPARK RM 7.2.4(3c)) or may (SPARK - -- RM 7.2.4(3d)) be repeated in the global refinement. + -- pragma Global which should be repeated in the global refinement + -- (SPARK RM 7.2.4(3c), SPARK RM 7.2.4(3d)). if Ekind (Item_Id) /= E_Abstract_State or else not Has_Visible_Refinement (Item_Id) @@ -25523,6 +25531,7 @@ package body Sem_Prag is procedure Report_Missing_Items is Item_Elmt : Elmt_Id; Item_Id : Entity_Id; + begin -- Do not perform this check in an instance because it was already -- performed successfully in the generic template. @@ -25650,10 +25659,11 @@ package body Sem_Prag is -- refinement, prior to calling checking procedures which remove items -- from the list of constituents. - No_Constit := No (In_Constits) - and then No (In_Out_Constits) - and then No (Out_Constits) - and then No (Proof_In_Constits); + No_Constit := + No (In_Constits) + and then No (In_Out_Constits) + and then No (Out_Constits) + and then No (Proof_In_Constits); -- For Input states with visible refinement, at least one constituent -- must be used as an Input in the global refinement. @@ -27267,46 +27277,10 @@ package body Sem_Prag is Constits : Elist_Id; Context : Node_Id) is - function Find_Encapsulating_State - (Constit_Id : Entity_Id) return Entity_Id; - -- Given the entity of a constituent, try to find a corresponding - -- encapsulating state that appears in the same context. The routine - -- returns Empty is no such state is found. - - ------------------------------ - -- Find_Encapsulating_State -- - ------------------------------ - - function Find_Encapsulating_State - (Constit_Id : Entity_Id) return Entity_Id - is - State_Id : Entity_Id; - - begin - -- Since a constituent may be part of a larger constituent set, climb - -- the encapsulating state chain looking for a state that appears in - -- the same context. - - State_Id := Encapsulating_State (Constit_Id); - while Present (State_Id) loop - if Contains (States, State_Id) then - return State_Id; - end if; - - State_Id := Encapsulating_State (State_Id); - end loop; - - return Empty; - end Find_Encapsulating_State; - - -- Local variables - Constit_Elmt : Elmt_Id; Constit_Id : Entity_Id; State_Id : Entity_Id; - -- Start of processing for Check_State_And_Constituent_Use - begin -- Nothing to do if there are no states or constituents @@ -27325,7 +27299,7 @@ package body Sem_Prag is -- state that appears in the same context and if this is the case, -- emit an error (SPARK RM 7.2.6(7)). - State_Id := Find_Encapsulating_State (Constit_Id); + State_Id := Find_Encapsulating_State (States, Constit_Id); if Present (State_Id) then Error_Msg_Name_1 := Chars (Constit_Id); @@ -27801,6 +27775,33 @@ package body Sem_Prag is return Num_Primitives (E mod 511); end Entity_Hash; + ------------------------------ + -- Find_Encapsulating_State -- + ------------------------------ + + function Find_Encapsulating_State + (States : Elist_Id; + Constit_Id : Entity_Id) return Entity_Id + is + State_Id : Entity_Id; + + begin + -- Since a constituent may be part of a larger constituent set, climb + -- the encapsulating state chain looking for a state that appears in + -- States. + + State_Id := Encapsulating_State (Constit_Id); + while Present (State_Id) loop + if Contains (States, State_Id) then + return State_Id; + end if; + + State_Id := Encapsulating_State (State_Id); + end loop; + + return Empty; + end Find_Encapsulating_State; + -------------------------- -- Find_Related_Context -- -------------------------- -- 2.7.4