From: charlet Date: Sun, 13 Oct 2013 16:31:00 +0000 (+0000) Subject: 2013-10-13 Hristian Kirtchev X-Git-Tag: upstream/4.9.2~3723 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=28ff117fcc4265431367a02b6c28a7312cbbeb3e;p=platform%2Fupstream%2Flinaro-gcc.git 2013-10-13 Hristian Kirtchev * einfo.adb: Add node/list usage for Refined_State and Refinement_Constituents. (Get_Pragma): Update the initialization of Is_CDG to include Refined_Global and Refined_Depends. Rename constant Delayed to In_Contract and update all of its occurrences. (Is_Non_Volatile_State): New routine. (Is_Volatile_State): Removed. (Refined_State): New routine. (Refinement_Constituents): New routine. (Set_Refined_State): New routine. (Set_Refinement_Constituents): New routine. (Write_Field8_Name): Add output for Refinement_Constituents. (Write_Field10_Name): Add output for Refined_State. * einfo.ads: Add new synthesized attribute Is_Non_Volatile_State. Remove synthesized attribute Is_Volatile_State. Add new attributes Refined_State and Refinement_Constituents along with usage in nodes. (Get_Pragma): Update the comment on usage. (Is_Non_Volatile_State): New routine. (Is_Volatile_State): Removed. (Refined_State): New routine and pragma Inline. (Refinement_Constituents): New routine and pragma Inline. (Set_Refined_State): New routine and pragma Inline. (Set_Refinement_Constituents): New routine and pragma Inline. * elists.ads, elists.adb (Clone): Removed. (New_Copy_Elist): New routine. (Remove): New routine. * sem_ch3.adb (Analyze_Declarations): Use Defining_Entity to get the entity of the subprogram [body]. (Analyze_Object_Declaration): Add initialization for Refined_State. * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing for Refined_Global and Refined_Depends. Emit an error when the body requires Refined_Global, but the aspect/pragma is not present. * sem_ch6.ads (Analyze_Subprogram_Body_Contract): Change procedure signature and add comment on usage. * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing for aspect Refined_Global. * sem_prag.adb (Analyze_Abstract_State): Add initialization of attributes Refined_State and Refinement_Constituents. (Analyze_Depends_In_Decl_Part, Analyze_Global_In_Decl_Part, Analyze_Contract_Cases_In_Decl_Part): Remove local constant Arg1. (Analyze_Pragma): Add processing for pragma Refined_Global. The analysis of Refined_Post and Refined_Pre has been merged. Update an error message in the processing of pragma Refined_State. (Analyze_Refined_Global_In_Decl_Part): Provide implementation. (Analyze_Refined_Pragma): New routine. (Analyze_Refined_Pre_Post_Condition): Removed. (Analyze_Refined_State_In_Decl_Part): Update the call to Clone. (Analyze_Refinement_Clause): Make State_Id visible to all nested subprogram. (Check_Matching_Constituent): Establish a relation between a refined state and its constituent. (Collect_Hidden_States_In_Decls): Remove ??? comment. Look at the entity of the object declaration to establish its kind. * sem_util.adb: Alphabetize with and use clauses. (Contains_Refined_State): New routine. * sem_util.ads (Contains_Refined_State): New routine. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@203504 138bc75d-0d04-0410-961f-82ee72b054a4 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6afa902..65093fa 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,68 @@ +2013-10-13 Hristian Kirtchev + + * einfo.adb: Add node/list usage for Refined_State + and Refinement_Constituents. + (Get_Pragma): Update the + initialization of Is_CDG to include Refined_Global and + Refined_Depends. Rename constant Delayed to In_Contract and update + all of its occurrences. + (Is_Non_Volatile_State): New routine. + (Is_Volatile_State): Removed. + (Refined_State): New routine. + (Refinement_Constituents): New routine. + (Set_Refined_State): New routine. + (Set_Refinement_Constituents): New routine. + (Write_Field8_Name): Add output for Refinement_Constituents. + (Write_Field10_Name): Add output for Refined_State. + * einfo.ads: Add new synthesized attribute Is_Non_Volatile_State. + Remove synthesized attribute Is_Volatile_State. Add new + attributes Refined_State and Refinement_Constituents along with + usage in nodes. + (Get_Pragma): Update the comment on usage. + (Is_Non_Volatile_State): New routine. + (Is_Volatile_State): Removed. + (Refined_State): New routine and pragma Inline. + (Refinement_Constituents): New routine and pragma Inline. + (Set_Refined_State): New routine and pragma Inline. + (Set_Refinement_Constituents): New routine and pragma Inline. + * elists.ads, elists.adb (Clone): Removed. + (New_Copy_Elist): New routine. + (Remove): New routine. + * sem_ch3.adb (Analyze_Declarations): Use Defining_Entity + to get the entity of the subprogram [body]. + (Analyze_Object_Declaration): Add initialization for + Refined_State. + * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing + for Refined_Global and Refined_Depends. Emit an error when + the body requires Refined_Global, but the aspect/pragma is + not present. + * sem_ch6.ads (Analyze_Subprogram_Body_Contract): Change + procedure signature and add comment on usage. + * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing + for aspect Refined_Global. + * sem_prag.adb (Analyze_Abstract_State): Add initialization + of attributes Refined_State and Refinement_Constituents. + (Analyze_Depends_In_Decl_Part, Analyze_Global_In_Decl_Part, + Analyze_Contract_Cases_In_Decl_Part): Remove local + constant Arg1. + (Analyze_Pragma): Add processing for pragma + Refined_Global. The analysis of Refined_Post and Refined_Pre + has been merged. Update an error message in the processing of + pragma Refined_State. + (Analyze_Refined_Global_In_Decl_Part): Provide implementation. + (Analyze_Refined_Pragma): New routine. + (Analyze_Refined_Pre_Post_Condition): Removed. + (Analyze_Refined_State_In_Decl_Part): Update the call to Clone. + (Analyze_Refinement_Clause): Make State_Id visible to all + nested subprogram. + (Check_Matching_Constituent): Establish + a relation between a refined state and its constituent. + (Collect_Hidden_States_In_Decls): Remove ??? comment. Look at + the entity of the object declaration to establish its kind. + * sem_util.adb: Alphabetize with and use clauses. + (Contains_Refined_State): New routine. + * sem_util.ads (Contains_Refined_State): New routine. + 2013-10-13 Thomas Quinot * scos.ads: Minor documentation clarification. diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 5d4da12..e9c262a 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -81,6 +81,7 @@ package body Einfo is -- Normalized_First_Bit Uint8 -- Postcondition_Proc Node8 -- Refined_State_Pragma Node8 + -- Refinement_Constituents Elist8 -- Return_Applies_To Node8 -- First_Exit_Statement Node8 @@ -93,6 +94,7 @@ package body Einfo is -- 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 @@ -2648,12 +2650,24 @@ 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 Refined_State_Pragma (Id : E) return N is begin pragma Assert (Ekind (Id) = E_Package_Body); return Node8 (Id); end Refined_State_Pragma; + function Refinement_Constituents (Id : E) return L is + begin + pragma Assert (Ekind (Id) = E_Abstract_State); + return Elist8 (Id); + end Refinement_Constituents; + function Register_Exception_Call (Id : E) return N is begin pragma Assert (Ekind (Id) = E_Exception); @@ -5308,12 +5322,24 @@ 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_Refined_State_Pragma (Id : E; V : N) is begin pragma Assert (Ekind (Id) = E_Package_Body); Set_Node8 (Id, V); end Set_Refined_State_Pragma; + procedure Set_Refinement_Constituents (Id : E; V : L) is + begin + pragma Assert (Ekind (Id) = E_Abstract_State); + Set_Elist8 (Id, V); + end Set_Refinement_Constituents; + procedure Set_Register_Exception_Call (Id : E; V : N) is begin pragma Assert (Ekind (Id) = E_Exception); @@ -6266,21 +6292,26 @@ package body Einfo is ---------------- function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is - Is_CDG : constant Boolean := - Id = Pragma_Depends or else Id = Pragma_Global; - Is_CTC : constant Boolean := - Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case; - Is_PPC : constant Boolean := - Id = Pragma_Precondition or else Id = Pragma_Postcondition; - Delayed : constant Boolean := Is_CDG or Is_CTC or Is_PPC; - Item : Node_Id; - Items : Node_Id; - - begin - -- Handle delayed pragmas that appear in N_Contract nodes. Those have to - -- be extracted from their specialized list. - - if Delayed then + Is_CDG : constant Boolean := + Id = Pragma_Depends + or else Id = Pragma_Global + or else Id = Pragma_Refined_Depends + or else Id = Pragma_Refined_Global; + Is_CTC : constant Boolean := + Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case; + Is_PPC : constant Boolean := + Id = Pragma_Precondition + or else Id = Pragma_Postcondition; + In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC; + + Item : Node_Id; + Items : Node_Id; + + begin + -- Handle pragmas that appear in N_Contract nodes. Those have to be + -- extracted from their specialized list. + + if In_Contract then Items := Contract (E); if No (Items) then @@ -6310,7 +6341,7 @@ package body Einfo is -- All nodes in N_Contract are chained using Next_Pragma - elsif Delayed then + elsif In_Contract then Item := Next_Pragma (Item); -- Regular pragmas @@ -6712,6 +6743,17 @@ package body Einfo is and then Has_Option (Id, Name_Input_Only); end Is_Input_Only_State; + --------------------------- + -- Is_Non_Volatile_State -- + --------------------------- + + function Is_Non_Volatile_State (Id : E) return B is + begin + return + Ekind (Id) = E_Abstract_State + and then Has_Option (Id, Name_Non_Volatile); + end Is_Non_Volatile_State; + ------------------- -- Is_Null_State -- ------------------- @@ -6872,17 +6914,6 @@ package body Einfo is and then Is_Task_Type (Corresponding_Concurrent_Type (Id)); end Is_Task_Record_Type; - ----------------------- - -- Is_Volatile_State -- - ----------------------- - - function Is_Volatile_State (Id : E) return B is - begin - return - Ekind (Id) = E_Abstract_State - and then Has_Option (Id, Name_Volatile); - end Is_Volatile_State; - ------------------------ -- Is_Wrapper_Package -- ------------------------ @@ -8309,6 +8340,9 @@ package body Einfo is when E_Package_Body => Write_Str ("Refined_State_Pragma"); + when E_Abstract_State => + Write_Str ("Refinement_Constituents"); + when E_Return_Statement => Write_Str ("Return_Applies_To"); @@ -8358,7 +8392,7 @@ package body Einfo is Concurrent_Kind => Write_Str ("Direct_Primitive_Operations"); - when Float_Kind => + when Float_Kind => Write_Str ("Float_Rep"); when E_In_Parameter | @@ -8375,6 +8409,10 @@ 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 1b4c381..fce0689 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -2576,6 +2576,10 @@ package Einfo is -- set right, at which point, these comments can be removed, and the -- tests for static subtypes greatly simplified. +-- Is_Non_Volatile_State (synthesized) +-- Applies to all entities, true for abstract states that are subject to +-- option Non_Volatile. + -- Is_Null_Init_Proc (Flag178) -- Defined in procedure entities. Set for generated init proc procedures -- (used to initialize composite types), if the code for the procedure @@ -2977,10 +2981,6 @@ package Einfo is -- optimizations on volatile objects should test Treat_As_Volatile -- rather than testing this flag. --- Is_Volatile_State (synthesized) --- Applies to all entities, true for abstract states that are subject to --- option Volatile. - -- Is_Wrapper_Package (synthesized) -- Defined in package entities. Indicates that the package has been -- created as a wrapper for a subprogram instantiation. @@ -3537,10 +3537,19 @@ 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. + -- Refined_State_Pragma (Node8) -- Defined in [generic] package bodies. Contains the pragma that refines -- all abstract states defined in the corresponding package declaration. +-- 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 +-- the constituent_list of aspect/pragma Refined_State. + -- Register_Exception_Call (Node20) -- Defined in exception entities. When an exception is declared, -- a call is expanded to Register_Exception. This field points to @@ -5096,11 +5105,13 @@ package Einfo is ------------------------------------------ -- E_Abstract_State + -- Refinement_Constituents (Elist8) + -- Refined_State (Node10) -- Is_External_State (synth) -- Is_Input_Only_State (synth) -- Is_Null_State (synth) -- Is_Output_Only_State (synth) - -- Is_Volatile_State (synth) + -- Is_Non_Volatile_State (synth) -- E_Access_Protected_Subprogram_Type -- Equivalent_Type (Node18) @@ -5913,6 +5924,7 @@ package Einfo is -- E_Variable -- Hiding_Loop_Variable (Node8) -- Current_Value (Node9) + -- Refined_State (Node10) -- Esize (Uint12) -- Extra_Accessibility (Node13) -- Alignment (Uint14) @@ -6540,7 +6552,9 @@ 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 Refined_State_Pragma (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; function Related_Expression (Id : E) return N; @@ -6691,6 +6705,7 @@ package Einfo is function Is_Ghost_Entity (Id : E) return B; function Is_Ghost_Subprogram (Id : E) return B; function Is_Input_Only_State (Id : E) return B; + function Is_Non_Volatile_State (Id : E) return B; function Is_Null_State (Id : E) return B; function Is_Output_Only_State (Id : E) return B; function Is_Package_Or_Generic_Package (Id : E) return B; @@ -6703,7 +6718,6 @@ package Einfo is function Is_Synchronized_Interface (Id : E) return B; function Is_Task_Interface (Id : E) return B; function Is_Task_Record_Type (Id : E) return B; - function Is_Volatile_State (Id : E) return B; function Is_Wrapper_Package (Id : E) return B; function Last_Formal (Id : E) return E; function Machine_Emax_Value (Id : E) return U; @@ -7158,7 +7172,9 @@ 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_Refined_State_Pragma (Id : E; V : N); + 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); procedure Set_Related_Expression (Id : E; V : N); @@ -7403,11 +7419,17 @@ package Einfo is -- Empty is returned. function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id; - -- Searches the Rep_Item chain for a given entity E, for an instance of - -- a pragma with the given pragma Id. If found, the value returned is the - -- N_Pragma node, otherwise Empty is returned. Delayed pragmas such as - -- Precondition, Postcondition, Contract_Cases, Depends and Global appear - -- in the N_Contract node of entity E and are also handled by this routine. + -- Searches the Rep_Item chain of entity E, for an instance of a pragma + -- with the given pragma Id. If found, the value returned is the N_Pragma + -- node, otherwise Empty is returned. The following contract pragmas that + -- appear in N_Contract nodes are also handled by this routine: + -- Contract_Cases + -- Depends + -- Global + -- Precondition + -- Postcondition + -- Refined_Depends + -- Refined_Global function Get_Record_Representation_Clause (E : Entity_Id) return Node_Id; -- Searches the Rep_Item chain for a given entity E, for a record @@ -7908,7 +7930,9 @@ package Einfo is pragma Inline (Referenced); pragma Inline (Referenced_As_LHS); pragma Inline (Referenced_As_Out_Parameter); + pragma Inline (Refined_State); pragma Inline (Refined_State_Pragma); + pragma Inline (Refinement_Constituents); pragma Inline (Register_Exception_Call); pragma Inline (Related_Array_Object); pragma Inline (Related_Expression); @@ -8324,7 +8348,9 @@ 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_Refined_State_Pragma); + pragma Inline (Set_Refinement_Constituents); pragma Inline (Set_Register_Exception_Call); pragma Inline (Set_Related_Array_Object); pragma Inline (Set_Related_Expression); diff --git a/gcc/ada/elists.adb b/gcc/ada/elists.adb index a840d95..7e62ce4 100644 --- a/gcc/ada/elists.adb +++ b/gcc/ada/elists.adb @@ -158,34 +158,6 @@ package body Elists is end loop; end Append_Unique_Elmt; - ----------- - -- Clone -- - ------------ - - function Clone (List : Elist_Id) return Elist_Id is - Result : Elist_Id; - Elmt : Elmt_Id; - - begin - if List = No_Elist then - return No_Elist; - - -- Replicate the contents of the input list while preserving the - -- original order. - - else - Result := New_Elmt_List; - - Elmt := First_Elmt (List); - while Present (Elmt) loop - Append_Elmt (Node (Elmt), Result); - Next_Elmt (Elmt); - end loop; - - return Result; - end if; - end Clone; - -------------- -- Contains -- -------------- @@ -315,6 +287,34 @@ package body Elists is Elmts.Release; end Lock; + -------------------- + -- New_Copy_Elist -- + -------------------- + + function New_Copy_Elist (List : Elist_Id) return Elist_Id is + Result : Elist_Id; + Elmt : Elmt_Id; + + begin + if List = No_Elist then + return No_Elist; + + -- Replicate the contents of the input list while preserving the + -- original order. + + else + Result := New_Elmt_List; + + Elmt := First_Elmt (List); + while Present (Elmt) loop + Append_Elmt (Node (Elmt), Result); + Next_Elmt (Elmt); + end loop; + + return Result; + end if; + end New_Copy_Elist; + ------------------- -- New_Elmt_List -- ------------------- @@ -425,6 +425,27 @@ package body Elists is return Elmt /= No_Elmt; end Present; + ------------ + -- Remove -- + ------------ + + procedure Remove (List : Elist_Id; N : Node_Or_Entity_Id) is + Elmt : Elmt_Id; + + begin + if Present (List) then + Elmt := First_Elmt (List); + while Present (Elmt) loop + if Node (Elmt) = N then + Remove_Elmt (List, Elmt); + exit; + end if; + + Next_Elmt (Elmt); + end loop; + end if; + end Remove; + ----------------- -- Remove_Elmt -- ----------------- diff --git a/gcc/ada/elists.ads b/gcc/ada/elists.ads index d2eb745..f033136 100644 --- a/gcc/ada/elists.ads +++ b/gcc/ada/elists.ads @@ -137,12 +137,20 @@ package Elists is -- Add a new element (N) right after the pre-existing element Elmt -- It is invalid to call this subprogram with Elmt = No_Elmt. + function New_Copy_Elist (List : Elist_Id) return Elist_Id; + -- Replicate the contents of a list. Internal list nodes are not shared and + -- order of elements is preserved. + procedure Replace_Elmt (Elmt : Elmt_Id; New_Node : Node_Or_Entity_Id); pragma Inline (Replace_Elmt); -- Causes the given element of the list to refer to New_Node, the node -- which was previously referred to by Elmt is effectively removed from -- the list and replaced by New_Node. + procedure Remove (List : Elist_Id; N : Node_Or_Entity_Id); + -- Remove a node or an entity from a list. If the list does not contain the + -- item in question, the routine has no effect. + procedure Remove_Elmt (List : Elist_Id; Elmt : Elmt_Id); -- Removes Elmt from the given list. The node itself is not affected, -- but the space used by the list element may be (but is not required @@ -153,10 +161,6 @@ package Elists is -- affected, but the space used by the list element may be (but is not -- required to be) freed for reuse in a subsequent Append_Elmt call. - function Clone (List : Elist_Id) return Elist_Id; - -- Create a copy of the input list. Internal list nodes are not shared and - -- order of elements is preserved. - function Contains (List : Elist_Id; N : Node_Or_Entity_Id) return Boolean; -- Perform a sequential search to determine whether the given list contains -- a node or an entity. diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index b059b13..71cc77e 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1977,10 +1977,21 @@ package body Sem_Ch13 is -- Refined_Global - -- ??? To be implemented + -- Aspect Refined_Global must be delayed because it can mention + -- state refinements introduced by aspect Refined_State. Since + -- Refined_State is already delayed due to forward references, + -- so is Refined_Global. when Aspect_Refined_Global => - null; + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Refined_Global); + + Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem); + Insert_Delayed_Pragma (Aitem); + goto Continue; -- Refined_Post diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 77805d1..85872e1 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2233,12 +2233,10 @@ package body Sem_Ch3 is Decl := First (L); while Present (Decl) loop if Nkind (Decl) = N_Subprogram_Body then - Analyze_Subprogram_Body_Contract - (Defining_Unit_Name (Specification (Decl))); + Analyze_Subprogram_Body_Contract (Defining_Entity (Decl)); elsif Nkind (Decl) = N_Subprogram_Declaration then - Analyze_Subprogram_Contract - (Defining_Unit_Name (Specification (Decl))); + Analyze_Subprogram_Contract (Defining_Entity (Decl)); end if; Next (Decl); @@ -3540,7 +3538,7 @@ package body Sem_Ch3 is if Constant_Present (N) then Set_Ekind (Id, E_Constant); - Set_Is_True_Constant (Id, True); + Set_Is_True_Constant (Id); else Set_Ekind (Id, E_Variable); @@ -3763,6 +3761,13 @@ package body Sem_Ch3 is end if; <> + -- Initialize the refined state of a variable here because this is a + -- common destination for legal and illegal object declarations. + + if Ekind (Id) = E_Variable then + Set_Refined_State (Id, Empty); + end if; + if Has_Aspects (N) then Analyze_Aspect_Specifications (N, Id); end if; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index f138aea..aee35fb 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1975,12 +1975,47 @@ package body Sem_Ch6 is -- Analyze_Subprogram_Body_Contract -- -------------------------------------- - -- ??? To be implemented + procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is + Body_Decl : constant Node_Id := Parent (Parent (Body_Id)); + Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); + Prag : Node_Id; + + Has_Refined_Global : Boolean := False; - procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id) is - pragma Unreferenced (Subp); begin - null; + -- When a subprogram body declaration is erroneous, its defining entity + -- is left unanalyzed. There is nothing left to do in this case because + -- the body lacks a contract. + + if not Analyzed (Body_Id) then + return; + end if; + + Prag := Classifications (Contract (Body_Id)); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Refined_Depends then + Analyze_Refined_Depends_In_Decl_Part (Prag); + + elsif Pragma_Name (Prag) = Name_Refined_Global then + Has_Refined_Global := True; + Analyze_Refined_Global_In_Decl_Part (Prag); + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- When the corresponding Global aspect/pragma references a state with + -- visible refinement, the body requires Refined_Global. + + if not Has_Refined_Global and then Present (Spec_Id) then + Prag := Get_Pragma (Spec_Id, Pragma_Global); + + if Present (Prag) and then Contains_Refined_State (Prag) then + Error_Msg_NE + ("body of subprogram & requires global refinement", + Body_Decl, Spec_Id); + end if; + end if; end Analyze_Subprogram_Body_Contract; ------------------------------------ diff --git a/gcc/ada/sem_ch6.ads b/gcc/ada/sem_ch6.ads index bc901cc..fc0c365 100644 --- a/gcc/ada/sem_ch6.ads +++ b/gcc/ada/sem_ch6.ads @@ -46,10 +46,10 @@ package Sem_Ch6 is procedure Analyze_Subprogram_Declaration (N : Node_Id); procedure Analyze_Subprogram_Body (N : Node_Id); - procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id); + procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id); -- Analyze all delayed aspects chained on the contract of subprogram body - -- Subp as if they appeared at the end of a declarative region. The aspects - -- in question are: + -- Body_Id as if they appeared at the end of a declarative region. The + -- aspects in question are: -- Refined_Depends -- Refined_Global diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index dc80904..4ef1867 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -401,7 +401,6 @@ package body Sem_Prag is -- Local variables - Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); All_Cases : Node_Id; CCase : Node_Id; Subp_Decl : Node_Id; @@ -417,7 +416,7 @@ package body Sem_Prag is Subp_Decl := Find_Related_Subprogram (N); Subp_Id := Defining_Unit_Name (Specification (Subp_Decl)); - All_Cases := Expression (Arg1); + All_Cases := Expression (First (Pragma_Argument_Associations (N))); -- Multiple contract cases appear in aggregate form @@ -460,8 +459,7 @@ package body Sem_Prag is ---------------------------------- procedure Analyze_Depends_In_Decl_Part (N : Node_Id) is - Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); - Loc : constant Source_Ptr := Sloc (N); + Loc : constant Source_Ptr := Sloc (N); All_Inputs_Seen : Elist_Id := No_Elist; -- A list containing the entities of all the inputs processed so far. @@ -1248,7 +1246,7 @@ package body Sem_Prag is Subp_Decl := Find_Related_Subprogram (N); Subp_Id := Defining_Unit_Name (Specification (Subp_Decl)); - Clause := Expression (Arg1); + Clause := Expression (First (Pragma_Argument_Associations (N))); -- Empty dependency list @@ -1348,8 +1346,6 @@ package body Sem_Prag is --------------------------------- procedure Analyze_Global_In_Decl_Part (N : Node_Id) is - Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); - 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. @@ -1680,7 +1676,7 @@ package body Sem_Prag is Next (Assoc); end loop; - -- Something went horribly wrong, we have a malformed tree + -- Invalid tree else raise Program_Error; @@ -1708,7 +1704,7 @@ package body Sem_Prag is Subp_Decl := Find_Related_Subprogram (N); Subp_Id := Defining_Unit_Name (Specification (Subp_Decl)); - List := Expression (Arg1); + List := Expression (First (Pragma_Argument_Associations (N))); -- There is nothing to be done for a null global list @@ -1781,9 +1777,15 @@ 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_Refined_Pre_Post_Condition; - -- Subsidiary routine to the analysis of pragmas Refined_Pre and - -- Refined_Post. + procedure Analyze_Refined_Pragma + (Spec_Id : out Entity_Id; + Body_Id : out Entity_Id; + Legal : out Boolean); + -- Subsidiary routine to the analysis of body pragmas Refined_Depends, + -- Refined_Global, Refined_Post and Refined_Pre. Check the placement and + -- related context of the pragma. Spec_Id is the entity of the related + -- subprogram. Body_Id is the entity of the subprogram body. Flag Legal + -- is set when the pragma is properly placed. procedure Check_Ada_83_Warning; -- Issues a warning message for the current pragma if operating in Ada @@ -2311,18 +2313,27 @@ package body Sem_Prag is end if; end Ada_2012_Pragma; - ---------------------------------------- - -- Analyze_Refined_Pre_Post_Condition -- - ---------------------------------------- + ---------------------------- + -- Analyze_Refined_Pragma -- + ---------------------------- - procedure Analyze_Refined_Pre_Post_Condition is + procedure Analyze_Refined_Pragma + (Spec_Id : out Entity_Id; + Body_Id : out Entity_Id; + Legal : out Boolean) + is Body_Decl : Node_Id := Parent (N); Pack_Spec : Node_Id; Spec_Decl : Node_Id; - Spec_Id : Entity_Id; Stmt : Node_Id; begin + -- Assume that the pragma is illegal + + Spec_Id := Empty; + Body_Id := Empty; + Legal := False; + GNAT_Pragma; Check_Arg_Count (1); Check_No_Identifiers; @@ -2385,6 +2396,8 @@ package body Sem_Prag is return; end if; + Body_Id := Defining_Entity (Body_Decl); + -- The body [stub] must not act as a spec, in other words it has to -- be paired with a corresponding spec. @@ -2421,10 +2434,10 @@ package body Sem_Prag is return; end if; - -- Analyze the boolean expression as a "spec expression" + -- If we get here, then the pragma is legal - Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id); - end Analyze_Refined_Pre_Post_Condition; + Legal := True; + end Analyze_Refined_Pragma; -------------------------- -- Check_Ada_83_Warning -- @@ -8492,10 +8505,12 @@ package body Sem_Prag is -- from the original state declaration. Decorate the entity. Id := Make_Defining_Identifier (Loc, New_External_Name (Name)); - Set_Comes_From_Source (Id, not Is_Null); - Set_Parent (Id, State); - Set_Ekind (Id, E_Abstract_State); - Set_Etype (Id, Standard_Void_Type); + Set_Comes_From_Source (Id, not Is_Null); + Set_Parent (Id, State); + Set_Ekind (Id, E_Abstract_State); + Set_Etype (Id, Standard_Void_Type); + Set_Refined_State (Id, Empty); + Set_Refinement_Constituents (Id, New_Elmt_List); -- Every non-null state must be nameable and resolvable the -- same way a constant is. @@ -11873,7 +11888,7 @@ package body Sem_Prag is -- Global -- ------------ - -- pragma Global (GLOBAL_SPECIFICATION) + -- pragma Global (GLOBAL_SPECIFICATION); -- GLOBAL_SPECIFICATION ::= -- null @@ -15939,31 +15954,59 @@ package body Sem_Prag is -- Refined_Global -- -------------------- - -- ??? To be implemented + -- pragma Refined_Global (GLOBAL_SPECIFICATION); + + -- GLOBAL_SPECIFICATION ::= + -- null + -- | GLOBAL_LIST + -- | MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST} - -- Would be better if these generated an error message saying that - -- the feature was not yet implemented ??? + -- MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST - when Pragma_Refined_Global => - null; + -- MODE_SELECTOR ::= Input | Output | In_Out | Contract_In + -- GLOBAL_LIST ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM}) + -- GLOBAL_ITEM ::= NAME - ------------------ - -- Refined_Post -- - ------------------ + when Pragma_Refined_Global => Refined_Global : declare + Body_Id : Entity_Id; + Legal : Boolean; + Spec_Id : Entity_Id; + + begin + Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal); + + -- Save the pragma in the contract of the subprogram body. The + -- remaining analysis is performed at the end of the enclosing + -- declarations. + + if Legal then + Add_Contract_Item (N, Body_Id); + end if; + end Refined_Global; + + ------------------------------ + -- Refined_Post/Refined_Pre -- + ------------------------------ -- pragma Refined_Post (boolean_EXPRESSION); + -- pragma Refined_Pre (boolean_EXPRESSION); - when Pragma_Refined_Post => - Analyze_Refined_Pre_Post_Condition; + when Pragma_Refined_Post | + Pragma_Refined_Pre => Refined_Pre_Post : + declare + Body_Id : Entity_Id; + Legal : Boolean; + Spec_Id : Entity_Id; - ----------------- - -- Refined_Pre -- - ----------------- + begin + Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal); - -- pragma Refined_Pre (boolean_EXPRESSION); + -- Analyze the boolean expression as a "spec expression" - when Pragma_Refined_Pre => - Analyze_Refined_Pre_Post_Condition; + if Legal then + Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id); + end if; + end Refined_Pre_Post; ------------------- -- Refined_State -- @@ -16009,8 +16052,9 @@ package body Sem_Prag is if No (Abstract_States (Spec_Id)) or else Has_Null_Abstract_State (Spec_Id) then - Error_Pragma - ("useless pragma %, package does not define abstract states"); + Error_Msg_NE + ("useless refinement, package & does not define abstract " + & "states", N, Spec_Id); return; end if; @@ -18534,12 +18578,874 @@ package body Sem_Prag is -- Analyze_Refined_Global_In_Decl_Part -- ----------------------------------------- - -- ??? To be implemented - procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id) is - pragma Unreferenced (N); + Global : Node_Id; + -- The corresponding Global aspect/pragma + + Has_In_State : Boolean := False; + Has_In_Out_State : Boolean := False; + Has_Out_State : Boolean := False; + -- These flags are set when the corresponding Global aspect/pragma has + -- a state of mode Input, In_Out and Output respectively with a visible + -- refinement. + + In_Constits : Elist_Id := No_Elist; + In_Out_Constits : Elist_Id := No_Elist; + Out_Constits : Elist_Id := No_Elist; + -- These lists contain the entities of all Input, In_Out and Output + -- constituents that appear in Refined_Global and participate in state + -- refinement. + + In_Items : Elist_Id := No_Elist; + In_Out_Items : Elist_Id := No_Elist; + Out_Items : Elist_Id := No_Elist; + -- These list contain the entities of all Input, In_Out and Output items + -- defined in the corresponding Global aspect. + + procedure Check_In_Out_States; + -- Determine whether the corresponding Global aspect/pragma mentions + -- In_Out states with visible refinement and if so, ensure that one of + -- the following completions apply to the constituents of the state: + -- 1) there is at least one constituent of mode In_Out + -- 2) there is at least one Input and one Output constituent + -- 3) not all constituents are present and one of them is of mode + -- Output. + -- This routine may remove elements from In_Constits, In_Out_Constits + -- and Out_Constits. + + procedure Check_Input_States; + -- Determine whether the corresponding Global aspect/pragma mentions + -- Input states with visible refinement and if so, ensure that at least + -- one of its constituents appears as an Input item in Refined_Global. + -- This routine may remove elements from In_Constits, In_Out_Constits + -- and Out_Constits. + + procedure Check_Output_States; + -- Determine whether the corresponding Global aspect/pragma mentions + -- Output states with visible refinement and if so, ensure that all of + -- its constituents appear as Output items in Refined_Global. This + -- routine may remove elements from In_Constits, In_Out_Constits and + -- Out_Constits. + + procedure Check_Refined_Global_List + (List : Node_Id; + Global_Mode : Name_Id := Name_Input); + -- Verify the legality of a single global list declaration. Global_Mode + -- denotes the current mode in effect. + + procedure Collect_Global_Items (Prag : Node_Id); + -- Collect the entities of all items of pragma Prag by populating lists + -- In_Items, In_Out_Items and Out_Items. The routine also sets flags + -- Has_In_State, Has_In_Out_State and Has_Out_State if there is a state + -- of a particular kind with visible refinement. + + function Present_Then_Remove + (List : Elist_Id; + Item : Entity_Id) return Boolean; + -- Search List for a particular entity Item. If Item has been found, + -- remove it from List. This routine is used to strip lists In_Constits, + -- In_Out_Constits and Out_Constits of valid constituents. + + procedure Report_Extra_Constituents; + -- Emit an error for each constituent found in lists In_Constits, + -- In_Out_Constits and Out_Constits. + + ------------------------- + -- Check_In_Out_States -- + ------------------------- + + procedure Check_In_Out_States is + procedure Check_Constituent_Usage (State_Id : Entity_Id); + -- Determine whether one of the following coverage scenarios is in + -- effect: + -- 1) there is at least one constituent of mode In_Out + -- 2) there is at least one Input and one Output constituent + -- 3) not all constituents are present and one of them is of mode + -- Output. + -- If this is not the case, emit an error. + + ----------------------------- + -- Check_Constituent_Usage -- + ----------------------------- + + procedure Check_Constituent_Usage (State_Id : Entity_Id) is + Constit_Elmt : Elmt_Id; + Constit_Id : Entity_Id; + Has_Missing : Boolean := False; + In_Out_Seen : Boolean := False; + In_Seen : Boolean := False; + Out_Seen : Boolean := False; + + begin + -- Process all the constituents of the state and note their modes + -- within the global refinement. + + Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id)); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); + + if Present_Then_Remove (In_Constits, Constit_Id) then + In_Seen := True; + + elsif Present_Then_Remove (In_Out_Constits, Constit_Id) then + In_Out_Seen := True; + + elsif Present_Then_Remove (Out_Constits, Constit_Id) then + Out_Seen := True; + + else + Has_Missing := True; + end if; + + Next_Elmt (Constit_Elmt); + end loop; + + -- A single In_Out constituent is a valid completion + + if In_Out_Seen then + null; + + -- A pair of one Input and one Output constituent is a valid + -- completion. + + elsif In_Seen and then Out_Seen then + null; + + -- A single Output constituent is a valid completion only when + -- some of the other constituents are missing. + + elsif Has_Missing and then Out_Seen then + null; + + else + Error_Msg_NE + ("global refinement of state & redefines the mode of its " + & "constituents", N, State_Id); + end if; + end Check_Constituent_Usage; + + -- Local variables + + Item_Elmt : Elmt_Id; + Item_Id : Entity_Id; + + -- Start of processing for Check_In_Out_States + + begin + -- Inspect the In_Out items of the corresponding Global aspect/pragma + -- looking for a state with a visible refinement. + + if Has_In_Out_State and then Present (In_Out_Items) then + Item_Elmt := First_Elmt (In_Out_Items); + while Present (Item_Elmt) loop + Item_Id := Node (Item_Elmt); + + -- Ensure that one of the three coverage variants is satisfied + + if Ekind (Item_Id) = E_Abstract_State + and then Present (Refinement_Constituents (Item_Id)) + then + Check_Constituent_Usage (Item_Id); + end if; + + Next_Elmt (Item_Elmt); + end loop; + end if; + end Check_In_Out_States; + + ------------------------ + -- Check_Input_States -- + ------------------------ + + procedure Check_Input_States is + procedure Check_Constituent_Usage (State_Id : Entity_Id); + -- Determine whether at least one constituent of state State_Id with + -- visible refinement is used and has mode Input. Ensure that the + -- remaining constituents do not have In_Out or Output modes. + + ----------------------------- + -- Check_Constituent_Usage -- + ----------------------------- + + procedure Check_Constituent_Usage (State_Id : Entity_Id) is + Constit_Elmt : Elmt_Id; + Constit_Id : Entity_Id; + In_Seen : Boolean := False; + + begin + Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id)); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); + + -- At least one of the constituents appears as an Input + + if Present_Then_Remove (In_Constits, Constit_Id) then + In_Seen := True; + + -- The constituent appears in the global refinement, but has + -- mode In_Out or Output. + + elsif Present_Then_Remove (In_Out_Constits, Constit_Id) + or else Present_Then_Remove (Out_Constits, Constit_Id) + then + Error_Msg_Name_1 := Chars (State_Id); + Error_Msg_NE + ("constituent & of state % must have mode Input in global " + & "refinement", N, Constit_Id); + end if; + + Next_Elmt (Constit_Elmt); + end loop; + + -- Not one of the constituents appeared as Input + + if not In_Seen then + Error_Msg_NE + ("global refinement of state & must include at least one " + & "constituent of mode Input", N, State_Id); + end if; + end Check_Constituent_Usage; + + -- Local variables + + Item_Elmt : Elmt_Id; + Item_Id : Entity_Id; + + -- Start of processing for Check_Input_States + + begin + -- Inspect the Input items of the corresponding Global aspect/pragma + -- looking for a state with a visible refinement. + + if Has_In_State and then Present (In_Items) then + Item_Elmt := First_Elmt (In_Items); + while Present (Item_Elmt) loop + Item_Id := Node (Item_Elmt); + + -- Ensure that at least one of the constituents is utilized and + -- is of mode Input. + + if Ekind (Item_Id) = E_Abstract_State + and then Present (Refinement_Constituents (Item_Id)) + then + Check_Constituent_Usage (Item_Id); + end if; + + Next_Elmt (Item_Elmt); + end loop; + end if; + end Check_Input_States; + + ------------------------- + -- Check_Output_States -- + ------------------------- + + procedure Check_Output_States is + procedure Check_Constituent_Usage (State_Id : Entity_Id); + -- Determine whether all constituents of state State_Id with visible + -- refinement are used and have mode Output. Emit an error if this is + -- not the case. + + ----------------------------- + -- Check_Constituent_Usage -- + ----------------------------- + + procedure Check_Constituent_Usage (State_Id : Entity_Id) is + Constit_Elmt : Elmt_Id; + Constit_Id : Entity_Id; + + begin + Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id)); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); + + if Present_Then_Remove (Out_Constits, Constit_Id) then + null; + + else + Remove (In_Constits, Constit_Id); + Remove (In_Out_Constits, Constit_Id); + + Error_Msg_Name_1 := Chars (State_Id); + Error_Msg_NE + ("constituent & of state % must have mode Output in " + & "global refinement", N, Constit_Id); + end if; + + Next_Elmt (Constit_Elmt); + end loop; + end Check_Constituent_Usage; + + -- Local variables + + Item_Elmt : Elmt_Id; + Item_Id : Entity_Id; + + -- Start of processing for Check_Output_States + + begin + -- Inspect the Output items of the corresponding Global aspect/pragma + -- looking for a state with a visible refinement. + + if Has_Out_State and then Present (Out_Items) then + Item_Elmt := First_Elmt (Out_Items); + while Present (Item_Elmt) loop + Item_Id := Node (Item_Elmt); + + -- Ensure that all of the constituents are utilized and they + -- have mode Output. + + if Ekind (Item_Id) = E_Abstract_State + and then Present (Refinement_Constituents (Item_Id)) + then + Check_Constituent_Usage (Item_Id); + end if; + + Next_Elmt (Item_Elmt); + end loop; + end if; + end Check_Output_States; + + ------------------------------- + -- Check_Refined_Global_List -- + ------------------------------- + + procedure Check_Refined_Global_List + (List : Node_Id; + Global_Mode : Name_Id := Name_Input) + is + procedure Check_Refined_Global_Item + (Item : Node_Id; + Global_Mode : Name_Id); + -- Verify the legality of a single global item declaration. Parameter + -- Global_Mode denotes the current mode in effect. + + ------------------------------- + -- Check_Refined_Global_Item -- + ------------------------------- + + procedure Check_Refined_Global_Item + (Item : Node_Id; + Global_Mode : Name_Id) + is + procedure Add_Constituent (Item_Id : Entity_Id); + -- Add a single constituent to one of the three constituent lists + -- depending on Global_Mode. + + procedure Check_Matching_Modes (Item_Id : Entity_Id); + -- Verify that the global modes of item Item_Id are the same in + -- both aspects/pragmas Global and Refined_Global. + + function Is_Part_Of + (State : Entity_Id; + Ancestor : Entity_Id) return Boolean; + -- 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. + + --------------------- + -- Add_Constituent -- + --------------------- + + procedure Add_Constituent (Item_Id : Entity_Id) is + begin + if Global_Mode = Name_Input then + Add_Item (Item_Id, In_Constits); + + elsif Global_Mode = Name_In_Out then + Add_Item (Item_Id, In_Out_Constits); + + elsif Global_Mode = Name_Output then + Add_Item (Item_Id, Out_Constits); + end if; + end Add_Constituent; + + -------------------------- + -- Check_Matching_Modes -- + -------------------------- + + procedure Check_Matching_Modes (Item_Id : Entity_Id) is + procedure Inconsistent_Mode_Error (Expect : Name_Id); + -- Issue a common error message for all mode mismatche. Expect + -- denotes the expected mode. + + ----------------------------- + -- Inconsistent_Mode_Error -- + ----------------------------- + + procedure Inconsistent_Mode_Error (Expect : Name_Id) is + begin + Error_Msg_NE + ("global item & has inconsistent modes", Item, Item_Id); + + Error_Msg_Name_1 := Global_Mode; + Error_Msg_N ("\ expected mode %", Item); + + Error_Msg_Name_1 := Expect; + Error_Msg_N ("\ found mode %", Item); + end Inconsistent_Mode_Error; + + -- Start processing for Check_Matching_Modes + + begin + if Contains (In_Items, Item_Id) then + if Global_Mode /= Name_Input then + Inconsistent_Mode_Error (Name_Input); + end if; + + elsif Contains (In_Out_Items, Item_Id) then + if Global_Mode /= Name_In_Out then + Inconsistent_Mode_Error (Name_In_Out); + end if; + + elsif Contains (Out_Items, Item_Id) then + if Global_Mode /= Name_Output then + Inconsistent_Mode_Error (Name_Output); + end if; + + -- The item does not appear in the corresponding Global aspect, + -- it must be an extra. + + else + Error_Msg_NE ("extra global item &", Item, Item_Id); + end if; + end Check_Matching_Modes; + + ---------------- + -- 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; + + -- Local variables + + Item_Id : constant Entity_Id := Entity_Of (Item); + + -- Start of processing for Check_Refined_Global_Item + + begin + -- State checks + + 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 Is_Part_Of (Item_Id, Refined_State (Item_Id)) then + Add_Constituent (Item_Id); + else + Error_Msg_Name_1 := Chars (Refined_State (Item_Id)); + Error_Msg_NE + ("state & is not a valid constituent of ancestor " + & "state %", Item, Item_Id); + end if; + + -- An abstract state with visible refinement cannot appear in a + -- global refinement as its place must be taken by some of its + -- constituents. + + elsif Present (Refinement_Constituents (Item_Id)) then + Error_Msg_NE + ("cannot mention state & in global refinement, use its " + & "constituents instead", Item, Item_Id); + + -- The state is not refined nor is it a constituent. Ensure + -- that the modes of both its occurrences in Global and + -- Refined_Global match. + + else + Check_Matching_Modes (Item_Id); + end if; + + -- Variable checks + + else pragma Assert (Ekind (Item_Id) = E_Variable); + + -- The 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 + Add_Constituent (Item_Id); + + -- The variable is not a constituent. Ensure that the modes of + -- both its occurrences in Global and Refined_Global match. + + else + Check_Matching_Modes (Item_Id); + end if; + end if; + end Check_Refined_Global_Item; + + -- Local variables + + Item : Node_Id; + + -- Start of processing for Check_Refined_Global_List + + begin + -- Single global item declaration + + if Nkind_In (List, N_Expanded_Name, + N_Identifier, + N_Selected_Component) + then + Check_Refined_Global_Item (List, Global_Mode); + + -- Simple global list or moded global list declaration + + elsif Nkind (List) = N_Aggregate then + + -- The declaration of a simple global list appear as a collection + -- of expressions. + + if Present (Expressions (List)) then + Item := First (Expressions (List)); + while Present (Item) loop + Check_Refined_Global_Item (Item, Global_Mode); + + Next (Item); + end loop; + + -- The declaration of a moded global list appears as a collection + -- of component associations where individual choices denote + -- modes. + + elsif Present (Component_Associations (List)) then + Item := First (Component_Associations (List)); + while Present (Item) loop + Check_Refined_Global_List + (List => Expression (Item), + Global_Mode => Chars (First (Choices (Item)))); + + Next (Item); + end loop; + + -- Invalid tree + + else + raise Program_Error; + end if; + + -- Invalid list + + else + raise Program_Error; + end if; + end Check_Refined_Global_List; + + -------------------------- + -- Collect_Global_Items -- + -------------------------- + + procedure Collect_Global_Items (Prag : Node_Id) is + procedure Process_Global_List + (List : Node_Id; + Mode : Name_Id := Name_Input); + -- Collect all items housed in a global list. Formal Mode denotes the + -- current mode in effect. + + ------------------------- + -- Process_Global_List -- + ------------------------- + + procedure Process_Global_List + (List : Node_Id; + Mode : Name_Id := Name_Input) + is + procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id); + -- Add a single item to the appropriate list. Formal Mode denotes + -- the current mode in effect. + + ------------------------- + -- Process_Global_Item -- + ------------------------- + + procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id) is + Item_Id : constant Entity_Id := Entity_Of (Item); + + begin + -- Signal that the global list contains at least one abstract + -- state with a visible refinement. + + if Ekind (Item_Id) = E_Abstract_State + and then Present (Refinement_Constituents (Item_Id)) + then + if Mode = Name_Input then + Has_In_State := True; + elsif Mode = Name_In_Out then + Has_In_Out_State := True; + elsif Mode = Name_Output then + Has_Out_State := True; + end if; + end if; + + -- Add the item to the proper list + + if Mode = Name_Input then + Add_Item (Item_Id, In_Items); + elsif Mode = Name_In_Out then + Add_Item (Item_Id, In_Out_Items); + elsif Mode = Name_Output then + Add_Item (Item_Id, Out_Items); + end if; + end Process_Global_Item; + + -- Local variables + + Item : Node_Id; + + -- Start of processing for Process_Global_List + + begin + -- Single global item declaration + + if Nkind_In (List, N_Expanded_Name, + N_Identifier, + N_Selected_Component) + then + Process_Global_Item (List, Mode); + + -- Single global list or moded global list declaration + + elsif Nkind (List) = N_Aggregate then + + -- The declaration of a simple global list appear as a + -- collection of expressions. + + if Present (Expressions (List)) then + Item := First (Expressions (List)); + while Present (Item) loop + Process_Global_Item (Item, Mode); + + Next (Item); + end loop; + + -- The declaration of a moded global list appears as a + -- collection of component associations where individual + -- choices denote modes. + + elsif Present (Component_Associations (List)) then + Item := First (Component_Associations (List)); + while Present (Item) loop + Process_Global_List + (List => Expression (Item), + Mode => Chars (First (Choices (Item)))); + + Next (Item); + end loop; + + -- Invalid tree + + else + raise Program_Error; + end if; + + -- Invalid list + + else + raise Program_Error; + end if; + end Process_Global_List; + + -- Local variables + + List : constant Node_Id := + Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag))); + + -- Start of processing for Collect_Global_Items + + begin + -- Do not process a null global list as it contains nothing + + if Nkind (List) /= N_Null then + Process_Global_List (List); + end if; + end Collect_Global_Items; + + ------------------------- + -- Present_Then_Remove -- + ------------------------- + + function Present_Then_Remove + (List : Elist_Id; + Item : Entity_Id) return Boolean + is + Elmt : Elmt_Id; + + begin + if Present (List) then + Elmt := First_Elmt (List); + while Present (Elmt) loop + if Node (Elmt) = Item then + Remove_Elmt (List, Elmt); + return True; + end if; + + Next_Elmt (Elmt); + end loop; + end if; + + return False; + end Present_Then_Remove; + + ------------------------------- + -- Report_Extra_Constituents -- + ------------------------------- + + procedure Report_Extra_Constituents is + procedure Report_Extra_Constituents_In_List (List : Elist_Id); + -- Emit an error for every element of List + + --------------------------------------- + -- Report_Extra_Constituents_In_List -- + --------------------------------------- + + procedure Report_Extra_Constituents_In_List (List : Elist_Id) is + Constit_Elmt : Elmt_Id; + + begin + if Present (List) then + Constit_Elmt := First_Elmt (List); + while Present (Constit_Elmt) loop + Error_Msg_NE ("extra constituent &", N, Node (Constit_Elmt)); + Next_Elmt (Constit_Elmt); + end loop; + end if; + end Report_Extra_Constituents_In_List; + + -- Start of processing for Report_Extra_Constituents + + begin + Report_Extra_Constituents_In_List (In_Constits); + Report_Extra_Constituents_In_List (In_Out_Constits); + Report_Extra_Constituents_In_List (Out_Constits); + end Report_Extra_Constituents; + + -- Local variables + + Body_Decl : constant Node_Id := Parent (N); + Errors : constant Nat := Serious_Errors_Detected; + List : constant Node_Id := + Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); + + -- Start of processing for Analyze_Refined_Global_In_Decl_Part + begin - null; + Global := Get_Pragma (Spec_Id, Pragma_Global); + + -- The subprogram declaration lacks aspect/pragma Global. This renders + -- Refined_Global useless as there is nothing to refine. + + if No (Global) then + Error_Msg_NE + ("useless refinement, subprogram & lacks global items", N, Spec_Id); + return; + end if; + + -- Extract all relevant items from the corresponding Global aspect or + -- pragma. + + Collect_Global_Items (Global); + + -- The corresponding Global aspect/pragma must mention at least one + -- state with a visible refinement at the point Refined_Global is + -- processed. + + if not Has_In_State + and then not Has_In_Out_State + and then not Has_Out_State + then + Error_Msg_NE + ("useless refinement, subprogram & does not mention abstract state " + & "with visible refinement", N, Spec_Id); + return; + end if; + + -- The global refinement of inputs and outputs cannot be null when the + -- corresponding Global aspect/pragma contains at least one item. + + if Nkind (List) = N_Null + and then + (Present (In_Items) + or else Present (In_Out_Items) + or else Present (Out_Items)) + then + Error_Msg_NE + ("refinement cannot be null, subprogram & has global items", + N, Spec_Id); + return; + end if; + + -- Analyze Refined_Global as if it behaved as a regular aspect/pragma + -- Global. This ensures that the categorization of all refined global + -- items is consistent with their role. + + Analyze_Global_In_Decl_Part (N); + + -- Perform all refinement checks with respect to completeness and mode + -- matching. + + if Serious_Errors_Detected = Errors then + Check_Refined_Global_List (List); + end if; + + -- For Input states with visible refinement, at least one constituent + -- must be used as an Input in the global refinement. + + if Serious_Errors_Detected = Errors then + Check_Input_States; + end if; + + -- Verify all possible completion variants for In_Out states with + -- visible refinement. + + if Serious_Errors_Detected = Errors then + Check_In_Out_States; + end if; + + -- For Output states with visible refinement, all constituents must be + -- used as Outputs in the global refinement. + + if Serious_Errors_Detected = Errors then + Check_Output_States; + end if; + + -- Emit errors for all constituents that belong to other states with + -- visible refinement that do not appear in Global. + + if Serious_Errors_Detected = Errors then + Report_Extra_Constituents; + end if; end Analyze_Refined_Global_In_Decl_Part; ---------------------------------------- @@ -18587,6 +19493,9 @@ package body Sem_Prag is ------------------------------- procedure Analyze_Refinement_Clause (Clause : Node_Id) is + State_Id : Entity_Id := Empty; + -- The entity of the state being refined in the current clause + Non_Null_Seen : Boolean := False; Null_Seen : Boolean := False; -- Flags used to detect multiple uses of null in a single clause or a @@ -18647,6 +19556,17 @@ package body Sem_Prag is Add_Item (Constit_Id, Constituents_Seen); Remove_Elmt (Hidden_States, State_Elmt); + -- Establish a relation between the refined state and its + -- constituent. + + if No (Refinement_Constituents (State_Id)) then + Set_Refinement_Constituents (State_Id, New_Elmt_List); + end if; + + Append_Elmt + (Constit_Id, Refinement_Constituents (State_Id)); + Set_Refined_State (Constit_Id, State_Id); + return; end if; @@ -18771,9 +19691,8 @@ package body Sem_Prag is -- Local declarations - Constit : Node_Id; - State : Node_Id; - State_Id : Entity_Id := Empty; + Constit : Node_Id; + State : Node_Id; -- Start of processing for Analyze_Refinement_Clause @@ -18891,12 +19810,8 @@ package body Sem_Prag is -- Source objects (non-constants) are valid hidden states - -- This is a very odd test, it misses many cases, e.g. - -- renamings of objects, in-out parameters etc ???. Why - -- not test the Ekind ??? - if Nkind (Decl) = N_Object_Declaration - and then not Constant_Present (Decl) + and then Ekind (Defining_Entity (Decl)) = E_Variable and then Comes_From_Source (Decl) then Add_Item (Defining_Entity (Decl), Result); @@ -19004,7 +19919,7 @@ package body Sem_Prag is -- Initialize the various lists used during analysis - Abstr_States := Clone (Abstract_States (Spec_Id)); + Abstr_States := New_Copy_Elist (Abstract_States (Spec_Id)); Hidden_States := Collect_Hidden_States; -- Multiple state refinements appear as an aggregate diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 935b727..7a0341b 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -27,8 +27,8 @@ with Atree; use Atree; with Casing; use Casing; with Checks; use Checks; with Debug; use Debug; -with Errout; use Errout; with Elists; use Elists; +with Errout; use Errout; with Exp_Ch11; use Exp_Ch11; with Exp_Disp; use Exp_Disp; with Exp_Util; use Exp_Util; @@ -3157,6 +3157,127 @@ package body Sem_Util is end if; end Conditional_Delay; + ---------------------------- + -- Contains_Refined_State -- + ---------------------------- + + function Contains_Refined_State (Prag : Node_Id) return Boolean is + function Has_Refined_State (List : Node_Id) return Boolean; + -- Determine whether a global list mentions a state with a visible + -- refinement. + + ----------------------- + -- Has_Refined_State -- + ----------------------- + + function Has_Refined_State (List : Node_Id) return Boolean is + function Is_Refined_State (Item : Node_Id) return Boolean; + -- Determine whether Item is a reference to an abstract state with a + -- visible refinement. + + ---------------------- + -- Is_Refined_State -- + ---------------------- + + function Is_Refined_State (Item : Node_Id) return Boolean is + Item_Id : Entity_Id; + + begin + if Nkind (Item) = N_Null then + return False; + + else + Item_Id := Entity_Of (Item); + + return + Ekind (Item_Id) = E_Abstract_State + and then Present (Refinement_Constituents (Item_Id)); + end if; + end Is_Refined_State; + + -- Local variables + + Item : Node_Id; + + -- Start of processing for Has_Refined_State + + begin + -- A null global list does not mention any states + + if Nkind (List) = N_Null then + return False; + + -- Single global item declaration + + elsif Nkind_In (List, N_Expanded_Name, + N_Identifier, + N_Selected_Component) + then + return Is_Refined_State (List); + + -- Simple global list or moded global list declaration + + elsif Nkind (List) = N_Aggregate then + + -- The declaration of a simple global list appear as a collection + -- of expressions. + + if Present (Expressions (List)) then + Item := First (Expressions (List)); + while Present (Item) loop + if Is_Refined_State (Item) then + return True; + end if; + + Next (Item); + end loop; + + -- The declaration of a moded global list appears as a collection + -- of component associations where individual choices denote + -- modes. + + else + Item := First (Component_Associations (List)); + while Present (Item) loop + if Has_Refined_State (Expression (Item)) then + return True; + end if; + + Next (Item); + end loop; + end if; + + -- If we get here, then the simple/moded global list did not + -- mention any states with a visible refinement. + + return False; + + -- Something went horribly wrong, we have a malformed tree + + else + raise Program_Error; + end if; + end Has_Refined_State; + + -- Local variables + + Arg : constant Node_Id := + Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag))); + Nam : constant Name_Id := Pragma_Name (Prag); + + -- Start of processing for Contains_Refined_State + + begin + -- ??? To be implemented + + if Nam = Name_Depends then + return False; + + else pragma Assert (Nam = Name_Global); + return Has_Refined_State (Arg); + end if; + end Contains_Refined_State; + ------------------------- -- Copy_Component_List -- ------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index d8d7db1..621cb01 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -326,6 +326,13 @@ package Sem_Util is -- Sets the Has_Delayed_Freeze flag of New if the Delayed_Freeze flag of -- Old is set and Old has no yet been Frozen (i.e. Is_Frozen is false). + function Contains_Refined_State (Prag : Node_Id) return Boolean; + -- Determine whether pragma Prag contains a reference to the entity of an + -- abstract state with a visible refinement. Prag must denote one of the + -- following pragmas: + -- Depends + -- Global + function Copy_Parameter_List (Subp_Id : Entity_Id) return List_Id; -- Utility to create a parameter profile for a new subprogram spec, when -- the subprogram has a body that acts as spec. This is done for some cases