===================================================================
@@ -2349,6 +2349,7 @@
| N_With_Clause
| N_Use_Type_Clause
| N_Validate_Unchecked_Conversion
+ | N_Variable_Reference_Marker
=>
null;
===================================================================
@@ -612,10 +612,12 @@
when N_With_Clause =>
Analyze_With_Clause (N);
- -- A call to analyze a call marker is ignored because the node does
- -- not have any static and run-time semantics.
+ -- A call to analyze a marker is ignored because the node does not
+ -- have any static and run-time semantics.
- when N_Call_Marker =>
+ when N_Call_Marker
+ | N_Variable_Reference_Marker
+ =>
null;
-- A call to analyze the Empty node is an error, but most likely it
===================================================================
@@ -3459,6 +3459,25 @@
Sprint_Node (Target_Type (Node));
Write_Str (");");
+ when N_Variable_Reference_Marker =>
+ null;
+
+ -- Enable the following code for debugging purposes only
+
+ -- if Is_Read (Node) and then Is_Write (Node) then
+ -- Write_Indent_Str ("rw#");
+
+ -- elsif Is_Read (Node) then
+ -- Write_Indent_Str ("r#");
+
+ -- else
+ -- pragma Assert (Is_Write (Node));
+ -- Write_Indent_Str ("w#");
+ -- end if;
+
+ -- Write_Id (Target (Node));
+ -- Write_Char ('#');
+
when N_Variant =>
Write_Indent_Str_Sloc ("when ");
Sprint_Bar_List (Discrete_Choices (Node));
===================================================================
@@ -7255,9 +7255,11 @@
null;
end if;
- -- Special case: a call marker
+ -- Special case: a marker
- when N_Call_Marker =>
+ when N_Call_Marker
+ | N_Variable_Reference_Marker
+ =>
if Is_List_Member (P) then
Insert_List_Before_And_Analyze (P, Ins_Actions);
return;
===================================================================
@@ -14865,10 +14865,6 @@
function Within_Check (Nod : Node_Id) return Boolean;
-- Determine whether an arbitrary node appears in a check node
- function Within_Subprogram_Call (Nod : Node_Id) return Boolean;
- -- Determine whether an arbitrary node appears in an entry, function, or
- -- procedure call.
-
function Within_Volatile_Function (Id : Entity_Id) return Boolean;
-- Determine whether an arbitrary entity appears in a volatile function
@@ -14931,36 +14927,6 @@
return False;
end Within_Check;
- ----------------------------
- -- Within_Subprogram_Call --
- ----------------------------
-
- function Within_Subprogram_Call (Nod : Node_Id) return Boolean is
- Par : Node_Id;
-
- begin
- -- Climb the parent chain looking for a function or procedure call
-
- Par := Nod;
- while Present (Par) loop
- if Nkind_In (Par, N_Entry_Call_Statement,
- N_Function_Call,
- N_Procedure_Call_Statement)
- then
- return True;
-
- -- Prevent the search from going too far
-
- elsif Is_Body_Or_Package_Declaration (Par) then
- exit;
- end if;
-
- Par := Parent (Par);
- end loop;
-
- return False;
- end Within_Subprogram_Call;
-
------------------------------
-- Within_Volatile_Function --
------------------------------
@@ -24241,6 +24207,36 @@
return Scope_Within_Or_Same (Scope (E), S);
end Within_Scope;
+ ----------------------------
+ -- Within_Subprogram_Call --
+ ----------------------------
+
+ function Within_Subprogram_Call (N : Node_Id) return Boolean is
+ Par : Node_Id;
+
+ begin
+ -- Climb the parent chain looking for a function or procedure call
+
+ Par := N;
+ while Present (Par) loop
+ if Nkind_In (Par, N_Entry_Call_Statement,
+ N_Function_Call,
+ N_Procedure_Call_Statement)
+ then
+ return True;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
+ return False;
+ end Within_Subprogram_Call;
+
----------------
-- Wrong_Type --
----------------
===================================================================
@@ -2735,6 +2735,10 @@
function Within_Scope (E : Entity_Id; S : Entity_Id) return Boolean;
-- Returns True if entity E is declared within scope S
+ function Within_Subprogram_Call (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N appears in an entry, function, or
+ -- procedure call.
+
procedure Wrong_Type (Expr : Node_Id; Expected_Type : Entity_Id);
-- Output error message for incorrectly typed expression. Expr is the node
-- for the incorrectly typed construct (Etype (Expr) is the type found),
===================================================================
@@ -3744,6 +3744,21 @@
and then Is_Entity_Name (A)
and then Comes_From_Source (A)
then
+ -- Annotate the tree by creating a variable reference marker when
+ -- the actual denotes a variable reference, in case the reference
+ -- is folded or optimized away. The variable reference marker is
+ -- automatically saved for later examination by the ABE Processing
+ -- phase. The status of the reference is set as follows:
+
+ -- status mode
+ -- read IN, IN OUT
+ -- write IN OUT, OUT
+
+ Build_Variable_Reference_Marker
+ (N => A,
+ Read => Ekind (F) /= E_Out_Parameter,
+ Write => Ekind (F) /= E_In_Parameter);
+
Orig_A := Entity (A);
if Present (Orig_A) then
===================================================================
@@ -2090,6 +2090,14 @@
return Flag4 (N);
end Is_Qualified_Universal_Literal;
+ function Is_Read
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Variable_Reference_Marker);
+ return Flag1 (N);
+ end Is_Read;
+
function Is_Recorded_Scenario
(N : Node_Id) return Boolean is
begin
@@ -2179,6 +2187,14 @@
return Flag5 (N);
end Is_Task_Master;
+ function Is_Write
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Variable_Reference_Marker);
+ return Flag2 (N);
+ end Is_Write;
+
function Iteration_Scheme
(N : Node_Id) return Node_Id is
begin
@@ -3277,7 +3293,8 @@
(N : Node_Id) return Entity_Id is
begin
pragma Assert (False
- or else NT (N).Nkind = N_Call_Marker);
+ or else NT (N).Nkind = N_Call_Marker
+ or else NT (N).Nkind = N_Variable_Reference_Marker);
return Node1 (N);
end Target;
@@ -5512,6 +5529,14 @@
Set_Flag4 (N, Val);
end Set_Is_Qualified_Universal_Literal;
+ procedure Set_Is_Read
+ (N : Node_Id; Val : Boolean := True) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Variable_Reference_Marker);
+ Set_Flag1 (N, Val);
+ end Set_Is_Read;
+
procedure Set_Is_Recorded_Scenario
(N : Node_Id; Val : Boolean := True) is
begin
@@ -5601,6 +5626,14 @@
Set_Flag5 (N, Val);
end Set_Is_Task_Master;
+ procedure Set_Is_Write
+ (N : Node_Id; Val : Boolean := True) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Variable_Reference_Marker);
+ Set_Flag2 (N, Val);
+ end Set_Is_Write;
+
procedure Set_Iteration_Scheme
(N : Node_Id; Val : Node_Id) is
begin
@@ -6699,7 +6732,8 @@
(N : Node_Id; Val : Entity_Id) is
begin
pragma Assert (False
- or else NT (N).Nkind = N_Call_Marker);
+ or else NT (N).Nkind = N_Call_Marker
+ or else NT (N).Nkind = N_Variable_Reference_Marker);
Set_Node1 (N, Val); -- semantic field, no parent set
end Set_Target;
===================================================================
@@ -1863,6 +1863,10 @@
-- the resolution of accidental overloading of binary or unary operators
-- which may occur in instances.
+ -- Is_Read (Flag1-Sem)
+ -- Present in variable reference markers. Set when the original variable
+ -- reference constitues a read of the variable.
+
-- Is_Recorded_Scenario (Flag6-Sem)
-- Present in call marker and instantiation nodes. Set when the scenario
-- was saved by the ABE Recording phase. This flag aids the ABE machinery
@@ -1916,6 +1920,10 @@
-- indicate that the construct is a task master (i.e. has declared tasks
-- or declares an access to a task type).
+ -- Is_Write (Flag2-Sem)
+ -- Present in variable reference markers. Set when the original variable
+ -- reference constitues a write of the variable.
+
-- Itype (Node1-Sem)
-- Used in N_Itype_Reference node to reference an itype for which it is
-- important to ensure that it is defined. See description of this node
@@ -2318,8 +2326,9 @@
-- only execute if invalid values are present).
-- Target (Node1-Sem)
- -- Present in call marker nodes. References the entity of the entry,
- -- operator, or subprogram invoked by the related call or requeue.
+ -- Present in call and variable reference marker nodes. References the
+ -- entity of the original entity, operator, or subprogram being invoked,
+ -- or the original variable being read or written.
-- Target_Type (Node2-Sem)
-- Used in an N_Validate_Unchecked_Conversion node to point to the target
@@ -8455,6 +8464,37 @@
-- Note: in the case where a debug source file is generated, the Sloc
-- for this node points to the VALIDATE keyword in the file output.
+ -------------------------------
+ -- Variable_Reference_Marker --
+ -------------------------------
+
+ -- This node is created during the analysis of direct or expanded names,
+ -- and the resolution of entry and subprogram calls. It performs several
+ -- functions:
+
+ -- * Variable reference markers provide a uniform model for handling
+ -- variable references by the ABE mechanism, regardless of whether
+ -- expansion took place.
+
+ -- * The variable reference marker captures the entity of the variable
+ -- being read or written.
+
+ -- * The variable reference markers aid the ABE Processing phase by
+ -- signaling the presence of a call in case the original variable
+ -- reference was transformed by expansion.
+
+ -- Sprint syntax: r#target# -- for a read
+ -- rw#target# -- for a read/write
+ -- w#target# -- for a write
+
+ -- The Sprint syntax shown above is not enabled by default
+
+ -- N_Variable_Reference_Marker
+ -- Sloc points to Sloc of original variable reference
+ -- Target (Node1-Sem)
+ -- Is_Read (Flag1-Sem)
+ -- Is_Write (Flag2-Sem)
+
-----------
-- Empty --
-----------
@@ -8877,6 +8917,7 @@
N_Triggering_Alternative,
N_Use_Type_Clause,
N_Validate_Unchecked_Conversion,
+ N_Variable_Reference_Marker,
N_Variant,
N_Variant_Part,
N_With_Clause,
@@ -9733,6 +9774,9 @@
function Is_Qualified_Universal_Literal
(N : Node_Id) return Boolean; -- Flag4
+ function Is_Read
+ (N : Node_Id) return Boolean; -- Flag1
+
function Is_Recorded_Scenario
(N : Node_Id) return Boolean; -- Flag6
@@ -9760,6 +9804,9 @@
function Is_Task_Master
(N : Node_Id) return Boolean; -- Flag5
+ function Is_Write
+ (N : Node_Id) return Boolean; -- Flag2
+
function Iteration_Scheme
(N : Node_Id) return Node_Id; -- Node2
@@ -10822,6 +10869,9 @@
procedure Set_Is_Qualified_Universal_Literal
(N : Node_Id; Val : Boolean := True); -- Flag4
+ procedure Set_Is_Read
+ (N : Node_Id; Val : Boolean := True); -- Flag1
+
procedure Set_Is_Recorded_Scenario
(N : Node_Id; Val : Boolean := True); -- Flag6
@@ -10849,6 +10899,9 @@
procedure Set_Is_Task_Master
(N : Node_Id; Val : Boolean := True); -- Flag5
+ procedure Set_Is_Write
+ (N : Node_Id; Val : Boolean := True); -- Flag2
+
procedure Set_Iteration_Scheme
(N : Node_Id; Val : Node_Id); -- Node2
@@ -13023,6 +13076,13 @@
4 => False, -- unused
5 => False), -- unused
+ N_Variable_Reference_Marker =>
+ (1 => False, -- Target (Node1-Sem)
+ 2 => False, -- unused
+ 3 => False, -- unused
+ 4 => False, -- unused
+ 5 => False), -- unused
+
-- Entries for Empty, Error and Unused. Even thought these have a Chars
-- field for debugging purposes, they are not really syntactic fields, so
-- we mark all fields as unused.
@@ -13276,6 +13336,7 @@
pragma Inline (Is_Prefixed_Call);
pragma Inline (Is_Protected_Subprogram_Body);
pragma Inline (Is_Qualified_Universal_Literal);
+ pragma Inline (Is_Read);
pragma Inline (Is_Recorded_Scenario);
pragma Inline (Is_Source_Call);
pragma Inline (Is_SPARK_Mode_On_Node);
@@ -13285,6 +13346,7 @@
pragma Inline (Is_Task_Allocation_Block);
pragma Inline (Is_Task_Body_Procedure);
pragma Inline (Is_Task_Master);
+ pragma Inline (Is_Write);
pragma Inline (Iteration_Scheme);
pragma Inline (Itype);
pragma Inline (Kill_Range_Check);
@@ -13634,6 +13696,7 @@
pragma Inline (Set_Is_Prefixed_Call);
pragma Inline (Set_Is_Protected_Subprogram_Body);
pragma Inline (Set_Is_Qualified_Universal_Literal);
+ pragma Inline (Set_Is_Read);
pragma Inline (Set_Is_Recorded_Scenario);
pragma Inline (Set_Is_Source_Call);
pragma Inline (Set_Is_SPARK_Mode_On_Node);
@@ -13643,6 +13706,7 @@
pragma Inline (Set_Is_Task_Allocation_Block);
pragma Inline (Set_Is_Task_Body_Procedure);
pragma Inline (Set_Is_Task_Master);
+ pragma Inline (Set_Is_Write);
pragma Inline (Set_Iteration_Scheme);
pragma Inline (Set_Iterator_Specification);
pragma Inline (Set_Itype);
===================================================================
@@ -5358,6 +5358,8 @@
-- Local variables
+ Is_Assignment_LHS : constant Boolean := Is_LHS (N) = Yes;
+
Nested_Inst : Entity_Id := Empty;
-- The entity of a nested instance which appears within Inst (if any)
@@ -5895,9 +5897,20 @@
<<Done>>
Check_Restriction_No_Use_Of_Entity (N);
- -- Save the scenario for later examination by the ABE Processing phase
+ -- Annotate the tree by creating a variable reference marker in case the
+ -- original variable reference is folded or optimized away. The variable
+ -- reference marker is automatically saved for later examination by the
+ -- ABE Processing phase. Variable references which act as actuals in a
+ -- call require special processing and are left to Resolve_Actuals. The
+ -- reference is a write when it appears on the left hand side of an
+ -- assignment.
- Record_Elaboration_Scenario (N);
+ if not Within_Subprogram_Call (N) then
+ Build_Variable_Reference_Marker
+ (N => N,
+ Read => not Is_Assignment_LHS,
+ Write => Is_Assignment_LHS);
+ end if;
end Find_Direct_Name;
------------------------
@@ -5969,8 +5982,10 @@
-- Local variables
- Selector : constant Node_Id := Selector_Name (N);
- Candidate : Entity_Id := Empty;
+ Is_Assignment_LHS : constant Boolean := Is_LHS (N) = Yes;
+ Selector : constant Node_Id := Selector_Name (N);
+
+ Candidate : Entity_Id := Empty;
P_Name : Entity_Id;
Id : Entity_Id;
@@ -6529,9 +6544,20 @@
Check_Restriction_No_Use_Of_Entity (N);
- -- Save the scenario for later examination by the ABE Processing phase
+ -- Annotate the tree by creating a variable reference marker in case the
+ -- original variable reference is folded or optimized away. The variable
+ -- reference marker is automatically saved for later examination by the
+ -- ABE Processing phase. Variable references which act as actuals in a
+ -- call require special processing and are left to Resolve_Actuals. The
+ -- reference is a write when it appears on the left hand side of an
+ -- assignment.
- Record_Elaboration_Scenario (N);
+ if not Within_Subprogram_Call (N) then
+ Build_Variable_Reference_Marker
+ (N => N,
+ Read => not Is_Assignment_LHS,
+ Write => Is_Assignment_LHS);
+ end if;
end Find_Expanded_Name;
--------------------
===================================================================
@@ -6727,8 +6727,11 @@
declare
New_Id : constant Entity_Id := Defining_Identifier (N);
Next_Temp : constant Entity_Id := Next_Entity (New_Id);
- S_Flag : constant Boolean :=
+ Save_CFS : constant Boolean :=
Comes_From_Source (Def_Id);
+ Save_SP : constant Node_Id := SPARK_Pragma (Def_Id);
+ Save_SPI : constant Boolean :=
+ SPARK_Pragma_Inherited (Def_Id);
begin
Set_Next_Entity (New_Id, Next_Entity (Def_Id));
@@ -6740,8 +6743,20 @@
Set_Sloc (Defining_Identifier (N), Sloc (Def_Id));
Set_Comes_From_Source (Def_Id, False);
+
+ -- ??? This is extremely dangerous!!! Exchanging entities
+ -- is very low level, and as a result it resets flags and
+ -- fields which belong to the original Def_Id. Several of
+ -- these attributes are saved and restored, but there may
+ -- be many more that need to be preserverd.
+
Exchange_Entities (Defining_Identifier (N), Def_Id);
- Set_Comes_From_Source (Def_Id, S_Flag);
+
+ -- Restore clobbered attributes
+
+ Set_Comes_From_Source (Def_Id, Save_CFS);
+ Set_SPARK_Pragma (Def_Id, Save_SP);
+ Set_SPARK_Pragma_Inherited (Def_Id, Save_SPI);
end;
end;
end if;
===================================================================
@@ -293,7 +293,7 @@
-- | | |
-- | +--> Process_Variable_Assignment |
-- | | |
- -- | +--> Process_Variable_Read |
+ -- | +--> Process_Variable_Reference |
-- | |
-- +------------------------- Processing phase -------------------------+
@@ -683,10 +683,6 @@
-- variable.
type Variable_Attributes is record
- SPARK_Mode_On : Boolean;
- -- This flag is set when the variable appears in a region subject to
- -- pragma SPARK_Mode with value On, or starts one such region.
-
Unit_Id : Entity_Id;
-- This attribute denotes the entity of the compilation unit where the
-- variable resides.
@@ -965,16 +961,16 @@
-- information message, otherwise it emits an error. If flag In_SPARK
-- is set, then string " in SPARK" is added to the end of the message.
- procedure Info_Variable_Read
+ procedure Info_Variable_Reference
(Ref : Node_Id;
Var_Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean);
- pragma Inline (Info_Variable_Read);
- -- Output information concerning reference Ref which reads variable Var_Id.
- -- If flag Info_Msg is set, the routine emits an information message,
- -- otherwise it emits an error. If flag In_SPARK is set, then string " in
- -- SPARK" is added to the end of the message.
+ pragma Inline (Info_Variable_Reference);
+ -- Output information concerning reference Ref which mentions variable
+ -- Var_Id. If flag Info_Msg is set, the routine emits an information
+ -- message, otherwise it emits an error. If flag In_SPARK is set, then
+ -- string " in SPARK" is added to the end of the message.
function Insertion_Node (N : Node_Id; Ins_Nod : Node_Id) return Node_Id;
pragma Inline (Insertion_Node);
@@ -1166,10 +1162,10 @@
-- Determine whether arbitrary node N denotes a suitable assignment for ABE
-- processing.
- function Is_Suitable_Variable_Read (N : Node_Id) return Boolean;
- pragma Inline (Is_Suitable_Variable_Read);
- -- Determine whether arbitrary node N is a suitable variable read for ABE
- -- processing.
+ function Is_Suitable_Variable_Reference (N : Node_Id) return Boolean;
+ pragma Inline (Is_Suitable_Variable_Reference);
+ -- Determine whether arbitrary node N is a suitable variable reference for
+ -- ABE processing.
function Is_Task_Entry (Id : Entity_Id) return Boolean;
pragma Inline (Is_Task_Entry);
@@ -1418,10 +1414,17 @@
-- Perform ABE checks and diagnostics for assignment statement Asmt that
-- updates the value of variable Var_Id using the SPARK rules.
- procedure Process_Variable_Read (Ref : Node_Id);
- -- Perform ABE checks and diagnostics for reference Ref that reads a
- -- variable.
+ procedure Process_Variable_Reference (Ref : Node_Id);
+ -- Top level dispatcher for processing of variable references. Perform ABE
+ -- checks and diagnostics for variable reference Ref.
+ procedure Process_Variable_Reference_Read
+ (Ref : Node_Id;
+ Var_Id : Entity_Id;
+ Attrs : Variable_Attributes);
+ -- Perform ABE checks and diagnostics for reference Ref described by its
+ -- attributes Attrs, that reads variable Var_Id.
+
procedure Push_Active_Scenario (N : Node_Id);
pragma Inline (Push_Active_Scenario);
-- Push scenario N on top of the scenario stack
@@ -1647,6 +1650,12 @@
if ASIS_Mode then
return;
+ -- Nothing to do when the call is being preanalyzed as the marker will
+ -- be inserted in the wrong place.
+
+ elsif Preanalysis_Active then
+ return;
+
-- Nothing to do when the input does not denote a call or a requeue
elsif not Nkind_In (N, N_Entry_Call_Statement,
@@ -1656,12 +1665,6 @@
then
return;
- -- Nothing to do when the call is being preanalyzed as the marker will
- -- be inserted in the wrong place.
-
- elsif Preanalysis_Active then
- return;
-
-- Nothing to do when the call is analyzed/resolved too early within an
-- intermediate context.
@@ -1808,6 +1811,146 @@
Record_Elaboration_Scenario (Marker);
end Build_Call_Marker;
+ -------------------------------------
+ -- Build_Variable_Reference_Marker --
+ -------------------------------------
+
+ procedure Build_Variable_Reference_Marker
+ (N : Node_Id;
+ Read : Boolean;
+ Write : Boolean)
+ is
+ function In_Pragma (Nod : Node_Id) return Boolean;
+ -- Determine whether arbitrary node Nod appears within a pragma
+
+ ---------------
+ -- In_Pragma --
+ ---------------
+
+ function In_Pragma (Nod : Node_Id) return Boolean is
+ Par : Node_Id;
+
+ begin
+ Par := Nod;
+ while Present (Par) loop
+ if Nkind (Par) = N_Pragma then
+ return True;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
+ return False;
+ end In_Pragma;
+
+ -- Local variables
+
+ Marker : Node_Id;
+ Prag : Node_Id;
+ Var_Attrs : Variable_Attributes;
+ Var_Id : Entity_Id;
+
+ -- Start of processing for Build_Variable_Reference_Marker
+
+ begin
+ -- Nothing to do for ASIS. As a result, ABE checks and diagnostics are
+ -- not performed in this mode.
+
+ if ASIS_Mode then
+ return;
+
+ -- Nothing to do when the reference is being preanalyzed as the marker
+ -- will be inserted in the wrong place.
+
+ elsif Preanalysis_Active then
+ return;
+
+ -- Nothing to do when the input does not denote a reference
+
+ elsif not Nkind_In (N, N_Expanded_Name, N_Identifier) then
+ return;
+
+ -- Nothing to do for internally-generated references
+
+ elsif not Comes_From_Source (N) then
+ return;
+
+ -- Nothing to do when the reference is erroneous, left in a bad state,
+ -- or does not denote a variable.
+
+ elsif not (Present (Entity (N))
+ and then Ekind (Entity (N)) = E_Variable
+ and then Entity (N) /= Any_Id)
+ then
+ return;
+ end if;
+
+ Extract_Variable_Reference_Attributes
+ (Ref => N,
+ Var_Id => Var_Id,
+ Attrs => Var_Attrs);
+
+ Prag := SPARK_Pragma (Var_Id);
+
+ if Comes_From_Source (Var_Id)
+
+ -- Both the variable and the reference must appear in SPARK_Mode On
+ -- regions because this scenario falls under the SPARK rules.
+
+ and then Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = On
+ and then Is_SPARK_Mode_On_Node (N)
+
+ -- The reference must not be considered when it appears in a pragma.
+ -- If the pragma has run-time semantics, then the reference will be
+ -- reconsidered once the pragma is expanded.
+
+ -- Performance note: parent traversal
+
+ and then not In_Pragma (N)
+ then
+ null;
+
+ -- Otherwise the reference is not suitable for ABE processing. This
+ -- prevents the generation of variable markers which will never play
+ -- a role in ABE diagnostics.
+
+ else
+ return;
+ end if;
+
+ -- At this point it is known that the variable reference will play some
+ -- role in ABE checks and diagnostics. Create a corresponding variable
+ -- marker in case the original variable reference is folded or optimized
+ -- away.
+
+ Marker := Make_Variable_Reference_Marker (Sloc (N));
+
+ -- Inherit the attributes of the original variable reference
+
+ Set_Target (Marker, Var_Id);
+ Set_Is_Read (Marker, Read);
+ Set_Is_Write (Marker, Write);
+
+ -- The marker is inserted prior to the original variable reference. The
+ -- insertion must take place even when the reference does not occur in
+ -- the main unit to keep the tree symmetric. This ensures that internal
+ -- name serialization is consistent in case the variable marker causes
+ -- the tree to transform in some way.
+
+ Insert_Action (N, Marker);
+
+ -- The marker becomes the "corresponding" scenario for the reference.
+ -- Save the marker for later processing for the ABE phase.
+
+ Record_Elaboration_Scenario (Marker);
+ end Build_Variable_Reference_Marker;
+
---------------------------------
-- Check_Elaboration_Scenarios --
---------------------------------
@@ -2990,15 +3133,46 @@
Var_Id : out Entity_Id;
Attrs : out Variable_Attributes)
is
+ function Get_Renamed_Variable (Id : Entity_Id) return Entity_Id;
+ -- Obtain the ultimate renamed variable of variable Id
+
+ --------------------------
+ -- Get_Renamed_Variable --
+ --------------------------
+
+ function Get_Renamed_Variable (Id : Entity_Id) return Entity_Id is
+ Ren_Id : Entity_Id;
+
+ begin
+ Ren_Id := Id;
+ while Present (Renamed_Entity (Ren_Id))
+ and then Nkind (Renamed_Entity (Ren_Id)) in N_Entity
+ loop
+ Ren_Id := Renamed_Entity (Ren_Id);
+ end loop;
+
+ return Ren_Id;
+ end Get_Renamed_Variable;
+
+ -- Start of processing for Extract_Variable_Reference_Attributes
+
begin
- -- Traverse a possible chain of renamings to obtain the original
- -- variable being referenced.
+ -- Extraction for variable reference markers
- Var_Id := Get_Renamed_Entity (Entity (Ref));
+ if Nkind (Ref) = N_Variable_Reference_Marker then
+ Var_Id := Target (Ref);
- Attrs.SPARK_Mode_On := Is_SPARK_Mode_On_Node (Ref);
- Attrs.Unit_Id := Find_Top_Unit (Var_Id);
+ -- Extraction for expanded names and identifiers
+ else
+ Var_Id := Entity (Ref);
+ end if;
+
+ -- Obtain the original variable which the reference mentions
+
+ Var_Id := Get_Renamed_Variable (Var_Id);
+ Attrs.Unit_Id := Find_Top_Unit (Var_Id);
+
-- At this point certain attributes should always be available
pragma Assert (Present (Attrs.Unit_Id));
@@ -4284,24 +4458,26 @@
In_SPARK => In_SPARK);
end Info_Instantiation;
- ------------------------
- -- Info_Variable_Read --
- ------------------------
+ -----------------------------
+ -- Info_Variable_Reference --
+ -----------------------------
- procedure Info_Variable_Read
+ procedure Info_Variable_Reference
(Ref : Node_Id;
Var_Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean)
is
begin
- Elab_Msg_NE
- (Msg => "read of variable & during elaboration",
- N => Ref,
- Id => Var_Id,
- Info_Msg => Info_Msg,
- In_SPARK => In_SPARK);
- end Info_Variable_Read;
+ if Is_Read (Ref) then
+ Elab_Msg_NE
+ (Msg => "read of variable & during elaboration",
+ N => Ref,
+ Id => Var_Id,
+ Info_Msg => Info_Msg,
+ In_SPARK => In_SPARK);
+ end if;
+ end Info_Variable_Reference;
--------------------
-- Insertion_Node --
@@ -5258,7 +5434,7 @@
or else Is_Suitable_Call (N)
or else Is_Suitable_Instantiation (N)
or else Is_Suitable_Variable_Assignment (N)
- or else Is_Suitable_Variable_Read (N);
+ or else Is_Suitable_Variable_Reference (N);
end Is_Suitable_Scenario;
-------------------------------------
@@ -5355,188 +5531,20 @@
and then Corresponding_Body (Var_Unit) = N_Unit_Id;
end Is_Suitable_Variable_Assignment;
- -------------------------------
- -- Is_Suitable_Variable_Read --
- -------------------------------
+ ------------------------------------
+ -- Is_Suitable_Variable_Reference --
+ ------------------------------------
- function Is_Suitable_Variable_Read (N : Node_Id) return Boolean is
- function In_Pragma (Nod : Node_Id) return Boolean;
- -- Determine whether arbitrary node Nod appears within a pragma
-
- function Is_Variable_Read (Ref : Node_Id) return Boolean;
- -- Determine whether variable reference Ref constitutes a read
-
- ---------------
- -- In_Pragma --
- ---------------
-
- function In_Pragma (Nod : Node_Id) return Boolean is
- Par : Node_Id;
-
- begin
- Par := Nod;
- while Present (Par) loop
- if Nkind (Par) = N_Pragma then
- return True;
-
- -- Prevent the search from going too far
-
- elsif Is_Body_Or_Package_Declaration (Par) then
- exit;
- end if;
-
- Par := Parent (Par);
- end loop;
-
- return False;
- end In_Pragma;
-
- ----------------------
- -- Is_Variable_Read --
- ----------------------
-
- function Is_Variable_Read (Ref : Node_Id) return Boolean is
- function Is_Out_Actual (Call : Node_Id) return Boolean;
- -- Determine whether the corresponding formal of actual Ref which
- -- appears in call Call has mode OUT.
-
- -------------------
- -- Is_Out_Actual --
- -------------------
-
- function Is_Out_Actual (Call : Node_Id) return Boolean is
- Actual : Node_Id;
- Call_Attrs : Call_Attributes;
- Formal : Entity_Id;
- Target_Id : Entity_Id;
-
- begin
- Extract_Call_Attributes
- (Call => Call,
- Target_Id => Target_Id,
- Attrs => Call_Attrs);
-
- -- Inspect the actual and formal parameters, trying to find the
- -- corresponding formal for Ref.
-
- Actual := First_Actual (Call);
- Formal := First_Formal (Target_Id);
- while Present (Actual) and then Present (Formal) loop
- if Actual = Ref then
- return Ekind (Formal) = E_Out_Parameter;
- end if;
-
- Next_Actual (Actual);
- Next_Formal (Formal);
- end loop;
-
- return False;
- end Is_Out_Actual;
-
- -- Local variables
-
- Context : constant Node_Id := Parent (Ref);
-
- -- Start of processing for Is_Variable_Read
-
- begin
- -- The majority of variable references are reads, and they can appear
- -- in a great number of contexts. To determine whether a reference is
- -- a read, it is more practical to find out whether it is a write.
-
- -- A reference is a write when it appears immediately on the left-
- -- hand side of an assignment.
-
- if Nkind (Context) = N_Assignment_Statement
- and then Name (Context) = Ref
- then
- return False;
-
- -- A reference is a write when it acts as an actual in a subprogram
- -- call and the corresponding formal has mode OUT.
-
- elsif Nkind_In (Context, N_Function_Call,
- N_Procedure_Call_Statement)
- and then Is_Out_Actual (Context)
- then
- return False;
- end if;
-
- -- Any other reference is a read
-
- return True;
- end Is_Variable_Read;
-
- -- Local variables
-
- Prag : Node_Id;
- Var_Id : Entity_Id;
-
- -- Start of processing for Is_Suitable_Variable_Read
-
+ function Is_Suitable_Variable_Reference (N : Node_Id) return Boolean is
begin
- -- This scenario is relevant only when the static model is in effect
- -- because it is graph-dependent and does not involve any run-time
- -- checks. Allowing it in the dynamic model would create confusing
- -- noise.
+ -- Expanded names and identifiers are intentionally ignored because they
+ -- be folded, optimized away, etc. Variable references markers play the
+ -- role of variable references and provide a uniform foundation for ABE
+ -- processing.
- if not Static_Elaboration_Checks then
- return False;
+ return Nkind (N) = N_Variable_Reference_Marker;
+ end Is_Suitable_Variable_Reference;
- -- Attributes and operator sumbols are not considered to be suitable
- -- references even though they are part of predicate Is_Entity_Name.
-
- elsif not Nkind_In (N, N_Expanded_Name, N_Identifier) then
- return False;
-
- -- Nothing to do for internally-generated references because they are
- -- assumed to be ABE safe.
-
- elsif not Comes_From_Source (N) then
- return False;
- end if;
-
- -- Sanitize the reference
-
- Var_Id := Entity (N);
-
- if No (Var_Id) then
- return False;
-
- elsif Var_Id = Any_Id then
- return False;
-
- elsif Ekind (Var_Id) /= E_Variable then
- return False;
- end if;
-
- Prag := SPARK_Pragma (Var_Id);
-
- -- To qualify, the reference must meet the following prerequisites:
-
- return
- Comes_From_Source (Var_Id)
-
- -- Both the variable and the reference must appear in SPARK_Mode On
- -- regions because this scenario falls under the SPARK rules.
-
- and then Present (Prag)
- and then Get_SPARK_Mode_From_Annotation (Prag) = On
- and then Is_SPARK_Mode_On_Node (N)
-
- -- The reference must denote a variable read
-
- and then Is_Variable_Read (N)
-
- -- The reference must not be considered when it appears in a pragma.
- -- If the pragma has run-time semantics, then the reference will be
- -- reconsidered once the pragma is expanded.
-
- -- Performance note: parent traversal
-
- and then not In_Pragma (N);
- end Is_Suitable_Variable_Read;
-
-------------------
-- Is_Task_Entry --
-------------------
@@ -5710,8 +5718,8 @@
Info_Msg => False,
In_SPARK => True);
- elsif Is_Suitable_Variable_Read (N) then
- Info_Variable_Read
+ elsif Is_Suitable_Variable_Reference (N) then
+ Info_Variable_Reference
(Ref => N,
Var_Id => Target_Id,
Info_Msg => False,
@@ -5875,8 +5883,8 @@
procedure Output_Variable_Assignment (N : Node_Id);
-- Emit a specific diagnostic message for assignment statement N
- procedure Output_Variable_Read (N : Node_Id);
- -- Emit a specific diagnostic message for reference N which reads a
+ procedure Output_Variable_Reference (N : Node_Id);
+ -- Emit a specific diagnostic message for reference N which mentions a
-- variable.
-------------------
@@ -6206,11 +6214,11 @@
Error_Msg_NE ("\\ variable & assigned #", Error_Nod, Var_Id);
end Output_Variable_Assignment;
- --------------------------
- -- Output_Variable_Read --
- --------------------------
+ -------------------------------
+ -- Output_Variable_Reference --
+ -------------------------------
- procedure Output_Variable_Read (N : Node_Id) is
+ procedure Output_Variable_Reference (N : Node_Id) is
Dummy : Variable_Attributes;
Var_Id : Entity_Id;
@@ -6221,9 +6229,12 @@
Attrs => Dummy);
Error_Msg_Sloc := Sloc (N);
- Error_Msg_NE ("\\ variable & read #", Error_Nod, Var_Id);
- end Output_Variable_Read;
+ if Is_Read (N) then
+ Error_Msg_NE ("\\ variable & read #", Error_Nod, Var_Id);
+ end if;
+ end Output_Variable_Reference;
+
-- Local variables
package Stack renames Scenario_Stack;
@@ -6283,10 +6294,10 @@
elsif Nkind (N) = N_Assignment_Statement then
Output_Variable_Assignment (N);
- -- Variable read
+ -- Variable references
- elsif Is_Suitable_Variable_Read (N) then
- Output_Variable_Read (N);
+ elsif Is_Suitable_Variable_Reference (N) then
+ Output_Variable_Reference (N);
else
pragma Assert (False);
@@ -8140,11 +8151,11 @@
end if;
end Process_Variable_Assignment_SPARK;
- ---------------------------
- -- Process_Variable_Read --
- ---------------------------
+ --------------------------------
+ -- Process_Variable_Reference --
+ --------------------------------
- procedure Process_Variable_Read (Ref : Node_Id) is
+ procedure Process_Variable_Reference (Ref : Node_Id) is
Var_Attrs : Variable_Attributes;
Var_Id : Entity_Id;
@@ -8154,6 +8165,24 @@
Var_Id => Var_Id,
Attrs => Var_Attrs);
+ if Is_Read (Ref) then
+ Process_Variable_Reference_Read
+ (Ref => Ref,
+ Var_Id => Var_Id,
+ Attrs => Var_Attrs);
+ end if;
+ end Process_Variable_Reference;
+
+ -------------------------------------
+ -- Process_Variable_Reference_Read --
+ -------------------------------------
+
+ procedure Process_Variable_Reference_Read
+ (Ref : Node_Id;
+ Var_Id : Entity_Id;
+ Attrs : Variable_Attributes)
+ is
+ begin
-- Output relevant information when switch -gnatel (info messages on
-- implicit Elaborate[_All] pragmas) is in effect.
@@ -8169,7 +8198,7 @@
-- Nothing to do when the variable appears within the main unit because
-- diagnostics on reads are relevant only for external variables.
- if Is_Same_Unit (Var_Attrs.Unit_Id, Cunit_Entity (Main_Unit)) then
+ if Is_Same_Unit (Attrs.Unit_Id, Cunit_Entity (Main_Unit)) then
null;
-- Nothing to do when the variable is already initialized. Note that the
@@ -8181,7 +8210,7 @@
-- Nothing to do when the external unit guarantees the initialization of
-- the variable by means of pragma Elaborate_Body.
- elsif Has_Pragma_Elaborate_Body (Var_Attrs.Unit_Id) then
+ elsif Has_Pragma_Elaborate_Body (Attrs.Unit_Id) then
null;
-- A variable read imposes an Elaborate requirement on the context of
@@ -8194,7 +8223,7 @@
Target_Id => Var_Id,
Req_Nam => Name_Elaborate);
end if;
- end Process_Variable_Read;
+ end Process_Variable_Reference_Read;
--------------------------
-- Push_Active_Scenario --
@@ -8271,10 +8300,21 @@
elsif Is_Suitable_Variable_Assignment (N) then
Process_Variable_Assignment (N);
- -- Variable read
+ -- Variable references
- elsif Is_Suitable_Variable_Read (N) then
- Process_Variable_Read (N);
+ elsif Is_Suitable_Variable_Reference (N) then
+
+ -- In general, only variable references found within the main unit
+ -- are processed because the ALI information supplied to binde is for
+ -- the main unit only. However, to preserve the consistency of the
+ -- tree and ensure proper serialization of internal names, external
+ -- variable references also receive corresponding variable reference
+ -- markers (see Build_Varaible_Reference_Marker). Regardless of the
+ -- reason, external variable references must not be processed.
+
+ if In_Main_Context (N) then
+ Process_Variable_Reference (N);
+ end if;
end if;
-- Remove the current scenario from the stack of active scenarios once
@@ -8365,7 +8405,7 @@
Possible_Local_Raise (N, Standard_Program_Error);
elsif Is_Suitable_Variable_Assignment (N)
- or else Is_Suitable_Variable_Read (N)
+ or else Is_Suitable_Variable_Reference (N)
then
null;
===================================================================
@@ -34,6 +34,15 @@
-- Create a call marker for call or requeue statement N and record it for
-- later processing by the ABE mechanism.
+ procedure Build_Variable_Reference_Marker
+ (N : Node_Id;
+ Read : Boolean;
+ Write : Boolean);
+ -- Create a variable reference marker for arbitrary node N if it mentions a
+ -- variable, and record it for later processing by the ABE mechanism. Flag
+ -- Read should be set when the reference denotes a read. Flag Write should
+ -- be set when the reference denotes a write.
+
procedure Check_Elaboration_Scenarios;
-- Examine each scenario recorded during analysis/resolution and apply the
-- Ada or SPARK elaboration rules taking into account the model in effect.
This patch reimplements the handling of variable references by the access- before-elaboration mechanism for the purpose of SPARK elaboration checks. Prior to the patch, variable references (N_Expanded_Name and N_Identifier) were detected and processed as is, however such references might be folded, optimized away, or hard to categorize as reads or writes. The patch ignores such references and instead installs markers in the tree to signal that a variable read or write took place. As a result, the access-before-elaboration mechanism has a uniform model for processing variable reference, regardless of whether the references were modified in any way. ------------ -- Source -- ------------ -- pack.ads package Pack with SPARK_Mode is type Iface is interface; procedure Prim_Proc (Obj : Iface; In_Val : Integer; IO_Val : in out Integer; Ou_Val : out Integer) is abstract; function Prim_Func (Obj : Iface; Val : Integer) return Boolean is abstract; procedure Iface_Dispatch_On_Prim_Proc; procedure Iface_Dispatch_On_Prim_Func; type Deriv is new Iface with record Data : Integer; end record; procedure Prim_Proc (Obj : Deriv; In_Val : Integer; IO_Val : in out Integer; Ou_Val : out Integer); function Prim_Func (Obj : Deriv; Val : Integer) return Boolean; procedure Deriv_Dispatch_On_Prim_Proc; procedure Deriv_Dispatch_On_Prim_Func; end Pack; -- pack.adb package body Pack with SPARK_Mode is procedure Iface_Dispatch_On_Prim_Proc is Obj : Iface'Class := Deriv'(Data => 123); In_Act : Integer := 1; IO_Act : Integer := 2; Ou_Act : Integer := 3; begin Obj.Prim_Proc (In_Act, IO_Act, Ou_Act); -- read read read end Iface_Dispatch_On_Prim_Proc; procedure Iface_Dispatch_On_Prim_Func is Obj : Iface'Class := Deriv'(Data => 123); In_Act : Integer := 1; Result : Boolean := False; begin Result := Obj.Prim_Func (In_Act); -- read read end Iface_Dispatch_On_Prim_Func; procedure Deriv_Dispatch_On_Prim_Proc is Obj : Deriv'Class := Deriv'(Data => 456); In_Act : Integer := 1; IO_Act : Integer := 2; Ou_Act : Integer := 3; begin Obj.Prim_Proc (In_Act, IO_Act, Ou_Act); -- read read read end Deriv_Dispatch_On_Prim_Proc; procedure Deriv_Dispatch_On_Prim_Func is Obj : Deriv'Class := Deriv'(Data => 456); In_Act : Integer := 1; Result : Boolean := False; begin Result := Obj.Prim_Func (In_Act); -- read read end Deriv_Dispatch_On_Prim_Func; procedure Prim_Proc (Obj : Deriv; In_Val : Integer; IO_Val : in out Integer; Ou_Val : out Integer) is begin if In_Val > 1 then -- read IO_Val := IO_Val + Obj.Data; -- read Ou_Val := Obj.Data; end if; end Prim_Proc; function Prim_Func (Obj : Deriv; Val : Integer) return Boolean is begin return Obj.Data = Val; end Prim_Func; Obj : Deriv := Deriv'(Data => 789); In_Act : Integer := 1; IO_Act : Integer := 2; Ou_Act : Integer := 3; Result : Boolean := False; begin Iface_Dispatch_On_Prim_Proc; Iface_Dispatch_On_Prim_Func; Deriv_Dispatch_On_Prim_Proc; Deriv_Dispatch_On_Prim_Func; Obj.Prim_Proc (In_Act, IO_Act, Ou_Act); -- read read read Result := Obj.Prim_Func (In_Act); -- read read end Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnatel pack.adb pack.adb:3:07: info: adjustment actions for type "Iface" during elaboration in SPARK pack.adb:10:07: info: read of variable "Obj" during elaboration in SPARK pack.adb:10:10: info: call to "Prim_Proc" during elaboration in SPARK pack.adb:10:22: info: read of variable "In_Act" during elaboration in SPARK pack.adb:10:30: info: read of variable "IO_Act" during elaboration in SPARK pack.adb:15:07: info: adjustment actions for type "Iface" during elaboration in SPARK pack.adb:21:17: info: read of variable "Obj" during elaboration in SPARK pack.adb:21:20: info: call to "Prim_Func" during elaboration in SPARK pack.adb:21:32: info: read of variable "In_Act" during elaboration in SPARK pack.adb:26:07: info: adjustment actions for type "Deriv" during elaboration in SPARK pack.adb:33:07: info: read of variable "Obj" during elaboration in SPARK pack.adb:33:10: info: call to "Prim_Proc" during elaboration in SPARK pack.adb:33:22: info: read of variable "In_Act" during elaboration in SPARK pack.adb:33:30: info: read of variable "IO_Act" during elaboration in SPARK pack.adb:38:07: info: adjustment actions for type "Deriv" during elaboration in SPARK pack.adb:44:17: info: read of variable "Obj" during elaboration in SPARK pack.adb:44:20: info: call to "Prim_Func" during elaboration in SPARK pack.adb:44:32: info: read of variable "In_Act" during elaboration in SPARK pack.adb:76:04: info: call to "Iface_Dispatch_On_Prim_Proc" during elaboration in SPARK pack.adb:77:04: info: call to "Iface_Dispatch_On_Prim_Func" during elaboration in SPARK pack.adb:78:04: info: call to "Deriv_Dispatch_On_Prim_Proc" during elaboration in SPARK pack.adb:79:04: info: call to "Deriv_Dispatch_On_Prim_Func" during elaboration in SPARK pack.adb:81:04: info: read of variable "Obj" during elaboration in SPARK pack.adb:81:07: info: call to "Prim_Proc" during elaboration in SPARK pack.adb:81:19: info: read of variable "In_Act" during elaboration in SPARK pack.adb:81:27: info: read of variable "IO_Act" during elaboration in SPARK pack.adb:83:14: info: read of variable "Obj" during elaboration in SPARK pack.adb:83:17: info: call to "Prim_Func" during elaboration in SPARK pack.adb:83:29: info: read of variable "In_Act" during elaboration in SPARK Tested on x86_64-pc-linux-gnu, committed on trunk 2017-11-08 Hristian Kirtchev <kirtchev@adacore.com> * exp_ch3.adb (Expand_N_Object_Declaration): Save and restore relevant SPARK-related flags. Add ??? comment. * exp_util.adb (Insert_Actions): Add an entry for node N_Variable_Reference_Marker. * sem.adb (Analyze): Add an entry for node N_Variable_Reference_Marker. * sem_ch8.adb (Find_Direct_Name): Add constant Is_Assignment_LHS. Build and record a variable reference marker for the current name. (Find_Expanded_Name): Add constant Is_Assignment_LHS. Build and record a variable reference marker for the current name. * sem_elab.adb (Build_Variable_Reference_Marker): New routine. (Extract_Variable_Reference_Attributes): Reimplemented. (Info_Scenario): Add output for variable references and remove output for variable reads. (Info_Variable_Read): Removed. (Info_Variable_Reference): New routine. (Is_Suitable_Scenario): Variable references are now suitable scenarios while variable reads are not. (Output_Active_Scenarios): Add output for variable references and remove output for variable reads. (Output_Variable_Read): Removed. (Output_Variable_Reference): New routine. (Process_Variable_Read): Removed. (Process_Variable_Reference): New routine. (Process_Variable_Reference_Read): New routine. * sem_elab.ads (Build_Variable_Reference_Marker): New routine. * sem_res.adb (Resolve_Actuals): Build and record a variable reference marker for the current actual. * sem_spark.adb (Check_Node): Add an entry for node N_Variable_Reference_Marker. * sem_util.adb (Within_Subprogram_Call): Moved to the library level. * sem_util.ads (Within_Subprogram_Call): Moved to the library level. * sinfo.adb (Is_Read): New routine. (Is_Write): New routine. (Target): Updated to handle variable reference markers. (Set_Is_Read): New routine. (Set_Is_Write): New routine. (Set_Target): Updated to handle variable reference markers. * sinfo.ads: Add new attributes Is_Read and Is_Write along with occurrences in nodes. Update attribute Target. Add new node kind N_Variable_Reference_Marker. (Is_Read): New routine along with pragma Inline. (Is_Write): New routine along with pragma Inline. (Set_Is_Read): New routine along with pragma Inline. (Set_Is_Write): New routine along with pragma Inline. * sprint.adb (Sprint_Node_Actual): Add an entry for node N_Variable_Reference_Marker.