Skip to content

R
riscv-gcc-1
Commit 3b8481cb by Arnaud Charlet
Options

[multiple changes] 

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.

From-SVN: r212803
parent daff5ab7
Showing with 397 additions and 641 deletions
gcc/ada/ChangeLog
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> 2014-07-18 Robert Dewar <dewar@adacore.com>
* repinfo.ads: Add documentation on handling of back annotation * repinfo.ads: Add documentation on handling of back annotation
......
gcc/ada/exp_util.adb
...@@ -6667,13 +6667,18 @@ package body Exp_Util is ...@@ -6667,13 +6667,18 @@ package body Exp_Util is
-- When wrapping the statements of an iterator loop, check whether -- When wrapping the statements of an iterator loop, check whether
-- the loop requires secondary stack management and if so, propagate -- the loop requires secondary stack management and if so, propagate
-- the flag to the block. This way the secondary stack is marked and -- the appropriate flags to the block. This ensures that the cursor
-- released at each iteration of the loop. -- 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); Iter_Loop := Find_Enclosing_Iterator_Loop (Scop);
if Present (Iter_Loop) and then Uses_Sec_Stack (Iter_Loop) then if Present (Iter_Loop) then
Set_Uses_Sec_Stack (Block_Id); 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; end if;
return Block_Nod; return Block_Nod;
......
gcc/ada/g-memdum.adb
...@@ -46,8 +46,16 @@ package body GNAT.Memory_Dump is ...@@ -46,8 +46,16 @@ package body GNAT.Memory_Dump is
procedure Dump procedure Dump
(Addr : Address; (Addr : Address;
Count : Natural)
is
begin
Dump (Addr, Count, Prefix => Absolute_Address);
end Dump;
procedure Dump
(Addr : Address;
Count : Natural; Count : Natural;
Prefix : Prefix_Type := Absolute_Address) Prefix : Prefix_Type)
is is
Ctr : Natural := Count; Ctr : Natural := Count;
-- Count of bytes left to output -- Count of bytes left to output
......
gcc/ada/g-memdum.ads
...@@ -42,20 +42,36 @@ package GNAT.Memory_Dump is ...@@ -42,20 +42,36 @@ package GNAT.Memory_Dump is
procedure Dump procedure Dump
(Addr : System.Address; (Addr : System.Address;
Count : Natural; Count : Natural);
Prefix : Prefix_Type := Absolute_Address);
-- Dumps indicated number (Count) of bytes, starting at the address given -- 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 -- 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 -- 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 -- 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 -- or more lines in the following format, which is for the case of 32-bit
-- addresses (64-bit addresses are handled appropriately): -- addresses (64-bit addresses are handled appropriately):
--
-- 0234_3368: 66 67 68 . . . 73 74 75 "fghijklmnopqstuv" -- 0234_3368: 66 67 68 . . . 73 74 75 "fghijklmnopqstuv"
--
-- All but the last line have 16 bytes. A question mark is used in the -- All but the last line have 16 bytes. A question mark is used in the
-- string data to indicate a non-printable character. -- 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; end GNAT.Memory_Dump;
gcc/ada/i-cstrea.ads
...@@ -230,9 +230,9 @@ package Interfaces.C_Streams is ...@@ -230,9 +230,9 @@ package Interfaces.C_Streams is
procedure set_text_mode (handle : int); procedure set_text_mode (handle : int);
-- set_wide_text_mode is as set_text_mode but switches the translation to -- 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 -- 16-bit wide-character instead of 8-bit character. Again, this routine
-- has not effect if text_translation_required is false. On Windows this -- has no effect if text_translation_required is false. On Windows this
-- is used to have proper 16-bits wide string output on the console for -- is used to have proper 16-bit wide-string output on the console for
-- example. -- example.
procedure set_wide_text_mode (handle : int); procedure set_wide_text_mode (handle : int);
......
gcc/ada/sem_ch5.adb
...@@ -2885,6 +2885,12 @@ package body Sem_Ch5 is ...@@ -2885,6 +2885,12 @@ package body Sem_Ch5 is
Add_Block_Identifier (Block_Nod, Block_Id); 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 -- The expansion of iterator loops generates an iterator in order
-- to traverse the elements of a container: -- to traverse the elements of a container:
......
gcc/ada/sem_prag.adb
...@@ -1340,7 +1340,7 @@ package body Sem_Prag is ...@@ -1340,7 +1340,7 @@ package body Sem_Prag is
-- Flag Multiple should be set when Output comes from a list with -- Flag Multiple should be set when Output comes from a list with
-- multiple items. -- multiple items.
procedure Split_Multiple_Outputs; procedure Normalize_Outputs;
-- If Clause contains more than one output, split the clause into -- If Clause contains more than one output, split the clause into
-- multiple clauses with a single output. All new clauses are added -- multiple clauses with a single output. All new clauses are added
-- after Clause. -- after Clause.
...@@ -1530,20 +1530,18 @@ package body Sem_Prag is ...@@ -1530,20 +1530,18 @@ package body Sem_Prag is
end if; end if;
end Create_Or_Modify_Clause; 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); Inputs : constant Node_Id := Expression (Clause);
Loc : constant Source_Ptr := Sloc (Clause); Loc : constant Source_Ptr := Sloc (Clause);
Outputs : constant Node_Id := First (Choices (Clause)); Outputs : constant Node_Id := First (Choices (Clause));
Last_Output : Node_Id; Last_Output : Node_Id;
New_Clause : Node_Id;
Next_Output : Node_Id; Next_Output : Node_Id;
Output : Node_Id; Output : Node_Id;
Split : Node_Id;
-- Start of processing for Split_Multiple_Outputs
begin begin
-- Multiple outputs appear as an aggregate. Nothing to do when -- Multiple outputs appear as an aggregate. Nothing to do when
...@@ -1576,7 +1574,7 @@ package body Sem_Prag is ...@@ -1576,7 +1574,7 @@ package body Sem_Prag is
-- Generate a clause of the form: -- Generate a clause of the form:
-- (Output => Inputs) -- (Output => Inputs)
Split := New_Clause :=
Make_Component_Association (Loc, Make_Component_Association (Loc,
Choices => New_List (Output), Choices => New_List (Output),
Expression => New_Copy_Tree (Inputs)); Expression => New_Copy_Tree (Inputs));
...@@ -1585,14 +1583,14 @@ package body Sem_Prag is ...@@ -1585,14 +1583,14 @@ package body Sem_Prag is
-- already been analyzed. There is not need to reanalyze -- already been analyzed. There is not need to reanalyze
-- them. -- them.
Set_Analyzed (Split); Set_Analyzed (New_Clause);
Insert_After (Clause, Split); Insert_After (Clause, New_Clause);
end if; end if;
Output := Next_Output; Output := Next_Output;
end loop; end loop;
end if; end if;
end Split_Multiple_Outputs; end Normalize_Outputs;
-- Local variables -- Local variables
...@@ -1652,7 +1650,7 @@ package body Sem_Prag is ...@@ -1652,7 +1650,7 @@ package body Sem_Prag is
-- Split a clause with multiple outputs into multiple clauses with a -- Split a clause with multiple outputs into multiple clauses with a
-- single output. -- single output.
Split_Multiple_Outputs; Normalize_Outputs;
end Normalize_Clause; end Normalize_Clause;
-- Local variables -- Local variables
...@@ -21831,6 +21829,9 @@ package body Sem_Prag is ...@@ -21831,6 +21829,9 @@ package body Sem_Prag is
Depends : Node_Id; Depends : Node_Id;
-- The corresponding Depends pragma along with its clauses -- 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; Refinements : List_Id := No_List;
-- The clauses of pragma Refined_Depends -- The clauses of pragma Refined_Depends
...@@ -21838,706 +21839,400 @@ package body Sem_Prag is ...@@ -21838,706 +21839,400 @@ package body Sem_Prag is
-- The entity of the subprogram subject to pragma Refined_Depends -- The entity of the subprogram subject to pragma Refined_Depends
procedure Check_Dependency_Clause (Dep_Clause : Node_Id); procedure Check_Dependency_Clause (Dep_Clause : Node_Id);
-- Verify the legality of a single clause -- Try to match a single dependency clause Dep_Clause against one or
-- more refinement clauses found in list Refinements. Each successful
function Input_Match -- match eliminates at least one refinement clause from Refinements.
(Dep_Input : Node_Id;
Ref_Inputs : List_Id; procedure Normalize_Clauses (Clauses : List_Id);
Post_Errors : Boolean) return Boolean; -- Given a list of dependence or refinement clauses Clauses, normalize
-- Determine whether input Dep_Input matches one of inputs found in list -- each clause by creating multiple dependencies with exactly one input
-- Ref_Inputs. If flag Post_Errors is set, the routine reports missed or -- and one output.
-- 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.
procedure Report_Extra_Clauses; 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 -- -- Check_Dependency_Clause --
----------------------------- -----------------------------
procedure Check_Dependency_Clause (Dep_Clause : Node_Id) is procedure Check_Dependency_Clause (Dep_Clause : Node_Id) is
Dep_Output : constant Node_Id := First (Choices (Dep_Clause)); Dep_Input : constant Node_Id := Expression (Dep_Clause);
Dep_Id : Entity_Id; Dep_Output : constant Node_Id := First (Choices (Dep_Clause));
Matching_Clause : Node_Id := Empty;
Next_Ref_Clause : Node_Id; function Is_In_Out_State_Clause return Boolean;
Ref_Clause : Node_Id; -- Determine whether dependence clause Dep_Clause denotes an abstract
Ref_Id : Entity_Id; -- state that depends on itself (State => State).
Ref_Output : Node_Id;
procedure Match_Items
Has_Constituent : Boolean := False; (Dep_Item : Node_Id;
-- Flag set when the refinement output list contains at least one Ref_Item : Node_Id;
-- constituent of the state denoted by Dep_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 -- Is_In_Out_State_Clause --
-- null refinement. ----------------------------
Has_Refined_State : Boolean := False; function Is_In_Out_State_Clause return Boolean is
-- Flag set when the output of clause Dep_Clause is a state with Dep_Input_Id : Entity_Id;
-- visible refinement. Dep_Output_Id : Entity_Id;
begin begin
-- The analysis of pragma Depends should produce normalized clauses -- Detect the following clause:
-- with exactly one output. This is important because output items -- State => State
-- are unique in the whole dependence relation and can be used as
-- keys.
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 Dep_Input_Id := Available_View (Entity_Of (Dep_Input));
-- output of Dep_Clause against an output from the refinement clauses Dep_Output_Id := Available_View (Entity_Of (Dep_Output));
-- set.
Ref_Clause := First (Refinements); return
while Present (Ref_Clause) loop Ekind (Dep_Input_Id) = E_Abstract_State
Matching_Clause := Empty; 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 -- Match_Items --
-- in pragma Refined_Depends. -----------------
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 begin
-- normalized clauses with exactly one output. -- Assume that the two items do not match
Ref_Output := First (Choices (Ref_Clause)); Matched := False;
pragma Assert (No (Next (Ref_Output)));
-- Two null output lists match if their inputs match -- A null matches null or Empty (special case)
if Nkind (Dep_Output) = N_Null if Nkind (Dep_Item) = N_Null
and then Nkind (Ref_Output) = N_Null and then (No (Ref_Item) or else Nkind (Ref_Item) = N_Null)
then then
Matching_Clause := Ref_Clause; Matched := True;
exit;
-- Two function 'Result attributes match if their inputs match. -- Attribute 'Result matches attribute 'Result
-- Note that there is no need to compare the two prefixes because
-- the attributes cannot denote anything but the related function.
elsif Is_Attribute_Result (Dep_Output) elsif Is_Attribute_Result (Dep_Item)
and then Is_Attribute_Result (Ref_Output) and then Is_Attribute_Result (Dep_Item)
then then
Matching_Clause := Ref_Clause; Matched := True;
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));
if Ekind (Dep_Id) = E_Abstract_State then -- Abstract states, formal parameters and variables
-- A state with a null refinement matches either a null elsif Is_Entity_Name (Dep_Item) then
-- output list or nothing at all (no clause):
-- 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) if Ekind (Dep_Item_Id) = E_Abstract_State then
-- Refined_Depends => null -- OK
-- Null output list -- An abstract state with visible null refinement matches
-- null or Empty (special case).
-- Depends => (State => <input>) if Has_Null_Refinement (Dep_Item_Id)
-- Refined_Depends => (null => <input>) -- OK and then (No (Ref_Item) or else Nkind (Ref_Item) = N_Null)
then
if Has_Null_Refinement (Dep_Id) then Matched := True;
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:
-- Refined_State => (State => (C1, C2)) -- An abstract state with visible non-null refinement
-- Depends => (State => <input>) -- matches one of its constituents.
-- Refined_Depends => (C1 => <input>)
elsif Is_Entity_Name (Ref_Output) then elsif Has_Non_Null_Refinement (Dep_Item_Id) then
Ref_Id := Entity_Of (Ref_Output); if Is_Entity_Name (Ref_Item) then
Ref_Item_Id := Entity_Of (Ref_Item);
if Ekind_In (Ref_Id, E_Abstract_State, E_Variable) if Ekind_In (Ref_Item_Id, E_Abstract_State, E_Variable)
and then Present (Encapsulating_State (Ref_Id)) and then Present (Encapsulating_State (Ref_Item_Id))
and then Encapsulating_State (Ref_Id) = Dep_Id and then Encapsulating_State (Ref_Item_Id) =
and then Inputs_Match Dep_Item_Id
(Dep_Clause => Dep_Clause,
Ref_Clause => Ref_Clause,
Post_Errors => False)
then then
Has_Constituent := True; -- Record the successfully refined state
-- Note that the search continues after the clause if not Contains (Refined_States, Dep_Item_Id) then
-- is removed from the pool of candidates because Add_Item (Dep_Item_Id, Refined_States);
-- it may have been normalized into multiple simple end if;
-- clauses.
Remove (Ref_Clause); Matched := True;
end if; end if;
end if; end if;
-- The abstract view of a state matches is corresponding -- An abstract state without a visible refinement matches
-- non-abstract view: -- itself.
-- Depends => (Lim_Pack.State => <input>)
-- Refined_Depends => (State => <input>)
elsif Is_Entity_Name (Ref_Output) elsif Is_Entity_Name (Ref_Item)
and then Entity_Of (Ref_Output) = Dep_Id and then Entity_Of (Ref_Item) = Dep_Item_Id
then then
Matching_Clause := Ref_Clause; Matched := True;
exit;
end if; 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) elsif Is_Entity_Name (Ref_Item)
and then Entity_Of (Ref_Output) = Dep_Id and then Entity_Of (Ref_Item) = Dep_Item_Id
then then
Matching_Clause := Ref_Clause; Matched := True;
exit;
end if; end if;
end if; end if;
end Match_Items;
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;
-- Local variables -- Local variables
Dep_Id : Node_Id; Clause_Matched : Boolean := False;
Next_Ref_Input : Node_Id; Dummy : Boolean := False;
Ref_Id : Entity_Id; Inputs_Match : Boolean;
Ref_Input : Node_Id; Next_Ref_Clause : Node_Id;
Outputs_Match : Boolean;
Has_Constituent : Boolean := False; Ref_Clause : Node_Id;
-- Flag set when the refinement input list contains at least one Ref_Input : Node_Id;
-- constituent of the state denoted by Dep_Id. Ref_Output : Node_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.
-- Start of processing for Input_Match -- Start of processing for Check_Dependency_Clause
begin begin
-- Match a null input with another null input -- Examine all refinement clauses and compare them against the
-- dependence clause.
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
if Nkind (Ref_Input) = N_Null then Ref_Clause := First (Refinements);
Remove (Ref_Input); while Present (Ref_Clause) loop
end if; Next_Ref_Clause := Next (Ref_Clause);
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.
Has_Constituent := True; -- Obtain the attributes of the current refinement clause
Remove (Ref_Input);
-- Ref_Input is an entity name Ref_Input := Expression (Ref_Clause);
Ref_Output := First (Choices (Ref_Clause));
elsif Is_Entity_Name (Ref_Input) then -- The current refinement clause matches the dependence clause
Ref_Id := Entity_Of (Ref_Input); -- 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 -- Depends Dep_Output => Dep_Input
-- constituent of the state. Remove the input from the -- ^ ^
-- pool of candidates. Note that the search continues -- match ? match ?
-- because the state may be represented by multiple -- v v
-- constituents. -- Refined_Depends Ref_Output => Ref_Input
if Ekind_In (Ref_Id, E_Abstract_State, Match_Items
E_Variable) (Dep_Item => Dep_Input,
and then Present (Encapsulating_State (Ref_Id)) Ref_Item => Ref_Input,
and then Encapsulating_State (Ref_Id) = Dep_Id Matched => Inputs_Match);
then
Has_Constituent := True;
Remove (Ref_Input);
end if;
end if;
-- The abstract view of a state matches its corresponding Match_Items
-- non-abstract view: (Dep_Item => Dep_Output,
Ref_Item => Ref_Output,
Matched => Outputs_Match);
-- Depends => (<output> => Lim_Pack.State) -- An In_Out state clause may be matched against a refinement with
-- Refined_Depends => (<output> => State) -- 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) if Is_In_Out_State_Clause then
and then Entity_Of (Ref_Input) = Dep_Id
then
Remove (Ref_Input);
return True;
end if;
-- Formal parameters and variables are matched on entities. If -- Depends => (State => State)
-- this is the case, remove the input from the candidate list. -- Refined_Depends => (null => Constit) -- OK
elsif Is_Entity_Name (Ref_Input) if Inputs_Match
and then Entity_Of (Ref_Input) = Dep_Id and then not Outputs_Match
and then Nkind (Ref_Output) = N_Null
then then
Remove (Ref_Input); Outputs_Match := True;
return True;
end if; end if;
Ref_Input := Next_Ref_Input; -- Depends => (State => State)
end loop; -- Refined_Depends => (Constit => null) -- OK
-- When a state with a null refinement appears as the last input, if not Inputs_Match
-- it matches nothing: and then Outputs_Match
and then Nkind (Ref_Input) = N_Null
-- Refined_State => (State => null) then
-- Depends => (<output> => (Input, State)) Inputs_Match := True;
-- Refined_Depends => (<output> => Input) -- OK end if;
if Ekind (Dep_Id) = E_Abstract_State
and then Has_Null_Refinement (Dep_Id)
and then No (Ref_Input)
then
Has_Null_State := 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 current refinement clause is legally constructed following
-- the refinement clause, emit an error. -- 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 if Inputs_Match and then Outputs_Match then
Match_Error Clause_Matched := True;
("input cannot be matched in corresponding refinement clause", Remove (Ref_Clause);
Dep_Input);
if Has_Refined_State then
Match_Error
("\check the use of constituents in dependence refinement",
Dep_Input);
end if; end if;
return False; Ref_Clause := Next_Ref_Clause;
end if; end loop;
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
procedure Report_Extra_Inputs; -- Depending on the order or composition of refinement clauses, an
-- Emit errors for all extra inputs that appear in Ref_Inputs -- In_Out state clause may not be directly refinable.
------------------------- -- Depends => ((Output, State) => (Input, State))
-- Report_Extra_Inputs -- -- Refined_State => (State => (Constit_1, Constit_2))
------------------------- -- Refined_Depends => (Constit_1 => Input, Output => Constit_2)
procedure Report_Extra_Inputs is -- Matching normalized clause (State => State) fails because there is
Input : Node_Id; -- 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 not Clause_Matched
if Present (Ref_Inputs) and then Post_Errors then and then Is_In_Out_State_Clause
Input := First (Ref_Inputs); and then Contains
while Present (Input) loop (Refined_States, Available_View (Entity_Of (Dep_Input)))
SPARK_Msg_N then
("unmatched or extra input in refinement clause", Input); Clause_Matched := True;
end if;
Next (Input);
end loop;
end if;
end Report_Extra_Inputs;
-- 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); -- Depends => (State => null)
Inputs : constant Node_Id := Expression (Ref_Clause); -- Refined_State => (State => null)
Dep_Input : Node_Id; -- Refined_Depends => null -- OK
Result : Boolean;
-- Start of processing for Inputs_Match if not Clause_Matched then
Match_Items
(Dep_Item => Dep_Input,
Ref_Item => Empty,
Matched => Inputs_Match);
begin Match_Items
-- Construct a list of all refinement inputs. Note that the input (Dep_Item => Dep_Output,
-- list is copied because the algorithm modifies its contents and Ref_Item => Empty,
-- this should not be visible in Refined_Depends. The same applies Matched => Outputs_Match);
-- for a solitary input.
if Nkind (Inputs) = N_Aggregate then Clause_Matched := Inputs_Match and Outputs_Match;
Ref_Inputs := New_Copy_List (Expressions (Inputs));
else
Ref_Inputs := New_List (New_Copy (Inputs));
end if; end if;
-- Depending on whether the original dependency clause mentions -- If the contents of Refined_Depends are legal, then the current
-- states with visible refinement, the corresponding refinement -- dependence clause should be satisfied either by an explicit match
-- clause may differ greatly in structure and contents: -- 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) -- Normalize_Clauses --
-- Refined_Depends => (<output> => null) -----------------------
-- Depends => (<output> => (State, Input)) procedure Normalize_Clauses (Clauses : List_Id) is
-- Refined_Depends => (<output> => Input) 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)) begin
-- Depends => (<output> => State) -- Normalization is performed only when the original clause has
-- Refined_Depends => (<output> => C1) -- more than one input. Multiple inputs appear as an aggregate.
-- or
-- Refined_Depends => (<output> => (C1, C2))
if Nkind (Dep_Inputs) = N_Aggregate then if Nkind (Inputs) = N_Aggregate then
Dep_Input := First (Expressions (Dep_Inputs)); Last_Input := Last (Expressions (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;
Next (Dep_Input); -- Create a new clause for each input
end loop;
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 Remove (Input);
Result :=
Input_Match
(Dep_Input => Dep_Inputs,
Ref_Inputs => Ref_Inputs,
Post_Errors => Post_Errors);
end if;
-- 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; -- Generate a clause of the form:
end Inputs_Match; -- Output => Input
------------------------- else
-- Is_Self_Referential -- 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 -- The new clause contains replicated content that has
function Denotes_Item (N : Node_Id) return Boolean; -- already been analyzed, mark the clause as analyzed.
-- Determine whether an arbitrary node N denotes item Item_Id
------------------ Set_Analyzed (New_Clause);
-- Denotes_Item -- Insert_After (Clause, New_Clause);
------------------ end if;
function Denotes_Item (N : Node_Id) return Boolean is Input := Next_Input;
begin end loop;
return end if;
Is_Entity_Name (N) end Normalize_Inputs;
and then Present (Entity (N))
and then Entity (N) = Item_Id;
end Denotes_Item;
-- Local variables -- Local variables
Clauses : constant Node_Id := Clause : Node_Id;
Get_Pragma_Arg
(First (Pragma_Argument_Associations (Depends)));
Clause : Node_Id;
Input : Node_Id;
Output : Node_Id;
-- Start of processing for Is_Self_Referential -- Start of processing for Normalize_Clauses
begin begin
Clause := First (Component_Associations (Clauses)); Clause := First (Clauses);
while Present (Clause) loop while Present (Clause) loop
Normalize_Inputs (Clause);
-- 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;
Next (Clause); Next (Clause);
end loop; end loop;
end Normalize_Clauses;
return False;
end Is_Self_Referential;
-------------------------- --------------------------
-- Report_Extra_Clauses -- -- Report_Extra_Clauses --
...@@ -22607,24 +22302,29 @@ package body Sem_Prag is ...@@ -22607,24 +22302,29 @@ package body Sem_Prag is
if Nkind (Deps) = N_Null then if Nkind (Deps) = N_Null then
SPARK_Msg_NE SPARK_Msg_NE
("useless refinement, subprogram & does not depend on abstract " ("useless refinement, subprogram & does not depend on abstract "
& "state with visible refinement", & "state with visible refinement", N, Spec_Id);
N, Spec_Id);
return; return;
end if; 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. -- Analyze Refined_Depends as if it behaved as a regular pragma Depends.
-- This ensures that the categorization of all refined dependency items -- This ensures that the categorization of all refined dependency items
-- is consistent with their role. -- is consistent with their role.
Analyze_Depends_In_Decl_Part (N); 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 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 if Nkind (Refs) = N_Null then
Refinements := No_List; Refinements := No_List;
...@@ -22633,33 +22333,24 @@ package body Sem_Prag is ...@@ -22633,33 +22333,24 @@ package body Sem_Prag is
-- modifies them and this should not be visible in Refined_Depends. -- modifies them and this should not be visible in Refined_Depends.
else pragma Assert (Nkind (Refs) = N_Aggregate); 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; end if;
-- Inspect all the clauses of pragma Depends looking for a matching -- At this point the clauses of pragmas Depends and Refined_Depends
-- clause in pragma Refined_Depends. The approach is to use the -- have been normalized into simple dependencies between one output
-- sole output of a clause as a key. Output items are unique in a -- and one input. Examine all clauses of pragma Depends looking for
-- dependence relation. Clause normalization also ensured that all -- matching clauses in pragma Refined_Depends.
-- 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.
Clause := First (Dependencies); Clause := First (Dependencies);
while Present (Clause) loop while Present (Clause) loop
Check_Dependency_Clause (Clause); Check_Dependency_Clause (Clause);
Next (Clause); Next (Clause);
end loop; end loop;
end if;
if Serious_Errors_Detected = Errors then if Serious_Errors_Detected = Errors then
Report_Extra_Clauses; Report_Extra_Clauses;
end if;
end if; end if;
end Analyze_Refined_Depends_In_Decl_Part; end Analyze_Refined_Depends_In_Decl_Part;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment