[multiple changes]

2015-11-18  Hristian Kirtchev  <kirtchev@adacore.com>

	* atree.adb (Elist11): New routine.
	(Set_Elist11): New routine.
	* atree.ads (Elist11): New routine.
	(Set_Elist11): New routine.
	* atree.h: Define Elist11.
	* contracts.adb (Analyze_Object_Contract): Verify the legality
	of all references to a variable given that the variable is a
	constituent of a single protected/task type.
	* einfo.adb: Part_Of_References now utilizes Elist11.
	(Part_Of_References): New routine.
	(Set_Part_Of_References): New routine.
	(Write_Field11_Name): Add output for Part_Of_References.
	* einfo.ads New attribute Part_Of_References along with usage
	in entities.
	(Part_Of_References): New routine along with
	pragma Inline.
	(Set_Part_Of_References): New routine along with pragma Inline.
	* sem_prag.adb (Analyze_Constituent): Record a possible
	reference to a concurrent constituent.
	(Analyze_Global_Item): Record a possible reference to a concurrent
	constituent.
	(Analyze_Input_Output): Record a possible reference to a
	concurrent constituent.
	* sem_res.adb (Resolve_Entity_Name): Record a possible reference
	to a concurrent constituent.
	* sem_util.adb (Check_Part_Of_Reference): New routine.
	(Record_Possible_Part_Of_Reference): New routine.
	* sem_util.ads (Check_Part_Of_Reference): New routine.
	(Record_Possible_Part_Of_Reference): New routine.

2015-11-18  Ed Schonberg  <schonberg@adacore.com>

	* checks.adb (Apply_Arithmetic_Overflow_Minimized_Eliminated):
	An if_expression is the proper place to apply the overflow
	minimization procedure if its context is not an enclosing
	arithmetic expression.

From-SVN: r230540
This commit is contained in:
Arnaud Charlet 2015-11-18 11:53:39 +01:00
parent 3f8d242bd3
commit fdc54be6a0
12 changed files with 334 additions and 7 deletions

View File

@ -1,3 +1,42 @@
2015-11-18 Hristian Kirtchev <kirtchev@adacore.com>
* atree.adb (Elist11): New routine.
(Set_Elist11): New routine.
* atree.ads (Elist11): New routine.
(Set_Elist11): New routine.
* atree.h: Define Elist11.
* contracts.adb (Analyze_Object_Contract): Verify the legality
of all references to a variable given that the variable is a
constituent of a single protected/task type.
* einfo.adb: Part_Of_References now utilizes Elist11.
(Part_Of_References): New routine.
(Set_Part_Of_References): New routine.
(Write_Field11_Name): Add output for Part_Of_References.
* einfo.ads New attribute Part_Of_References along with usage
in entities.
(Part_Of_References): New routine along with
pragma Inline.
(Set_Part_Of_References): New routine along with pragma Inline.
* sem_prag.adb (Analyze_Constituent): Record a possible
reference to a concurrent constituent.
(Analyze_Global_Item): Record a possible reference to a concurrent
constituent.
(Analyze_Input_Output): Record a possible reference to a
concurrent constituent.
* sem_res.adb (Resolve_Entity_Name): Record a possible reference
to a concurrent constituent.
* sem_util.adb (Check_Part_Of_Reference): New routine.
(Record_Possible_Part_Of_Reference): New routine.
* sem_util.ads (Check_Part_Of_Reference): New routine.
(Record_Possible_Part_Of_Reference): New routine.
2015-11-18 Ed Schonberg <schonberg@adacore.com>
* checks.adb (Apply_Arithmetic_Overflow_Minimized_Eliminated):
An if_expression is the proper place to apply the overflow
minimization procedure if its context is not an enclosing
arithmetic expression.
2015-11-18 Arnaud Charlet <charlet@adacore.com>
* gnat_ugn/gnat_project_manager.rst,

View File

@ -3093,6 +3093,17 @@ package body Atree is
end if;
end Elist10;
function Elist11 (N : Node_Id) return Elist_Id is
pragma Assert (Nkind (N) in N_Entity);
Value : constant Union_Id := Nodes.Table (N + 1).Field11;
begin
if Value = 0 then
return No_Elist;
else
return Elist_Id (Value);
end if;
end Elist11;
function Elist13 (N : Node_Id) return Elist_Id is
pragma Assert (Nkind (N) in N_Entity);
Value : constant Union_Id := Nodes.Table (N + 2).Field6;
@ -5924,6 +5935,12 @@ package body Atree is
Nodes.Table (N + 1).Field10 := Union_Id (Val);
end Set_Elist10;
procedure Set_Elist11 (N : Node_Id; Val : Elist_Id) is
begin
pragma Assert (Nkind (N) in N_Entity);
Nodes.Table (N + 1).Field11 := Union_Id (Val);
end Set_Elist11;
procedure Set_Elist13 (N : Node_Id; Val : Elist_Id) is
begin
pragma Assert (Nkind (N) in N_Entity);

View File

@ -1439,6 +1439,9 @@ package Atree is
function Elist10 (N : Node_Id) return Elist_Id;
pragma Inline (Elist10);
function Elist11 (N : Node_Id) return Elist_Id;
pragma Inline (Elist11);
function Elist13 (N : Node_Id) return Elist_Id;
pragma Inline (Elist13);
@ -2799,6 +2802,9 @@ package Atree is
procedure Set_Elist10 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist10);
procedure Set_Elist11 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist11);
procedure Set_Elist13 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist13);

View File

@ -516,6 +516,7 @@ extern Node_Id Current_Error_Node;
#define Elist8(N) Field8 (N)
#define Elist9(N) Field9 (N)
#define Elist10(N) Field10 (N)
#define Elist11(N) Field11 (N)
#define Elist13(N) Field13 (N)
#define Elist15(N) Field15 (N)
#define Elist16(N) Field16 (N)

View File

@ -1208,8 +1208,19 @@ package body Checks is
or else (Nkind (P) = N_Range
and then Nkind (Parent (P)) in N_Membership_Test)
then
-- If_Expressions and Case_Expressions are treated as arithmetic
-- ops, but if they appear in an assignment or similar contexts
-- there is no overflow check that starts from that parent node,
-- so apply check now.
if Nkind_In (P, N_If_Expression, N_Case_Expression)
and then not Is_Signed_Integer_Arithmetic_Op (Parent (P))
then
null;
else
return;
end if;
end if;
-- Otherwise, we have a top level arithmetic operation node, and this
-- is where we commence the special processing for MINIMIZED/ELIMINATED
@ -1302,7 +1313,7 @@ package body Checks is
Analyze_And_Resolve (Op);
end;
-- Here we know the result is Long_Long_Integer'Base, of that it has
-- Here we know the result is Long_Long_Integer'Base, or that it has
-- been rewritten because the parent operation is a conversion. See
-- Apply_Arithmetic_Overflow_Strict.Conversion_Optimization.

View File

@ -634,6 +634,7 @@ package body Contracts is
Items : Node_Id;
Mode : SPARK_Mode_Type;
Prag : Node_Id;
Ref_Elmt : Elmt_Id;
Restore_Mode : Boolean := False;
Seen : Boolean := False;
@ -770,6 +771,23 @@ package body Contracts is
if Present (Prag) then
Analyze_Part_Of_In_Decl_Part (Prag);
-- The variable is a constituent of a single protected/task type
-- and behaves as a component of the type. Verify that references
-- to the variable occur within the definition or body of the type
-- (SPARK RM 9.3).
if Present (Encapsulating_State (Obj_Id))
and then Is_Single_Concurrent_Object
(Encapsulating_State (Obj_Id))
and then Present (Part_Of_References (Obj_Id))
then
Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id));
while Present (Ref_Elmt) loop
Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt));
Next_Elmt (Ref_Elmt);
end loop;
end if;
-- Otherwise check whether the lack of indicator Part_Of agrees with
-- the placement of the variable with respect to the state space.

View File

@ -95,13 +95,14 @@ package body Einfo is
-- Normalized_Position_Max Uint10
-- Part_Of_Constituents Elist10
-- Block_Node Node11
-- Component_Bit_Offset Uint11
-- Full_View Node11
-- Entry_Component Node11
-- Enumeration_Pos Uint11
-- Generic_Homonym Node11
-- Part_Of_References Elist11
-- Protected_Body_Subprogram Node11
-- Block_Node Node11
-- Barrier_Function Node12
-- Enumeration_Rep Uint12
@ -2861,6 +2862,12 @@ package body Einfo is
return Elist10 (Id);
end Part_Of_Constituents;
function Part_Of_References (Id : E) return L is
begin
pragma Assert (Ekind (Id) = E_Variable);
return Elist11 (Id);
end Part_Of_References;
function Partial_View_Has_Unknown_Discr (Id : E) return B is
begin
pragma Assert (Is_Type (Id));
@ -5897,6 +5904,12 @@ package body Einfo is
Set_Elist10 (Id, V);
end Set_Part_Of_Constituents;
procedure Set_Part_Of_References (Id : E; V : L) is
begin
pragma Assert (Ekind (Id) = E_Variable);
Set_Elist11 (Id, V);
end Set_Part_Of_References;
procedure Set_Partial_View_Has_Unknown_Discr (Id : E; V : B := True) is
begin
pragma Assert (Is_Type (Id));
@ -9363,10 +9376,13 @@ package body Einfo is
when E_Generic_Package =>
Write_Str ("Generic_Homonym");
when E_Function |
E_Procedure |
E_Entry |
E_Entry_Family =>
when E_Variable =>
Write_Str ("Part_Of_References");
when E_Entry |
E_Entry_Family |
E_Function |
E_Procedure =>
Write_Str ("Protected_Body_Subprogram");
when others =>

View File

@ -3696,6 +3696,12 @@ package Einfo is
-- constituents that are subject to indicator Part_Of (both aspect and
-- option variants).
-- Part_Of_References (Elist11)
-- Present in variable entities. Contains all references to the variable
-- when it is subject to pragma Part_Of. If the variable is a constituent
-- of a single protected/task type, the references are examined as they
-- must appear only within the type defintion and the corresponding body.
-- Partial_View_Has_Unknown_Discr (Flag280)
-- Present in all types. Set to Indicate that the partial view of a type
-- has unknown discriminants. A default initialization of an object of
@ -6431,6 +6437,7 @@ package Einfo is
-- Hiding_Loop_Variable (Node8)
-- Current_Value (Node9)
-- Part_Of_Constituents (Elist10)
-- Part_Of_References (Elist11)
-- Esize (Uint12)
-- Extra_Accessibility (Node13)
-- Alignment (Uint14)
@ -7089,6 +7096,7 @@ package Einfo is
function Packed_Array_Impl_Type (Id : E) return E;
function Parent_Subtype (Id : E) return E;
function Part_Of_Constituents (Id : E) return L;
function Part_Of_References (Id : E) return L;
function Partial_View_Has_Unknown_Discr (Id : E) return B;
function Pending_Access_Types (Id : E) return L;
function Postconditions_Proc (Id : E) return E;
@ -7756,6 +7764,7 @@ package Einfo is
procedure Set_Packed_Array_Impl_Type (Id : E; V : E);
procedure Set_Parent_Subtype (Id : E; V : E);
procedure Set_Part_Of_Constituents (Id : E; V : L);
procedure Set_Part_Of_References (Id : E; V : L);
procedure Set_Partial_View_Has_Unknown_Discr (Id : E; V : B := True);
procedure Set_Pending_Access_Types (Id : E; V : L);
procedure Set_Postconditions_Proc (Id : E; V : E);
@ -8582,6 +8591,7 @@ package Einfo is
pragma Inline (Parameter_Mode);
pragma Inline (Parent_Subtype);
pragma Inline (Part_Of_Constituents);
pragma Inline (Part_Of_References);
pragma Inline (Partial_View_Has_Unknown_Discr);
pragma Inline (Pending_Access_Types);
pragma Inline (Postconditions_Proc);
@ -9043,6 +9053,7 @@ package Einfo is
pragma Inline (Set_Packed_Array_Impl_Type);
pragma Inline (Set_Parent_Subtype);
pragma Inline (Set_Part_Of_Constituents);
pragma Inline (Set_Part_Of_References);
pragma Inline (Set_Partial_View_Has_Unknown_Discr);
pragma Inline (Set_Pending_Access_Types);
pragma Inline (Set_Postconditions_Proc);

View File

@ -957,6 +957,16 @@ package body Sem_Prag is
if Ekind (Item_Id) = E_Abstract_State then
Append_New_Elmt (Item_Id, States_Seen);
-- The variable may eventually become a constituent of a
-- single protected/task type. Record the reference now
-- and verify its legality when analyzing the contract of
-- the variable (SPARK RM 9.3).
elsif Ekind (Item_Id) = E_Variable then
Record_Possible_Part_Of_Reference
(Var_Id => Item_Id,
Ref => Item);
end if;
if Ekind_In (Item_Id, E_Abstract_State,
@ -2209,6 +2219,16 @@ package body Sem_Prag is
if Ekind (Item_Id) = E_Abstract_State then
Append_New_Elmt (Item_Id, States_Seen);
-- The variable may eventually become a constituent of a single
-- protected/task type. Record the reference now and verify its
-- legality when analyzing the contract of the variable
-- (SPARK RM 9.3).
elsif Ekind (Item_Id) = E_Variable then
Record_Possible_Part_Of_Reference
(Var_Id => Item_Id,
Ref => Item);
end if;
if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
@ -25452,6 +25472,17 @@ package body Sem_Prag is
then
Match_Constituent (Constit_Id);
-- The variable may eventually become a constituent of a
-- single protected/task type. Record the reference now
-- and verify its legality when analyzing the contract of
-- the variable (SPARK RM 9.3).
if Ekind (Constit_Id) = E_Variable then
Record_Possible_Part_Of_Reference
(Var_Id => Constit_Id,
Ref => Constit);
end if;
-- Otherwise the constituent is illegal
else

View File

@ -7240,6 +7240,15 @@ package body Sem_Res is
then
Check_Elab_Call (N);
end if;
-- The variable may eventually become a constituent of a single
-- protected/task type. Record the reference now and verify its
-- legality when analyzing the contract of the variable
-- (SPARK RM 9.3).
if Ekind (E) = E_Variable then
Record_Possible_Part_Of_Reference (E, N);
end if;
end if;
-- A Ghost entity must appear in a specific context

View File

@ -1916,6 +1916,126 @@ package body Sem_Util is
end if;
end Cannot_Raise_Constraint_Error;
-----------------------------
-- Check_Part_Of_Reference --
-----------------------------
procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id) is
Conc_Typ : constant Entity_Id := Encapsulating_State (Var_Id);
Decl : Node_Id;
OK_Use : Boolean := False;
Par : Node_Id;
Prag_Nam : Name_Id;
Spec_Id : Entity_Id;
begin
-- Traverse the parent chain looking for a suitable context for the
-- reference to the concurrent constituent.
Par := Parent (Ref);
while Present (Par) loop
if Nkind (Par) = N_Pragma then
Prag_Nam := Pragma_Name (Par);
-- A concurrent constituent is allowed to appear in pragmas
-- Initial_Condition and Initializes as this is part of the
-- elaboration checks for the constituent (SPARK RM 9.3).
if Nam_In (Prag_Nam, Name_Initial_Condition, Name_Initializes) then
OK_Use := True;
exit;
-- When the reference appears within pragma Depends or Global,
-- check whether the pragma applies to a single task type. Note
-- that the pragma is not encapsulated by the type definition,
-- but this is still a valid context.
elsif Nam_In (Prag_Nam, Name_Depends, Name_Global) then
Decl := Find_Related_Declaration_Or_Body (Par);
if Nkind (Decl) = N_Object_Declaration
and then Defining_Entity (Decl) = Conc_Typ
then
OK_Use := True;
exit;
end if;
end if;
-- The reference appears somewhere in the definition of the single
-- protected/task type (SPARK RM 9.3).
elsif Nkind_In (Par, N_Single_Protected_Declaration,
N_Single_Task_Declaration)
and then Defining_Entity (Par) = Conc_Typ
then
OK_Use := True;
exit;
-- The reference appears within the expanded declaration or the body
-- of the single protected/task type (SPARK RM 9.3).
elsif Nkind_In (Par, N_Protected_Body,
N_Protected_Type_Declaration,
N_Task_Body,
N_Task_Type_Declaration)
then
Spec_Id := Unique_Defining_Entity (Par);
if Present (Anonymous_Object (Spec_Id))
and then Anonymous_Object (Spec_Id) = Conc_Typ
then
OK_Use := True;
exit;
end if;
-- The reference has been relocated within an internally generated
-- package or subprogram. Assume that the reference is legal as the
-- real check was already performed in the original context of the
-- reference.
elsif Nkind_In (Par, N_Package_Body,
N_Package_Declaration,
N_Subprogram_Body,
N_Subprogram_Declaration)
and then not Comes_From_Source (Par)
then
OK_Use := True;
exit;
-- The reference has been relocated to an inlined body for GNATprove.
-- Assume that the reference is legal as the real check was already
-- performed in the original context of the reference.
elsif GNATprove_Mode
and then Nkind (Par) = N_Subprogram_Body
and then Chars (Defining_Entity (Par)) = Name_uParent
then
OK_Use := True;
exit;
end if;
Par := Parent (Par);
end loop;
-- The reference is illegal as it appears outside the definition or
-- body of the single protected/task type.
if not OK_Use then
Error_Msg_NE
("reference to variable & cannot appear in this context",
Ref, Var_Id);
Error_Msg_Name_1 := Chars (Var_Id);
if Ekind (Conc_Typ) = E_Protected_Type then
Error_Msg_NE
("\% is constituent of single protected type &", Ref, Conc_Typ);
else
Error_Msg_NE
("\% is constituent of single task type &", Ref, Conc_Typ);
end if;
end if;
end Check_Part_Of_Reference;
-----------------------------------------
-- Check_Dynamically_Tagged_Expression --
-----------------------------------------
@ -17255,6 +17375,42 @@ package body Sem_Util is
Set_Sloc (Endl, Loc);
end Process_End_Label;
---------------------------------------
-- Record_Possible_Part_Of_Reference --
---------------------------------------
procedure Record_Possible_Part_Of_Reference
(Var_Id : Entity_Id;
Ref : Node_Id)
is
Encap : constant Entity_Id := Encapsulating_State (Var_Id);
Refs : Elist_Id;
begin
-- The variable is a constituent of a single protected/task type. Such
-- a variable acts as a component of the type and must appear within a
-- specific region (SPARK RM 9.3). Instead of recording the reference,
-- verify its legality now.
if Present (Encap) and then Is_Single_Concurrent_Object (Encap) then
Check_Part_Of_Reference (Var_Id, Ref);
-- The variable is subject to pragma Part_Of and may eventually become a
-- constituent of a single protected/task type. Record the reference to
-- verify its placement when the contract of the variable is analyzed.
elsif Present (Get_Pragma (Var_Id, Pragma_Part_Of)) then
Refs := Part_Of_References (Var_Id);
if No (Refs) then
Refs := New_Elmt_List;
Set_Part_Of_References (Var_Id, Refs);
end if;
Append_Elmt (Ref, Refs);
end if;
end Record_Possible_Part_Of_Reference;
----------------
-- Referenced --
----------------

View File

@ -252,6 +252,10 @@ package Sem_Util is
-- not necessarily mean that CE could be raised, but a response of True
-- means that for sure CE cannot be raised.
procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id);
-- Verify the legality of reference Ref to variable Var_Id when the
-- variable is a constituent of a single protected/task type.
procedure Check_Dynamically_Tagged_Expression
(Expr : Node_Id;
Typ : Entity_Id;
@ -1922,6 +1926,14 @@ package Sem_Util is
-- parameter Ent gives the entity to which the End_Label refers,
-- and to which cross-references are to be generated.
procedure Record_Possible_Part_Of_Reference
(Var_Id : Entity_Id;
Ref : Node_Id);
-- Save reference Ref to variable Var_Id when the variable is subject to
-- pragma Part_Of. If the variable is known to be a constituent of a single
-- protected/task type, the legality of the reference is verified and the
-- save does not take place.
function Referenced (Id : Entity_Id; Expr : Node_Id) return Boolean;
-- Determine whether entity Id is referenced within expression Expr