From: Viljar Indus Date: Wed, 5 Mar 2025 09:18:20 +0000 (+0200) Subject: ada: Multiple levels of ghost code X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=5d5290455397c092d0b1189d980bc7b271d6eb5f;p=thirdparty%2Fgcc.git ada: Multiple levels of ghost code Adds support for the new language feature that allows ghost enties and assertion pragmas and aspects to be associated with a new entity called assertion level. Added support for a new pragma Assertion_Level that declares new assertion levels. This pragma consists of the level name and assertion levels it depends on. pragma Assertion_Level (L1); pragma Assertion_Level (L2); pragma Assertion_Level (L3, Depends => [L1, L2]); There are two special assertion levels that are considered to be declared in the Standard package that have unique properties. Assertion level Runtime is always considered to be Checked. Its assertion policy cannot be changed and it is considered that all other assertion levels depend on this level. Assertion level Static is always considered to be Ignored. Its assertion policy cannot be changed. All assertion levels that depend on this level can also never be activated. Aspect Ghost now supports the assertion level as a possible argument: ... with Ghost => Level; All pragmas and aspects which were considered to be valid assertion kinds for pragma Assertion_Policy now support assertion level associations. The association consists of an assertion level and a set of existing arguments. Note that you can have multiple assertion level associations in a given pragma or aspect. e.g. pragma Assert (Level1 => (Check => Expr1, Message => "Msg1", Level2 => (Check => Expr2, Message => "Msg2")); It is possible to set an explicit Assertion_Policy for those levels which can control the policies for all entities associated with those levels. Setting the policy Check for a given level means also that policy Check is set for all of the policies that it depends on. From the previous example. pragma Assertion_Policy (L3 => Check); is equivalent to: pragma Assertion_Policy (L1 => Check); pragma Assertion_Policy (L2 => Check); pragma Assertion_Policy (L3 => Check); Setting the policy Ignore for a given level means that the policy Ignore is also applied to all the levels that depend on it. e.g pragma Assertion_Policy (L2 => Ignore); is equivalent to: pragma Assertion_Policy (L2 => Ignore); pragma Assertion_Policy (L3 => Ignore); Since now ghost regions can contain other ghost regions with a different assertion policy then new rules needed to be added for those situations to ensure valid compilation. Additionally all rules where we checked for compatible assertion policies have an additional check for a compatible assertion level dependencies. Ghost entities A and B are considered assertion level dependent when * A or B does not have an associated assertion level. * Both A and B have an assertion level and either * the level of A is or depends on the level of B. * the level of B cannot be enabled (is or depends on Static) gcc/ada/ChangeLog: * atree.adb (Mark_New_Ghost_Node): Store the assertion level on the entity. * contracts.adb (Analyze_Package_Contract): Add support for multiple pragma Initial_Condition orginating from multiple assertion levels. * cstand.adb (Make_Assertion_Level_Definition): New function that creates a new Assertion_Level and adds it to the Assertion_Levels table. (Create_Standard): Add definitions for assertion levels defined in Standard. (Print_Standard): Add assertion level pragmas do the output. * exp_ch6.adb (Check_Subprogram_Variant): Add support for multiple Subprogram_Variant pragmas created by assertion levels. * einfo.ads: add info for the new nodes and attributes. * exp_prag.adb (Consequence_Error): Fix error message string corruption caused by another call to the internal strings during the call to Make_Procedure_Call_Statement. (Expand_Pragma_Initial_Condition): Ensure all ghost related attributes are copied to the new pragma. (Expand_Pragma_Loop_Variant): Likewise. (Expand_Pragma_Subprogram_Variant). Likewise. Additionally create a new Subprogram_Variant function for each pragma associated with an assertion level. * exp_util.adb (Add_DIC_Check): Ensure all ghost related attributes are copied to the new pragma. (Build_DIC_Procedure_Body): Add support for mutliple DIC pragmas created from assertion levels. * gen_il-fields.ads: (Aspect_Ghost_Assertion_Level): New field. (Original_Aspect): New field. (Original_Pragma): New field. (Pragma_Ghost_Assertion_Level): New field. (Child_Levels): New field. (Ghost_Assertion_Level): New field. (Parent_Levels): New field. * gen_il-gen-gen_entities.adb: Add Ghost_Assertion_Level field for all entities Add new E_Assertion_Level entity for storing assertion levels. * gen_il-gen-gen_nodes.adb: Add Aspect_Ghost_Assertion_Level for N_Aspect to store the assertion level associated with the aspect. Add Original_Aspect to store the original aspect where the aspect that was transformed from an aspect with an assertion level origninated from. Add Pragma_Ghost_Assertion_Level and Original_Pragma to store the same information for N_Prama nodes. * gen_il-types.ads: Add new entity kind E_Assertion_Level * ghost.adb (Assertion_Level_Error_Msg): Create constant for error messages using the same main error message. (Ghost_Policy_Error_Msg): Likewise. (Assertion_Level_To_Name): New subprogram. (Check_Valid_Ghost_Declaration): New subprogram. (Get_Ghost_Aspect): New subprogram. (Get_Ghost_Assertion_Level): New subprogram. (Ghost_Policy_In_Effect): New subprogram. (Install_Ghost_Region): New subprogram. (Mark_And_Set_Ghost_Region): New subprogram. (Mark_Ghost_Declaration_Or_Body): Add new argument for assertion levels. (Check_Ghost_Completion): Update ghost policy calculation with assertion levels. Refactor error message. (Is_OK_Statement): Add new checks for valid assertion policies and assertion levels. (Is_OK_Pragma): Refactor the calculation of valid ghost pragmas. (Check_Ghost_Policy): Make the checks ghost region based. (Check_Ghost_Context): Refactor the order of checks. (Check_Ghost_Formal_Procedure_Or_Package): Relax the checks for overriding procedures. Now only ignored subprograms cannot be overridden by checked or non-ghost subprograms. (Check_Ghost_Primitive): Relax conditions for primitve operations. Now only checked primitive subprograms are considered invalid for ignored tagged types. Add assertion level compatibility checks. (Check_Ghost_Refinement): Relax conditions for ghost refinements. Add assertion level compatibility checks for refinements. (Install_Ghost_Region): Store the current region and the assertion for that region in the ghost config. (Enables_Ghostness): Refactor implementation to support assertion levels. (Is_Subject_To_Ghost): Simplify implementation. (Mark_And_Set_Ghost_Assignment): Refactor implementation. (Mark_And_Set_Ghost_Body): Add support for assertion levels. (Mark_And_Set_Ghost_Completion): Likewise. (Mark_And_Set_Ghost_Declaration): Likwise. (Mark_And_Set_Ghost_Instantiation): Likwise. (Mark_And_Set_Ghost_Procedure_Call): Refactor implementation. (Mark_Ghost_Declaration_Or_Body): Add support for assertion levels. (Set_Ghost_Mode): Likwise. * ghost.ads (Assertion_Level_From_Arg): New subprogram. (Install_Ghost_Region): Add argument Level for assertrion levels. (Is_Assertion_Level_Dependent): New subprogram. * lib-xref.ads: Add new mapping for E_Assertion_Level entities. * opt.ads (Ghost_Config_Type): Add new members Ghost_Assertion_Mode and Current_Region to the structure. * par-prag.adb (Prag): Add new pragma name Assertion_Level. * rtsfind.adb (Load_RTU): Update the arguments for the call to Install_Ghost_Region. * sem.adb (Do_Analyze): Likewise. * sem_ch13.adb (Convert_Aspect_With_Assertion_Levels): New subprogram. (Make_Aitem_Pragma): Copy ghost mode attributes from the aspect to the pragma. (Analyze_Aspect_Specifications): Convert aspects that have an assertion level association in the aspects without the association and the original supported syntax and with the assertion level stored on the aspect node. Updated duplicate detection to avoid duplicates being called on aspects with assertion levels that orginated from the same aspect. * sem_prag.adb (Apply_Check_Policy): New subprogram. (Get_Applicable_Policy): New subprogram. (Mark_Is_Checked): New subprogram. (Mark_Is_Disabled): New subprogram. (Mark_Is_Ignored): New subprgram. (Check_Arg_Is_One_Of): Remove versions that had a specific number of arguments and replace them with a list one. (Create_Pragma_Without_Assertion_Level): New subprogram. (Assertion_Level_Pragma_Comes_From_Source): New subprogram. (Analyze_Pragma): Replace aspects that have an assertion level with aspects without them where the level is stored on the pragma node. (Abstract_State): Add support for assertion levels in ghost Abstract_State pragmas. (Assert): Update argument handling for Assert like pragmas. (Assertion_Level): Add a new section to support the analysis of pragma Assertion_Level. (Assertion_Policy): Add support for setting the policy for assertion levels. (Check): Update argument handling. Update the assertion policy application process. (Check_Policy): Add support for assertion levels. Add check_policy pragmas for assertion_level dependencis also to the stack of known Check_Policy pragmas. (Default_Initial_Condition): Reject the use of DIC with assertion levels. Update duplication checks. (Ghost): Add support for assertion levels. Fix issue where assertion levels with Ghost => False were treated as ghost. (Predicate): Update the policy handling of Ghost_Predicate. (Analyze_Refined_State_In_Decl_Part): Create a new ghost region for analyzing Refined_State. (Check_Applicable_Policy): Refactor the implementation. Break it down to Get_Applicable_Policy and Apply_Check_Policy. (Check_Kind): Removed. Replaced by Get_Applicable_Policy and Apply_Check_Policy. (Initialize): Initialize the table storing all know assertion levels. * sem_prag.ads (Find_Assertion_Level): New subprogram. (Insert_Assertion_Level): New subprogram. (Check_Applicable_Policy): Add new argument Level. (Check_Kind): Removed. Merged with Get_Applicable_Policy. (Get_Assertion_Level): New subprogram. (Is_Valid_Assertion_Level): New subprogram. * sem_util.adb (Copy_Assertion_Policy_Attributes): New function for copying the ghost related attributes from one pragma to another. (Copy_Subprogram_Spec): Additionally copy the level from the spec. (Depends_On_Level): New function for checking if one level depends on another level. (From_Same_Aspect): New function for checking whether the aspects orignate from the same original aspect. (From_Same_Pragma): New function for checking whether the pragmas originate from the same original aspect or pragma. (Get_Subprogram_Entity): Avoid crash when being called when the entity has not been set for the subprogram. (Has_Assertion_Level_Argument): New function for checking whether the aspect or a pragma has an argument that is using an assertion level association. (Policy_In_Effect): add an additional argument for the level that should be checked along with the assertion name. * sem_util.ads (Copy_Assertion_Policy_Attributes): New function. (Depends_On_Level): Likewise. (From_Same_Aspect): Likewise. (From_Same_Pragma): Likewise. (Has_Assertion_Level_Argument): Likewise. (Is_Same_Or_Depends_On_Level): Likewise. (Policy_In_Effect): Add new argument Level. * sinfo.ads: Add documentation for all the new attributes that were added to the nodes and entities. * snames.ads-tmpl: Add new entries for Name_Assertion_Level, Name_uDefault_Assertion_Level and Pragma_Assertion_Level. * stand.ads: Add new entities for the predefined assertion levels. (Standard_Level_Static): Definition for the predefined Static level that is always ignored. (Standard_Level_Runtime): Defintion for the predefined Runtime level that is always checked. (Standard_Level_Default): Definition for the implicit Default level that is given for ghost entities that were not associated with an assertion level (e.g. Ghost => True). * tbuild.adb (Make_Assertion_Level): New function for constructin an assertion level. * tbuild.ads (Make_Assertion_Level): Likewise. --- diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 0ff3d6e34a8..197d1ee5121 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -1805,11 +1805,15 @@ package body Atree is if Ghost_Config.Ghost_Mode = Check then if Nkind (N) in N_Entity then Set_Is_Checked_Ghost_Entity (N); + Set_Ghost_Assertion_Level + (N, Ghost_Config.Ghost_Mode_Assertion_Level); end if; elsif Ghost_Config.Ghost_Mode = Ignore then if Nkind (N) in N_Entity then Set_Is_Ignored_Ghost_Entity (N); + Set_Ghost_Assertion_Level + (N, Ghost_Config.Ghost_Mode_Assertion_Level); end if; Set_Is_Ignored_Ghost_Node (N); diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 7e4e4a2077f..b7b2c507885 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -1278,7 +1278,12 @@ package body Contracts is while Present (Prag) loop Prag_Nam := Pragma_Name (Prag); - if Prag_Nam = Name_Initial_Condition then + -- When Assertion_Levels are used then the pacakage can have + -- multiple consecutive Initial_Condition pragmas. + -- Find the first one here and then iterate over all of them + -- later. + + if Prag_Nam = Name_Initial_Condition and then No (Init_Cond) then Init_Cond := Prag; elsif Prag_Nam = Name_Initializes then @@ -1295,9 +1300,12 @@ package body Contracts is Analyze_Initializes_In_Decl_Part (Init); end if; - if Present (Init_Cond) then + while Present (Init_Cond) + and then Pragma_Name (Init_Cond) = Name_Initial_Condition + loop Analyze_Initial_Condition_In_Decl_Part (Init_Cond); - end if; + Init_Cond := Next_Pragma (Init_Cond); + end loop; end if; -- Restore the SPARK_Mode of the enclosing context after all delayed diff --git a/gcc/ada/cstand.adb b/gcc/ada/cstand.adb index 79e7083f62b..cdf2b5d6c30 100644 --- a/gcc/ada/cstand.adb +++ b/gcc/ada/cstand.adb @@ -41,6 +41,7 @@ with Targparm; use Targparm; with Tbuild; use Tbuild; with Ttypes; use Ttypes; with Sem_Mech; use Sem_Mech; +with Sem_Prag; use Sem_Prag; with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; with Sinfo.Nodes; use Sinfo.Nodes; @@ -456,6 +457,11 @@ package body CStand is procedure Make_Dummy_Index (E : Entity_Id); -- Called to provide a dummy index field value for Any_Array/Any_String + function Make_Assertion_Level_Definition + (Nam : Name_Id) return Entity_Id; + -- Create an Assertion_Level definition with the given name in the' + -- Sandard package. + procedure Pack_String_Type (String_Type : Entity_Id); -- Generate proper tree for pragma Pack that applies to given type, and -- mark type as having the pragma. @@ -558,6 +564,18 @@ package body CStand is Set_First_Index (E, Index); end Make_Dummy_Index; + ------------------------------------- + -- Make_Assertion_Level_Definition -- + ------------------------------------- + + function Make_Assertion_Level_Definition (Nam : Name_Id) return Entity_Id + is + Level : constant Entity_Id := Make_Assertion_Level (Stloc, Nam); + begin + Insert_Assertion_Level (Level); + return Level; + end Make_Assertion_Level_Definition; + ---------------------- -- Pack_String_Type -- ---------------------- @@ -1494,6 +1512,11 @@ package body CStand is Set_Size_Known_At_Compile_Time (Standard_Duration); end Build_Duration; + Standard_Level_Static := Make_Assertion_Level_Definition (Name_Static); + Standard_Level_Runtime := Make_Assertion_Level_Definition (Name_Runtime); + Standard_Level_Default := + Make_Assertion_Level_Definition (Name_uDefault_Assertion_Level); + -- Build standard exception type. Note that the type name here is -- actually used in the generated code, so it must be set correctly. -- The type Standard_Exception_Type must be consistent with the type @@ -1935,6 +1958,10 @@ package body CStand is P ("-- characteristics of the Standard types for this compiler"); Write_Eol; + P ("pragma Assertion_Level (Runtime);"); + P ("pragma Assertion_Level (Static);"); + Write_Eol; + P ("package Standard is"); P ("pragma Pure (Standard);"); Write_Eol; diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 916d9c6f47c..97abab9e96a 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -608,6 +608,10 @@ package Einfo is -- determine if there actually is an active Suppress or Unsuppress pragma -- that applies to the entity. +-- Child_Levels +-- Assrtion levels that depend on the given level are considered to be +-- the child levels of that level. + -- Class_Postconditions -- Defined on subprogram entities. Set if the subprogram has class-wide -- postconditions. Denotes the (and-then) expression built by merging @@ -1461,6 +1465,12 @@ package Einfo is -- associates generic parameters with the corresponding instances, in -- those cases where the instance is an entity. +-- Ghost_Assertion_Level +-- Assertion level associated with the declaration of the entity. Its +-- value is either Empty for non-ghost entities. Standard_Level_Default +-- for Ghost entities without an assertion level or a user defined +-- assertion level. + -- Has_Aliased_Components [implementation base type only] -- Defined in array type entities. Indicates that the component type -- of the array is aliased. Should this also be set for records to @@ -4008,6 +4018,10 @@ package Einfo is -- used when obtaining the formal kind of a formal parameter (the result -- is one of E_[In/Out/In_Out]_Parameter). +-- Parent_Levels +-- Assrtion levels that the given level depends on are considered to be +-- parent levels of that level. + -- Parent_Subtype [base type only] -- Defined in E_Record_Type. Set only for derived tagged types, in which -- case it points to the subtype of the parent type. This is the type @@ -5243,6 +5257,10 @@ package Einfo is -- Number_Dimensions (synth) -- (plus type attributes) + -- E_Assertion_Level + -- Child_Levels + -- Parent_Levels + -- E_Block -- Renamed_Entity $$$ -- Renamed_Object $$$ diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index e8774699a66..a58fb667c8e 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -4027,7 +4027,8 @@ package body Exp_Ch6 is procedure Check_Subprogram_Variant; -- Emit a call to the internally generated procedure with checks for - -- aspect Subprogram_Variant, if present and enabled. + -- aspect Subprogram_Variant, if present and enabled. Multiple calls are + -- added when the subprogram was using Assertion_Levels. function Inherited_From_Formal (S : Entity_Id) return Entity_Id; -- Within an instance, a type derived from an untagged formal derived @@ -4312,7 +4313,7 @@ package body Exp_Ch6 is -- Local variables - Variant_Prag : constant Node_Id := + Variant_Prag : Node_Id := Get_Pragma (Current_Scope, Pragma_Subprogram_Variant); New_Call : Node_Id; @@ -4320,8 +4321,10 @@ package body Exp_Ch6 is Variant_Proc : Entity_Id; begin - if Present (Variant_Prag) and then Is_Checked (Variant_Prag) then - + while Present (Variant_Prag) + and then Is_Checked (Variant_Prag) + and then Pragma_Name (Variant_Prag) = Name_Subprogram_Variant + loop Pragma_Arg1 := Expression (First (Pragma_Argument_Associations (Variant_Prag))); @@ -4330,12 +4333,13 @@ package body Exp_Ch6 is -- run-time execution. if Nkind (Pragma_Arg1) = N_Aggregate then - pragma Assert - (Chars - (First - (Choices - (First (Component_Associations (Pragma_Arg1))))) = - Name_Structural); + pragma + Assert + (Chars + (First + (Choices + (First (Component_Associations (Pragma_Arg1))))) + = Name_Structural); return; end if; @@ -4345,7 +4349,8 @@ package body Exp_Ch6 is Variant_Proc := Entity (Pragma_Arg1); New_Call := - Make_Procedure_Call_Statement (Loc, + Make_Procedure_Call_Statement + (Loc, Name => New_Occurrence_Of (Variant_Proc, Loc), Parameter_Associations => @@ -4353,9 +4358,13 @@ package body Exp_Ch6 is Insert_Action (Call_Node, New_Call); - pragma Assert (Etype (New_Call) /= Any_Type - or else Serious_Errors_Detected > 0); - end if; + pragma + Assert + (Etype (New_Call) /= Any_Type + or else Serious_Errors_Detected > 0); + + Variant_Prag := Next_Pragma (Variant_Prag); + end loop; end Check_Subprogram_Variant; --------------------------- diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index 7ec963a1950..f60bca0e896 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -1520,7 +1520,7 @@ package body Exp_Prag is is Cond : Node_Id; Error : Node_Id; - + Str : String_Id; begin -- Generate: -- Flag and then not Conseq @@ -1540,12 +1540,17 @@ package body Exp_Prag is Store_String_Chars ("failed contract case at "); Store_String_Chars (Build_Location_String (Sloc (Conseq))); + -- Store the string value as the call to RTE can cause a new unit to + -- be loaded which causes new strings to be created. + + Str := End_String; + Error := Make_Procedure_Call_Statement (Loc, Name => New_Occurrence_Of (RTE (RE_Raise_Assert_Failure), Loc), Parameter_Associations => New_List ( - Make_String_Literal (Loc, End_String))); + Make_String_Literal (Loc, Str))); if No (Checks) then Checks := @@ -2516,6 +2521,7 @@ package body Exp_Prag is Call : Node_Id; Call_List : List_Id; Call_Loc : Source_Ptr; + Check_Prag : Node_Id; Expr : Node_Id; Loc : Source_Ptr; Proc_Body : Node_Id; @@ -2604,6 +2610,20 @@ package body Exp_Prag is -- pragma Check (Initial_Condition, ); -- end Initial_Condition; + Check_Prag := + Make_Pragma + (Loc, + Chars => Name_Check, + Pragma_Argument_Associations => + New_List + (Make_Pragma_Argument_Association + (Loc, + Expression => + Make_Identifier (Loc, Name_Initial_Condition)), + Make_Pragma_Argument_Association + (Loc, Expression => New_Copy_Tree (Expr)))); + Copy_Assertion_Policy_Attributes (Check_Prag, IC_Prag); + Proc_Body := Make_Subprogram_Body (Loc, Specification => @@ -2611,15 +2631,7 @@ package body Exp_Prag is Declarations => Empty_List, Handled_Statement_Sequence => Make_Handled_Sequence_Of_Statements (Loc, - Statements => New_List ( - Make_Pragma (Loc, - Chars => Name_Check, - Pragma_Argument_Associations => New_List ( - Make_Pragma_Argument_Association (Loc, - Expression => - Make_Identifier (Loc, Name_Initial_Condition)), - Make_Pragma_Argument_Association (Loc, - Expression => New_Copy_Tree (Expr))))))); + Statements => New_List (Check_Prag))); Append_To (Body_List, Proc_Body); @@ -2943,6 +2955,7 @@ package body Exp_Prag is Typ => Expr_Typ, Curr_Val => New_Occurrence_Of (Curr_Id, Loc), Old_Val => New_Occurrence_Of (Old_Id, Loc))))); + Copy_Assertion_Policy_Attributes (Prag, N); -- Generate: -- if Curr /= Old then @@ -3221,6 +3234,11 @@ package body Exp_Prag is -- Prev_Decl and is stored in this parameter for a next call to this -- routine. Is_Last is True when there are no more variants to process. + function Variants_Function_Name (Prag : Node_Id) return Name_Id; + -- The name of the variants function is either + -- * _variants: if no assertion level was associated with the pragma. + -- * _variants_ otherwise. + ---------------------- -- Formal_Param_Map -- ---------------------- @@ -3264,11 +3282,11 @@ package body Exp_Prag is Expr_Typ : constant Entity_Id := Etype (Expr); Loc : constant Source_Ptr := Sloc (Expr); - Old_Id : Entity_Id; - Old_Decl : Node_Id; - Curr_Id : Entity_Id; - Curr_Decl : Node_Id; - Prag : Node_Id; + Old_Id : Entity_Id; + Old_Decl : Node_Id; + Curr_Id : Entity_Id; + Curr_Decl : Node_Id; + Check_Prag : Node_Id; begin -- Create temporaries that store the old values of the associated @@ -3308,7 +3326,7 @@ package body Exp_Prag is -- Generate: -- pragma Check (Variant, Curr <|> Old); - Prag := + Check_Prag := Make_Pragma (Loc, Chars => Name_Check, Pragma_Argument_Associations => New_List ( @@ -3323,6 +3341,7 @@ package body Exp_Prag is Typ => Expr_Typ, Curr_Val => New_Occurrence_Of (Curr_Id, Loc), Old_Val => New_Occurrence_Of (Old_Id, Loc))))); + Copy_Assertion_Policy_Attributes (Check_Prag, Prag); -- Generate: -- if Curr /= Old then @@ -3335,7 +3354,7 @@ package body Exp_Prag is -- pragma. if Is_Last then - If_Stmt := Prag; + If_Stmt := Check_Prag; else If_Stmt := Make_If_Statement (Loc, @@ -3343,7 +3362,7 @@ package body Exp_Prag is Make_Op_Ne (Loc, Left_Opnd => New_Occurrence_Of (Curr_Id, Loc), Right_Opnd => New_Occurrence_Of (Old_Id, Loc)), - Then_Statements => New_List (Prag)); + Then_Statements => New_List (Check_Prag)); end if; -- Generate: @@ -3352,7 +3371,7 @@ package body Exp_Prag is -- end if; elsif Is_Last then - Set_Else_Statements (If_Stmt, New_List (Prag)); + Set_Else_Statements (If_Stmt, New_List (Check_Prag)); -- Generate: -- elsif Curr /= Old then @@ -3369,10 +3388,30 @@ package body Exp_Prag is Make_Op_Ne (Loc, Left_Opnd => New_Occurrence_Of (Curr_Id, Loc), Right_Opnd => New_Occurrence_Of (Old_Id, Loc)), - Then_Statements => New_List (Prag))); + Then_Statements => New_List (Check_Prag))); end if; end Process_Variant; + ---------------------------- + -- Variants_Function_Name -- + ---------------------------- + + function Variants_Function_Name (Prag : Node_Id) return Name_Id is + begin + if Present (Pragma_Ghost_Assertion_Level (Prag)) + and then Pragma_Ghost_Assertion_Level (Prag) + /= Standard_Level_Default + then + Get_Name_String (Name_uVariants); + Add_Str_To_Name_Buffer ("_"); + Get_Name_String_And_Append + (Chars (Pragma_Ghost_Assertion_Level (Prag))); + return Name_Enter; + else + return Name_uVariants; + end if; + end Variants_Function_Name; + -- Local variables Loc : constant Source_Ptr := Sloc (Prag); @@ -3386,6 +3425,7 @@ package body Exp_Prag is Proc_Bod : Node_Id; Proc_Decl : Node_Id; Proc_Id : Entity_Id; + Proc_Nam : Name_Id; Proc_Spec : Node_Id; Variant : Node_Id; @@ -3411,7 +3451,9 @@ package body Exp_Prag is -- variant expressions captured at the start of subprogram with their -- values at the recursive call of the subprogram. - Proc_Id := Make_Defining_Identifier (Loc, Name_uVariants); + Proc_Nam := Variants_Function_Name (Prag); + + Proc_Id := Make_Defining_Identifier (Loc, Proc_Nam); Proc_Spec := Make_Procedure_Specification diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index e9ec7b73d87..ed515d0d49e 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1893,12 +1893,11 @@ package body Exp_Util is ------------------- procedure Add_DIC_Check - (DIC_Prag : Node_Id; - DIC_Expr : Node_Id; - Stmts : in out List_Id) + (DIC_Prag : Node_Id; DIC_Expr : Node_Id; Stmts : in out List_Id) is - Loc : constant Source_Ptr := Sloc (DIC_Prag); - Nam : constant Name_Id := Original_Aspect_Pragma_Name (DIC_Prag); + Loc : constant Source_Ptr := Sloc (DIC_Prag); + Nam : constant Name_Id := Original_Aspect_Pragma_Name (DIC_Prag); + Prag : Node_Id; begin -- The DIC pragma is ignored, nothing left to do @@ -1908,21 +1907,25 @@ package body Exp_Util is -- Otherwise the DIC expression must be checked at run time. -- Generate: - + -- -- pragma Check (, ); else - Append_New_To (Stmts, - Make_Pragma (Loc, - Pragma_Identifier => - Make_Identifier (Loc, Name_Check), + Prag := + Make_Pragma + (Loc, + Pragma_Identifier => + Make_Identifier (Loc, Name_Check), + Pragma_Argument_Associations => + New_List + (Make_Pragma_Argument_Association + (Loc, Expression => Make_Identifier (Loc, Nam)), + Make_Pragma_Argument_Association + (Loc, Expression => DIC_Expr))); - Pragma_Argument_Associations => New_List ( - Make_Pragma_Argument_Association (Loc, - Expression => Make_Identifier (Loc, Nam)), + Copy_Assertion_Policy_Attributes (Prag, DIC_Prag); - Make_Pragma_Argument_Association (Loc, - Expression => DIC_Expr)))); + Append_New_To (Stmts, Prag); end if; -- Add the pragma to the list of processed pragmas @@ -2318,6 +2321,7 @@ package body Exp_Util is DIC_Typ : Entity_Id; Dummy_1 : Entity_Id; Dummy_2 : Entity_Id; + Prag : Node_Id; Proc_Body : Node_Id; Proc_Body_Id : Entity_Id; Proc_Decl : Node_Id; @@ -2464,12 +2468,23 @@ package body Exp_Util is if Partial_DIC then pragma Assert (Present (Priv_Typ)); - if Has_Own_DIC (Work_Typ) then -- If we're testing this then maybe - Add_Own_DIC -- we shouldn't be calling Find_DIC_Typ above??? - (DIC_Prag => DIC_Prag, - DIC_Typ => DIC_Typ, -- Should this just be Work_Typ??? - Obj_Id => Obj_Id, - Stmts => Stmts); + if Has_Own_DIC (Work_Typ) then + -- If we're testing this then maybe + + Prag := DIC_Prag; + while Present (Prag) + and then Nkind (Prag) = N_Pragma + and then Pragma_Name (Prag) = Name_Default_Initial_Condition + and then (Prag = DIC_Prag + or else From_Same_Pragma (Prag, DIC_Prag)) + loop + Add_Own_DIC -- we shouldn't be calling Find_DIC_Typ above??? + (DIC_Prag => Prag, + DIC_Typ => DIC_Typ, -- Should this just be Work_Typ??? + Obj_Id => Obj_Id, + Stmts => Stmts); + Next_Rep_Item (Prag); + end loop; end if; -- Otherwise, the "full" DIC procedure verifies the DICs inherited from @@ -3229,8 +3244,9 @@ package body Exp_Util is Ploc : constant Source_Ptr := Sloc (Prag); Str_Arg : constant Node_Id := Next (Next (First (Args))); - Assoc : List_Id; - Str : String_Id; + Assoc : List_Id; + Check_Prag : Node_Id; + Str : String_Id; begin -- The invariant is ignored, nothing left to do @@ -3273,10 +3289,14 @@ package body Exp_Util is -- Generate: -- pragma Check (, , ); - Append_New_To (Checks, + Check_Prag := Make_Pragma (Ploc, - Chars => Name_Check, - Pragma_Argument_Associations => Assoc)); + Chars => Name_Check, + Pragma_Argument_Associations => Assoc); + + Copy_Assertion_Policy_Attributes (Check_Prag, Prag); + + Append_New_To (Checks, Check_Prag); end if; -- Output an info message when inheriting an invariant and the diff --git a/gcc/ada/gen_il-fields.ads b/gcc/ada/gen_il-fields.ads index a1e284f14e4..4ebefd2c68e 100644 --- a/gcc/ada/gen_il-fields.ads +++ b/gcc/ada/gen_il-fields.ads @@ -72,6 +72,7 @@ package Gen_IL.Fields is Ancestor_Part, Atomic_Sync_Required, Array_Aggregate, + Aspect_Ghost_Assertion_Level, Aspect_On_Partial_View, Aspect_Rep_Item, Aspect_Specifications, @@ -336,8 +337,10 @@ package Gen_IL.Fields is Null_Statement, Object_Definition, Of_Present, + Original_Aspect, Original_Discriminant, Original_Entity, + Original_Pragma, Others_Discrete_Choices, Out_Present, Parameter_Associations, @@ -347,6 +350,7 @@ package Gen_IL.Fields is Parent_With, Position, Pragma_Argument_Associations, + Pragma_Ghost_Assertion_Level, Pragma_Identifier, Pragmas_After, Pragmas_Before, @@ -463,6 +467,7 @@ package Gen_IL.Fields is Can_Never_Be_Null, Can_Use_Internal_Rep, Checks_May_Be_Suppressed, + Child_Levels, Class_Postconditions, Class_Preconditions, Class_Preconditions_Subprogram, @@ -557,6 +562,7 @@ package Gen_IL.Fields is Full_View, Generic_Homonym, Generic_Renamings, + Ghost_Assertion_Level, Has_Aliased_Components, Has_Alignment_Clause, Has_All_Calls_Remote, @@ -860,6 +866,7 @@ package Gen_IL.Fields is Overridden_Operation, Package_Instantiation, Packed_Array_Impl_Type, + Parent_Levels, Parent_Subtype, Part_Of_Constituents, Part_Of_References, diff --git a/gcc/ada/gen_il-gen-gen_entities.adb b/gcc/ada/gen_il-gen-gen_entities.adb index 0fedfbc6099..00d49133af2 100644 --- a/gcc/ada/gen_il-gen-gen_entities.adb +++ b/gcc/ada/gen_il-gen-gen_entities.adb @@ -63,6 +63,7 @@ begin -- Gen_IL.Gen.Gen_Entities Sm (First_Rep_Item, Node_Id), Sm (Freeze_Node, Node_Id), Sm (From_Limited_With, Flag), + Sm (Ghost_Assertion_Level, Node_Id), Sm (Has_Aliased_Components, Flag, Impl_Base_Type_Only), Sm (Has_Alignment_Clause, Flag), Sm (Has_All_Calls_Remote, Flag), @@ -1344,6 +1345,17 @@ begin -- Gen_IL.Gen.Gen_Entities Sm (SPARK_Pragma, Node_Id), Sm (SPARK_Pragma_Inherited, Flag))); + Cc (E_Assertion_Level, Entity_Kind, + -- An assertion level. Used to associate a level indicator to an + -- assertion like construct. Constructs assigned with a certain level + -- can be disabled through pragma Assertion_Policy. Levels can form a + -- hierarchy. A declaration of a level can include a list of levels + -- this level depends on known as the Parent_Levels. An opposite list + -- is also kept to store all the levels that depend on it known as the + -- Child_Levels. + (Sm (Child_Levels, Elist_Id), + Sm (Parent_Levels, Elist_Id))); + -- Union types. These don't fit into the normal parent/child hierarchy -- above. diff --git a/gcc/ada/gen_il-gen-gen_nodes.adb b/gcc/ada/gen_il-gen-gen_nodes.adb index 412565f42a8..0acc1849ba9 100644 --- a/gcc/ada/gen_il-gen-gen_nodes.adb +++ b/gcc/ada/gen_il-gen-gen_nodes.adb @@ -1127,6 +1127,7 @@ begin -- Gen_IL.Gen.Gen_Nodes (Sy (Identifier, Node_Id, Default_Empty), Sy (Expression, Node_Id, Default_Empty), Sy (Class_Present, Flag), + Sm (Aspect_Ghost_Assertion_Level, Node_Id), Sm (Aspect_On_Partial_View, Flag), Sm (Aspect_Rep_Item, Node_Id), Sm (Aspect_Subprograms, Elist_Id), @@ -1137,7 +1138,8 @@ begin -- Gen_IL.Gen.Gen_Nodes Sm (Is_Delayed_Aspect, Flag), Sm (Is_Disabled, Flag), Sm (Is_Ignored, Flag), - Sm (Next_Rep_Item, Node_Id))); + Sm (Next_Rep_Item, Node_Id), + Sm (Original_Aspect, Node_Id))); Cc (N_Call_Marker, Node_Kind, (Sm (Is_Declaration_Level_Node, Flag), @@ -1444,6 +1446,8 @@ begin -- Gen_IL.Gen.Gen_Nodes Sm (Is_Ignored_Ghost_Pragma, Flag), Sm (Next_Pragma, Node_Id), Sm (Next_Rep_Item, Node_Id), + Sm (Original_Pragma, Node_Id), + Sm (Pragma_Ghost_Assertion_Level, Node_Id), Sm (Uneval_Old_Accept, Flag), Sm (Uneval_Old_Warn, Flag))); diff --git a/gcc/ada/gen_il-types.ads b/gcc/ada/gen_il-types.ads index c3a97558f70..66d912721fa 100644 --- a/gcc/ada/gen_il-types.ads +++ b/gcc/ada/gen_il-types.ads @@ -445,6 +445,7 @@ package Gen_IL.Types is -- Concrete entity types: E_Void, + E_Assertion_Level, E_Component, E_Constant, E_Discriminant, diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index f9c285316cd..4af4e4be93e 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -38,12 +38,12 @@ with Sem_Aux; use Sem_Aux; with Sem_Disp; use Sem_Disp; with Sem_Eval; use Sem_Eval; with Sem_Prag; use Sem_Prag; -with Sem_Res; use Sem_Res; with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; with Sinfo.Nodes; use Sinfo.Nodes; with Sinfo.Utils; use Sinfo.Utils; with Snames; use Snames; +with Stand; use Stand; with Table; package body Ghost is @@ -63,18 +63,49 @@ package body Ghost is Table_Increment => Alloc.Ignored_Ghost_Nodes_Increment, Table_Name => "Ignored_Ghost_Nodes"); + --------------------- + -- Local variables -- + --------------------- + + Assertion_Level_Error_Msg : constant String := + "incompatible assertion levels in effect"; + + Ghost_Policy_Error_Msg : constant String := + "incompatible ghost policies in effect"; + ----------------------- -- Local subprograms -- ----------------------- - procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type); - pragma Inline (Install_Ghost_Mode); - -- Install Ghost mode Mode as the Ghost mode in effect + function Assertion_Level_To_Name (Level : Entity_Id) return Name_Id; + -- Returns No_Name if there is no Level or the name of the Level. + + procedure Check_Valid_Ghost_Declaration (N : Node_Id); + -- Check that the declaration for a Ghost node N has a valid + -- Assertion_Policy and a valid Assertion_Level. + + function Get_Ghost_Aspect (N : Node_Id) return Node_Id; + -- Returns the Ghost aspect for a given node if it has one. - procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id); + function Get_Ghost_Pragma (N : Node_Id) return Node_Id; + -- Return the Ghost pragma following this node. + + function Get_Ghost_Assertion_Level (N : Node_Id) return Entity_Id; + -- Returns the Assertion_Level entity if the node has a Ghost aspect and + -- the Ghost aspect is using an Assertion_Level. + + function Ghost_Policy_In_Effect (Id : Entity_Id) return Name_Id; + -- Returns the first Assertion Policy in place for either Ghost or the + -- Assertion_Level associated with Ghost aspect on the the declaration node + -- Decl. + + procedure Install_Ghost_Region + (Mode : Name_Id; + N : Node_Id; + Level : Entity_Id); pragma Inline (Install_Ghost_Region); -- Install a Ghost region comprised of mode Mode and ignored region start - -- node N. + -- node N and Level as the Assertion_Level that was associated with it. function Is_Subject_To_Ghost (N : Node_Id) return Boolean; -- Determine whether declaration or body N is subject to aspect or pragma @@ -82,17 +113,82 @@ package body Ghost is -- been analyzed yet, but the context needs to establish the "ghostness" -- of N. + procedure Mark_And_Set_Ghost_Region (N : Node_Id; Id : Entity_Id); + -- Install a new ghost region for N based on the active policy applied for + -- Id. Additionally if the policy is ignored mark and set the node as an + -- ignored ghost region. + procedure Mark_Ghost_Declaration_Or_Body - (N : Node_Id; - Mode : Name_Id); + (N : Node_Id; + Mode : Name_Id; + Level : Entity_Id); -- Mark the defining entity of declaration or body N as Ghost depending on -- mode Mode. Mark all formals parameters when N denotes a subprogram or a - -- body. + -- body. Additionally set level as the Ghost_Assertion_Level for all of + -- them. procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id); -- Save ignored Ghost node or entity N in table Ignored_Ghost_Nodes for -- later elimination. + ------------------------------ + -- Assertion_Level_From_Arg -- + ------------------------------ + + function Assertion_Level_From_Arg (Arg : Node_Id) return Entity_Id is + Expr : constant Node_Id := Get_Pragma_Arg (Arg); + Level : Entity_Id; + + begin + -- Aspect Ghost without an expression uses Standard_Level_Default + + if No (Expr) then + return Standard_Level_Default; + end if; + + -- Check if the expression matches a static boolean expression first + + Preanalyze_And_Resolve_Without_Errors (Expr); + if Is_OK_Static_Expression (Expr) then + if Is_True (Expr_Value (Expr)) then + return Standard_Level_Default; + else + -- Ghost => False is considered to be non-ghost + + return Empty; + end if; + end if; + + -- Alternatively the argument could be an Assertion_Level + + if Nkind (Expr) = N_Identifier + and then Present (Get_Assertion_Level (Chars (Expr))) + then + Level := Get_Assertion_Level (Chars (Expr)); + if Present (Level) then + return Level; + end if; + end if; + + -- We are dealing with a malformed ghost argument. + -- An error will be emitted when the pragma is analyzed. + + return Empty; + end Assertion_Level_From_Arg; + + ----------------------------- + -- Assertion_Level_To_Name -- + ----------------------------- + + function Assertion_Level_To_Name (Level : Entity_Id) return Name_Id is + begin + if No (Level) then + return No_Name; + end if; + + return Chars (Level); + end Assertion_Level_To_Name; + ---------------------------- -- Check_Ghost_Completion -- ---------------------------- @@ -101,23 +197,26 @@ package body Ghost is (Prev_Id : Entity_Id; Compl_Id : Entity_Id) is - Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + Policy : Name_Id; begin -- Nothing to do if one of the views is missing if No (Prev_Id) or else No (Compl_Id) then - null; + return; + end if; + + Policy := Ghost_Policy_In_Effect (Prev_Id); -- The Ghost policy in effect at the point of declaration and at the -- point of completion must match (SPARK RM 6.9(16)). - elsif Is_Checked_Ghost_Entity (Prev_Id) + if Is_Checked_Ghost_Entity (Prev_Id) and then Policy = Name_Ignore then Error_Msg_Sloc := Sloc (Compl_Id); - Error_Msg_N ("incompatible ghost policies in effect", Prev_Id); + Error_Msg_N (Ghost_Policy_Error_Msg, Prev_Id); Error_Msg_N ("\& declared with ghost policy `Check`", Prev_Id); Error_Msg_N ("\& completed # with ghost policy `Ignore`", Prev_Id); @@ -126,7 +225,7 @@ package body Ghost is then Error_Msg_Sloc := Sloc (Compl_Id); - Error_Msg_N ("incompatible ghost policies in effect", Prev_Id); + Error_Msg_N (Ghost_Policy_Error_Msg, Prev_Id); Error_Msg_N ("\& declared with ghost policy `Ignore`", Prev_Id); Error_Msg_N ("\& completed # with ghost policy `Check`", Prev_Id); end if; @@ -175,7 +274,8 @@ package body Ghost is -- -- * Contain a reference to a Ghost entity - function Is_OK_Statement (Stmt : Node_Id) return Boolean; + function Is_OK_Statement + (Stmt : Node_Id; Id : Entity_Id; Call_Arg : Node_Id) return Boolean; -- Determine whether node Stmt is a suitable context for a reference -- to a Ghost entity. To qualify as such, Stmt must either -- @@ -309,19 +409,17 @@ package body Ghost is function Is_OK_Pragma (Prag : Node_Id; Id : Entity_Id) return Boolean is - procedure Check_Policies (Prag_Nam : Name_Id); + procedure Check_Policies; -- Verify that the Ghost policy in effect at the point of the - -- declaration of Ghost entity Id (if present) is the same as the - -- assertion policy for pragma name Prag_Nam. Emit an error if - -- this is not the case. + -- declaration of Ghost entity Id (if present) is the same as + -- the assertion policy for the pragma. Emit an error if this + -- is not the case. -------------------- -- Check_Policies -- -------------------- - procedure Check_Policies (Prag_Nam : Name_Id) is - AP : constant Name_Id := Check_Kind (Prag_Nam); - + procedure Check_Policies is begin -- If the Ghost policy in effect at the point of the -- declaration of Ghost entity Id is Ignore, then the assertion @@ -329,18 +427,15 @@ package body Ghost is if Present (Id) and then not Is_Checked_Ghost_Entity (Id) - and then AP /= Name_Ignore + and then not Is_Ignored (Prag) then - Error_Msg_N - ("incompatible ghost policies in effect", - Ghost_Ref); + Error_Msg_N (Ghost_Policy_Error_Msg, Ghost_Ref); Error_Msg_NE ("\ghost entity & has policy `Ignore`", Ghost_Ref, Ghost_Id); - - Error_Msg_Name_1 := AP; Error_Msg_N - ("\assertion expression has policy %", Ghost_Ref); + ("\assertion expression has policy `Check`", + Ghost_Ref); end if; end Check_Policies; @@ -352,53 +447,58 @@ package body Ghost is -- Start of processing for Is_OK_Pragma begin - if Nkind (Prag) = N_Pragma then - Prag_Id := Get_Pragma_Id (Prag); - Prag_Nam := Original_Aspect_Pragma_Name (Prag); + if Nkind (Prag) /= N_Pragma then + return False; + end if; - -- A pragma that applies to a Ghost construct or specifies an - -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3)) + Prag_Id := Get_Pragma_Id (Prag); + Prag_Nam := Original_Aspect_Pragma_Name (Prag); - if Is_Ghost_Pragma (Prag) then - return True; + -- A pragma may not be analyzed, so that its Ghost status is + -- not determined yet, but it is guaranteed to be Ghost when + -- referencing a Ghost entity. - -- A pragma may not be analyzed, so that its Ghost status is - -- not determined yet, but it is guaranteed to be Ghost when - -- referencing a Ghost entity. + if Prag_Nam + in Name_Annotate + | Name_Compile_Time_Error + | Name_Compile_Time_Warning + | Name_Unreferenced + then + return True; - elsif Prag_Nam in Name_Annotate - | Name_Compile_Time_Error - | Name_Compile_Time_Warning - | Name_Unreferenced - then - return True; + -- An assertion expression pragma is Ghost when it contains a + -- reference to a Ghost entity (SPARK RM 6.9(10)), except for + -- predicate pragmas (SPARK RM 6.9(11)). - -- An assertion expression pragma is Ghost when it contains a - -- reference to a Ghost entity (SPARK RM 6.9(10)), except for - -- predicate pragmas (SPARK RM 6.9(11)). + elsif Is_Valid_Assertion_Kind (Prag_Nam) + and then Assertion_Expression_Pragma (Prag_Id) + and then Prag_Id /= Pragma_Predicate + then + -- Ensure that the assertion policy and the Ghost policy are + -- compatible (SPARK RM 6.9(20)). - elsif Assertion_Expression_Pragma (Prag_Id) - and then Prag_Id /= Pragma_Predicate - then - -- Ensure that the assertion policy and the Ghost policy are - -- compatible (SPARK RM 6.9(20)). + Check_Policies; + return True; - Check_Policies (Prag_Nam); - return True; + -- A pragma that applies to a Ghost construct or specifies an + -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3)) - -- Several pragmas that may apply to a non-Ghost entity are - -- treated as Ghost when they contain a reference to a Ghost - -- entity (SPARK RM 6.9(11)). + elsif Is_Ghost_Pragma (Prag) then + return True; - elsif Prag_Nam in Name_Global - | Name_Depends - | Name_Initializes - | Name_Refined_Global - | Name_Refined_Depends - | Name_Refined_State - then - return True; - end if; + -- Several pragmas that may apply to a non-Ghost entity are + -- treated as Ghost when they contain a reference to a Ghost + -- entity (SPARK RM 6.9(11)). + + elsif Prag_Nam + in Name_Global + | Name_Depends + | Name_Initializes + | Name_Refined_Global + | Name_Refined_Depends + | Name_Refined_State + then + return True; end if; return False; @@ -408,18 +508,190 @@ package body Ghost is -- Is_OK_Statement -- --------------------- - function Is_OK_Statement (Stmt : Node_Id) return Boolean is + function Is_OK_Statement + (Stmt : Node_Id; Id : Entity_Id; Call_Arg : Node_Id) return Boolean + is + procedure Check_Assignment_Policies (Assignee : Entity_Id); + -- Check that: + -- * An ignored entity is not used to modify a checked ghost + -- entity in an assignment. + -- * A checked ghost assignment is not used in an ignored ghost + -- region. + -- * The level of the ghost region depends on the level of the + -- ghost assignment. + + procedure Check_Procedure_Call_Policies (Callee : Entity_Id); + -- Check that + -- * the a checked call argument is not modified by an ignored + -- procedure call. + -- * the level of the modified call argument depends on the level + -- of the call. + + function Is_Modified_By_Call + (Call : Node_Id; Call_Arg : Node_Id; Callee : Entity_Id) + return Boolean; + -- Check that Call_Arg was used in the call and that the formal + -- for that argument was either out or in-out. + + ------------------------------- + -- Check_Assignment_Policies -- + ------------------------------- + + procedure Check_Assignment_Policies (Assignee : Entity_Id) is + A_Policy : constant Name_Id := + Ghost_Policy_In_Effect (Assignee); + A_Level : constant Entity_Id := + Ghost_Assertion_Level (Assignee); + Id_Policy : constant Name_Id := Ghost_Policy_In_Effect (Id); + Region_Policy : constant Ghost_Mode_Type := + Ghost_Config.Ghost_Mode; + Region_Level : constant Entity_Id := + Ghost_Config.Ghost_Mode_Assertion_Level; + begin + if A_Policy = Name_Check and then Id_Policy = Name_Ignore then + Error_Msg_Sloc := Sloc (Ghost_Ref); + + Error_Msg_N (Ghost_Policy_Error_Msg, Ghost_Ref); + Error_Msg_NE ("\& has ghost policy `Ignore`", Ghost_Ref, Id); + Error_Msg_NE + ("\& used # to modify an entity with `Check`", + Ghost_Ref, + Id); + end if; + + if A_Policy = Name_Check and then Region_Policy = Ignore then + Error_Msg_N (Ghost_Policy_Error_Msg, Stmt); + Error_Msg_NE ("\& has ghost policy `Check`", Stmt, Assignee); + Error_Msg_NE + ("\& is modified in a region with `Ignore`", + Stmt, + Assignee); + end if; + + if Present (Region_Level) + and then not Is_Assertion_Level_Dependent + (Region_Level, A_Level) + then + Error_Msg_Sloc := Sloc (Stmt); + + Error_Msg_N (Assertion_Level_Error_Msg, Stmt); + Error_Msg_Name_1 := Chars (A_Level); + Error_Msg_NE ("\& has assertion level %", Stmt, Assignee); + Error_Msg_Name_1 := Chars (Region_Level); + Error_Msg_NE + ("\& is modified within a region with %", Stmt, Id); + Error_Msg_Name_1 := Chars (Region_Level); + Error_Msg_NE + ("\assertion level of & should depend on %", + Stmt, + Assignee); + end if; + end Check_Assignment_Policies; + + ----------------------------------- + -- Check_Procedure_Call_Policies -- + ----------------------------------- + + procedure Check_Procedure_Call_Policies (Callee : Entity_Id) is + Id_Level : constant Entity_Id := Ghost_Assertion_Level (Id); + Id_Policy : constant Name_Id := Ghost_Policy_In_Effect (Id); + + Call_Level : Entity_Id; + Call_Policy : Name_Id; + begin + if No (Callee) then + return; + end if; + + -- Checks apply only if we are processing a call argument that + -- is modified by the call. + + if No (Call_Arg) + or else not Is_Modified_By_Call (Stmt, Call_Arg, Callee) + then + return; + end if; + + Call_Policy := Ghost_Policy_In_Effect (Callee); + Call_Level := Ghost_Assertion_Level (Callee); + + if Id_Policy = Name_Check + and then Call_Policy = Name_Ignore + then + Error_Msg_Sloc := Sloc (Ghost_Ref); + Error_Msg_N (Ghost_Policy_Error_Msg, Ghost_Ref); + Error_Msg_NE ("\& has ghost policy `Check`", Ghost_Ref, Id); + Error_Msg_NE + ("\& is modified # by a procedure with `Ignore`", + Ghost_Ref, + Id); + end if; + + if not Is_Assertion_Level_Dependent (Id_Level, Call_Level) then + Error_Msg_Sloc := Sloc (Ghost_Ref); + + Error_Msg_N (Assertion_Level_Error_Msg, Ghost_Ref); + Error_Msg_Name_1 := Chars (Id_Level); + Error_Msg_NE ("\& has assertion level %", Ghost_Ref, Id); + Error_Msg_Name_1 := Chars (Call_Level); + Error_Msg_NE + ("\& is modified # by a procedure with %", Ghost_Ref, Id); + Error_Msg_Name_1 := Chars (Call_Level); + Error_Msg_NE + ("\assertion level of & should depend on %", + Ghost_Ref, + Id); + end if; + end Check_Procedure_Call_Policies; + + ------------------------- + -- Is_Modified_By_Call -- + ------------------------- + + function Is_Modified_By_Call + (Call : Node_Id; Call_Arg : Node_Id; Callee : Entity_Id) + return Boolean + is + Form : Node_Id; + Act : Node_Id; + begin + Act := First_Actual (Call); + Form := First_Formal (Callee); + + while Present (Form) and then Present (Act) loop + if Act = Call_Arg then + return + Ekind (Form) in E_Out_Parameter | E_In_Out_Parameter; + end if; + + Next_Formal (Form); + Next_Actual (Act); + end loop; + + return False; + end Is_Modified_By_Call; + + -- Start of processing for Is_OK_Statement + begin -- An assignment statement is Ghost when the target is a Ghost -- entity. if Nkind (Stmt) = N_Assignment_Statement then - return Is_Ghost_Assignment (Stmt); + if Is_Ghost_Assignment (Stmt) then + Check_Assignment_Policies + (Get_Enclosing_Ghost_Entity (Name (Stmt))); + + return True; + end if; -- A procedure call is Ghost when it calls a Ghost procedure elsif Nkind (Stmt) = N_Procedure_Call_Statement then - return Is_Ghost_Procedure_Call (Stmt); + if Is_Ghost_Procedure_Call (Stmt) then + Check_Procedure_Call_Policies (Get_Subprogram_Entity (Stmt)); + return True; + end if; -- Special cases @@ -439,23 +711,18 @@ package body Ghost is -- Local variables - Par : Node_Id; + Par : Node_Id; + Prev : Node_Id; -- Start of processing for Is_OK_Ghost_Context begin - -- The context is Ghost when it appears within a Ghost package or - -- subprogram. - - if Ghost_Config.Ghost_Mode > None then - return True; - -- Routine Expand_Record_Extension creates a parent subtype without -- inserting it into the tree. There is no good way of recognizing -- this special case as there is no parent. Try to approximate the -- context. - elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then + if No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then return True; -- Otherwise climb the parent chain looking for a suitable Ghost @@ -463,15 +730,13 @@ package body Ghost is else Par := Context; + Prev := Empty; while Present (Par) loop - 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 + if Nkind (Par) = N_Generic_Association then return True; -- A reference to a Ghost entity can appear within an aspect @@ -531,7 +796,7 @@ package body Ghost is elsif Is_OK_Pragma (Par, Ghost_Id) then return True; - elsif Is_OK_Statement (Par) then + elsif Is_OK_Statement (Par, Ghost_Id, Prev) then return True; -- Prevent the search from going too far @@ -540,6 +805,7 @@ package body Ghost is exit; end if; + Prev := Par; Par := Parent (Par); end loop; @@ -565,27 +831,51 @@ package body Ghost is ------------------------ procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is - Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); - + Ghost_Region : constant Node_Id := Ghost_Config.Current_Region; + Region_Policy : constant Ghost_Mode_Type := Ghost_Config.Ghost_Mode; begin + -- Ghost entities can be referenced inside a renaming declaration if + -- used within a renaming declaration. + + if No (Ghost_Region) + or else Nkind (Ghost_Region) + in N_Object_Renaming_Declaration + | N_Subprogram_Renaming_Declaration + then + return; + end if; + -- The Ghost policy in effect a the point of declaration and at the -- point of use must match (SPARK RM 6.9(15)). if Is_Checked_Ghost_Entity (Id) - and then Policy = Name_Ignore + and then Region_Policy = Ignore and then Known_To_Be_Assigned (Ref) then - Error_Msg_Sloc := Sloc (Ref); - - Error_Msg_N ("incompatible ghost policies in effect", Ref); + Error_Msg_N (Ghost_Policy_Error_Msg, Ref); Error_Msg_NE ("\& declared with ghost policy `Check`", Ref, Id); + Error_Msg_Sloc := Sloc (Ref); Error_Msg_NE ("\& used # with ghost policy `Ignore`", Ref, Id); + end if; - elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then - Error_Msg_Sloc := Sloc (Ref); + if No (Ghost_Region) + or else (Nkind (Ghost_Region) = N_Pragma + and then Get_Pragma_Id (Ghost_Region) + in Pragma_Global + | Pragma_Depends + | Pragma_Refined_Global + | Pragma_Refined_Depends + | Pragma_Initializes + | Pragma_Refined_State) + then + return; + end if; - Error_Msg_N ("incompatible ghost policies in effect", Ref); + if Is_Ignored_Ghost_Entity (Id) and then Region_Policy = Check + then + Error_Msg_N (Ghost_Policy_Error_Msg, Ref); Error_Msg_NE ("\& declared with ghost policy `Ignore`", Ref, Id); + Error_Msg_Sloc := Sloc (Ref); Error_Msg_NE ("\& used # with ghost policy `Check`", Ref, Id); end if; end Check_Ghost_Policy; @@ -643,19 +933,10 @@ package body Ghost is return; end if; - -- 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 - if Present (Ghost_Id) then - Check_Ghost_Policy (Ghost_Id, Ghost_Ref); - end if; - - -- Otherwise the Ghost entity appears in a non-Ghost context and affects + -- If the Ghost entity appears in a non-Ghost context and affects -- its behavior or value (SPARK RM 6.9(10,11)). - else + if not Is_OK_Ghost_Context (Ghost_Ref) then Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref); -- When the Ghost entity appears in a pragma Predicate, explain the @@ -672,6 +953,14 @@ package body Ghost is & "or use a type invariant on a private type", Ghost_Ref); end if; end if; + + -- 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 Present (Ghost_Id) then + Check_Ghost_Policy (Ghost_Id, Ghost_Ref); + end if; end Check_Ghost_Context; ------------------------------------------------ @@ -732,6 +1021,80 @@ package body Ghost is end if; end Check_Ghost_Context_In_Generic_Association; + ----------------------------------- + -- Check_Valid_Ghost_Declaration -- + ----------------------------------- + + procedure Check_Valid_Ghost_Declaration (N : Node_Id) is + procedure Check_Valid_Assertion_Level (Id : Entity_Id; Ref : Node_Id); + -- Check that the the assertion level of the declared entity is + -- compatible with assertion level of the ghost region. + + procedure Check_Valid_Ghost_Policy (Id : Entity_Id; Ref : Node_Id); + -- Check that the declared identifier does not have a Checked assertion + -- policy while being declared inside an ignored ghost region. + + --------------------------------- + -- Check_Valid_Assertion_Level -- + --------------------------------- + + procedure Check_Valid_Assertion_Level (Id : Entity_Id; Ref : Node_Id) is + Id_Level : constant Entity_Id := Ghost_Assertion_Level (Id); + Region_Level : constant Entity_Id := + Ghost_Config.Ghost_Mode_Assertion_Level; + begin + -- This check is not applied for generic isntantiations + + if Is_Generic_Instance (Id) then + return; + end if; + + if not Is_Assertion_Level_Dependent (Id_Level, Region_Level) then + Error_Msg_Sloc := Sloc (Ref); + + Error_Msg_N (Assertion_Level_Error_Msg, Ref); + Error_Msg_Name_1 := Chars (Id_Level); + Error_Msg_NE ("\& has assertion level %", Ref, Id); + Error_Msg_Name_1 := Chars (Region_Level); + Error_Msg_NE ("\& is declared within a region with %", Ref, Id); + Error_Msg_Name_1 := Chars (Region_Level); + Error_Msg_NE ("\assertion level of & should depend on %", Ref, Id); + end if; + end Check_Valid_Assertion_Level; + + ------------------------------ + -- Check_Valid_Ghost_Policy -- + ------------------------------ + + procedure Check_Valid_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is + Policy : constant Name_Id := Ghost_Policy_In_Effect (Id); + begin + if Ghost_Config.Ghost_Mode = Ignore and then Policy = Name_Check + then + Error_Msg_Sloc := Sloc (Ref); + + Error_Msg_N (Ghost_Policy_Error_Msg, Ref); + Error_Msg_NE ("\& has ghost policy `Check`", Ref, Id); + Error_Msg_NE + ("\& is declared # within ghost policy `Ignore`", Ref, Id); + end if; + end Check_Valid_Ghost_Policy; + + -- Local variables + + Id : constant Entity_Id := Defining_Entity (N); + + -- Start of processing for Check_Valid_Ghost_Declaration + begin + if not Is_Ghost_Entity (Id) or else Ghost_Config.Ghost_Mode = None + then + return; + end if; + + Check_Valid_Ghost_Policy (Id, N); + Check_Valid_Assertion_Level (Id, N); + end Check_Valid_Ghost_Declaration; + --------------------------------------------- -- Check_Ghost_Formal_Procedure_Or_Package -- --------------------------------------------- @@ -808,129 +1171,127 @@ package body Ghost is Over_Subp : Entity_Id; begin - if Present (Subp) and then Present (Overridden_Subp) then - Over_Subp := Ultimate_Alias (Overridden_Subp); - Deriv_Typ := Find_Dispatching_Type (Subp); - - -- A Ghost primitive of a non-Ghost type extension cannot override an - -- inherited non-Ghost primitive (SPARK RM 6.9(8)). - - if Is_Ghost_Entity (Subp) - and then Present (Deriv_Typ) - and then not Is_Ghost_Entity (Deriv_Typ) - and then not Is_Ghost_Entity (Over_Subp) - and then not Is_Abstract_Subprogram (Over_Subp) - then - Error_Msg_N ("incompatible overriding in effect", Subp); + if No (Subp) or else No (Overridden_Subp) then + return; + end if; - Error_Msg_Sloc := Sloc (Over_Subp); - Error_Msg_N ("\& declared # as non-ghost subprogram", Subp); + Over_Subp := Ultimate_Alias (Overridden_Subp); + Deriv_Typ := Find_Dispatching_Type (Subp); - Error_Msg_Sloc := Sloc (Subp); - Error_Msg_N ("\overridden # with ghost subprogram", Subp); - end if; + -- A Ghost primitive of a non-Ghost type extension cannot override an + -- inherited non-Ghost primitive (SPARK RM 6.9(8)). - -- A non-Ghost primitive of a type extension cannot override an - -- inherited Ghost primitive (SPARK RM 6.9(8)). + if Is_Ghost_Entity (Subp) + and then Present (Deriv_Typ) + and then not Is_Ghost_Entity (Deriv_Typ) + and then not Is_Ghost_Entity (Over_Subp) + and then not Is_Abstract_Subprogram (Over_Subp) + then + Error_Msg_N ("incompatible overriding in effect", Subp); - if Is_Ghost_Entity (Over_Subp) - and then not Is_Ghost_Entity (Subp) - and then not Is_Abstract_Subprogram (Subp) - then - Error_Msg_N ("incompatible overriding in effect", Subp); + Error_Msg_Sloc := Sloc (Over_Subp); + Error_Msg_N ("\& declared # as non-ghost subprogram", Subp); - Error_Msg_Sloc := Sloc (Over_Subp); - Error_Msg_N ("\& declared # as ghost subprogram", Subp); + Error_Msg_Sloc := Sloc (Subp); + Error_Msg_N ("\overridden # with ghost subprogram", Subp); + end if; - Error_Msg_Sloc := Sloc (Subp); - Error_Msg_N ("\overridden # with non-ghost subprogram", Subp); - end if; + -- A non-Ghost primitive of a type extension cannot override an + -- inherited Ghost primitive (SPARK RM 6.9(8)). - if Present (Deriv_Typ) - and then not Is_Ignored_Ghost_Entity (Deriv_Typ) - then - -- When a tagged type is either non-Ghost or checked Ghost and - -- one of its primitives overrides an inherited operation, the - -- overridden operation of the ancestor type must be ignored Ghost - -- if the primitive is ignored Ghost (SPARK RM 6.9(19)). + if Is_Ghost_Entity (Over_Subp) + and then not Is_Ghost_Entity (Subp) + and then not Is_Abstract_Subprogram (Subp) + then + Error_Msg_N ("incompatible overriding in effect", Subp); - if Is_Ignored_Ghost_Entity (Subp) then + Error_Msg_Sloc := Sloc (Over_Subp); + Error_Msg_N ("\& declared # as ghost subprogram", Subp); - -- Both the parent subprogram and overriding subprogram are - -- ignored Ghost. + Error_Msg_Sloc := Sloc (Subp); + Error_Msg_N ("\overridden # with non-ghost subprogram", Subp); + end if; - if Is_Ignored_Ghost_Entity (Over_Subp) then - null; + if Present (Deriv_Typ) + and then not Is_Ignored_Ghost_Entity (Deriv_Typ) + then + -- When a tagged type is either non-Ghost or checked Ghost and + -- one of its primitives overrides an inherited operation, the + -- overridden operation of the ancestor type must be ignored Ghost + -- if the primitive is ignored Ghost (SPARK RM 6.9(19)). - -- The parent subprogram carries policy Check + if Is_Ignored_Ghost_Entity (Subp) then - elsif Is_Checked_Ghost_Entity (Over_Subp) then - Error_Msg_N - ("incompatible ghost policies in effect", Subp); + -- Both the parent subprogram and overriding subprogram are + -- ignored Ghost. - Error_Msg_Sloc := Sloc (Over_Subp); - Error_Msg_N - ("\& declared # with ghost policy `Check`", Subp); + if Is_Ignored_Ghost_Entity (Over_Subp) then + null; - Error_Msg_Sloc := Sloc (Subp); - Error_Msg_N - ("\overridden # with ghost policy `Ignore`", Subp); + -- The parent subprogram carries policy Check - -- The parent subprogram is non-Ghost + elsif Is_Checked_Ghost_Entity (Over_Subp) then + Error_Msg_N (Ghost_Policy_Error_Msg, Subp); - else - Error_Msg_N - ("incompatible ghost policies in effect", Subp); + Error_Msg_Sloc := Sloc (Over_Subp); + Error_Msg_N + ("\& declared # with ghost policy `Check`", Subp); - Error_Msg_Sloc := Sloc (Over_Subp); - Error_Msg_N ("\& declared # as non-ghost subprogram", Subp); + Error_Msg_Sloc := Sloc (Subp); + Error_Msg_N + ("\overridden # with ghost policy `Ignore`", Subp); - Error_Msg_Sloc := Sloc (Subp); - Error_Msg_N - ("\overridden # with ghost policy `Ignore`", Subp); - end if; + -- The parent subprogram is non-Ghost - -- When a tagged type is either non-Ghost or checked Ghost and - -- one of its primitives overrides an inherited operation, the - -- the primitive of the tagged type must be ignored Ghost if the - -- overridden operation is ignored Ghost (SPARK RM 6.9(19)). + else + Error_Msg_N (Ghost_Policy_Error_Msg, Subp); - elsif Is_Ignored_Ghost_Entity (Over_Subp) then + Error_Msg_Sloc := Sloc (Over_Subp); + Error_Msg_N ("\& declared # as non-ghost subprogram", Subp); - -- Both the parent subprogram and the overriding subprogram are - -- ignored Ghost. + Error_Msg_Sloc := Sloc (Subp); + Error_Msg_N + ("\overridden # with ghost policy `Ignore`", Subp); + end if; - if Is_Ignored_Ghost_Entity (Subp) then - null; + -- When a tagged type is either non-Ghost or checked Ghost and + -- one of its primitives overrides an inherited operation, the + -- the primitive of the tagged type must be ignored Ghost if the + -- overridden operation is ignored Ghost (SPARK RM 6.9(19)). - -- The overriding subprogram carries policy Check + elsif Is_Ignored_Ghost_Entity (Over_Subp) then - elsif Is_Checked_Ghost_Entity (Subp) then - Error_Msg_N - ("incompatible ghost policies in effect", Subp); + -- Both the parent subprogram and the overriding subprogram are + -- ignored Ghost. - Error_Msg_Sloc := Sloc (Over_Subp); - Error_Msg_N - ("\& declared # with ghost policy `Ignore`", Subp); + if Is_Ignored_Ghost_Entity (Subp) then + null; - Error_Msg_Sloc := Sloc (Subp); - Error_Msg_N - ("\overridden # with Ghost policy `Check`", Subp); + -- The overriding subprogram carries policy Check - -- The overriding subprogram is non-Ghost + elsif Is_Checked_Ghost_Entity (Subp) then + Error_Msg_N (Ghost_Policy_Error_Msg, Subp); - else - Error_Msg_N - ("incompatible ghost policies in effect", Subp); + Error_Msg_Sloc := Sloc (Over_Subp); + Error_Msg_N + ("\& declared # with ghost policy `Ignore`", Subp); - Error_Msg_Sloc := Sloc (Over_Subp); - Error_Msg_N - ("\& declared # with ghost policy `Ignore`", Subp); + Error_Msg_Sloc := Sloc (Subp); + Error_Msg_N + ("\overridden # with Ghost policy `Check`", Subp); - Error_Msg_Sloc := Sloc (Subp); - Error_Msg_N - ("\overridden # with non-ghost subprogram", Subp); - end if; + -- The overriding subprogram is non-Ghost + + else + Error_Msg_N (Ghost_Policy_Error_Msg, Subp); + + Error_Msg_Sloc := Sloc (Over_Subp); + Error_Msg_N + ("\& declared # with ghost policy `Ignore`", Subp); + + Error_Msg_Sloc := Sloc (Subp); + Error_Msg_N + ("\overridden # with non-ghost subprogram", Subp); end if; end if; end if; @@ -941,41 +1302,48 @@ package body Ghost is --------------------------- procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is + Prim_Level : Entity_Id; + Typ_Level : Entity_Id; begin - -- The Ghost policy in effect at the point of declaration of a primitive - -- operation and a tagged type must match (SPARK RM 6.9(18)). + if not Is_Tagged_Type (Typ) then + return; + end if; - if Is_Tagged_Type (Typ) then - if Is_Checked_Ghost_Entity (Prim) - and then Is_Ignored_Ghost_Entity (Typ) - then - Error_Msg_N ("incompatible ghost policies in effect", Prim); + -- The Ghost policy in effect at the point of declaration of a primitive + -- operation and a tagged type must match (SPARK RM 6.9(20)). - Error_Msg_Sloc := Sloc (Typ); - Error_Msg_NE - ("\tagged type & declared # with ghost policy `Ignore`", - Prim, Typ); + if Is_Checked_Ghost_Entity (Prim) + and then Is_Ignored_Ghost_Entity (Typ) + then + Error_Msg_N (Ghost_Policy_Error_Msg, Prim); - Error_Msg_Sloc := Sloc (Prim); - Error_Msg_N - ("\primitive subprogram & declared # with ghost policy `Check`", - Prim); + Error_Msg_Sloc := Sloc (Typ); + Error_Msg_NE + ("\tagged type & declared # with ghost policy `Ignore`", + Prim, Typ); - elsif Is_Ignored_Ghost_Entity (Prim) - and then Is_Checked_Ghost_Entity (Typ) - then - Error_Msg_N ("incompatible ghost policies in effect", Prim); + Error_Msg_Sloc := Sloc (Prim); + Error_Msg_N + ("\primitive subprogram & declared # with ghost policy `Check`", + Prim); + end if; - Error_Msg_Sloc := Sloc (Typ); - Error_Msg_NE - ("\tagged type & declared # with ghost policy `Check`", - Prim, Typ); + Prim_Level := Ghost_Assertion_Level (Prim); + Typ_Level := Ghost_Assertion_Level (Typ); + + if not Is_Assertion_Level_Dependent (Prim_Level, Typ_Level) then + Error_Msg_N (Assertion_Level_Error_Msg, Prim); + Error_Msg_Name_1 := Chars (Typ_Level); + Error_Msg_Sloc := Sloc (Typ); + Error_Msg_NE ("\tagged type & declared # with %", Prim, Typ); + Error_Msg_Name_1 := Chars (Prim_Level); + Error_Msg_Sloc := Sloc (Prim); + Error_Msg_NE + ("\primitive subprogram & declared # with %", Prim, Prim); + Error_Msg_Name_1 := Chars (Typ_Level); + Error_Msg_NE + ("\assertion level of & should depend on %", Prim, Prim); - Error_Msg_Sloc := Sloc (Prim); - Error_Msg_N - ("\primitive subprogram & declared # with ghost policy `Ignore`", - Prim); - end if; end if; end Check_Ghost_Primitive; @@ -989,48 +1357,56 @@ package body Ghost is Constit : Node_Id; Constit_Id : Entity_Id) is + State_Level : Entity_Id; + Constit_Level : Entity_Id; begin - if Is_Ghost_Entity (State_Id) then - if Is_Ghost_Entity (Constit_Id) then + -- Only check ghost states - -- The Ghost policy in effect at the point of abstract state - -- declaration and constituent must match (SPARK RM 6.9(17)). + if not Is_Ghost_Entity (State_Id) then + return; + end if; - if Is_Checked_Ghost_Entity (State_Id) - and then Is_Ignored_Ghost_Entity (Constit_Id) - then - Error_Msg_Sloc := Sloc (Constit); - SPARK_Msg_N ("incompatible ghost policies in effect", State); - - SPARK_Msg_NE - ("\abstract state & declared with ghost policy `Check`", - State, State_Id); - SPARK_Msg_NE - ("\constituent & declared # with ghost policy `Ignore`", - State, Constit_Id); - - elsif Is_Ignored_Ghost_Entity (State_Id) - and then Is_Checked_Ghost_Entity (Constit_Id) - then - Error_Msg_Sloc := Sloc (Constit); - SPARK_Msg_N ("incompatible ghost policies in effect", State); - - SPARK_Msg_NE - ("\abstract state & declared with ghost policy `Ignore`", - State, State_Id); - SPARK_Msg_NE - ("\constituent & declared # with ghost policy `Check`", - State, Constit_Id); - end if; + -- A constituent of a Ghost abstract state must be a Ghost entity + -- (SPARK RM 7.2.2(12)). + + if not Is_Ghost_Entity (Constit_Id) then + SPARK_Msg_NE + ("constituent of ghost state & must be ghost", + Constit, State_Id); + end if; - -- A constituent of a Ghost abstract state must be a Ghost entity - -- (SPARK RM 7.2.2(12)). + -- The Ghost policy in effect at the point of an ignored abstract state + -- cannot be check (SPARK RM 6.9(19)). + + if Is_Ignored_Ghost_Entity (State_Id) + and then Is_Checked_Ghost_Entity (Constit_Id) + then + SPARK_Msg_N (Ghost_Policy_Error_Msg, State); + Error_Msg_Sloc := Sloc (State_Id); + SPARK_Msg_NE + ("\abstract state & declared # with ghost policy `Ignore`", + State, State_Id); + Error_Msg_Sloc := Sloc (Constit_Id); + SPARK_Msg_NE + ("\constituent & declared # with ghost policy `Check`", + State, Constit_Id); + end if; + + State_Level := Ghost_Assertion_Level (State_Id); + Constit_Level := Ghost_Assertion_Level (Constit_Id); + + if not Is_Assertion_Level_Dependent (Constit_Level, State_Level) then + SPARK_Msg_N (Assertion_Level_Error_Msg, State); + Error_Msg_Name_1 := Chars (State_Level); + Error_Msg_Sloc := Sloc (State_Id); + SPARK_Msg_NE ("\abstract state & declared # with %", State, State_Id); + Error_Msg_Name_1 := Chars (Constit_Level); + Error_Msg_Sloc := Sloc (Constit_Id); + SPARK_Msg_NE ("\constituent & declared # with %", State, Constit_Id); + Error_Msg_Name_1 := Chars (State_Level); + SPARK_Msg_NE + ("\assertion level of & should depend on %", State, Constit_Id); - else - SPARK_Msg_NE - ("constituent of ghost state & must be ghost", - Constit, State_Id); - end if; end if; end Check_Ghost_Refinement; @@ -1074,6 +1450,110 @@ package body Ghost is end if; end Check_Ghost_Type; + ---------------------- + -- Get_Ghost_Aspect -- + ---------------------- + + function Get_Ghost_Aspect (N : Node_Id) return Node_Id is + Asp : Node_Id; + begin + if not Permits_Aspect_Specifications (N) then + return Empty; + end if; + + Asp := First (Aspect_Specifications (N)); + while Present (Asp) loop + if Chars (Identifier (Asp)) = Name_Ghost then + return Asp; + end if; + + Next (Asp); + end loop; + + return Empty; + end Get_Ghost_Aspect; + + ---------------------- + -- Get_Ghost_Pragma -- + ---------------------- + + function Get_Ghost_Pragma (N : Node_Id) return Node_Id is + Decl : Node_Id := Empty; + begin + -- When the context is a [generic] package declaration, pragma Ghost + -- resides in the visible declarations. + + if Nkind (N) in N_Generic_Package_Declaration | N_Package_Declaration + then + Decl := First (Visible_Declarations (Specification (N))); + + -- When the context is a package or a subprogram body, pragma Ghost + -- resides in the declarative part. + + elsif Nkind (N) in N_Package_Body | N_Subprogram_Body then + Decl := First (Declarations (N)); + + -- Otherwise pragma Ghost appears in the declarations following N + + elsif Is_List_Member (N) then + Decl := Next (N); + end if; + + while Present (Decl) loop + if Nkind (Decl) = N_Pragma + and then Pragma_Name (Decl) = Name_Ghost + then + return Decl; + + -- A source construct ends the region where pragma Ghost may appear, + -- stop the traversal. Check the original node as source constructs + -- may be rewritten into something else by expansion. + + elsif Comes_From_Source (Original_Node (Decl)) then + exit; + end if; + + Next (Decl); + end loop; + + return Empty; + end Get_Ghost_Pragma; + + ------------------------------- + -- Get_Ghost_Assertion_Level -- + ------------------------------- + + function Get_Ghost_Assertion_Level (N : Node_Id) return Entity_Id is + Ghost_Asp : constant Node_Id := Get_Ghost_Aspect (N); + Ghost_Prag : Node_Id; + + begin + if Present (Ghost_Asp) then + return Assertion_Level_From_Arg (Expression (Ghost_Asp)); + end if; + + Ghost_Prag := Get_Ghost_Pragma (N); + if Present (Ghost_Prag) then + return + Assertion_Level_From_Arg + (First (Pragma_Argument_Associations (Ghost_Prag))); + end if; + + return Empty; + end Get_Ghost_Assertion_Level; + + ---------------------------- + -- Ghost_Policy_In_Effect -- + ---------------------------- + + function Ghost_Policy_In_Effect (Id : Entity_Id) return Name_Id is + Level : constant Entity_Id := Ghost_Assertion_Level (Id); + Level_Nam : constant Name_Id := + (if No (Level) then No_Name else Chars (Level)); + begin + return Policy_In_Effect (Name_Ghost, Level_Nam); + end Ghost_Policy_In_Effect; + -------------------------------- -- Implements_Ghost_Interface -- -------------------------------- @@ -1112,20 +1592,15 @@ package body Ghost is Set_Ignored_Ghost_Recording_Proc (Record_Ignored_Ghost_Node'Access); end Initialize; - ------------------------ - -- Install_Ghost_Mode -- - ------------------------ - - procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is - begin - Install_Ghost_Region (Mode, Empty); - end Install_Ghost_Mode; - -------------------------- -- Install_Ghost_Region -- -------------------------- - procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is + procedure Install_Ghost_Region + (Mode : Ghost_Mode_Type; + N : Node_Id; + Level : Entity_Id) + is begin -- The context is already within an ignored Ghost region. Maintain the -- start of the outermost ignored Ghost region. @@ -1145,14 +1620,34 @@ package body Ghost is Ghost_Config.Ignored_Ghost_Region := Empty; end if; + Ghost_Config.Current_Region := N; Ghost_Config.Ghost_Mode := Mode; + Ghost_Config.Ghost_Mode_Assertion_Level := Level; end Install_Ghost_Region; - procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id) is + procedure Install_Ghost_Region + (Mode : Name_Id; + N : Node_Id; + Level : Entity_Id) is begin - Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N); + Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N, Level); end Install_Ghost_Region; + ------------------------- + -- Is_Compatible_Level -- + ------------------------- + + function Is_Assertion_Level_Dependent + (Self : Entity_Id; Other : Entity_Id) return Boolean + is + begin + return + Self = Standard_Level_Default + or else Other = Standard_Level_Default + or else Is_Same_Or_Depends_On_Level (Self, Other) + or else Is_Same_Or_Depends_On_Level (Self, Standard_Level_Static); + end Is_Assertion_Level_Dependent; + ------------------------- -- Is_Ghost_Assignment -- ------------------------- @@ -1279,37 +1774,38 @@ package body Ghost is ----------------------- function Enables_Ghostness (Arg : Node_Id) return Boolean is - Expr : Node_Id; + Expr : constant Node_Id := Get_Pragma_Arg (Arg); begin - Expr := Arg; + -- Aspect Ghost without an expression enables ghostness - if Nkind (Expr) = N_Pragma_Argument_Association then - Expr := Get_Pragma_Arg (Expr); + if No (Expr) then + return True; end if; - -- Determine whether the expression of the aspect or pragma is static - -- and denotes True. + -- Check if the expression matches a static boolean expression first - if Present (Expr) then - Preanalyze_And_Resolve (Expr); - - return - Is_OK_Static_Expression (Expr) - and then Is_True (Expr_Value (Expr)); + Preanalyze_And_Resolve_Without_Errors (Expr); + if Is_OK_Static_Expression (Expr) then + return Is_True (Expr_Value (Expr)); + end if; - -- Otherwise Ghost defaults to True + -- Alternatively the argument could be an Assertion_Level - else + if Nkind (Expr) = N_Identifier + and then Present (Get_Assertion_Level (Chars (Expr))) + then return True; end if; + + return False; end Enables_Ghostness; -- Local variables Id : constant Entity_Id := Defining_Entity (N); Asp : Node_Id; - Decl : Node_Id; + Prag : Node_Id; Prev_Id : Entity_Id; -- Start of processing for Is_Subject_To_Ghost @@ -1342,56 +1838,21 @@ package body Ghost is -- Examine the aspect specifications (if any) looking for aspect Ghost - if Permits_Aspect_Specifications (N) then - Asp := First (Aspect_Specifications (N)); - while Present (Asp) loop - if Chars (Identifier (Asp)) = Name_Ghost then - return Enables_Ghostness (Expression (Asp)); - end if; + Asp := Get_Ghost_Aspect (N); - Next (Asp); - end loop; + if Present (Asp) then + return Enables_Ghostness (Expression (Asp)); end if; - Decl := Empty; - - -- When the context is a [generic] package declaration, pragma Ghost - -- resides in the visible declarations. - - if Nkind (N) in N_Generic_Package_Declaration | N_Package_Declaration - then - Decl := First (Visible_Declarations (Specification (N))); - - -- When the context is a package or a subprogram body, pragma Ghost - -- resides in the declarative part. - - elsif Nkind (N) in N_Package_Body | N_Subprogram_Body then - Decl := First (Declarations (N)); + -- Examine the following pragmas for an applicable Ghost pragma - -- Otherwise pragma Ghost appears in the declarations following N + Prag := Get_Ghost_Pragma (N); - elsif Is_List_Member (N) then - Decl := Next (N); + if Present (Prag) then + return + Enables_Ghostness (First (Pragma_Argument_Associations (Prag))); end if; - while Present (Decl) loop - if Nkind (Decl) = N_Pragma - and then Pragma_Name (Decl) = Name_Ghost - then - return - Enables_Ghostness (First (Pragma_Argument_Associations (Decl))); - - -- A source construct ends the region where pragma Ghost may appear, - -- stop the traversal. Check the original node as source constructs - -- may be rewritten into something else by expansion. - - elsif Comes_From_Source (Original_Node (Decl)) then - exit; - end if; - - Next (Decl); - end loop; - return False; end Is_Subject_To_Ghost; @@ -1416,72 +1877,54 @@ package body Ghost is -- where P is a package, X is a record, and Comp is an array, we need -- to check the ghost flags of X. - Orig_Lhs : constant Node_Id := Name (N); + Orig_Lhs : constant Node_Id := Name (N); + Id : Entity_Id; + Lhs : Node_Id; + begin -- Ghost assignments are irrelevant when the expander is inactive, and -- processing them in that mode can lead to spurious errors. - if Expander_Active then - -- Cases where full analysis is needed, involving array indexing - -- which would otherwise be missing array-bounds checks: - - if not Analyzed (Orig_Lhs) - and then - ((Nkind (Orig_Lhs) = N_Indexed_Component - and then Nkind (Prefix (Orig_Lhs)) = N_Selected_Component - and then Nkind (Prefix (Prefix (Orig_Lhs))) = - N_Indexed_Component) - or else - (Nkind (Orig_Lhs) = N_Selected_Component - and then Nkind (Prefix (Orig_Lhs)) = N_Indexed_Component - and then Nkind (Prefix (Prefix (Orig_Lhs))) = - N_Selected_Component - and then Nkind (Parent (N)) /= N_Loop_Statement)) - then - Analyze (Orig_Lhs); - end if; - - -- Make sure Lhs is at least preanalyzed, so we can tell whether - -- it denotes a ghost variable. In some cases we need to do a full - -- analysis, or else the back end gets confused. Note that in the - -- preanalysis case, we are preanalyzing a copy of the left-hand - -- side name, temporarily attached to the tree. - - declare - Lhs : constant Node_Id := - (if Analyzed (Orig_Lhs) then Orig_Lhs - else New_Copy_Tree (Orig_Lhs)); - begin - if not Analyzed (Lhs) then - Set_Name (N, Lhs); - Set_Parent (Lhs, N); - Preanalyze_Without_Errors (Lhs); - Set_Name (N, Orig_Lhs); - end if; - - declare - Id : constant Entity_Id := Get_Enclosing_Ghost_Entity (Lhs); - begin - if Present (Id) then - -- Left-hand side denotes a Checked ghost entity, so install - -- the region. + if not Expander_Active then + return; + end if; - if Is_Checked_Ghost_Entity (Id) then - Install_Ghost_Region (Check, N); + -- Cases where full analysis is needed, involving array indexing + -- which would otherwise be missing array-bounds checks: - -- Left-hand side denotes an Ignored ghost entity, so - -- install the region, and mark the assignment statement as - -- an ignored ghost assignment, so it will be removed later. + if not Analyzed (Orig_Lhs) + and then + ((Nkind (Orig_Lhs) = N_Indexed_Component + and then Nkind (Prefix (Orig_Lhs)) = N_Selected_Component + and then Nkind (Prefix (Prefix (Orig_Lhs))) = + N_Indexed_Component) + or else + (Nkind (Orig_Lhs) = N_Selected_Component + and then Nkind (Prefix (Orig_Lhs)) = N_Indexed_Component + and then Nkind (Prefix (Prefix (Orig_Lhs))) = + N_Selected_Component + and then Nkind (Parent (N)) /= N_Loop_Statement)) + then + Analyze (Orig_Lhs); + end if; - elsif Is_Ignored_Ghost_Entity (Id) then - Install_Ghost_Region (Ignore, N); - Set_Is_Ignored_Ghost_Node (N); - Record_Ignored_Ghost_Node (N); - end if; - end if; - end; - end; + -- Make sure Lhs is at least preanalyzed, so we can tell whether + -- it denotes a ghost variable. In some cases we need to do a full + -- analysis, or else the back end gets confused. Note that in the + -- preanalysis case, we are preanalyzing a copy of the left-hand + -- side name, temporarily attached to the tree. + + Lhs := + (if Analyzed (Orig_Lhs) then Orig_Lhs else New_Copy_Tree (Orig_Lhs)); + if not Analyzed (Lhs) then + Set_Name (N, Lhs); + Set_Parent (Lhs, N); + Preanalyze_Without_Errors (Lhs); + Set_Name (N, Orig_Lhs); end if; + + Id := Get_Enclosing_Ghost_Entity (Lhs); + Mark_And_Set_Ghost_Region (N, Id); end Mark_And_Set_Ghost_Assignment; ----------------------------- @@ -1493,22 +1936,31 @@ package body Ghost is Spec_Id : Entity_Id) is Body_Id : constant Entity_Id := Defining_Entity (N); + Level : Entity_Id := Empty; Policy : Name_Id := No_Name; begin -- A body becomes Ghost when it is subject to aspect or pragma Ghost if Is_Subject_To_Ghost (N) then - Policy := Policy_In_Effect (Name_Ghost); + if Present (Spec_Id) then + Policy := Ghost_Policy_In_Effect (Spec_Id); + Level := Ghost_Assertion_Level (Spec_Id); + else + Policy := Ghost_Policy_In_Effect (Body_Id); + Level := Ghost_Assertion_Level (Body_Id); + end if; -- A body declared within a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). elsif Ghost_Config.Ghost_Mode = Check then Policy := Name_Check; + Level := Ghost_Config.Ghost_Mode_Assertion_Level; elsif Ghost_Config.Ghost_Mode = Ignore then Policy := Name_Ignore; + Level := Ghost_Config.Ghost_Mode_Assertion_Level; -- Inherit the "ghostness" of the previous declaration when the body -- acts as a completion. @@ -1520,6 +1972,8 @@ package body Ghost is elsif Is_Ignored_Ghost_Entity (Spec_Id) then Policy := Name_Ignore; end if; + + Level := Ghost_Assertion_Level (Spec_Id); end if; -- The Ghost policy in effect at the point of declaration and at the @@ -1529,13 +1983,17 @@ package body Ghost is (Prev_Id => Spec_Id, Compl_Id => Body_Id); + if Present (Level) then + Set_Ghost_Assertion_Level (Body_Id, Level); + end if; + -- Mark the body as its formals as Ghost - Mark_Ghost_Declaration_Or_Body (N, Policy); + Mark_Ghost_Declaration_Or_Body (N, Policy, Level); -- Install the appropriate Ghost region - Install_Ghost_Region (Policy, N); + Install_Ghost_Region (Policy, N, Level); end Mark_And_Set_Ghost_Body; ----------------------------------- @@ -1547,6 +2005,7 @@ package body Ghost is Prev_Id : Entity_Id) is Compl_Id : constant Entity_Id := Defining_Entity (N); + Level : Entity_Id := Empty; Policy : Name_Id := No_Name; begin @@ -1555,18 +2014,22 @@ package body Ghost is if Ghost_Config.Ghost_Mode = Check then Policy := Name_Check; + Level := Ghost_Config.Ghost_Mode_Assertion_Level; elsif Ghost_Config.Ghost_Mode = Ignore then Policy := Name_Ignore; + Level := Ghost_Config.Ghost_Mode_Assertion_Level; -- The completion becomes Ghost when its initial declaration is also -- Ghost. elsif Is_Checked_Ghost_Entity (Prev_Id) then Policy := Name_Check; + Level := Ghost_Assertion_Level (Prev_Id); elsif Is_Ignored_Ghost_Entity (Prev_Id) then Policy := Name_Ignore; + Level := Ghost_Assertion_Level (Prev_Id); end if; -- The Ghost policy in effect at the point of declaration and at the @@ -1578,11 +2041,11 @@ package body Ghost is -- Mark the completion as Ghost - Mark_Ghost_Declaration_Or_Body (N, Policy); + Mark_Ghost_Declaration_Or_Body (N, Policy, Level); -- Install the appropriate Ghost region - Install_Ghost_Region (Policy, N); + Install_Ghost_Region (Policy, N, Level); end Mark_And_Set_Ghost_Completion; ------------------------------------ @@ -1590,24 +2053,49 @@ package body Ghost is ------------------------------------ procedure Mark_And_Set_Ghost_Declaration (N : Node_Id) is + Level : Entity_Id := Empty; Par_Id : Entity_Id; Policy : Name_Id := No_Name; + Id : Entity_Id; begin -- A declaration becomes Ghost when it is subject to aspect or pragma -- Ghost. if Is_Subject_To_Ghost (N) then - Policy := Policy_In_Effect (Name_Ghost); + Id := Defining_Entity (N); + + if Is_Ghost_Entity (Id) then + if Is_Checked_Ghost_Entity (Id) then + Policy := Name_Check; + + elsif Is_Ignored_Ghost_Entity (Id) then + Policy := Name_Ignore; + end if; + + Level := Ghost_Assertion_Level (Id); + + else + -- We need to mark the declaration before the analysis so we + -- cannot rely on the Id already having the correct ghost markers. + -- Analyze if the node is associated with a ghost aspect here and + -- check for the applicable policy. + + Level := Get_Ghost_Assertion_Level (N); + Policy := + Policy_In_Effect (Name_Ghost, Assertion_Level_To_Name (Level)); + end if; -- A declaration elaborated in a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). elsif Ghost_Config.Ghost_Mode = Check then Policy := Name_Check; + Level := Ghost_Config.Ghost_Mode_Assertion_Level; elsif Ghost_Config.Ghost_Mode = Ignore then Policy := Name_Ignore; + Level := Ghost_Config.Ghost_Mode_Assertion_Level; -- A child package or subprogram declaration becomes Ghost when its -- parent is Ghost (SPARK RM 6.9(2)). @@ -1631,15 +2119,19 @@ package body Ghost is elsif Is_Ignored_Ghost_Entity (Par_Id) then Policy := Name_Ignore; end if; + + Level := Ghost_Assertion_Level (Par_Id); end if; -- Mark the declaration and its formals as Ghost - Mark_Ghost_Declaration_Or_Body (N, Policy); + Mark_Ghost_Declaration_Or_Body (N, Policy, Level); + + Check_Valid_Ghost_Declaration (N); -- Install the appropriate Ghost region - Install_Ghost_Region (Policy, N); + Install_Ghost_Region (Policy, N, Level); end Mark_And_Set_Ghost_Declaration; -------------------------------------- @@ -1687,22 +2179,25 @@ package body Ghost is -- Local variables + Level : Entity_Id := Empty; Policy : Name_Id := No_Name; begin -- An instantiation becomes Ghost when it is subject to pragma Ghost if Is_Subject_To_Ghost (N) then - Policy := Policy_In_Effect (Name_Ghost); + Policy := Ghost_Policy_In_Effect (Gen_Id); -- An instantiation declaration within a Ghost region is automatically -- Ghost (SPARK RM 6.9(2)). elsif Ghost_Config.Ghost_Mode = Check then Policy := Name_Check; + Level := Ghost_Config.Ghost_Mode_Assertion_Level; elsif Ghost_Config.Ghost_Mode = Ignore then Policy := Name_Ignore; + Level := Ghost_Config.Ghost_Mode_Assertion_Level; -- Inherit the "ghostness" of the generic unit, but the current Ghost -- policy is the relevant one for the instantiation. @@ -1710,20 +2205,22 @@ package body Ghost is elsif Is_Checked_Ghost_Entity (Gen_Id) or else Is_Ignored_Ghost_Entity (Gen_Id) then - Policy := Policy_In_Effect (Name_Ghost); + Policy := Ghost_Policy_In_Effect (Gen_Id); if Policy = No_Name then Policy := Name_Ignore; end if; + + Level := Ghost_Assertion_Level (Gen_Id); end if; -- Mark the instantiation as Ghost - Mark_Ghost_Declaration_Or_Body (N, Policy); + Mark_Ghost_Declaration_Or_Body (N, Policy, Level); -- Install the appropriate Ghost region - Install_Ghost_Region (Policy, N); + Install_Ghost_Region (Policy, N, Level); -- Check Ghost actuals. Given that this routine is unconditionally -- invoked with subprogram and package instantiations, this check @@ -1739,25 +2236,39 @@ package body Ghost is procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id) is Id : Entity_Id; - begin -- A procedure call becomes Ghost when the procedure being invoked is -- Ghost. Install the Ghost mode of the procedure. Id := Get_Enclosing_Ghost_Entity (Name (N)); - if Present (Id) then - if Is_Checked_Ghost_Entity (Id) then - Install_Ghost_Region (Check, N); + Mark_And_Set_Ghost_Region (N, Id); + end Mark_And_Set_Ghost_Procedure_Call; - elsif Is_Ignored_Ghost_Entity (Id) then - Install_Ghost_Region (Ignore, N); + ------------------------------- + -- Mark_And_Set_Ghost_Region -- + ------------------------------- - Set_Is_Ignored_Ghost_Node (N); - Record_Ignored_Ghost_Node (N); - end if; + procedure Mark_And_Set_Ghost_Region (N : Node_Id; Id : Entity_Id) is + Id_Policy : Name_Id; + begin + -- Nothing to do if we are not dealing with a ghost entity + + if No (Id) or else not Is_Ghost_Entity (Id) then + return; end if; - end Mark_And_Set_Ghost_Procedure_Call; + + Id_Policy := Ghost_Policy_In_Effect (Id); + + if Id_Policy = Name_Check then + Install_Ghost_Region (Check, N, Ghost_Assertion_Level (Id)); + + elsif Id_Policy = Name_Ignore then + Install_Ghost_Region (Ignore, N, Ghost_Assertion_Level (Id)); + Set_Is_Ignored_Ghost_Node (N); + Record_Ignored_Ghost_Node (N); + end if; + end Mark_And_Set_Ghost_Region; ----------------------- -- Mark_Ghost_Clause -- @@ -1792,8 +2303,9 @@ package body Ghost is ------------------------------------ procedure Mark_Ghost_Declaration_Or_Body - (N : Node_Id; - Mode : Name_Id) + (N : Node_Id; + Mode : Name_Id; + Level : Entity_Id) is Id : constant Entity_Id := Defining_Entity (N); @@ -1802,7 +2314,7 @@ package body Ghost is Param_Id : Entity_Id; begin - -- Mark the related node and its entity + Set_Ghost_Assertion_Level (Id, Level); if Mode = Name_Check then Mark_Formals := True; @@ -1835,6 +2347,8 @@ package body Ghost is while Present (Param) loop Param_Id := Defining_Entity (Param); + Set_Ghost_Assertion_Level (Param_Id, Level); + if Mode = Name_Check then Set_Is_Checked_Ghost_Entity (Param_Id); @@ -1891,7 +2405,7 @@ package body Ghost is Id : Entity_Id) is Policy : Name_Id := No_Name; - + Level : constant Entity_Id := Ghost_Assertion_Level (Id); begin -- A renaming becomes Ghost when it renames a Ghost entity @@ -1902,7 +2416,7 @@ package body Ghost is Policy := Name_Ignore; end if; - Mark_Ghost_Declaration_Or_Body (N, Policy); + Mark_Ghost_Declaration_Or_Body (N, Policy, Level); end Mark_Ghost_Renaming; ------------------------ @@ -2036,19 +2550,21 @@ package body Ghost is -------------------------------- procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is + Level : constant Entity_Id := Ghost_Assertion_Level (Id); begin if Is_Checked_Ghost_Entity (Id) then - Install_Ghost_Mode (Check); + Install_Ghost_Region (Check, N, Level); elsif Is_Ignored_Ghost_Entity (Id) then - Install_Ghost_Mode (Ignore); + Install_Ghost_Region (Ignore, N, Level); else - Install_Ghost_Mode (None); + Install_Ghost_Region (None, N, Level); end if; end Set_Ghost_Mode_From_Entity; -- Local variables - Id : Entity_Id; + Id : Entity_Id; + Level : Entity_Id; -- Start of processing for Set_Ghost_Mode @@ -2084,12 +2600,13 @@ package body Ghost is -- property is encoded in the pragma itself. elsif Nkind (N) = N_Pragma then + Level := Pragma_Ghost_Assertion_Level (N); if Is_Checked_Ghost_Pragma (N) then - Install_Ghost_Mode (Check); + Install_Ghost_Region (Check, N, Level); elsif Is_Ignored_Ghost_Pragma (N) then - Install_Ghost_Mode (Ignore); + Install_Ghost_Region (Ignore, N, Level); else - Install_Ghost_Mode (None); + Install_Ghost_Region (None, N, Level); end if; -- The Ghost mode of a procedure call depends on the Ghost mode of the @@ -2109,7 +2626,7 @@ package body Ghost is ------------------------- procedure Set_Is_Ghost_Entity (Id : Entity_Id) is - Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + Policy : constant Name_Id := Ghost_Policy_In_Effect (Id); begin if Policy = Name_Check then Set_Is_Checked_Ghost_Entity (Id); diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 62c809c8fd3..cc83d678088 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -32,6 +32,16 @@ with Types; use Types; package Ghost is + function Assertion_Level_From_Arg (Arg : Node_Id) return Entity_Id; + -- Returns the assertion level for the given pragma or aspect based on + -- the argument Arg. Which is either + -- + -- * Standard_Level_Default if there was no argument or the argument + -- evaluated to True. + -- * Assertion_Level if the argument was referencing a user defined + -- Assertion_Level. + -- * Empty othrwise since we are not dealing with a ghost entity. + procedure Check_Ghost_Completion (Prev_Id : Entity_Id; Compl_Id : Entity_Id); @@ -90,7 +100,9 @@ package Ghost is Constit : Node_Id; Constit_Id : Entity_Id); -- Verify that the Ghost policy of constituent Constit_Id is compatible - -- with the Ghost policy of abstract state State_I. + -- with the Ghost policy of abstract state State_Id. + -- + -- Additionally verify that the Ghost_Assertion_Levels are compatible. procedure Check_Ghost_Type (Typ : Entity_Id); -- Verify that Ghost type Typ is neither concurrent, nor effectively @@ -102,11 +114,23 @@ package Ghost is procedure Initialize; -- Initialize internal tables - procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id); + procedure Install_Ghost_Region + (Mode : Ghost_Mode_Type; + N : Node_Id; + Level : Entity_Id); pragma Inline (Install_Ghost_Region); -- Install a Ghost region described by mode Mode and ignored region start -- node N. + function Is_Assertion_Level_Dependent + (Self : Entity_Id; Other : Entity_Id) return Boolean; + -- Check that assertion level Self is assertion-level-dependent with Other. + -- + -- According to SPARK RM 6.9(5) this means that + -- * Either Self or Other has the default assertion level. + -- * Self either is or depends on Other + -- * Self either is or depends on Static + function Is_Ghost_Assignment (N : Node_Id) return Boolean; -- Determine whether arbitrary node N denotes an assignment statement whose -- target is a Ghost entity. diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads index 6fc636794d3..b022b337c44 100644 --- a/gcc/ada/lib-xref.ads +++ b/gcc/ada/lib-xref.ads @@ -445,6 +445,7 @@ package Lib.Xref is E_Anonymous_Access_Type => ' ', E_Array_Subtype => 'A', E_Array_Type => 'A', + E_Assertion_Level => 'z', E_Block => 'q', E_Class_Wide_Subtype => 'C', E_Class_Wide_Type => 'C', @@ -547,7 +548,7 @@ package Lib.Xref is -- w protected object protected type -- x abstract procedure exception -- y abstract function entry or entry family - -- z generic formal parameter (unused) + -- z generic formal parameter assertion level --------------------------------------------------- -- Handling of Imported and Exported Subprograms -- diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 73f9fe8e8f7..524a823bb8f 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -755,6 +755,18 @@ package Opt is -- reflect the starting node of the outermost ignored Ghost region. If a -- nested ignored Ghost region is entered, the value must remain -- unchanged. + + Ghost_Mode_Assertion_Level : Entity_Id := Empty; + -- The Assertion_Level that is applied to the current ghost region. + -- It is either: + -- * Empty - when there is no ghost region + -- * Assertion_Level - if the ghost aspect/pragama had an + -- Assertion_Levle associated with it. + -- * Standard_Default_Level - if the ghost aspect/pragama did not have + -- an Assertion_Level associated to it. + + Current_Region : Node_Id := Empty; + -- Latest ghost region end record; Ghost_Config : Ghost_Config_Type; diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 4d0ffe62549..1bb81b0c79a 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1394,6 +1394,7 @@ begin | Pragma_Annotate | Pragma_Assert | Pragma_Assert_And_Cut + | Pragma_Assertion_Level | Pragma_Assertion_Policy | Pragma_Assume | Pragma_Assume_No_Invalid_Values diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb index f47aacc7748..e15e93f2fba 100644 --- a/gcc/ada/rtsfind.adb +++ b/gcc/ada/rtsfind.adb @@ -1114,7 +1114,7 @@ package body Rtsfind is -- Provide a clean environment for the unit Ignore_SPARK_Mode_Pragmas_In_Instance := False; - Install_Ghost_Region (None, Empty); + Install_Ghost_Region (None, Empty, Empty); Install_SPARK_Mode (None, Empty); -- Otherwise we need to load the unit, First build unit name from the diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index 944ece11978..731a97daaec 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.adb @@ -1460,7 +1460,7 @@ package body Sem is -- Set up a clean environment before analyzing - Install_Ghost_Region (None, Empty); + Install_Ghost_Region (None, Empty, Empty); Ignore_SPARK_Mode_Pragmas_In_Instance := False; Outer_Generic_Scope := Empty; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 31735e41a9c..5adf5f48320 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1960,6 +1960,14 @@ package body Sem_Ch13 is -- expression is allowed. Includes checking that the expression -- does not raise Constraint_Error. + procedure Convert_Aspect_With_Assertion_Levels (Aspect : Node_Id); + -- If an Aspect is using an association with an Assertion_Level + -- analyze the aspect with the level and convert it into an aspect + -- without the Assertion_Level. In the case the aspect has + -- associations with Assertion_Levels then multiple aspects are + -- created and each one will point to the original aspect that + -- they were created from in the Original_Aspect field. + function Directly_Specified (Id : Entity_Id; A : Aspect_Id) return Boolean; -- Returns True if the given aspect is directly (as opposed to @@ -3114,6 +3122,73 @@ package body Sem_Ch13 is end case; end Check_Expr_Is_OK_Static_Expression; + ------------------------------------------ + -- Convert_Aspect_With_Assertion_Levels -- + ------------------------------------------ + + procedure Convert_Aspect_With_Assertion_Levels (Aspect : Node_Id) + is + Assoc : Node_Id; + Assocs : List_Id; + Choice : Node_Id; + Level : Entity_Id; + Sub_Expr : Node_Id; + New_Aspect : Node_Id; + begin + Assocs := Component_Associations (Expression (Aspect)); + Assoc := First (Assocs); + + if Present (Expressions (Expression (Aspect))) then + Error_Msg_N + ("wrong syntax for argument of %", Expression (Aspect)); + Error_Msg_N + ("\aspect with Assertion_Level can only contain " + & "contain Assertion_Level associations", + Expression (Aspect)); + end if; + + while Present (Assoc) loop + if List_Length (Choices (Assoc)) > 1 then + Error_Msg_Name_1 := Nam; + Error_Msg_N ("wrong syntax for argument of %", Assoc); + Error_Msg_N + ("\only one Assertion_Level can be associated " + & "with an expression", + Assoc); + end if; + + Choice := First (Choices (Assoc)); + + if Nkind (Choice) /= N_Identifier then + Error_Msg_N ("wrong syntax for argument of %", Assoc); + Error_Msg_N + ("\association must denote an Assertion_Level", Assoc); + end if; + + Level := Get_Assertion_Level (Chars (Choice)); + + Sub_Expr := Expression (Assoc); + New_Aspect := + Make_Aspect_Specification + (Sloc => Sloc (Assoc), + Identifier => New_Copy_Tree (Id), + Expression => Sub_Expr); + + Check_Applicable_Policy (New_Aspect, Level); + + Set_Aspect_Ghost_Assertion_Level (New_Aspect, Level); + + Insert_After (Aspect, New_Aspect); + + -- Store the Original_Aspect for the detection of + -- duplicates. + + Set_Original_Aspect (New_Aspect, Aspect); + + Next (Assoc); + end loop; + end Convert_Aspect_With_Assertion_Levels; + ------------------------ -- Directly_Specified -- ------------------------ @@ -3160,11 +3235,10 @@ package body Sem_Ch13 is -- Set additional semantic fields - if Is_Ignored (Aspect) then - Set_Is_Ignored (Aitem); - elsif Is_Checked (Aspect) then - Set_Is_Checked (Aitem); - end if; + Set_Is_Checked (Aitem, Is_Checked (Aspect)); + Set_Is_Ignored (Aitem, Is_Ignored (Aspect)); + Set_Pragma_Ghost_Assertion_Level + (Aitem, Aspect_Ghost_Assertion_Level (Aspect)); Set_Corresponding_Aspect (Aitem, Aspect); Set_From_Aspect_Specification (Aitem); @@ -3185,7 +3259,22 @@ package body Sem_Ch13 is -- as such for later reference in the tree. This also sets the -- Is_Ignored and Is_Checked flags appropriately. - Check_Applicable_Policy (Aspect); + if Is_Valid_Assertion_Kind (Nam) then + if Is_Checked (Aspect) or else Is_Ignored (Aspect) then + null; + + -- If the Aspect has at least one Assertion_Level argument + -- then split the original Aspect into multiple aspects each + -- with an associated Assertion_Level. + + elsif Has_Assertion_Level_Argument (Aspect) then + Convert_Aspect_With_Assertion_Levels (Aspect); + goto Continue; + else + Check_Applicable_Policy (Aspect); + end if; + + end if; if Is_Disabled (Aspect) then goto Continue; @@ -3249,8 +3338,11 @@ package body Sem_Ch13 is if No_Duplicates_Allowed (A_Id) then Anod := First (L); while Anod /= Aspect loop - if Comes_From_Source (Aspect) - and then Same_Aspect (A_Id, Get_Aspect_Id (Anod)) + + if (Comes_From_Source (Aspect) + or else (Original_Aspect (Aspect) /= Anod + and then not From_Same_Aspect (Aspect, Anod))) + and then Same_Aspect (A_Id, Get_Aspect_Id (Anod)) then Error_Msg_Name_1 := Nam; Error_Msg_Sloc := Sloc (Anod); @@ -3260,12 +3352,12 @@ package body Sem_Ch13 is if Class_Present (Anod) = Class_Present (Aspect) then if not Class_Present (Anod) then Error_Msg_NE - ("aspect% for & previously given#", - Id, E); + ("aspect% for & previously given#", Id, E); else Error_Msg_NE ("aspect `%''Class` for & previously given#", - Id, E); + Id, + E); end if; end if; end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 4fd5b658a78..191a6603f88 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -101,6 +101,121 @@ with System.Case_Util; package body Sem_Prag is + ---------------------------------- + -- Handling of Assertion Levels -- + ---------------------------------- + + -- Assertion levels are special entities declared using pragma + -- Assertion_Level. Assertion levels can be used in most Assertion_Kind + -- pragmas to associate a given level with a given list of existing + -- arguments. E.g. + -- + -- pragma Assert (Level1 => (Expr1, "Msg1"), + -- Level2 => (Expr2, "Msg2")); + -- + -- Assertion levels can also be used in pragma Assertion_Policy and + -- Check_Policy as a valid policy name. E.g. + -- + -- pragma Assertion_Policy (Level1 => Check); + + -------------------------------- + -- Declaring Assertion Levels -- + -------------------------------- + + -- Assertion levels are declared using configuration level pragma + -- Assertion_Level. We create a new E_Assertion_Level entity for each + -- pragma and add each unique level to the Assertion_Levels table. + -- + -- A pragma can be declared with dependencies. e.g. + -- + -- pragma Assertion_Level (L1); + -- pragma Assertion_Level (L2, Depends => L1); + -- pragma Assertion_Level (L3, Depends => L2); + -- + -- Levels that a level depends are called parent levels. Levels that depend + -- on a given level are called child levels. These dependencies are stored + -- in an E_Assertion_Level entity as attributes Parent_Levels and + -- Child_Levels. + -- + -- When a pragma with the same level name is declared, we check that the + -- assertion level is declared with the same dependencies as the existing + -- level. Otherwise an error is raised. + + package Assertion_Levels is new Table.Table ( + Table_Component_Type => Entity_Id, + Table_Index_Type => Nat, + Table_Low_Bound => 1, + Table_Initial => 30, + Table_Increment => 200, + Table_Name => "Assertion_Levels"); + + ------------------------------------------- + -- Applying Policies to Assertion Levels -- + ------------------------------------------- + + -- When a policy is applied to an assertion level, all assertions + -- associated with that level are subjected to the same policy. Depending + -- on the policy value, the same policy is applied to its dependencies. + -- + -- Consider the following assertion levels: + -- + -- pragma Assertion_Level (L1); + -- pragma Assertion_Level (L2, Depends => L1); + -- pragma Assertion_Level (L3, Depends => L2); + -- + -- When policy Check (or On) is applied to an assertion level, it is also + -- applied to all of its transitive parent levels. For example + -- + -- pragma Assertion_Policy (L3 => Check); + -- + -- applies policy Check to L2 and L1. + -- + -- When policy Ignore (or Off) is applied to an assertion level, it is also + -- applied to all of its transitive child levels. For example + -- + -- pragma Assertion_Policy (L1 => Ignore); + -- + -- applies the policy Ignore for L2 and L3. + -- + -- Note that assertion levels are not allowed to have the same name as any + -- other Assertion_Kind defined in the RM in order to avoid unintentional + -- name overloading. + + -------------------------------------------------- + -- Handling of Assertions with Assertion Levels -- + -------------------------------------------------- + + -- Each Assertion pragma (see Is_Valid_Assertion) supports a new syntax + -- where the existing arguments can be associated with an assertion level. + -- + -- Each association is converted into a new pragma with the same name but + -- without the level argument, and the old pragma is rewritten as N_Null. + -- An applicable policy for those pragmas is calculated by looking at the + -- first active Check_Policy that either matches the pragma name or the + -- name of the Assertion_Level. The following policy-based attributes are + -- set for the given pramga: + -- + -- * Is_Checked - Based on the policy + -- * Is_Ignored - Based on the policy + -- * Is_Disabled - Based on the policy + -- * Pragma_Ghost_Assertion_Level - level associated with the assertion. + -- * Original_Pragma - reference to the original pragma that had the + -- Assertion_Levels. + -- + -- For example, the following pragma: + -- + -- pragma Assert (L1 => (Expr1, "Msg1"), + -- L2 => (Expr2, "Msg2")); + -- + -- is rewritten as: + -- + -- null; -- The original pragma + -- pragma Assert (Expr1, "Msg1"); + -- pragma Assert (Expr2, "Msg2"); + -- + -- Each of the new pragmas is analyzed according to its existing semantic + -- rules. + ---------------------------------------------- -- Common Handling of Import-Export Pragmas -- ---------------------------------------------- @@ -212,6 +327,14 @@ package body Sem_Prag is -- Query whether a particular item appears in a mixed list of nodes and -- entities. It is assumed that all nodes in the list have entities. + procedure Apply_Check_Policy (N : Node_Id; Policy : Name_Id); + -- Set the Is_Checked, Is_Ignored, Is_Disabled attributes on node N + -- based on the Policy. e.g. + -- + -- * When Name_Ignore (or Name_Off) is used the node is marked as ignored. + -- * When Name_Check (or Name_On) is used the node is marked as checked. + -- * When Name_Disable is used the node is marked as disabled. + procedure Check_Postcondition_Use_In_Inlined_Subprogram (Prag : Node_Id; Spec_Id : Entity_Id); @@ -266,6 +389,11 @@ package body Sem_Prag is -- set, the routine reports duplicate pragmas. The routine returns Empty -- when reaching the start of the node chain. + function Get_Applicable_Policy + (Nam : Name_Id; Level : Entity_Id) return Name_Id; + -- Return the name of the Check_Policy applied to the name or the level + -- associated with the node. + function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id; -- If Def_Id refers to a renamed subprogram, then the base subprogram (the -- original one, following the renaming chain) is returned. Otherwise the @@ -281,6 +409,15 @@ package body Sem_Prag is -- Determine whether dependency clause Clause is surrounded by extra -- parentheses. If this is the case, issue an error message. + procedure Mark_Is_Checked (N : Node_Id); + -- Sets Is_Checked and unsets Is_Ignored + + procedure Mark_Is_Disabled (N : Node_Id); + -- Sets Is_Disabled and Is_Ignored and unsets Is_Checked + + procedure Mark_Is_Ignored (N : Node_Id); + -- Sets Is_Ignored and unsets Is_Checked + procedure Record_Possible_Body_Reference (State_Id : Entity_Id; Ref : Node_Id); @@ -4830,16 +4967,10 @@ package body Sem_Prag is (Arg : Node_Id; N1, N2 : Name_Id); procedure Check_Arg_Is_One_Of - (Arg : Node_Id; - N1, N2, N3 : Name_Id); - procedure Check_Arg_Is_One_Of - (Arg : Node_Id; - N1, N2, N3, N4 : Name_Id); - procedure Check_Arg_Is_One_Of - (Arg : Node_Id; - N1, N2, N3, N4, N5 : Name_Id); + (Arg : Node_Id; + Names : Name_List); -- Check the specified argument Arg to make sure that it is an - -- identifier whose name matches either N1 or N2 (or N3, N4, N5 if + -- identifier whose name matches either N1 or N2 (or a list of names is -- present). If not then give error and raise Pragma_Exit. procedure Check_Arg_Is_Queuing_Policy (Arg : Node_Id); @@ -4995,6 +5126,11 @@ package body Sem_Prag is -- presence of at least one component. UU_Typ is the related Unchecked_ -- Union type. + function Create_Pragma_Without_Assertion_Level + (Expr : Node_Id) return Node_Id; + -- Creates a new pragma from an Assertion_Level association argument + -- with the same name as the orignal pragma. + procedure Ensure_Aggregate_Form (Arg : Node_Id); -- Subsidiary routine to the processing of pragmas Abstract_State, -- Contract_Cases, Depends, Exceptional_Cases, Global, Initializes, @@ -5450,6 +5586,19 @@ package body Sem_Prag is -- a class-wide precondition only if one of its ancestors has an -- explicit class-wide precondition. + function Assertion_Level_Pragma_Comes_From_Source + (N : Node_Id) return Boolean + is (Present (Original_Pragma (N)) + and then Present (Original_Node (Original_Pragma (N))) + and then Comes_From_Source (Original_Node (Original_Pragma (N)))); + -- Determine whether a pragma was originally from source and used an + -- assertion level. + -- + -- When the pragma was using an Assertion_Level it was replaced by + -- a new pragma where the Original_Pragma points to the original + -- pragma node which was removed from the tree and replaced by a + -- null node. + ----------------------------- -- Inherits_Class_Wide_Pre -- ----------------------------- @@ -5543,7 +5692,9 @@ package body Sem_Prag is -- rewriting the pragma identifier. This allows the retrieval of the -- original pragma name by routine Original_Aspect_Pragma_Name. - if Comes_From_Source (N) then + if Comes_From_Source (N) + or else Assertion_Level_Pragma_Comes_From_Source (N) + then if Pname in Name_Pre | Name_Pre_Class then Is_Pre_Post := True; Set_Class_Present (N, Pname = Name_Pre_Class); @@ -6445,45 +6596,18 @@ package body Sem_Prag is end Check_Arg_Is_One_Of; procedure Check_Arg_Is_One_Of - (Arg : Node_Id; - N1, N2, N3 : Name_Id) + (Arg : Node_Id; + Names : Name_List) is Argx : constant Node_Id := Get_Pragma_Arg (Arg); - begin Check_Arg_Is_Identifier (Argx); - if Chars (Argx) not in N1 | N2 | N3 then - Error_Pragma_Arg ("invalid argument for pragma%", Argx); - end if; - end Check_Arg_Is_One_Of; - - procedure Check_Arg_Is_One_Of - (Arg : Node_Id; - N1, N2, N3, N4 : Name_Id) - is - Argx : constant Node_Id := Get_Pragma_Arg (Arg); - - begin - Check_Arg_Is_Identifier (Argx); - - if Chars (Argx) not in N1 | N2 | N3 | N4 then - Error_Pragma_Arg ("invalid argument for pragma%", Argx); + if (for some Name of Names => Chars (Argx) = Name) then + return; end if; - end Check_Arg_Is_One_Of; - - procedure Check_Arg_Is_One_Of - (Arg : Node_Id; - N1, N2, N3, N4, N5 : Name_Id) - is - Argx : constant Node_Id := Get_Pragma_Arg (Arg); - begin - Check_Arg_Is_Identifier (Argx); - - if Chars (Argx) not in N1 | N2 | N3 | N4 | N5 then - Error_Pragma_Arg ("invalid argument for pragma%", Argx); - end if; + Error_Pragma_Arg ("invalid argument for pragma%", Argx); end Check_Arg_Is_One_Of; --------------------------------- @@ -7602,6 +7726,114 @@ package body Sem_Prag is end loop; end Check_Variant; + ------------------------------------------- + -- Create_Pragma_Without_Assertion_Level -- + ------------------------------------------- + + function Create_Pragma_Without_Assertion_Level + (Expr : Node_Id) return Node_Id + is + function Aggregate_To_Associations (N : Node_Id) return List_Id; + -- Converts an Aggregate into a list of + -- Pragma_Argument_Associations. + + procedure Validate_Assertion_Level_Aggregate (N : Node_Id); + -- Handle invalid syntax scenarios for an Aggregate containing + -- Assertion_Levels. + + ------------------------------- + -- Aggregate_To_Associations -- + ------------------------------- + + function Aggregate_To_Associations (N : Node_Id) return List_Id is + Args : constant List_Id := New_List; + Comp_Assn : Node_Id; + Comp_Expr : Node_Id; + Comp_Expr_Repl : Node_Id; + Choice : Node_Id; + begin + pragma Assert (Nkind (N) = N_Aggregate); + Validate_Assertion_Level_Aggregate (N); + + Comp_Expr := First (Expressions (N)); + while Present (Comp_Expr) loop + -- Remove the expression from the list so that it can be + -- inserted into the new Pragma_Argument_Association. + + Comp_Expr_Repl := Comp_Expr; + Next (Comp_Expr); + Remove (Comp_Expr_Repl); + Append_To + (Args, + Make_Pragma_Argument_Association + (Sloc (Comp_Expr_Repl), + Expression => Comp_Expr_Repl)); + end loop; + + Comp_Assn := First (Component_Associations (N)); + while Present (Comp_Assn) loop + Choice := First (Choices (Comp_Assn)); + Append_To + (Args, + Make_Pragma_Argument_Association + (Sloc (Comp_Assn), + Chars => Chars (Choice), + Expression => Expression (Comp_Assn))); + Next (Comp_Assn); + end loop; + return Args; + end Aggregate_To_Associations; + + ---------------------------------------- + -- Validate_Assertion_Level_Aggregate -- + ---------------------------------------- + + procedure Validate_Assertion_Level_Aggregate (N : Node_Id) is + Comp_Assn : Node_Id; + Choice : Node_Id; + begin + Comp_Assn := First (Component_Associations (N)); + while Present (Comp_Assn) loop + if List_Length (Choices (Comp_Assn)) /= 1 then + Error_Pragma_Arg + ("only one Assertion_Level can be associated " + & "with an expression", + Comp_Assn); + end if; + + Choice := First (Choices (Comp_Assn)); + + if Nkind (Choice) /= N_Identifier then + Error_Pragma_Arg + ("\association must denote an Assertion_Level", Comp_Assn); + end if; + Next (Comp_Assn); + end loop; + end Validate_Assertion_Level_Aggregate; + + -- Local variables + + Args : List_Id; + + -- Start of proessing for Create_Pragma_Without_Assertion_Level + + begin + if Nkind (Expr) in N_Aggregate then + Validate_Assertion_Level_Aggregate (Expr); + Args := Aggregate_To_Associations (Expr); + else + Args := + New_List + (Make_Pragma_Argument_Association (Sloc (Expr), + Expression => Expr)); + end if; + + return + Make_Pragma (Sloc (N), + Chars => Pname, + Pragma_Argument_Associations => Args); + end Create_Pragma_Without_Assertion_Level; + --------------------------- -- Ensure_Aggregate_Form -- --------------------------- @@ -12336,6 +12568,13 @@ package body Sem_Prag is end Set_Ravenscar_Profile; + -- Local variables + + Assoc : Node_Id; + Last_Prag : Node_Id; + Level : Entity_Id; + Sub_Prag : Node_Id; + -- Start of processing for Analyze_Pragma begin @@ -12429,8 +12668,7 @@ package body Sem_Prag is elsif Is_Rewrite_Substitution (N) and then Nkind (Original_Node (N)) = N_Pragma then - Set_Is_Ignored (N, Is_Ignored (Original_Node (N))); - Set_Is_Checked (N, Is_Checked (Original_Node (N))); + Set_Pragma_Ghost_Assertion_Level (N, Original_Node (N)); -- Skip querying the applicable policy at this point for dynamic -- predicate checks since they rely on the policy applicable in @@ -12446,18 +12684,67 @@ package body Sem_Prag is -- Otherwise query the applicable policy at this point - else - Check_Applicable_Policy (N); + elsif Is_Valid_Assertion_Kind (Pname) then + -- If the pragma is using Assertion_Level associations, analyze the + -- applicable policies for that pragma and then convert it into a + -- pragma without assertion levels. Analyze the new pragma with + -- policy-related attributes (Is_Checked/Is_Ignored/Is_Disabled) + -- already set. + + if Has_Assertion_Level_Argument (N) then + Assoc := First (Pragma_Argument_Associations (N)); + Last_Prag := N; + while Present (Assoc) loop + Level := Get_Assertion_Level (Chars (Assoc)); + Sub_Prag := + Create_Pragma_Without_Assertion_Level (Expression (Assoc)); + + -- Set policy based attributes based on the pragma name and the + -- assertion level. + + Check_Applicable_Policy (Sub_Prag, Level); - -- If pragma is disabled, rewrite as NULL and skip analysis + -- Store the Level on the pragma node for easier access + + Set_Pragma_Ghost_Assertion_Level (Sub_Prag, Level); + + -- Store the Original_Pragma for the detection of + -- duplicates. + + Set_Original_Pragma (Sub_Prag, N); + + -- Insert the created pragmas in the same order after the + -- original pragma and analyze them later. + + Insert_After (Last_Prag, Sub_Prag); + Last_Prag := Sub_Prag; + + Next (Assoc); + end loop; + + -- Remove the original pragma and continue processing all + -- of the new sub-pragmas. - if Is_Disabled (N) then Rewrite (N, Make_Null_Statement (Loc)); Analyze (N); raise Pragma_Exit; + + -- Otherwise apply the policy based attributes based on the pragma + -- name. + + else + Check_Applicable_Policy (N, Empty); end if; end if; + -- If the pragma is disabled, rewrite it as NULL and skip its analysis + + if Is_Disabled (N) then + Rewrite (N, Make_Null_Statement (Loc)); + Analyze (N); + raise Pragma_Exit; + end if; + -- Mark assertion pragmas as Ghost depending on their enclosing context if Assertion_Expression_Pragma (Prag_Id) then @@ -13090,6 +13377,12 @@ package body Sem_Prag is if Present (State_Id) then Set_Is_Ghost_Entity (State_Id); + + -- Amend the Assertion_Level coming from the + -- package. + + Set_Ghost_Assertion_Level + (State_Id, Standard_Level_Default); end if; -- Synchronous @@ -13170,7 +13463,26 @@ package body Sem_Prag is elsif Chars (Opt_Nam) = Name_Part_Of then Analyze_Part_Of_Option (Opt); + elsif Chars (Opt_Nam) = Name_Ghost then + Check_Duplicate_Option (Opt, Ghost_Seen); + Check_Ghost_Synchronous; + + if Present (State_Id) then + Set_Is_Ghost_Entity (State_Id); + + -- Amend the Assertion_Level coming from the + -- package. + + if Nkind (Expression (Opt)) /= N_Identifier then + Error_Pragma_Arg + ("level name must be an identifier", N); + end if; + Set_Ghost_Assertion_Level + (State_Id, + Get_Assertion_Level + (Chars (Expression (Opt)))); + end if; else SPARK_Msg_N ("invalid state option", Opt); end if; @@ -14022,8 +14334,13 @@ package body Sem_Prag is -- Local variables - Expr : Node_Id; - New_Args : List_Id; + Args : Args_List (1 .. 2); + Arg_Check : Node_Id renames Args (1); + Arg_Message : Node_Id renames Args (2); + Check_Prag : Node_Id; + New_Args : List_Id; + Names : constant Name_List (1 .. 2) := + (Name_Check, Name_Message); -- Start of processing for Assert @@ -14041,25 +14358,25 @@ package body Sem_Prag is Check_At_Least_N_Arguments (1); Check_At_Most_N_Arguments (2); - Check_Arg_Order ((Name_Check, Name_Message)); - Check_Optional_Identifier (Arg1, Name_Check); - Expr := Get_Pragma_Arg (Arg1); + Gather_Associations (Names, Args); + Check_Arg_Order (Names); -- Special processing for Loop_Invariant, Loop_Variant or for -- other cases where a Loop_Entry attribute is present. If the -- assertion pragma contains attribute Loop_Entry, ensure that -- the related pragma is within a loop. - if Prag_Id = Pragma_Loop_Invariant + if Prag_Id = Pragma_Loop_Invariant or else Prag_Id = Pragma_Loop_Variant - or else Contains_Loop_Entry (Expr) + or else Contains_Loop_Entry (Arg_Check) then Check_Loop_Pragma_Placement; -- Perform preanalysis to deal with embedded Loop_Entry -- attributes. - Preanalyze_And_Resolve_Assert_Expression (Expr, Any_Boolean); + Preanalyze_And_Resolve_Assert_Expression + (Arg_Check, Any_Boolean); end if; -- Implement Assert[_And_Cut]/Assume/Loop_Invariant by generating @@ -14079,30 +14396,186 @@ package body Sem_Prag is New_Args := New_List ( Make_Pragma_Argument_Association (Loc, Expression => Make_Identifier (Loc, Pname)), - Make_Pragma_Argument_Association (Sloc (Expr), - Expression => Expr)); + Make_Pragma_Argument_Association (Sloc (Arg_Check), + Expression => Arg_Check)); - if Arg_Count > 1 then - Check_Optional_Identifier (Arg2, Name_Message); + if Present (Arg_Message) then -- Provide semantic annotations for optional argument, for -- ASIS use, before rewriting. -- Is this still needed??? - Preanalyze_And_Resolve (Expression (Arg2), Standard_String); + Preanalyze_And_Resolve (Arg_Message, Standard_String); Append_To (New_Args, New_Copy_Tree (Arg2)); end if; -- Rewrite as Check pragma - Rewrite (N, - Make_Pragma (Loc, - Chars => Name_Check, - Pragma_Argument_Associations => New_Args)); + Check_Prag := + Make_Pragma + (Loc, + Chars => Name_Check, + Pragma_Argument_Associations => New_Args); + Copy_Assertion_Policy_Attributes (Check_Prag, N); + Rewrite (N, Check_Prag); Analyze (N); end Assert; + --------------------- + -- Assertion_Level -- + --------------------- + + -- pragma Assertion_Level (LEVEL_IDENTIFIER + -- [, depends => DEPENDENCY_DESCRIPTOR]); + -- + -- DEPENDENCY_DESCRIPTOR ::= LEVEL_IDENTIFIER | LEVEL_IDENTIFIER_LIST + -- + -- LEVEL_IDENTIFIER_LIST ::= '[' LEVEL_IDENTIFIER + -- {, LEVEL_IDENTIFIER} ']' + + when Pragma_Assertion_Level => Assertion_Level : declare + procedure Add_Dependencies + (Level : Entity_Id; Parent_Level : Entity_Id); + -- Adds the following dependencies: + -- * Adds Parent_Level to the Parent_Levels of Level + -- * Adds Level to the Child_Levels of Parent_Level + + procedure Check_Known_Level_Name + (Level : Entity_Id; Ref : Node_Id); + -- Raise an error if the level has not be declared before + + procedure Check_Valid_Level_Name (Nam : Name_Id); + -- Raise an error if the name matches a valid assertion kind. + -- + -- This is to avoid the ambigiouty in Assertion_Policy if either + -- the level or the assertion kind is affected by the policy. + + procedure Check_Valid_Level_Node (N : Node_Id); + -- Raise an error if the node is not a simple identifier + + ---------------------- + -- Add_Dependencies -- + ---------------------- + + procedure Add_Dependencies + (Level : Entity_Id; Parent_Level : Entity_Id) + is + Parent_Level_List : Elist_Id; + Child_Levels_List : Elist_Id; + begin + if No (Parent_Levels (Level)) then + Set_Parent_Levels (Level, New_Elmt_List); + end if; + Parent_Level_List := Parent_Levels (Level); + Append_Elmt (Parent_Level, Parent_Level_List); + + if No (Child_Levels (Parent_Level)) then + Set_Child_Levels (Parent_Level, New_Elmt_List); + end if; + Child_Levels_List := Child_Levels (Parent_Level); + Append_Elmt (Level, Child_Levels_List); + end Add_Dependencies; + + ---------------------------- + -- Check_Known_Level_Name -- + ---------------------------- + + procedure Check_Known_Level_Name + (Level : Entity_Id; Ref : Node_Id) is + begin + if No (Level) then + Error_Msg_Name_1 := Chars (Ref); + Error_Msg_N ("unknown assertion level &", Ref); + raise Pragma_Exit; + end if; + end Check_Known_Level_Name; + + ---------------------------- + -- Check_Valid_Level_Name -- + ---------------------------- + + procedure Check_Valid_Level_Name (Nam : Name_Id) is + begin + if Is_Valid_Assertion_Kind (Nam) then + Error_Pragma_Arg + ("level name cannot match an assertion kind", Arg1); + end if; + end Check_Valid_Level_Name; + + ---------------------------- + -- Check_Valid_Level_Node -- + ---------------------------- + + procedure Check_Valid_Level_Node (N : Node_Id) is + begin + if Nkind (N) /= N_Identifier then + Error_Pragma_Arg ("level name must be an identifier", N); + end if; + end Check_Valid_Level_Node; + + -- Local variables + + Dep : Node_Id; + Dep_Id : Entity_Id; + Dep_Arg : Node_Id; + Level_Arg : Node_Id; + Level_Id : Entity_Id; + Level_Nam : Name_Id; + + -- Start of processing for Pragma_Assertion_Level + + begin + GNAT_Pragma; + Check_Valid_Configuration_Pragma; + Check_At_Least_N_Arguments (1); + Check_At_Most_N_Arguments (2); + + Check_No_Identifier (Arg1); + + Level_Arg := Expression (Arg1); + Check_Valid_Level_Node (Level_Arg); + + Level_Nam := Chars (Level_Arg); + Check_Valid_Level_Name (Level_Nam); + + Level_Id := Make_Assertion_Level (Loc, Level_Nam); + + Set_Parent (Level_Id, Level_Arg); + Set_Entity (Level_Arg, Level_Id); + + if Arg_Count = 2 then + Check_Identifier (Arg2, Name_Depends); + + Dep_Arg := Expression (Arg2); + + if Nkind (Dep_Arg) = N_Identifier then + Dep_Id := Get_Assertion_Level (Chars (Dep_Arg)); + Check_Known_Level_Name (Dep_Id, Dep_Arg); + Add_Dependencies (Level_Id, Dep_Id); + elsif Nkind (Dep_Arg) = N_Aggregate then + Dep := First (Expressions (Dep_Arg)); + while Present (Dep) loop + Check_Valid_Level_Node (Dep); + Dep_Id := Get_Assertion_Level (Chars (Dep)); + Check_Known_Level_Name (Dep_Id, Dep); + Add_Dependencies (Level_Id, Dep_Id); + + Next (Dep); + end loop; + else + Error_Pragma_Arg + ("depends argument must be either " + & "an identifier or " + & "an aggregate of identifiers", Dep_Arg); + end if; + end if; + + -- Register the new Assertion_Level + + Insert_Assertion_Level (Level_Id); + end Assertion_Level; + ---------------------- -- Assertion_Policy -- ---------------------- @@ -14115,7 +14588,9 @@ package body Sem_Prag is -- ASSERTION_KIND => POLICY_IDENTIFIER -- {, ASSERTION_KIND => POLICY_IDENTIFIER}); - -- ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND + -- ASSERTION_KIND ::= RM_ASSERTION_KIND | + -- ID_ASSERTION_KIND | + -- LEVEL_IDENTIFIER -- RM_ASSERTION_KIND ::= Assert | -- Static_Predicate | @@ -14194,8 +14669,13 @@ package body Sem_Prag is -- Local variables + Policy_Names : constant Name_List := + (Name_Check, Name_Disable, Name_Ignore, Name_Suppressible); + Arg : Node_Id; + Id : Node_Id; Kind : Name_Id; + Level : Entity_Id; LocP : Source_Ptr; Policy : Node_Id; @@ -14222,8 +14702,7 @@ package body Sem_Prag is and then (Nkind (Arg1) /= N_Pragma_Argument_Association or else Chars (Arg1) = No_Name) then - Check_Arg_Is_One_Of (Arg1, - Name_Check, Name_Disable, Name_Ignore, Name_Suppressible); + Check_Arg_Is_One_Of (Arg1, Policy_Names); Resolve_Suppressible (Arg1); @@ -14272,15 +14751,22 @@ package body Sem_Prag is -- Check Kind and Policy have allowed forms Kind := Chars (Arg); + Id := Make_Identifier (LocP, Kind); Policy := Get_Pragma_Arg (Arg); if not Is_Valid_Assertion_Kind (Kind) then - Error_Pragma_Arg - ("invalid assertion kind for pragma%", Arg); + Set_Entity (Id, Get_Assertion_Level (Kind)); + Level := Entity (Id); + if No (Level) + or else Ekind (Level) /= E_Assertion_Level + then + Error_Pragma_Arg + ("invalid assertion kind for pragma%", + Arg); + end if; end if; - Check_Arg_Is_One_Of (Arg, - Name_Check, Name_Disable, Name_Ignore, Name_Suppressible); + Check_Arg_Is_One_Of (Arg, Policy_Names); Resolve_Suppressible (Arg); @@ -14321,7 +14807,7 @@ package body Sem_Prag is Chars => Name_Check_Policy, Pragma_Argument_Associations => New_List ( Make_Pragma_Argument_Association (LocP, - Expression => Make_Identifier (LocP, Kind)), + Expression => Id), Make_Pragma_Argument_Association (LocP, Expression => Policy)))); @@ -14864,12 +15350,10 @@ package body Sem_Prag is pragma Assert (Has_Dynamic_Predicate_Aspect (Typ)); if not Predicates_Ignored (Typ) then - Set_Is_Checked (N, True); - Set_Is_Ignored (N, False); + Mark_Is_Checked (N); else - Set_Is_Checked (N, False); - Set_Is_Ignored (N, True); + Mark_Is_Ignored (N); end if; end Handle_Dynamic_Predicate_Check; @@ -14879,11 +15363,16 @@ package body Sem_Prag is Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit + Names : constant Name_List (1 .. 3) := + (Name_Name, Name_Check, Name_Message); + + Args : Args_List (1 .. 3); + Arg_Name : Node_Id renames Args (1); + Arg_Check : Node_Id renames Args (2); + Arg_Message : Node_Id renames Args (3); + Cname : Name_Id; Eloc : Source_Ptr; - Expr : Node_Id; - Str : Node_Id; - pragma Warnings (Off, Str); -- Start of processing for Pragma_Check @@ -14897,17 +15386,12 @@ package body Sem_Prag is GNAT_Pragma; Check_At_Least_N_Arguments (2); Check_At_Most_N_Arguments (3); - Check_Optional_Identifier (Arg1, Name_Name); - Check_Optional_Identifier (Arg2, Name_Check); - if Arg_Count = 3 then - Check_Optional_Identifier (Arg3, Name_Message); - Str := Get_Pragma_Arg (Arg3); - end if; + Gather_Associations (Names, Args); - Rewrite_Assertion_Kind (Get_Pragma_Arg (Arg1)); - Check_Arg_Is_Identifier (Arg1); - Cname := Chars (Get_Pragma_Arg (Arg1)); + Rewrite_Assertion_Kind (Arg_Name); + Check_Arg_Is_Identifier (Arg_Name); + Cname := Chars (Arg_Name); -- Check forbidden name Assertions or Statement_Assertions @@ -14915,12 +15399,12 @@ package body Sem_Prag is when Name_Assertions => Error_Pragma_Arg ("""Assertions"" is not allowed as a check kind for " - & "pragma%", Arg1); + & "pragma%", Arg_Name); when Name_Statement_Assertions => Error_Pragma_Arg ("""Statement_Assertions"" is not allowed as a check kind " - & "for pragma%", Arg1); + & "for pragma%", Arg_Name); when others => null; @@ -14938,8 +15422,7 @@ package body Sem_Prag is elsif Is_Rewrite_Substitution (N) and then Nkind (Original_Node (N)) = N_Pragma then - Set_Is_Ignored (N, Is_Ignored (Original_Node (N))); - Set_Is_Checked (N, Is_Checked (Original_Node (N))); + Copy_Assertion_Policy_Attributes (N, Original_Node (N)); -- Internally added dynamic predicate checks require checking the -- applicable policy at the point of the type declaration of their @@ -14954,34 +15437,18 @@ package body Sem_Prag is -- Otherwise query the applicable policy at this point else - case Check_Kind (Cname) is - when Name_Ignore => - Set_Is_Ignored (N, True); - Set_Is_Checked (N, False); + Apply_Check_Policy (N, Get_Applicable_Policy (Cname, Empty)); - when Name_Check => - Set_Is_Ignored (N, False); - Set_Is_Checked (N, True); + -- For disable, rewrite pragma as null statement and skip + -- rest of the analysis of the pragma. - -- For disable, rewrite pragma as null statement and skip - -- rest of the analysis of the pragma. - - when Name_Disable => - Rewrite (N, Make_Null_Statement (Loc)); - Analyze (N); - raise Pragma_Exit; - - -- No other possibilities - - when others => - raise Program_Error; - end case; + if Is_Disabled (N) then + Rewrite (N, Make_Null_Statement (Loc)); + Analyze (N); + raise Pragma_Exit; + end if; end if; - -- If check kind was not Disable, then continue pragma analysis - - Expr := Get_Pragma_Arg (Arg2); - -- Mark the pragma (or, if rewritten from an aspect, the original -- aspect) as enabled. Nothing to do for an internally generated -- check for a dynamic predicate. @@ -15005,8 +15472,8 @@ package body Sem_Prag is -- expression is only evaluated if the check fails and -- Assertion_Error is to be raised. - if Arg_Count = 3 then - Preanalyze_And_Resolve (Str, Standard_String); + if Present (Arg_Message) then + Preanalyze_And_Resolve (Arg_Message, Standard_String); end if; -- Now you might think we could just do the same with the Boolean @@ -15035,14 +15502,14 @@ package body Sem_Prag is -- warning when we delete the if statement. if Expander_Active and Is_Ignored_In_Codegen (N) then - Eloc := Sloc (Expr); + Eloc := Sloc (Arg_Check); Rewrite (N, Make_If_Statement (Eloc, Condition => Make_And_Then (Eloc, Left_Opnd => Make_Identifier (Eloc, Name_False), - Right_Opnd => Expr), + Right_Opnd => Arg_Check), Then_Statements => New_List ( Make_Null_Statement (Eloc)))); @@ -15083,7 +15550,7 @@ package body Sem_Prag is else In_Assertion_Expr := In_Assertion_Expr + 1; - Analyze_And_Resolve (Expr, Any_Boolean); + Analyze_And_Resolve (Arg_Check, Any_Boolean); In_Assertion_Expr := In_Assertion_Expr - 1; end if; @@ -15157,7 +15624,90 @@ package body Sem_Prag is -- new form syntax. when Pragma_Check_Policy => Check_Policy : declare - Kind : Node_Id; + procedure Get_All_Child_Levels + (Level : Entity_Id; + Deps : in out Elist_Id); + -- Add all of the transitive children of the given Level to the + -- Deps list. + + procedure Get_All_Parent_Levels + (Level : Entity_Id; + Deps : in out Elist_Id); + -- Add all of the transitive parents of the given Level to the + -- Deps list. + + -------------------------- + -- Get_All_Child_Levels -- + -------------------------- + + procedure Get_All_Child_Levels + (Level : Entity_Id; + Deps : in out Elist_Id) + is + It : Elmt_Id; + Child_Lvl : Entity_Id; + begin + if No (Child_Levels (Level)) then + return; + end if; + + It := First_Elmt (Child_Levels (Level)); + while Present (It) loop + Child_Lvl := Node (It); + if not Contains (Deps, Child_Lvl) then + Append_New_Elmt (Child_Lvl, Deps); + Get_All_Child_Levels (Child_Lvl, Deps); + end if; + + Next_Elmt (It); + end loop; + end Get_All_Child_Levels; + + --------------------------- + -- Get_All_Parent_Levels -- + --------------------------- + + procedure Get_All_Parent_Levels + (Level : Entity_Id; + Deps : in out Elist_Id) + is + It : Elmt_Id; + D : Entity_Id; + begin + if No (Parent_Levels (Level)) then + return; + end if; + + It := First_Elmt (Parent_Levels (Level)); + while Present (It) loop + D := Node (It); + + if not Contains (Deps, D) then + Append_New_Elmt (D, Deps); + Get_All_Parent_Levels (D, Deps); + end if; + + Next_Elmt (It); + end loop; + end Get_All_Parent_Levels; + + -- Local variables + + Policy_Names : constant Name_List := + (Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore); + + Affected_Levels : Elist_Id := New_Elmt_List; + Depends_On_Static : Boolean := False; + + Kind : Node_Id; + Level : Entity_Id; + L : Entity_Id; + L_It : Elmt_Id; + L_Id : Node_Id; + New_P : Node_Id; + Policy_Nam : Name_Id; + + -- Start of processing for Pragma Check_Policy begin GNAT_Pragma; @@ -15199,15 +15749,92 @@ package body Sem_Prag is -- Check policy Check_Optional_Identifier (Arg2, Name_Policy); - Check_Arg_Is_One_Of - (Arg2, - Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore); + Check_Arg_Is_One_Of (Arg2, Policy_Names); + + Policy_Nam := Chars (Get_Pragma_Arg (Arg2)); -- And chain pragma on the Check_Policy_List for search Set_Next_Pragma (N, Opt.Check_Policy_List); Opt.Check_Policy_List := N; + -- For Assertion_Levels create new policies for all of the + -- level dependencies. + + if Present (Entity (Kind)) + and then Ekind (Entity (Kind)) = E_Assertion_Level + then + Level := Entity (Kind); + + Depends_On_Static := + Depends_On_Level (Level, Standard_Level_Static); + + if Policy_Nam in Name_On | Name_Check then + if Level = Standard_Level_Static then + Error_Pragma_Arg + ("policy for `Static` cannot be changed to `Check`", + Arg1); + elsif Depends_On_Static then + Error_Pragma_Arg + ("Policy for a level that depends on `Static` " + & "cannot be changed to `Check`", + Arg1); + end if; + end if; + + if Policy_Nam in Name_Off | Name_Ignore + and then Level = Standard_Level_Runtime + then + Error_Pragma_Arg + ("policy for `Runtime` cannot be changed to `Ignore`", + Arg1); + end if; + + -- For Assertion_Levels create new policyies for all of the + -- level dependencies. + + if Policy_Nam in Name_On | Name_Check then + + -- Activating a level activates all levels that it + -- depends on (Parent_Levels). + + Get_All_Parent_Levels (Level, Affected_Levels); + elsif Policy_Nam in Name_Off | Name_Ignore then + + -- Deactivating a level deactivates all levels that + -- depend on it (Child_Levels) + + Get_All_Child_Levels (Level, Affected_Levels); + end if; + + L_It := First_Elmt (Affected_Levels); + while Present (L_It) loop + L := Node (L_It); + L_Id := Make_Identifier (Sloc (Arg1), Chars (L)); + Set_Entity (L_Id, L); + New_P := + Make_Pragma (Sloc (N), + Chars => Name_Check_Policy, + Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Sloc (Arg1), + Expression => L_Id), + Make_Pragma_Argument_Association (Sloc (Arg2), + Expression => + New_Copy_Tree (Get_Pragma_Arg (Arg2))))); + + -- We have collected the unique list of all transitive + -- Parent_Levels or Child_Levels. Avoid calculating + -- them again. + + Set_Analyzed (New_P); + + Set_Next_Pragma (New_P, Opt.Check_Policy_List); + Opt.Check_Policy_List := New_P; + + Next_Elmt (L_It); + end loop; + end if; + -- For the new syntax, what we do is to convert each argument to -- an old syntax equivalent. We do that because we want to chain -- old style Check_Policy pragmas for the search (we don't want @@ -15218,8 +15845,6 @@ package body Sem_Prag is Arg : Node_Id; Argx : Node_Id; LocP : Source_Ptr; - New_P : Node_Id; - begin Arg := Arg1; while Present (Arg) loop @@ -16362,6 +16987,21 @@ package body Sem_Prag is Check_No_Identifiers; Check_At_Most_N_Arguments (2); -- Accounts for implicit type arg + -- The value "null" cannot be associated with an assertion level + -- as it has no runtime semantics. + + if Present (Pragma_Ghost_Assertion_Level (N)) + and then Pragma_Ghost_Assertion_Level (N) + /= Standard_Level_Default + and then Present (Arg1) + and then Nkind (Get_Pragma_Arg (Arg1)) = N_Null + then + Error_Pragma_Arg + ("null argument cannot be used together " + & "with assertion levels", + Arg1); + end if; + Typ := Empty; Stmt := Prev (N); while Present (Stmt) loop @@ -16369,7 +17009,9 @@ package body Sem_Prag is -- Skip prior pragmas, but check for duplicates if Nkind (Stmt) = N_Pragma then - if Pragma_Name (Stmt) = Pname then + if Pragma_Name (Stmt) = Pname + and then not From_Same_Pragma (N, Stmt) + then Duplication_Error (Prag => N, Prev => Stmt); @@ -18020,7 +18662,8 @@ package body Sem_Prag is GNAT_Pragma; Check_Arg_Count (1); Check_No_Identifiers; - Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off, Name_All_Extensions); + Check_Arg_Is_One_Of + (Arg1, (Name_On, Name_Off, Name_All_Extensions)); if Chars (Get_Pragma_Arg (Arg1)) = Name_On then Ada_Version := Ada_With_Core_Extensions; @@ -18225,7 +18868,7 @@ package body Sem_Prag is if Arg_Count = 2 then Check_Arg_Is_One_Of - (Arg2, Name_As_Is, Name_Uppercase, Name_Lowercase); + (Arg2, (Name_As_Is, Name_Uppercase, Name_Lowercase)); case Chars (Get_Pragma_Arg (Arg2)) is when Name_As_Is => @@ -18470,12 +19113,15 @@ package body Sem_Prag is -- Ghost -- ----------- - -- pragma Ghost [ (static_boolean_EXPRESSION) ]; + -- pragma Ghost [ (static_boolean_EXPRESSION + -- | Assertion_Level) ]; when Pragma_Ghost => Ghost : declare Context : Node_Id; Expr : Node_Id; Id : Entity_Id; + Is_Ghost : Boolean := True; + Level : Entity_Id; Orig_Stmt : Node_Id; Prev_Id : Entity_Id; Stmt : Node_Id; @@ -18699,30 +19345,48 @@ package body Sem_Prag is if Present (Arg1) then Expr := Get_Pragma_Arg (Arg1); - Analyze_And_Resolve (Expr, Standard_Boolean); - - if Is_OK_Static_Expression (Expr) then - - -- "Ghostness" cannot be turned off once enabled within a - -- region (SPARK RM 6.9(6)). + if Nkind (Expr) /= N_Identifier + or else No (Get_Assertion_Level (Chars (Expr))) + then + Analyze_And_Resolve (Expr, Standard_Boolean); - if Is_False (Expr_Value (Expr)) - and then Ghost_Config.Ghost_Mode > None - then - Error_Pragma - ("pragma % with value False cannot appear in enabled " - & "ghost region"); + if not Is_OK_Static_Expression (Expr) then + Error_Pragma_Arg + ("expression of pragma % must be static", Expr); end if; - -- Otherwise the expression is not static + if Is_False (Expr_Value (Expr)) then + Is_Ghost := False; - else - Error_Pragma_Arg - ("expression of pragma % must be static", Expr); + -- "Ghostness" cannot be turned off once enabled within a + -- region (SPARK RM 6.9(6)). + + if Ghost_Config.Ghost_Mode > None then + Error_Pragma + ("pragma % with value False cannot appear in enabled" + & " ghost region"); + end if; + end if; end if; end if; - Set_Is_Ghost_Entity (Id); + Level := Assertion_Level_From_Arg (Arg1); + + -- Associate the assertion level before determing the kind of + -- ghost entity we should mark the entity as. + + Set_Ghost_Assertion_Level (Id, Level); + + -- Store it on the pragma node as well + + Set_Pragma_Ghost_Assertion_Level (N, Level); + + -- Mark it as a Ghost entity unless it was explicitly marked with + -- pragma Ghost (False). + + if Is_Ghost then + Set_Is_Ghost_Entity (Id); + end if; end Ghost; ------------ @@ -18943,17 +19607,17 @@ package body Sem_Prag is Proc_Id : Entity_Id; Typ : Entity_Id; + Impl_Names : constant Name_List := (Name_By_Any, + Name_By_Entry, + Name_By_Protected_Procedure, + Name_Optional); begin Ada_2012_Pragma; Check_Arg_Count (2); Check_No_Identifiers; Check_Arg_Is_Identifier (Arg1); Check_Arg_Is_Local_Name (Arg1); - Check_Arg_Is_One_Of (Arg2, - Name_By_Any, - Name_By_Entry, - Name_By_Protected_Procedure, - Name_Optional); + Check_Arg_Is_One_Of (Arg2, Impl_Names); -- Extract the name of the local procedure @@ -20875,6 +21539,11 @@ package body Sem_Prag is when Pragma_Loop_Optimize => Loop_Optimize : declare Hint : Node_Id; + Hint_Names : constant Name_List := (Name_Ivdep, + Name_No_Unroll, + Name_Unroll, + Name_No_Vector, + Name_Vector); begin GNAT_Pragma; Check_At_Least_N_Arguments (1); @@ -20882,11 +21551,7 @@ package body Sem_Prag is Hint := First (Pragma_Argument_Associations (N)); while Present (Hint) loop - Check_Arg_Is_One_Of (Hint, Name_Ivdep, - Name_No_Unroll, - Name_Unroll, - Name_No_Vector, - Name_Vector); + Check_Arg_Is_One_Of (Hint, Hint_Names); Next (Hint); end loop; @@ -22238,7 +22903,7 @@ package body Sem_Prag is when Pragma_Optimize => Check_No_Identifiers; Check_Arg_Count (1); - Check_Arg_Is_One_Of (Arg1, Name_Time, Name_Space, Name_Off); + Check_Arg_Is_One_Of (Arg1, (Name_Time, Name_Space, Name_Off)); ------------------------ -- Optimize_Alignment -- @@ -23158,12 +23823,18 @@ package body Sem_Prag is -- removal of ignored Ghost code. if From_Aspect_Specification (N) - and then Get_Aspect_Id - (Chars (Identifier (Corresponding_Aspect (N)))) - = Aspect_Ghost_Predicate + and then Get_Aspect_Id (Corresponding_Aspect (N)) + = Aspect_Ghost_Predicate then - Mark_Ghost_Pragma - (N, Name_To_Ghost_Mode (Policy_In_Effect (Name_Ghost))); + -- For Ghost_Predicate we have already analyzed the applicable + -- ghost policy already and set the policy using Is_Checked and + -- Is_Ignored. + + if Is_Ignored (N) then + Mark_Ghost_Pragma (N, Opt.Ignore); + else + Mark_Ghost_Pragma (N, Opt.Check); + end if; else Mark_Ghost_Pragma (N, Typ); end if; @@ -25675,7 +26346,7 @@ package body Sem_Prag is -- Check the legality of the mode (no argument = ON) if Arg_Count = 1 then - Check_Arg_Is_One_Of (Arg1, Name_Auto, Name_On, Name_Off); + Check_Arg_Is_One_Of (Arg1, (Name_Auto, Name_On, Name_Off)); Mode := Chars (Get_Pragma_Arg (Arg1)); else Mode := Name_On; @@ -27145,7 +27816,7 @@ package body Sem_Prag is GNAT_Pragma; Check_Arg_Count (1); Check_No_Identifiers; - Check_Arg_Is_One_Of (Arg1, Name_Error, Name_Warn, Name_Allow); + Check_Arg_Is_One_Of (Arg1, (Name_Error, Name_Warn, Name_Allow)); -- Suppress/Unsuppress can appear as a configuration pragma, or in -- a declarative part or a package spec. @@ -30875,6 +31546,9 @@ package body Sem_Prag is -- A list that contains all refined states processed so far. The list is -- used to detect duplicate refinements. + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; + -- Ghost configuration before starting to process this pragma + procedure Analyze_Refinement_Clause (Clause : Node_Id); -- Perform full analysis of a single refinement clause @@ -31634,6 +32308,10 @@ package body Sem_Prag is return; end if; + -- Get the Ghost context from the pragma before analyzing its parts + + Set_Ghost_Mode (N); + -- Save the scenario for examination by the ABE Processing phase Record_Elaboration_Scenario (N); @@ -31677,6 +32355,8 @@ package body Sem_Prag is Report_Unrefined_States (Available_States); Set_Is_Analyzed_Pragma (N); + + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Refined_State_In_Decl_Part; --------------------------------------------- @@ -32002,6 +32682,30 @@ package body Sem_Prag is return False; end Appears_In; + ------------------------ + -- Apply_Check_Policy -- + ------------------------ + + procedure Apply_Check_Policy (N : Node_Id; Policy : Name_Id) is + begin + case Policy is + when Name_Ignore | Name_Off => + Mark_Is_Ignored (N); + + when Name_Check | Name_On => + Mark_Is_Checked (N); + + when Name_Disable => + Mark_Is_Disabled (N); + + -- That should be exhaustive, the null here is a defence + -- against a malformed tree from previous errors. + + when others => + null; + end case; + end Apply_Check_Policy; + ----------------------------------- -- Build_Pragma_Check_Equivalent -- ----------------------------------- @@ -32142,84 +32846,18 @@ package body Sem_Prag is -- Check_Applicable_Policy -- ----------------------------- - procedure Check_Applicable_Policy (N : Node_Id) is - PP : Node_Id; - Policy : Name_Id; - - Ename : constant Name_Id := Original_Aspect_Pragma_Name (N); + procedure Check_Applicable_Policy (N : Node_Id; Level : Entity_Id := Empty) + is + Nam : constant Name_Id := Original_Aspect_Pragma_Name (N); begin -- No effect if not valid assertion kind name - if not Is_Valid_Assertion_Kind (Ename) then + if not Is_Valid_Assertion_Kind (Nam) then return; end if; - -- Loop through entries in check policy list - - PP := Opt.Check_Policy_List; - while Present (PP) loop - declare - PPA : constant List_Id := Pragma_Argument_Associations (PP); - Pnm : constant Name_Id := Chars (Get_Pragma_Arg (First (PPA))); - - begin - if Ename = Pnm - or else Pnm = Name_Assertion - or else (Pnm = Name_Statement_Assertions - and then Ename in Name_Assert - | Name_Assert_And_Cut - | Name_Assume - | Name_Loop_Invariant - | Name_Loop_Variant) - then - Policy := Chars (Get_Pragma_Arg (Last (PPA))); - - case Policy is - when Name_Ignore - | Name_Off - => - Set_Is_Checked (N, False); - Set_Is_Ignored (N, True); - - when Name_Check - | Name_On - => - Set_Is_Checked (N, True); - Set_Is_Ignored (N, False); - - when Name_Disable => - Set_Is_Ignored (N, True); - Set_Is_Checked (N, False); - Set_Is_Disabled (N, True); - - -- That should be exhaustive, the null here is a defence - -- against a malformed tree from previous errors. - - when others => - null; - end case; - - return; - end if; - - PP := Next_Pragma (PP); - end; - end loop; - - -- If there are no specific entries that matched, then we let the - -- setting of assertions govern. Note that this provides the needed - -- compatibility with the RM for the cases of assertion, invariant, - -- precondition, predicate, and postcondition. Note also that - -- Assertions_Enabled is forced in CodePeer mode and GNATprove mode. - - if Assertions_Enabled then - Set_Is_Checked (N, True); - Set_Is_Ignored (N, False); - else - Set_Is_Checked (N, False); - Set_Is_Ignored (N, True); - end if; + Apply_Check_Policy (N, Get_Applicable_Policy (Nam, Level)); end Check_Applicable_Policy; ------------------------------- @@ -32267,69 +32905,6 @@ package body Sem_Prag is Item); end Check_External_Properties; - ---------------- - -- Check_Kind -- - ---------------- - - function Check_Kind (Nam : Name_Id) return Name_Id is - PP : Node_Id; - - begin - -- Loop through entries in check policy list - - PP := Opt.Check_Policy_List; - while Present (PP) loop - declare - PPA : constant List_Id := Pragma_Argument_Associations (PP); - Pnm : constant Name_Id := Chars (Get_Pragma_Arg (First (PPA))); - - begin - if Nam = Pnm - or else (Pnm = Name_Assertion - and then Is_Valid_Assertion_Kind (Nam)) - or else (Pnm = Name_Statement_Assertions - and then Nam in Name_Assert - | Name_Assert_And_Cut - | Name_Assume - | Name_Loop_Invariant - | Name_Loop_Variant) - then - case Chars (Get_Pragma_Arg (Last (PPA))) is - when Name_Check - | Name_On - => - return Name_Check; - - when Name_Ignore - | Name_Off - => - return Name_Ignore; - - when Name_Disable => - return Name_Disable; - - when others => - raise Program_Error; - end case; - - else - PP := Next_Pragma (PP); - end if; - end; - end loop; - - -- If there are no specific entries that matched, then we let the - -- setting of assertions govern. Note that this provides the needed - -- compatibility with the RM for the cases of assertion, invariant, - -- precondition, predicate, and postcondition. - - if Assertions_Enabled then - return Name_Check; - else - return Name_Ignore; - end if; - end Check_Kind; - --------------------------- -- Check_Missing_Part_Of -- --------------------------- @@ -33047,6 +33622,21 @@ package body Sem_Prag is end if; end Duplication_Error; + -------------------------- + -- Find_Assertion_Level -- + -------------------------- + + function Find_Assertion_Level (Nam : Name_Id) return Entity_Id is + begin + for J in Assertion_Levels.First .. Assertion_Levels.Last loop + if Chars (Assertion_Levels.Table (J)) = Nam then + return Assertion_Levels.Table (J); + end if; + end loop; + + return Empty; + end Find_Assertion_Level; + ------------------------------ -- Find_Encapsulating_State -- ------------------------------ @@ -33195,10 +33785,9 @@ package body Sem_Prag is if Nkind (Stmt) = N_Pragma then if Do_Checks and then Original_Aspect_Pragma_Name (Stmt) = Prag_Nam + and then not From_Same_Pragma (Prag, Stmt) then - Duplication_Error - (Prag => Prag, - Prev => Stmt); + Duplication_Error (Prag => Prag, Prev => Stmt); end if; -- Emit an error when a refinement pragma appears on an expression @@ -33361,10 +33950,11 @@ package body Sem_Prag is -- Skip prior pragmas, but check for duplicates if Nkind (Stmt) = N_Pragma then - if Do_Checks and then Pragma_Name (Stmt) = Prag_Nam then - Duplication_Error - (Prag => Prag, - Prev => Stmt); + if Do_Checks + and then Pragma_Name (Stmt) = Prag_Nam + and then not From_Same_Pragma (Prag, Stmt) + then + Duplication_Error (Prag => Prag, Prev => Stmt); end if; -- Skip internally generated code @@ -33430,6 +34020,80 @@ package body Sem_Prag is end if; end Find_Related_Package_Or_Body; + --------------------------- + -- Get_Applicable_Policy -- + --------------------------- + + function Get_Applicable_Policy + (Nam : Name_Id; Level : Entity_Id) return Name_Id + is + function Is_Statement_Assertion (Nam : Name_Id) return Boolean + is (Nam + in Name_Assert + | Name_Assert_And_Cut + | Name_Assume + | Name_Loop_Invariant + | Name_Loop_Variant); + + -- Local variables + + Assocs : List_Id; + P_Arg : Node_Id; + P_Nam : Name_Id; + Policy_Prag : Node_Id; + + -- Start of processing for Get_Applicable_Policy + + begin + -- Runtime level should always be checked irregardless of other + -- policies that are applied. + + if Level = Standard_Level_Runtime then + return Name_Check; + + -- Static level or levels that depend on Static should never be + -- checked irregardless of other policies that are applied. + + elsif Level = Standard_Level_Static + or else Depends_On_Level (Level, Standard_Level_Static) + then + return Name_Ignore; + end if; + + -- Loop through entries in check policy list + + Policy_Prag := Opt.Check_Policy_List; + while Present (Policy_Prag) loop + Assocs := Pragma_Argument_Associations (Policy_Prag); + P_Arg := Get_Pragma_Arg (First (Assocs)); + P_Nam := Chars (P_Arg); + + if P_Nam = Nam + or else P_Nam = Name_Assertion + or else (P_Nam = Name_Statement_Assertions + and then Is_Statement_Assertion (Nam)) + or else (Present (Level) and then Entity (P_Arg) = Level) + then + return Chars (Get_Pragma_Arg (Last (Assocs))); + end if; + + Policy_Prag := Next_Pragma (Policy_Prag); + end loop; + + -- If there are no specific entries that matched, then we let the + -- setting of assertions govern. Note that this provides the + -- needed compatibility with the RM for the cases of assertion, + -- invariant, precondition, predicate, and postcondition. Note + -- also that Assertions_Enabled is forced in CodePeer mode and + -- GNATprove mode. + + if Assertions_Enabled then + return Name_Check; + else + return Name_Ignore; + end if; + end Get_Applicable_Policy; + ------------------ -- Get_Argument -- ------------------ @@ -33462,6 +34126,19 @@ package body Sem_Prag is end if; end Get_Argument; + ------------------------- + -- Get_Assertion_Level -- + ------------------------- + + function Get_Assertion_Level (Nam : Name_Id) return Entity_Id is + begin + if Nam = No_Name then + return Empty; + end if; + + return Find_Assertion_Level (Nam); + end Get_Assertion_Level; + ------------------------- -- Get_Base_Subprogram -- ------------------------- @@ -33602,6 +34279,7 @@ package body Sem_Prag is begin Externals.Init; Compile_Time_Warnings_Errors.Init; + Assertion_Levels.Init; end Initialize; -------- @@ -33613,6 +34291,79 @@ package body Sem_Prag is Dummy := Dummy + 1; end ip; + ---------------------------- + -- Insert_Assertion_Level -- + ---------------------------- + + procedure Insert_Assertion_Level (Level : Entity_Id) is + Nam : constant Name_Id := Chars (Level); + + Dupl : constant Entity_Id := Find_Assertion_Level (Nam); + + function Same_Dependencies (Self, Other : Entity_Id) return Boolean; + -- Check that both levels have the same number of dependencies and the + -- names of the dependencies match. + + ----------------------- + -- Same_Dependencies -- + ----------------------- + + function Same_Dependencies (Self, Other : Entity_Id) return Boolean is + Other_El : Elmt_Id; + Other_Level : Entity_Id; + Self_El : Elmt_Id; + Self_Level : Entity_Id; + + begin + pragma Assert (Ekind (Self) = E_Assertion_Level); + pragma Assert (Ekind (Other) = E_Assertion_Level); + + if List_Length (Parent_Levels (Self)) + /= List_Length (Parent_Levels (Other)) + then + return False; + end if; + + if No (Parent_Levels (Self)) then + return True; + end if; + + -- Check that dependencies match. + -- Note that we are checking for positional and element matching. + -- The positional part could be relaxed. + + Self_El := First_Elmt (Parent_Levels (Self)); + Other_El := First_Elmt (Parent_Levels (Other)); + while Present (Self_El) loop + Self_Level := Node (Self_El); + Other_Level := Node (Other_El); + + if Chars (Self_Level) /= Chars (Other_Level) then + return False; + end if; + + Next_Elmt (Self_El); + Next_Elmt (Other_El); + end loop; + + return True; + end Same_Dependencies; + + -- Start of processing for Insert_Assertion_Level + + begin + if No (Dupl) then + Assertion_Levels.Append (Level); + else + if not Same_Dependencies (Level, Dupl) then + Error_Msg_N + ("conflicting Assertion_Level definition for &", Level); + Error_Msg_Sloc := Sloc (Dupl); + Error_Msg_NE ("\differs from existing definition #", Level, Dupl); + end if; + end if; + end Insert_Assertion_Level; + ----------------------------- -- Is_Config_Static_String -- ----------------------------- @@ -33753,6 +34504,7 @@ package body Sem_Prag is Pragma_Annotate => 93, Pragma_Assert => -1, Pragma_Assert_And_Cut => -1, + Pragma_Assertion_Level => 0, Pragma_Assertion_Policy => 0, Pragma_Assume => -1, Pragma_Assume_No_Invalid_Values => 0, @@ -34207,6 +34959,15 @@ package body Sem_Prag is end case; end Is_Valid_Assertion_Kind; + ------------------------------ + -- Is_Valid_Assertion_Level -- + ------------------------------ + + function Is_Valid_Assertion_Level (Nam : Name_Id) return Boolean is + begin + return Present (Get_Assertion_Level (Nam)); + end Is_Valid_Assertion_Level; + -------------------------------------- -- Process_Compilation_Unit_Pragmas -- -------------------------------------- @@ -34375,6 +35136,37 @@ package body Sem_Prag is end if; end Validate_Compile_Time_Warning_Or_Error; + --------------------- + -- Mark_Is_Checked -- + --------------------- + + procedure Mark_Is_Checked (N : Node_Id) is + begin + Set_Is_Checked (N, True); + Set_Is_Ignored (N, False); + end Mark_Is_Checked; + + ---------------------- + -- Mark_Is_Disabled -- + ---------------------- + + procedure Mark_Is_Disabled (N : Node_Id) is + begin + Set_Is_Ignored (N, True); + Set_Is_Checked (N, False); + Set_Is_Disabled (N, True); + end Mark_Is_Disabled; + + --------------------- + -- Mark_Is_Ignored -- + --------------------- + + procedure Mark_Is_Ignored (N : Node_Id) is + begin + Set_Is_Checked (N, False); + Set_Is_Ignored (N, True); + end Mark_Is_Ignored; + ------------------------------------ -- Record_Possible_Body_Reference -- ------------------------------------ diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 9228a8774a5..1657d6db691 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -253,6 +253,15 @@ package Sem_Prag is (Pragma_Extensions_Visible => True, others => False); + function Find_Assertion_Level (Nam : Name_Id) return Entity_Id; + -- Find an existing definition with the given name that has been inserted + -- into the Assertion_Levels table. + + procedure Insert_Assertion_Level (Level : Entity_Id); + -- Insert a new level into the Assertion_Levels table. If there is already + -- an entry with the same name check that it has the same dependencies as + -- the level you are trying to insert. Raises an error otherwise. + ----------------- -- Subprograms -- ----------------- @@ -377,7 +386,7 @@ package Sem_Prag is -- in fact of the same kind as the source pragma Prag. This is used -- in GNATprove_Mode to generate the inherited pre- and postconditions. - procedure Check_Applicable_Policy (N : Node_Id); + procedure Check_Applicable_Policy (N : Node_Id; Level : Entity_Id := Empty); -- N is either an N_Aspect or an N_Pragma node. There are two cases. If -- the name of the aspect or pragma is not one of those recognized as -- an assertion kind by an Assertion_Policy pragma, then the call has @@ -410,25 +419,6 @@ package Sem_Prag is -- is the related variable or state. Ensure legality of the combination and -- issue an error for an illegal combination. - function Check_Kind (Nam : Name_Id) return Name_Id; - -- This function is used in connection with pragmas Assert, Check, - -- and assertion aspects and pragmas, to determine if Check pragmas - -- (or corresponding assertion aspects or pragmas) are currently active - -- as determined by the presence of -gnata on the command line (which - -- sets the default), and the appearance of pragmas Check_Policy and - -- Assertion_Policy as configuration pragmas either in a configuration - -- pragma file, or at the start of the current unit, or locally given - -- Check_Policy and Assertion_Policy pragmas that are currently active. - -- - -- The value returned is one of the names Check, Ignore, Disable (On - -- returns Check, and Off returns Ignore). - -- - -- Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class, - -- and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost, - -- Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre, - -- _Post, _Invariant, or _Type_Invariant, which are special names used - -- in identifiers to represent these attribute references. - procedure Check_Missing_Part_Of (Item_Id : Entity_Id); -- Determine whether the placement within the state space of an abstract -- state, variable or package instantiation denoted by Item_Id requires the @@ -533,6 +523,9 @@ package Sem_Prag is -- Context denotes the entity of the function, package or procedure where -- Prag resides. + function Get_Assertion_Level (Nam : Name_Id) return Entity_Id; + -- Returns the entity of a known Assertion_Level name + function Get_SPARK_Mode_From_Annotation (N : Node_Id) return SPARK_Mode_Type; -- Given an aspect or pragma SPARK_Mode node, return corresponding mode id @@ -599,6 +592,10 @@ package Sem_Prag is -- Name_uInvariant, and Name_uType_Invariant (_Pre, _Post, _Invariant, -- and _Type_Invariant). + function Is_Valid_Assertion_Level (Nam : Name_Id) return Boolean; + -- Return True if Nam is one of the Assertion_Levels declared in the + -- current context. + procedure Process_Compilation_Unit_Pragmas (N : Node_Id); -- Called at the start of processing compilation unit N to deal with any -- special issues regarding pragmas. In particular, we have to deal with diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index d19b3b95622..1e855150673 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -2016,7 +2016,7 @@ package body Sem_Util is -- Elaboration entity is never a ghost object, regardless of the context -- in which this routine is called. - Install_Ghost_Region (None, N); + Install_Ghost_Region (None, N, Empty); -- Here we need the elaboration entity @@ -6202,6 +6202,18 @@ package body Sem_Util is end if; end Conditional_Delay; + -------------------------------------- + -- Copy_Assertion_Policy_Attributes -- + -------------------------------------- + + procedure Copy_Assertion_Policy_Attributes (New_Prag, Old_Prag : Node_Id) is + begin + Set_Is_Checked (New_Prag, Is_Checked (Old_Prag)); + Set_Is_Ignored (New_Prag, Is_Ignored (Old_Prag)); + Set_Pragma_Ghost_Assertion_Level + (New_Prag, Pragma_Ghost_Assertion_Level (Old_Prag)); + end Copy_Assertion_Policy_Attributes; + ------------------------- -- Copy_Component_List -- ------------------------- @@ -6316,6 +6328,7 @@ package body Sem_Util is Def_Id : Node_Id; Formal_Spec : Node_Id; Result : Node_Id; + Level : Entity_Id; begin -- The structure of the original tree must be replicated without any @@ -6334,6 +6347,7 @@ package body Sem_Util is -- Create a new entity for the defining unit name Def_Id := Defining_Unit_Name (Result); + Level := Ghost_Assertion_Level (Def_Id); case Nkind (Def_Id) is when N_Defining_Identifier => @@ -6344,6 +6358,10 @@ package body Sem_Util is when others => raise Program_Error; end case; + -- Copy the relevant Ghost Assertion_Level + + Set_Ghost_Assertion_Level (Def_Id, Level); + Set_Defining_Unit_Name (Result, Def_Id); -- Create new entities for the formal parameters @@ -7199,6 +7217,42 @@ package body Sem_Util is return Is_Variable (N) and then Paren_Count (N) = 0; end Denotes_Variable; + ---------------------- + -- Depends_On_Level -- + ---------------------- + + function Depends_On_Level + (Self : Entity_Id; Other : Entity_Id) return Boolean + is + Elm : Elmt_Id; + Dep : Entity_Id; + begin + if No (Self) then + return False; + elsif No (Other) then + return False; + end if; + + pragma Assert (Ekind (Self) = E_Assertion_Level); + pragma Assert (Ekind (Other) = E_Assertion_Level); + + if No (Parent_Levels (Self)) then + return False; + end if; + + Elm := First_Elmt (Parent_Levels (Self)); + while Present (Elm) loop + Dep := Node (Elm); + if Dep = Other or else Depends_On_Level (Dep, Other) then + return True; + end if; + + Next_Elmt (Elm); + end loop; + + return False; + end Depends_On_Level; + ----------------------------- -- Depends_On_Discriminant -- ----------------------------- @@ -9642,6 +9696,35 @@ package body Sem_Util is and then In_Open_Scopes (Scope (Pack)); end From_Nested_Package; + ---------------------- + -- From_Same_Aspect -- + ---------------------- + + function From_Same_Aspect (Self, Other : Node_Id) return Boolean is + begin + return + Present (Original_Aspect (Self)) + and then Present (Original_Aspect (Other)) + and then Original_Aspect (Self) = Original_Aspect (Other); + end From_Same_Aspect; + + ---------------------- + -- From_Same_Pragma -- + ---------------------- + + function From_Same_Pragma (Self, Other : Node_Id) return Boolean is + begin + return + (Present (Original_Pragma (Self)) + and then Present (Original_Pragma (Other)) + and then Original_Pragma (Self) = Original_Pragma (Other)) + or else (From_Aspect_Specification (Self) + and then From_Aspect_Specification (Other) + and then From_Same_Aspect + (Corresponding_Aspect (Self), + Corresponding_Aspect (Other))); + end From_Same_Pragma; + ----------------------- -- Gather_Components -- ----------------------- @@ -11088,6 +11171,10 @@ package body Sem_Util is if Is_Entity_Name (Subp) then Subp_Id := Entity (Subp); + if No (Subp_Id) then + return Empty; + end if; + if Ekind (Subp_Id) = E_Access_Subprogram_Type then Subp_Id := Directly_Designated_Type (Subp_Id); end if; @@ -11216,6 +11303,46 @@ package body Sem_Util is end if; end Get_Views; + ---------------------------------- + -- Has_Assertion_Level_Argument -- + ---------------------------------- + + function Has_Assertion_Level_Argument (N : Node_Id) return Boolean is + Assocs : List_Id; + Assoc : Node_Id; + Choice : Node_Id; + begin + if Nkind (N) = N_Aspect_Specification then + if Nkind (Expression (N)) /= N_Aggregate then + return False; + end if; + + Assocs := Component_Associations (Expression (N)); + + if No (Assocs) then + return False; + end if; + + Assoc := First (Assocs); + Choice := First (Choices (Assoc)); + + if Nkind (Choice) = N_Identifier then + return Present (Get_Assertion_Level (Chars (Choice))); + end if; + + return False; + else + pragma Assert (Nkind (N) = N_Pragma); + Assocs := Pragma_Argument_Associations (N); + Assoc := First (Assocs); + if Present (Assoc) and then Chars (Assoc) /= No_Name then + return Present (Get_Assertion_Level (Chars (Assoc))); + end if; + + return False; + end if; + end Has_Assertion_Level_Argument; + ------------------------------ -- Has_Compatible_Alignment -- ------------------------------ @@ -26405,7 +26532,10 @@ package body Sem_Util is -- Policy_In_Effect -- ---------------------- - function Policy_In_Effect (Policy : Name_Id) return Name_Id is + function Policy_In_Effect + (Policy : Name_Id; + Level : Name_Id := No_Name) return Name_Id + is function Policy_In_List (List : Node_Id) return Name_Id; -- Determine the mode of a policy in a N_Pragma list @@ -26430,7 +26560,7 @@ package body Sem_Util is -- The current Check_Policy pragma matches the requested policy or -- appears in the single argument form (Assertion, policy_id). - if Chars (Arg1) in Name_Assertion | Policy then + if Chars (Arg1) in Name_Assertion | Policy | Level then return Chars (Arg2); end if; @@ -26451,6 +26581,12 @@ package body Sem_Util is raise Program_Error; end if; + if Present (Level) + and then not Is_Valid_Assertion_Level (Level) + then + raise Program_Error; + end if; + -- Inspect all policy pragmas that appear within scopes (if any) Kind := Policy_In_List (Check_Policy_List); diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 47fcc7d14eb..a1d4ae0a897 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -560,6 +560,10 @@ package Sem_Util is -- of Old_Ent is set and Old_Ent has not yet been Frozen (i.e. Is_Frozen is -- False). + procedure Copy_Assertion_Policy_Attributes (New_Prag, Old_Prag : Node_Id); + -- Copy Is_Checked, Is_Ignored and Ghost_Assertion_Level attributes from + -- Old_Node. + function Copy_Component_List (R_Typ : Entity_Id; Loc : Source_Ptr) return List_Id; @@ -707,6 +711,11 @@ package Sem_Util is function Denotes_Variable (N : Node_Id) return Boolean; -- Returns True if node N denotes a single variable without parentheses + function Depends_On_Level + (Self : Entity_Id; Other : Entity_Id) return Boolean; + -- Check if Assertion_Level Self depends on the Assertion_Level Other + -- either directly or transitively. + function Depends_On_Discriminant (N : Node_Id) return Boolean; -- Returns True if N denotes a discriminant or if N is a range, a subtype -- indication or a scalar subtype where one of the bounds is a @@ -1055,6 +1064,13 @@ package Sem_Util is -- to entities local to the nested package. In that case the package must -- be installed on the scope stack to prevent spurious visibility errors. + function From_Same_Aspect (Self, Other : Node_Id) return Boolean; + -- True if aspects Self and Other have the same Orginal_Aspect. + + function From_Same_Pragma (Self, Other : Node_Id) return Boolean; + -- True if pragmas Self and Other have the same Original Pragma or + -- they are from the same aspect. + procedure Gather_Components (Typ : Entity_Id; Comp_List : Node_Id; @@ -1343,6 +1359,10 @@ package Sem_Util is -- Result of Has_Compatible_Alignment test, description found below. Note -- that the values are arranged in increasing order of problematicness. + function Has_Assertion_Level_Argument (N : Node_Id) return Boolean; + -- Returns true if the first argument of a pragma or an aspect is using + -- an Assertion_Level association. + function Has_Compatible_Alignment (Obj : Entity_Id; Expr : Node_Id; @@ -2259,6 +2279,11 @@ package Sem_Util is -- legal. They will need to be checked again after subprogram call has -- been resolved. + function Is_Same_Or_Depends_On_Level + (Self : Entity_Id; Other : Entity_Id) return Boolean + is (Self = Other or else Depends_On_Level (Self, Other)); + -- Check if Assertion_Level Self is or depends on the Assertion_Level Other + function Is_Package_Contract_Annotation (Item : Node_Id) return Boolean; -- Determine whether aspect specification or pragma Item is one of the -- following package contract annotations: @@ -2913,7 +2938,10 @@ package Sem_Util is -- of the corresponding formal entity, otherwise returns Empty. Also -- handles the case of references to renamings of formals. - function Policy_In_Effect (Policy : Name_Id) return Name_Id; + function Policy_In_Effect + (Policy : Name_Id; + Level : Name_Id := No_Name) + return Name_Id; -- Given a policy, return the policy identifier associated with it. If no -- such policy is in effect, the value returned is No_Name. diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 3d11d5c5aa6..eb9529f52ce 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -798,6 +798,12 @@ package Sinfo is -- ancestor of the type of the aggregate in a generic context, if any, -- when the type is a derived tagged type. Otherwise Empty. + -- Aspect_Ghost_Assertion_Level + -- Assertion_Level that was originally used in the assertion level + -- associations of its arguments. These aspects are transformed to new + -- aspects with the associated arguments and the original assertion + -- level is stored in this attribute. + -- Aspect_On_Partial_View -- Present on an N_Aspect_Specification node. For an aspect that applies -- to a type entity, indicates whether the specification appears on the @@ -2122,6 +2128,12 @@ package Sinfo is -- indication carries a null-exclusion indicator, which is distinct from -- the null-exclusion indicator that may precede the access keyword. + -- Original_Pragma + -- When aspects with assertion level associations are transformed in to + -- individual aspects without the assertion level we store the original + -- aspect in this attribute. This is used to avoid duplicate detection on + -- these aspects. + -- Original_Discriminant -- Present in identifiers. Used in references to discriminants that -- appear in generic units. Because the names of the discriminants may be @@ -2138,6 +2150,12 @@ package Sinfo is -- interferes with the Entity field, making it impossible to preserve the -- original entity at the point of instantiation. + -- Original_Pragma + -- When pragmas with assertion level associations are transformed in to + -- individual pragmas without the assertion level we store the original + -- prama in this attribute. This is used to avoid duplicate detection on + -- these pragmas. + -- Others_Discrete_Choices -- When a case statement or variant is analyzed, the semantic checks -- determine the actual list of choices that correspond to an others @@ -2166,6 +2184,12 @@ package Sinfo is -- type, a subsequently generated error message indicates the position -- of its full declaration. + -- Pragma_Ghost_Assertion_Level + -- Assertion_Level that was originally used in the assertion level + -- associations of its arguments. These pragmas are transformed to new + -- pragmas with the associated arguments and the original assertion + -- level is stored in this attribute. + -- Present_Expr -- Present in an N_Variant node. This has a meaningful value only after -- Gigi has back annotated the tree with representation information. At @@ -2705,6 +2729,8 @@ package Sinfo is -- Is_Delayed_Aspect -- Is_Disabled -- Import_Interface_Present + -- Original_Pragma + -- Pragma_Ghost_Assertion_Level -- Uneval_Old_Warn -- Note: we should have a section on what pragmas are passed on to @@ -7627,7 +7653,9 @@ package Sinfo is -- Is_Delayed_Aspect -- Is_Disabled -- Is_Boolean_Aspect + -- Aspect_Ghost_Assertion_Level -- Aspect_On_Partial_View + -- Original_Aspect -- Note: Aspect_Specification is an Ada 2012 feature diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 272e10ba1d5..6e6e85f946b 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -424,6 +424,7 @@ package Snames is Name_Aggregate_Individually_Assign : constant Name_Id := N + $; -- GNAT Name_Allow_Integer_Address : constant Name_Id := N + $; -- GNAT Name_Annotate : constant Name_Id := N + $; -- GNAT + Name_Assertion_Level : constant Name_Id := N + $; -- GNAT Name_Assertion_Policy : constant Name_Id := N + $; -- Ada 05 Name_Assume_No_Invalid_Values : constant Name_Id := N + $; -- GNAT Name_C_Pass_By_Copy : constant Name_Id := N + $; -- GNAT @@ -1409,6 +1410,10 @@ package Snames is Name_Reference_Control_Type : constant Name_Id := N + $; Name_Get_Element_Access : constant Name_Id := N + $; + -- Names used to implement Assertion_Levels + + Name_uDefault_Assertion_Level : constant Name_Id := N + $; + -- Names for Ada 202x Aggregate aspect. Name_Aggregate is already -- present for gprbuild. @@ -1773,6 +1778,7 @@ package Snames is Pragma_Aggregate_Individually_Assign, Pragma_Allow_Integer_Address, Pragma_Annotate, + Pragma_Assertion_Level, Pragma_Assertion_Policy, Pragma_Assume_No_Invalid_Values, Pragma_C_Pass_By_Copy, diff --git a/gcc/ada/stand.ads b/gcc/ada/stand.ads index 9b511d584c8..770b7fa44c2 100644 --- a/gcc/ada/stand.ads +++ b/gcc/ada/stand.ads @@ -484,4 +484,16 @@ package Stand is Standard_Op_Shift_Right_Arithmetic : Entity_Id; -- These entities are used for shift operators generated by the expander + Standard_Level_Static : Entity_Id; + -- Assertion_Level that indicates that the associated entity is never + -- checked. + + Standard_Level_Runtime : Entity_Id; + -- Assertion_Level that indicates that the associated entity is always + -- checked. + + Standard_Level_Default : Entity_Id; + -- A special internally defined Assertion_Level that is applied to entities + -- that were not using Assertion_Levels syntactically. + end Stand; diff --git a/gcc/ada/tbuild.adb b/gcc/ada/tbuild.adb index 52fdbfc2163..57ea93260f1 100644 --- a/gcc/ada/tbuild.adb +++ b/gcc/ada/tbuild.adb @@ -151,6 +151,20 @@ package body Tbuild is null; end Discard_Node; + -------------------------- + -- Make_Assertion_Level -- + -------------------------- + + function Make_Assertion_Level + (Loc : Source_Ptr; Nam : Name_Id) return Entity_Id + is + Level : constant Entity_Id := Make_Defining_Identifier (Loc, Nam); + begin + Mutate_Ekind (Level, E_Assertion_Level); + Set_Etype (Level, Standard_Void_Type); + return Level; + end Make_Assertion_Level; + ------------------------------------------- -- Make_Byte_Aligned_Attribute_Reference -- ------------------------------------------- diff --git a/gcc/ada/tbuild.ads b/gcc/ada/tbuild.ads index dc8b7f310c0..3a0adff97c7 100644 --- a/gcc/ada/tbuild.ads +++ b/gcc/ada/tbuild.ads @@ -60,6 +60,10 @@ package Tbuild is -- effect (e.g. a call to the parser to parse a list of compilation -- units), but the List_Id value is not required. + function Make_Assertion_Level + (Loc : Source_Ptr; Nam : Name_Id) return Entity_Id; + -- Create a new Defining_Identifier node for an Assertion_Level + function Make_Byte_Aligned_Attribute_Reference (Sloc : Source_Ptr; Prefix : Node_Id;