From c5cec2fe71b243a3a4e76ef41b2ed6b36a3d543c Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 31 Oct 2014 15:49:31 +0100 Subject: 2014-10-31 Hristian Kirtchev * aspects.adb Add an entry for aspect Ghost in table Canonical_Aspect. * aspects.ads Add an entry for aspect Ghost in tables Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names and Implementation_Defined_Aspect. * einfo.adb: Flags 277 and 278 are now in use. (Is_Checked_Ghost_Entity): New routine. (Is_Ghost_Entity): Removed. (Is_Ghost_Subprogram): Removed. (Is_Ignored_Ghost_Entity): New routine. (Set_Is_Checked_Ghost_Entity): New routine. (Set_Is_Ignored_Ghost_Entity): New routine. (Write_Entity_Flags): Output flags Is_Checked_Ghost_Entity and Is_Ignored_Ghost_Entity. * einfo.ads: Add new flags Is_Checked_Ghost_Entity and Is_Ignored_Ghost_Entity along with usage in nodes. (Is_Checked_Ghost_Entity): New routine and pragma Inline. (Is_Ghost_Entity): Removed along with synthesized flag description and usage in nodes. (Is_Ghost_Subprogram): Removed along with synthesized flag description and usage in nodes. (Is_Ignored_Ghost_Entity): New routine and pragma Inline. (Set_Is_Checked_Ghost_Entity): New routine and pragma Inline. (Set_Is_Ignored_Ghost_Entity): New routine and pragma Inline. * freeze.adb (Freeze_Entity): A Ghost type cannot be effectively volatile. * par-prag.adb Pragma Ghost does not need special handling by the parser. * repinfo.adb (List_Mechanisms): Remove the entry for convention Ghost. * sem_attr.adb (Analyze_Access_Attribute): Remove obsolete check. * sem_ch3.adb (Analyze_Full_Type_Declaration): Mark the type as Ghost when its enclosing context is Ghost. (Analyze_Incomplete_Type_Decl): Mark the type as Ghost when its enclosing context is Ghost. (Analyze_Number_Declaration): Mark the number as Ghost when its enclosing context is Ghost. (Analyze_Object_Declaration): Mark the object as Ghost when its enclosing context is Ghost. Verify the Ghost policy between initial declaration and completion of a deferred constant. (Analyze_Object_Contract): A Ghost variable cannot be effectively volatile, imported or exported. (Build_Derived_Record_Type): Mark a type extension as Ghost when it implements a Ghost interface. (Build_Record_Type): Inherit volatility and "ghostness" from the parent type. (Check_Completion): A Ghost entity declared in a non-Ghost package does not require completion in a body. (Implements_Ghost_Interface): New routine. (Process_Full_View): Inherit "ghostness" from the partial view. Verify the Ghost policy between the partial and full views. Verify the completion of a Ghost type extension. * sem_ch4.adb (Check_Ghost_Subprogram_Call): Removed. * sem_ch5.adb (Analyze_Assignment): Analyze the left hand side first. * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Mark the subprogram as Ghost when its enclosing context is Ghost. (Analyze_Generic_Subprogram_Body): Mark the generic body as Ghost when its enclosing context is Ghost. Verify the Ghost policy between the spec and body. (Analyze_Subprogram_Body_Helper): Mark the body as Ghost when its enclosing context is Ghost. Verify the Ghost policy between the spec and body. (Check_Conformance): A Ghost subprogram profile and a non-Ghost subprogram profile are not subtype conformant. (Convention_Of): Removed. * sem_ch7.adb (Analyze_Package_Body_Helper): Inherit the "ghostness" from the spec. Verify the Ghost policy between the spec and body. (Analyze_Private_Type_Declaration): Mark the type as Ghost when its enclosing context is Ghost. (Requires_Completion_In_Body): New routine. (Unit_Requires_Body): Use Requires_Completion_In_Body. (Unit_Requires_Body_Info): Rename formal parameter P to Pack_Id, update comment on usage and all uses of P in the body. Use Requires_Completion_In_Body. * sem_ch7.ads (Unit_Requires_Body): Rename formal parameter P to Pack_Id, update comment on usage and all uses of P in the body. * sem_ch8.adb (Analyze_Exception_Renaming): Inherit the "ghostness" from the renamed excention. (Analyze_Generic_Renaming): Inherit the "ghostness" from the renamed generic subprogram. (Analyze_Object_Renaming): Inherit the "ghostness" from the renamed object. (Analyze_Package_Renaming): Inherit the "ghostness" from the renamed package. (Analyze_Subprogram_Renaming): Inherit the "ghostness" from the renamed subprogram. * sem_ch11.adb (Analyze_Exception_Declaration): Mark an exception as Ghost when its enclosing context is Ghost. * sem_ch12.adb (Analyze_Generic_Package_Declaration, Analyze_Generic_Subprogram_Declaration): Mark an exception as Ghost when its enclosing context is Ghost. (Preanalyze_Actuals): Remove obsolete check. * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing for aspect Ghost. (Check_Aspect_At_Freeze_Point): Aspects Depends and Global do no need special checking at freeze point. (Insert_After_SPARK_Mode): Update comment on usage. * sem_mech.adb (Set_Mechanisms): Remove the entry for convention Ghost. * sem_prag.adb Add an entry for pragma Ghost in table Sig_Flags. (Analyze_Abstract_State): Update the grammar of the pragma. Add formal parameter Pack_Id along with comment on usage. Mark an abstract state as Ghost when its enclosing context is Ghost. Add processing for option Ghost. (Analyze_Constituent): Verify that a Ghost abstract state is refined by Ghost constituents. (Analyze_Pragma): "Ghost" is now a valid policy. Add checks related to the use and placement of Check_Policy Ghost. Add processing for pragma Ghost. (Check_Ghost_Constituent): New routine. (Is_Valid_Assertion_Kind): "Ghost" is now a valid assertion. (Process_Convention): Remove obsolete check. (Set_Convention_From_Pragma): Remove the processing for convention Ghost. * sem_res.adb (Check_Ghost_Context): New routine. (Resolve_Call): Verify that a reference to a Ghost entity appears in a suitable context. Verify the Ghost polity between point of declaration and point of use. (Resolve_Entity_Name): Verify that a reference to a Ghost entity appears in a suitable context. Verify the Ghost polity between point of declaration and point of use. * sem_util.adb (Check_Ghost_Completion): New routine. (Check_Ghost_Derivation): New routine. (Incomplete_Or_Partial_View): New routine. (Incomplete_Or_Private_View): Removed. (Is_Ghost_Entity): New routine. (Is_Ghost_Statement_Or_Pragma): New routine. (Is_Subject_To_Ghost): New routine. (Policy_In_Effect): New routine. (Set_Is_Ghost_Entity): New routine. (Within_Ghost_Scope): New routine. * sem_util.ads (Check_Ghost_Completion): New routine. (Check_Ghost_Derivation): New routine. (Incomplete_Or_Partial_View): New routine. (Incomplete_Or_Private_View): Removed. (Is_Ghost_Entity): New routine. (Is_Ghost_Statement_Or_Pragma): New routine. (Is_Subject_To_Ghost): New routine. (Policy_In_Effect): New routine. (Set_Is_Ghost_Entity): New routine. (Within_Ghost_Scope): New routine. * snames.adb-tmpl (Get_Convention_Id): Remove the entry for convention Ghost. (Get_Convention_Name): Remove the entry for convention Ghost. * snames.ads-tmpl Remove the convention id for Ghost. Add a pragma id for Ghost. 2014-10-31 Sergey Rybin * gnat_ugn.texi: Add description of --RTS option for ASIS tools. From-SVN: r216981 --- gcc/ada/sem_res.adb | 261 ++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 234 insertions(+), 27 deletions(-) (limited to 'gcc/ada/sem_res.adb') diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 97f6ea1..893e1e1 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -109,6 +109,10 @@ package body Sem_Res is Pref : Node_Id); -- Check that the type of the prefix of a dereference is not incomplete + procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id); + -- Determine whether node Ghost_Ref appears within a Ghost-friendly context + -- where Ghost entity Ghost_Id can safely reside. + function Check_Infinite_Recursion (N : Node_Id) return Boolean; -- Given a call node, N, which is known to occur immediately within the -- subprogram being called, determines whether it is a detectable case of @@ -688,6 +692,193 @@ package body Sem_Res is end if; end Check_Fully_Declared_Prefix; + ------------------------- + -- Check_Ghost_Context -- + ------------------------- + + procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is + procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id); + -- Verify that the Ghost policy at the point of declaration of entity Id + -- matches the policy at the point of reference. If this is not the case + -- emit an error at Err_N. + + function Is_OK_Ghost_Context (Context : Node_Id) return Boolean; + -- Determine whether node Context denotes a Ghost-friendly context where + -- a Ghost entity can safely reside. + + ------------------------- + -- Is_OK_Ghost_Context -- + ------------------------- + + function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is + function Is_Ghost_Declaration (Decl : Node_Id) return Boolean; + -- Determine whether node Decl is a Ghost declaration or appears + -- within a Ghost declaration. + + -------------------------- + -- Is_Ghost_Declaration -- + -------------------------- + + function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is + Par : Node_Id; + Subp_Decl : Node_Id; + Subp_Id : Entity_Id; + + begin + -- Climb the parent chain looking for an object declaration + + Par := Decl; + while Present (Par) loop + case Nkind (Par) is + when N_Abstract_Subprogram_Declaration | + N_Exception_Declaration | + N_Exception_Renaming_Declaration | + N_Full_Type_Declaration | + N_Generic_Function_Renaming_Declaration | + N_Generic_Package_Declaration | + N_Generic_Package_Renaming_Declaration | + N_Generic_Procedure_Renaming_Declaration | + N_Generic_Subprogram_Declaration | + N_Number_Declaration | + N_Object_Declaration | + N_Object_Renaming_Declaration | + N_Package_Declaration | + N_Package_Renaming_Declaration | + N_Private_Extension_Declaration | + N_Private_Type_Declaration | + N_Subprogram_Declaration | + N_Subprogram_Renaming_Declaration | + N_Subtype_Declaration => + return Is_Subject_To_Ghost (Par); + + when others => + null; + end case; + + -- Special cases + + -- A reference to a Ghost entity may appear as the default + -- expression of a formal parameter of a subprogram body. This + -- context must be treated as suitable because the relation + -- between the spec and the body has not been established and + -- the body is not marked as Ghost yet. The real check was + -- performed on the spec. + + if Nkind (Par) = N_Parameter_Specification + and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body + then + return True; + + -- References to Ghost entities may be relocated in internally + -- generated bodies. + + elsif Nkind (Par) = N_Subprogram_Body + and then not Comes_From_Source (Par) + then + Subp_Id := Corresponding_Spec (Par); + + -- The original context is an expression function that has + -- been split into a spec and a body. The context is OK as + -- long as the the initial declaration is Ghost. + + if Present (Subp_Id) then + Subp_Decl := + Original_Node (Unit_Declaration_Node (Subp_Id)); + + if Nkind (Subp_Decl) = N_Expression_Function then + return Is_Subject_To_Ghost (Subp_Decl); + end if; + end if; + + -- Otherwise this is either an internal body or an internal + -- completion. Both are OK because the real check was done + -- before expansion activities. + + return True; + end if; + + -- Prevent the search from going too far + + if Is_Body_Or_Package_Declaration (Par) then + return False; + end if; + + Par := Parent (Par); + end loop; + + return False; + end Is_Ghost_Declaration; + + -- Start of processing for Is_OK_Ghost_Context + + begin + -- The Ghost entity appears within an assertion expression + + if In_Assertion_Expr > 0 then + return True; + + -- The Ghost entity is part of a declaration or its completion + + elsif Is_Ghost_Declaration (Context) then + return True; + + -- The Ghost entity is referenced within a Ghost statement + + elsif Is_Ghost_Statement_Or_Pragma (Context) then + return True; + + else + return False; + end if; + end Is_OK_Ghost_Context; + + ------------------------ + -- Check_Ghost_Policy -- + ------------------------ + + procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is + Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + + begin + -- The Ghost policy in effect a the point of declaration and at the + -- point of use must match (SPARK RM 6.9(13)). + + if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then + Error_Msg_Sloc := Sloc (Err_N); + + SPARK_Msg_N ("incompatible ghost policies in effect", Err_N); + SPARK_Msg_NE ("\& declared with ghost policy Check", Err_N, Id); + SPARK_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id); + + elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then + Error_Msg_Sloc := Sloc (Err_N); + + SPARK_Msg_N ("incompatible ghost policies in effect", Err_N); + SPARK_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id); + SPARK_Msg_NE ("\& used # with ghost policy Check", Err_N, Id); + end if; + end Check_Ghost_Policy; + + -- Start of processing for Check_Ghost_Context + + begin + -- Once it has been established that the reference to the Ghost entity + -- is within a suitable context, ensure that the policy at the point of + -- declaration and at the point of use match. + + if Is_OK_Ghost_Context (Ghost_Ref) then + Check_Ghost_Policy (Ghost_Id, Ghost_Ref); + + -- Otherwise the Ghost entity appears in a non-Ghost context and affects + -- its behavior or value. + + else + SPARK_Msg_N + ("ghost entity cannot appear in this context (SPARK RM 6.9(12))", + Ghost_Ref); + end if; + end Check_Ghost_Context; + ------------------------------ -- Check_Infinite_Recursion -- ------------------------------ @@ -5545,9 +5736,9 @@ package body Sem_Res is end if; if Is_Access_Subprogram_Type (Base_Type (Etype (Nam))) - and then not Is_Access_Subprogram_Type (Base_Type (Typ)) - and then Nkind (Subp) /= N_Explicit_Dereference - and then Present (Parameter_Associations (N)) + and then not Is_Access_Subprogram_Type (Base_Type (Typ)) + and then Nkind (Subp) /= N_Explicit_Dereference + and then Present (Parameter_Associations (N)) then -- The prefix is a parameterless function call that returns an access -- to subprogram. If parameters are present in the current call, add @@ -5808,6 +5999,12 @@ package body Sem_Res is Set_Is_Overloaded (Subp, False); Set_Is_Overloaded (N, False); + -- A Ghost entity must appear in a specific context + + if Is_Ghost_Entity (Nam) and then Comes_From_Source (N) then + Check_Ghost_Context (Nam, N); + end if; + -- If we are calling the current subprogram from immediately within its -- body, then that is the case where we can sometimes detect cases of -- infinite recursion statically. Do not try this in case restriction @@ -6855,38 +7052,48 @@ package body Sem_Res is Par := Parent (Par); end if; - -- An effectively volatile object subject to enabled properties - -- Async_Writers or Effective_Reads must appear in a specific context. -- The following checks are only relevant when SPARK_Mode is on as they -- are not standard Ada legality rules. - if SPARK_Mode = On - and then Is_Object (E) - and then Is_Effectively_Volatile (E) - and then Comes_From_Source (E) - and then - (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E)) - then - -- The effectively volatile objects appears in a "non-interfering - -- context" as defined in SPARK RM 7.1.3(13). + if SPARK_Mode = On then - if Is_OK_Volatile_Context (Par, N) then - null; + -- An effectively volatile object subject to enabled properties + -- Async_Writers or Effective_Reads must appear in a specific + -- context. + + if Is_Object (E) + and then Is_Effectively_Volatile (E) + and then + (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E)) + and then Comes_From_Source (N) + then + -- The effectively volatile objects appears in a "non-interfering + -- context" as defined in SPARK RM 7.1.3(13). - -- Assume that references to effectively volatile objects that appear - -- as actual parameters in a procedure call are always legal. A full - -- legality check is done when the actuals are resolved. + if Is_OK_Volatile_Context (Par, N) then + null; - elsif Nkind (Par) = N_Procedure_Call_Statement then - null; + -- Assume that references to effectively volatile objects that + -- appear as actual parameters in a procedure call are always + -- legal. A full legality check is done when the actuals are + -- resolved. - -- Otherwise the context causes a side effect with respect to the - -- effectively volatile object. + elsif Nkind (Par) = N_Procedure_Call_Statement then + null; - else - Error_Msg_N - ("volatile object cannot appear in this context " - & "(SPARK RM 7.1.3(13))", N); + -- Otherwise the context causes a side effect with respect to the + -- effectively volatile object. + + else + SPARK_Msg_N + ("volatile object cannot appear in this context " + & "(SPARK RM 7.1.3(13))", N); + end if; + + -- A Ghost entity must appear in a specific context + + elsif Is_Ghost_Entity (E) and then Comes_From_Source (N) then + Check_Ghost_Context (E, N); end if; end if; end Resolve_Entity_Name; -- cgit v1.1