From fdc54be6a0216ac2b4c585824539712d162b8e26 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Wed, 18 Nov 2015 11:53:39 +0100 Subject: [PATCH] [multiple changes] 2015-11-18 Hristian Kirtchev * 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 * 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 --- gcc/ada/ChangeLog | 39 +++++++++++ gcc/ada/atree.adb | 17 +++++ gcc/ada/atree.ads | 6 ++ gcc/ada/atree.h | 1 + gcc/ada/checks.adb | 15 +++- gcc/ada/contracts.adb | 18 +++++ gcc/ada/einfo.adb | 26 +++++-- gcc/ada/einfo.ads | 11 +++ gcc/ada/sem_prag.adb | 31 +++++++++ gcc/ada/sem_res.adb | 9 +++ gcc/ada/sem_util.adb | 156 ++++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_util.ads | 12 ++++ 12 files changed, 334 insertions(+), 7 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8cafc9a19c2..c1b77c7f55f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,42 @@ +2015-11-18 Hristian Kirtchev + + * 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 + + * 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 * gnat_ugn/gnat_project_manager.rst, diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 1afaca6908d..5ae768a41ea 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -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); diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads index 08ea27770c8..0f5b51225df 100644 --- a/gcc/ada/atree.ads +++ b/gcc/ada/atree.ads @@ -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); diff --git a/gcc/ada/atree.h b/gcc/ada/atree.h index f92961ee7ec..a2159c83777 100644 --- a/gcc/ada/atree.h +++ b/gcc/ada/atree.h @@ -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) diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 64dcf57ae8a..07a9dac3abc 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -1208,7 +1208,18 @@ package body Checks is or else (Nkind (P) = N_Range and then Nkind (Parent (P)) in N_Membership_Test) then - return; + -- 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 @@ -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. diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 4b6a1279aba..bc1691175f3 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -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. diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index a8cfa1abefb..b252e8c0b96 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -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 => diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index d1f441bec5b..cd5a4fb2544 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -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); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index f3282ea97f9..dd462199378 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -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 diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index ec7e01908c3..f551c5e71c2 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 9a000ae7dc6..47ad601c578 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -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 -- ---------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index cc53a57bb51..91c5d85a518 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -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 -- 2.30.2