From a85dbeec8d84e07ee549fca50dc118234f16d3f1 Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Thu, 11 Jan 2018 08:55:57 +0000 Subject: [PATCH] [Ada] Prohibit concurrent types in Ghost regions This patch ensures that single concurrent type declarations are marked as Ghost when they appear within a Ghost region. In addition, the patch verifies that no concurrent type is declared within a Ghost region and issues an error. ------------ -- Source -- ------------ -- types.ads package Types with Ghost is protected Prot_Obj is -- Error end Prot_Obj; protected type Prot_Typ is -- Error end Prot_Typ; task Task_Obj; -- Error task type Task_Typ; -- Error end Types; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c types.ads types.ads:2:14: ghost type "Prot_Obj" cannot be concurrent types.ads:5:19: ghost type "Prot_Typ" cannot be concurrent types.ads:8:09: ghost type "Task_Obj" cannot be concurrent types.ads:10:14: ghost type "Task_Typ" cannot be concurrent 2018-01-11 Hristian Kirtchev gcc/ada/ * freeze.adb (Freeze_Entity): Ensure that a Ghost type is not concurrent, nor effectively volatile. * ghost.adb (Check_Ghost_Type): New routine. * ghost.ads (Check_Ghost_Type): New routine. * sem_util.adb (Is_Declaration): Reimplemented. The routine can now consider specific subsets of declarations. (Is_Declaration_Other_Than_Renaming): Removed. Its functionality is replicated by Is_Declaration. * sem_util.ads (Is_Declaration): New parameter profile. Update the comment on usage. (Is_Declaration_Other_Than_Renaming): Removed. From-SVN: r256521 --- gcc/ada/ChangeLog | 14 ++++++ gcc/ada/freeze.adb | 20 ++------ gcc/ada/ghost.adb | 36 ++++++++++++++ gcc/ada/ghost.ads | 4 ++ gcc/ada/sem_util.adb | 113 +++++++++++++++++++++++++++++++++++-------- gcc/ada/sem_util.ads | 38 +++++++++++++-- 6 files changed, 185 insertions(+), 40 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index cd66210109b..1eabde4f2e3 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,17 @@ +2018-01-11 Hristian Kirtchev + + * freeze.adb (Freeze_Entity): Ensure that a Ghost type is not + concurrent, nor effectively volatile. + * ghost.adb (Check_Ghost_Type): New routine. + * ghost.ads (Check_Ghost_Type): New routine. + * sem_util.adb (Is_Declaration): Reimplemented. The routine can now + consider specific subsets of declarations. + (Is_Declaration_Other_Than_Renaming): Removed. Its functionality is + replicated by Is_Declaration. + * sem_util.ads (Is_Declaration): New parameter profile. Update the + comment on usage. + (Is_Declaration_Other_Than_Renaming): Removed. + 2018-01-11 Hristian Kirtchev * sem_ch5.adb (Analyze_Assignment): Assignments to variables that act diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index ba49b39b632..1e6e2575fef 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -5517,6 +5517,11 @@ package body Freeze is -- Case of a type or subtype being frozen else + -- Verify several SPARK legality rules related to Ghost types now + -- that the type is frozen. + + Check_Ghost_Type (E); + -- We used to check here that a full type must have preelaborable -- initialization if it completes a private type specified with -- pragma Preelaborable_Initialization, but that missed cases where @@ -5567,21 +5572,6 @@ package body Freeze is end if; end; - if Is_Ghost_Entity (E) then - - -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify - -- this legality rule first to five a finer-grained diagnostic. - - if Is_Concurrent_Type (E) then - Error_Msg_N ("ghost type & cannot be concurrent", E); - - -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7)) - - elsif Is_Effectively_Volatile (E) then - Error_Msg_N ("ghost type & cannot be volatile", E); - end if; - end if; - -- Deal with special cases of freezing for subtype if E /= Base_Type (E) then diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 6dad9c24325..59977244818 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -806,6 +806,42 @@ package body Ghost is end if; end Check_Ghost_Refinement; + ---------------------- + -- Check_Ghost_Type -- + ---------------------- + + procedure Check_Ghost_Type (Typ : Entity_Id) is + Conc_Typ : Entity_Id; + Full_Typ : Entity_Id; + + begin + if Is_Ghost_Entity (Typ) then + Conc_Typ := Empty; + Full_Typ := Typ; + + if Is_Single_Concurrent_Type (Typ) then + Conc_Typ := Anonymous_Object (Typ); + Full_Typ := Conc_Typ; + + elsif Is_Concurrent_Type (Typ) then + Conc_Typ := Typ; + end if; + + -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this + -- legality rule first to give a finer-grained diagnostic. + + if Present (Conc_Typ) then + Error_Msg_N ("ghost type & cannot be concurrent", Conc_Typ); + end if; + + -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7)) + + if Is_Effectively_Volatile (Full_Typ) then + Error_Msg_N ("ghost type & cannot be volatile", Full_Typ); + end if; + end if; + end Check_Ghost_Type; + ------------------ -- Ghost_Entity -- ------------------ diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 10fe447c00b..8e23bcf6ac4 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -68,6 +68,10 @@ package Ghost is -- Verify that the Ghost policy of constituent Constit_Id is compatible -- with the Ghost policy of abstract state State_I. + procedure Check_Ghost_Type (Typ : Entity_Id); + -- Verify that Ghost type Typ is neither concurrent, nor effectively + -- volatile. + function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean; -- Determine whether type Typ implements at least one Ghost interface diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index c72164b2888..5fa02ddde1c 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -13368,40 +13368,113 @@ package body Sem_Util is -- Is_Declaration -- -------------------- - function Is_Declaration (N : Node_Id) return Boolean is + function Is_Declaration + (N : Node_Id; + Body_OK : Boolean := True; + Concurrent_OK : Boolean := True; + Formal_OK : Boolean := True; + Generic_OK : Boolean := True; + Instantiation_OK : Boolean := True; + Renaming_OK : Boolean := True; + Stub_OK : Boolean := True; + Subprogram_OK : Boolean := True; + Type_OK : Boolean := True) return Boolean + is begin - return - Is_Declaration_Other_Than_Renaming (N) - or else Is_Renaming_Declaration (N); - end Is_Declaration; + case Nkind (N) is - ---------------------------------------- - -- Is_Declaration_Other_Than_Renaming -- - ---------------------------------------- + -- Body declarations + + when N_Proper_Body => + return Body_OK; + + -- Concurrent type declarations + + when N_Protected_Type_Declaration + | N_Single_Protected_Declaration + | N_Single_Task_Declaration + | N_Task_Type_Declaration + => + return Concurrent_OK or Type_OK; + + -- Formal declarations + + when N_Formal_Abstract_Subprogram_Declaration + | N_Formal_Concrete_Subprogram_Declaration + | N_Formal_Object_Declaration + | N_Formal_Package_Declaration + | N_Formal_Type_Declaration + => + return Formal_OK; + + -- Generic declarations + + when N_Generic_Package_Declaration + | N_Generic_Subprogram_Declaration + => + return Generic_OK; + + -- Generic instantiations + + when N_Function_Instantiation + | N_Package_Instantiation + | N_Procedure_Instantiation + => + return Instantiation_OK; + + -- Generic renaming declarations + + when N_Generic_Renaming_Declaration => + return Generic_OK or Renaming_OK; + + -- Renaming declarations + + when N_Exception_Renaming_Declaration + | N_Object_Renaming_Declaration + | N_Package_Renaming_Declaration + | N_Subprogram_Renaming_Declaration + => + return Renaming_OK; + + -- Stub declarations + + when N_Body_Stub => + return Stub_OK; + + -- Subprogram declarations - function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean is - begin - case Nkind (N) is when N_Abstract_Subprogram_Declaration - | N_Exception_Declaration + | N_Entry_Declaration | N_Expression_Function - | N_Full_Type_Declaration - | N_Generic_Package_Declaration - | N_Generic_Subprogram_Declaration - | N_Number_Declaration - | N_Object_Declaration - | N_Package_Declaration + | N_Subprogram_Declaration + => + return Subprogram_OK; + + -- Type declarations + + when N_Full_Type_Declaration + | N_Incomplete_Type_Declaration | N_Private_Extension_Declaration | N_Private_Type_Declaration - | N_Subprogram_Declaration | N_Subtype_Declaration + => + return Type_OK; + + -- Miscellaneous + + when N_Component_Declaration + | N_Exception_Declaration + | N_Implicit_Label_Declaration + | N_Number_Declaration + | N_Object_Declaration + | N_Package_Declaration => return True; when others => return False; end case; - end Is_Declaration_Other_Than_Renaming; + end Is_Declaration; -------------------------------- -- Is_Declared_Within_Variant -- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index a4ed9662164..3de394456b0 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1561,11 +1561,39 @@ package Sem_Util is -- declarations. In Ada 2012 it also covers type and subtype declarations -- with aspects: Invariant, Predicate, and Default_Initial_Condition. - function Is_Declaration (N : Node_Id) return Boolean; - -- Determine whether arbitrary node N denotes a declaration - - function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean; - -- Determine whether arbitrary node N denotes a non-renaming declaration + function Is_Declaration + (N : Node_Id; + Body_OK : Boolean := True; + Concurrent_OK : Boolean := True; + Formal_OK : Boolean := True; + Generic_OK : Boolean := True; + Instantiation_OK : Boolean := True; + Renaming_OK : Boolean := True; + Stub_OK : Boolean := True; + Subprogram_OK : Boolean := True; + Type_OK : Boolean := True) return Boolean; + -- Determine whether arbitrary node N denotes a declaration depending + -- on the allowed subsets of declarations. Set the following flags to + -- consider specific subsets of declarations: + -- + -- * Body_OK - body declarations + -- + -- * Concurrent_OK - concurrent type declarations + -- + -- * Formal_OK - formal declarations + -- + -- * Generic_OK - generic declarations, including generic renamings + -- + -- * Instantiation_OK - generic instantiations + -- + -- * Renaming_OK - renaming declarations, including generic renamings + -- + -- * Stub_OK - stub declarations + -- + -- * Subprogram_OK - entry, expression function, and subprogram + -- declarations. + -- + -- * Type_OK - type declarations, including concurrent types function Is_Declared_Within_Variant (Comp : Entity_Id) return Boolean; -- Returns True iff component Comp is declared within a variant part -- 2.30.2