diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -472,6 +472,13 @@ package body Ghost is if Is_Ignored_Ghost_Node (Par) then return True; + -- It is not possible to check correct use of Ghost entities + -- in generic instantiations until after the generic has been + -- resolved. Postpone that verification to after resolution. + + elsif Nkind (Par) = N_Generic_Association then + return True; + -- A reference to a Ghost entity can appear within an aspect -- specification (SPARK RM 6.9(10)). The precise checking will -- occur when analyzing the corresponding pragma. We make an @@ -521,19 +528,6 @@ package body Ghost is then return True; - -- In the context of an instantiation, accept currently Ghost - -- arguments for formal subprograms, as SPARK does not provide - -- a way to distinguish Ghost formal parameters from non-Ghost - -- ones. Illegal use of such arguments in a non-Ghost context - -- will lead to errors inside the instantiation. - - elsif Nkind (Parent (Par)) = N_Generic_Association - and then (Nkind (Par) in N_Has_Entity - and then Present (Entity (Par)) - and then Is_Subprogram (Entity (Par))) - then - return True; - elsif Is_OK_Declaration (Par) then return True; @@ -680,6 +674,128 @@ package body Ghost is end if; end Check_Ghost_Context; + ------------------------------------------------ + -- Check_Ghost_Context_In_Generic_Association -- + ------------------------------------------------ + + procedure Check_Ghost_Context_In_Generic_Association + (Actual : Node_Id; + Formal : Entity_Id) + is + function Emit_Error_On_Ghost_Reference + (N : Node_Id) + return Traverse_Result; + -- Determine wether N denotes a reference to a ghost entity, and if so + -- issue an error. + + ----------------------------------- + -- Emit_Error_On_Ghost_Reference -- + ----------------------------------- + + function Emit_Error_On_Ghost_Reference + (N : Node_Id) + return Traverse_Result + is + begin + if Is_Entity_Name (N) + and then Present (Entity (N)) + and then Is_Ghost_Entity (Entity (N)) + then + Error_Msg_N ("ghost entity cannot appear in this context", N); + Error_Msg_Sloc := Sloc (Formal); + Error_Msg_NE ("\formal & was not declared as ghost #", N, Formal); + return Abandon; + end if; + + return OK; + end Emit_Error_On_Ghost_Reference; + + procedure Check_Ghost_References is + new Traverse_Proc (Emit_Error_On_Ghost_Reference); + + -- Start of processing for Check_Ghost_Context_In_Generic_Association + + begin + -- The context is ghost when it appears within a Ghost package or + -- subprogram. + + if Ghost_Mode > None then + return; + + -- The context is ghost if Formal is explicitly marked as ghost + + elsif Is_Ghost_Entity (Formal) then + return; + + else + Check_Ghost_References (Actual); + end if; + end Check_Ghost_Context_In_Generic_Association; + + --------------------------------------------- + -- Check_Ghost_Formal_Procedure_Or_Package -- + --------------------------------------------- + + procedure Check_Ghost_Formal_Procedure_Or_Package + (N : Node_Id; + Actual : Entity_Id; + Formal : Entity_Id; + Is_Default : Boolean := False) + is + begin + if not Is_Ghost_Entity (Formal) then + return; + end if; + + if Present (Actual) and then Is_Ghost_Entity (Actual) then + return; + end if; + + if Is_Default then + Error_Msg_N ("ghost procedure expected as default", N); + Error_Msg_NE ("\formal & is declared as ghost", N, Formal); + + else + if Ekind (Formal) = E_Procedure then + Error_Msg_N ("ghost procedure expected for actual", N); + else + Error_Msg_N ("ghost package expected for actual", N); + end if; + + Error_Msg_Sloc := Sloc (Formal); + Error_Msg_NE ("\formal & was declared as ghost #", N, Formal); + end if; + end Check_Ghost_Formal_Procedure_Or_Package; + + --------------------------------- + -- Check_Ghost_Formal_Variable -- + --------------------------------- + + procedure Check_Ghost_Formal_Variable + (Actual : Node_Id; + Formal : Entity_Id; + Is_Default : Boolean := False) + is + Actual_Obj : constant Entity_Id := Get_Enclosing_Deep_Object (Actual); + begin + if not Is_Ghost_Entity (Formal) then + return; + end if; + + if No (Actual_Obj) + or else not Is_Ghost_Entity (Actual_Obj) + then + if Is_Default then + Error_Msg_N ("ghost object expected as default", Actual); + Error_Msg_NE ("\formal & is declared as ghost", Actual, Formal); + else + Error_Msg_N ("ghost object expected for mutable actual", Actual); + Error_Msg_Sloc := Sloc (Formal); + Error_Msg_NE ("\formal & was declared as ghost #", Actual, Formal); + end if; + end if; + end Check_Ghost_Formal_Variable; + ---------------------------- -- Check_Ghost_Overriding -- ---------------------------- diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -44,6 +44,33 @@ package Ghost is -- Determine whether node Ghost_Ref appears within a Ghost-friendly context -- where Ghost entity Ghost_Id can safely reside. + procedure Check_Ghost_Context_In_Generic_Association + (Actual : Node_Id; + Formal : Entity_Id); + -- Check that if Actual contains references to ghost entities, generic + -- formal parameter Formal is ghost (SPARK RM 6.9(10)). + + procedure Check_Ghost_Formal_Procedure_Or_Package + (N : Node_Id; + Actual : Entity_Id; + Formal : Entity_Id; + Is_Default : Boolean := False); + -- Verify that if generic formal procedure (resp. package) Formal is ghost, + -- then Actual is not Empty and also a ghost procedure (resp. package) + -- (SPARK RM 6.9(13-14)). The error if any is located on N. If + -- Is_Default is False, N and Actual represent the actual parameter in an + -- instantiation. Otherwise, they represent the default subprogram of a + -- formal subprogram declaration. + + procedure Check_Ghost_Formal_Variable + (Actual : Node_Id; + Formal : Entity_Id; + Is_Default : Boolean := False); + -- Verify that if Formal (either an IN OUT generic formal parameter, or an + -- IN generic formal parameter of access-to-variable type) is ghost, then + -- Actual is a ghost object (SPARK RM 6.9(13-14)). Is_Default is True when + -- Actual is the default expression of the formal object declaration. + procedure Check_Ghost_Overriding (Subp : Entity_Id; Overridden_Subp : Entity_Id); diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads --- a/gcc/ada/libgnat/s-imageu.ads +++ b/gcc/ada/libgnat/s-imageu.ads @@ -54,27 +54,34 @@ generic Unsigned_Width_Ghost : Natural; - with function Wrap_Option (Value : Uns) return Uns_Option; + with function Wrap_Option (Value : Uns) return Uns_Option + with Ghost; with function Only_Decimal_Ghost (Str : String; From, To : Integer) - return Boolean; - with function Hexa_To_Unsigned_Ghost (X : Character) return Uns; + return Boolean + with Ghost; + with function Hexa_To_Unsigned_Ghost (X : Character) return Uns + with Ghost; with function Scan_Based_Number_Ghost (Str : String; From, To : Integer; Base : Uns := 10; - Acc : Uns := 0) return Uns_Option; - with function Is_Unsigned_Ghost (Str : String) return Boolean; + Acc : Uns := 0) return Uns_Option + with Ghost; + with function Is_Unsigned_Ghost (Str : String) return Boolean + with Ghost; with function Value_Unsigned (Str : String) return Uns; with procedure Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2 : String; From, To : Integer; Base : Uns := 10; - Acc : Uns := 0); + Acc : Uns := 0) + with Ghost; with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; - Val : Uns); + Val : Uns) + with Ghost; package System.Image_U is diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads --- a/gcc/ada/libgnat/s-valuei.ads +++ b/gcc/ada/libgnat/s-valuei.ads @@ -55,30 +55,37 @@ generic -- Additional parameters for ghost subprograms used inside contracts type Uns_Option is private; - with function Wrap_Option (Value : Uns) return Uns_Option; - with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean; + with function Wrap_Option (Value : Uns) return Uns_Option + with Ghost; + with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean + with Ghost; with function Raw_Unsigned_Overflows_Ghost (Str : String; From, To : Integer) - return Boolean; + return Boolean + with Ghost; with function Scan_Raw_Unsigned_Ghost (Str : String; From, To : Integer) - return Uns; + return Uns + with Ghost; with function Raw_Unsigned_Last_Ghost (Str : String; From, To : Integer) - return Positive; + return Positive + with Ghost; with function Only_Decimal_Ghost (Str : String; From, To : Integer) - return Boolean; + return Boolean + with Ghost; with function Scan_Based_Number_Ghost (Str : String; From, To : Integer; Base : Uns := 10; Acc : Uns := 0) - return Uns_Option; + return Uns_Option + with Ghost; package System.Value_I is pragma Preelaborate; diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -384,27 +384,36 @@ is Unsigned_Width_Ghost : Natural; - with function Wrap_Option (Value : Uns) return Uns_Option; + with function Wrap_Option (Value : Uns) return Uns_Option + with Ghost; with function Only_Decimal_Ghost (Str : String; From, To : Integer) - return Boolean; - with function Hexa_To_Unsigned_Ghost (X : Character) return Uns; + return Boolean + with Ghost; + with function Hexa_To_Unsigned_Ghost (X : Character) return Uns + with Ghost; with function Scan_Based_Number_Ghost (Str : String; From, To : Integer; Base : Uns := 10; Acc : Uns := 0) - return Uns_Option; - with function Is_Integer_Ghost (Str : String) return Boolean; + return Uns_Option + with Ghost; + with function Is_Integer_Ghost (Str : String) return Boolean + with Ghost; with procedure Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2 : String; From, To : Integer; Base : Uns := 10; - Acc : Uns := 0); - with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int); - with function Abs_Uns_Of_Int (Val : Int) return Uns; - with function Value_Integer (Str : String) return Int; + Acc : Uns := 0) + with Ghost; + with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) + with Ghost; + with function Abs_Uns_Of_Int (Val : Int) return Uns + with Ghost; + with function Value_Integer (Str : String) return Int + with Ghost; package Int_Params is end Int_Params; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -2204,6 +2204,19 @@ package body Sem_Ch12 is raise Program_Error; end case; + -- Check here the correct use of Ghost entities in generic + -- instantiations, as now the generic has been resolved and + -- we know which formal generic parameters are ghost (SPARK + -- RM 6.9(10)). + + if Nkind (Formal) not in N_Use_Package_Clause + | N_Use_Type_Clause + then + Check_Ghost_Context_In_Generic_Association + (Actual => Match, + Formal => Defining_Entity (Analyzed_Formal)); + end if; + Formal := Saved_Formal; Next_Non_Pragma (Analyzed_Formal); end loop; @@ -2715,6 +2728,17 @@ package body Sem_Ch12 is if Present (E) then Preanalyze_Spec_Expression (E, T); + -- The default for a ghost generic formal IN parameter of + -- access-to-variable type should be a ghost object (SPARK + -- RM 6.9(13)). + + if Is_Access_Variable (T) then + Check_Ghost_Formal_Variable + (Actual => E, + Formal => Id, + Is_Default => True); + end if; + if Is_Limited_Type (T) and then not OK_For_Limited_Init (T, E) then Error_Msg_N ("initialization not allowed for limited types", E); @@ -3398,6 +3422,25 @@ package body Sem_Ch12 is goto Leave; end if; + -- The default for a ghost generic formal procedure should be a ghost + -- procedure (SPARK RM 6.9(13)). + + if Ekind (Nam) = E_Procedure then + declare + Def_E : Entity_Id := Empty; + begin + if Nkind (Def) in N_Has_Entity then + Def_E := Entity (Def); + end if; + + Check_Ghost_Formal_Procedure_Or_Package + (N => Def, + Actual => Def_E, + Formal => Nam, + Is_Default => True); + end; + end if; + -- Default name may be overloaded, in which case the interpretation -- with the correct profile must be selected, as for a renaming. -- If the definition is an indexed component, it must denote a @@ -10594,6 +10637,14 @@ package body Sem_Ch12 is Gen_Parent := Generic_Parent (Specification (Analyzed_Formal)); Formal_Pack := Defining_Unit_Name (Specification (Analyzed_Formal)); + -- The actual for a ghost generic formal package should be a ghost + -- package (SPARK RM 6.9(14)). + + Check_Ghost_Formal_Procedure_Or_Package + (N => Actual, + Actual => Actual_Pack, + Formal => Formal_Pack); + if Nkind (Parent (Actual_Pack)) = N_Defining_Program_Unit_Name then Parent_Spec := Package_Specification (Actual_Pack); else @@ -10881,6 +10932,18 @@ package body Sem_Ch12 is Act_E := Empty; end if; + -- The actual for a ghost generic formal procedure should be a ghost + -- procedure (SPARK RM 6.9(14)). + + if Present (Act_E) + and then Ekind (Act_E) = E_Procedure + then + Check_Ghost_Formal_Procedure_Or_Package + (N => Act, + Actual => Act_E, + Formal => Analyzed_S); + end if; + if (Present (Act_E) and then Is_Overloadable (Act_E)) or else Nkind (Act) in N_Attribute_Reference | N_Indexed_Component @@ -11400,40 +11463,22 @@ package body Sem_Ch12 is -- volatility refinement aspects. declare - Actual_Obj : Entity_Id; - N : Node_Id := Actual; + Actual_Obj : constant Entity_Id := + Get_Enclosing_Deep_Object (Actual); begin - -- Similar to Sem_Util.Get_Enclosing_Object, but treat - -- pointer dereference like component selection. - loop - if Is_Entity_Name (N) then - Actual_Obj := Entity (N); - exit; - end if; - - case Nkind (N) is - when N_Indexed_Component - | N_Selected_Component - | N_Slice - | N_Explicit_Dereference - => - N := Prefix (N); - - when N_Type_Conversion => - N := Expression (N); - - when others => - Actual_Obj := Etype (N); - exit; - end case; - end loop; - Check_Volatility_Compatibility (Actual_Obj, A_Gen_Obj, "actual object", "its corresponding formal object of mode in out", Srcpos_Bearer => Actual); end; + -- The actual for a ghost generic formal IN OUT parameter should be a + -- ghost object (SPARK RM 6.9(14)). + + Check_Ghost_Formal_Variable + (Actual => Actual, + Formal => A_Gen_Obj); + -- Formal in-parameter else @@ -11459,6 +11504,7 @@ package body Sem_Ch12 is Object_Definition => Def, Expression => Actual); + Copy_Ghost_Aspect (Formal, To => Decl_Node); Set_Corresponding_Generic_Association (Decl_Node, Act_Assoc); -- A generic formal object of a tagged type is defined to be @@ -11470,6 +11516,16 @@ package body Sem_Ch12 is Append (Decl_Node, List); + -- The actual for a ghost generic formal IN parameter of + -- access-to-variable type should be a ghost object (SPARK + -- RM 6.9(14)). + + if Is_Access_Variable (Etype (A_Gen_Obj)) then + Check_Ghost_Formal_Variable + (Actual => Actual, + Formal => A_Gen_Obj); + end if; + -- No need to repeat (pre-)analysis of some expression nodes -- already handled in Preanalyze_Actuals. @@ -11543,6 +11599,7 @@ package body Sem_Ch12 is Expression => New_Copy_Tree (Default_Expression (Formal))); + Copy_Ghost_Aspect (Formal, To => Decl_Node); Set_Corresponding_Generic_Association (Decl_Node, Expression (Decl_Node)); @@ -14199,6 +14256,8 @@ package body Sem_Ch12 is Defining_Identifier => Subt, Subtype_Indication => New_Occurrence_Of (Act_T, Loc)); + Copy_Ghost_Aspect (Formal, To => Decl_Node); + -- Record whether the actual is private at this point, so that -- Check_Generic_Actuals can restore its proper view before the -- semantic analysis of the instance. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -17002,6 +17002,9 @@ package body Sem_Prag is -- The pragma applies to a legal construct, stop the traversal elsif Nkind (Stmt) in N_Abstract_Subprogram_Declaration + | N_Formal_Object_Declaration + | N_Formal_Subprogram_Declaration + | N_Formal_Type_Declaration | N_Full_Type_Declaration | N_Generic_Subprogram_Declaration | N_Object_Declaration diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -7024,6 +7024,25 @@ package body Sem_Util is return Comps; end Copy_Component_List; + ----------------------- + -- Copy_Ghost_Aspect -- + ----------------------- + + procedure Copy_Ghost_Aspect (From : Node_Id; To : Node_Id) is + pragma Assert (not Has_Aspects (To)); + Asp : Node_Id; + + begin + if Has_Aspects (From) then + Asp := Find_Aspect (Defining_Entity (From), Aspect_Ghost); + + if Present (Asp) then + Set_Aspect_Specifications (To, New_List (New_Copy_Tree (Asp))); + Set_Has_Aspects (To, True); + end if; + end if; + end Copy_Ghost_Aspect; + ------------------------- -- Copy_Parameter_List -- ------------------------- @@ -11004,6 +11023,32 @@ package body Sem_Util is end if; end Get_Enclosing_Object; + ------------------------------- + -- Get_Enclosing_Deep_Object -- + ------------------------------- + + function Get_Enclosing_Deep_Object (N : Node_Id) return Entity_Id is + begin + if Is_Entity_Name (N) then + return Entity (N); + else + case Nkind (N) is + when N_Explicit_Dereference + | N_Indexed_Component + | N_Selected_Component + | N_Slice + => + return Get_Enclosing_Deep_Object (Prefix (N)); + + when N_Type_Conversion => + return Get_Enclosing_Deep_Object (Expression (N)); + + when others => + return Empty; + end case; + end if; + end Get_Enclosing_Deep_Object; + --------------------------- -- Get_Enum_Lit_From_Pos -- --------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -625,6 +625,11 @@ package Sem_Util is -- create a new compatible record type. Loc is the source location assigned -- to the created nodes. + procedure Copy_Ghost_Aspect (From : Node_Id; To : Node_Id); + -- Copy the Ghost aspect if present in the aspect specifications of node + -- From to node To. On entry it is assumed that To does not have aspect + -- specifications. If From has no aspects, the routine has no effect. + function Copy_Parameter_List (Subp_Id : Entity_Id) return List_Id; -- Utility to create a parameter profile for a new subprogram spec, when -- the subprogram has a body that acts as spec. This is done for some cases @@ -1183,6 +1188,12 @@ package Sem_Util is -- If expression N references a part of an object, return this object. -- Otherwise return Empty. Expression N should have been resolved already. + function Get_Enclosing_Deep_Object (N : Node_Id) return Entity_Id; + -- If expression N references a reachable part of an object (as defined in + -- SPARK RM 6.9), return this object. Otherwise return Empty. It is similar + -- to Get_Enclosing_Object, but treats pointer dereference like component + -- selection. Expression N should have been resolved already. + function Get_Generic_Entity (N : Node_Id) return Entity_Id; -- Returns the true generic entity in an instantiation. If the name in the -- instantiation is a renaming, the function returns the renamed generic.