diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 126caade912f..4f853b9a6917 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,157 @@ +2014-01-29 Hristian Kirtchev + + * aspects.adb Add an entry for aspect Part_Of in table + Canonical_Aspect. + * aspects.ads Add an entry for aspect Part_Of in tables Aspect_Id, + Aspect_Argument, Aspect_Names and Aspect_Delay. + * atree.h Define Elist9. + * atree.adb (Elist9): New routine. + (Set_Elist9): New routine. + * atree.ads (Elist9): New routine. + (Set_Elist9): New routine. + * einfo.adb Add Part_Of_Constituents and Encapsulating_State to + the list of node usage. Remove Refined_State from the list of + node usage. + (Encapsulating_State): New routine. + (Get_Pragma): + Handle pragma Part_Of; (Part_Of_Constituents): New routine. + (Refined_State): Removed. + (Set_Encapsulating_State): New routine. + (Set_Part_Of_Constituents): New routine. + (Set_Refined_State): Removed. + (Write_Field9_Name): Add an entry + for Part_Of_Constituents (Write_Field10_Name): Add an entry for + Encapsulating_State. Remove the entry for Refined_State. + * einfo.ads Add new attributes Encapsulating_State + and Part_Of_Constituents alond with their usage in + entities. Remove attribute Refined_State along with its + usage in entities. + (Encapsulating_State): New routine and + pragma Inline. (Get_Pragma): Update the comment on usage. + (Part_Of_Constituents): New routine and pragma Inline. + (Refined_State): Removed along with pragma Inline. + (Set_Encapsulating_State): New routine and pragma Inline. + (Set_Part_Of_Constituents): New routine and pragma Inline. + (Set_Refined_State): Removed along with pragma Inline. + * par-prag.adb Pragma Part_Of does not need any special processing + by the parser. + * sem_ch3.adb (Analyze_Declarations): Remove local variables + Body_Id and Prag. Call separate routines to analyze the + contract of a package [body]. + (Analyze_Object_Contract): + Update the comment on usage. Remove local variables + Items and Nam. Use Get_Pragma rather than traversing the + classification list. Verify whether the lack of indicator + Part_Of agrees with the placement of the variable in state space. + (Analyze_Object_Declaration): Initialize the encapsulating state + of a variable. (Requires_State_Refinement): Moved to sem_util. + * sem_ch7.adb (Analyze_Package_Body_Contract): New routine. + (Analyze_Package_Contract): New routine. + * sem_ch7.ads (Analyze_Package_Body_Contract): New routine. + (Analyze_Package_Contract): New routine. + * sem_ch10.adb (Decorate_State): Initialize the encapsulating + state and Part_Of constituents. + * sem_ch13.adb (Analyze_Aspect_Specifications): + Add processing for aspect Part_Of. Update all + calls to Decorate_Delayed_Aspect_And_Pragma. + (Check_Aspect_At_Freeze_Point): Aspect Part_Of does + not need any special processing at freeze time. + (Decorate_Delayed_Aspect_And_Pragma): Renamed to + Decorate_Aspect_And_Pragma. Add formal parameter Delayed and + update the associated comment. + * sem_prag.adb Add an entry for pragma Part_Of in table Sig_Flags. + (Analyze_Abstract_State): Add new global variable State_Id. Remove + local constants Errors and Loc. Remove local variables Is_Null + and State_Nam. Create the entity of the abstract state on the + spot, before all remaining checks are performed. Verify that a + missing Part_Of option agrees with the placement of the abstract + state within the state space. + (Analyze_Depends_In_Decl_Part): + Add new global variables Constits_Seen and States_Seen. Check + that a state and a corresponding constituent do not appear + in pragma [Refined_]Depends. + (Analyze_Global_In_Decl_Part): + Add new global variables Constits_Seen and States_Seen. Check + that a state and a corresponding constituent do not appear + in pragma [Refined_]Global. + (Analyze_Global_Item): + Remove the now obsolete code that deals with Part_Of. + Add the entity of the global item to the list of processed + items. (Analyze_Initializes_In_Decl_Part): Add new global + variables Constits_Seen and States_Seen. Check that a state + and a corresponding constituent do not appear in pragma + Initializes. + (Analyze_Initialization_Item): Add the entity + of the initialization item to the list of processed items. + (Analyze_Input_Item): Add the entity of the initialization + item to the list of processed items. + (Analyze_Input_Output): + Remove the now obsolete code that deals with Part_Of. Add the + entity of the input/output to the list of processed items. + (Analyze_Part_Of): New routine. + (Analyze_Part_Of_Option): Remove + local constant Par_State. Add local constant Encaps and local + variables Encaps_Id and Legal. Use Analyze_Part of to analyze + the option. Turn the related state into a Part_Of constituent + if the option is legal. + (Analyze_Pragma): Add processing + for pragma Part_Of. + (Analyze_Refined_State_In_Decl_Part): + Remove global constants Pack_Body and Spec_Id. Remove + global variables Abstr_States and Hidden_States. Add new + global variables Available_States, Body_Id, Body_States and + Spec_Id. Add new local constant Body_Decl. Reimplement the + logic that extracts the states available for refinement from + the related package and the body hidden states of the said + package. + (Analyze_Refinement_Clause): Add local variable Part_Of_Constits. + (Check_Applicable_Policy): Alphabetize body. + (Check_Dependency_Clause): Replace Refined_State + with Encapsulating_State. + (Check_Matching_Constituent): + Reimplement the logic that determines whether an item is a valid + / invalid constituent of the current refined state. Return when + a construct does not denote a valid abstract state. Extract the + list of Part_Of constituents for further analysis. Check that all + Part_Of constituents of a state have been used in its refinement. + (Check_Matching_State): Update the comment on usage. Operate + on the list of available states. + (Check_Missing_Part_Of): New routine. + (Check_Refined_Global_Item): Replace Refined_State + with Encapsulating_State. + (Check_State_And_Constituent_Use): New routine. + (Create_Abstract_State): New routine. + (Is_Matching_Input): Replace Refined_State with Encapsulating_State. + (Is_Part_Of): Removed. + (Collect_Body_States): New routine. + (Collect_Constituent): Replace Refined_State with Encapsulating_State. + (Collect_Hidden_States): Removed. + (Report_Unrefined_States): Change the profile of the procedure along + with the comment on usage. + (Report_Unused_Constituents): New routine. + (Report_Unused_Hidden_States): Removed. + (Report_Unused_States): New routine. + * sem_prag.ads (Check_Missing_Part_Of): New routine. + * sem_util.adb (Add_Contract_Item): Pragma Part_Of can now + appear in the classification pragmas of a package instantiation + or a variable. + (Find_Placement_In_State_Space): New routine. + (Is_Child): Removed. + (Is_Child_Or_Sibling): Remove formal + parameter Private_Child. Remove the private child checks. + (Requires_State_Refinement): Moved from sem_ch3. + * sem_util.ads Add new type State_Space_Kind along with + comment on its usage and values. + (Add_Contract_Item): Update the comment on usage. + (Find_Body_Discriminal): Alphabetize spec. + (Find_Placement_In_State_Space): New routine. + (Is_Child_Or_Sibling): Remove formal parameter Private_Child + and update the comment on usage. + (Requires_State_Refinement): Moved from sem_ch3. + * sinfo.ads: Update the documentation of N_Contract. + * snames.ads-tmpl The predefined name for Part_Of is now used + to denote a pragma. Add Pragma_Id for Part_Of. + 2014-01-29 Emmanuel Briot * s-regexp.adb (Create_Secondary_Table): Automatically grow the state diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index e3ff78d0bc08..cff2b811c626 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -523,6 +523,7 @@ package body Aspects is Aspect_Object_Size => Aspect_Object_Size, Aspect_Output => Aspect_Output, Aspect_Pack => Aspect_Pack, + Aspect_Part_Of => Aspect_Part_Of, Aspect_Persistent_BSS => Aspect_Persistent_BSS, Aspect_Post => Aspect_Post, Aspect_Postcondition => Aspect_Post, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 5b76f6a6562f..1ba3ee0ecceb 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -107,6 +107,7 @@ package Aspects is Aspect_Machine_Radix, Aspect_Object_Size, -- GNAT Aspect_Output, + Aspect_Part_Of, -- GNAT Aspect_Post, Aspect_Postcondition, Aspect_Pre, @@ -330,6 +331,7 @@ package Aspects is Aspect_Machine_Radix => Expression, Aspect_Object_Size => Expression, Aspect_Output => Name, + Aspect_Part_Of => Expression, Aspect_Post => Expression, Aspect_Postcondition => Expression, Aspect_Pre => Expression, @@ -429,6 +431,7 @@ package Aspects is Aspect_Object_Size => Name_Object_Size, Aspect_Output => Name_Output, Aspect_Pack => Name_Pack, + Aspect_Part_Of => Name_Part_Of, Aspect_Persistent_BSS => Name_Persistent_BSS, Aspect_Post => Name_Post, Aspect_Postcondition => Name_Postcondition, @@ -679,6 +682,7 @@ package Aspects is Aspect_Convention => Never_Delay, Aspect_Dimension => Never_Delay, Aspect_Dimension_System => Never_Delay, + Aspect_Part_Of => Never_Delay, Aspect_Refined_Post => Never_Delay, Aspect_SPARK_Mode => Never_Delay, Aspect_Synchronization => Never_Delay, diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 86820b45e459..e4592359bb5d 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -2758,6 +2758,17 @@ package body Atree is end if; end Elist8; + function Elist9 (N : Node_Id) return Elist_Id is + pragma Assert (Nkind (N) in N_Entity); + Value : constant Union_Id := Nodes.Table (N + 1).Field9; + begin + if Value = 0 then + return No_Elist; + else + return Elist_Id (Value); + end if; + end Elist9; + function Elist10 (N : Node_Id) return Elist_Id is pragma Assert (Nkind (N) in N_Entity); Value : constant Union_Id := Nodes.Table (N + 1).Field10; @@ -5476,6 +5487,12 @@ package body Atree is Nodes.Table (N + 1).Field8 := Union_Id (Val); end Set_Elist8; + procedure Set_Elist9 (N : Node_Id; Val : Elist_Id) is + begin + pragma Assert (Nkind (N) in N_Entity); + Nodes.Table (N + 1).Field9 := Union_Id (Val); + end Set_Elist9; + procedure Set_Elist10 (N : Node_Id; Val : Elist_Id) is begin pragma Assert (Nkind (N) in N_Entity); diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads index d5b3bca3f0c7..48b6858af4cb 100644 --- a/gcc/ada/atree.ads +++ b/gcc/ada/atree.ads @@ -1279,6 +1279,9 @@ package Atree is function Elist8 (N : Node_Id) return Elist_Id; pragma Inline (Elist8); + function Elist9 (N : Node_Id) return Elist_Id; + pragma Inline (Elist9); + function Elist10 (N : Node_Id) return Elist_Id; pragma Inline (Elist10); @@ -2585,6 +2588,9 @@ package Atree is procedure Set_Elist8 (N : Node_Id; Val : Elist_Id); pragma Inline (Set_Elist8); + procedure Set_Elist9 (N : Node_Id; Val : Elist_Id); + pragma Inline (Set_Elist9); + procedure Set_Elist10 (N : Node_Id; Val : Elist_Id); pragma Inline (Set_Elist10); diff --git a/gcc/ada/atree.h b/gcc/ada/atree.h index f3913852e12a..7d603ba425dd 100644 --- a/gcc/ada/atree.h +++ b/gcc/ada/atree.h @@ -501,6 +501,7 @@ extern Node_Id Current_Error_Node; #define Elist4(N) Field4 (N) #define Elist5(N) Field5 (N) #define Elist8(N) Field8 (N) +#define Elist9(N) Field9 (N) #define Elist10(N) Field10 (N) #define Elist13(N) Field13 (N) #define Elist15(N) Field15 (N) diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 8d81ce8ff26b..cc1c23f51612 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -86,14 +86,15 @@ package body Einfo is -- Class_Wide_Type Node9 -- Current_Value Node9 + -- Part_Of_Constituents Elist9 -- Renaming_Map Uint9 + -- Encapsulating_State Node10 -- Direct_Primitive_Operations Elist10 -- Discriminal_Link Node10 -- Float_Rep Uint10 (but returns Float_Rep_Kind) -- Handler_Records List10 -- Normalized_Position_Max Uint10 - -- Refined_State Node10 -- Component_Bit_Offset Uint11 -- Full_View Node11 @@ -1059,6 +1060,12 @@ package body Einfo is return Flag174 (Id); end Elaboration_Entity_Required; + function Encapsulating_State (Id : E) return N is + begin + pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable)); + return Node10 (Id); + end Encapsulating_State; + function Enclosing_Scope (Id : E) return E is begin return Node18 (Id); @@ -2630,6 +2637,12 @@ package body Einfo is return Node19 (Base_Type (Id)); end Parent_Subtype; + function Part_Of_Constituents (Id : E) return L is + begin + pragma Assert (Ekind (Id) = E_Abstract_State); + return Elist9 (Id); + end Part_Of_Constituents; + function Postcondition_Proc (Id : E) return E is begin pragma Assert (Ekind (Id) = E_Procedure); @@ -2705,12 +2718,6 @@ package body Einfo is return Flag227 (Id); end Referenced_As_Out_Parameter; - function Refined_State (Id : E) return N is - begin - pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable)); - return Node10 (Id); - end Refined_State; - function Refinement_Constituents (Id : E) return L is begin pragma Assert (Ekind (Id) = E_Abstract_State); @@ -3714,6 +3721,12 @@ package body Einfo is Set_Flag174 (Id, V); end Set_Elaboration_Entity_Required; + procedure Set_Encapsulating_State (Id : E; V : E) is + begin + pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable)); + Set_Node10 (Id, V); + end Set_Encapsulating_State; + procedure Set_Enclosing_Scope (Id : E; V : E) is begin Set_Node18 (Id, V); @@ -5352,6 +5365,12 @@ package body Einfo is Set_Node19 (Id, V); end Set_Parent_Subtype; + procedure Set_Part_Of_Constituents (Id : E; V : L) is + begin + pragma Assert (Ekind (Id) = E_Abstract_State); + Set_Elist9 (Id, V); + end Set_Part_Of_Constituents; + procedure Set_Postcondition_Proc (Id : E; V : E) is begin pragma Assert (Ekind (Id) = E_Procedure); @@ -5435,12 +5454,6 @@ package body Einfo is Set_Flag227 (Id, V); end Set_Referenced_As_Out_Parameter; - procedure Set_Refined_State (Id : E; V : E) is - begin - pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable)); - Set_Node10 (Id, V); - end Set_Refined_State; - procedure Set_Refinement_Constituents (Id : E; V : L) is begin pragma Assert (Ekind (Id) = E_Abstract_State); @@ -6445,6 +6458,7 @@ package body Einfo is Id = Pragma_Global or else Id = Pragma_Initial_Condition or else Id = Pragma_Initializes or else + Id = Pragma_Part_Of or else Id = Pragma_Refined_Depends or else Id = Pragma_Refined_Global or else Id = Pragma_Refined_State; @@ -8535,6 +8549,9 @@ package body Einfo is when Object_Kind => Write_Str ("Current_Value"); + when E_Abstract_State => + Write_Str ("Part_Of_Constituents"); + when E_Function | E_Generic_Function | E_Generic_Package | @@ -8555,6 +8572,10 @@ package body Einfo is procedure Write_Field10_Name (Id : Entity_Id) is begin case Ekind (Id) is + when E_Abstract_State | + E_Variable => + Write_Str ("Encapsulating_State"); + when Class_Wide_Kind | Incomplete_Kind | E_Record_Type | @@ -8580,10 +8601,6 @@ package body Einfo is E_Discriminant => Write_Str ("Normalized_Position_Max"); - when E_Abstract_State | - E_Variable => - Write_Str ("Refined_State"); - when others => Write_Str ("Field10??"); end case; diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 352574311c0c..538af8ae56e8 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -976,6 +976,10 @@ package Einfo is -- then if there is no other elaboration code, obviously there is no -- need to set the flag. +-- Encapsulating_State (Node10) +-- Defined in abstract states and variables. Contains the entity of an +-- ancestor state whose refinement utilizes this item as a constituent. + -- Enclosing_Scope (Node18) -- Defined in labels. Denotes the innermost enclosing construct that -- contains the label. Identical to the scope of the label, except for @@ -3435,6 +3439,10 @@ package Einfo is -- case it points to the subtype of the parent type. This is the type -- that is used as the Etype of the _parent field. +-- Part_Of_Constituents (Elist9) +-- Present in abstract state entities. Contains all constituents that are +-- subject to indicator Part_Of (both aspect and option variants). + -- Postcondition_Proc (Node8) -- Defined only in procedure entities, saves the entity of the generated -- postcondition proc if one is present, otherwise is set to Empty. Used @@ -3549,10 +3557,6 @@ package Einfo is -- we have a separate warning for variables that are only assigned and -- never read, and out parameters are a special case. --- Refined_State (Node10) --- Defined in abstract states and variables. Contains the entity of an --- ancestor state whose refinement mentions this item. - -- Refinement_Constituents (Elist8) -- Present in abstract state entities. Contains all the constituents that -- refine the state, in other words, all the hidden states that appear in @@ -5146,7 +5150,8 @@ package Einfo is -- E_Abstract_State -- Refinement_Constituents (Elist8) - -- Refined_State (Node10) + -- Part_Of_Constituents (Elist9) + -- Encapsulating_State (Node10) -- Body_References (Elist16) -- Non_Limited_View (Node17) -- From_Limited_With (Flag159) @@ -5982,7 +5987,7 @@ package Einfo is -- E_Variable -- Hiding_Loop_Variable (Node8) -- Current_Value (Node9) - -- Refined_State (Node10) + -- Encapsulating_State (Node10) -- Esize (Uint12) -- Extra_Accessibility (Node13) -- Alignment (Uint14) @@ -6328,6 +6333,7 @@ package Einfo is function Elaborate_Body_Desirable (Id : E) return B; function Elaboration_Entity (Id : E) return E; function Elaboration_Entity_Required (Id : E) return B; + function Encapsulating_State (Id : E) return E; function Enclosing_Scope (Id : E) return E; function Entry_Accepted (Id : E) return B; function Entry_Bodies_Array (Id : E) return E; @@ -6604,6 +6610,7 @@ package Einfo is function Package_Instantiation (Id : E) return N; function Packed_Array_Type (Id : E) return E; function Parent_Subtype (Id : E) return E; + function Part_Of_Constituents (Id : E) return L; function Postcondition_Proc (Id : E) return E; function Prival (Id : E) return E; function Prival_Link (Id : E) return E; @@ -6617,7 +6624,6 @@ package Einfo is function Referenced (Id : E) return B; function Referenced_As_LHS (Id : E) return B; function Referenced_As_Out_Parameter (Id : E) return B; - function Refined_State (Id : E) return E; function Refinement_Constituents (Id : E) return L; function Register_Exception_Call (Id : E) return N; function Related_Array_Object (Id : E) return E; @@ -6949,6 +6955,7 @@ package Einfo is procedure Set_Elaborate_Body_Desirable (Id : E; V : B := True); procedure Set_Elaboration_Entity (Id : E; V : E); procedure Set_Elaboration_Entity_Required (Id : E; V : B := True); + procedure Set_Encapsulating_State (Id : E; V : E); procedure Set_Enclosing_Scope (Id : E; V : E); procedure Set_Entry_Accepted (Id : E; V : B := True); procedure Set_Entry_Bodies_Array (Id : E; V : E); @@ -7228,6 +7235,7 @@ package Einfo is procedure Set_Package_Instantiation (Id : E; V : N); procedure Set_Packed_Array_Type (Id : E; V : E); procedure Set_Parent_Subtype (Id : E; V : E); + procedure Set_Part_Of_Constituents (Id : E; V : L); procedure Set_Postcondition_Proc (Id : E; V : E); procedure Set_Prival (Id : E; V : E); procedure Set_Prival_Link (Id : E; V : E); @@ -7241,7 +7249,6 @@ package Einfo is procedure Set_Referenced (Id : E; V : B := True); procedure Set_Referenced_As_LHS (Id : E; V : B := True); procedure Set_Referenced_As_Out_Parameter (Id : E; V : B := True); - procedure Set_Refined_State (Id : E; V : E); procedure Set_Refinement_Constituents (Id : E; V : L); procedure Set_Register_Exception_Call (Id : E; V : N); procedure Set_Related_Array_Object (Id : E; V : E); @@ -7504,6 +7511,7 @@ package Einfo is -- Global -- Initial_Condition -- Initializes + -- Part_Of -- Precondition -- Postcondition -- Refined_Depends @@ -7680,6 +7688,7 @@ package Einfo is pragma Inline (Elaborate_Body_Desirable); pragma Inline (Elaboration_Entity); pragma Inline (Elaboration_Entity_Required); + pragma Inline (Encapsulating_State); pragma Inline (Enclosing_Scope); pragma Inline (Entry_Accepted); pragma Inline (Entry_Bodies_Array); @@ -8000,6 +8009,7 @@ package Einfo is pragma Inline (Packed_Array_Type); pragma Inline (Parameter_Mode); pragma Inline (Parent_Subtype); + pragma Inline (Part_Of_Constituents); pragma Inline (Postcondition_Proc); pragma Inline (Prival); pragma Inline (Prival_Link); @@ -8013,7 +8023,6 @@ package Einfo is pragma Inline (Referenced); pragma Inline (Referenced_As_LHS); pragma Inline (Referenced_As_Out_Parameter); - pragma Inline (Refined_State); pragma Inline (Refinement_Constituents); pragma Inline (Register_Exception_Call); pragma Inline (Related_Array_Object); @@ -8149,6 +8158,7 @@ package Einfo is pragma Inline (Set_Elaborate_Body_Desirable); pragma Inline (Set_Elaboration_Entity); pragma Inline (Set_Elaboration_Entity_Required); + pragma Inline (Set_Encapsulating_State); pragma Inline (Set_Enclosing_Scope); pragma Inline (Set_Entry_Accepted); pragma Inline (Set_Entry_Bodies_Array); @@ -8424,6 +8434,7 @@ package Einfo is pragma Inline (Set_Package_Instantiation); pragma Inline (Set_Packed_Array_Type); pragma Inline (Set_Parent_Subtype); + pragma Inline (Set_Part_Of_Constituents); pragma Inline (Set_Postcondition_Proc); pragma Inline (Set_Prival); pragma Inline (Set_Prival_Link); @@ -8437,7 +8448,6 @@ package Einfo is pragma Inline (Set_Referenced); pragma Inline (Set_Referenced_As_LHS); pragma Inline (Set_Referenced_As_Out_Parameter); - pragma Inline (Set_Refined_State); pragma Inline (Set_Refinement_Constituents); pragma Inline (Set_Register_Exception_Call); pragma Inline (Set_Related_Array_Object); diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 0d70800973e8..5b2f4487ffbf 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1236,6 +1236,7 @@ begin Pragma_Overflow_Mode | Pragma_Overriding_Renamings | Pragma_Pack | + Pragma_Part_Of | Pragma_Partition_Elaboration_Policy | Pragma_Passive | Pragma_Preelaborable_Initialization | diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index 257de8ee4145..cedcab7b7948 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.adb @@ -5532,8 +5532,9 @@ package body Sem_Ch10 is Set_Ekind (Ent, E_Abstract_State); Set_Etype (Ent, Standard_Void_Type); Set_Scope (Ent, Scop); - Set_Refined_State (Ent, Empty); + Set_Encapsulating_State (Ent, Empty); Set_Refinement_Constituents (Ent, New_Elmt_List); + Set_Part_Of_Constituents (Ent, New_Elmt_List); end Decorate_State; ------------------- diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 61db885924ce..68a6e354587d 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1140,33 +1140,35 @@ package body Sem_Ch13 is ----------------------------------- procedure Analyze_Aspect_Specifications (N : Node_Id; E : Entity_Id) is - procedure Decorate_Delayed_Aspect_And_Pragma - (Asp : Node_Id; - Prag : Node_Id); - -- Establish the linkages between a delayed aspect and its corresponding - -- pragma. Set all delay-related flags on both constructs. + procedure Decorate_Aspect_And_Pragma + (Asp : Node_Id; + Prag : Node_Id; + Delayed : Boolean := False); + -- Establish the linkages between an aspect and its corresponding + -- pragma. Flag Delayed should be set when both constructs are delayed. procedure Insert_Delayed_Pragma (Prag : Node_Id); -- Insert a postcondition-like pragma into the tree depending on the -- context. Prag must denote one of the following: Pre, Post, Depends, -- Global or Contract_Cases. - ---------------------------------------- - -- Decorate_Delayed_Aspect_And_Pragma -- - ---------------------------------------- + -------------------------------- + -- Decorate_Aspect_And_Pragma -- + -------------------------------- - procedure Decorate_Delayed_Aspect_And_Pragma - (Asp : Node_Id; - Prag : Node_Id) + procedure Decorate_Aspect_And_Pragma + (Asp : Node_Id; + Prag : Node_Id; + Delayed : Boolean := False) is begin - Set_Aspect_Rep_Item (Asp, Prag); + Set_Aspect_Rep_Item (Asp, Prag); Set_Corresponding_Aspect (Prag, Asp); Set_From_Aspect_Specification (Prag); - Set_Is_Delayed_Aspect (Prag); - Set_Is_Delayed_Aspect (Asp); + Set_Is_Delayed_Aspect (Prag, Delayed); + Set_Is_Delayed_Aspect (Asp, Delayed); Set_Parent (Prag, Asp); - end Decorate_Delayed_Aspect_And_Pragma; + end Decorate_Aspect_And_Pragma; --------------------------- -- Insert_Delayed_Pragma -- @@ -2004,7 +2006,7 @@ package body Sem_Ch13 is Make_Pragma_Argument_Association (Loc, Expression => Relocate_Node (Expr))), Pragma_Name => Name_Abstract_State); - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + Decorate_Aspect_And_Pragma (Aspect, Aitem); if No (Decls) then Decls := New_List; @@ -2036,7 +2038,8 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Name_Depends); - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + Decorate_Aspect_And_Pragma + (Aspect, Aitem, Delayed => True); Insert_Delayed_Pragma (Aitem); goto Continue; @@ -2054,7 +2057,8 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Name_Global); - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + Decorate_Aspect_And_Pragma + (Aspect, Aitem, Delayed => True); Insert_Delayed_Pragma (Aitem); goto Continue; @@ -2079,7 +2083,9 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Name_Initial_Condition); - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + + Decorate_Aspect_And_Pragma + (Aspect, Aitem, Delayed => True); if No (Decls) then Decls := New_List; @@ -2117,7 +2123,9 @@ package body Sem_Ch13 is Make_Pragma_Argument_Association (Loc, Expression => Relocate_Node (Expr))), Pragma_Name => Name_Initializes); - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + + Decorate_Aspect_And_Pragma + (Aspect, Aitem, Delayed => True); if No (Decls) then Decls := New_List; @@ -2135,6 +2143,24 @@ package body Sem_Ch13 is goto Continue; end Initializes; + -- Part_Of + + when Aspect_Part_Of => + if Nkind_In (N, N_Object_Declaration, + N_Package_Instantiation) + then + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Part_Of); + + else + Error_Msg_NE + ("aspect & must apply to a variable or package " + & "instantiation", Aspect, Id); + end if; + -- SPARK_Mode when Aspect_SPARK_Mode => SPARK_Mode : declare @@ -2152,7 +2178,8 @@ package body Sem_Ch13 is -- emulate the behavior of a source pragma. if Nkind (N) = N_Package_Body then - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + Decorate_Aspect_And_Pragma (Aspect, Aitem); + Decls := Declarations (N); if No (Decls) then @@ -2168,7 +2195,8 @@ package body Sem_Ch13 is -- declarations to emulate the behavior of a source pragma. elsif Nkind (N) = N_Package_Declaration then - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + Decorate_Aspect_And_Pragma (Aspect, Aitem); + Decls := Visible_Declarations (Specification (N)); if No (Decls) then @@ -2195,7 +2223,8 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Name_Refined_Depends); - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + Decorate_Aspect_And_Pragma + (Aspect, Aitem, Delayed => True); Insert_Delayed_Pragma (Aitem); goto Continue; @@ -2213,7 +2242,8 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Name_Refined_Global); - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + Decorate_Aspect_And_Pragma + (Aspect, Aitem, Delayed => True); Insert_Delayed_Pragma (Aitem); goto Continue; @@ -2245,7 +2275,7 @@ package body Sem_Ch13 is Make_Pragma_Argument_Association (Loc, Expression => Relocate_Node (Expr))), Pragma_Name => Name_Refined_State); - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + Decorate_Aspect_And_Pragma (Aspect, Aitem); if No (Decls) then Decls := New_List; @@ -2515,7 +2545,8 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Nam); - Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + Decorate_Aspect_And_Pragma + (Aspect, Aitem, Delayed => True); Insert_Delayed_Pragma (Aitem); goto Continue; @@ -7989,6 +8020,7 @@ package body Sem_Ch13 is Aspect_Implicit_Dereference | Aspect_Initial_Condition | Aspect_Initializes | + Aspect_Part_Of | Aspect_Post | Aspect_Postcondition | Aspect_Pre | diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 56bd43a00371..2cc3ea3e4d4e 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -99,6 +99,7 @@ package body Sem_Ch3 is -- Async_Writers -- Effective_Reads -- Effective_Writes + -- Part_Of procedure Build_Derived_Type (N : Node_Id; @@ -2086,12 +2087,6 @@ package body Sem_Ch3 is -- If the states have visible refinement, remove the visibility of each -- constituent at the end of the package body declarations. - function Requires_State_Refinement - (Spec_Id : Entity_Id; - Body_Id : Entity_Id) return Boolean; - -- Determine whether a package denoted by its spec and body entities - -- requires refinement of abstract states. - ----------------- -- Adjust_Decl -- ----------------- @@ -2185,89 +2180,11 @@ package body Sem_Ch3 is end if; end Remove_Visible_Refinements; - ------------------------------- - -- Requires_State_Refinement -- - ------------------------------- - - function Requires_State_Refinement - (Spec_Id : Entity_Id; - Body_Id : Entity_Id) return Boolean - is - function Mode_Is_Off (Prag : Node_Id) return Boolean; - -- Given pragma SPARK_Mode, determine whether the mode is Off - - ----------------- - -- Mode_Is_Off -- - ----------------- - - function Mode_Is_Off (Prag : Node_Id) return Boolean is - Mode : Node_Id; - - begin - -- The default SPARK mode is On - - if No (Prag) then - return False; - end if; - - Mode := - Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag))); - - -- Then the pragma lacks an argument, the default mode is On - - if No (Mode) then - return False; - else - return Chars (Mode) = Name_Off; - end if; - end Mode_Is_Off; - - -- Start of processing for Requires_State_Refinement - - begin - -- A package that does not define at least one abstract state cannot - -- possibly require refinement. - - if No (Abstract_States (Spec_Id)) then - return False; - - -- The package instroduces a single null state which does not merit - -- refinement. - - elsif Has_Null_Abstract_State (Spec_Id) then - return False; - - -- Check whether the package body is subject to pragma SPARK_Mode. If - -- it is and the mode is Off, the package body is considered to be in - -- regular Ada and does not require refinement. - - elsif Mode_Is_Off (SPARK_Pragma (Body_Id)) then - return False; - - -- The body's SPARK_Mode may be inherited from a similar pragma that - -- appears in the private declarations of the spec. The pragma we are - -- interested appears as the second entry in SPARK_Pragma. - - elsif Present (SPARK_Pragma (Spec_Id)) - and then Mode_Is_Off (Next_Pragma (SPARK_Pragma (Spec_Id))) - then - return False; - - -- The spec defines at least one abstract state and the body has no - -- way of circumventing the refinement. - - else - return True; - end if; - end Requires_State_Refinement; - -- Local variables - Body_Id : Entity_Id; Context : Node_Id; Freeze_From : Entity_Id := Empty; Next_Decl : Node_Id; - Prag : Node_Id; Spec_Id : Entity_Id; Body_Seen : Boolean := False; @@ -2415,54 +2332,21 @@ package body Sem_Ch3 is Decl := Next_Decl; end loop; + -- Analyze the contracts of packages and their bodies + if Present (L) then Context := Parent (L); - -- Analyze pragmas Initializes and Initial_Condition of a package at - -- the end of the visible declarations as the pragmas have visibility - -- over the said region. - if Nkind (Context) = N_Package_Specification and then L = Visible_Declarations (Context) then - Spec_Id := Defining_Entity (Parent (Context)); - Prag := Get_Pragma (Spec_Id, Pragma_Initializes); - - if Present (Prag) then - Analyze_Initializes_In_Decl_Part (Prag); - end if; - - Prag := Get_Pragma (Spec_Id, Pragma_Initial_Condition); - - if Present (Prag) then - Analyze_Initial_Condition_In_Decl_Part (Prag); - end if; - - -- Analyze the state refinements within a package body now, after - -- all hidden states have been encountered and freely visible. - -- Refinements must be processed before pragmas Refined_Depends and - -- Refined_Global because the last two may mention constituents. + Analyze_Package_Contract (Defining_Entity (Context)); 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); - -- The analysis of pragma Refined_State detects whether the spec - -- has abstract states available for refinement. - - if Present (Prag) then - Analyze_Refined_State_In_Decl_Part (Prag); - - -- State refinement is required when the package declaration has - -- abstract states. Null states are not considered. - - elsif Requires_State_Refinement (Spec_Id, Body_Id) then - Error_Msg_NE - ("package & requires state refinement", Context, Spec_Id); - end if; + Analyze_Package_Body_Contract (Defining_Entity (Context)); end if; end if; @@ -2472,14 +2356,14 @@ package body Sem_Ch3 is Decl := First (L); while Present (Decl) loop - if Nkind (Decl) = N_Subprogram_Body then + if Nkind (Decl) = N_Object_Declaration then + Analyze_Object_Contract (Defining_Entity (Decl)); + + elsif Nkind (Decl) = N_Subprogram_Body then Analyze_Subprogram_Body_Contract (Defining_Entity (Decl)); elsif Nkind (Decl) = N_Subprogram_Declaration then Analyze_Subprogram_Contract (Defining_Entity (Decl)); - - elsif Nkind (Decl) = N_Object_Declaration then - Analyze_Object_Contract (Defining_Entity (Decl)); end if; Next (Decl); @@ -3078,8 +2962,6 @@ package body Sem_Ch3 is AW_Val : Boolean := False; ER_Val : Boolean := False; EW_Val : Boolean := False; - Items : Node_Id; - Nam : Name_Id; Prag : Node_Id; Seen : Boolean := False; @@ -3127,45 +3009,50 @@ package body Sem_Ch3 is end if; end if; - -- Examine the contract + -- Analyze all external properties - Items := Contract (Obj_Id); + Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers); - if Present (Items) then - - -- Analyze classification pragmas - - Prag := Classifications (Items); - while Present (Prag) loop - Nam := Pragma_Name (Prag); - - if Nam = Name_Async_Readers then - Analyze_External_Property_In_Decl_Part (Prag, AR_Val); - Seen := True; - - elsif Nam = Name_Async_Writers then - Analyze_External_Property_In_Decl_Part (Prag, AW_Val); - Seen := True; - - elsif Nam = Name_Effective_Reads then - Analyze_External_Property_In_Decl_Part (Prag, ER_Val); - Seen := True; - - else pragma Assert (Nam = Name_Effective_Writes); - Analyze_External_Property_In_Decl_Part (Prag, EW_Val); - Seen := True; - end if; - - Prag := Next_Pragma (Prag); - end loop; + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, AR_Val); + Seen := True; end if; - -- Once all external properties have been processed, verify their - -- mutual interaction. + Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers); + + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, AW_Val); + Seen := True; + end if; + + Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads); + + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, ER_Val); + Seen := True; + end if; + + Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes); + + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, EW_Val); + Seen := True; + end if; + + -- Verify the mutual interaction of the various external properties if Seen then Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); end if; + + -- Check whether the lack of indicator Part_Of agrees with the + -- placement of the variable with respect to the state space. + + Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); + + if No (Prag) then + Check_Missing_Part_Of (Obj_Id); + end if; end if; end Analyze_Object_Contract; @@ -4117,7 +4004,7 @@ package body Sem_Ch3 is -- common destination for legal and illegal object declarations. if Ekind (Id) = E_Variable then - Set_Refined_State (Id, Empty); + Set_Encapsulating_State (Id, Empty); end if; if Has_Aspects (N) then diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index d0d80ba2b212..4b3b613e8da7 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -174,6 +174,31 @@ package body Sem_Ch7 is end if; end Analyze_Package_Body; + ----------------------------------- + -- Analyze_Package_Body_Contract -- + ----------------------------------- + + procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id) is + Spec_Id : constant Entity_Id := Spec_Entity (Body_Id); + Prag : Node_Id; + + begin + Prag := Get_Pragma (Body_Id, Pragma_Refined_State); + + -- The analysis of pragma Refined_State detects whether the spec has + -- abstract states available for refinement. + + if Present (Prag) then + Analyze_Refined_State_In_Decl_Part (Prag); + + -- State refinement is required when the package declaration has + -- abstract states. Null states are not considered. + + elsif Requires_State_Refinement (Spec_Id, Body_Id) then + Error_Msg_N ("package & requires state refinement", Spec_Id); + end if; + end Analyze_Package_Body_Contract; + --------------------------------- -- Analyze_Package_Body_Helper -- --------------------------------- @@ -801,6 +826,41 @@ package body Sem_Ch7 is end if; end Analyze_Package_Body_Helper; + ------------------------------ + -- Analyze_Package_Contract -- + ------------------------------ + + procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is + Prag : Node_Id; + + begin + -- Analyze the initialization related pragmas. Initializes must come + -- before Initial_Condition due to item dependencies. + + Prag := Get_Pragma (Pack_Id, Pragma_Initializes); + + if Present (Prag) then + Analyze_Initializes_In_Decl_Part (Prag); + end if; + + Prag := Get_Pragma (Pack_Id, Pragma_Initial_Condition); + + if Present (Prag) then + Analyze_Initial_Condition_In_Decl_Part (Prag); + end if; + + -- Check whether the lack of indicator Part_Of agrees with the placement + -- of the package instantiation with respect to the state space. + + if Is_Generic_Instance (Pack_Id) then + Prag := Get_Pragma (Pack_Id, Pragma_Part_Of); + + if No (Prag) then + Check_Missing_Part_Of (Pack_Id); + end if; + end if; + end Analyze_Package_Contract; + --------------------------------- -- Analyze_Package_Declaration -- --------------------------------- @@ -2850,8 +2910,7 @@ package body Sem_Ch7 is not Is_Null_State (Node (First_Elmt (Abstract_States (P)))) then Error_Msg_N - ("?Y?info: & requires body (non-null abstract state aspect)", - P); + ("?Y?info: & requires body (non-null abstract state aspect)", P); end if; -- Otherwise search entity chain for entity requiring completion diff --git a/gcc/ada/sem_ch7.ads b/gcc/ada/sem_ch7.ads index 783fc57efa0a..2ee0c9ebbb39 100644 --- a/gcc/ada/sem_ch7.ads +++ b/gcc/ada/sem_ch7.ads @@ -32,6 +32,20 @@ package Sem_Ch7 is procedure Analyze_Package_Specification (N : Node_Id); procedure Analyze_Private_Type_Declaration (N : Node_Id); + procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id); + -- Analyze all delayed aspects chained on the contract of package body + -- Body_Id as if they appeared at the end of a declarative region. The + -- aspects in consideration are: + -- Refined_State + + procedure Analyze_Package_Contract (Pack_Id : Entity_Id); + -- Analyze all delayed aspects chained on the contract of package Pack_Id + -- as if they appeared at the end of a declarative region. The aspects in + -- consideration are: + -- Initial_Condition + -- Initializes + -- Part_Of + procedure End_Package_Scope (P : Entity_Id); -- Calls Uninstall_Declarations, and then pops the scope stack diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index b6846d452997..d976438b854e 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -203,6 +203,15 @@ package body Sem_Prag is -- _Post, _Invariant, or _Type_Invariant, which are special names used -- in identifiers to represent these attribute references. + procedure Check_State_And_Constituent_Use + (States : Elist_Id; + Constits : Elist_Id; + Context : Node_Id); + -- Subsidiary to the analysis of pragmas [Refined_]Depends, [Refined_] + -- Global and Initializes. Determine whether a state from list States and a + -- corresponding constituent from list Constits (if any) appear in the same + -- context denoted by Context. If this is the case, emit an error. + procedure Collect_Global_Items (Prag : Node_Id; In_Items : in out Elist_Id; @@ -259,14 +268,6 @@ package body Sem_Prag is -- Get_SPARK_Mode_Type. Convert a name into a corresponding value of type -- SPARK_Mode_Type. - function Is_Part_Of - (State : Entity_Id; - Ancestor : Entity_Id) return Boolean; - -- Subsidiary to the processing of pragma Refined_Depends and pragma - -- Refined_Global. Determine whether abstract state State is part of an - -- ancestor abstract state Ancestor. For this relationship to hold, State - -- must have option Part_Of in its Abstract_State definition. - function Is_Unconstrained_Or_Tagged_Item (Item : Entity_Id) return Boolean; -- Subsidiary to Collect_Subprogram_Inputs_Outputs and the analysis of -- pragma Depends. Determine whether the type of dependency item Item is @@ -502,6 +503,11 @@ package body Sem_Prag is -- The list is populated with unique entities because output items are -- unique in a dependence relation. + Constits_Seen : Elist_Id := No_Elist; + -- A list containing the entities of all constituents processed so far. + -- It aids in detecting illegal usage of a state and a corresponding + -- constituent in pragma [Refinde_]Depends. + Global_Seen : Boolean := False; -- A flag set when pragma Global has been processed @@ -514,6 +520,11 @@ package body Sem_Prag is Spec_Id : Entity_Id; -- The entity of the subprogram subject to pragma [Refined_]Depends + States_Seen : Elist_Id := No_Elist; + -- A list containing the entities of all states processed so far. It + -- helps in detecting illegal usage of a state and a corresponding + -- constituent in pragma [Refined_]Depends. + Subp_Id : Entity_Id; -- The entity of the subprogram [body or stub] subject to pragma -- [Refined_]Depends. @@ -831,35 +842,14 @@ package body Sem_Prag is Add_Item (Item_Id, All_Inputs_Seen); end if; - if Ekind (Item_Id) = E_Abstract_State then - - -- The state acts as a constituent of some other - -- state. Ensure that the other state is a proper - -- ancestor of the item. - - if Present (Refined_State (Item_Id)) then - if not Is_Part_Of - (Item_Id, Refined_State (Item_Id)) - then - Error_Msg_Name_1 := - Chars (Refined_State (Item_Id)); - Error_Msg_NE - ("state & is not a valid constituent of " - & "ancestor state %", Item, Item_Id); - return; - end if; - - -- An abstract state with visible refinement cannot - -- appear in pragma [Refined_]Global as its place must - -- be taken by some of its constituents. - - elsif Has_Visible_Refinement (Item_Id) then - Error_Msg_NE - ("cannot mention state & in global refinement, " - & "use its constituents instead (SPARK RM " - & "6.1.5(3))", Item, Item_Id); - return; - end if; + if Ekind (Item_Id) = E_Abstract_State + and then Has_Visible_Refinement (Item_Id) + then + Error_Msg_NE + ("cannot mention state & in global refinement, use " + & "its constituents instead (SPARK RM 6.1.5(3))", + Item, Item_Id); + return; end if; -- When the item renames an entire object, replace the @@ -871,6 +861,19 @@ package body Sem_Prag is Analyze (Item); end if; + -- Add the entity of the current item to the list of + -- processed items. + + if Ekind (Item_Id) = E_Abstract_State then + Add_Item (Item_Id, States_Seen); + end if; + + if Ekind_In (Item_Id, E_Abstract_State, E_Variable) + and then Present (Encapsulating_State (Item_Id)) + then + Add_Item (Item_Id, Constits_Seen); + end if; + -- All other input/output items are illegal else @@ -1703,6 +1706,14 @@ package body Sem_Prag is else Error_Msg_N ("malformed dependency relation", Clause); end if; + + -- Ensure that a state and a corresponding constituent do not appear + -- together in pragma [Refined_]Depends. + + Check_State_And_Constituent_Use + (States => States_Seen, + Constits => Constits_Seen, + Context => N); end Analyze_Depends_In_Decl_Part; -------------------------------------------- @@ -1761,6 +1772,11 @@ package body Sem_Prag is --------------------------------- procedure Analyze_Global_In_Decl_Part (N : Node_Id) is + Constits_Seen : Elist_Id := No_Elist; + -- A list containing the entities of all constituents processed so far. + -- It aids in detecting illegal usage of a state and a corresponding + -- constituent in pragma [Refinde_]Global. + Seen : Elist_Id := No_Elist; -- A list containing the entities of all the items processed so far. It -- plays a role in detecting distinct entities. @@ -1768,6 +1784,11 @@ package body Sem_Prag is Spec_Id : Entity_Id; -- The entity of the subprogram subject to pragma [Refined_]Global + States_Seen : Elist_Id := No_Elist; + -- A list containing the entities of all states processed so far. It + -- helps in detecting illegal usage of a state and a corresponding + -- constituent in pragma [Refined_]Global. + Subp_Id : Entity_Id; -- The entity of the subprogram [body or stub] subject to pragma -- [Refined_]Global. @@ -1886,24 +1907,11 @@ package body Sem_Prag is if Ekind (Item_Id) = E_Abstract_State then - -- The state acts as a constituent of some other state. - -- Ensure that the other state is a proper ancestor of the - -- item. - - if Present (Refined_State (Item_Id)) then - if not Is_Part_Of (Item_Id, Refined_State (Item_Id)) then - Error_Msg_Name_1 := Chars (Refined_State (Item_Id)); - Error_Msg_NE - ("state & is not a valid constituent of ancestor " - & "state %", Item, Item_Id); - return; - end if; - -- An abstract state with visible refinement cannot appear -- in pragma [Refined_]Global as its place must be taken by -- some of its constituents. - elsif Has_Visible_Refinement (Item_Id) then + if Has_Visible_Refinement (Item_Id) then Error_Msg_NE ("cannot mention state & in global refinement, use its " & "constituents instead (SPARK RM 6.1.4(8))", @@ -1978,6 +1986,16 @@ package body Sem_Prag is else Add_Item (Item_Id, Seen); + + if Ekind (Item_Id) = E_Abstract_State then + Add_Item (Item_Id, States_Seen); + end if; + + if Ekind_In (Item_Id, E_Abstract_State, E_Variable) + and then Present (Encapsulating_State (Item_Id)) + then + Add_Item (Item_Id, Constits_Seen); + end if; end if; end Analyze_Global_Item; @@ -2227,6 +2245,14 @@ package body Sem_Prag is End_Scope; end if; end if; + + -- Ensure that a state and a corresponding constituent do not appear + -- together in pragma [Refined_]Global. + + Check_State_And_Constituent_Use + (States => States_Seen, + Constits => Constits_Seen, + Context => N); end Analyze_Global_In_Decl_Part; -------------------------------------------- @@ -2425,6 +2451,11 @@ package body Sem_Prag is Pack_Spec : constant Node_Id := Parent (N); Pack_Id : constant Entity_Id := Defining_Entity (Parent (Pack_Spec)); + Constits_Seen : Elist_Id := No_Elist; + -- A list containing the entities of all constituents processed so far. + -- It aids in detecting illegal usage of a state and a corresponding + -- constituent in pragma Initializes. + Items_Seen : Elist_Id := No_Elist; -- A list of all initialization items processed so far. This list is -- used to detect duplicate items. @@ -2438,6 +2469,11 @@ package body Sem_Prag is -- declarations of the related package. This list is used to detect the -- legality of initialization items. + States_Seen : Elist_Id := No_Elist; + -- A list containing the entities of all states processed so far. It + -- helps in detecting illegal usage of a state and a corresponding + -- constituent in pragma Initializes. + procedure Analyze_Initialization_Item (Item : Node_Id); -- Verify the legality of a single initialization item @@ -2510,6 +2546,14 @@ package body Sem_Prag is else Add_Item (Item_Id, Items_Seen); + + if Ekind (Item_Id) = E_Abstract_State then + Add_Item (Item_Id, States_Seen); + end if; + + if Present (Encapsulating_State (Item_Id)) then + Add_Item (Item_Id, Constits_Seen); + end if; end if; -- The item references something that is not a state or a @@ -2607,6 +2651,14 @@ package body Sem_Prag is else Add_Item (Input_Id, Inputs_Seen); + + if Ekind (Input_Id) = E_Abstract_State then + Add_Item (Input_Id, States_Seen); + end if; + + if Present (Encapsulating_State (Input_Id)) then + Add_Item (Input_Id, Constits_Seen); + end if; end if; -- The input references something that is not a state or a @@ -2749,6 +2801,14 @@ package body Sem_Prag is Next (Init); end loop; end if; + + -- Ensure that a state and a corresponding constituent do not appear + -- together in pragma Initializes. + + Check_State_And_Constituent_Use + (States => States_Seen, + Constits => Constits_Seen, + Context => N); end Analyze_Initializes_In_Decl_Part; -------------------- @@ -2794,6 +2854,17 @@ package body Sem_Prag is -- In Ada 95 or 05 mode, these are implementation defined pragmas, so -- should be caught by the No_Implementation_Pragmas restriction. + procedure Analyze_Part_Of + (Item_Id : Entity_Id; + State : Node_Id; + Indic : Node_Id; + Legal : out Boolean); + -- Subsidiary to the analysis of pragmas Abstract_State and Part_Of. + -- Perform full analysis of indicator Part_Of. Item_Id is the entity of + -- an abstract state, variable or package instantiation. State is the + -- encapsulating state. Indic is the Part_Of indicator. Flag Legal is + -- set when the indicator is legal. + procedure Analyze_Refined_Pragma (Spec_Id : out Entity_Id; Body_Id : out Entity_Id; @@ -3344,6 +3415,124 @@ package body Sem_Prag is end if; end Ada_2012_Pragma; + --------------------- + -- Analyze_Part_Of -- + --------------------- + + procedure Analyze_Part_Of + (Item_Id : Entity_Id; + State : Node_Id; + Indic : Node_Id; + Legal : out Boolean) + is + Pack_Id : Entity_Id; + Placement : State_Space_Kind; + State_Id : Entity_Id; + + begin + -- Assume that the pragma/option is illegal + + Legal := False; + + Analyze (State); + Resolve_State (State); + + if Is_Entity_Name (State) + and then Ekind (Entity (State)) = E_Abstract_State + then + State_Id := Entity (State); + + else + Error_Msg_N + ("indicator Part_Of must denote an abstract state", State); + return; + end if; + + -- Determine where the state, variable or the package instantiation + -- lives with respect to the enclosing packages or package bodies (if + -- any). This placement dictates the legality of the encapsulating + -- state. + + Find_Placement_In_State_Space + (Item_Id => Item_Id, + Placement => Placement, + Pack_Id => Pack_Id); + + -- The item appears in a non-package construct with a declarative + -- part (subprogram, block, etc). As such, the item is not allowed + -- to be a part of an encapsulating state because the item is not + -- visible. + + if Placement = Not_In_Package then + Error_Msg_N + ("indicator Part_Of may not appear in this context (SPARK RM " + & "7.2.6(5))", Indic); + Error_Msg_Name_1 := Chars (Scope (State_Id)); + Error_Msg_NE + ("\& is not part of the hidden state of package %", + Indic, Item_Id); + + -- The item appears in the visible state space of some package. In + -- general this scenario does not warrant Part_Of except when the + -- package is a private child unit and the encapsulating state is + -- declared in a parent unit or a public descendant of that parent + -- unit. + + elsif Placement = Visible_State_Space then + if Is_Child_Unit (Pack_Id) + and then Is_Private_Descendant (Pack_Id) + then + if not Is_Child_Or_Sibling (Pack_Id, Scope (State_Id)) then + Error_Msg_N + ("indicator Part_Of must denote an abstract state of " + & "parent unit or descendant (SPARK RM 7.2.6(3))", Indic); + end if; + + -- Indicator Part_Of is not needed when the related package is not + -- a private child unit or a public descendant thereof. + + else + Error_Msg_N + ("indicator Part_Of may not appear in this context (SPARK " + & "RM 7.2.6(5))", Indic); + Error_Msg_Name_1 := Chars (Pack_Id); + Error_Msg_NE + ("\& is declared in the visible part of package %", + Indic, Item_Id); + end if; + + -- When the item appears in the private state space of a package, the + -- encapsulating state must be declared in the same package. + + elsif Placement = Private_State_Space then + if Scope (State_Id) /= Pack_Id then + Error_Msg_NE + ("indicator Part_Of must designate an abstract state of " + & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id); + Error_Msg_Name_1 := Chars (Pack_Id); + Error_Msg_NE + ("\& is declared in the private part of package %", + Indic, Item_Id); + end if; + + -- Items declared in the body state space of a package do not need + -- Part_Of indicators as the refinement has already been seen. + + else + Error_Msg_N + ("indicator Part_Of may not appear in this context (SPARK RM " + & "7.2.6(5))", Indic); + + if Scope (State_Id) = Pack_Id then + Error_Msg_Name_1 := Chars (Pack_Id); + Error_Msg_NE + ("\& is declared in the body of package %", Indic, Item_Id); + end if; + end if; + + Legal := True; + end Analyze_Part_Of; + ---------------------------- -- Analyze_Refined_Pragma -- ---------------------------- @@ -9620,7 +9809,7 @@ package body Sem_Prag is -- Abstract_State -- -------------------- - -- pragma Abstract_State (ABSTRACT_STATE_LIST) + -- pragma Abstract_State (ABSTRACT_STATE_LIST); -- ABSTRACT_STATE_LIST ::= -- null @@ -9697,6 +9886,9 @@ package body Sem_Prag is ER_Val : Boolean := False; EW_Val : Boolean := False; + State_Id : Entity_Id := Empty; + -- The entity to be generated for the current state declaration + procedure Analyze_External_Option (Opt : Node_Id); -- Verify the legality of option External @@ -9725,6 +9917,13 @@ package body Sem_Prag is -- that Prop is not a duplicate property and sets flag Status. -- Opt is not a duplicate property and sets the flag Status. + procedure Create_Abstract_State + (State_Nam : Name_Id; + Is_Null : Boolean := False); + -- Generate an abstract state entity with name State_Nam and + -- enter it into visibility. Flag Is_Null should be set when + -- the associated Abstract_State pragma defines a null state. + ----------------------------- -- Analyze_External_Option -- ----------------------------- @@ -9909,22 +10108,27 @@ package body Sem_Prag is ---------------------------- procedure Analyze_Part_Of_Option (Opt : Node_Id) is - Par_State : constant Node_Id := Expression (Opt); + Encaps : constant Node_Id := Expression (Opt); + Encaps_Id : Entity_Id; + Legal : Boolean; begin Check_Duplicate_Option (Opt, Part_Of_Seen); - Analyze (Par_State); + Analyze_Part_Of + (Item_Id => State_Id, + State => Encaps, + Indic => First (Choices (Opt)), + Legal => Legal); - -- Expression of option Part_Of must denote abstract state + -- The Part_Of indicator turns an abstract state into a + -- constituent of the encapsulating state. - if not Is_Entity_Name (Par_State) - or else No (Entity (Par_State)) - or else Ekind (Entity (Par_State)) /= E_Abstract_State - then - Error_Msg_N - ("option Part_Of must denote an abstract state", - Par_State); + if Legal then + Encaps_Id := Entity (Encaps); + + Append_Elmt (State_Id, Part_Of_Constituents (Encaps_Id)); + Set_Encapsulating_State (State_Id, Encaps_Id); end if; end Analyze_Part_Of_Option; @@ -9963,15 +10167,46 @@ package body Sem_Prag is Status := True; end Check_Duplicate_Property; + --------------------------- + -- Create_Abstract_State -- + --------------------------- + + procedure Create_Abstract_State + (State_Nam : Name_Id; + Is_Null : Boolean := False) + is + begin + -- The generated state abstraction reuses the same chars + -- from the original state declaration. Decorate the entity. + + State_Id := + Make_Defining_Identifier (Sloc (State), + Chars => New_External_Name (State_Nam)); + + -- Null states never come from source + + Set_Comes_From_Source (State_Id, not Is_Null); + Set_Parent (State_Id, State); + Set_Ekind (State_Id, E_Abstract_State); + Set_Etype (State_Id, Standard_Void_Type); + Set_Encapsulating_State (State_Id, Empty); + Set_Refinement_Constituents (State_Id, New_Elmt_List); + Set_Part_Of_Constituents (State_Id, New_Elmt_List); + + -- Every non-null state must be nameable and resolvable the + -- same way a constant is. + + if not Is_Null then + Push_Scope (Pack_Id); + Enter_Name (State_Id); + Pop_Scope; + end if; + end Create_Abstract_State; + -- Local variables - Errors : constant Nat := Serious_Errors_Detected; - Loc : constant Source_Ptr := Sloc (State); - Is_Null : Boolean := False; - Opt : Node_Id; - Opt_Nam : Node_Id; - State_Id : Entity_Id; - State_Nam : Name_Id; + Opt : Node_Id; + Opt_Nam : Node_Id; -- Start of processing for Analyze_Abstract_State @@ -9986,8 +10221,9 @@ package body Sem_Prag is -- Null states appear as internally generated entities elsif Nkind (State) = N_Null then - State_Nam := New_Internal_Name ('S'); - Is_Null := True; + Create_Abstract_State + (State_Nam => New_Internal_Name ('S'), + Is_Null => True); Null_Seen := True; -- Catch a case where a null state appears in a list of @@ -10002,7 +10238,7 @@ package body Sem_Prag is -- Simple state declaration elsif Nkind (State) = N_Identifier then - State_Nam := Chars (State); + Create_Abstract_State (Chars (State)); Non_Null_Seen := True; -- State declaration with various options. This construct @@ -10010,7 +10246,7 @@ package body Sem_Prag is elsif Nkind (State) = N_Extension_Aggregate then if Nkind (Ancestor_Part (State)) = N_Identifier then - State_Nam := Chars (Ancestor_Part (State)); + Create_Abstract_State (Chars (Ancestor_Part (State))); Non_Null_Seen := True; else Error_Msg_N @@ -10035,7 +10271,7 @@ package body Sem_Prag is elsif Chars (Opt) = Name_Part_Of then Error_Msg_N - ("option Part_Of must denote an abstract state " + ("indicator Part_Of must denote an abstract state " & "(SPARK RM 7.1.4(9))", Opt); else @@ -10077,47 +10313,33 @@ package body Sem_Prag is Error_Msg_N ("malformed abstract state declaration", State); end if; - -- Do not generate a state abstraction entity if it was not - -- properly declared. + -- Guard against a junk state. In such cases no entity is + -- generated and the subsequent checks cannot be applied. - if Serious_Errors_Detected > Errors then - return; + if Present (State_Id) then + + -- Verify whether the state does not introduce an illegal + -- hidden state within a package subject to a null abstract + -- state. + + Check_No_Hidden_State (State_Id); + + -- Check whether the lack of option Part_Of agrees with the + -- placement of the abstract state with respect to the state + -- space. + + if not Part_Of_Seen then + Check_Missing_Part_Of (State_Id); + end if; + + -- Associate the state with its related package + + if No (Abstract_States (Pack_Id)) then + Set_Abstract_States (Pack_Id, New_Elmt_List); + end if; + + Append_Elmt (State_Id, Abstract_States (Pack_Id)); end if; - - -- The generated state abstraction reuses the same characters - -- from the original state declaration. Decorate the entity. - - State_Id := - Make_Defining_Identifier (Loc, New_External_Name (State_Nam)); - - Set_Comes_From_Source (State_Id, not Is_Null); - Set_Parent (State_Id, State); - Set_Ekind (State_Id, E_Abstract_State); - Set_Etype (State_Id, Standard_Void_Type); - Set_Refined_State (State_Id, Empty); - Set_Refinement_Constituents (State_Id, New_Elmt_List); - - -- Every non-null state must be nameable and resolvable the - -- same way a constant is. - - if not Is_Null then - Push_Scope (Pack_Id); - Enter_Name (State_Id); - Pop_Scope; - end if; - - -- Verify whether the state introduces an illegal hidden state - -- within a package subject to a null abstract state. - - Check_No_Hidden_State (State_Id); - - -- Associate the state with its related package - - if No (Abstract_States (Pack_Id)) then - Set_Abstract_States (Pack_Id, New_Elmt_List); - end if; - - Append_Elmt (State_Id, Abstract_States (Pack_Id)); end Analyze_Abstract_State; -- Local variables @@ -16774,6 +16996,212 @@ package body Sem_Prag is when Pragma_Page => null; + ------------- + -- Part_Of -- + ------------- + + -- pragma Part_Of (ABSTRACT_STATE); + + -- ABSTRACT_STATE ::= name + + when Pragma_Part_Of => Part_Of : declare + procedure Propagate_Part_Of + (Pack_Id : Entity_Id; + State_Id : Entity_Id; + Instance : Node_Id); + -- Propagate the Part_Of indicator to all abstract states and + -- variables declared in the visible state space of a package + -- denoted by Pack_Id. State_Id is the encapsulating state. + -- Instance is the package instantiation node. + + ----------------------- + -- Propagate_Part_Of -- + ----------------------- + + procedure Propagate_Part_Of + (Pack_Id : Entity_Id; + State_Id : Entity_Id; + Instance : Node_Id) + is + Has_Item : Boolean := False; + -- Flag set when the visible state space contains at least one + -- abstract state or variable. + + procedure Propagate_Part_Of (Pack_Id : Entity_Id); + -- Propagate the Part_Of indicator to all abstract states and + -- variables declared in the visible state space of a package + -- denoted by Pack_Id. + + ----------------------- + -- Propagate_Part_Of -- + ----------------------- + + procedure Propagate_Part_Of (Pack_Id : Entity_Id) is + Item_Id : Entity_Id; + + begin + -- Traverse the entity chain of the package and set relevant + -- attributes of abstract states and variables declared in + -- the visible state space of the package. + + Item_Id := First_Entity (Pack_Id); + while Present (Item_Id) + and then not In_Private_Part (Item_Id) + loop + -- Do not consider internally generated items + + if not Comes_From_Source (Item_Id) then + null; + + -- The Part_Of indicator turns an abstract state or + -- variable into a constituent of the encapsulating + -- state. + + elsif Ekind_In (Item_Id, E_Abstract_State, + E_Variable) + then + Has_Item := True; + + Append_Elmt (Item_Id, Part_Of_Constituents (State_Id)); + Set_Encapsulating_State (Item_Id, State_Id); + + -- Recursively handle nested packages and instantiations + + elsif Ekind (Item_Id) = E_Package then + Propagate_Part_Of (Item_Id); + end if; + + Next_Entity (Item_Id); + end loop; + end Propagate_Part_Of; + + -- Start of processing for Propagate_Part_Of + + begin + Propagate_Part_Of (Pack_Id); + + -- Detect a package instantiation that is subject to a Part_Of + -- indicator, but has no visible state. + + if not Has_Item then + Error_Msg_NE + ("package instantiation & has Part_Of indicator but " + & "lacks visible state", Instance, Pack_Id); + end if; + end Propagate_Part_Of; + + -- Local variables + + Item_Id : Entity_Id; + Legal : Boolean; + State : Node_Id; + State_Id : Entity_Id; + Stmt : Node_Id; + + -- Start of processing for Part_Of + + begin + GNAT_Pragma; + Check_Arg_Count (1); + + -- Ensure the proper placement of the pragma. Part_Of must appear + -- on a variable declaration or a package instantiation. + + Stmt := Prev (N); + while Present (Stmt) loop + + -- Skip prior pragmas, but check for duplicates + + if Nkind (Stmt) = N_Pragma then + if Pragma_Name (Stmt) = Pname then + Error_Msg_Name_1 := Pname; + Error_Msg_Sloc := Sloc (Stmt); + Error_Msg_N ("pragma% duplicates pragma declared#", N); + end if; + + -- Skip internally generated code + + elsif not Comes_From_Source (Stmt) then + null; + + -- The pragma applies to an object declaration (possibly a + -- variable) or a package instantiation. Stop the traversal + -- and continue the analysis. + + elsif Nkind_In (Stmt, N_Object_Declaration, + N_Package_Instantiation) + then + exit; + + -- The pragma does not apply to a legal construct, issue an + -- error and stop the analysis. + + else + Pragma_Misplaced; + return; + end if; + + Stmt := Prev (Stmt); + end loop; + + -- When the context is an object declaration, ensure that we are + -- dealing with a variable. + + if Nkind (Stmt) = N_Object_Declaration + and then Ekind (Defining_Entity (Stmt)) /= E_Variable + then + Error_Msg_N ("indicator Part_Of must apply to a variable", N); + return; + end if; + + -- Extract the entity of the related object declaration or package + -- instantiation. In the case of the instantiation, use the entity + -- of the instance spec. + + if Nkind (Stmt) = N_Package_Instantiation then + Stmt := Instance_Spec (Stmt); + end if; + + Item_Id := Defining_Entity (Stmt); + State := Get_Pragma_Arg (Arg1); + + -- Detect any discrepancies between the placement of the object + -- or package instantiation with respect to state space and the + -- encapsulating state. + + Analyze_Part_Of + (Item_Id => Item_Id, + State => State, + Indic => N, + Legal => Legal); + + if Legal then + State_Id := Entity (State); + + -- Add the pragma to the contract of the item. This aids with + -- the detection of a missing but required Part_Of indicator. + + Add_Contract_Item (N, Item_Id); + + -- The Part_Of indicator turns a variable into a constituent + -- of the encapsulating state. + + if Ekind (Item_Id) = E_Variable then + Append_Elmt (Item_Id, Part_Of_Constituents (State_Id)); + Set_Encapsulating_State (Item_Id, State_Id); + + -- Propagate the Part_Of indicator to the visible state space + -- of the package instantiation. + + else + Propagate_Part_Of + (Pack_Id => Item_Id, + State_Id => State_Id, + Instance => Stmt); + end if; + end if; + end Part_Of; + ---------------------------------- -- Partition_Elaboration_Policy -- ---------------------------------- @@ -20911,8 +21339,8 @@ package body Sem_Prag is if Ekind_In (Ref_Id, E_Abstract_State, E_Variable) - and then Present (Refined_State (Ref_Id)) - and then Refined_State (Ref_Id) = Dep_Id + and then Present (Encapsulating_State (Ref_Id)) + and then Encapsulating_State (Ref_Id) = Dep_Id then Has_Constituent := True; Remove (Ref_Input); @@ -21211,8 +21639,8 @@ package body Sem_Prag is -- per the example above. if Ekind_In (Ref_Id, E_Abstract_State, E_Variable) - and then Present (Refined_State (Ref_Id)) - and then Refined_State (Ref_Id) = Dep_Id + and then Present (Encapsulating_State (Ref_Id)) + and then Encapsulating_State (Ref_Id) = Dep_Id and then Inputs_Match (Ref_Clause, Do_Checks => False) then @@ -21957,7 +22385,7 @@ package body Sem_Prag is -- The state or variable acts as a constituent of a state, collect -- it for the state completeness checks performed later on. - if Present (Refined_State (Item_Id)) then + if Present (Encapsulating_State (Item_Id)) then if Global_Mode = Name_Input then Add_Item (Item_Id, In_Constits); @@ -22245,40 +22673,41 @@ package body Sem_Prag is ---------------------------------------- procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id) is - Pack_Body : constant Node_Id := Parent (N); - Spec_Id : constant Entity_Id := Corresponding_Spec (Pack_Body); + Available_States : Elist_Id := No_Elist; + -- A list of all abstract states defined in the package declaration that + -- are available for refinement. The list is used to report unrefined + -- states. - Abstr_States : Elist_Id := No_Elist; - -- A list of all abstract states defined in the package declaration. The - -- list is used to report unrefined states. + Body_Id : Entity_Id; + -- The body entity of the package subject to pragma Refined_State + + Body_States : Elist_Id := No_Elist; + -- A list of all hidden states that appear in the body of the related + -- package. The list is used to report unused hidden states. Constituents_Seen : Elist_Id := No_Elist; -- A list that contains all constituents processed so far. The list is -- used to detect multiple uses of the same constituent. - Hidden_States : Elist_Id := No_Elist; - -- A list of all hidden states (abstract states and variables) that - -- appear in the package spec and body. The list is used to report - -- unused hidden states. - Refined_States_Seen : Elist_Id := No_Elist; -- A list that contains all refined states processed so far. The list is -- used to detect duplicate refinements. + Spec_Id : Entity_Id; + -- The spec entity of the package subject to pragma Refined_State + procedure Analyze_Refinement_Clause (Clause : Node_Id); -- Perform full analysis of a single refinement clause - procedure Collect_Hidden_States; - -- Gather the entities of all hidden states that appear in the spec and - -- body of the related package in Hidden_States. + function Collect_Body_States (Pack_Id : Entity_Id) return Elist_Id; + -- Gather the entities of all abstract states and variables declared in + -- the body state space of package Pack_Id. - procedure Report_Unrefined_States; - -- Emit errors for all abstract states that have not been refined by - -- the pragma. + procedure Report_Unrefined_States (States : Elist_Id); + -- Emit errors for all unrefined abstract states found in list States - procedure Report_Unused_Hidden_States; - -- Emit errors for all hidden states of the related package that do not - -- participate in a refinement. + procedure Report_Unused_States (States : Elist_Id); + -- Emit errors for all unused states found in list States ------------------------------- -- Analyze_Refinement_Clause -- @@ -22302,9 +22731,13 @@ package body Sem_Prag is -- Flags used to detect multiple uses of null in a single clause or a -- mixture of null and non-null constituents. + Part_Of_Constits : Elist_Id := No_Elist; + -- A list of all candidate constituents subject to indicator Part_Of + -- where the encapsulating state is the current state. + State : Node_Id; State_Id : Entity_Id; - -- The state being refined in the current clause + -- The current state being refined procedure Analyze_Constituent (Constit : Node_Id); -- Perform full analysis of a single constituent @@ -22319,10 +22752,13 @@ package body Sem_Prag is -- this is not the case, emit an error message. procedure Check_Matching_State; - -- Determine whether the state being refined appears in Abstr_States. - -- Emit an error when attempting to re-refine the state or when the - -- state is not defined in the package declaration. Otherwise remove - -- the state from Abstr_States. + -- Determine whether the state being refined appears in list + -- Available_States. Emit an error when attempting to re-refine the + -- state or when the state is not defined in the package declaration, + -- otherwise remove the state from Available_States. + + procedure Report_Unused_Constituents (Constits : Elist_Id); + -- Emit errors for all unused Part_Of constituents in list Constits ------------------------- -- Analyze_Constituent -- @@ -22355,12 +22791,12 @@ package body Sem_Prag is Add_Item (Constit_Id, Constituents_Seen); - -- Collect the constituent in the list of refinement items. - -- Establish a relation between the refined state and its - -- constituent. + -- Collect the constituent in the list of refinement items + -- and establish a relation between the refined state and + -- the item. Append_Elmt (Constit_Id, Refinement_Constituents (State_Id)); - Set_Refined_State (Constit_Id, State_Id); + Set_Encapsulating_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 @@ -22405,70 +22841,59 @@ package body Sem_Prag is Error_Msg_NE ("duplicate use of constituent &", Constit, Constit_Id); return; + end if; - -- A state can act as a constituent only when it is part of - -- another state. This relation is expressed by option Part_Of - -- of pragma Abstract_State. + -- The constituent is subject to a Part_Of indicator - elsif Ekind (Constit_Id) = E_Abstract_State then - if not Is_Part_Of (Constit_Id, State_Id) then + if Present (Encapsulating_State (Constit_Id)) then + if Encapsulating_State (Constit_Id) = State_Id then + Remove (Part_Of_Constits, Constit_Id); + Collect_Constituent; + + -- The constituent is part of another state and is used + -- incorrectly in the refinement of the current state. + + else Error_Msg_Name_1 := Chars (State_Id); Error_Msg_NE - ("state & is not a valid constituent of ancestor " - & "state %", Constit, Constit_Id); - return; - - -- The constituent has the proper Part_Of option, but may - -- not appear in the immediate hidden state of the related - -- package. This case arises when the constituent appears - -- in a private child or a private sibling. Recognize these - -- scenarios and collect the constituent. - - elsif Is_Child_Or_Sibling - (Pack_1 => Scope (State_Id), - Pack_2 => Scope (Constit_Id), - Private_Child => True) - then - Collect_Constituent; - return; + ("& cannot act as constituent of state %", + Constit, Constit_Id); + Error_Msg_NE + ("\Part_Of indicator specifies & as encapsulating " + & "state", Constit, Encapsulating_State (Constit_Id)); end if; + + -- The only other source of legal constituents is the body + -- state space of the related package. + + else + if Present (Body_States) then + State_Elmt := First_Elmt (Body_States); + while Present (State_Elmt) loop + + -- Consume a valid constituent to signal that it has + -- been encountered. + + if Node (State_Elmt) = Constit_Id then + Remove_Elmt (Body_States, State_Elmt); + Collect_Constituent; + return; + end if; + + Next_Elmt (State_Elmt); + end loop; + end if; + + -- If we get here, then the constituent is not a hidden + -- state of the related package and may not be used in a + -- refinement. + + Error_Msg_Name_1 := Chars (Spec_Id); + Error_Msg_NE + ("cannot use & in refinement, constituent is not a hidden " + & "state of package % (SPARK RM 7.2.2(9))", + Constit, Constit_Id); end if; - - -- Inspect the hidden states of the related package looking for - -- a match. - - if Present (Hidden_States) then - State_Elmt := First_Elmt (Hidden_States); - while Present (State_Elmt) loop - - -- A valid hidden state or variable acts as a constituent - - if Node (State_Elmt) = Constit_Id then - - -- Add the constituent to the lis of processed items - -- to aid with the detection of duplicates. Remove the - -- constituent from Hidden_States to signal that it - -- has already been matched. - - Add_Item (Constit_Id, Constituents_Seen); - Remove_Elmt (Hidden_States, State_Elmt); - - Collect_Constituent; - return; - end if; - - Next_Elmt (State_Elmt); - end loop; - end if; - - -- If we get here, we are refining a state that is not hidden - -- with respect to the related package. - - Error_Msg_Name_1 := Chars (Spec_Id); - Error_Msg_NE - ("cannot use & in refinement, constituent is not a hidden " - & "state of package % (SPARK RM 7.2.2(9))", - Constit, Constit_Id); end Check_Matching_Constituent; -- Local variables @@ -22593,18 +23018,18 @@ package body Sem_Prag is -- Inspect the abstract states defined in the package declaration -- looking for a match. - State_Elmt := First_Elmt (Abstr_States); + State_Elmt := First_Elmt (Available_States); while Present (State_Elmt) loop -- A valid abstract state is being refined in the body. Add -- the state to the list of processed refined states to aid -- with the detection of duplicate refinements. Remove the - -- state from Abstr_States to signal that it has already been - -- refined. + -- state from Available_States to signal that it has already + -- been refined. if Node (State_Elmt) = State_Id then Add_Item (State_Id, Refined_States_Seen); - Remove_Elmt (Abstr_States, State_Elmt); + Remove_Elmt (Available_States, State_Elmt); return; end if; @@ -22620,6 +23045,49 @@ package body Sem_Prag is State, State_Id); end Check_Matching_State; + -------------------------------- + -- Report_Unused_Constituents -- + -------------------------------- + + procedure Report_Unused_Constituents (Constits : Elist_Id) is + Constit_Elmt : Elmt_Id; + Constit_Id : Entity_Id; + Posted : Boolean := False; + + begin + if Present (Constits) then + Constit_Elmt := First_Elmt (Constits); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); + + -- Generate an error message of the form: + + -- state ... has unused Part_Of constituents + -- abstract state ... defined at ... + -- variable ... defined at ... + + if not Posted then + Posted := True; + Error_Msg_NE + ("state & has unused Part_Of constituents", + State, State_Id); + end if; + + Error_Msg_Sloc := Sloc (Constit_Id); + + if Ekind (Constit_Id) = E_Abstract_State then + Error_Msg_NE + ("\ abstract state & defined #", State, Constit_Id); + else + Error_Msg_NE + ("\ variable & defined #", State, Constit_Id); + end if; + + Next_Elmt (Constit_Elmt); + end loop; + end if; + end Report_Unused_Constituents; + -- Local declarations Body_Ref : Node_Id; @@ -22651,6 +23119,7 @@ package body Sem_Prag is else Error_Msg_NE ("& must denote an abstract state", State, State_Id); + return; end if; -- A global item cannot denote a state abstraction whose @@ -22673,10 +23142,11 @@ package body Sem_Prag is end loop; end if; - -- The state name is illegal + -- The state name is illegal else Error_Msg_N ("malformed state name in refinement clause", State); + return; end if; -- A refinement clause may only refine one state at a time @@ -22688,6 +23158,11 @@ package body Sem_Prag is ("refinement clause cannot cover multiple states", Extra_State); end if; + -- Replicate the Part_Of constituents of the refined state because + -- the algorithm will consume items. + + Part_Of_Constits := New_Copy_Elist (Part_Of_Constituents (State_Id)); + -- Analyze all constituents of the refinement. Multiple constituents -- appear as an aggregate. @@ -22768,98 +23243,112 @@ package body Sem_Prag is ("non-external state & cannot contain external constituents in " & "refinement (SPARK RM 7.2.8(1))", State, State_Id); end if; + + -- Ensure that all Part_Of candidate constituents have been mentioned + -- in the refinement clause. + + Report_Unused_Constituents (Part_Of_Constits); end Analyze_Refinement_Clause; - --------------------------- - -- Collect_Hidden_States -- - --------------------------- + ------------------------- + -- Collect_Body_States -- + ------------------------- - procedure Collect_Hidden_States is - procedure Collect_Hidden_States_In_Decls (Decls : List_Id); - -- Find all hidden states that appear in declarative list Decls and - -- append their entities to Result. + function Collect_Body_States (Pack_Id : Entity_Id) return Elist_Id is + Result : Elist_Id := No_Elist; + -- A list containing all body states of Pack_Id - ------------------------------------ - -- Collect_Hidden_States_In_Decls -- - ------------------------------------ + procedure Collect_Visible_States (Pack_Id : Entity_Id); + -- Gather the entities of all abstract states and variables declared + -- in the visible state space of package Pack_Id. - procedure Collect_Hidden_States_In_Decls (Decls : List_Id) is - procedure Collect_Abstract_States (States : Elist_Id); - -- Copy the abstract states defined in list States to list Result + ---------------------------- + -- Collect_Visible_States -- + ---------------------------- - ----------------------------- - -- Collect_Abstract_States -- - ----------------------------- - - procedure Collect_Abstract_States (States : Elist_Id) is - State_Elmt : Elmt_Id; - begin - if Present (States) then - State_Elmt := First_Elmt (States); - while Present (State_Elmt) loop - Add_Item (Node (State_Elmt), Hidden_States); - Next_Elmt (State_Elmt); - end loop; - end if; - end Collect_Abstract_States; - - -- Local variables - - Decl : Node_Id; - - -- Start of processing for Collect_Hidden_States_In_Decls + procedure Collect_Visible_States (Pack_Id : Entity_Id) is + Item_Id : Entity_Id; begin - Decl := First (Decls); - while Present (Decl) loop + -- Traverse the entity chain of the package and inspect all + -- visible items. - -- Source objects (non-constants) are valid hidden states + Item_Id := First_Entity (Pack_Id); + while Present (Item_Id) and then not In_Private_Part (Item_Id) loop - if Nkind (Decl) = N_Object_Declaration - and then Ekind (Defining_Entity (Decl)) = E_Variable - and then Comes_From_Source (Decl) - then - Add_Item (Defining_Entity (Decl), Hidden_States); + -- Do not consider internally generated items as those cannot + -- be named and participate in refinement. - -- Gather the abstract states of a package along with all - -- hidden states in its visible declarations. + if not Comes_From_Source (Item_Id) then + null; - elsif Nkind (Decl) = N_Package_Declaration then - Collect_Abstract_States - (Abstract_States (Defining_Entity (Decl))); + elsif Ekind_In (Item_Id, E_Abstract_State, E_Variable) then + Add_Item (Item_Id, Result); - Collect_Hidden_States_In_Decls - (Visible_Declarations (Specification (Decl))); + -- Recursively gather the visible states of a nested package + + elsif Ekind (Item_Id) = E_Package then + Collect_Visible_States (Item_Id); end if; - Next (Decl); + Next_Entity (Item_Id); end loop; - end Collect_Hidden_States_In_Decls; + end Collect_Visible_States; -- Local variables - Pack_Spec : constant Node_Id := Package_Specification (Spec_Id); + Pack_Body : constant Node_Id := + Declaration_Node (Body_Entity (Pack_Id)); + Decl : Node_Id; + Item_Id : Entity_Id; - -- Start of processing for Collect_Hidden_States + -- Start of processing for Collect_Body_States begin - -- Process the private declarations of the package spec and the - -- declarations of the body. + -- Inspect the declarations of the body looking for source variables, + -- packages and package instantiations. - Collect_Hidden_States_In_Decls (Private_Declarations (Pack_Spec)); - Collect_Hidden_States_In_Decls (Declarations (Pack_Body)); - end Collect_Hidden_States; + Decl := First (Declarations (Pack_Body)); + while Present (Decl) loop + if Nkind (Decl) = N_Object_Declaration then + Item_Id := Defining_Entity (Decl); + + -- Capture source variables only as internally generated + -- temporaries cannot be named and participate in refinement. + + if Ekind (Item_Id) = E_Variable + and then Comes_From_Source (Item_Id) + then + Add_Item (Item_Id, Result); + end if; + + elsif Nkind (Decl) = N_Package_Declaration then + Item_Id := Defining_Entity (Decl); + + -- Capture the visible abstract states and variables of a + -- source package [instantiation]. + + if Comes_From_Source (Item_Id) then + Collect_Visible_States (Item_Id); + end if; + end if; + + Next (Decl); + end loop; + + return Result; + end Collect_Body_States; ----------------------------- -- Report_Unrefined_States -- ----------------------------- - procedure Report_Unrefined_States is + procedure Report_Unrefined_States (States : Elist_Id) is State_Elmt : Elmt_Id; begin - if Present (Abstr_States) then - State_Elmt := First_Elmt (Abstr_States); + if Present (States) then + State_Elmt := First_Elmt (States); while Present (State_Elmt) loop Error_Msg_N ("abstract state & must be refined", Node (State_Elmt)); @@ -22869,61 +23358,72 @@ package body Sem_Prag is end if; end Report_Unrefined_States; - --------------------------------- - -- Report_Unused_Hidden_States -- - --------------------------------- + -------------------------- + -- Report_Unused_States -- + -------------------------- - procedure Report_Unused_Hidden_States is + procedure Report_Unused_States (States : Elist_Id) is Posted : Boolean := False; State_Elmt : Elmt_Id; State_Id : Entity_Id; begin - if Present (Hidden_States) then - State_Elmt := First_Elmt (Hidden_States); + if Present (States) then + State_Elmt := First_Elmt (States); while Present (State_Elmt) loop State_Id := Node (State_Elmt); -- Generate an error message of the form: - -- package ... has unused hidden states + -- body of package ... has unused hidden states -- abstract state ... defined at ... -- variable ... defined at ... if not Posted then Posted := True; - Error_Msg_NE - ("package & has unused hidden states", N, Spec_Id); + Error_Msg_N + ("body of package & has unused hidden states", Body_Id); end if; Error_Msg_Sloc := Sloc (State_Id); if Ekind (State_Id) = E_Abstract_State then - Error_Msg_NE ("\ abstract state & defined #", N, State_Id); + Error_Msg_NE + ("\ abstract state & defined #", Body_Id, State_Id); else - Error_Msg_NE ("\ variable & defined #", N, State_Id); + Error_Msg_NE ("\ variable & defined #", Body_Id, State_Id); end if; Next_Elmt (State_Elmt); end loop; end if; - end Report_Unused_Hidden_States; + end Report_Unused_States; -- Local declarations - Clauses : constant Node_Id := - Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); - Clause : Node_Id; + Body_Decl : constant Node_Id := Parent (N); + Clauses : constant Node_Id := + Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Clause : Node_Id; -- Start of processing for Analyze_Refined_State_In_Decl_Part begin Set_Analyzed (N); - -- Initialize the various lists used during analysis + Body_Id := Defining_Entity (Body_Decl); + Spec_Id := Corresponding_Spec (Body_Decl); - Abstr_States := New_Copy_Elist (Abstract_States (Spec_Id)); - Collect_Hidden_States; + -- Replicate the abstract states declared by the package because the + -- matching algorithm will consume states. + + Available_States := New_Copy_Elist (Abstract_States (Spec_Id)); + + -- Gather all abstract states and variables declared in the visible + -- state space of the package body. These items must be utilized as + -- constituents in a state refinement. + + Body_States := Collect_Body_States (Spec_Id); -- Multiple non-null state refinements appear as an aggregate @@ -22949,11 +23449,14 @@ package body Sem_Prag is Analyze_Refinement_Clause (Clauses); end if; - -- Ensure that all abstract states have been refined and all hidden - -- states of the related package unilized in refinements. + -- List all abstract states that were left unrefined - Report_Unrefined_States; - Report_Unused_Hidden_States; + Report_Unrefined_States (Available_States); + + -- Ensure that all abstract states and variables declared in the body + -- state space of the related package are utilized as constituents. + + Report_Unused_States (Body_States); end Analyze_Refined_State_In_Decl_Part; ------------------------------------ @@ -23013,6 +23516,85 @@ package body Sem_Prag is return False; end Appears_In; + ----------------------------- + -- Check_Applicable_Policy -- + ----------------------------- + + procedure Check_Applicable_Policy (N : Node_Id) is + PP : Node_Id; + Policy : Name_Id; + + Ename : constant Name_Id := Original_Aspect_Name (N); + + begin + -- No effect if not valid assertion kind name + + if not Is_Valid_Assertion_Kind (Ename) then + return; + end if; + + -- Loop through entries in check policy list + + PP := Opt.Check_Policy_List; + while Present (PP) loop + declare + PPA : constant List_Id := Pragma_Argument_Associations (PP); + Pnm : constant Name_Id := Chars (Get_Pragma_Arg (First (PPA))); + + begin + if Ename = Pnm + or else Pnm = Name_Assertion + or else (Pnm = Name_Statement_Assertions + and then Nam_In (Ename, Name_Assert, + Name_Assert_And_Cut, + Name_Assume, + Name_Loop_Invariant, + Name_Loop_Variant)) + then + Policy := Chars (Get_Pragma_Arg (Last (PPA))); + + case Policy is + when Name_Off | Name_Ignore => + Set_Is_Ignored (N, True); + Set_Is_Checked (N, False); + + when Name_On | Name_Check => + Set_Is_Checked (N, True); + Set_Is_Ignored (N, False); + + when Name_Disable => + Set_Is_Ignored (N, True); + Set_Is_Checked (N, False); + Set_Is_Disabled (N, True); + + -- That should be exhaustive, the null here is a defence + -- against a malformed tree from previous errors. + + when others => + null; + end case; + + return; + end if; + + PP := Next_Pragma (PP); + end; + end loop; + + -- If there are no specific entries that matched, then we let the + -- setting of assertions govern. Note that this provides the needed + -- compatibility with the RM for the cases of assertion, invariant, + -- precondition, predicate, and postcondition. + + if Assertions_Enabled then + Set_Is_Checked (N, True); + Set_Is_Ignored (N, False); + else + Set_Is_Checked (N, False); + Set_Is_Ignored (N, True); + end if; + end Check_Applicable_Policy; + ------------------------------- -- Check_External_Properties -- ------------------------------- @@ -23120,84 +23702,154 @@ package body Sem_Prag is end if; end Check_Kind; - ----------------------------- - -- Check_Applicable_Policy -- - ----------------------------- + --------------------------- + -- Check_Missing_Part_Of -- + --------------------------- - procedure Check_Applicable_Policy (N : Node_Id) is - PP : Node_Id; - Policy : Name_Id; - - Ename : constant Name_Id := Original_Aspect_Name (N); + procedure Check_Missing_Part_Of (Item_Id : Entity_Id) is + Pack_Id : Entity_Id; + Placement : State_Space_Kind; begin - -- No effect if not valid assertion kind name + -- Do not consider internally generated entities as these can never + -- have a Part_Of indicator. - if not Is_Valid_Assertion_Kind (Ename) then + if not Comes_From_Source (Item_Id) then + return; + + -- Perform these checks only when SPARK_Mode is enabled as they will + -- interfere with standard Ada rules and produce false positives. + + elsif SPARK_Mode /= On then return; end if; - -- Loop through entries in check policy list + -- Find where the abstract state, variable or package instantiation + -- lives with respect to the state space. - PP := Opt.Check_Policy_List; - while Present (PP) loop - declare - PPA : constant List_Id := Pragma_Argument_Associations (PP); - Pnm : constant Name_Id := Chars (Get_Pragma_Arg (First (PPA))); + Find_Placement_In_State_Space + (Item_Id => Item_Id, + Placement => Placement, + Pack_Id => Pack_Id); - begin - if Ename = Pnm - or else Pnm = Name_Assertion - or else (Pnm = Name_Statement_Assertions - and then Nam_In (Ename, Name_Assert, - Name_Assert_And_Cut, - Name_Assume, - Name_Loop_Invariant, - Name_Loop_Variant)) - then - Policy := Chars (Get_Pragma_Arg (Last (PPA))); + -- Items that appear in a non-package construct (subprogram, block, etc) + -- do not require a Part_Of indicator because they can never act as a + -- hidden state. - case Policy is - when Name_Off | Name_Ignore => - Set_Is_Ignored (N, True); - Set_Is_Checked (N, False); + -- An item declared in the body state space of a package always act as a + -- constituent and does not need explicit Part_Of indicator. - when Name_On | Name_Check => - Set_Is_Checked (N, True); - Set_Is_Ignored (N, False); + -- In general an item declared in the visible state space of a package + -- does not require a Part_Of indicator. The only exception is when the + -- related package is a private child unit in which case Part_Of must + -- denote a state in the parent unit or in one of its descendants. - when Name_Disable => - Set_Is_Ignored (N, True); - Set_Is_Checked (N, False); - Set_Is_Disabled (N, True); + if Placement = Visible_State_Space then + if Is_Child_Unit (Pack_Id) + and then Is_Private_Descendant (Pack_Id) + then + Error_Msg_N + ("indicator Part_Of is required in this context (SPARK RM " + & "7.2.6(3))", Item_Id); + Error_Msg_Name_1 := Chars (Pack_Id); + Error_Msg_N + ("\& is declared in the visible part of private child unit %", + Item_Id); + end if; - -- That should be exhaustive, the null here is a defence - -- against a malformed tree from previous errors. + -- When the item appears in the private state space of a packge, it must + -- be a part of some state declared by the said package. - when others => - null; - end case; + elsif Placement = Private_State_Space then + Error_Msg_N + ("indicator Part_Of is required in this context (SPARK RM " + & "7.2.6(2))", Item_Id); + Error_Msg_Name_1 := Chars (Pack_Id); + Error_Msg_N + ("\& is declared in the private part of package %", Item_Id); + end if; + end Check_Missing_Part_Of; - return; + ------------------------------------- + -- Check_State_And_Constituent_Use -- + ------------------------------------- + + procedure Check_State_And_Constituent_Use + (States : Elist_Id; + 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 encapsulated 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; - PP := Next_Pragma (PP); - end; - end loop; + State_Id := Encapsulating_State (State_Id); + end loop; - -- If there are no specific entries that matched, then we let the - -- setting of assertions govern. Note that this provides the needed - -- compatibility with the RM for the cases of assertion, invariant, - -- precondition, predicate, and postcondition. + return Empty; + end Find_Encapsulating_State; - if Assertions_Enabled then - Set_Is_Checked (N, True); - Set_Is_Ignored (N, False); - else - Set_Is_Checked (N, False); - Set_Is_Ignored (N, True); + -- 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 + + if No (States) or else No (Constits) then + return; end if; - end Check_Applicable_Policy; + + -- Inspect the list of constituents and try to determine whether its + -- encapsulating state is in list States. + + Constit_Elmt := First_Elmt (Constits); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); + + -- Determine whether the constituent is part of an encapsulating + -- state that appears in the same context and if this is the case, + -- emit an error. + + State_Id := Find_Encapsulating_State (Constit_Id); + + if Present (State_Id) then + Error_Msg_Name_1 := Chars (Constit_Id); + Error_Msg_NE + ("cannot mention state & and its constituent % in the same " + & "context (SPARK RM 7.2.6(7))", Context, State_Id); + exit; + end if; + + Next_Elmt (Constit_Elmt); + end loop; + end Check_State_And_Constituent_Use; -------------------------- -- Collect_Global_Items -- @@ -23949,6 +24601,7 @@ package body Sem_Prag is Pragma_Ordered => 0, Pragma_Pack => 0, Pragma_Page => -1, + Pragma_Part_Of => -1, Pragma_Partition_Elaboration_Policy => -1, Pragma_Passive => -1, Pragma_Persistent_BSS => 0, @@ -24091,40 +24744,6 @@ package body Sem_Prag is end if; end Is_Non_Significant_Pragma_Reference; - ---------------- - -- Is_Part_Of -- - ---------------- - - function Is_Part_Of - (State : Entity_Id; - Ancestor : Entity_Id) return Boolean - is - Options : constant Node_Id := Parent (State); - Name : Node_Id; - Option : Node_Id; - Value : Node_Id; - - begin - -- A state declaration with option Part_Of appears as an extension - -- aggregate with component associations. - - if Nkind (Options) = N_Extension_Aggregate then - Option := First (Component_Associations (Options)); - while Present (Option) loop - Name := First (Choices (Option)); - Value := Expression (Option); - - if Chars (Name) = Name_Part_Of then - return Entity (Value) = Ancestor; - end if; - - Next (Option); - end loop; - end if; - - return False; - end Is_Part_Of; - ------------------------------ -- Is_Pragma_String_Literal -- ------------------------------ diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 730643a1c515..9e1d8b397b87 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -139,6 +139,11 @@ package Sem_Prag is -- is the related variable or state. Ensure legality of the combination and -- issue an error for an illegal combination. + procedure Check_Missing_Part_Of (Item_Id : Entity_Id); + -- Determine whether the placement within the state space of an abstract + -- state, variable or package instantiation denoted by Item_Id requires the + -- use of indicator/option Part_Of. If this is the case, emit an error. + function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean; -- N is a pragma appearing in a configuration pragma file. Most such -- pragmas are analyzed when the file is read, before parsing and analyzing diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 8fc28ef4be81..bfc2efeb7820 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -233,11 +233,12 @@ package body Sem_Util is Nam := Original_Aspect_Name (Prag); - -- Contract items related to [generic] packages. The applicable pragmas - -- are: + -- Contract items related to [generic] packages or instantiations. The + -- applicable pragmas are: -- Abstract_States -- Initial_Condition -- Initializes + -- Part_Of (instantiation only) if Ekind_In (Id, E_Generic_Package, E_Package) then if Nam_In (Nam, Name_Abstract_State, @@ -247,6 +248,12 @@ package body Sem_Util is Set_Next_Pragma (Prag, Classifications (Items)); Set_Classifications (Items, Prag); + -- Indicator Part_Of must be associated with a package instantiation + + elsif Nam = Name_Part_Of and then Is_Generic_Instance (Id) then + Set_Next_Pragma (Prag, Classifications (Items)); + Set_Classifications (Items, Prag); + -- The pragma is not a proper contract item else @@ -355,12 +362,14 @@ package body Sem_Util is -- Async_Writers -- Effective_Reads -- Effective_Writes + -- Part_Of elsif Ekind (Id) = E_Variable then if Nam_In (Nam, Name_Async_Readers, Name_Async_Writers, Name_Effective_Reads, - Name_Effective_Writes) + Name_Effective_Writes, + Name_Part_Of) then Set_Next_Pragma (Prag, Classifications (Items)); Set_Classifications (Items, Prag); @@ -4201,6 +4210,7 @@ package body Sem_Util is Set_Defining_Unit_Name (N, Err); return Err; + -- If not an entity, get defining identifier else @@ -5827,6 +5837,75 @@ package body Sem_Util is end if; end Find_Parameter_Type; + ----------------------------------- + -- Find_Placement_In_State_Space -- + ----------------------------------- + + procedure Find_Placement_In_State_Space + (Item_Id : Entity_Id; + Placement : out State_Space_Kind; + Pack_Id : out Entity_Id) + is + Context : Entity_Id; + + begin + -- Assume that the item does not appear in the state space of a package + + Pack_Id := Empty; + + -- Climb the scope stack and examine the enclosing context + + Context := Scope (Item_Id); + while Present (Context) and then Context /= Standard_Standard loop + if Ekind (Context) = E_Package then + Pack_Id := Context; + + -- A package body is a cut off point for the traversal as the item + -- cannot be visible to the outside from this point on. Note that + -- this test must be done first as a body is also classified as a + -- private part. + + if In_Package_Body (Context) then + Placement := Body_State_Space; + return; + + -- The private part of a package is a cut off point for the + -- traversal as the item cannot be visible to the outside from + -- this point on. + + elsif In_Private_Part (Context) then + Placement := Private_State_Space; + return; + + -- When the item appears in the visible state space of a package, + -- continue to climb the scope stack as this may not be the final + -- state space. + + else + Placement := Visible_State_Space; + + -- The visible state space of a private child unit acts as the + -- proper placement of an item. + + if Is_Child_Unit (Context) + and then Is_Private_Descendant (Context) + then + return; + end if; + end if; + + -- The item or its enclosing package appear in a construct that has + -- no state space. + + else + Placement := Not_In_Package; + return; + end if; + + Context := Scope (Context); + end loop; + end Find_Placement_In_State_Space; + ----------------------------- -- Find_Static_Alternative -- ----------------------------- @@ -8948,9 +9027,8 @@ package body Sem_Util is ------------------------- function Is_Child_Or_Sibling - (Pack_1 : Entity_Id; - Pack_2 : Entity_Id; - Private_Child : Boolean) return Boolean + (Pack_1 : Entity_Id; + Pack_2 : Entity_Id) return Boolean is function Distance_From_Standard (Pack : Entity_Id) return Nat; -- Given an arbitrary package, return the number of "climbs" necessary @@ -8964,10 +9042,6 @@ package body Sem_Util is -- climb the scope chain until the said depth is reached. The pointer -- to the package and its depth a modified during the climb. - function Is_Child (Pack : Entity_Id) return Boolean; - -- Given a package Pack, determine whether it is a child package that - -- satisfies the privacy requirement (if set). - ---------------------------- -- Distance_From_Standard -- ---------------------------- @@ -9011,26 +9085,6 @@ package body Sem_Util is end loop; end Equalize_Depths; - -------------- - -- Is_Child -- - -------------- - - function Is_Child (Pack : Entity_Id) return Boolean is - begin - if Is_Child_Unit (Pack) then - if Private_Child then - return Is_Private_Descendant (Pack); - else - return True; - end if; - - -- The package is nested, it cannot act a child or a sibling - - else - return False; - end if; - end Is_Child; - -- Local variables P_1 : Entity_Id := Pack_1; @@ -9062,7 +9116,10 @@ package body Sem_Util is -- P_1 P_1 elsif P_1_Depth > P_2_Depth then - Equalize_Depths (P_1, P_1_Depth, P_2_Depth); + Equalize_Depths + (Pack => P_1, + Depth => P_1_Depth, + Depth_To_Reach => P_2_Depth); P_1_Child := True; -- (root) P_1 @@ -9072,7 +9129,10 @@ package body Sem_Util is -- P_2 P_2 elsif P_2_Depth > P_1_Depth then - Equalize_Depths (P_2, P_2_Depth, P_1_Depth); + Equalize_Depths + (Pack => P_2, + Depth => P_2_Depth, + Depth_To_Reach => P_1_Depth); P_2_Child := True; end if; @@ -9088,9 +9148,10 @@ package body Sem_Util is if P_1 = P_2 then if P_1_Child then - return Is_Child (Pack_1); + return Is_Child_Unit (Pack_1); + else pragma Assert (P_2_Child); - return Is_Child (Pack_2); + return Is_Child_Unit (Pack_2); end if; -- The packages may come from the same package chain or from entirely @@ -9107,7 +9168,7 @@ package body Sem_Util is -- The two packages may be siblings if P_1 = P_2 then - return Is_Child (Pack_1) and then Is_Child (Pack_2); + return Is_Child_Unit (Pack_1) and then Is_Child_Unit (Pack_2); end if; P_1 := Scope (P_1); @@ -14554,6 +14615,81 @@ package body Sem_Util is end if; end Require_Entity; + ------------------------------- + -- Requires_State_Refinement -- + ------------------------------- + + function Requires_State_Refinement + (Spec_Id : Entity_Id; + Body_Id : Entity_Id) return Boolean + is + function Mode_Is_Off (Prag : Node_Id) return Boolean; + -- Given pragma SPARK_Mode, determine whether the mode is Off + + ----------------- + -- Mode_Is_Off -- + ----------------- + + function Mode_Is_Off (Prag : Node_Id) return Boolean is + Mode : Node_Id; + + begin + -- The default SPARK mode is On + + if No (Prag) then + return False; + end if; + + Mode := Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag))); + + -- Then the pragma lacks an argument, the default mode is On + + if No (Mode) then + return False; + else + return Chars (Mode) = Name_Off; + end if; + end Mode_Is_Off; + + -- Start of processing for Requires_State_Refinement + + begin + -- A package that does not define at least one abstract state cannot + -- possibly require refinement. + + if No (Abstract_States (Spec_Id)) then + return False; + + -- The package instroduces a single null state which does not merit + -- refinement. + + elsif Has_Null_Abstract_State (Spec_Id) then + return False; + + -- Check whether the package body is subject to pragma SPARK_Mode. If + -- it is and the mode is Off, the package body is considered to be in + -- regular Ada and does not require refinement. + + elsif Mode_Is_Off (SPARK_Pragma (Body_Id)) then + return False; + + -- The body's SPARK_Mode may be inherited from a similar pragma that + -- appears in the private declarations of the spec. The pragma we are + -- interested appears as the second entry in SPARK_Pragma. + + elsif Present (SPARK_Pragma (Spec_Id)) + and then Mode_Is_Off (Next_Pragma (SPARK_Pragma (Spec_Id))) + then + return False; + + -- The spec defines at least one abstract state and the body has no way + -- of circumventing the refinement. + + else + return True; + end if; + end Requires_State_Refinement; + ------------------------------ -- Requires_Transient_Scope -- ------------------------------ diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 3c512df64fc7..2fe44fc15a4d 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -44,8 +44,9 @@ package Sem_Util is -- freeze node of E. procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id); - -- Add pragma Prag to the contract of an entry, a package [body] or a - -- subprogram [body] denoted by Id. The following are valid pragmas: + -- Add pragma Prag to the contract of an entry, a package [body], a + -- subprogram [body] or variable denoted by Id. The following are valid + -- pragmas: -- Abstract_States -- Async_Readers -- Async_Writers @@ -56,6 +57,7 @@ package Sem_Util is -- Global -- Initial_Condition -- Initializes + -- Part_Of -- Postcondition -- Precondition -- Refined_Depends @@ -571,6 +573,12 @@ package Sem_Util is -- Call is set to the node for the corresponding call. If the node N is not -- an actual parameter then Formal and Call are set to Empty. + function Find_Body_Discriminal + (Spec_Discriminant : Entity_Id) return Entity_Id; + -- Given a discriminant of the record type that implements a task or + -- protected type, return the discriminal of the corresponding discriminant + -- of the actual concurrent type. + function Find_Corresponding_Discriminant (Id : Node_Id; Typ : Entity_Id) return Entity_Id; @@ -600,17 +608,93 @@ package Sem_Util is -- Return the type of formal parameter Param as determined by its -- specification. + -- The following type describes the placement of an arbitrary entity with + -- respect to SPARK visible / hidden state space. + + type State_Space_Kind is + (Not_In_Package, + -- An entity is not in the visible, private or body state space when + -- the immediate enclosing construct is not a package. + + Visible_State_Space, + -- An entity is in the visible state space when it appears immediately + -- within the visible declarations of a package or when it appears in + -- the visible state space of a nested package which in turn is declared + -- in the visible declarations of an enclosing package: + + -- package Pack is + -- Visible_Variable : ... + -- package Nested + -- with Abstract_State => Visible_State + -- is + -- Visible_Nested_Variable : ... + -- end Nested; + -- end Pack; + + -- Entities associated with a package instantiation inherit the state + -- space from the instance placement: + + -- generic + -- package Gen is + -- Generic_Variable : ... + -- end Gen; + + -- with Gen; + -- package Pack is + -- package Inst is new Gen; + -- -- Generic_Variable is in the visible state space of Pack + -- end Pack; + + Private_State_Space, + -- An entity is in the private state space when it appears immediately + -- within the private declarations of a package or when it appears in + -- the visible state space of a nested package which in turn is declared + -- in the private declarations of an enclosing package: + + -- package Pack is + -- private + -- Private_Variable : ... + -- package Nested + -- with Abstract_State => Private_State + -- is + -- Private_Nested_Variable : ... + -- end Nested; + -- end Pack; + + -- The same placement principle applies to package instantiations + + Body_State_Space); + -- An entity is in the body state space when it appears immediately + -- within the declarations of a package body or when it appears in the + -- visible state space of a nested package which in turn is declared in + -- the declarations of an enclosing package body: + + -- package body Pack is + -- Body_Variable : ... + -- package Nested + -- with Abstract_State => Body_State + -- is + -- Body_Nested_Variable : ... + -- end Nested; + -- end Pack; + + -- The same placement principle applies to package instantiations + + procedure Find_Placement_In_State_Space + (Item_Id : Entity_Id; + Placement : out State_Space_Kind; + Pack_Id : out Entity_Id); + -- Determine the state space placement of an item. Item_Id denotes the + -- entity of an abstract state, variable or package instantiation. + -- Placement captures the precise placement of the item in the enclosing + -- state space. If the state space is that of a package, Pack_Id denotes + -- its entity, otherwise Pack_Id is Empty. + function Find_Static_Alternative (N : Node_Id) return Node_Id; -- N is a case statement whose expression is a compile-time value. -- Determine the alternative chosen, so that the code of non-selected -- alternatives, and the warnings that may apply to them, are removed. - function Find_Body_Discriminal - (Spec_Discriminant : Entity_Id) return Entity_Id; - -- Given a discriminant of the record type that implements a task or - -- protected type, return the discriminal of the corresponding discriminant - -- of the actual concurrent type. - function First_Actual (Node : Node_Id) return Node_Id; -- Node is an N_Function_Call or N_Procedure_Call_Statement node. The -- result returned is the first actual parameter in declaration order @@ -1006,14 +1090,11 @@ package Sem_Util is -- Returns True if N is a call to a CPP constructor function Is_Child_Or_Sibling - (Pack_1 : Entity_Id; - Pack_2 : Entity_Id; - Private_Child : Boolean) return Boolean; + (Pack_1 : Entity_Id; + Pack_2 : Entity_Id) return Boolean; -- Determine the following relations between two arbitrary packages: -- 1) One package is the parent of a child package -- 2) Both packages are siblings and share a common parent - -- If flag Private_Child is set, then the child in case 1) or both siblings - -- in case 2) must be private. function Is_Concurrent_Interface (T : Entity_Id) return Boolean; -- First determine whether type T is an interface and then check whether @@ -1540,6 +1621,12 @@ package Sem_Util is -- This is used as a defense mechanism against ill-formed trees caused by -- previous errors (particularly in -gnatq mode). + function Requires_State_Refinement + (Spec_Id : Entity_Id; + Body_Id : Entity_Id) return Boolean; + -- Determine whether a package denoted by its spec and body entities + -- requires refinement of abstract states. + function Requires_Transient_Scope (Id : Entity_Id) return Boolean; -- Id is a type entity. The result is True when temporaries of this type -- need to be wrapped in a transient scope to be reclaimed properly when a diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 61c7da4c7c46..8bd23356e2d0 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -7283,6 +7283,7 @@ package Sinfo is -- Global -- Initial_Condition -- Initializes + -- Part_Of -- Refined_Depends -- Refined_Global -- Refined_States diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index a018dc9aaa0a..2cf58f558ad0 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -565,6 +565,7 @@ package Snames is Name_Ordered : constant Name_Id := N + $; -- GNAT Name_Pack : constant Name_Id := N + $; Name_Page : constant Name_Id := N + $; + Name_Part_Of : constant Name_Id := N + $; -- GNAT Name_Passive : constant Name_Id := N + $; -- GNAT Name_Post : constant Name_Id := N + $; -- GNAT Name_Postcondition : constant Name_Id := N + $; -- GNAT @@ -761,7 +762,6 @@ package Snames is Name_Optional : constant Name_Id := N + $; Name_Policy : constant Name_Id := N + $; Name_Parameter_Types : constant Name_Id := N + $; - Name_Part_Of : constant Name_Id := N + $; Name_Proof_In : constant Name_Id := N + $; Name_Reason : constant Name_Id := N + $; Name_Reference : constant Name_Id := N + $; @@ -1870,6 +1870,7 @@ package Snames is Pragma_Ordered, Pragma_Pack, Pragma_Page, + Pragma_Part_Of, Pragma_Passive, Pragma_Post, Pragma_Postcondition,