From 9057bd6af94f176dd904b476534cc42158799ae5 Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Thu, 24 May 2018 13:04:52 +0000 Subject: [PATCH] [Ada] Fix crash on formal containers This patch modifies several mechanisms in the compiler: 1) The handling of Ghost regions now records the start of the outermost ignored Ghost region which is currently in effect. 2) Generation of freeze actions for an arbitrary entity now inserts the actions prior to the start of the outermost ignored Ghost region when the freezing takes effect within an ignored Ghost region, but the entity being frozen is "living". This ensures that any freeze actions associated with the living entity will not be eliminated from the tree once ignored Ghost code is stripped away. 3) The Default_Initial_Condition and Invariant procedures are not treated as primitives even when they apply to tagged types. These procedures already employ class-wide precondition-like semantics to handle inheritance and overriding. In addition, the procedures cannot be invoked from source and should not be targets of dispatching calls. 2018-05-24 Hristian Kirtchev gcc/ada/ * expander.adb (Expand): Update the save and restore of the Ghost region. * exp_ch3.adb (Freeze_Type): Likewise. * exp_disp.adb (Make_DT): Likewise. * exp_util.adb (Build_DIC_Procedure_Body): Likewise. (Build_DIC_Procedure_Declaration): Likewise. (Build_Invariant_Procedure_Body): Likewise. (Build_Invariant_Procedure_Declaration): Likewise. (Make_Predicate_Call): Likewise. * freeze.adb (Add_To_Result): Insert the freeze action of a living entity prior to the start of the enclosing ignored Ghost region. (Freeze_Entity): Update the save and restore of the Ghost region. * ghost.adb (Install_Ghost_Mode): Reimplemented. (Install_Ghost_Region): New routine. (Mark_And_Set_Ghost_Assignment): Install a region rather than a mode. (Mark_And_Set_Ghost_Body): Likewise. (Mark_And_Set_Ghost_Completion): Likewise. (Mark_And_Set_Ghost_Declaration): Likewise. (Mark_And_Set_Ghost_Instantiation): Likewise. (Mark_And_Set_Ghost_Procedure_Call): Likewise. (Name_To_Ghost_Mode): New routine. (Restore_Ghost_Region): New routine. * ghost.ads (Install_Ghost_Region): New routine. (Restore_Ghost_Region): New routine. * opt.ads: Add new global variable Ignored_Ghost_Region. * rtsfind.adb (Load_RTU): Update the save and restore of the Ghost region. Install a clean region. * sem.adb (Analyze): Likewise. (Do_Analyze): Likewise. * sem_ch3.adb (Analyze_Object_Declaration): Likewise (Derive_Progenitor_Subprograms): Use local variable Iface_Alias to capture the ultimate alias of the current primitive. (Process_Full_View): Update the save and restore of the Ghost region. Do not inherit DIC and invariant procedures. * sem_ch5.adb (Analyze_Assignment): Update the save and restore of the Ghost region. * sem_ch6.adb (Analyze_Procedure_Call): Likewise. (Analyze_Subprogram_Body_Helper): Likewise. * sem_ch7.adb (Analyze_Package_Body_Helper): Likewise. * sem_ch12.adb (Analyze_Package_Instantiation): Likewise. (Analyze_Subprogram_Instantiation): Likewise. (Instantiate_Package_Body): Likewise. (Instantiate_Subprogram_Body): Likewise. * sem_ch13.adb (Build_Predicate_Functions): Likewise. (Build_Predicate_Function_Declaration): Likewise. * sem_disp.adb (Add_Dispatching_Operation): Do not consider DIC and invariant procedures. (Check_Dispatching_Operation): Use Add_Dispatching_Operation to collect a dispatching subprogram. (Check_Operation_From_Private_View): Likewise. (Override_Dispatching_Operation): Likewise. * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Update the save and restore of the Ghost region. (Analyze_Initial_Condition_In_Decl_Part): Likewise. (Analyze_Pragma): Update the save and restore of the Ghost region. (Analyze_Pre_Post_Condition_In_Decl_Part): Likewise. * sem_util.adb (Is_Suitable_Primitive): New routine. * sem_util.ads (Is_Suitable_Primitive): New routine. * sinfo.ads: Update the section of Ghost regions. gcc/testsuite/ * gnat.dg/formal_containers.adb: New testcase. From-SVN: r260648 --- gcc/ada/ChangeLog | 63 ++++++++++++++ gcc/ada/exp_ch3.adb | 9 +- gcc/ada/exp_disp.adb | 7 +- gcc/ada/exp_util.adb | 35 ++++---- gcc/ada/expander.adb | 7 +- gcc/ada/freeze.adb | 41 ++++++---- gcc/ada/ghost.adb | 123 ++++++++++++++++++++-------- gcc/ada/ghost.ads | 34 ++++---- gcc/ada/opt.ads | 8 +- gcc/ada/rtsfind.adb | 15 ++-- gcc/ada/sem.adb | 22 +++-- gcc/ada/sem_ch12.adb | 28 ++++--- gcc/ada/sem_ch13.adb | 14 ++-- gcc/ada/sem_ch3.adb | 52 ++++++------ gcc/ada/sem_ch5.adb | 7 +- gcc/ada/sem_ch6.adb | 10 ++- gcc/ada/sem_ch7.adb | 3 +- gcc/ada/sem_disp.adb | 17 +++- gcc/ada/sem_prag.adb | 31 ++++--- gcc/ada/sem_util.adb | 23 ++++++ gcc/ada/sem_util.ads | 4 + gcc/ada/sinfo.ads | 66 +++++++++------ gcc/testsuite/ChangeLog | 4 + gcc/testsuite/gnat.dg/formal_containers.adb | 23 ++++++ 24 files changed, 451 insertions(+), 195 deletions(-) create mode 100644 gcc/testsuite/gnat.dg/formal_containers.adb diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 219fa8b..cad2b78 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,66 @@ +2018-05-24 Hristian Kirtchev + + * expander.adb (Expand): Update the save and restore of the Ghost + region. + * exp_ch3.adb (Freeze_Type): Likewise. + * exp_disp.adb (Make_DT): Likewise. + * exp_util.adb (Build_DIC_Procedure_Body): Likewise. + (Build_DIC_Procedure_Declaration): Likewise. + (Build_Invariant_Procedure_Body): Likewise. + (Build_Invariant_Procedure_Declaration): Likewise. + (Make_Predicate_Call): Likewise. + * freeze.adb (Add_To_Result): Insert the freeze action of a living + entity prior to the start of the enclosing ignored Ghost region. + (Freeze_Entity): Update the save and restore of the Ghost region. + * ghost.adb (Install_Ghost_Mode): Reimplemented. + (Install_Ghost_Region): New routine. + (Mark_And_Set_Ghost_Assignment): Install a region rather than a mode. + (Mark_And_Set_Ghost_Body): Likewise. + (Mark_And_Set_Ghost_Completion): Likewise. + (Mark_And_Set_Ghost_Declaration): Likewise. + (Mark_And_Set_Ghost_Instantiation): Likewise. + (Mark_And_Set_Ghost_Procedure_Call): Likewise. + (Name_To_Ghost_Mode): New routine. + (Restore_Ghost_Region): New routine. + * ghost.ads (Install_Ghost_Region): New routine. + (Restore_Ghost_Region): New routine. + * opt.ads: Add new global variable Ignored_Ghost_Region. + * rtsfind.adb (Load_RTU): Update the save and restore of the Ghost + region. Install a clean region. + * sem.adb (Analyze): Likewise. + (Do_Analyze): Likewise. + * sem_ch3.adb (Analyze_Object_Declaration): Likewise + (Derive_Progenitor_Subprograms): Use local variable Iface_Alias to + capture the ultimate alias of the current primitive. + (Process_Full_View): Update the save and restore of the Ghost region. + Do not inherit DIC and invariant procedures. + * sem_ch5.adb (Analyze_Assignment): Update the save and restore of the + Ghost region. + * sem_ch6.adb (Analyze_Procedure_Call): Likewise. + (Analyze_Subprogram_Body_Helper): Likewise. + * sem_ch7.adb (Analyze_Package_Body_Helper): Likewise. + * sem_ch12.adb (Analyze_Package_Instantiation): Likewise. + (Analyze_Subprogram_Instantiation): Likewise. + (Instantiate_Package_Body): Likewise. + (Instantiate_Subprogram_Body): Likewise. + * sem_ch13.adb (Build_Predicate_Functions): Likewise. + (Build_Predicate_Function_Declaration): Likewise. + * sem_disp.adb + (Add_Dispatching_Operation): Do not consider DIC and invariant + procedures. + (Check_Dispatching_Operation): Use Add_Dispatching_Operation to collect + a dispatching subprogram. + (Check_Operation_From_Private_View): Likewise. + (Override_Dispatching_Operation): Likewise. + * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Update the save + and restore of the Ghost region. + (Analyze_Initial_Condition_In_Decl_Part): Likewise. + (Analyze_Pragma): Update the save and restore of the Ghost region. + (Analyze_Pre_Post_Condition_In_Decl_Part): Likewise. + * sem_util.adb (Is_Suitable_Primitive): New routine. + * sem_util.ads (Is_Suitable_Primitive): New routine. + * sinfo.ads: Update the section of Ghost regions. + 2018-05-24 Piotr Trojanek * doc/gnat_rm/implementation_defined_pragmas.rst (Contract_Cases): diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index 3c1bede..4c5d940 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -7554,8 +7554,9 @@ package body Exp_Ch3 is Def_Id : constant Entity_Id := Entity (N); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit Result : Boolean := False; @@ -7920,13 +7921,13 @@ package body Exp_Ch3 is end if; end if; - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); return Result; exception when RE_Not_Available => - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); return False; end Freeze_Type; diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb index 0d674e7..0a63645 100644 --- a/gcc/ada/exp_disp.adb +++ b/gcc/ada/exp_disp.adb @@ -4516,8 +4516,9 @@ package body Exp_Disp is Name_TSD : constant Name_Id := New_External_Name (Tname, 'B', Suffix_Index => -1); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit AI : Elmt_Id; AI_Tag_Elmt : Elmt_Id; @@ -6545,7 +6546,7 @@ package body Exp_Disp is Register_CG_Node (Typ); <> - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); return Result; end Make_DT; diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 2f3068d..5ede9a6 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1578,8 +1578,9 @@ package body Exp_Util is Loc : constant Source_Ptr := Sloc (Typ); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit DIC_Prag : Node_Id; DIC_Typ : Entity_Id; @@ -1814,7 +1815,7 @@ package body Exp_Util is end if; <> - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Build_DIC_Procedure_Body; ------------------------------------- @@ -1828,8 +1829,9 @@ package body Exp_Util is procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is Loc : constant Source_Ptr := Sloc (Typ); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit DIC_Prag : Node_Id; DIC_Typ : Entity_Id; @@ -2015,7 +2017,7 @@ package body Exp_Util is end if; <> - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Build_DIC_Procedure_Declaration; ------------------------------------ @@ -2945,8 +2947,9 @@ package body Exp_Util is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit Dummy : Entity_Id; Priv_Item : Node_Id; @@ -3286,7 +3289,7 @@ package body Exp_Util is end if; <> - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Build_Invariant_Procedure_Body; ------------------------------------------- @@ -3303,8 +3306,9 @@ package body Exp_Util is is Loc : constant Source_Ptr := Sloc (Typ); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit Proc_Decl : Node_Id; Proc_Id : Entity_Id; @@ -3519,7 +3523,7 @@ package body Exp_Util is end if; <> - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Build_Invariant_Procedure_Declaration; -------------------------- @@ -9256,8 +9260,9 @@ package body Exp_Util is is Loc : constant Source_Ptr := Sloc (Expr); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit Call : Node_Id; Func_Id : Entity_Id; @@ -9296,7 +9301,7 @@ package body Exp_Util is Parameter_Associations => New_List (Relocate_Node (Expr))); end if; - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); return Call; end Make_Predicate_Call; diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb index e26daf5..2e552cd 100644 --- a/gcc/ada/expander.adb +++ b/gcc/ada/expander.adb @@ -82,8 +82,9 @@ package body Expander is -- Ghost mode. procedure Expand (N : Node_Id) is - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit begin -- If we were analyzing a default expression (or other spec expression) @@ -530,7 +531,7 @@ package body Expander is end if; <> - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Expand; --------------------------- diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index a95a367..50485f1 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -2165,7 +2165,12 @@ package body Freeze is N : Node_Id; Do_Freeze_Profile : Boolean := True) return List_Id is - Loc : constant Source_Ptr := Sloc (N); + Loc : constant Source_Ptr := Sloc (N); + + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit + Atype : Entity_Id; Comp : Entity_Id; F_Node : Node_Id; @@ -2181,8 +2186,8 @@ package body Freeze is Test_E : Entity_Id := E; -- This could use a comment ??? - procedure Add_To_Result (N : Node_Id); - -- N is a freezing action to be appended to the Result + procedure Add_To_Result (Fnod : Node_Id); + -- Add freeze action Fnod to list Result function After_Last_Declaration return Boolean; -- If Loc is a freeze_entity that appears after the last declaration @@ -2244,12 +2249,24 @@ package body Freeze is -- Add_To_Result -- ------------------- - procedure Add_To_Result (N : Node_Id) is + procedure Add_To_Result (Fnod : Node_Id) is begin - if No (Result) then - Result := New_List (N); + -- The Ghost mode of the enclosing context is ignored, while the + -- entity being frozen is living. Insert the freezing action prior + -- to the start of the enclosing ignored Ghost region. As a result + -- the freezeing action will be preserved when the ignored Ghost + -- context is eliminated. + + if Saved_GM = Ignore + and then Ghost_Mode /= Ignore + and then Present (Ignored_Ghost_Region) + then + Insert_Action (Ignored_Ghost_Region, Fnod); + + -- Otherwise add the freezing action to the result list + else - Append (N, Result); + Append_New_To (Result, Fnod); end if; end Add_To_Result; @@ -3188,7 +3205,6 @@ package body Freeze is ------------------------------- procedure Freeze_Object_Declaration (E : Entity_Id) is - procedure Check_Large_Modular_Array (Typ : Entity_Id); -- Check that the size of array type Typ can be computed without -- overflow, and generates a Storage_Error otherwise. This is only @@ -5173,7 +5189,7 @@ package body Freeze is -- Build the call -- An imported function whose result type is anonymous access - -- creates a new anonynous access type when it is relocated into + -- creates a new anonymous access type when it is relocated into -- the declarations of the body generated below. As a result, the -- accessibility level of these two anonymous access types may not -- be compatible even though they are essentially the same type. @@ -5231,11 +5247,6 @@ package body Freeze is end if; end Wrap_Imported_Subprogram; - -- Local variables - - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit - -- Start of processing for Freeze_Entity begin @@ -6854,7 +6865,7 @@ package body Freeze is end if; <> - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); return Result; end Freeze_Entity; diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 5997724..fe56691 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -46,6 +46,10 @@ with Table; package body Ghost is + --------------------- + -- Data strictures -- + --------------------- + -- The following table contains the N_Compilation_Unit node for a unit that -- is either subject to pragma Ghost with policy Ignore or contains ignored -- Ghost code. The table is used in the removal of ignored Ghost code from @@ -60,16 +64,21 @@ package body Ghost is Table_Name => "Ignored_Ghost_Units"); ----------------------- - -- Local Subprograms -- + -- Local subprograms -- ----------------------- function Ghost_Entity (N : Node_Id) return Entity_Id; -- Find the entity of a reference to a Ghost entity. Return Empty if there -- is no such entity. - procedure Install_Ghost_Mode (Mode : Name_Id); - -- Install a specific Ghost mode denoted by Mode by setting global variable - -- Ghost_Mode. + procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type); + pragma Inline (Install_Ghost_Mode); + -- Install Ghost mode Mode as the Ghost mode in effect + + procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id); + pragma Inline (Install_Ghost_Region); + -- Install a Ghost region comprised of mode Mode and ignored region start + -- node N. function Is_Subject_To_Ghost (N : Node_Id) return Boolean; -- Determine whether declaration or body N is subject to aspect or pragma @@ -84,6 +93,11 @@ package body Ghost is -- mode Mode. Mark all formals parameters when N denotes a subprogram or a -- body. + function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type; + pragma Inline (Name_To_Ghost_Mode); + -- Convert a Ghost mode denoted by name Mode into its respective enumerated + -- value. + procedure Propagate_Ignored_Ghost_Code (N : Node_Id); -- Signal all enclosing scopes that they now contain at least one ignored -- Ghost node denoted by N. Add the compilation unit containing N to table @@ -908,21 +922,40 @@ package body Ghost is procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is begin - Ghost_Mode := Mode; + Install_Ghost_Region (Mode, Empty); end Install_Ghost_Mode; - procedure Install_Ghost_Mode (Mode : Name_Id) is + -------------------------- + -- Install_Ghost_Region -- + -------------------------- + + procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is begin - if Mode = Name_Check then - Ghost_Mode := Check; + -- The context is already within an ignored Ghost region. Maintain the + -- start of the outermost ignored Ghost region. - elsif Mode = Name_Ignore then - Ghost_Mode := Ignore; + if Present (Ignored_Ghost_Region) then + null; + + -- The current region is the outermost ignored Ghost region. Save its + -- starting node. + + elsif Present (N) and then Mode = Ignore then + Ignored_Ghost_Region := N; - elsif Mode = Name_None then - Ghost_Mode := None; + -- Otherwise the current region is not ignored, nothing to save + + else + Ignored_Ghost_Region := Empty; end if; - end Install_Ghost_Mode; + + Ghost_Mode := Mode; + end Install_Ghost_Region; + + procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id) is + begin + Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N); + end Install_Ghost_Region; ------------------------- -- Is_Ghost_Assignment -- @@ -1162,10 +1195,10 @@ package body Ghost is if Present (Id) then if Is_Checked_Ghost_Entity (Id) then - Install_Ghost_Mode (Check); + Install_Ghost_Region (Check, N); elsif Is_Ignored_Ghost_Entity (Id) then - Install_Ghost_Mode (Ignore); + Install_Ghost_Region (Ignore, N); Set_Is_Ignored_Ghost_Node (N); Propagate_Ignored_Ghost_Code (N); @@ -1222,9 +1255,9 @@ package body Ghost is Mark_Ghost_Declaration_Or_Body (N, Policy); - -- Install the appropriate Ghost mode + -- Install the appropriate Ghost region - Install_Ghost_Mode (Policy); + Install_Ghost_Region (Policy, N); end Mark_And_Set_Ghost_Body; ----------------------------------- @@ -1269,9 +1302,9 @@ package body Ghost is Mark_Ghost_Declaration_Or_Body (N, Policy); - -- Install the appropriate Ghost mode + -- Install the appropriate Ghost region - Install_Ghost_Mode (Policy); + Install_Ghost_Region (Policy, N); end Mark_And_Set_Ghost_Completion; ------------------------------------ @@ -1326,9 +1359,9 @@ package body Ghost is Mark_Ghost_Declaration_Or_Body (N, Policy); - -- Install the appropriate Ghost mode + -- Install the appropriate Ghost region - Install_Ghost_Mode (Policy); + Install_Ghost_Region (Policy, N); end Mark_And_Set_Ghost_Declaration; -------------------------------------- @@ -1406,11 +1439,11 @@ package body Ghost is Mark_Ghost_Declaration_Or_Body (N, Policy); - -- Install the appropriate Ghost mode + -- Install the appropriate Ghost region - Install_Ghost_Mode (Policy); + Install_Ghost_Region (Policy, N); - -- Check ghost actuals. Given that this routine is unconditionally + -- Check Ghost actuals. Given that this routine is unconditionally -- invoked with subprogram and package instantiations, this check -- verifies the context of all the ghost entities passed in generic -- instantiations. @@ -1433,10 +1466,10 @@ package body Ghost is if Present (Id) then if Is_Checked_Ghost_Entity (Id) then - Install_Ghost_Mode (Check); + Install_Ghost_Region (Check, N); elsif Is_Ignored_Ghost_Entity (Id) then - Install_Ghost_Mode (Ignore); + Install_Ghost_Region (Ignore, N); Set_Is_Ignored_Ghost_Node (N); Propagate_Ignored_Ghost_Code (N); @@ -1577,6 +1610,31 @@ package body Ghost is Mark_Ghost_Declaration_Or_Body (N, Policy); end Mark_Ghost_Renaming; + ------------------------ + -- Name_To_Ghost_Mode -- + ------------------------ + + function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type is + begin + if Mode = Name_Check then + return Check; + + elsif Mode = Name_Ignore then + return Ignore; + + -- Otherwise the mode must denote one of the following: + -- + -- * Disable indicates that the Ghost policy in effect is Disable + -- + -- * None or No_Name indicates that the associated construct is not + -- subject to any Ghost annotation. + + else + pragma Assert (Nam_In (Mode, Name_Disable, Name_None, No_Name)); + return None; + end if; + end Name_To_Ghost_Mode; + ---------------------------------- -- Propagate_Ignored_Ghost_Code -- ---------------------------------- @@ -1742,14 +1800,15 @@ package body Ghost is end loop; end Remove_Ignored_Ghost_Code; - ------------------------ - -- Restore_Ghost_Mode -- - ------------------------ + -------------------------- + -- Restore_Ghost_Region -- + -------------------------- - procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type) is + procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is begin - Ghost_Mode := Mode; - end Restore_Ghost_Mode; + Ghost_Mode := Mode; + Ignored_Ghost_Region := N; + end Restore_Ghost_Region; -------------------- -- Set_Ghost_Mode -- diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 8e23bcf..ef95116 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -78,9 +78,10 @@ package Ghost is procedure Initialize; -- Initialize internal tables - procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type); - -- Set the value of global variable Ghost_Mode depending on the Ghost - -- policy denoted by Mode. + procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id); + pragma Inline (Install_Ghost_Region); + -- Install a Ghost region described by mode Mode and ignored region start + -- node N. function Is_Ghost_Assignment (N : Node_Id) return Boolean; -- Determine whether arbitrary node N denotes an assignment statement whose @@ -111,7 +112,7 @@ package Ghost is -- * The left hand side denotes a Ghost entity -- -- Install the Ghost mode of the assignment statement. This routine starts - -- a Ghost region and must be used in conjunction with Restore_Ghost_Mode. + -- a Ghost region and must be used with routine Restore_Ghost_Region. procedure Mark_And_Set_Ghost_Body (N : Node_Id; @@ -126,7 +127,7 @@ package Ghost is -- * The body appears within a Ghost region -- -- Install the Ghost mode of the body. This routine starts a Ghost region - -- and must be used in conjunction with Restore_Ghost_Mode. + -- and must be used with routine Restore_Ghost_Region. procedure Mark_And_Set_Ghost_Completion (N : Node_Id; @@ -139,7 +140,7 @@ package Ghost is -- * The completion appears within a Ghost region -- -- Install the Ghost mode of the completion. This routine starts a Ghost - -- region and must be used in conjunction with Restore_Ghost_Mode. + -- region and must be used with routine Restore_Ghost_Region. procedure Mark_And_Set_Ghost_Declaration (N : Node_Id); -- Mark declaration N as Ghost when: @@ -152,7 +153,7 @@ package Ghost is -- * The declaration appears within a Ghost region -- -- Install the Ghost mode of the declaration. This routine starts a Ghost - -- region and must be used in conjunction with Restore_Ghost_Mode. + -- region and must be used with routine Restore_Ghost_Region. procedure Mark_And_Set_Ghost_Instantiation (N : Node_Id; @@ -166,7 +167,7 @@ package Ghost is -- * The instantiation appears within a Ghost region -- -- Install the Ghost mode of the instantiation. This routine starts a Ghost - -- region and must be used in conjunction with Restore_Ghost_Mode. + -- region and must be used with routine Restore_Ghost_Region. procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id); -- Mark procedure call N as Ghost when: @@ -174,7 +175,7 @@ package Ghost is -- * The procedure being invoked is a Ghost entity -- -- Install the Ghost mode of the procedure call. This routine starts a - -- Ghost region and must be used in conjunction with Restore_Ghost_Mode. + -- Ghost region and must be used with routine Restore_Ghost_Region. procedure Mark_Ghost_Clause (N : Node_Id); -- Mark use package, use type, or with clause N as Ghost when: @@ -204,14 +205,19 @@ package Ghost is -- WARNING: this is a separate front end pass, care should be taken to keep -- it optimized. - procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type); - -- Terminate a Ghost region by restoring the Ghost mode prior to the - -- region denoted by Mode. This routine must be used in conjunction - -- with Mark_And_Set_xxx routines as well as Set_Ghost_Mode. + procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id); + pragma Inline (Restore_Ghost_Region); + -- Restore a Ghost region to a previous state described by mode Mode and + -- ignored region start node N. This routine must be used in conjunction + -- with the following routines: + -- + -- Install_Ghost_Region + -- Mark_And_Set_xxx + -- Set_Ghost_Mode procedure Set_Ghost_Mode (N : Node_Or_Entity_Id); -- Install the Ghost mode of arbitrary node N. This routine starts a Ghost - -- region and must be used in conjunction with Restore_Ghost_Mode. + -- region and must be used with routine Restore_Ghost_Region. procedure Set_Is_Ghost_Entity (Id : Entity_Id); -- Set the relevant Ghost attributes of entity Id depending on the current diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index e98f885..2d57e1c 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -786,7 +786,7 @@ package Opt is Ghost_Mode : Ghost_Mode_Type := None; -- GNAT - -- Current Ghost mode setting + -- The current Ghost mode in effect Global_Discard_Names : Boolean := False; -- GNAT, GNATBIND @@ -848,6 +848,12 @@ package Opt is -- use of -gnateu, causing subsequent unrecognized switches to result in -- a warning rather than an error. + Ignored_Ghost_Region : Node_Id := Empty; + -- GNAT + -- The start of the current ignored Ghost region. This value must always + -- reflect the starting node of the outermost ignored Ghost region. If a + -- nested ignored Ghost region is entered, the value must remain unchanged. + Implementation_Unit_Warnings : Boolean := True; -- GNAT -- Set True to active warnings for use of implementation internal units. diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb index 63d8a00..bc3d675 100644 --- a/gcc/ada/rtsfind.adb +++ b/gcc/ada/rtsfind.adb @@ -929,9 +929,10 @@ package body Rtsfind is -- Local variables - Save_GM : constant Ghost_Mode_Type := Ghost_Mode; - Save_SM : constant SPARK_Mode_Type := SPARK_Mode; - Save_SMP : constant Node_Id := SPARK_Mode_Pragma; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; + Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; -- Save Ghost and SPARK mode-related data to restore on exit -- Start of processing for Load_RTU @@ -945,8 +946,8 @@ package body Rtsfind is -- Provide a clean environment for the unit - Install_Ghost_Mode (None); - Install_SPARK_Mode (None, Empty); + Install_Ghost_Region (None, Empty); + Install_SPARK_Mode (None, Empty); -- Note if secondary stack is used @@ -1049,8 +1050,8 @@ package body Rtsfind is Set_Is_Potentially_Use_Visible (U.Entity, True); end if; - Restore_Ghost_Mode (Save_GM); - Restore_SPARK_Mode (Save_SM, Save_SMP); + Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Load_RTU; -------------------- diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index 4987845..ca87496 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.adb @@ -101,8 +101,9 @@ package body Sem is -- Ghost mode. procedure Analyze (N : Node_Id) is - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit begin Debug_A_Entry ("analyzing ", N); @@ -803,7 +804,7 @@ package body Sem is Expand_SPARK_Potential_Renaming (N); end if; - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Analyze; -- Version with check(s) suppressed @@ -1351,14 +1352,16 @@ package body Sem is -- the Ghost mode. procedure Do_Analyze is - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit -- Generally style checks are preserved across compilations, with -- one exception: s-oscons.ads, which allows arbitrary long lines -- unconditionally, and has no restore mechanism, because it is -- intended as a lowest-level Pure package. - Save_Max_Line : constant Int := Style_Max_Line_Length; + Saved_ML : constant Int := Style_Max_Line_Length; List : Elist_Id; @@ -1368,7 +1371,8 @@ package body Sem is -- Set up a clean environment before analyzing - Install_Ghost_Mode (None); + Install_Ghost_Region (None, Empty); + Outer_Generic_Scope := Empty; Scope_Suppress := Suppress_Options; Scope_Stack.Table @@ -1389,9 +1393,9 @@ package body Sem is -- Then pop entry for Standard, and pop implicit types Pop_Scope; - Restore_Scope_Stack (List); - Restore_Ghost_Mode (Save_Ghost_Mode); - Style_Max_Line_Length := Save_Max_Line; + Restore_Scope_Stack (List); + Restore_Ghost_Region (Saved_GM, Saved_IGR); + Style_Max_Line_Length := Saved_ML; end Do_Analyze; -- Local variables diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 6bfe989..c8d4df0 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3909,6 +3909,7 @@ package body Sem_Ch12 is Loc : constant Source_Ptr := Sloc (N); Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; @@ -4736,8 +4737,8 @@ package body Sem_Ch12 is end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Mode (Saved_GM); - Restore_SPARK_Mode (Saved_SM, Saved_SMP); + Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); Style_Check := Saved_Style_Check; exception @@ -4751,8 +4752,8 @@ package body Sem_Ch12 is end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Mode (Saved_GM); - Restore_SPARK_Mode (Saved_SM, Saved_SMP); + Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); Style_Check := Saved_Style_Check; end Analyze_Package_Instantiation; @@ -5399,6 +5400,7 @@ package body Sem_Ch12 is -- Local variables Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; @@ -5773,8 +5775,8 @@ package body Sem_Ch12 is end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Mode (Saved_GM); - Restore_SPARK_Mode (Saved_SM, Saved_SMP); + Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); exception when Instantiation_Error => @@ -5787,8 +5789,8 @@ package body Sem_Ch12 is end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Mode (Saved_GM); - Restore_SPARK_Mode (Saved_SM, Saved_SMP); + Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Analyze_Subprogram_Instantiation; ------------------------- @@ -11271,6 +11273,7 @@ package body Sem_Ch12 is -- Local variables Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; -- Save the Ghost and SPARK mode-related data to restore on exit @@ -11600,8 +11603,8 @@ package body Sem_Ch12 is <> Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Mode (Saved_GM); - Restore_SPARK_Mode (Saved_SM, Saved_SMP); + Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); Style_Check := Saved_Style_Check; end Instantiate_Package_Body; @@ -11628,6 +11631,7 @@ package body Sem_Ch12 is Defining_Unit_Name (Parent (Act_Decl)); Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; @@ -11929,8 +11933,8 @@ package body Sem_Ch12 is <> Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Mode (Saved_GM); - Restore_SPARK_Mode (Saved_SM, Saved_SMP); + Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_SPARK_Mode (Saved_SM, Saved_SMP); Style_Check := Saved_Style_Check; end Instantiate_Subprogram_Body; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index c0118b4..74bfd42 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -8666,8 +8666,9 @@ package body Sem_Ch13 is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit -- Start of processing for Build_Predicate_Functions @@ -9041,7 +9042,7 @@ package body Sem_Ch13 is end; end if; - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Build_Predicate_Functions; ------------------------------------------ @@ -9057,8 +9058,9 @@ package body Sem_Ch13 is is Loc : constant Source_Ptr := Sloc (Typ); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit Func_Decl : Node_Id; Func_Id : Entity_Id; @@ -9102,7 +9104,7 @@ package body Sem_Ch13 is Insert_After (Parent (Typ), Func_Decl); Analyze (Func_Decl); - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); return Func_Decl; end Build_Predicate_Function_Declaration; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 4887e86..57a662a 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -3905,8 +3905,9 @@ package body Sem_Ch3 is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit Related_Id : Entity_Id; @@ -4970,7 +4971,7 @@ package body Sem_Ch3 is Check_No_Hidden_State (Id); end if; - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Analyze_Object_Declaration; --------------------------- @@ -15003,15 +15004,16 @@ package body Sem_Ch3 is (Parent_Type : Entity_Id; Tagged_Type : Entity_Id) is - E : Entity_Id; - Elmt : Elmt_Id; - Iface : Entity_Id; - Iface_Elmt : Elmt_Id; - Iface_Subp : Entity_Id; - New_Subp : Entity_Id := Empty; - Prim_Elmt : Elmt_Id; - Subp : Entity_Id; - Typ : Entity_Id; + E : Entity_Id; + Elmt : Elmt_Id; + Iface : Entity_Id; + Iface_Alias : Entity_Id; + Iface_Elmt : Elmt_Id; + Iface_Subp : Entity_Id; + New_Subp : Entity_Id := Empty; + Prim_Elmt : Elmt_Id; + Subp : Entity_Id; + Typ : Entity_Id; begin pragma Assert (Ada_Version >= Ada_2005 @@ -15082,7 +15084,8 @@ package body Sem_Ch3 is Prim_Elmt := First_Elmt (Primitive_Operations (Iface)); while Present (Prim_Elmt) loop - Iface_Subp := Node (Prim_Elmt); + Iface_Subp := Node (Prim_Elmt); + Iface_Alias := Ultimate_Alias (Iface_Subp); -- Exclude derivation of predefined primitives except those -- that come from source, or are inherited from one that comes @@ -15093,11 +15096,12 @@ package body Sem_Ch3 is -- function "=" (Left, Right : Iface) return Boolean; if not Is_Predefined_Dispatching_Operation (Iface_Subp) - or else Comes_From_Source (Ultimate_Alias (Iface_Subp)) + or else Comes_From_Source (Iface_Alias) then - E := Find_Primitive_Covering_Interface - (Tagged_Type => Tagged_Type, - Iface_Prim => Iface_Subp); + E := + Find_Primitive_Covering_Interface + (Tagged_Type => Tagged_Type, + Iface_Prim => Iface_Subp); -- If not found we derive a new primitive leaving its alias -- attribute referencing the interface primitive. @@ -20265,7 +20269,9 @@ package body Sem_Ch3 is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit Full_Indic : Node_Id; Full_Parent : Entity_Id; @@ -20749,7 +20755,6 @@ package body Sem_Ch3 is else Full_List := Primitive_Operations (Full_T); - while Present (Prim_Elmt) loop Prim := Node (Prim_Elmt); @@ -20791,16 +20796,17 @@ package body Sem_Ch3 is then Check_Controlling_Formals (Full_T, Prim); - if not Is_Dispatching_Operation (Prim) then + if Is_Suitable_Primitive (Prim) + and then not Is_Dispatching_Operation (Prim) + then Append_Elmt (Prim, Full_List); - Set_Is_Dispatching_Operation (Prim, True); + Set_Is_Dispatching_Operation (Prim); Set_DT_Position_Value (Prim, No_Uint); end if; elsif Is_Dispatching_Operation (Prim) and then Disp_Typ /= Full_T then - -- Verify that it is not otherwise controlled by a -- formal or a return value of type T. @@ -20927,7 +20933,7 @@ package body Sem_Ch3 is end if; <> - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Process_Full_View; ----------------------------------- diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 0da972a..f18fd40 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -450,8 +450,9 @@ package body Sem_Ch5 is Save_Full_Analysis : Boolean := False; -- Force initialization to facilitate static analysis - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit -- Start of processing for Analyze_Assignment @@ -1197,7 +1198,7 @@ package body Sem_Ch5 is Analyze_Dimension (N); <> - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); -- If the right-hand side contains target names, expansion has been -- disabled to prevent expansion that might move target names out of diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 997f4ed..e838e6a 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1799,8 +1799,9 @@ package body Sem_Ch6 is Loc : constant Source_Ptr := Sloc (N); P : constant Node_Id := Name (N); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit Actual : Node_Id; New_N : Node_Id; @@ -2043,7 +2044,7 @@ package body Sem_Ch6 is end if; <> - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Analyze_Procedure_Call; ------------------------------ @@ -3505,6 +3506,7 @@ package body Sem_Ch6 is -- Local variables Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; -- Save the Ghost and SPARK mode-related data to restore on exit @@ -4720,7 +4722,7 @@ package body Sem_Ch6 is <> Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Analyze_Subprogram_Body_Helper; ------------------------------------ diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index b20f77c..866c6f9 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -638,6 +638,7 @@ package body Sem_Ch7 is -- Local variables Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; -- Save the Ghost and SPARK mode-related data to restore on exit @@ -1045,7 +1046,7 @@ package body Sem_Ch7 is end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Analyze_Package_Body_Helper; --------------------------------- diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb index 9c9fe24..69c2a56 100644 --- a/gcc/ada/sem_disp.adb +++ b/gcc/ada/sem_disp.adb @@ -106,7 +106,16 @@ package body Sem_Disp is -- for the construction of function wrappers). The list of primitive -- operations must not contain duplicates. - Append_Unique_Elmt (New_Op, List); + -- The Default_Initial_Condition and invariant procedures are not added + -- to the list of primitives even when they are generated for a tagged + -- type. These routines must not be targets of dispatching calls and + -- therefore must not appear in the dispatch table because they already + -- utilize class-wide-precondition semantics to handle inheritance and + -- overriding. + + if Is_Suitable_Primitive (New_Op) then + Append_Unique_Elmt (New_Op, List); + end if; end Add_Dispatching_Operation; -------------------------- @@ -1472,7 +1481,7 @@ package body Sem_Disp is -- Attach operation to list of primitives of the synchronized type -- itself, for ASIS use. - Append_Elmt (Subp, Direct_Primitive_Operations (Tagged_Type)); + Add_Dispatching_Operation (Tagged_Type, Subp); -- If no old subprogram, then we add this as a dispatching operation, -- but we avoid doing this if an error was posted, to prevent annoying @@ -1783,7 +1792,7 @@ package body Sem_Disp is -- Add Old_Subp to primitive operations if not already present if Present (Tagged_Type) and then Is_Tagged_Type (Tagged_Type) then - Append_Unique_Elmt (Old_Subp, Primitive_Operations (Tagged_Type)); + Add_Dispatching_Operation (Tagged_Type, Old_Subp); -- If Old_Subp isn't already marked as dispatching then this is -- the case of an operation of an untagged private type fulfilled @@ -2541,7 +2550,7 @@ package body Sem_Disp is Find_Dispatching_Type (Alias (Prev_Op))) then Remove_Elmt (Primitive_Operations (Tagged_Type), Elmt); - Append_Elmt (New_Op, Primitive_Operations (Tagged_Type)); + Add_Dispatching_Operation (Tagged_Type, New_Op); -- The new primitive replaces the overridden entity. Required to ensure -- that overriding primitive is assigned the same dispatch table slot. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 21ef6cb..d75f20e 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -468,8 +468,9 @@ package body Sem_Prag is CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit CCase : Node_Id; Restore_Scope : Boolean := False; @@ -536,7 +537,7 @@ package body Sem_Prag is Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Analyze_Contract_Cases_In_Decl_Part; ---------------------------------- @@ -2720,8 +2721,9 @@ package body Sem_Prag is Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl); Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit begin -- Do not analyze the pragma multiple times @@ -2744,7 +2746,7 @@ package body Sem_Prag is Preanalyze_Assert_Expression (Expr, Standard_Boolean); Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Analyze_Initial_Condition_In_Decl_Part; -------------------------------------- @@ -13224,8 +13226,9 @@ package body Sem_Prag is -- restore the Ghost mode. when Pragma_Check => Check : declare - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit Cname : Name_Id; Eloc : Source_Ptr; @@ -13420,7 +13423,7 @@ package body Sem_Prag is In_Assertion_Expr := In_Assertion_Expr - 1; end if; - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Check; -------------------------- @@ -24968,9 +24971,11 @@ package body Sem_Prag is -- Local variables - Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - -- Save the Ghost mode to restore on exit + Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); + + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit Errors : Nat; Restore_Scope : Boolean := False; @@ -25069,7 +25074,7 @@ package body Sem_Prag is Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Mode (Saved_GM); + Restore_Ghost_Region (Saved_GM, Saved_IGR); end Analyze_Pre_Post_Condition_In_Decl_Part; ------------------------------------------ diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 76b4fb0..4e12f93 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -17192,6 +17192,29 @@ package body Sem_Util is and then Ekind (Defining_Entity (N)) /= E_Subprogram_Body; end Is_Subprogram_Stub_Without_Prior_Declaration; + --------------------------- + -- Is_Suitable_Primitive -- + --------------------------- + + function Is_Suitable_Primitive (Subp_Id : Entity_Id) return Boolean is + begin + -- The Default_Initial_Condition and invariant procedures must not be + -- treated as primitive operations even when they apply to a tagged + -- type. These routines must not act as targets of dispatching calls + -- because they already utilize class-wide-precondition semantics to + -- handle inheritance and overriding. + + if Ekind (Subp_Id) = E_Procedure + and then (Is_DIC_Procedure (Subp_Id) + or else + Is_Invariant_Procedure (Subp_Id)) + then + return False; + end if; + + return True; + end Is_Suitable_Primitive; + -------------------------- -- Is_Suspension_Object -- -------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 4fa49db..66280f9 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1986,6 +1986,10 @@ package Sem_Util is -- Return True if N is a subprogram stub with no prior subprogram -- declaration. + function Is_Suitable_Primitive (Subp_Id : Entity_Id) return Boolean; + -- Determine whether arbitrary subprogram Subp_Id may act as a primitive of + -- an arbitrary tagged type. + function Is_Suspension_Object (Id : Entity_Id) return Boolean; -- Determine whether arbitrary entity Id denotes Suspension_Object defined -- in Ada.Synchronous_Task_Control. diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index f1a532d..5107665 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -531,75 +531,89 @@ package Sinfo is -- The SPARK RM 6.9 defines two classes of constructs - Ghost entities and -- Ghost statements. The intent of the feature is to treat Ghost constructs -- as non-existent when Ghost assertion policy Ignore is in effect. - + -- -- The corresponding nodes which map to Ghost constructs are: - + -- -- Ghost entities -- Declaration nodes -- N_Package_Body -- N_Subprogram_Body - + -- -- Ghost statements -- N_Assignment_Statement -- N_Procedure_Call_Statement -- N_Pragma - + -- -- In addition, the compiler treats instantiations as Ghost entities - + -- -- To achieve the removal of ignored Ghost constructs, the compiler relies - -- on global variable Ghost_Mode and a mechanism called "Ghost regions". - -- The values of the global variable are as follows: - + -- on global variables Ghost_Mode and Ignored_Ghost_Region, which comprise + -- a mechanism called "Ghost regions". + -- + -- The values of Ghost_Mode are as follows: + -- -- 1. Check - All static semantics as defined in SPARK RM 6.9 are in -- effect. The Ghost region has mode Check. - + -- -- 2. Ignore - Same as Check, ignored Ghost code is not present in ALI -- files, object files, and the final executable. The Ghost region -- has mode Ignore. - + -- -- 3. None - No Ghost region is in effect - + -- + -- The value of Ignored_Ghost_Region captures the node which initiates an + -- ignored Ghost region. + -- -- A Ghost region is a compiler operating mode, similar to Check_Syntax, -- however a region is much more finely grained and depends on the policy -- in effect. The region starts prior to the analysis of a Ghost construct -- and ends immediately after its expansion. The region is established as -- follows: - + -- -- 1. Declarations - Prior to analysis, if the declaration is subject to -- pragma Ghost. - + -- -- 2. Renaming declarations - Same as 1) or when the renamed entity is -- Ghost. - + -- -- 3. Completing declarations - Same as 1) or when the declaration is -- partially analyzed and the declaration completes a Ghost entity. - + -- -- 4. N_Package_Body, N_Subprogram_Body - Same as 1) or when the body is -- partially analyzed and completes a Ghost entity. - + -- -- 5. N_Assignment_Statement - After the left hand side is analyzed and -- references a Ghost entity. - + -- -- 6. N_Procedure_Call_Statement - After the name is analyzed and denotes -- a Ghost procedure. - + -- -- 7. N_Pragma - During analysis, when the related entity is Ghost or the -- pragma encloses a Ghost entity. - + -- -- 8. Instantiations - Save as 1) or when the instantiation is partially -- analyzed and the generic template is Ghost. - - -- Routines Mark_And_Set_Ghost_xxx and Set_Ghost_Mode install a new Ghost - -- region and routine Restore_Ghost_Mode ends a Ghost region. A region may - -- be reinstalled similarly to scopes for decoupled expansion such as the - -- generation of dispatch tables or the creation of a predicate function. - + -- + -- The following routines install a new Ghost region: + -- + -- Install_Ghost_Region + -- Mark_And_Set_Ghost_xxx + -- Set_Ghost_Mode + -- + -- The following routine ends a Ghost region: + -- + -- Restore_Ghost_Region + -- + -- A region may be reinstalled similarly to scopes for decoupled expansion + -- such as the generation of dispatch tables or the creation of a predicate + -- function. + -- -- If the mode of a Ghost region is Ignore, any newly created nodes as well -- as source entities are marked as ignored Ghost. In additon, the marking -- process signals all enclosing scopes that an ignored Ghost node resides -- within. The compilation unit where the node resides is also added to an -- auxiliary table for post processing. - + -- -- After the analysis and expansion of all compilation units takes place -- as well as the instantiation of all inlined [generic] bodies, the GNAT -- driver initiates a separate pass which removes all ignored Ghost nodes diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 14a578e..8381235 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2018-05-24 Hristian Kirtchev + + * gnat.dg/formal_containers.adb: New testcase. + 2018-05-24 Rainer Orth * gcc.target/i386/pr85345.c: Require ifunc support. diff --git a/gcc/testsuite/gnat.dg/formal_containers.adb b/gcc/testsuite/gnat.dg/formal_containers.adb new file mode 100644 index 0000000..185b946 --- /dev/null +++ b/gcc/testsuite/gnat.dg/formal_containers.adb @@ -0,0 +1,23 @@ +-- { dg-do compile } + +with Ada.Containers.Formal_Hashed_Sets; + +procedure Formal_Containers is + type T is new Integer; + + function Eq (X : T; Y : T) return Boolean; + + function Hash (X : T) return Ada.Containers.Hash_Type is (0); + + package TSet is new Ada.Containers.Formal_Hashed_Sets + (Element_Type => T, + Hash => Hash, + Equivalent_Elements => Eq); + + S : Tset.Set := TSet.Empty_Set; + + function Eq (X : T; Y : T) return Boolean is + begin + return TSet.Contains (S, X) or TSet.Contains (S, Y); + end Eq; +begin null; end Formal_Containers; -- 2.7.4