From: Arnaud Charlet Date: Thu, 20 Nov 2014 11:55:37 +0000 (+0100) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c5e108f9bc25c1a4043e402d6c9adf6d9405e31;p=gcc.git [multiple changes] 2014-11-20 Ed Schonberg * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Do not apply inlining expansion if function build in place, i.e. has a limited return type. 2014-11-20 Hristian Kirtchev * sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Add variables Body_Id, Body_Inputs, Body_Outputs, Spec_Inputs, Spec_Outputs. Synthesize the inputs and outputs of the subprogram when pragma [Refined_]Global is missing and perform legality checks on output states with visible refinement. (Appears_In): Update the comment on usage. (Check_Output_States): New routine. (Collect_Dependency_Clause): New routine. (Collect_Global_Items): Relocated to Analyze_Refined_Global_In_Decl_Part. (Collect_Subprogram_Inputs_Outputs): Add new formal parameters Synthesize and Depends_Seen. The routine can now synthesize inputs and outputs from pragma [Refined_]Depends. (Normalize_Clause): Update the comment on usage. The routine no longer performs normalization of outputs. (Normalize_Clauses): Normalize both inputs and outputs. (Normalize_Output): Relocated to Normalize_Clauses. * sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Add new formal parameters Synthesize and Depends_Seen and update the comment on usage. 2014-11-20 Ed Schonberg * sem_ch13.adb (Reset_Loop_Variable): New subsidiary procedure in Build_Predicate_Functions, to handle properly quantified expressions in dynamic predicates. From-SVN: r217850 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 83156e02012..f24e4fd26b9 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,44 @@ +2014-11-20 Ed Schonberg + + * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Do not apply + inlining expansion if function build in place, i.e. has a limited + return type. + +2014-11-20 Hristian Kirtchev + + * sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Add + variables Body_Id, Body_Inputs, Body_Outputs, Spec_Inputs, + Spec_Outputs. Synthesize the inputs and outputs of the subprogram + when pragma [Refined_]Global is missing and perform legality + checks on output states with visible refinement. + (Appears_In): Update the comment on usage. + (Check_Output_States): New routine. + (Collect_Dependency_Clause): New routine. + (Collect_Global_Items): Relocated to + Analyze_Refined_Global_In_Decl_Part. + (Collect_Subprogram_Inputs_Outputs): Add new formal parameters + Synthesize and Depends_Seen. The routine can now synthesize inputs + and outputs from pragma [Refined_]Depends. + (Normalize_Clause): Update the comment on usage. The routine no longer + performs normalization of outputs. + (Normalize_Clauses): Normalize both inputs and outputs. + (Normalize_Output): Relocated to Normalize_Clauses. + * sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Add new + formal parameters Synthesize and Depends_Seen and update the + comment on usage. + +2014-11-20 Vincent Celier + + PR ada/47500 + * back_end.adb (Scan_Back_End_Switches): Skip switch -G and + its argument. + +2014-11-20 Ed Schonberg + + * sem_ch13.adb (Reset_Loop_Variable): New subsidiary procedure + in Build_Predicate_Functions, to handle properly quantified + expressions in dynamic predicates. + 2014-11-20 Robert Dewar * gnatcmd.adb, sem_ch6.adb, exp_dist.adb: Minor reformatting. diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index d8f71c53d59..fe358b30b78 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -2853,6 +2853,7 @@ package body Sem_Ch13 is begin if A_Id = Aspect_Pre or else A_Id = Aspect_Precondition then Pname := Name_Precondition; + else Pname := Name_Postcondition; end if; @@ -2925,6 +2926,7 @@ package body Sem_Ch13 is -- with delay of visibility for the expression analysis. Insert_Pragma (Aitem); + goto Continue; end Pre_Post; @@ -3552,7 +3554,7 @@ package body Sem_Ch13 is -- the type of the formal match. if Base_Type (Typ) /= Base_Type (Ent) - or else Present ((Next_Formal (F))) + or else Present (Next_Formal (F)) then return False; @@ -3630,7 +3632,8 @@ package body Sem_Ch13 is Error_Msg_N ("stream subprogram must not be abstract", Expr); return; - -- Test for stream subprogram for interface type being non-null + -- A stream subprogram for an interface type must be a null + -- procedure (RM 13.13.2 (38/3)). elsif Is_Interface (U_Ent) and then not Inside_A_Generic @@ -8268,11 +8271,44 @@ package body Sem_Ch13 is if Raise_Expression_Present then declare - Map : constant Elist_Id := New_Elmt_List; + Map : constant Elist_Id := New_Elmt_List; + New_V : Entity_Id := Empty; + + -- The unanalyzed expression will be copied and appear in + -- both functions. Normally expressions do not declare new + -- entities, but quantified expressions do, so we need to + -- create new entities for their bound variables, to prevent + -- multiple definitions in gigi. + + function Reset_Loop_Variable (N : Node_Id) + return Traverse_Result; + + procedure Collect_Loop_Variables is + new Traverse_Proc (Reset_Loop_Variable); + + ------------------------ + -- Reset_Loop_Variable -- + ------------------------ + + function Reset_Loop_Variable (N : Node_Id) + return Traverse_Result + is + begin + if Nkind (N) = N_Iterator_Specification then + New_V := Make_Defining_Identifier + (Sloc (N), Chars (Defining_Identifier (N))); + + Set_Defining_Identifier (N, New_V); + end if; + + return OK; + end Reset_Loop_Variable; + begin Append_Elmt (Object_Entity, Map); Append_Elmt (Object_Entity_M, Map); Expr_M := New_Copy_Tree (Expr, Map => Map); + Collect_Loop_Variables (Expr_M); end; end if; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 8c6b0d2233c..d0c1f9e8972 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -3691,6 +3691,11 @@ package body Sem_Ch6 is if Comes_From_Source (Body_Id) and then Ekind (Spec_Id) = E_Function and then Returns_Unconstrained_Type (Spec_Id) + + -- If function builds in place, i.e. returns a limited type, + -- inlining cannot be done. + + and then not Is_Limited_Type (Etype (Spec_Id)) then Check_And_Split_Unconstrained_Function (N, Spec_Id, Body_Id); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 52853199a29..aed0d21cde1 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -178,9 +178,9 @@ package body Sem_Prag is -- casing is constructed. function Appears_In (List : Elist_Id; Item_Id : Entity_Id) return Boolean; - -- Subsidiary to the analysis of pragma Global and pragma Depends. Query - -- whether a particular item appears in a mixed list of nodes and entities. - -- It is assumed that all nodes in the list have entities. + -- Subsidiary to analysis of pragmas Depends, Global and Refined_Depends. + -- Query whether a particular item appears in a mixed list of nodes and + -- entities. It is assumed that all nodes in the list have entities. function Check_Kind (Nam : Name_Id) return Name_Id; -- This function is used in connection with pragmas Assert, Check, @@ -216,25 +216,6 @@ package body Sem_Prag is -- 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; - In_Out_Items : in out Elist_Id; - Out_Items : in out Elist_Id; - Proof_In_Items : in out Elist_Id; - Has_In_State : out Boolean; - Has_In_Out_State : out Boolean; - Has_Out_State : out Boolean; - Has_Proof_In_State : out Boolean; - Has_Null_State : out Boolean); - -- Subsidiary to the analysis of pragma Refined_Depends/Refined_Global. - -- Prag denotes pragma [Refined_]Global. Gather all input, in out, output - -- and Proof_In items of Prag in lists In_Items, In_Out_Items, Out_Items - -- and Proof_In_Items. Flags Has_In_State, Has_In_Out_State, Has_Out_State - -- and Has_Proof_In_State are set when there is at least one abstract state - -- with visible refinement available in the corresponding mode. Flag - -- Has_Null_State is set when at least state has a null refinement. - function Find_Related_Subprogram_Or_Body (Prag : Node_Id; Do_Checks : Boolean := False) return Node_Id; @@ -581,9 +562,7 @@ package body Sem_Prag is -- error if this is not the case. procedure Normalize_Clause (Clause : Node_Id); - -- Remove a self-dependency "+" from the input list of a clause. Split - -- a clause with multiple outputs into multiple clauses with a single - -- output. + -- Remove a self-dependency "+" from the input list of a clause ----------------------------- -- Add_Item_To_Name_Buffer -- @@ -1335,11 +1314,6 @@ package body Sem_Prag is -- Flag Multiple should be set when Output comes from a list with -- multiple items. - procedure Normalize_Outputs; - -- If Clause contains more than one output, split the clause into - -- multiple clauses with a single output. All new clauses are added - -- after Clause. - ----------------------------- -- Create_Or_Modify_Clause -- ----------------------------- @@ -1525,68 +1499,6 @@ package body Sem_Prag is end if; end Create_Or_Modify_Clause; - ----------------------- - -- Normalize_Outputs -- - ----------------------- - - procedure Normalize_Outputs is - Inputs : constant Node_Id := Expression (Clause); - Loc : constant Source_Ptr := Sloc (Clause); - Outputs : constant Node_Id := First (Choices (Clause)); - Last_Output : Node_Id; - New_Clause : Node_Id; - Next_Output : Node_Id; - Output : Node_Id; - - begin - -- Multiple outputs appear as an aggregate. Nothing to do when - -- the clause has exactly one output. - - if Nkind (Outputs) = N_Aggregate then - Last_Output := Last (Expressions (Outputs)); - - -- Create a clause for each output. Note that each time a new - -- clause is created, the original output list slowly shrinks - -- until there is one item left. - - Output := First (Expressions (Outputs)); - while Present (Output) loop - Next_Output := Next (Output); - - -- Unhook the output from the original output list as it - -- will be relocated to a new clause. - - Remove (Output); - - -- Special processing for the last output. At this point - -- the original aggregate has been stripped down to one - -- element. Replace the aggregate by the element itself. - - if Output = Last_Output then - Rewrite (Outputs, Output); - - else - -- Generate a clause of the form: - -- (Output => Inputs) - - New_Clause := - Make_Component_Association (Loc, - Choices => New_List (Output), - Expression => New_Copy_Tree (Inputs)); - - -- The new clause contains replicated content that has - -- already been analyzed. There is not need to reanalyze - -- them. - - Set_Analyzed (New_Clause); - Insert_After (Clause, New_Clause); - end if; - - Output := Next_Output; - end loop; - end if; - end Normalize_Outputs; - -- Local variables Outputs : constant Node_Id := First (Choices (Clause)); @@ -1641,11 +1553,6 @@ package body Sem_Prag is Multiple => False); end if; end if; - - -- Split a clause with multiple outputs into multiple clauses with a - -- single output. - - Normalize_Outputs; end Normalize_Clause; -- Local variables @@ -21856,6 +21763,11 @@ package body Sem_Prag is ------------------------------------------ procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id) is + Body_Inputs : Elist_Id := No_Elist; + Body_Outputs : Elist_Id := No_Elist; + -- The inputs and outputs of the subprogram body synthesized from pragma + -- Refined_Depends. + Dependencies : List_Id := No_List; Depends : Node_Id; -- The corresponding Depends pragma along with its clauses @@ -21870,11 +21782,21 @@ package body Sem_Prag is Spec_Id : Entity_Id; -- The entity of the subprogram subject to pragma Refined_Depends + Spec_Inputs : Elist_Id := No_Elist; + Spec_Outputs : Elist_Id := No_Elist; + -- The inputs and outputs of the subprogram spec synthesized from pragma + -- Depends. + procedure Check_Dependency_Clause (Dep_Clause : Node_Id); -- Try to match a single dependency clause Dep_Clause against one or -- more refinement clauses found in list Refinements. Each successful -- match eliminates at least one refinement clause from Refinements. + procedure Check_Output_States; + -- Determine whether pragma Depends contains an output state with a + -- visible refinement and if so, ensure that pragma Refined_Depends + -- mentions all its constituents as outputs. + procedure Normalize_Clauses (Clauses : List_Id); -- Given a list of dependence or refinement clauses Clauses, normalize -- each clause by creating multiple dependencies with exactly one input @@ -22250,6 +22172,109 @@ package body Sem_Prag is end if; end Check_Dependency_Clause; + ------------------------- + -- 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 as outputs in pragma Refined_Depends. 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; + Posted : Boolean := False; + + begin + Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id)); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); + + -- The constituent acts as an input (SPARK RM 7.2.5(3)) + + if Present (Body_Inputs) + and then Appears_In (Body_Inputs, Constit_Id) + then + Error_Msg_Name_1 := Chars (State_Id); + SPARK_Msg_NE + ("constituent & of state % must act as output in " + & "dependence refinement", N, Constit_Id); + + -- The constituent is altogether missing (SPARK RM 7.2.5(3)) + + elsif No (Body_Outputs) + or else not Appears_In (Body_Outputs, Constit_Id) + then + if not Posted then + Posted := True; + SPARK_Msg_NE + ("output state & must be replaced by all its " + & "constituents in dependence refinement", + N, State_Id); + end if; + + SPARK_Msg_NE + ("\constituent & is missing in output list", + N, Constit_Id); + end if; + + Next_Elmt (Constit_Elmt); + end loop; + end Check_Constituent_Usage; + + -- Local variables + + Item : Node_Id; + Item_Elmt : Elmt_Id; + Item_Id : Entity_Id; + + -- Start of processing for Check_Output_States + + begin + -- Inspect the outputs of pragma Depends looking for a state with a + -- visible refinement. + + if Present (Spec_Outputs) then + Item_Elmt := First_Elmt (Spec_Outputs); + while Present (Item_Elmt) loop + Item := Node (Item_Elmt); + + -- Deal with the mixed nature of the input and output lists + + if Nkind (Item) = N_Defining_Identifier then + Item_Id := Item; + else + Item_Id := Available_View (Entity_Of (Item)); + end if; + + if Ekind (Item_Id) = E_Abstract_State then + + -- The state acts as an input-output, skip it + + if Present (Spec_Inputs) + and then Appears_In (Spec_Inputs, Item_Id) + then + null; + + -- Ensure that all of the constituents are utilized as + -- outputs in pragma Refined_Depends. + + elsif Has_Non_Null_Refinement (Item_Id) then + Check_Constituent_Usage (Item_Id); + end if; + end if; + + Next_Elmt (Item_Elmt); + end loop; + end if; + end Check_Output_States; + ----------------------- -- Normalize_Clauses -- ----------------------- @@ -22265,6 +22290,15 @@ package body Sem_Prag is -- Output => Input_1 -- normalizations -- Output => Input_2 + procedure Normalize_Outputs (Clause : Node_Id); + -- Normalize clause Clause by creating multiple clause for each + -- output item of Clause. The transformation is as follows: + -- + -- (Output_1, Output_2) => Input -- original + -- + -- Output_1 => Input -- normalization + -- Output_2 => Input + ---------------------- -- Normalize_Inputs -- ---------------------- @@ -22324,6 +22358,68 @@ package body Sem_Prag is end if; end Normalize_Inputs; + ----------------------- + -- Normalize_Outputs -- + ----------------------- + + procedure Normalize_Outputs (Clause : Node_Id) is + Inputs : constant Node_Id := Expression (Clause); + Loc : constant Source_Ptr := Sloc (Clause); + Outputs : constant Node_Id := First (Choices (Clause)); + Last_Output : Node_Id; + New_Clause : Node_Id; + Next_Output : Node_Id; + Output : Node_Id; + + begin + -- Multiple outputs appear as an aggregate. Nothing to do when + -- the clause has exactly one output. + + if Nkind (Outputs) = N_Aggregate then + Last_Output := Last (Expressions (Outputs)); + + -- Create a clause for each output. Note that each time a new + -- clause is created, the original output list slowly shrinks + -- until there is one item left. + + Output := First (Expressions (Outputs)); + while Present (Output) loop + Next_Output := Next (Output); + + -- Unhook the output from the original output list as it + -- will be relocated to a new clause. + + Remove (Output); + + -- Special processing for the last output. At this point + -- the original aggregate has been stripped down to one + -- element. Replace the aggregate by the element itself. + + if Output = Last_Output then + Rewrite (Outputs, Output); + + else + -- Generate a clause of the form: + -- (Output => Inputs) + + New_Clause := + Make_Component_Association (Loc, + Choices => New_List (Output), + Expression => New_Copy_Tree (Inputs)); + + -- The new clause contains replicated content that has + -- already been analyzed. There is not need to reanalyze + -- them. + + Set_Analyzed (New_Clause); + Insert_After (Clause, New_Clause); + end if; + + Output := Next_Output; + end loop; + end if; + end Normalize_Outputs; + -- Local variables Clause : Node_Id; @@ -22331,6 +22427,12 @@ package body Sem_Prag is -- Start of processing for Normalize_Clauses begin + Clause := First (Clauses); + while Present (Clause) loop + Normalize_Outputs (Clause); + Next (Clause); + end loop; + Clause := First (Clauses); while Present (Clause) loop Normalize_Inputs (Clause); @@ -22368,12 +22470,14 @@ package body Sem_Prag is -- Local variables - Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); - Errors : constant Nat := Serious_Errors_Detected; - Refs : constant Node_Id := + Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); + Errors : constant Nat := Serious_Errors_Detected; + Refs : constant Node_Id := Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); Clause : Node_Id; Deps : Node_Id; + Dummy : Boolean; -- Start of processing for Analyze_Refined_Depends_In_Decl_Part @@ -22417,11 +22521,43 @@ package body Sem_Prag is Analyze_Depends_In_Decl_Part (N); -- Do not match dependencies against refinements if Refined_Depends is - -- illegal to avoid emitting misleading error. Matching is disabled in - -- ASIS because clauses are not normalized as this is a tree altering - -- activity similar to expansion. + -- illegal to avoid emitting misleading error. + + if Serious_Errors_Detected = Errors then + + -- The related subprogram lacks pragma [Refined_]Global. Synthesize + -- the inputs and outputs of the subprogram spec and body to verify + -- the use of states with visible refinement and their constituents. + + if No (Get_Pragma (Spec_Id, Pragma_Global)) + or else No (Get_Pragma (Body_Id, Pragma_Refined_Global)) + then + Collect_Subprogram_Inputs_Outputs + (Subp_Id => Spec_Id, + Synthesize => True, + Subp_Inputs => Spec_Inputs, + Subp_Outputs => Spec_Outputs, + Global_Seen => Dummy); + + Collect_Subprogram_Inputs_Outputs + (Subp_Id => Body_Id, + Synthesize => True, + Subp_Inputs => Body_Inputs, + Subp_Outputs => Body_Outputs, + Global_Seen => Dummy); + + -- For an output state with a visible refinement, ensure that all + -- constituents appear as outputs in the dependency refinement. - if Serious_Errors_Detected = Errors and then not ASIS_Mode then + Check_Output_States; + end if; + + -- Matching is disabled in ASIS because clauses are not normalized as + -- this is a tree altering activity similar to expansion. + + if ASIS_Mode then + return; + end if; -- Multiple dependency clauses appear as component associations of an -- aggregate. Note that the clauses are copied because the algorithm @@ -22533,6 +22669,14 @@ package body Sem_Prag is -- Verify the legality of a single global list declaration. Global_Mode -- denotes the current mode in effect. + procedure Collect_Global_Items (Prag : Node_Id); + -- Gather all input, in out, output and Proof_In items of pragma Prag + -- in lists In_Items, In_Out_Items, Out_Items and Proof_In_Items. Flags + -- Has_In_State, Has_In_Out_State, Has_Out_State and Has_Proof_In_State + -- are set when there is at least one abstract state with visible + -- refinement available in the corresponding mode. Flag Has_Null_State + -- is set when at least state has a null refinement. + function Present_Then_Remove (List : Elist_Id; Item : Entity_Id) return Boolean; @@ -23068,6 +23212,142 @@ package body Sem_Prag is 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 := + Available_View (Entity_Of (Item)); + -- The above handles abstract views of variables and states + -- built for limited with clauses. + + begin + -- Signal that the global list contains at least one abstract + -- state with a visible refinement. Note that the refinement + -- may be null in which case there are no constituents. + + if Ekind (Item_Id) = E_Abstract_State then + if Has_Null_Refinement (Item_Id) then + Has_Null_State := True; + + elsif Has_Non_Null_Refinement (Item_Id) then + if Mode = Name_Input then + Has_In_State := True; + elsif Mode = Name_In_Out then + Has_In_Out_State := True; + elsif Mode = Name_Output then + Has_Out_State := True; + elsif Mode = Name_Proof_In then + Has_Proof_In_State := True; + end if; + 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); + elsif Mode = Name_Proof_In then + Add_Item (Item_Id, Proof_In_Items); + end if; + end Process_Global_Item; + + -- Local variables + + Item : Node_Id; + + -- Start of processing for Process_Global_List + + begin + if Nkind (List) = N_Null then + null; + + -- Single global item declaration + + elsif 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 mode. + + 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; + + -- To accomodate partial decoration of disabled SPARK features, + -- this routine may be called with illegal input. If this is the + -- case, do not raise Program_Error. + + else + null; + end if; + end Process_Global_List; + + -- Start of processing for Collect_Global_Items + + begin + Process_Global_List + (Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)))); + end Collect_Global_Items; + ------------------------- -- Present_Then_Remove -- ------------------------- @@ -23159,17 +23439,7 @@ package body Sem_Prag is -- Extract all relevant items from the corresponding Global pragma - Collect_Global_Items - (Prag => Global, - In_Items => In_Items, - In_Out_Items => In_Out_Items, - Out_Items => Out_Items, - Proof_In_Items => Proof_In_Items, - Has_In_State => Has_In_State, - Has_In_Out_State => Has_In_Out_State, - Has_Out_State => Has_Out_State, - Has_Proof_In_State => Has_Proof_In_State, - Has_Null_State => Has_Null_State); + Collect_Global_Items (Global); -- Corresponding Global pragma must mention at least one state witha -- visible refinement at the point Refined_Global is processed. States @@ -24638,135 +24908,89 @@ package body Sem_Prag is end loop; end Check_State_And_Constituent_Use; - -------------------------- - -- Collect_Global_Items -- - -------------------------- - - procedure Collect_Global_Items - (Prag : Node_Id; - In_Items : in out Elist_Id; - In_Out_Items : in out Elist_Id; - Out_Items : in out Elist_Id; - Proof_In_Items : in out Elist_Id; - Has_In_State : out Boolean; - Has_In_Out_State : out Boolean; - Has_Out_State : out Boolean; - Has_Proof_In_State : out Boolean; - Has_Null_State : out Boolean) + --------------------------------------- + -- Collect_Subprogram_Inputs_Outputs -- + --------------------------------------- + + procedure Collect_Subprogram_Inputs_Outputs + (Subp_Id : Entity_Id; + Synthesize : Boolean := False; + Subp_Inputs : in out Elist_Id; + Subp_Outputs : in out Elist_Id; + Global_Seen : out Boolean) is - procedure Process_Global_List + procedure Collect_Dependency_Clause (Clause : Node_Id); + -- Collect all relevant items from a dependency clause + + procedure Collect_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. + -- Collect all relevant items from a global list - ------------------------- - -- Process_Global_List -- - ------------------------- + ------------------------------- + -- Collect_Dependency_Clause -- + ------------------------------- - 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. + procedure Collect_Dependency_Clause (Clause : Node_Id) is + procedure Collect_Dependency_Item + (Item : Node_Id; + Is_Input : Boolean); + -- Add an item to the proper subprogram input or output collection - ------------------------- - -- Process_Global_Item -- - ------------------------- + ----------------------------- + -- Collect_Dependency_Item -- + ----------------------------- - procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id) is - Item_Id : constant Entity_Id := Available_View (Entity_Of (Item)); - -- The above handles abstract views of variables and states built - -- for limited with clauses. + procedure Collect_Dependency_Item + (Item : Node_Id; + Is_Input : Boolean) + is + Extra : Node_Id; begin - -- Signal that the global list contains at least one abstract - -- state with a visible refinement. Note that the refinement may - -- be null in which case there are no constituents. - - if Ekind (Item_Id) = E_Abstract_State then - if Has_Null_Refinement (Item_Id) then - Has_Null_State := True; - - elsif Has_Non_Null_Refinement (Item_Id) then - if Mode = Name_Input then - Has_In_State := True; - elsif Mode = Name_In_Out then - Has_In_Out_State := True; - elsif Mode = Name_Output then - Has_Out_State := True; - elsif Mode = Name_Proof_In then - Has_Proof_In_State := True; - end if; - 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); - elsif Mode = Name_Proof_In then - Add_Item (Item_Id, Proof_In_Items); - end if; - end Process_Global_Item; - - -- Local variables - - Item : Node_Id; + -- Nothing to collect when the item is null - -- Start of processing for Process_Global_List - - begin - if Nkind (List) = N_Null then - null; - - -- Single global item declaration - - elsif 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 + if Nkind (Item) = N_Null then + null; - elsif Nkind (List) = N_Aggregate then + -- Ditto for attribute 'Result - -- The declaration of a simple global list appear as a collection - -- of expressions. + elsif Is_Attribute_Result (Item) then + null; - if Present (Expressions (List)) then - Item := First (Expressions (List)); - while Present (Item) loop - Process_Global_Item (Item, Mode); + -- Multiple items appear as an aggregate - Next (Item); + elsif Nkind (Item) = N_Aggregate then + Extra := First (Expressions (Item)); + while Present (Extra) loop + Collect_Dependency_Item (Extra, Is_Input); + Next (Extra); end loop; - -- The declaration of a moded global list appears as a collection - -- of component associations where individual choices denote mode. + -- Otherwise this is a solitary item - 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)))); + else + if Is_Input then + Add_Item (Item, Subp_Inputs); + else + Add_Item (Item, Subp_Outputs); + end if; + end if; + end Collect_Dependency_Item; - Next (Item); - end loop; + -- Start of processing for Collect_Dependency_Clause - -- Invalid tree + begin + if Nkind (Clause) = N_Null then + null; - else - raise Program_Error; - end if; + -- A dependency cause appears as component association + + elsif Nkind (Clause) = N_Component_Association then + Collect_Dependency_Item + (Expression (Clause), Is_Input => True); + Collect_Dependency_Item + (First (Choices (Clause)), Is_Input => False); -- To accomodate partial decoration of disabled SPARK features, this -- routine may be called with illegal input. If this is the case, do @@ -24775,41 +24999,7 @@ package body Sem_Prag is else null; end if; - end Process_Global_List; - - -- Local variables - - Items : constant Node_Id := - Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag))); - - -- Start of processing for Collect_Global_Items - - begin - -- Assume that no states have been encountered - - Has_In_State := False; - Has_In_Out_State := False; - Has_Out_State := False; - Has_Proof_In_State := False; - Has_Null_State := False; - - Process_Global_List (Items); - end Collect_Global_Items; - - --------------------------------------- - -- Collect_Subprogram_Inputs_Outputs -- - --------------------------------------- - - procedure Collect_Subprogram_Inputs_Outputs - (Subp_Id : Entity_Id; - Subp_Inputs : in out Elist_Id; - Subp_Outputs : in out Elist_Id; - Global_Seen : out Boolean) - is - procedure Collect_Global_List - (List : Node_Id; - Mode : Name_Id := Name_Input); - -- Collect all relevant items from a global list + end Collect_Dependency_Clause; ------------------------- -- Collect_Global_List -- @@ -24887,7 +25077,10 @@ package body Sem_Prag is -- Local variables - Subp_Decl : constant Node_Id := Parent (Parent (Subp_Id)); + Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); + Clause : Node_Id; + Clauses : Node_Id; + Depends : Node_Id; Formal : Entity_Id; Global : Node_Id; List : Node_Id; @@ -24939,18 +25132,23 @@ package body Sem_Prag is Next_Formal (Formal); end loop; - -- When processing a subprogram body, look for pragma Refined_Global as - -- it provides finer granularity of inputs and outputs. + -- When processing a subprogram body, look for pragmas Refined_Depends + -- and Refined_Global as they specify the inputs and outputs. if Ekind (Subp_Id) = E_Subprogram_Body then - Global := Get_Pragma (Subp_Id, Pragma_Refined_Global); + Depends := Get_Pragma (Subp_Id, Pragma_Refined_Depends); + Global := Get_Pragma (Subp_Id, Pragma_Refined_Global); - -- Subprogram declaration case, look for pragma Global + -- Subprogram declaration case, look for pragmas Depends and Global else - Global := Get_Pragma (Spec_Id, Pragma_Global); + Depends := Get_Pragma (Spec_Id, Pragma_Depends); + Global := Get_Pragma (Spec_Id, Pragma_Global); end if; + -- Pragma [Refined_]Global takes precedence over [Refined_]Depends + -- because it provides finer granularity of inputs and outputs. + if Present (Global) then Global_Seen := True; List := Expression (First (Pragma_Argument_Associations (Global))); @@ -24967,10 +25165,29 @@ package body Sem_Prag is end if; end if; - -- Nothing to be done for a null global list + Collect_Global_List (List); + + -- When the related subprogram lacks pragma [Refined_]Global, fall back + -- to [Refined_]Depends if the caller requests this behavior. Synthesize + -- the inputs and outputs from [Refined_]Depends. + + elsif Synthesize and then Present (Depends) then + Clauses := + Get_Pragma_Arg (First (Pragma_Argument_Associations (Depends))); + + -- Multiple dependency clauses appear as an aggregate + + if Nkind (Clauses) = N_Aggregate then + Clause := First (Component_Associations (Clauses)); + while Present (Clause) loop + Collect_Dependency_Clause (Clause); + Next (Clause); + end loop; + + -- Otherwise this is a single dependency clause - if Nkind (List) /= N_Null then - Collect_Global_List (List); + else + Collect_Dependency_Clause (Clauses); end if; end if; end Collect_Subprogram_Inputs_Outputs; diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 4d6b1c0407e..d89039af320 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -172,14 +172,21 @@ package Sem_Prag is procedure Collect_Subprogram_Inputs_Outputs (Subp_Id : Entity_Id; + Synthesize : Boolean := False; Subp_Inputs : in out Elist_Id; Subp_Outputs : in out Elist_Id; Global_Seen : out Boolean); - -- Used during the analysis of pragmas Depends, Global, Refined_Depends, - -- and Refined_Global. Also used by GNATprove. Gathers all inputs and - -- outputs of subprogram Subp_Id in lists Subp_Inputs and Subp_Outputs. - -- If subprogram has no inputs and/or outputs, then the returned list - -- is No_Elist. Global_Seen is set when the related subprogram has + -- Subsidiary to the analysis of pragmas Depends, Global, Refined_Depends + -- and Refined_Global. The routine is also used by GNATprove. Collect all + -- inputs and outputs of subprogram Subp_Id in lists Subp_Inputs (inputs) + -- and Subp_Outputs (outputs). The inputs and outputs are gathered from: + -- 1) The formal parameters of the subprogram + -- 2) The items of pragma [Refined_]Global + -- or + -- 3) The items of pragma [Refined_]Depends if there is no pragma + -- [Refined_]Global present and flag Synthesize is set to True. + -- If the subprogram has no inputs and/or outputs, then the returned list + -- is No_Elist. Flag Global_Seen is set when the related subprogram has -- pragma [Refined_]Global. function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean;