diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 30 | ||||
| -rw-r--r-- | gcc/ada/exp_util.adb | 13 | ||||
| -rw-r--r-- | gcc/ada/g-memdum.adb | 10 | ||||
| -rw-r--r-- | gcc/ada/g-memdum.ads | 28 | ||||
| -rw-r--r-- | gcc/ada/i-cstrea.ads | 6 | ||||
| -rw-r--r-- | gcc/ada/sem_ch5.adb | 6 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 945 |
7 files changed, 397 insertions, 641 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f136cc7..504e7f8 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,33 @@ +2014-07-18 Thomas Quinot <quinot@adacore.com> + + * g-memdum.adb, g-memdum.ads: Code clean ups. + +2014-07-18 Hristian Kirtchev <kirtchev@adacore.com> + + * sem_prag.adb (Check_Dependency_Clause): + Update the comment on usage. Reimplement the mechanism which + attempts to match a single clause of Depends against one or + more clauses of Refined_Depends. + (Input_Match): Removed. + (Inputs_Match): Removed. + (Is_Self_Referential): Removed. + (Normalize_Clause): Update the call to Split_Multiple_Outputs. + (Normalize_Outputs): Rename variable Split to New_Claue and update + all its occurrences. + (Report_Extra_Clauses): Update the comment on usage. + (Split_Multiple_Outputs): Renamed to Normalize_Outputs. + +2014-07-18 Gary Dismukes <dismukes@adacore.com> + + * i-cstrea.ads: Minor reformatting. + +2014-07-18 Hristian Kirtchev <kirtchev@adacore.com> + + * exp_util.adb (Wrap_Statements_In_Block): Propagate both + secondary stack-related flags to the generated block. + * sem_ch5.adb (Analyze_Loop_Statement): Update the scope chain + once the loop is relocated in a block. + 2014-07-18 Robert Dewar <dewar@adacore.com> * repinfo.ads: Add documentation on handling of back annotation diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 6db424c..a94a11b 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -6667,13 +6667,18 @@ package body Exp_Util is -- When wrapping the statements of an iterator loop, check whether -- the loop requires secondary stack management and if so, propagate - -- the flag to the block. This way the secondary stack is marked and - -- released at each iteration of the loop. + -- the appropriate flags to the block. This ensures that the cursor + -- is properly cleaned up at each iteration of the loop. Management + -- is not performed when the loop contains a return statement which + -- also uses the secondary stack as this will destroy the result + -- prematurely. Iter_Loop := Find_Enclosing_Iterator_Loop (Scop); - if Present (Iter_Loop) and then Uses_Sec_Stack (Iter_Loop) then - Set_Uses_Sec_Stack (Block_Id); + if Present (Iter_Loop) then + Set_Sec_Stack_Needed_For_Return + (Block_Id, Sec_Stack_Needed_For_Return (Iter_Loop)); + Set_Uses_Sec_Stack (Block_Id, Uses_Sec_Stack (Iter_Loop)); end if; return Block_Nod; diff --git a/gcc/ada/g-memdum.adb b/gcc/ada/g-memdum.adb index 9d7b25c..8aa24a7 100644 --- a/gcc/ada/g-memdum.adb +++ b/gcc/ada/g-memdum.adb @@ -46,8 +46,16 @@ package body GNAT.Memory_Dump is procedure Dump (Addr : Address; + Count : Natural) + is + begin + Dump (Addr, Count, Prefix => Absolute_Address); + end Dump; + + procedure Dump + (Addr : Address; Count : Natural; - Prefix : Prefix_Type := Absolute_Address) + Prefix : Prefix_Type) is Ctr : Natural := Count; -- Count of bytes left to output diff --git a/gcc/ada/g-memdum.ads b/gcc/ada/g-memdum.ads index 840fc92..7f9951b 100644 --- a/gcc/ada/g-memdum.ads +++ b/gcc/ada/g-memdum.ads @@ -42,20 +42,36 @@ package GNAT.Memory_Dump is procedure Dump (Addr : System.Address; - Count : Natural; - Prefix : Prefix_Type := Absolute_Address); + Count : Natural); -- Dumps indicated number (Count) of bytes, starting at the address given -- by Addr. The coding of this routine in its current form assumes the case -- of a byte addressable machine (and is therefore inapplicable to machines -- like the AAMP, where the storage unit is not 8 bits). The output is one -- or more lines in the following format, which is for the case of 32-bit -- addresses (64-bit addresses are handled appropriately): - -- + -- 0234_3368: 66 67 68 . . . 73 74 75 "fghijklmnopqstuv" - -- + -- All but the last line have 16 bytes. A question mark is used in the -- string data to indicate a non-printable character. - -- - -- Please document Prefix ??? + + procedure Dump + (Addr : System.Address; + Count : Natural; + Prefix : Prefix_Type); + -- Same as above, but allows the selection of different line formats. + -- If Prefix is set to Absolute_Address, the output is identical to the + -- above version, each line starting with the absolute address of the + -- first dumped storage element. + + -- If Prefix is set to Offset, then instead each line starts with the + -- indication of the offset relative to Addr: + + -- 00: 66 67 68 . . . 73 74 75 "fghijklmnopqstuv" + + -- Finally if Prefix is set to None, the prefix is suppressed altogether, + -- and only the memory contents are displayed: + + -- 66 67 68 . . . 73 74 75 "fghijklmnopqstuv" end GNAT.Memory_Dump; diff --git a/gcc/ada/i-cstrea.ads b/gcc/ada/i-cstrea.ads index 67ca62f..dc33787 100644 --- a/gcc/ada/i-cstrea.ads +++ b/gcc/ada/i-cstrea.ads @@ -230,9 +230,9 @@ package Interfaces.C_Streams is procedure set_text_mode (handle : int); -- set_wide_text_mode is as set_text_mode but switches the translation to - -- 16-bits wide-character instead of 8-bits character. Again this routine - -- has not effect if text_translation_required is false. On Windows this - -- is used to have proper 16-bits wide string output on the console for + -- 16-bit wide-character instead of 8-bit character. Again, this routine + -- has no effect if text_translation_required is false. On Windows this + -- is used to have proper 16-bit wide-string output on the console for -- example. procedure set_wide_text_mode (handle : int); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index d90a7e5..40034e7 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -2885,6 +2885,12 @@ package body Sem_Ch5 is Add_Block_Identifier (Block_Nod, Block_Id); + -- Fix the loop scope once the loop statement is relocated inside + -- the block, otherwise the loop and the block end up sharing the + -- same parent scope. + + Set_Scope (Ent, Block_Id); + -- The expansion of iterator loops generates an iterator in order -- to traverse the elements of a container: diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index c36a8fb..73a4f87 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -1340,7 +1340,7 @@ package body Sem_Prag is -- Flag Multiple should be set when Output comes from a list with -- multiple items. - procedure Split_Multiple_Outputs; + 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. @@ -1530,20 +1530,18 @@ package body Sem_Prag is end if; end Create_Or_Modify_Clause; - ---------------------------- - -- Split_Multiple_Outputs -- - ---------------------------- + ----------------------- + -- Normalize_Outputs -- + ----------------------- - procedure Split_Multiple_Outputs is + 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; - Split : Node_Id; - - -- Start of processing for Split_Multiple_Outputs begin -- Multiple outputs appear as an aggregate. Nothing to do when @@ -1576,7 +1574,7 @@ package body Sem_Prag is -- Generate a clause of the form: -- (Output => Inputs) - Split := + New_Clause := Make_Component_Association (Loc, Choices => New_List (Output), Expression => New_Copy_Tree (Inputs)); @@ -1585,14 +1583,14 @@ package body Sem_Prag is -- already been analyzed. There is not need to reanalyze -- them. - Set_Analyzed (Split); - Insert_After (Clause, Split); + Set_Analyzed (New_Clause); + Insert_After (Clause, New_Clause); end if; Output := Next_Output; end loop; end if; - end Split_Multiple_Outputs; + end Normalize_Outputs; -- Local variables @@ -1652,7 +1650,7 @@ package body Sem_Prag is -- Split a clause with multiple outputs into multiple clauses with a -- single output. - Split_Multiple_Outputs; + Normalize_Outputs; end Normalize_Clause; -- Local variables @@ -21831,6 +21829,9 @@ package body Sem_Prag is Depends : Node_Id; -- The corresponding Depends pragma along with its clauses + Refined_States : Elist_Id := No_Elist; + -- A list containing all successfully refined states + Refinements : List_Id := No_List; -- The clauses of pragma Refined_Depends @@ -21838,706 +21839,400 @@ package body Sem_Prag is -- The entity of the subprogram subject to pragma Refined_Depends procedure Check_Dependency_Clause (Dep_Clause : Node_Id); - -- Verify the legality of a single clause - - function Input_Match - (Dep_Input : Node_Id; - Ref_Inputs : List_Id; - Post_Errors : Boolean) return Boolean; - -- Determine whether input Dep_Input matches one of inputs found in list - -- Ref_Inputs. If flag Post_Errors is set, the routine reports missed or - -- extra input items. - - function Inputs_Match - (Dep_Clause : Node_Id; - Ref_Clause : Node_Id; - Post_Errors : Boolean) return Boolean; - -- Determine whether the inputs of Depends clause Dep_Clause match those - -- of refinement clause Ref_Clause. If flag Post_Errors is set, then the - -- routine reports missed or extra input items. - - function Is_Self_Referential (Item_Id : Entity_Id) return Boolean; - -- Determine whether a formal parameter, variable or state denoted by - -- Item_Id appears both as input and an output in a single clause of - -- pragma Depends. + -- 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 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 + -- and one output. procedure Report_Extra_Clauses; - -- Emit an error for each extra clause the appears in Refined_Depends + -- Emit an error for each extra clause found in list Refinements ----------------------------- -- Check_Dependency_Clause -- ----------------------------- procedure Check_Dependency_Clause (Dep_Clause : Node_Id) is - Dep_Output : constant Node_Id := First (Choices (Dep_Clause)); - Dep_Id : Entity_Id; - Matching_Clause : Node_Id := Empty; - Next_Ref_Clause : Node_Id; - Ref_Clause : Node_Id; - Ref_Id : Entity_Id; - Ref_Output : Node_Id; - - Has_Constituent : Boolean := False; - -- Flag set when the refinement output list contains at least one - -- constituent of the state denoted by Dep_Id. + Dep_Input : constant Node_Id := Expression (Dep_Clause); + Dep_Output : constant Node_Id := First (Choices (Dep_Clause)); + + function Is_In_Out_State_Clause return Boolean; + -- Determine whether dependence clause Dep_Clause denotes an abstract + -- state that depends on itself (State => State). + + procedure Match_Items + (Dep_Item : Node_Id; + Ref_Item : Node_Id; + Matched : out Boolean); + -- Try to match dependence item Dep_Item against refinement item + -- Ref_Item. To match against a possible null refinement (see 2, 7), + -- set Ref_Item to Empty. Flag Matched is set to True when one of + -- the following conformance scenarios is in effect: + -- 1) Both items denote null + -- 2) Dep_Item denotes null and Ref_Item is Empty (special case) + -- 3) Both items denote attribute 'Result + -- 4) Both items denote the same formal parameter + -- 5) Both items denote the same variable + -- 6) Dep_Item is an abstract state with visible null refinement + -- and Ref_Item denotes null. + -- 7) Dep_Item is an abstract state with visible null refinement + -- and Ref_Item is Empty (special case). + -- 8) Dep_Item is an abstract state with visible non-null + -- refinement and Ref_Item denotes one of its constituents. + -- 9) Dep_Item is an abstract state without a visible refinement + -- and Ref_Item denotes the same state. + -- When scenario 8 is in effect, the entity of the abstract state + -- denoted by Dep_Item is added to list Refined_States. - Has_Null_State : Boolean := False; - -- Flag set when the output of clause Dep_Clause is a state with a - -- null refinement. + ---------------------------- + -- Is_In_Out_State_Clause -- + ---------------------------- - Has_Refined_State : Boolean := False; - -- Flag set when the output of clause Dep_Clause is a state with - -- visible refinement. + function Is_In_Out_State_Clause return Boolean is + Dep_Input_Id : Entity_Id; + Dep_Output_Id : Entity_Id; - begin - -- The analysis of pragma Depends should produce normalized clauses - -- with exactly one output. This is important because output items - -- are unique in the whole dependence relation and can be used as - -- keys. + begin + -- Detect the following clause: + -- State => State - pragma Assert (No (Next (Dep_Output))); + if Is_Entity_Name (Dep_Input) + and then Is_Entity_Name (Dep_Output) + then + -- Handle abstract views generated for limited with clauses - -- Inspect all clauses of Refined_Depends and attempt to match the - -- output of Dep_Clause against an output from the refinement clauses - -- set. + Dep_Input_Id := Available_View (Entity_Of (Dep_Input)); + Dep_Output_Id := Available_View (Entity_Of (Dep_Output)); - Ref_Clause := First (Refinements); - while Present (Ref_Clause) loop - Matching_Clause := Empty; + return + Ekind (Dep_Input_Id) = E_Abstract_State + and then Dep_Input_Id = Dep_Output_Id; + else + return False; + end if; + end Is_In_Out_State_Clause; - -- Store the next clause now because a match will trim the list of - -- refinement clauses and this side effect should not be visible - -- in pragma Refined_Depends. + ----------------- + -- Match_Items -- + ----------------- - Next_Ref_Clause := Next (Ref_Clause); + procedure Match_Items + (Dep_Item : Node_Id; + Ref_Item : Node_Id; + Matched : out Boolean) + is + Dep_Item_Id : Entity_Id; + Ref_Item_Id : Entity_Id; - -- The analysis of pragma Refined_Depends should produce - -- normalized clauses with exactly one output. + begin + -- Assume that the two items do not match - Ref_Output := First (Choices (Ref_Clause)); - pragma Assert (No (Next (Ref_Output))); + Matched := False; - -- Two null output lists match if their inputs match + -- A null matches null or Empty (special case) - if Nkind (Dep_Output) = N_Null - and then Nkind (Ref_Output) = N_Null + if Nkind (Dep_Item) = N_Null + and then (No (Ref_Item) or else Nkind (Ref_Item) = N_Null) then - Matching_Clause := Ref_Clause; - exit; + Matched := True; - -- Two function 'Result attributes match if their inputs match. - -- Note that there is no need to compare the two prefixes because - -- the attributes cannot denote anything but the related function. + -- Attribute 'Result matches attribute 'Result - elsif Is_Attribute_Result (Dep_Output) - and then Is_Attribute_Result (Ref_Output) + elsif Is_Attribute_Result (Dep_Item) + and then Is_Attribute_Result (Dep_Item) then - Matching_Clause := Ref_Clause; - exit; - - -- The remaining cases are formal parameters, variables and states - - elsif Is_Entity_Name (Dep_Output) then - - -- Handle abstract views of states and variables generated for - -- limited with clauses. - - Dep_Id := Available_View (Entity_Of (Dep_Output)); + Matched := True; - if Ekind (Dep_Id) = E_Abstract_State then + -- Abstract states, formal parameters and variables - -- A state with a null refinement matches either a null - -- output list or nothing at all (no clause): + elsif Is_Entity_Name (Dep_Item) then - -- Refined_State => (State => null) + -- Handle abstract views generated for limited with clauses - -- No clause + Dep_Item_Id := Available_View (Entity_Of (Dep_Item)); - -- Depends => (State => null) - -- Refined_Depends => null -- OK + if Ekind (Dep_Item_Id) = E_Abstract_State then - -- Null output list + -- An abstract state with visible null refinement matches + -- null or Empty (special case). - -- Depends => (State => <input>) - -- Refined_Depends => (null => <input>) -- OK - - if Has_Null_Refinement (Dep_Id) then - Has_Null_State := True; - - -- When a state with null refinement matches a null - -- output, compare their inputs. - - if Nkind (Ref_Output) = N_Null then - Matching_Clause := Ref_Clause; - end if; - - exit; - - -- The state has a non-null refinement in which case the - -- match is based on constituents and inputs. A state with - -- multiple output constituents may match multiple clauses: - - -- Refined_State => (State => (C1, C2)) - -- Depends => (State => <input>) - -- Refined_Depends => ((C1, C2) => <input>) - - -- When normalized, the above becomes: - - -- Refined_Depends => (C1 => <input>, - -- C2 => <input>) - - elsif Has_Non_Null_Refinement (Dep_Id) then - Has_Refined_State := True; - - -- Account for the case where a state with a non-null - -- refinement matches a null output list: - - -- Refined_State => (State_1 => (C1, C2), - -- State_2 => (C3, C4)) - -- Depends => (State_1 => State_2) - -- Refined_Depends => (null => C3) - - if Nkind (Ref_Output) = N_Null - and then Inputs_Match - (Dep_Clause => Dep_Clause, - Ref_Clause => Ref_Clause, - Post_Errors => False) - then - Has_Constituent := True; - - -- Note that the search continues after the clause is - -- removed from the pool of candidates because it may - -- have been normalized into multiple simple clauses. - - Remove (Ref_Clause); - - -- Otherwise the output of the refinement clause must be - -- a valid constituent of the state: + if Has_Null_Refinement (Dep_Item_Id) + and then (No (Ref_Item) or else Nkind (Ref_Item) = N_Null) + then + Matched := True; - -- Refined_State => (State => (C1, C2)) - -- Depends => (State => <input>) - -- Refined_Depends => (C1 => <input>) + -- An abstract state with visible non-null refinement + -- matches one of its constituents. - elsif Is_Entity_Name (Ref_Output) then - Ref_Id := Entity_Of (Ref_Output); + elsif Has_Non_Null_Refinement (Dep_Item_Id) then + if Is_Entity_Name (Ref_Item) then + Ref_Item_Id := Entity_Of (Ref_Item); - if Ekind_In (Ref_Id, E_Abstract_State, E_Variable) - and then Present (Encapsulating_State (Ref_Id)) - and then Encapsulating_State (Ref_Id) = Dep_Id - and then Inputs_Match - (Dep_Clause => Dep_Clause, - Ref_Clause => Ref_Clause, - Post_Errors => False) + if Ekind_In (Ref_Item_Id, E_Abstract_State, E_Variable) + and then Present (Encapsulating_State (Ref_Item_Id)) + and then Encapsulating_State (Ref_Item_Id) = + Dep_Item_Id then - Has_Constituent := True; + -- Record the successfully refined state - -- Note that the search continues after the clause - -- is removed from the pool of candidates because - -- it may have been normalized into multiple simple - -- clauses. + if not Contains (Refined_States, Dep_Item_Id) then + Add_Item (Dep_Item_Id, Refined_States); + end if; - Remove (Ref_Clause); + Matched := True; end if; end if; - -- The abstract view of a state matches is corresponding - -- non-abstract view: - - -- Depends => (Lim_Pack.State => <input>) - -- Refined_Depends => (State => <input>) + -- An abstract state without a visible refinement matches + -- itself. - elsif Is_Entity_Name (Ref_Output) - and then Entity_Of (Ref_Output) = Dep_Id + elsif Is_Entity_Name (Ref_Item) + and then Entity_Of (Ref_Item) = Dep_Item_Id then - Matching_Clause := Ref_Clause; - exit; + Matched := True; end if; - -- Formal parameters and variables match if their inputs match + -- A formal parameter or a variable matches itself - elsif Is_Entity_Name (Ref_Output) - and then Entity_Of (Ref_Output) = Dep_Id + elsif Is_Entity_Name (Ref_Item) + and then Entity_Of (Ref_Item) = Dep_Item_Id then - Matching_Clause := Ref_Clause; - exit; + Matched := True; end if; end if; - - Ref_Clause := Next_Ref_Clause; - end loop; - - -- Handle the case where pragma Depends contains one or more clauses - -- that only mention states with null refinements. In that case the - -- corresponding pragma Refined_Depends may have a null relation. - - -- Refined_State => (State => null) - -- Depends => (State => null) - -- Refined_Depends => null -- OK - - -- Another instance of the same scenario occurs when the list of - -- refinements has been depleted while processing previous clauses. - - if Is_Entity_Name (Dep_Output) - and then (No (Refinements) or else Is_Empty_List (Refinements)) - then - Dep_Id := Entity_Of (Dep_Output); - - if Ekind (Dep_Id) = E_Abstract_State - and then Has_Null_Refinement (Dep_Id) - then - Has_Null_State := True; - end if; - end if; - - -- The above search produced a match based on unique output. Ensure - -- that the inputs match as well and if they do, remove the clause - -- from the pool of candidates. - - if Present (Matching_Clause) then - if Inputs_Match - (Ref_Clause => Ref_Clause, - Dep_Clause => Matching_Clause, - Post_Errors => True) - then - Remove (Matching_Clause); - end if; - - -- A state with a visible refinement was matched against one or - -- more clauses containing appropriate constituents. - - elsif Has_Constituent then - null; - - -- A state with a null refinement did not warrant a clause - - elsif Has_Null_State then - null; - - -- The dependence relation of pragma Refined_Depends does not contain - -- a matching clause, emit an error. - - else - SPARK_Msg_NE - ("dependence clause of subprogram & has no matching refinement " - & "in body", Ref_Clause, Spec_Id); - - if Has_Refined_State then - SPARK_Msg_N - ("\check the use of constituents in dependence refinement", - Ref_Clause); - end if; - end if; - end Check_Dependency_Clause; - - ----------------- - -- Input_Match -- - ----------------- - - function Input_Match - (Dep_Input : Node_Id; - Ref_Inputs : List_Id; - Post_Errors : Boolean) return Boolean - is - procedure Match_Error (Msg : String; N : Node_Id); - -- Emit a matching error if flag Post_Errors is set - - ----------------- - -- Match_Error -- - ----------------- - - procedure Match_Error (Msg : String; N : Node_Id) is - begin - if Post_Errors then - SPARK_Msg_N (Msg, N); - end if; - end Match_Error; + end Match_Items; -- Local variables - Dep_Id : Node_Id; - Next_Ref_Input : Node_Id; - Ref_Id : Entity_Id; - Ref_Input : Node_Id; - - Has_Constituent : Boolean := False; - -- Flag set when the refinement input list contains at least one - -- constituent of the state denoted by Dep_Id. - - Has_Null_State : Boolean := False; - -- Flag set when the dependency input is a state with a visible null - -- refinement. - - Has_Refined_State : Boolean := False; - -- Flag set when the dependency input is a state with visible non- - -- null refinement. + Clause_Matched : Boolean := False; + Dummy : Boolean := False; + Inputs_Match : Boolean; + Next_Ref_Clause : Node_Id; + Outputs_Match : Boolean; + Ref_Clause : Node_Id; + Ref_Input : Node_Id; + Ref_Output : Node_Id; - -- Start of processing for Input_Match + -- Start of processing for Check_Dependency_Clause begin - -- Match a null input with another null input - - if Nkind (Dep_Input) = N_Null then - Ref_Input := First (Ref_Inputs); - - -- Remove the matching null from the pool of candidates - - if Nkind (Ref_Input) = N_Null then - Remove (Ref_Input); - return True; - - else - Match_Error - ("null input cannot be matched in corresponding refinement " - & "clause", Dep_Input); - end if; - - -- Remaining cases are formal parameters, variables, and states - - else - -- Handle abstract views of states and variables generated for - -- limited with clauses. - - Dep_Id := Available_View (Entity_Of (Dep_Input)); - - -- Inspect all inputs of the refinement clause and attempt to - -- match against the inputs of the dependence clause. - - Ref_Input := First (Ref_Inputs); - while Present (Ref_Input) loop - - -- Store the next input now because a match will remove it from - -- the list. - - Next_Ref_Input := Next (Ref_Input); - - if Ekind (Dep_Id) = E_Abstract_State then - - -- A state with a null refinement matches either a null - -- input list or nothing at all (no input): - - -- Refined_State => (State => null) - - -- No input - - -- Depends => (<output> => (State, Input)) - -- Refined_Depends => (<output> => Input) -- OK - - -- Null input list - - -- Depends => (<output> => State) - -- Refined_Depends => (<output> => null) -- OK - - if Has_Null_Refinement (Dep_Id) then - Has_Null_State := True; - - -- Remove the matching null from the pool of candidates + -- Examine all refinement clauses and compare them against the + -- dependence clause. - if Nkind (Ref_Input) = N_Null then - Remove (Ref_Input); - end if; - - return True; - - -- The state has a non-null refinement in which case remove - -- all the matching constituents of the state: - - -- Refined_State => (State => (C1, C2)) - -- Depends => (<output> => State) - -- Refined_Depends => (<output> => (C1, C2)) - - elsif Has_Non_Null_Refinement (Dep_Id) then - Has_Refined_State := True; - - -- A state with a visible non-null refinement may have a - -- null input_list only when it is self referential. - - -- Refined_State => (State => (C1, C2)) - -- Depends => (State => State) - -- Refined_Depends => (C2 => null) -- OK - - if Nkind (Ref_Input) = N_Null - and then Is_Self_Referential (Dep_Id) - then - -- Remove the null from the pool of candidates. Note - -- that the search continues because the state may be - -- represented by multiple constituents. + Ref_Clause := First (Refinements); + while Present (Ref_Clause) loop + Next_Ref_Clause := Next (Ref_Clause); - Has_Constituent := True; - Remove (Ref_Input); + -- Obtain the attributes of the current refinement clause - -- Ref_Input is an entity name + Ref_Input := Expression (Ref_Clause); + Ref_Output := First (Choices (Ref_Clause)); - elsif Is_Entity_Name (Ref_Input) then - Ref_Id := Entity_Of (Ref_Input); + -- The current refinement clause matches the dependence clause + -- when both outputs match and both inputs match. See routine + -- Match_Items for all possible conformance scenarios. - -- The input of the refinement clause is a valid - -- constituent of the state. Remove the input from the - -- pool of candidates. Note that the search continues - -- because the state may be represented by multiple - -- constituents. + -- Depends Dep_Output => Dep_Input + -- ^ ^ + -- match ? match ? + -- v v + -- Refined_Depends Ref_Output => Ref_Input - if Ekind_In (Ref_Id, E_Abstract_State, - E_Variable) - and then Present (Encapsulating_State (Ref_Id)) - and then Encapsulating_State (Ref_Id) = Dep_Id - then - Has_Constituent := True; - Remove (Ref_Input); - end if; - end if; + Match_Items + (Dep_Item => Dep_Input, + Ref_Item => Ref_Input, + Matched => Inputs_Match); - -- The abstract view of a state matches its corresponding - -- non-abstract view: + Match_Items + (Dep_Item => Dep_Output, + Ref_Item => Ref_Output, + Matched => Outputs_Match); - -- Depends => (<output> => Lim_Pack.State) - -- Refined_Depends => (<output> => State) + -- An In_Out state clause may be matched against a refinement with + -- a null input or null output as long as the non-null side of the + -- relation contains a valid constituent of the In_Out_State. - elsif Is_Entity_Name (Ref_Input) - and then Entity_Of (Ref_Input) = Dep_Id - then - Remove (Ref_Input); - return True; - end if; + if Is_In_Out_State_Clause then - -- Formal parameters and variables are matched on entities. If - -- this is the case, remove the input from the candidate list. + -- Depends => (State => State) + -- Refined_Depends => (null => Constit) -- OK - elsif Is_Entity_Name (Ref_Input) - and then Entity_Of (Ref_Input) = Dep_Id + if Inputs_Match + and then not Outputs_Match + and then Nkind (Ref_Output) = N_Null then - Remove (Ref_Input); - return True; + Outputs_Match := True; end if; - Ref_Input := Next_Ref_Input; - end loop; + -- Depends => (State => State) + -- Refined_Depends => (Constit => null) -- OK - -- When a state with a null refinement appears as the last input, - -- it matches nothing: - - -- Refined_State => (State => null) - -- Depends => (<output> => (Input, State)) - -- Refined_Depends => (<output> => Input) -- OK - - if Ekind (Dep_Id) = E_Abstract_State - and then Has_Null_Refinement (Dep_Id) - and then No (Ref_Input) - then - Has_Null_State := True; + if not Inputs_Match + and then Outputs_Match + and then Nkind (Ref_Input) = N_Null + then + Inputs_Match := True; + end if; end if; - end if; - - -- A state with visible refinement was matched against one or more of - -- its constituents. - - if Has_Constituent then - return True; - - -- A state with a null refinement matched null or nothing - - elsif Has_Null_State then - return True; - -- The input of a dependence clause does not have a matching input in - -- the refinement clause, emit an error. + -- The current refinement clause is legally constructed following + -- the rules in SPARK RM 7.2.5, therefore it can be removed from + -- the pool of candidates. The seach continues because a single + -- dependence clause may have multiple matching refinements. - else - Match_Error - ("input cannot be matched in corresponding refinement clause", - Dep_Input); - - if Has_Refined_State then - Match_Error - ("\check the use of constituents in dependence refinement", - Dep_Input); + if Inputs_Match and then Outputs_Match then + Clause_Matched := True; + Remove (Ref_Clause); end if; - return False; - end if; - end Input_Match; - - ------------------ - -- Inputs_Match -- - ------------------ - - function Inputs_Match - (Dep_Clause : Node_Id; - Ref_Clause : Node_Id; - Post_Errors : Boolean) return Boolean - is - Ref_Inputs : List_Id; - -- The input list of the refinement clause + Ref_Clause := Next_Ref_Clause; + end loop; - procedure Report_Extra_Inputs; - -- Emit errors for all extra inputs that appear in Ref_Inputs + -- Depending on the order or composition of refinement clauses, an + -- In_Out state clause may not be directly refinable. - ------------------------- - -- Report_Extra_Inputs -- - ------------------------- + -- Depends => ((Output, State) => (Input, State)) + -- Refined_State => (State => (Constit_1, Constit_2)) + -- Refined_Depends => (Constit_1 => Input, Output => Constit_2) - procedure Report_Extra_Inputs is - Input : Node_Id; + -- Matching normalized clause (State => State) fails because there is + -- no direct refinement capable of satisfying this relation. Another + -- similar case arises when clauses (Constit_1 => Input) and (Output + -- => Constit_2) are matched first, leaving no candidates for clause + -- (State => State). Both scenarios are legal as long as one of the + -- previous clauses mentioned a valid constituent of State. - begin - if Present (Ref_Inputs) and then Post_Errors then - Input := First (Ref_Inputs); - while Present (Input) loop - SPARK_Msg_N - ("unmatched or extra input in refinement clause", Input); - - Next (Input); - end loop; - end if; - end Report_Extra_Inputs; + if not Clause_Matched + and then Is_In_Out_State_Clause + and then Contains + (Refined_States, Available_View (Entity_Of (Dep_Input))) + then + Clause_Matched := True; + end if; - -- Local variables + -- At this point either all refinement clauses have been examined or + -- pragma Refined_Depends contains a solitary null. Only an abstract + -- state with null refinement can possibly match these cases. - Dep_Inputs : constant Node_Id := Expression (Dep_Clause); - Inputs : constant Node_Id := Expression (Ref_Clause); - Dep_Input : Node_Id; - Result : Boolean; + -- Depends => (State => null) + -- Refined_State => (State => null) + -- Refined_Depends => null -- OK - -- Start of processing for Inputs_Match + if not Clause_Matched then + Match_Items + (Dep_Item => Dep_Input, + Ref_Item => Empty, + Matched => Inputs_Match); - begin - -- Construct a list of all refinement inputs. Note that the input - -- list is copied because the algorithm modifies its contents and - -- this should not be visible in Refined_Depends. The same applies - -- for a solitary input. + Match_Items + (Dep_Item => Dep_Output, + Ref_Item => Empty, + Matched => Outputs_Match); - if Nkind (Inputs) = N_Aggregate then - Ref_Inputs := New_Copy_List (Expressions (Inputs)); - else - Ref_Inputs := New_List (New_Copy (Inputs)); + Clause_Matched := Inputs_Match and Outputs_Match; end if; - -- Depending on whether the original dependency clause mentions - -- states with visible refinement, the corresponding refinement - -- clause may differ greatly in structure and contents: + -- If the contents of Refined_Depends are legal, then the current + -- dependence clause should be satisfied either by an explicit match + -- or by one of the special cases. - -- State with null refinement + if not Clause_Matched then + SPARK_Msg_NE + ("dependence clause of subprogram & has no matching refinement " + & "in body", Dep_Clause, Spec_Id); + end if; + end Check_Dependency_Clause; - -- Refined_State => (State => null) - -- Depends => (<output> => State) - -- Refined_Depends => (<output> => null) + ----------------------- + -- Normalize_Clauses -- + ----------------------- - -- Depends => (<output> => (State, Input)) - -- Refined_Depends => (<output> => Input) + procedure Normalize_Clauses (Clauses : List_Id) is + procedure Normalize_Inputs (Clause : Node_Id); + -- Normalize clause Clause by creating multiple clauses for each + -- input item of Clause. It is assumed that Clause has exactly one + -- output. The transformation is as follows: + -- + -- Output => (Input_1, Input_2) -- original + -- + -- Output => Input_1 -- normalizations + -- Output => Input_2 - -- Depends => (<output> => (Input_1, State, Input_2)) - -- Refined_Depends => (<output> => (Input_1, Input_2)) + ---------------------- + -- Normalize_Inputs -- + ---------------------- - -- State with non-null refinement + procedure Normalize_Inputs (Clause : Node_Id) is + Inputs : constant Node_Id := Expression (Clause); + Loc : constant Source_Ptr := Sloc (Clause); + Output : constant List_Id := Choices (Clause); + Last_Input : Node_Id; + Input : Node_Id; + New_Clause : Node_Id; + Next_Input : Node_Id; - -- Refined_State => (State_1 => (C1, C2)) - -- Depends => (<output> => State) - -- Refined_Depends => (<output> => C1) - -- or - -- Refined_Depends => (<output> => (C1, C2)) + begin + -- Normalization is performed only when the original clause has + -- more than one input. Multiple inputs appear as an aggregate. - if Nkind (Dep_Inputs) = N_Aggregate then - Dep_Input := First (Expressions (Dep_Inputs)); - while Present (Dep_Input) loop - if not Input_Match - (Dep_Input => Dep_Input, - Ref_Inputs => Ref_Inputs, - Post_Errors => Post_Errors) - then - Result := False; - end if; + if Nkind (Inputs) = N_Aggregate then + Last_Input := Last (Expressions (Inputs)); - Next (Dep_Input); - end loop; + -- Create a new clause for each input - Result := True; + Input := First (Expressions (Inputs)); + while Present (Input) loop + Next_Input := Next (Input); - -- Solitary input + -- Unhook the current input from the original input list + -- because it will be relocated to a new clause. - else - Result := - Input_Match - (Dep_Input => Dep_Inputs, - Ref_Inputs => Ref_Inputs, - Post_Errors => Post_Errors); - end if; + Remove (Input); - -- List all inputs that appear as extras + -- Special processing for the last input. At this point the + -- original aggregate has been stripped down to one element. + -- Replace the aggregate by the element itself. - Report_Extra_Inputs; + if Input = Last_Input then + Rewrite (Inputs, Input); - return Result; - end Inputs_Match; + -- Generate a clause of the form: + -- Output => Input - ------------------------- - -- Is_Self_Referential -- - ------------------------- + else + New_Clause := + Make_Component_Association (Loc, + Choices => New_Copy_List_Tree (Output), + Expression => Input); - function Is_Self_Referential (Item_Id : Entity_Id) return Boolean is - function Denotes_Item (N : Node_Id) return Boolean; - -- Determine whether an arbitrary node N denotes item Item_Id + -- The new clause contains replicated content that has + -- already been analyzed, mark the clause as analyzed. - ------------------ - -- Denotes_Item -- - ------------------ + Set_Analyzed (New_Clause); + Insert_After (Clause, New_Clause); + end if; - function Denotes_Item (N : Node_Id) return Boolean is - begin - return - Is_Entity_Name (N) - and then Present (Entity (N)) - and then Entity (N) = Item_Id; - end Denotes_Item; + Input := Next_Input; + end loop; + end if; + end Normalize_Inputs; -- Local variables - Clauses : constant Node_Id := - Get_Pragma_Arg - (First (Pragma_Argument_Associations (Depends))); - Clause : Node_Id; - Input : Node_Id; - Output : Node_Id; + Clause : Node_Id; - -- Start of processing for Is_Self_Referential + -- Start of processing for Normalize_Clauses begin - Clause := First (Component_Associations (Clauses)); + Clause := First (Clauses); while Present (Clause) loop - - -- Due to normalization, a dependence clause has exactly one - -- output even if the original clause had multiple outputs. - - Output := First (Choices (Clause)); - - -- Detect the following scenario: - -- - -- Item_Id => [(...,] Item_Id [, ...)] - - if Denotes_Item (Output) then - Input := Expression (Clause); - - -- Multiple inputs appear as an aggregate - - if Nkind (Input) = N_Aggregate then - Input := First (Expressions (Input)); - - if Denotes_Item (Input) then - return True; - end if; - - Next (Input); - - -- Solitary input - - elsif Denotes_Item (Input) then - return True; - end if; - end if; - + Normalize_Inputs (Clause); Next (Clause); end loop; - - return False; - end Is_Self_Referential; + end Normalize_Clauses; -------------------------- -- Report_Extra_Clauses -- @@ -22607,24 +22302,29 @@ package body Sem_Prag is if Nkind (Deps) = N_Null then SPARK_Msg_NE ("useless refinement, subprogram & does not depend on abstract " - & "state with visible refinement", - N, Spec_Id); + & "state with visible refinement", N, Spec_Id); return; end if; - -- Multiple dependency clauses appear as component associations of an - -- aggregate. - - pragma Assert (Nkind (Deps) = N_Aggregate); - Dependencies := Component_Associations (Deps); - -- Analyze Refined_Depends as if it behaved as a regular pragma Depends. -- This ensures that the categorization of all refined dependency items -- is consistent with their role. Analyze_Depends_In_Decl_Part (N); + -- Do not match dependencies against refinements if Refined_Depends is + -- illegal to avoid emitting misleading error. + if Serious_Errors_Detected = Errors then + + -- Multiple dependency clauses appear as component associations of an + -- aggregate. Note that the clauses are copied because the algorithm + -- modifies them and this should not be visible in Depends. + + pragma Assert (Nkind (Deps) = N_Aggregate); + Dependencies := New_Copy_List_Tree (Component_Associations (Deps)); + Normalize_Clauses (Dependencies); + if Nkind (Refs) = N_Null then Refinements := No_List; @@ -22633,33 +22333,24 @@ package body Sem_Prag is -- modifies them and this should not be visible in Refined_Depends. else pragma Assert (Nkind (Refs) = N_Aggregate); - Refinements := New_Copy_List (Component_Associations (Refs)); + Refinements := New_Copy_List_Tree (Component_Associations (Refs)); + Normalize_Clauses (Refinements); end if; - -- Inspect all the clauses of pragma Depends looking for a matching - -- clause in pragma Refined_Depends. The approach is to use the - -- sole output of a clause as a key. Output items are unique in a - -- dependence relation. Clause normalization also ensured that all - -- clauses have exactly one output. Depending on what the key is, one - -- or more refinement clauses may satisfy the dependency clause. Each - -- time a dependency clause is matched, its related refinement clause - -- is consumed. In the end, two things may happen: - - -- 1) A clause of pragma Depends was not matched in which case - -- Check_Dependency_Clause reports the error. - - -- 2) Refined_Depends has an extra clause in which case the error - -- is reported by Report_Extra_Clauses. + -- At this point the clauses of pragmas Depends and Refined_Depends + -- have been normalized into simple dependencies between one output + -- and one input. Examine all clauses of pragma Depends looking for + -- matching clauses in pragma Refined_Depends. Clause := First (Dependencies); while Present (Clause) loop Check_Dependency_Clause (Clause); Next (Clause); end loop; - end if; - if Serious_Errors_Detected = Errors then - Report_Extra_Clauses; + if Serious_Errors_Detected = Errors then + Report_Extra_Clauses; + end if; end if; end Analyze_Refined_Depends_In_Decl_Part; |