From 58996b09cafcb656b74a6df85b2c632f6500d2ab Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Mon, 26 Oct 2015 15:40:10 +0000 Subject: [PATCH] contracts.adb (Analyze_Object_Contract): Set and restore the SPARK_Mode for both constants and objects. 2015-10-26 Hristian Kirtchev * contracts.adb (Analyze_Object_Contract): Set and restore the SPARK_Mode for both constants and objects. Factor out the semantic checks concerning Ghost objects. * freeze.adb (Freeze_Array_Type): A Ghost array type cannot have a concurrent component type. (Freeze_Entity): A Ghost type cannot also be concurrent. (Freeze_Record_Type): A Ghost record type cannot have a concurrent component. * sem_prag.adb (Analyze_Abstract_State): A Ghost abstract state cannot also be synchronized. (Check_Ghost_Synchronous): New routine. * sem_util.adb (Yields_Synchronized_Object): Correct the case of record components to account for the case where the type has no component list. 2015-10-26 Hristian Kirtchev * expander.adb (Expand): Expand a single protected declaration. * exp_ch9.ads, exp_ch9.adb (Expand_N_Single_Protected_Declaration): New routine. 2015-10-26 Hristian Kirtchev * sem_res.adb (Is_OK_Volatile_Context): A volatile object may appear in an object declaration as long as it denotes the name. From-SVN: r229376 --- gcc/ada/ChangeLog | 28 +++++++++++++ gcc/ada/contracts.adb | 92 +++++++++++++++++++++---------------------- gcc/ada/exp_ch9.adb | 22 +++++++++-- gcc/ada/exp_ch9.ads | 15 +++---- gcc/ada/expander.adb | 5 ++- gcc/ada/freeze.adb | 45 ++++++++++++++++++--- gcc/ada/sem_prag.adb | 21 ++++++++++ gcc/ada/sem_res.adb | 7 ++++ gcc/ada/sem_util.adb | 18 ++++++--- 9 files changed, 184 insertions(+), 69 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 86893ba18a1..7cafbd88c89 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,31 @@ +2015-10-26 Hristian Kirtchev + + * contracts.adb (Analyze_Object_Contract): Set and restore + the SPARK_Mode for both constants and objects. Factor out the + semantic checks concerning Ghost objects. + * freeze.adb (Freeze_Array_Type): A Ghost array type cannot have a + concurrent component type. + (Freeze_Entity): A Ghost type cannot also be concurrent. + (Freeze_Record_Type): A Ghost record type cannot have a concurrent + component. + * sem_prag.adb (Analyze_Abstract_State): A Ghost abstract + state cannot also be synchronized. + (Check_Ghost_Synchronous): New routine. + * sem_util.adb (Yields_Synchronized_Object): Correct the case + of record components to account for the case where the type has + no component list. + +2015-10-26 Hristian Kirtchev + + * expander.adb (Expand): Expand a single protected declaration. + * exp_ch9.ads, exp_ch9.adb (Expand_N_Single_Protected_Declaration): New + routine. + +2015-10-26 Hristian Kirtchev + + * sem_res.adb (Is_OK_Volatile_Context): A volatile object may appear + in an object declaration as long as it denotes the name. + 2015-10-26 Hristian Kirtchev * sem_ch9.adb (Analyze_Single_Protected_Declaration): The anonymous diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 30318dc63f6..2ab91f98fec 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -648,10 +648,34 @@ package body Contracts is end if; end if; + -- The anonymous object created for a single concurrent type inherits + -- the SPARK_Mode from the type. Due to the timing of contract analysis, + -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that + -- of the enclosing context. To remedy this, restore the original mode + -- of the related anonymous object. + + if Is_Single_Concurrent_Object (Obj_Id) + and then Present (SPARK_Pragma (Obj_Id)) + then + Restore_Mode := True; + Save_SPARK_Mode_And_Set (Obj_Id, Mode); + end if; + -- Constant-related checks if Ekind (Obj_Id) = E_Constant then + -- Analyze indicator Part_Of + + Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); + + -- Check whether the lack of indicator Part_Of agrees with the + -- placement of the constant with respect to the state space. + + if No (Prag) then + Check_Missing_Part_Of (Obj_Id); + end if; + -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)). -- This check is relevant only when SPARK_Mode is on, as it is not -- a standard Ada legality rule. Internally-generated constants that @@ -666,32 +690,10 @@ package body Contracts is Error_Msg_N ("constant cannot be volatile", Obj_Id); end if; - Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); - - -- Check whether the lack of indicator Part_Of agrees with the - -- placement of the constant with respect to the state space. - - if No (Prag) then - Check_Missing_Part_Of (Obj_Id); - end if; - -- Variable-related checks else pragma Assert (Ekind (Obj_Id) = E_Variable); - -- The anonymous object created for a single concurrent type inherits - -- the SPARK_Mode from the type. Due to the timing of contract - -- analysis, delayed pragmas may be subject to the wrong SPARK_Mode, - -- usually that of the enclosing context. To remedy this, restore the - -- original SPARK_Mode of the related variable. - - if Is_Single_Concurrent_Object (Obj_Id) - and then Present (SPARK_Pragma (Obj_Id)) - then - Restore_Mode := True; - Save_SPARK_Mode_And_Set (Obj_Id, Mode); - end if; - -- Analyze all external properties Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers); @@ -834,44 +836,42 @@ package body Contracts is & "protected type %"), Obj_Id); end if; end if; + end if; - if Is_Ghost_Entity (Obj_Id) then + -- Common checks - -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8)) + if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then - if Is_Effectively_Volatile (Obj_Id) then - Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id); + -- A Ghost object cannot be of a type that yields a synchronized + -- object (SPARK RM 6.9(19)). - -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8)) + if Yields_Synchronized_Object (Obj_Typ) then + Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id); - elsif Is_Imported (Obj_Id) then - Error_Msg_N ("ghost object & cannot be imported", Obj_Id); + -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8) and + -- SPARK RM 6.9(19)). - elsif Is_Exported (Obj_Id) then - Error_Msg_N ("ghost object & cannot be exported", Obj_Id); - end if; - end if; + elsif Is_Effectively_Volatile (Obj_Id) then + Error_Msg_N ("ghost object & cannot be volatile", Obj_Id); - -- Restore the SPARK_Mode of the enclosing context after all delayed - -- pragmas have been analyzed. + -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8)). + -- One exception to this is the object that represents the dispatch + -- table of a Ghost tagged type, as the symbol needs to be exported. - if Restore_Mode then - Restore_SPARK_Mode (Mode); - end if; - end if; - - -- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One - -- exception to this is the object that represents the dispatch table of - -- a Ghost tagged type, as the symbol needs to be exported. - - if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then - if Is_Exported (Obj_Id) then + elsif Is_Exported (Obj_Id) then Error_Msg_N ("ghost object & cannot be exported", Obj_Id); elsif Is_Imported (Obj_Id) then Error_Msg_N ("ghost object & cannot be imported", Obj_Id); end if; end if; + + -- Restore the SPARK_Mode of the enclosing context after all delayed + -- pragmas have been analyzed. + + if Restore_Mode then + Restore_SPARK_Mode (Mode); + end if; end Analyze_Object_Contract; ----------------------------------- diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb index 00b3b60c55a..4887c707f69 100644 --- a/gcc/ada/exp_ch9.adb +++ b/gcc/ada/exp_ch9.adb @@ -11388,14 +11388,28 @@ package body Exp_Ch9 is end loop; end Expand_N_Selective_Accept; + ------------------------------------------- + -- Expand_N_Single_Protected_Declaration -- + ------------------------------------------- + + -- A single protected declaration should never be present after semantic + -- analysis because it is transformed into a protected type declaration + -- and an accompanying anonymous object. This routine ensures that the + -- transformation takes place. + + procedure Expand_N_Single_Protected_Declaration (N : Node_Id) is + begin + raise Program_Error; + end Expand_N_Single_Protected_Declaration; + -------------------------------------- -- Expand_N_Single_Task_Declaration -- -------------------------------------- - -- Single task declarations should never be present after semantic - -- analysis, since we expect them to be replaced by a declaration of an - -- anonymous task type, followed by a declaration of the task object. We - -- include this routine to make sure that is happening. + -- A single task declaration should never be present after semantic + -- analysis because it is transformed into a task type declaration and + -- an accompanying anonymous object. This routine ensures that the + -- transformation takes place. procedure Expand_N_Single_Task_Declaration (N : Node_Id) is begin diff --git a/gcc/ada/exp_ch9.ads b/gcc/ada/exp_ch9.ads index d9fa7d6d7fb..d49201bfe0d 100644 --- a/gcc/ada/exp_ch9.ads +++ b/gcc/ada/exp_ch9.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -266,12 +266,13 @@ package Exp_Ch9 is -- allows these two nodes to be found from the type, without benefit of -- further attributes, using Corresponding_Record. - procedure Expand_N_Requeue_Statement (N : Node_Id); - procedure Expand_N_Selective_Accept (N : Node_Id); - procedure Expand_N_Single_Task_Declaration (N : Node_Id); - procedure Expand_N_Task_Body (N : Node_Id); - procedure Expand_N_Task_Type_Declaration (N : Node_Id); - procedure Expand_N_Timed_Entry_Call (N : Node_Id); + procedure Expand_N_Requeue_Statement (N : Node_Id); + procedure Expand_N_Selective_Accept (N : Node_Id); + procedure Expand_N_Single_Protected_Declaration (N : Node_Id); + procedure Expand_N_Single_Task_Declaration (N : Node_Id); + procedure Expand_N_Task_Body (N : Node_Id); + procedure Expand_N_Task_Type_Declaration (N : Node_Id); + procedure Expand_N_Timed_Entry_Call (N : Node_Id); procedure Expand_Protected_Body_Declarations (N : Node_Id; diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb index 2d9b6d964ac..4aa20d6f41b 100644 --- a/gcc/ada/expander.adb +++ b/gcc/ada/expander.adb @@ -432,6 +432,9 @@ package body Expander is when N_Selective_Accept => Expand_N_Selective_Accept (N); + when N_Single_Protected_Declaration => + Expand_N_Single_Protected_Declaration (N); + when N_Single_Task_Declaration => Expand_N_Single_Task_Declaration (N); @@ -471,7 +474,7 @@ package body Expander is when N_Variant_Part => Expand_N_Variant_Part (N); - -- For all other node kinds, no expansion activity required + -- For all other node kinds, no expansion activity required when others => null; diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index e09fbd20239..59a49ced0ae 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -2806,6 +2806,15 @@ package body Freeze is then Set_Alignment (Arr, Alignment (Component_Type (Arr))); end if; + + -- A Ghost type cannot have a component of protected or task type + -- (SPARK RM 6.9(19)). + + if Is_Ghost_Entity (Arr) and then Is_Concurrent_Type (Ctyp) then + Error_Msg_N + ("ghost array type & cannot have concurrent component type", + Arr); + end if; end Freeze_Array_Type; ------------------------------- @@ -4341,6 +4350,25 @@ package body Freeze is Next_Component (Comp); end loop; end if; + + -- A Ghost type cannot have a component of protected or task type + -- (SPARK RM 6.9(19)). + + if Is_Ghost_Entity (Rec) then + Comp := First_Component (Rec); + while Present (Comp) loop + if Comes_From_Source (Comp) + and then Is_Concurrent_Type (Etype (Comp)) + then + Error_Msg_Name_1 := Chars (Rec); + Error_Msg_N + ("component & of ghost type % cannot be concurrent", + Comp); + end if; + + Next_Component (Comp); + end loop; + end if; end if; -- Make sure that if we have an iterator aspect, then we have @@ -5091,12 +5119,19 @@ package body Freeze is end if; end; - -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(8)) + if Is_Ghost_Entity (E) then - if Is_Ghost_Entity (E) - and then Is_Effectively_Volatile (E) - then - Error_Msg_N ("ghost type & cannot be volatile", E); + -- 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(8)) + + 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 diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index a8998cc78cf..17544f0cb81 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -10068,6 +10068,11 @@ package body Sem_Prag is -- Opt is not a duplicate property and sets the flag Status. -- (SPARK RM 7.1.4(2)) + procedure Check_Ghost_Synchronous; + -- Ensure that the abstract state is not subject to both Ghost + -- and Synchronous simple options. Emit an error if this is the + -- case. + procedure Create_Abstract_State (Nam : Name_Id; Decl : Node_Id; @@ -10320,6 +10325,20 @@ package body Sem_Prag is Status := True; end Check_Duplicate_Property; + ----------------------------- + -- Check_Ghost_Synchronous -- + ----------------------------- + + procedure Check_Ghost_Synchronous is + begin + -- A synchronized abstract state cannot be Ghost and vice + -- versa (SPARK RM 6.9(19)). + + if Ghost_Seen and Synchronous_Seen then + SPARK_Msg_N ("synchronized state cannot be ghost", State); + end if; + end Check_Ghost_Synchronous; + --------------------------- -- Create_Abstract_State -- --------------------------- @@ -10464,6 +10483,7 @@ package body Sem_Prag is elsif Chars (Opt) = Name_Ghost then Check_Duplicate_Option (Opt, Ghost_Seen); + Check_Ghost_Synchronous; if Present (State_Id) then Set_Is_Ghost_Entity (State_Id); @@ -10473,6 +10493,7 @@ package body Sem_Prag is elsif Chars (Opt) = Name_Synchronous then Check_Duplicate_Option (Opt, Synchronous_Seen); + Check_Ghost_Synchronous; -- Option Part_Of without an encapsulating state is -- illegal (SPARK RM 7.1.4(9)). diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index d2963f73e7c..d3312e2d84c 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6993,6 +6993,13 @@ package body Sem_Res is return True; end if; + -- The volatile object acts as the name of a renaming declaration + + elsif Nkind (Context) = N_Object_Renaming_Declaration + and then Name (Context) = Obj_Ref + then + return True; + -- The volatile object appears as an actual parameter in a call to an -- instance of Unchecked_Conversion whose result is renamed. diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 8e33f4c4036..d8567c59e7f 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -20121,7 +20121,8 @@ package body Sem_Util is -------------------------------- function Yields_Synchronized_Object (Typ : Entity_Id) return Boolean is - Id : Entity_Id; + Has_Sync_Comp : Boolean := False; + Id : Entity_Id; begin -- An array type yields a synchronized object if its component type @@ -20154,10 +20155,15 @@ package body Sem_Util is Id := First_Entity (Typ); while Present (Id) loop if Comes_From_Source (Id) then - if Ekind (Id) = E_Component - and then not Yields_Synchronized_Object (Etype (Id)) - then - return False; + if Ekind (Id) = E_Component then + if Yields_Synchronized_Object (Etype (Id)) then + Has_Sync_Comp := True; + + -- The component does not yield a synchronized object + + else + return False; + end if; elsif Ekind (Id) = E_Discriminant and then Present (Expression (Parent (Id))) @@ -20181,7 +20187,7 @@ package body Sem_Util is -- If we get here, then all discriminants lack default values and all -- components are of a type that yields a synchronized object. - return True; + return Has_Sync_Comp; -- A synchronized interface type yields a synchronized object by default -- 2.30.2