From 82e5c2434e6709118bdf4499cdcbd5dc2c535368 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 13 Jan 2017 12:13:00 +0100 Subject: [PATCH] [multiple changes] 2017-01-13 Gary Dismukes * checks.adb: Minor typo fix and reformatting. 2017-01-13 Javier Miranda * contracts.adb (Contract_Only_Subprograms): Remove formal. (Copy_Original_Specification): Removed. (Skip_Contract_Only_Subprogram): Move here checks previously located in the caller of this routine (to leave the code more clean). (Build_Contract_Only_Subprogram): Code cleanup. * scil_ll.ads, scil_ll.adb (Get_Contract_Only_Body_Name): Removed. (Get_Contract_Only_Missing_Body_Name): Removed. From-SVN: r244424 --- gcc/ada/ChangeLog | 14 + gcc/ada/checks.adb | 23 +- gcc/ada/contracts.adb | 2979 ++++++++++++++++++++--------------------- gcc/ada/scil_ll.adb | 28 - gcc/ada/scil_ll.ads | 7 - 5 files changed, 1477 insertions(+), 1574 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 0702a6d31cd..5aa38770395 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,17 @@ +2017-01-13 Gary Dismukes + + * checks.adb: Minor typo fix and reformatting. + +2017-01-13 Javier Miranda + + * contracts.adb (Contract_Only_Subprograms): Remove formal. + (Copy_Original_Specification): Removed. + (Skip_Contract_Only_Subprogram): Move here checks previously + located in the caller of this routine (to leave the code more clean). + (Build_Contract_Only_Subprogram): Code cleanup. + * scil_ll.ads, scil_ll.adb (Get_Contract_Only_Body_Name): Removed. + (Get_Contract_Only_Missing_Body_Name): Removed. + 2017-01-13 Javier Miranda * sem_ch6.adb (Cloned_Expression): New subprogram. diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index f67c44f37d4..80b4b4b782f 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -3390,10 +3390,10 @@ package body Checks is In_Subrange_Of (Expr_Type, Target_Base, Fixed_Int => Conv_OK) and then not Float_To_Int then - -- A small optimization : the attribute 'Pos applied to an + -- A small optimization: the attribute 'Pos applied to an -- enumeration type has a known range, even though its type - -- is Universal_Integer. so in numeric conversions it is - -- usually within range of of the target integer type. Use the + -- is Universal_Integer. So in numeric conversions it is + -- usually within range of the target integer type. Use the -- static bounds of the base types to check. if Nkind (Expr) = N_Attribute_Reference @@ -3402,15 +3402,15 @@ package body Checks is and then Is_Integer_Type (Target_Type) then declare - Enum_T : constant Entity_Id := - Root_Type (Etype (Prefix (Expr))); - Int_T : constant Entity_Id := Base_Type (Target_Type); - Last_I : constant Uint := - Intval (High_Bound (Scalar_Range (Int_T))); - Last_E : Uint; + Enum_T : constant Entity_Id := + Root_Type (Etype (Prefix (Expr))); + Int_T : constant Entity_Id := Base_Type (Target_Type); + Last_I : constant Uint := + Intval (High_Bound (Scalar_Range (Int_T))); + Last_E : Uint; begin - -- Character types have no explicit literals, we use + -- Character types have no explicit literals, so we use -- the known number of characters in the type. if Root_Type (Enum_T) = Standard_Character then @@ -3422,7 +3422,8 @@ package body Checks is Last_E := UI_From_Int (65535); else - Last_E := Enumeration_Pos + Last_E := + Enumeration_Pos (Entity (High_Bound (Scalar_Range (Enum_T)))); end if; diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 862e85b7424..eb73d035472 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -53,11 +53,6 @@ with Tbuild; use Tbuild; package body Contracts is - procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id); - -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the - -- contract-only subprogram body of eligible subprograms found in L, adds - -- them to their corresponding list of declarations, and analyzes them. - procedure Analyze_Contracts (L : List_Id; Freeze_Nod : Node_Id; @@ -68,6 +63,11 @@ package body Contracts is -- is reached. Freeze_Id is the entity of some related context which caused -- freezing up to node Freeze_Nod. + procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id); + -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the + -- contract-only subprogram body of eligible subprograms found in L, adds + -- them to their corresponding list of declarations, and analyzes them. + procedure Expand_Subprogram_Contract (Body_Id : Entity_Id); -- Expand the contracts of a subprogram body and its correspoding spec (if -- any). This routine processes all [refined] pre- and postconditions as @@ -1253,1020 +1253,1104 @@ package body Contracts is Restore_SPARK_Mode (Mode); end Analyze_Task_Contract; - ----------------------------- - -- Create_Generic_Contract -- - ----------------------------- + ------------------------------------------------- + -- Build_And_Analyze_Contract_Only_Subprograms -- + ------------------------------------------------- - procedure Create_Generic_Contract (Unit : Node_Id) is - Templ : constant Node_Id := Original_Node (Unit); - Templ_Id : constant Entity_Id := Defining_Entity (Templ); + procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is + procedure Analyze_Contract_Only_Subprograms; + -- Analyze the contract-only subprograms of L - procedure Add_Generic_Contract_Pragma (Prag : Node_Id); - -- Add a single contract-related source pragma Prag to the contract of - -- generic template Templ_Id. + procedure Append_Contract_Only_Subprograms (Subp_List : List_Id); + -- Append the contract-only bodies of Subp_List to its declarations list - --------------------------------- - -- Add_Generic_Contract_Pragma -- - --------------------------------- + function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id; + -- If E is an entity for a non-imported subprogram specification with + -- pre/postconditions and we are compiling with CodePeer mode, then + -- this procedure will create a wrapper to help Gnat2scil process its + -- contracts. Return Empty if the wrapper cannot be built. - procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is - Prag_Templ : Node_Id; + function Build_Contract_Only_Subprograms (L : List_Id) return List_Id; + -- Build the contract-only subprograms of all eligible subprograms found + -- in list L. - begin - -- Mark the pragma to prevent the premature capture of global - -- references when capturing global references of the context - -- (see Save_References_In_Pragma). + function Has_Private_Declarations (N : Node_Id) return Boolean; + -- Return True for package specs, task definitions, and protected type + -- definitions whose list of private declarations is not empty. - Set_Is_Generic_Contract_Pragma (Prag); + --------------------------------------- + -- Analyze_Contract_Only_Subprograms -- + --------------------------------------- - -- Pragmas that apply to a generic subprogram declaration are not - -- part of the semantic structure of the generic template: + procedure Analyze_Contract_Only_Subprograms is + procedure Analyze_Contract_Only_Bodies; + -- Analyze all the contract-only bodies of L - -- generic - -- procedure Example (Formal : Integer); - -- pragma Precondition (Formal > 0); + ---------------------------------- + -- Analyze_Contract_Only_Bodies -- + ---------------------------------- - -- Create a generic template for such pragmas and link the template - -- of the pragma with the generic template. + procedure Analyze_Contract_Only_Bodies is + Decl : Node_Id; - if Nkind (Templ) = N_Generic_Subprogram_Declaration then - Rewrite - (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False)); - Prag_Templ := Original_Node (Prag); + begin + Decl := First (L); + while Present (Decl) loop + if Nkind (Decl) = N_Subprogram_Body + and then Is_Contract_Only_Body + (Defining_Unit_Name (Specification (Decl))) + then + Analyze (Decl); + end if; - Set_Is_Generic_Contract_Pragma (Prag_Templ); - Add_Contract_Item (Prag_Templ, Templ_Id); + Next (Decl); + end loop; + end Analyze_Contract_Only_Bodies; - -- Otherwise link the pragma with the generic template + -- Start of processing for Analyze_Contract_Only_Subprograms + + begin + if Ekind (Current_Scope) /= E_Package then + Analyze_Contract_Only_Bodies; else - Add_Contract_Item (Prag, Templ_Id); - end if; - end Add_Generic_Contract_Pragma; + declare + Pkg_Spec : constant Node_Id := + Package_Specification (Current_Scope); - -- Local variables + begin + if not Has_Private_Declarations (Pkg_Spec) then + Analyze_Contract_Only_Bodies; - Context : constant Node_Id := Parent (Unit); - Decl : Node_Id := Empty; + -- For packages with private declarations, the contract-only + -- bodies of subprograms defined in the visible part of the + -- package are added to its private declarations (to ensure + -- that they do not cause premature freezing of types and also + -- that they are analyzed with proper visibility). Hence they + -- will be analyzed later. - -- Start of processing for Create_Generic_Contract + elsif Visible_Declarations (Pkg_Spec) = L then + null; - begin - -- A generic package declaration carries contract-related source pragmas - -- in its visible declarations. + elsif Private_Declarations (Pkg_Spec) = L then + Analyze_Contract_Only_Bodies; + end if; + end; + end if; + end Analyze_Contract_Only_Subprograms; - if Nkind (Templ) = N_Generic_Package_Declaration then - Set_Ekind (Templ_Id, E_Generic_Package); + -------------------------------------- + -- Append_Contract_Only_Subprograms -- + -------------------------------------- - if Present (Visible_Declarations (Specification (Templ))) then - Decl := First (Visible_Declarations (Specification (Templ))); + procedure Append_Contract_Only_Subprograms (Subp_List : List_Id) is + begin + if No (Subp_List) then + return; end if; - -- A generic package body carries contract-related source pragmas in its - -- declarations. + if Ekind (Current_Scope) /= E_Package then + Append_List (Subp_List, To => L); - elsif Nkind (Templ) = N_Package_Body then - Set_Ekind (Templ_Id, E_Package_Body); + else + declare + Pkg_Spec : constant Node_Id := + Package_Specification (Current_Scope); - if Present (Declarations (Templ)) then - Decl := First (Declarations (Templ)); - end if; + begin + if not Has_Private_Declarations (Pkg_Spec) then + Append_List (Subp_List, To => L); - -- Generic subprogram declaration + -- If the package has private declarations then append them to + -- its private declarations; they will be analyzed when the + -- contracts of its private declarations are analyzed. - elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then - if Nkind (Specification (Templ)) = N_Function_Specification then - Set_Ekind (Templ_Id, E_Generic_Function); - else - Set_Ekind (Templ_Id, E_Generic_Procedure); + else + Append_List + (List => Subp_List, + To => Private_Declarations (Pkg_Spec)); + end if; + end; end if; + end Append_Contract_Only_Subprograms; - -- When the generic subprogram acts as a compilation unit, inspect - -- the Pragmas_After list for contract-related source pragmas. + ------------------------------------ + -- Build_Contract_Only_Subprogram -- + ------------------------------------ - if Nkind (Context) = N_Compilation_Unit then - if Present (Aux_Decls_Node (Context)) - and then Present (Pragmas_After (Aux_Decls_Node (Context))) - then - Decl := First (Pragmas_After (Aux_Decls_Node (Context))); - end if; + -- This procedure takes care of building a wrapper to generate better + -- analysis results in the case of a call to a subprogram whose body + -- is unavailable to CodePeer but whose specification includes Pre/Post + -- conditions. The body might be unavailable for any of a number or + -- reasons (it is imported, the .adb file is simply missing, or the + -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis) + -- pragma). The built subprogram has the following contents: + -- * check preconditions + -- * call the subprogram + -- * check postconditions - -- Otherwise inspect the successive declarations for contract-related - -- source pragmas. + function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id is + Loc : constant Source_Ptr := Sloc (E); - else - Decl := Next (Unit); - end if; + Missing_Body_Name : constant Name_Id := + New_External_Name (Chars (E), "__missing_body"); - -- A generic subprogram body carries contract-related source pragmas in - -- its declarations. + function Build_Missing_Body_Decls return List_Id; + -- Build the declaration of the missing body subprogram and its + -- corresponding pragma Import. - elsif Nkind (Templ) = N_Subprogram_Body then - Set_Ekind (Templ_Id, E_Subprogram_Body); + function Build_Missing_Body_Subprogram_Call return Node_Id; + -- Build the call to the missing body subprogram - if Present (Declarations (Templ)) then - Decl := First (Declarations (Templ)); - end if; - end if; + function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean; + -- Return True for cases where the wrapper is not needed or we cannot + -- build it. - -- Inspect the relevant declarations looking for contract-related source - -- pragmas and add them to the contract of the generic unit. + ------------------------------ + -- Build_Missing_Body_Decls -- + ------------------------------ - while Present (Decl) loop - if Comes_From_Source (Decl) then - if Nkind (Decl) = N_Pragma then + function Build_Missing_Body_Decls return List_Id is + Spec : constant Node_Id := Declaration_Node (E); + Decl : Node_Id; + Prag : Node_Id; - -- The source pragma is a contract annotation + begin + Decl := + Make_Subprogram_Declaration (Loc, Copy_Subprogram_Spec (Spec)); + Set_Chars (Defining_Entity (Decl), Missing_Body_Name); - if Is_Contract_Annotation (Decl) then - Add_Generic_Contract_Pragma (Decl); - end if; + Prag := + Make_Pragma (Loc, + Chars => Name_Import, + Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Make_Identifier (Loc, Name_Ada)), - -- The region where a contract-related source pragma may appear - -- ends with the first source non-pragma declaration or statement. + Make_Pragma_Argument_Association (Loc, + Expression => Make_Identifier (Loc, Missing_Body_Name)))); - else - exit; - end if; - end if; + return New_List (Decl, Prag); + end Build_Missing_Body_Decls; - Next (Decl); - end loop; - end Create_Generic_Contract; + ---------------------------------------- + -- Build_Missing_Body_Subprogram_Call -- + ---------------------------------------- - -------------------------------- - -- Expand_Subprogram_Contract -- - -------------------------------- + function Build_Missing_Body_Subprogram_Call return Node_Id is + Forml : Entity_Id; + Parms : List_Id; - procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is - Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); - Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); + begin + Parms := New_List; - procedure Add_Invariant_And_Predicate_Checks - (Subp_Id : Entity_Id; - Stmts : in out List_Id; - Result : out Node_Id); - -- Process the result of function Subp_Id (if applicable) and all its - -- formals. Add invariant and predicate checks where applicable. The - -- routine appends all the checks to list Stmts. If Subp_Id denotes a - -- function, Result contains the entity of parameter _Result, to be - -- used in the creation of procedure _Postconditions. - - procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id); - -- Append a node to a list. If there is no list, create a new one. When - -- the item denotes a pragma, it is added to the list only when it is - -- enabled. + -- Build parameter list that we need - procedure Build_Postconditions_Procedure - (Subp_Id : Entity_Id; - Stmts : List_Id; - Result : Entity_Id); - -- Create the body of procedure _Postconditions which handles various - -- assertion actions on exit from subprogram Subp_Id. Stmts is the list - -- of statements to be checked on exit. Parameter Result is the entity - -- of parameter _Result when Subp_Id denotes a function. + Forml := First_Formal (E); + while Present (Forml) loop + Append_To (Parms, Make_Identifier (Loc, Chars (Forml))); + Next_Formal (Forml); + end loop; - procedure Process_Contract_Cases (Stmts : in out List_Id); - -- Process pragma Contract_Cases. This routine prepends items to the - -- body declarations and appends items to list Stmts. + -- Build the call to the missing body subprogram - procedure Process_Postconditions (Stmts : in out List_Id); - -- Collect all [inherited] spec and body postconditions and accumulate - -- their pragma Check equivalents in list Stmts. + if Ekind_In (E, E_Function, E_Generic_Function) then + return + Make_Simple_Return_Statement (Loc, + Expression => + Make_Function_Call (Loc, + Name => + Make_Identifier (Loc, Missing_Body_Name), + Parameter_Associations => Parms)); - procedure Process_Preconditions; - -- Collect all [inherited] spec and body preconditions and prepend their - -- pragma Check equivalents to the declarations of the body. + else + return + Make_Procedure_Call_Statement (Loc, + Name => + Make_Identifier (Loc, Missing_Body_Name), + Parameter_Associations => Parms); + end if; + end Build_Missing_Body_Subprogram_Call; - ---------------------------------------- - -- Add_Invariant_And_Predicate_Checks -- - ---------------------------------------- + ----------------------------------- + -- Skip_Contract_Only_Subprogram -- + ----------------------------------- - procedure Add_Invariant_And_Predicate_Checks - (Subp_Id : Entity_Id; - Stmts : in out List_Id; - Result : out Node_Id) - is - procedure Add_Invariant_Access_Checks (Id : Entity_Id); - -- Id denotes the return value of a function or a formal parameter. - -- Add an invariant check if the type of Id is access to a type with - -- invariants. The routine appends the generated code to Stmts. + function Skip_Contract_Only_Subprogram + (E : Entity_Id) return Boolean + is + function Depends_On_Enclosing_Private_Type return Boolean; + -- Return True if some formal of E (or its return type) are + -- private types defined in an enclosing package. - function Invariant_Checks_OK (Typ : Entity_Id) return Boolean; - -- Determine whether type Typ can benefit from invariant checks. To - -- qualify, the type must have a non-null invariant procedure and - -- subprogram Subp_Id must appear visible from the point of view of - -- the type. + function Some_Enclosing_Package_Has_Private_Decls return Boolean; + -- Return True if some enclosing package of the current scope has + -- private declarations. - --------------------------------- - -- Add_Invariant_Access_Checks -- - --------------------------------- + --------------------------------------- + -- Depends_On_Enclosing_Private_Type -- + --------------------------------------- - procedure Add_Invariant_Access_Checks (Id : Entity_Id) is - Loc : constant Source_Ptr := Sloc (Body_Decl); - Ref : Node_Id; - Typ : Entity_Id; + function Depends_On_Enclosing_Private_Type return Boolean is + function Defined_In_Enclosing_Package + (Typ : Entity_Id) return Boolean; + -- Return True if Typ is an entity defined in an enclosing + -- package of the current scope. - begin - Typ := Etype (Id); + ---------------------------------- + -- Defined_In_Enclosing_Package -- + ---------------------------------- - if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then - Typ := Designated_Type (Typ); + function Defined_In_Enclosing_Package + (Typ : Entity_Id) return Boolean + is + Scop : Entity_Id := Scope (Current_Scope); - if Invariant_Checks_OK (Typ) then - Ref := - Make_Explicit_Dereference (Loc, - Prefix => New_Occurrence_Of (Id, Loc)); - Set_Etype (Ref, Typ); + begin + while Scop /= Scope (Typ) + and then not Is_Compilation_Unit (Scop) + loop + Scop := Scope (Scop); + end loop; - -- Generate: - -- if /= null then - -- )> - -- end if; + return Scop = Scope (Typ); + end Defined_In_Enclosing_Package; - Append_Enabled_Item - (Item => - Make_If_Statement (Loc, - Condition => - Make_Op_Ne (Loc, - Left_Opnd => New_Occurrence_Of (Id, Loc), - Right_Opnd => Make_Null (Loc)), - Then_Statements => New_List ( - Make_Invariant_Call (Ref))), - List => Stmts); - end if; - end if; - end Add_Invariant_Access_Checks; + -- Local variables - ------------------------- - -- Invariant_Checks_OK -- - ------------------------- + Param_E : Entity_Id; + Typ : Entity_Id; - function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is - function Has_Public_Visibility_Of_Subprogram return Boolean; - -- Determine whether type Typ has public visibility of subprogram - -- Subp_Id. + -- Start of processing for Depends_On_Enclosing_Private_Type - ----------------------------------------- - -- Has_Public_Visibility_Of_Subprogram -- - ----------------------------------------- + begin + Param_E := First_Entity (E); + while Present (Param_E) loop + Typ := Etype (Param_E); - function Has_Public_Visibility_Of_Subprogram return Boolean is - Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); + if Is_Private_Type (Typ) + and then Defined_In_Enclosing_Package (Typ) + then + return True; + end if; - begin - -- An Initialization procedure must be considered visible even - -- though it is internally generated. + Next_Entity (Param_E); + end loop; - if Is_Init_Proc (Defining_Entity (Subp_Decl)) then - return True; + return + Ekind (E) = E_Function + and then Is_Private_Type (Etype (E)) + and then Defined_In_Enclosing_Package (Etype (E)); + end Depends_On_Enclosing_Private_Type; - elsif Ekind (Scope (Typ)) /= E_Package then - return False; + ---------------------------------------------- + -- Some_Enclosing_Package_Has_Private_Decls -- + ---------------------------------------------- - -- Internally generated code is never publicly visible except - -- for a subprogram that is the implementation of an expression - -- function. In that case the visibility is determined by the - -- last check. + function Some_Enclosing_Package_Has_Private_Decls return Boolean is + Scop : Entity_Id := Current_Scope; + Pkg_Spec : Node_Id := Package_Specification (Scop); - elsif not Comes_From_Source (Subp_Decl) - and then - (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function - or else not - Comes_From_Source (Defining_Entity (Subp_Decl))) - then - return False; + begin + loop + if Ekind (Scop) = E_Package + and then Has_Private_Declarations + (Package_Specification (Scop)) + then + Pkg_Spec := Package_Specification (Scop); + end if; - -- Determine whether the subprogram is declared in the visible - -- declarations of the package containing the type. + exit when Is_Compilation_Unit (Scop); + Scop := Scope (Scop); + end loop; - else - return List_Containing (Subp_Decl) = - Visible_Declarations - (Specification (Unit_Declaration_Node (Scope (Typ)))); - end if; - end Has_Public_Visibility_Of_Subprogram; + return Pkg_Spec /= Package_Specification (Current_Scope); + end Some_Enclosing_Package_Has_Private_Decls; - -- Start of processing for Invariant_Checks_OK + -- Start of processing for Skip_Contract_Only_Subprogram begin - return - Has_Invariants (Typ) - and then Present (Invariant_Procedure (Typ)) - and then not Has_Null_Body (Invariant_Procedure (Typ)) - and then Has_Public_Visibility_Of_Subprogram; - end Invariant_Checks_OK; + if not CodePeer_Mode + or else Inside_A_Generic + or else not Is_Subprogram (E) + or else Is_Abstract_Subprogram (E) + or else Is_Imported (E) + or else No (Contract (E)) + or else No (Pre_Post_Conditions (Contract (E))) + or else Is_Contract_Only_Body (E) + or else Convention (E) = Convention_Protected + then + return True; - -- Local variables + -- We do not support building the contract-only subprogram if E + -- is a subprogram declared in a nested package that has some + -- formal or return type depending on a private type defined in + -- an enclosing package. - Loc : constant Source_Ptr := Sloc (Body_Decl); - -- Source location of subprogram body contract + elsif Ekind (Current_Scope) = E_Package + and then Some_Enclosing_Package_Has_Private_Decls + and then Depends_On_Enclosing_Private_Type + then + if Debug_Flag_Dot_KK then + declare + Saved_Mode : constant Warning_Mode_Type := Warning_Mode; - Formal : Entity_Id; - Typ : Entity_Id; + begin + -- Warnings are disabled by default under CodePeer_Mode + -- (see switch-c). Enable them temporarily. - -- Start of processing for Add_Invariant_And_Predicate_Checks + Warning_Mode := Normal; + Error_Msg_N + ("cannot generate contract-only subprogram?", E); + Warning_Mode := Saved_Mode; + end; + end if; - begin - Result := Empty; + return True; + end if; - -- Process the result of a function + return False; + end Skip_Contract_Only_Subprogram; - if Ekind (Subp_Id) = E_Function then - Typ := Etype (Subp_Id); + -- Start of processing for Build_Contract_Only_Subprogram - -- Generate _Result which is used in procedure _Postconditions to - -- verify the return value. + begin + -- Test cases where the wrapper is not needed and cases where we + -- cannot build it. - Result := Make_Defining_Identifier (Loc, Name_uResult); - Set_Etype (Result, Typ); + if Skip_Contract_Only_Subprogram (E) then + return Empty; + end if; - -- Add an invariant check when the return type has invariants and - -- the related function is visible to the outside. + -- Note on calls to Copy_Separate_Tree. The trees we are copying + -- here are fully analyzed, but we definitely want fully syntactic + -- unanalyzed trees in the body we construct, so that the analysis + -- generates the right visibility, and that is exactly what the + -- calls to Copy_Separate_Tree give us. - if Invariant_Checks_OK (Typ) then - Append_Enabled_Item - (Item => - Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), - List => Stmts); - end if; + declare + Name : constant Name_Id := + New_External_Name (Chars (E), "__contract_only"); + Id : Entity_Id; + Bod : Node_Id; - -- Add an invariant check when the return type is an access to a - -- type with invariants. + begin + Bod := + Make_Subprogram_Body (Loc, + Specification => + Copy_Subprogram_Spec (Declaration_Node (E)), + Declarations => + Build_Missing_Body_Decls, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => New_List ( + Build_Missing_Body_Subprogram_Call), + End_Label => Make_Identifier (Loc, Name))); - Add_Invariant_Access_Checks (Result); - end if; + Id := Defining_Unit_Name (Specification (Bod)); - -- Add invariant and predicates for all formals that qualify + -- Copy only the pre/postconditions of the original contract + -- since it is what we need, but also because pragmas stored in + -- the other fields have N_Pragmas with N_Aspect_Specifications + -- that reference their associated pragma (thus causing an endless + -- loop when trying to copy the subtree). - Formal := First_Formal (Subp_Id); - while Present (Formal) loop - Typ := Etype (Formal); + declare + New_Contract : constant Node_Id := Make_Contract (Sloc (E)); - if Ekind (Formal) /= E_In_Parameter - or else Is_Access_Type (Typ) - then - if Invariant_Checks_OK (Typ) then - Append_Enabled_Item - (Item => - Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)), - List => Stmts); - end if; + begin + Set_Pre_Post_Conditions (New_Contract, + Copy_Separate_Tree (Pre_Post_Conditions (Contract (E)))); + Set_Contract (Id, New_Contract); + end; - Add_Invariant_Access_Checks (Formal); + -- Fix the name of this new subprogram and link the original + -- subprogram with its Contract_Only_Body subprogram. - -- Note: we used to add predicate checks for OUT and IN OUT - -- formals here, but that was misguided, since such checks are - -- performed on the caller side, based on the predicate of the - -- actual, rather than the predicate of the formal. + Set_Chars (Id, Name); + Set_Is_Contract_Only_Body (Id); + Set_Contract_Only_Body (E, Id); - end if; + return Bod; + end; + end Build_Contract_Only_Subprogram; - Next_Formal (Formal); - end loop; - end Add_Invariant_And_Predicate_Checks; + ------------------------------------- + -- Build_Contract_Only_Subprograms -- + ------------------------------------- - ------------------------- - -- Append_Enabled_Item -- - ------------------------- + function Build_Contract_Only_Subprograms (L : List_Id) return List_Id is + Decl : Node_Id; + New_Subp : Node_Id; + Result : List_Id := No_List; + Subp_Id : Entity_Id; - procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is begin - -- Do not chain ignored or disabled pragmas - - if Nkind (Item) = N_Pragma - and then (Is_Ignored (Item) or else Is_Disabled (Item)) - then - null; + Decl := First (L); + while Present (Decl) loop + if Nkind (Decl) = N_Subprogram_Declaration then + Subp_Id := Defining_Unit_Name (Specification (Decl)); + New_Subp := Build_Contract_Only_Subprogram (Subp_Id); - -- Otherwise, add the item + if Present (New_Subp) then + if No (Result) then + Result := New_List; + end if; - else - if No (List) then - List := New_List; + Append_To (Result, New_Subp); + end if; end if; - -- If the pragma is a conjunct in a composite postcondition, it - -- has been processed in reverse order. In the postcondition body - -- it must appear before the others. + Next (Decl); + end loop; - if Nkind (Item) = N_Pragma - and then From_Aspect_Specification (Item) - and then Split_PPC (Item) - then - Prepend (Item, List); - else - Append (Item, List); - end if; - end if; - end Append_Enabled_Item; + return Result; + end Build_Contract_Only_Subprograms; - ------------------------------------ - -- Build_Postconditions_Procedure -- - ------------------------------------ + ------------------------------ + -- Has_Private_Declarations -- + ------------------------------ - procedure Build_Postconditions_Procedure - (Subp_Id : Entity_Id; - Stmts : List_Id; - Result : Entity_Id) - is - procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id); - -- Insert node Stmt before the first source declaration of the - -- related subprogram's body. If no such declaration exists, Stmt - -- becomes the last declaration. + function Has_Private_Declarations (N : Node_Id) return Boolean is + begin + if not Nkind_In (N, N_Package_Specification, + N_Protected_Definition, + N_Task_Definition) + then + return False; + else + return + Present (Private_Declarations (N)) + and then Is_Non_Empty_List (Private_Declarations (N)); + end if; + end Has_Private_Declarations; - -------------------------------------------- - -- Insert_Before_First_Source_Declaration -- - -------------------------------------------- + -- Local variables - procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is - Decls : constant List_Id := Declarations (Body_Decl); - Decl : Node_Id; + Subp_List : List_Id; - begin - -- Inspect the declarations of the related subprogram body looking - -- for the first source declaration. + -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms - if Present (Decls) then - Decl := First (Decls); - while Present (Decl) loop - if Comes_From_Source (Decl) then - Insert_Before (Decl, Stmt); - return; - end if; + begin + Subp_List := Build_Contract_Only_Subprograms (L); + Append_Contract_Only_Subprograms (Subp_List); + Analyze_Contract_Only_Subprograms; + end Build_And_Analyze_Contract_Only_Subprograms; - Next (Decl); - end loop; + ----------------------------- + -- Create_Generic_Contract -- + ----------------------------- - -- If we get there, then the subprogram body lacks any source - -- declarations. The body of _Postconditions now acts as the - -- last declaration. + procedure Create_Generic_Contract (Unit : Node_Id) is + Templ : constant Node_Id := Original_Node (Unit); + Templ_Id : constant Entity_Id := Defining_Entity (Templ); - Append (Stmt, Decls); + procedure Add_Generic_Contract_Pragma (Prag : Node_Id); + -- Add a single contract-related source pragma Prag to the contract of + -- generic template Templ_Id. - -- Ensure that the body has a declaration list + --------------------------------- + -- Add_Generic_Contract_Pragma -- + --------------------------------- - else - Set_Declarations (Body_Decl, New_List (Stmt)); - end if; - end Insert_Before_First_Source_Declaration; + procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is + Prag_Templ : Node_Id; - -- Local variables + begin + -- Mark the pragma to prevent the premature capture of global + -- references when capturing global references of the context + -- (see Save_References_In_Pragma). - Loc : constant Source_Ptr := Sloc (Body_Decl); - Params : List_Id := No_List; - Proc_Bod : Node_Id; - Proc_Decl : Node_Id; - Proc_Id : Entity_Id; - Proc_Spec : Node_Id; + Set_Is_Generic_Contract_Pragma (Prag); - -- Start of processing for Build_Postconditions_Procedure + -- Pragmas that apply to a generic subprogram declaration are not + -- part of the semantic structure of the generic template: - begin - -- Nothing to do if there are no actions to check on exit + -- generic + -- procedure Example (Formal : Integer); + -- pragma Precondition (Formal > 0); - if No (Stmts) then - return; - end if; + -- Create a generic template for such pragmas and link the template + -- of the pragma with the generic template. - Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions); - Set_Debug_Info_Needed (Proc_Id); - Set_Postconditions_Proc (Subp_Id, Proc_Id); + if Nkind (Templ) = N_Generic_Subprogram_Declaration then + Rewrite + (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False)); + Prag_Templ := Original_Node (Prag); - -- Force the front-end inlining of _Postconditions when generating C - -- code, since its body may have references to itypes defined in the - -- enclosing subprogram, which would cause problems for unnesting - -- routines in the absence of inlining. + Set_Is_Generic_Contract_Pragma (Prag_Templ); + Add_Contract_Item (Prag_Templ, Templ_Id); - if Generate_C_Code then - Set_Has_Pragma_Inline (Proc_Id); - Set_Has_Pragma_Inline_Always (Proc_Id); - Set_Is_Inlined (Proc_Id); + -- Otherwise link the pragma with the generic template + + else + Add_Contract_Item (Prag, Templ_Id); end if; + end Add_Generic_Contract_Pragma; - -- The related subprogram is a function: create the specification of - -- parameter _Result. + -- Local variables - if Present (Result) then - Params := New_List ( - Make_Parameter_Specification (Loc, - Defining_Identifier => Result, - Parameter_Type => - New_Occurrence_Of (Etype (Result), Loc))); - end if; + Context : constant Node_Id := Parent (Unit); + Decl : Node_Id := Empty; - Proc_Spec := - Make_Procedure_Specification (Loc, - Defining_Unit_Name => Proc_Id, - Parameter_Specifications => Params); + -- Start of processing for Create_Generic_Contract - Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec); + begin + -- A generic package declaration carries contract-related source pragmas + -- in its visible declarations. - -- Insert _Postconditions before the first source declaration of the - -- body. This ensures that the body will not cause any premature - -- freezing, as it may mention types: + if Nkind (Templ) = N_Generic_Package_Declaration then + Set_Ekind (Templ_Id, E_Generic_Package); - -- procedure Proc (Obj : Array_Typ) is - -- procedure _postconditions is - -- begin - -- ... Obj ... - -- end _postconditions; - - -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1)); - -- begin - - -- In the example above, Obj is of type T but the incorrect placement - -- of _Postconditions will cause a crash in gigi due to an out-of- - -- order reference. The body of _Postconditions must be placed after - -- the declaration of Temp to preserve correct visibility. - - Insert_Before_First_Source_Declaration (Proc_Decl); - Analyze (Proc_Decl); + if Present (Visible_Declarations (Specification (Templ))) then + Decl := First (Visible_Declarations (Specification (Templ))); + end if; - -- Set an explicit End_Label to override the sloc of the implicit - -- RETURN statement, and prevent it from inheriting the sloc of one - -- the postconditions: this would cause confusing debug info to be - -- produced, interfering with coverage-analysis tools. + -- A generic package body carries contract-related source pragmas in its + -- declarations. - Proc_Bod := - Make_Subprogram_Body (Loc, - Specification => - Copy_Subprogram_Spec (Proc_Spec), - Declarations => Empty_List, - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => Stmts, - End_Label => Make_Identifier (Loc, Chars (Proc_Id)))); + elsif Nkind (Templ) = N_Package_Body then + Set_Ekind (Templ_Id, E_Package_Body); - Insert_After_And_Analyze (Proc_Decl, Proc_Bod); - end Build_Postconditions_Procedure; + if Present (Declarations (Templ)) then + Decl := First (Declarations (Templ)); + end if; - ---------------------------- - -- Process_Contract_Cases -- - ---------------------------- + -- Generic subprogram declaration - procedure Process_Contract_Cases (Stmts : in out List_Id) is - procedure Process_Contract_Cases_For (Subp_Id : Entity_Id); - -- Process pragma Contract_Cases for subprogram Subp_Id + elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then + if Nkind (Specification (Templ)) = N_Function_Specification then + Set_Ekind (Templ_Id, E_Generic_Function); + else + Set_Ekind (Templ_Id, E_Generic_Procedure); + end if; - -------------------------------- - -- Process_Contract_Cases_For -- - -------------------------------- + -- When the generic subprogram acts as a compilation unit, inspect + -- the Pragmas_After list for contract-related source pragmas. - procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is - Items : constant Node_Id := Contract (Subp_Id); - Prag : Node_Id; + if Nkind (Context) = N_Compilation_Unit then + if Present (Aux_Decls_Node (Context)) + and then Present (Pragmas_After (Aux_Decls_Node (Context))) + then + Decl := First (Pragmas_After (Aux_Decls_Node (Context))); + end if; - begin - if Present (Items) then - Prag := Contract_Test_Cases (Items); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Contract_Cases then - Expand_Pragma_Contract_Cases - (CCs => Prag, - Subp_Id => Subp_Id, - Decls => Declarations (Body_Decl), - Stmts => Stmts); - end if; + -- Otherwise inspect the successive declarations for contract-related + -- source pragmas. - Prag := Next_Pragma (Prag); - end loop; - end if; - end Process_Contract_Cases_For; + else + Decl := Next (Unit); + end if; - -- Start of processing for Process_Contract_Cases + -- A generic subprogram body carries contract-related source pragmas in + -- its declarations. - begin - Process_Contract_Cases_For (Body_Id); + elsif Nkind (Templ) = N_Subprogram_Body then + Set_Ekind (Templ_Id, E_Subprogram_Body); - if Present (Spec_Id) then - Process_Contract_Cases_For (Spec_Id); + if Present (Declarations (Templ)) then + Decl := First (Declarations (Templ)); end if; - end Process_Contract_Cases; + end if; - ---------------------------- - -- Process_Postconditions -- - ---------------------------- + -- Inspect the relevant declarations looking for contract-related source + -- pragmas and add them to the contract of the generic unit. - procedure Process_Postconditions (Stmts : in out List_Id) is - procedure Process_Body_Postconditions (Post_Nam : Name_Id); - -- Collect all [refined] postconditions of a specific kind denoted - -- by Post_Nam that belong to the body, and generate pragma Check - -- equivalents in list Stmts. + while Present (Decl) loop + if Comes_From_Source (Decl) then + if Nkind (Decl) = N_Pragma then - procedure Process_Spec_Postconditions; - -- Collect all [inherited] postconditions of the spec, and generate - -- pragma Check equivalents in list Stmts. + -- The source pragma is a contract annotation - --------------------------------- - -- Process_Body_Postconditions -- - --------------------------------- + if Is_Contract_Annotation (Decl) then + Add_Generic_Contract_Pragma (Decl); + end if; - procedure Process_Body_Postconditions (Post_Nam : Name_Id) is - Items : constant Node_Id := Contract (Body_Id); - Unit_Decl : constant Node_Id := Parent (Body_Decl); - Decl : Node_Id; - Prag : Node_Id; + -- The region where a contract-related source pragma may appear + -- ends with the first source non-pragma declaration or statement. - begin - -- Process the contract + else + exit; + end if; + end if; - if Present (Items) then - Prag := Pre_Post_Conditions (Items); - while Present (Prag) loop - if Pragma_Name (Prag) = Post_Nam then - Append_Enabled_Item - (Item => Build_Pragma_Check_Equivalent (Prag), - List => Stmts); - end if; + Next (Decl); + end loop; + end Create_Generic_Contract; - Prag := Next_Pragma (Prag); - end loop; - end if; + -------------------------------- + -- Expand_Subprogram_Contract -- + -------------------------------- - -- The subprogram body being processed is actually the proper body - -- of a stub with a corresponding spec. The subprogram stub may - -- carry a postcondition pragma, in which case it must be taken - -- into account. The pragma appears after the stub. + procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is + Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); + Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); - if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then - Decl := Next (Corresponding_Stub (Unit_Decl)); - while Present (Decl) loop + procedure Add_Invariant_And_Predicate_Checks + (Subp_Id : Entity_Id; + Stmts : in out List_Id; + Result : out Node_Id); + -- Process the result of function Subp_Id (if applicable) and all its + -- formals. Add invariant and predicate checks where applicable. The + -- routine appends all the checks to list Stmts. If Subp_Id denotes a + -- function, Result contains the entity of parameter _Result, to be + -- used in the creation of procedure _Postconditions. - -- Note that non-matching pragmas are skipped + procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id); + -- Append a node to a list. If there is no list, create a new one. When + -- the item denotes a pragma, it is added to the list only when it is + -- enabled. - if Nkind (Decl) = N_Pragma then - if Pragma_Name (Decl) = Post_Nam then - Append_Enabled_Item - (Item => Build_Pragma_Check_Equivalent (Decl), - List => Stmts); - end if; + procedure Build_Postconditions_Procedure + (Subp_Id : Entity_Id; + Stmts : List_Id; + Result : Entity_Id); + -- Create the body of procedure _Postconditions which handles various + -- assertion actions on exit from subprogram Subp_Id. Stmts is the list + -- of statements to be checked on exit. Parameter Result is the entity + -- of parameter _Result when Subp_Id denotes a function. - -- Skip internally generated code + procedure Process_Contract_Cases (Stmts : in out List_Id); + -- Process pragma Contract_Cases. This routine prepends items to the + -- body declarations and appends items to list Stmts. - elsif not Comes_From_Source (Decl) then - null; + procedure Process_Postconditions (Stmts : in out List_Id); + -- Collect all [inherited] spec and body postconditions and accumulate + -- their pragma Check equivalents in list Stmts. - -- Postcondition pragmas are usually grouped together. There - -- is no need to inspect the whole declarative list. + procedure Process_Preconditions; + -- Collect all [inherited] spec and body preconditions and prepend their + -- pragma Check equivalents to the declarations of the body. - else - exit; - end if; + ---------------------------------------- + -- Add_Invariant_And_Predicate_Checks -- + ---------------------------------------- - Next (Decl); - end loop; - end if; - end Process_Body_Postconditions; + procedure Add_Invariant_And_Predicate_Checks + (Subp_Id : Entity_Id; + Stmts : in out List_Id; + Result : out Node_Id) + is + procedure Add_Invariant_Access_Checks (Id : Entity_Id); + -- Id denotes the return value of a function or a formal parameter. + -- Add an invariant check if the type of Id is access to a type with + -- invariants. The routine appends the generated code to Stmts. + + function Invariant_Checks_OK (Typ : Entity_Id) return Boolean; + -- Determine whether type Typ can benefit from invariant checks. To + -- qualify, the type must have a non-null invariant procedure and + -- subprogram Subp_Id must appear visible from the point of view of + -- the type. --------------------------------- - -- Process_Spec_Postconditions -- + -- Add_Invariant_Access_Checks -- --------------------------------- - procedure Process_Spec_Postconditions is - Subps : constant Subprogram_List := - Inherited_Subprograms (Spec_Id); - Items : Node_Id; - Prag : Node_Id; - Subp_Id : Entity_Id; + procedure Add_Invariant_Access_Checks (Id : Entity_Id) is + Loc : constant Source_Ptr := Sloc (Body_Decl); + Ref : Node_Id; + Typ : Entity_Id; begin - -- Process the contract - - Items := Contract (Spec_Id); + Typ := Etype (Id); - if Present (Items) then - Prag := Pre_Post_Conditions (Items); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Postcondition then - Append_Enabled_Item - (Item => Build_Pragma_Check_Equivalent (Prag), - List => Stmts); - end if; + if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then + Typ := Designated_Type (Typ); - Prag := Next_Pragma (Prag); - end loop; + if Invariant_Checks_OK (Typ) then + Ref := + Make_Explicit_Dereference (Loc, + Prefix => New_Occurrence_Of (Id, Loc)); + Set_Etype (Ref, Typ); + + -- Generate: + -- if /= null then + -- )> + -- end if; + + Append_Enabled_Item + (Item => + Make_If_Statement (Loc, + Condition => + Make_Op_Ne (Loc, + Left_Opnd => New_Occurrence_Of (Id, Loc), + Right_Opnd => Make_Null (Loc)), + Then_Statements => New_List ( + Make_Invariant_Call (Ref))), + List => Stmts); + end if; end if; + end Add_Invariant_Access_Checks; - -- Process the contracts of all inherited subprograms, looking for - -- class-wide postconditions. + ------------------------- + -- Invariant_Checks_OK -- + ------------------------- - for Index in Subps'Range loop - Subp_Id := Subps (Index); - Items := Contract (Subp_Id); + function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is + function Has_Public_Visibility_Of_Subprogram return Boolean; + -- Determine whether type Typ has public visibility of subprogram + -- Subp_Id. - if Present (Items) then - Prag := Pre_Post_Conditions (Items); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Postcondition - and then Class_Present (Prag) - then - Append_Enabled_Item - (Item => - Build_Pragma_Check_Equivalent - (Prag => Prag, - Subp_Id => Spec_Id, - Inher_Id => Subp_Id), - List => Stmts); - end if; + ----------------------------------------- + -- Has_Public_Visibility_Of_Subprogram -- + ----------------------------------------- - Prag := Next_Pragma (Prag); - end loop; - end if; - end loop; - end Process_Spec_Postconditions; + function Has_Public_Visibility_Of_Subprogram return Boolean is + Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); - -- Start of processing for Process_Postconditions + begin + -- An Initialization procedure must be considered visible even + -- though it is internally generated. - begin - -- The processing of postconditions is done in reverse order (body - -- first) to ensure the following arrangement: + if Is_Init_Proc (Defining_Entity (Subp_Decl)) then + return True; - -- - -- - -- - -- + elsif Ekind (Scope (Typ)) /= E_Package then + return False; - Process_Body_Postconditions (Name_Refined_Post); - Process_Body_Postconditions (Name_Postcondition); + -- Internally generated code is never publicly visible except + -- for a subprogram that is the implementation of an expression + -- function. In that case the visibility is determined by the + -- last check. - if Present (Spec_Id) then - Process_Spec_Postconditions; - end if; - end Process_Postconditions; + elsif not Comes_From_Source (Subp_Decl) + and then + (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function + or else not + Comes_From_Source (Defining_Entity (Subp_Decl))) + then + return False; - --------------------------- - -- Process_Preconditions -- - --------------------------- + -- Determine whether the subprogram is declared in the visible + -- declarations of the package containing the type. - procedure Process_Preconditions is - Class_Pre : Node_Id := Empty; - -- The sole [inherited] class-wide precondition pragma that applies - -- to the subprogram. + else + return List_Containing (Subp_Decl) = + Visible_Declarations + (Specification (Unit_Declaration_Node (Scope (Typ)))); + end if; + end Has_Public_Visibility_Of_Subprogram; - Insert_Node : Node_Id := Empty; - -- The insertion node after which all pragma Check equivalents are - -- inserted. + -- Start of processing for Invariant_Checks_OK - function Is_Prologue_Renaming (Decl : Node_Id) return Boolean; - -- Determine whether arbitrary declaration Decl denotes a renaming of - -- a discriminant or protection field _object. + begin + return + Has_Invariants (Typ) + and then Present (Invariant_Procedure (Typ)) + and then not Has_Null_Body (Invariant_Procedure (Typ)) + and then Has_Public_Visibility_Of_Subprogram; + end Invariant_Checks_OK; - procedure Merge_Preconditions (From : Node_Id; Into : Node_Id); - -- Merge two class-wide preconditions by "or else"-ing them. The - -- changes are accumulated in parameter Into. Update the error - -- message of Into. + -- Local variables - procedure Prepend_To_Decls (Item : Node_Id); - -- Prepend a single item to the declarations of the subprogram body + Loc : constant Source_Ptr := Sloc (Body_Decl); + -- Source location of subprogram body contract - procedure Prepend_To_Decls_Or_Save (Prag : Node_Id); - -- Save a class-wide precondition into Class_Pre, or prepend a normal - -- precondition to the declarations of the body and analyze it. + Formal : Entity_Id; + Typ : Entity_Id; - procedure Process_Inherited_Preconditions; - -- Collect all inherited class-wide preconditions and merge them into - -- one big precondition to be evaluated as pragma Check. + -- Start of processing for Add_Invariant_And_Predicate_Checks - procedure Process_Preconditions_For (Subp_Id : Entity_Id); - -- Collect all preconditions of subprogram Subp_Id and prepend their - -- pragma Check equivalents to the declarations of the body. + begin + Result := Empty; - -------------------------- - -- Is_Prologue_Renaming -- - -------------------------- + -- Process the result of a function - function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is - Nam : Node_Id; - Obj : Entity_Id; - Pref : Node_Id; - Sel : Node_Id; + if Ekind (Subp_Id) = E_Function then + Typ := Etype (Subp_Id); - begin - if Nkind (Decl) = N_Object_Renaming_Declaration then - Obj := Defining_Entity (Decl); - Nam := Name (Decl); + -- Generate _Result which is used in procedure _Postconditions to + -- verify the return value. - if Nkind (Nam) = N_Selected_Component then - Pref := Prefix (Nam); - Sel := Selector_Name (Nam); + Result := Make_Defining_Identifier (Loc, Name_uResult); + Set_Etype (Result, Typ); - -- A discriminant renaming appears as - -- Discr : constant ... := Prefix.Discr; + -- Add an invariant check when the return type has invariants and + -- the related function is visible to the outside. - if Ekind (Obj) = E_Constant - and then Is_Entity_Name (Sel) - and then Present (Entity (Sel)) - and then Ekind (Entity (Sel)) = E_Discriminant - then - return True; + if Invariant_Checks_OK (Typ) then + Append_Enabled_Item + (Item => + Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), + List => Stmts); + end if; - -- A protection field renaming appears as - -- Prot : ... := _object._object; + -- Add an invariant check when the return type is an access to a + -- type with invariants. - -- A renamed private component is just a component of - -- _object, with an arbitrary name. + Add_Invariant_Access_Checks (Result); + end if; - elsif Ekind (Obj) = E_Variable - and then Nkind (Pref) = N_Identifier - and then Chars (Pref) = Name_uObject - and then Nkind (Sel) = N_Identifier - then - return True; - end if; + -- Add invariant and predicates for all formals that qualify + + Formal := First_Formal (Subp_Id); + while Present (Formal) loop + Typ := Etype (Formal); + + if Ekind (Formal) /= E_In_Parameter + or else Is_Access_Type (Typ) + then + if Invariant_Checks_OK (Typ) then + Append_Enabled_Item + (Item => + Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)), + List => Stmts); end if; - end if; - return False; - end Is_Prologue_Renaming; + Add_Invariant_Access_Checks (Formal); - ------------------------- - -- Merge_Preconditions -- - ------------------------- + -- Note: we used to add predicate checks for OUT and IN OUT + -- formals here, but that was misguided, since such checks are + -- performed on the caller side, based on the predicate of the + -- actual, rather than the predicate of the formal. - procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is - function Expression_Arg (Prag : Node_Id) return Node_Id; - -- Return the boolean expression argument of a precondition while - -- updating its parentheses count for the subsequent merge. + end if; - function Message_Arg (Prag : Node_Id) return Node_Id; - -- Return the message argument of a precondition + Next_Formal (Formal); + end loop; + end Add_Invariant_And_Predicate_Checks; - -------------------- - -- Expression_Arg -- - -------------------- + ------------------------- + -- Append_Enabled_Item -- + ------------------------- - function Expression_Arg (Prag : Node_Id) return Node_Id is - Args : constant List_Id := Pragma_Argument_Associations (Prag); - Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args))); + procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is + begin + -- Do not chain ignored or disabled pragmas - begin - if Paren_Count (Arg) = 0 then - Set_Paren_Count (Arg, 1); - end if; + if Nkind (Item) = N_Pragma + and then (Is_Ignored (Item) or else Is_Disabled (Item)) + then + null; - return Arg; - end Expression_Arg; + -- Otherwise, add the item - ----------------- - -- Message_Arg -- - ----------------- + else + if No (List) then + List := New_List; + end if; - function Message_Arg (Prag : Node_Id) return Node_Id is - Args : constant List_Id := Pragma_Argument_Associations (Prag); - begin - return Get_Pragma_Arg (Last (Args)); - end Message_Arg; + -- If the pragma is a conjunct in a composite postcondition, it + -- has been processed in reverse order. In the postcondition body + -- it must appear before the others. - -- Local variables + if Nkind (Item) = N_Pragma + and then From_Aspect_Specification (Item) + and then Split_PPC (Item) + then + Prepend (Item, List); + else + Append (Item, List); + end if; + end if; + end Append_Enabled_Item; - From_Expr : constant Node_Id := Expression_Arg (From); - From_Msg : constant Node_Id := Message_Arg (From); - Into_Expr : constant Node_Id := Expression_Arg (Into); - Into_Msg : constant Node_Id := Message_Arg (Into); - Loc : constant Source_Ptr := Sloc (Into); + ------------------------------------ + -- Build_Postconditions_Procedure -- + ------------------------------------ - -- Start of processing for Merge_Preconditions + procedure Build_Postconditions_Procedure + (Subp_Id : Entity_Id; + Stmts : List_Id; + Result : Entity_Id) + is + procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id); + -- Insert node Stmt before the first source declaration of the + -- related subprogram's body. If no such declaration exists, Stmt + -- becomes the last declaration. + + -------------------------------------------- + -- Insert_Before_First_Source_Declaration -- + -------------------------------------------- + + procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is + Decls : constant List_Id := Declarations (Body_Decl); + Decl : Node_Id; begin - -- Merge the two preconditions by "or else"-ing them + -- Inspect the declarations of the related subprogram body looking + -- for the first source declaration. - Rewrite (Into_Expr, - Make_Or_Else (Loc, - Right_Opnd => Relocate_Node (Into_Expr), - Left_Opnd => From_Expr)); + if Present (Decls) then + Decl := First (Decls); + while Present (Decl) loop + if Comes_From_Source (Decl) then + Insert_Before (Decl, Stmt); + return; + end if; - -- Merge the two error messages to produce a single message of the - -- form: + Next (Decl); + end loop; - -- failed precondition from ... - -- also failed inherited precondition from ... + -- If we get there, then the subprogram body lacks any source + -- declarations. The body of _Postconditions now acts as the + -- last declaration. - if not Exception_Locations_Suppressed then - Start_String (Strval (Into_Msg)); - Store_String_Char (ASCII.LF); - Store_String_Chars (" also "); - Store_String_Chars (Strval (From_Msg)); + Append (Stmt, Decls); - Set_Strval (Into_Msg, End_String); + -- Ensure that the body has a declaration list + + else + Set_Declarations (Body_Decl, New_List (Stmt)); end if; - end Merge_Preconditions; + end Insert_Before_First_Source_Declaration; - ---------------------- - -- Prepend_To_Decls -- - ---------------------- + -- Local variables - procedure Prepend_To_Decls (Item : Node_Id) is - Decls : List_Id := Declarations (Body_Decl); + Loc : constant Source_Ptr := Sloc (Body_Decl); + Params : List_Id := No_List; + Proc_Bod : Node_Id; + Proc_Decl : Node_Id; + Proc_Id : Entity_Id; + Proc_Spec : Node_Id; - begin - -- Ensure that the body has a declarative list + -- Start of processing for Build_Postconditions_Procedure - if No (Decls) then - Decls := New_List; - Set_Declarations (Body_Decl, Decls); - end if; + begin + -- Nothing to do if there are no actions to check on exit - Prepend_To (Decls, Item); - end Prepend_To_Decls; + if No (Stmts) then + return; + end if; - ------------------------------ - -- Prepend_To_Decls_Or_Save -- - ------------------------------ + Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions); + Set_Debug_Info_Needed (Proc_Id); + Set_Postconditions_Proc (Subp_Id, Proc_Id); - procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is - Check_Prag : Node_Id; + -- Force the front-end inlining of _Postconditions when generating C + -- code, since its body may have references to itypes defined in the + -- enclosing subprogram, which would cause problems for unnesting + -- routines in the absence of inlining. - begin - Check_Prag := Build_Pragma_Check_Equivalent (Prag); + if Generate_C_Code then + Set_Has_Pragma_Inline (Proc_Id); + Set_Has_Pragma_Inline_Always (Proc_Id); + Set_Is_Inlined (Proc_Id); + end if; - -- Save the sole class-wide precondition (if any) for the next - -- step, where it will be merged with inherited preconditions. + -- The related subprogram is a function: create the specification of + -- parameter _Result. - if Class_Present (Prag) then - pragma Assert (No (Class_Pre)); - Class_Pre := Check_Prag; + if Present (Result) then + Params := New_List ( + Make_Parameter_Specification (Loc, + Defining_Identifier => Result, + Parameter_Type => + New_Occurrence_Of (Etype (Result), Loc))); + end if; - -- Accumulate the corresponding Check pragmas at the top of the - -- declarations. Prepending the items ensures that they will be - -- evaluated in their original order. + Proc_Spec := + Make_Procedure_Specification (Loc, + Defining_Unit_Name => Proc_Id, + Parameter_Specifications => Params); - else - if Present (Insert_Node) then - Insert_After (Insert_Node, Check_Prag); - else - Prepend_To_Decls (Check_Prag); - end if; + Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec); - Analyze (Check_Prag); - end if; - end Prepend_To_Decls_Or_Save; + -- Insert _Postconditions before the first source declaration of the + -- body. This ensures that the body will not cause any premature + -- freezing, as it may mention types: - ------------------------------------- - -- Process_Inherited_Preconditions -- - ------------------------------------- + -- procedure Proc (Obj : Array_Typ) is + -- procedure _postconditions is + -- begin + -- ... Obj ... + -- end _postconditions; - procedure Process_Inherited_Preconditions is - Subps : constant Subprogram_List := - Inherited_Subprograms (Spec_Id); - Check_Prag : Node_Id; - Items : Node_Id; - Prag : Node_Id; - Subp_Id : Entity_Id; + -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1)); + -- begin - begin - -- Process the contracts of all inherited subprograms, looking for - -- class-wide preconditions. + -- In the example above, Obj is of type T but the incorrect placement + -- of _Postconditions will cause a crash in gigi due to an out-of- + -- order reference. The body of _Postconditions must be placed after + -- the declaration of Temp to preserve correct visibility. - for Index in Subps'Range loop - Subp_Id := Subps (Index); - Items := Contract (Subp_Id); + Insert_Before_First_Source_Declaration (Proc_Decl); + Analyze (Proc_Decl); - if Present (Items) then - Prag := Pre_Post_Conditions (Items); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Precondition - and then Class_Present (Prag) - then - Check_Prag := - Build_Pragma_Check_Equivalent - (Prag => Prag, - Subp_Id => Spec_Id, - Inher_Id => Subp_Id); + -- Set an explicit End_Label to override the sloc of the implicit + -- RETURN statement, and prevent it from inheriting the sloc of one + -- the postconditions: this would cause confusing debug info to be + -- produced, interfering with coverage-analysis tools. + + Proc_Bod := + Make_Subprogram_Body (Loc, + Specification => + Copy_Subprogram_Spec (Proc_Spec), + Declarations => Empty_List, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => Stmts, + End_Label => Make_Identifier (Loc, Chars (Proc_Id)))); + + Insert_After_And_Analyze (Proc_Decl, Proc_Bod); + end Build_Postconditions_Procedure; + + ---------------------------- + -- Process_Contract_Cases -- + ---------------------------- + + procedure Process_Contract_Cases (Stmts : in out List_Id) is + procedure Process_Contract_Cases_For (Subp_Id : Entity_Id); + -- Process pragma Contract_Cases for subprogram Subp_Id + + -------------------------------- + -- Process_Contract_Cases_For -- + -------------------------------- + + procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is + Items : constant Node_Id := Contract (Subp_Id); + Prag : Node_Id; + + begin + if Present (Items) then + Prag := Contract_Test_Cases (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Contract_Cases then + Expand_Pragma_Contract_Cases + (CCs => Prag, + Subp_Id => Subp_Id, + Decls => Declarations (Body_Decl), + Stmts => Stmts); + end if; - -- The spec of an inherited subprogram already yielded - -- a class-wide precondition. Merge the existing - -- precondition with the current one using "or else". + Prag := Next_Pragma (Prag); + end loop; + end if; + end Process_Contract_Cases_For; - if Present (Class_Pre) then - Merge_Preconditions (Check_Prag, Class_Pre); - else - Class_Pre := Check_Prag; - end if; - end if; + -- Start of processing for Process_Contract_Cases - Prag := Next_Pragma (Prag); - end loop; - end if; - end loop; + begin + Process_Contract_Cases_For (Body_Id); - -- Add the merged class-wide preconditions + if Present (Spec_Id) then + Process_Contract_Cases_For (Spec_Id); + end if; + end Process_Contract_Cases; - if Present (Class_Pre) then - Prepend_To_Decls (Class_Pre); - Analyze (Class_Pre); - end if; - end Process_Inherited_Preconditions; + ---------------------------- + -- Process_Postconditions -- + ---------------------------- - ------------------------------- - -- Process_Preconditions_For -- - ------------------------------- + procedure Process_Postconditions (Stmts : in out List_Id) is + procedure Process_Body_Postconditions (Post_Nam : Name_Id); + -- Collect all [refined] postconditions of a specific kind denoted + -- by Post_Nam that belong to the body, and generate pragma Check + -- equivalents in list Stmts. - procedure Process_Preconditions_For (Subp_Id : Entity_Id) is - Items : constant Node_Id := Contract (Subp_Id); + procedure Process_Spec_Postconditions; + -- Collect all [inherited] postconditions of the spec, and generate + -- pragma Check equivalents in list Stmts. + + --------------------------------- + -- Process_Body_Postconditions -- + --------------------------------- + + procedure Process_Body_Postconditions (Post_Nam : Name_Id) is + Items : constant Node_Id := Contract (Body_Id); + Unit_Decl : constant Node_Id := Parent (Body_Decl); Decl : Node_Id; Prag : Node_Id; - Subp_Decl : Node_Id; begin -- Process the contract @@ -2274,33 +2358,32 @@ package body Contracts is if Present (Items) then Prag := Pre_Post_Conditions (Items); while Present (Prag) loop - if Pragma_Name (Prag) = Name_Precondition then - Prepend_To_Decls_Or_Save (Prag); + if Pragma_Name (Prag) = Post_Nam then + Append_Enabled_Item + (Item => Build_Pragma_Check_Equivalent (Prag), + List => Stmts); end if; Prag := Next_Pragma (Prag); end loop; end if; - -- The subprogram declaration being processed is actually a body - -- stub. The stub may carry a precondition pragma, in which case - -- it must be taken into account. The pragma appears after the - -- stub. - - Subp_Decl := Unit_Declaration_Node (Subp_Id); - - if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then - - -- Inspect the declarations following the body stub + -- The subprogram body being processed is actually the proper body + -- of a stub with a corresponding spec. The subprogram stub may + -- carry a postcondition pragma, in which case it must be taken + -- into account. The pragma appears after the stub. - Decl := Next (Subp_Decl); + if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then + Decl := Next (Corresponding_Stub (Unit_Decl)); while Present (Decl) loop -- Note that non-matching pragmas are skipped if Nkind (Decl) = N_Pragma then - if Pragma_Name (Decl) = Name_Precondition then - Prepend_To_Decls_Or_Save (Decl); + if Pragma_Name (Decl) = Post_Nam then + Append_Enabled_Item + (Item => Build_Pragma_Check_Equivalent (Decl), + List => Stmts); end if; -- Skip internally generated code @@ -2308,8 +2391,8 @@ package body Contracts is elsif not Comes_From_Source (Decl) then null; - -- Preconditions are usually grouped together. There is no - -- need to inspect the whole declarative list. + -- Postcondition pragmas are usually grouped together. There + -- is no need to inspect the whole declarative list. else exit; @@ -2318,926 +2401,766 @@ package body Contracts is Next (Decl); end loop; end if; - end Process_Preconditions_For; - - -- Local variables - - Decls : constant List_Id := Declarations (Body_Decl); - Decl : Node_Id; + end Process_Body_Postconditions; - -- Start of processing for Process_Preconditions + --------------------------------- + -- Process_Spec_Postconditions -- + --------------------------------- - begin - -- Find the proper insertion point for all pragma Check equivalents + procedure Process_Spec_Postconditions is + Subps : constant Subprogram_List := + Inherited_Subprograms (Spec_Id); + Items : Node_Id; + Prag : Node_Id; + Subp_Id : Entity_Id; - if Present (Decls) then - Decl := First (Decls); - while Present (Decl) loop + begin + -- Process the contract - -- First source declaration terminates the search, because all - -- preconditions must be evaluated prior to it, by definition. + Items := Contract (Spec_Id); - if Comes_From_Source (Decl) then - exit; + if Present (Items) then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Postcondition then + Append_Enabled_Item + (Item => Build_Pragma_Check_Equivalent (Prag), + List => Stmts); + end if; - -- Certain internally generated object renamings such as those - -- for discriminants and protection fields must be elaborated - -- before the preconditions are evaluated, as their expressions - -- may mention the discriminants. The renamings include those - -- for private components so we need to find the last such. + Prag := Next_Pragma (Prag); + end loop; + end if; - elsif Is_Prologue_Renaming (Decl) then - while Present (Next (Decl)) - and then Is_Prologue_Renaming (Next (Decl)) - loop - Next (Decl); - end loop; + -- Process the contracts of all inherited subprograms, looking for + -- class-wide postconditions. - Insert_Node := Decl; + for Index in Subps'Range loop + Subp_Id := Subps (Index); + Items := Contract (Subp_Id); - -- Otherwise the declaration does not come from source. This - -- also terminates the search, because internal code may raise - -- exceptions which should not preempt the preconditions. + if Present (Items) then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Postcondition + and then Class_Present (Prag) + then + Append_Enabled_Item + (Item => + Build_Pragma_Check_Equivalent + (Prag => Prag, + Subp_Id => Spec_Id, + Inher_Id => Subp_Id), + List => Stmts); + end if; - else - exit; + Prag := Next_Pragma (Prag); + end loop; end if; - - Next (Decl); end loop; - end if; + end Process_Spec_Postconditions; - -- The processing of preconditions is done in reverse order (body - -- first), because each pragma Check equivalent is inserted at the - -- top of the declarations. This ensures that the final order is - -- consistent with following diagram: + -- Start of processing for Process_Postconditions - -- - -- - -- + begin + -- The processing of postconditions is done in reverse order (body + -- first) to ensure the following arrangement: - Process_Preconditions_For (Body_Id); + -- + -- + -- + -- + + Process_Body_Postconditions (Name_Refined_Post); + Process_Body_Postconditions (Name_Postcondition); if Present (Spec_Id) then - Process_Preconditions_For (Spec_Id); - Process_Inherited_Preconditions; + Process_Spec_Postconditions; end if; - end Process_Preconditions; - - -- Local variables - - Restore_Scope : Boolean := False; - Result : Entity_Id; - Stmts : List_Id := No_List; - Subp_Id : Entity_Id; - - -- Start of processing for Expand_Subprogram_Contract - - begin - -- Obtain the entity of the initial declaration - - if Present (Spec_Id) then - Subp_Id := Spec_Id; - else - Subp_Id := Body_Id; - end if; - - -- Do not perform expansion activity when it is not needed - - if not Expander_Active then - return; - - -- ASIS requires an unaltered tree - - elsif ASIS_Mode then - return; - - -- GNATprove does not need the executable semantics of a contract - - elsif GNATprove_Mode then - return; - - -- The contract of a generic subprogram or one declared in a generic - -- context is not expanded, as the corresponding instance will provide - -- the executable semantics of the contract. - - elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then - return; - - -- All subprograms carry a contract, but for some it is not significant - -- and should not be processed. This is a small optimization. - - elsif not Has_Significant_Contract (Subp_Id) then - return; - - -- The contract of an ignored Ghost subprogram does not need expansion, - -- because the subprogram and all calls to it will be removed. + end Process_Postconditions; - elsif Is_Ignored_Ghost_Entity (Subp_Id) then - return; - end if; + --------------------------- + -- Process_Preconditions -- + --------------------------- - -- Do not re-expand the same contract. This scenario occurs when a - -- construct is rewritten into something else during its analysis - -- (expression functions for instance). + procedure Process_Preconditions is + Class_Pre : Node_Id := Empty; + -- The sole [inherited] class-wide precondition pragma that applies + -- to the subprogram. - if Has_Expanded_Contract (Subp_Id) then - return; + Insert_Node : Node_Id := Empty; + -- The insertion node after which all pragma Check equivalents are + -- inserted. - -- Otherwise mark the subprogram + function Is_Prologue_Renaming (Decl : Node_Id) return Boolean; + -- Determine whether arbitrary declaration Decl denotes a renaming of + -- a discriminant or protection field _object. - else - Set_Has_Expanded_Contract (Subp_Id); - end if; + procedure Merge_Preconditions (From : Node_Id; Into : Node_Id); + -- Merge two class-wide preconditions by "or else"-ing them. The + -- changes are accumulated in parameter Into. Update the error + -- message of Into. - -- Ensure that the formal parameters are visible when expanding all - -- contract items. + procedure Prepend_To_Decls (Item : Node_Id); + -- Prepend a single item to the declarations of the subprogram body - if not In_Open_Scopes (Subp_Id) then - Restore_Scope := True; - Push_Scope (Subp_Id); + procedure Prepend_To_Decls_Or_Save (Prag : Node_Id); + -- Save a class-wide precondition into Class_Pre, or prepend a normal + -- precondition to the declarations of the body and analyze it. - if Is_Generic_Subprogram (Subp_Id) then - Install_Generic_Formals (Subp_Id); - else - Install_Formals (Subp_Id); - end if; - end if; + procedure Process_Inherited_Preconditions; + -- Collect all inherited class-wide preconditions and merge them into + -- one big precondition to be evaluated as pragma Check. - -- The expansion of a subprogram contract involves the creation of Check - -- pragmas to verify the contract assertions of the spec and body in a - -- particular order. The order is as follows: + procedure Process_Preconditions_For (Subp_Id : Entity_Id); + -- Collect all preconditions of subprogram Subp_Id and prepend their + -- pragma Check equivalents to the declarations of the body. - -- function Example (...) return ... is - -- procedure _Postconditions (...) is - -- begin - -- - -- - -- - -- - -- - -- - -- - -- end _Postconditions; + -------------------------- + -- Is_Prologue_Renaming -- + -------------------------- - -- - -- - -- - -- + function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is + Nam : Node_Id; + Obj : Entity_Id; + Pref : Node_Id; + Sel : Node_Id; - -- - -- begin - -- + begin + if Nkind (Decl) = N_Object_Renaming_Declaration then + Obj := Defining_Entity (Decl); + Nam := Name (Decl); - -- _Preconditions (Result); - -- return Result; - -- end Example; + if Nkind (Nam) = N_Selected_Component then + Pref := Prefix (Nam); + Sel := Selector_Name (Nam); - -- Routine _Postconditions holds all contract assertions that must be - -- verified on exit from the related subprogram. + -- A discriminant renaming appears as + -- Discr : constant ... := Prefix.Discr; - -- Step 1: Handle all preconditions. This action must come before the - -- processing of pragma Contract_Cases because the pragma prepends items - -- to the body declarations. + if Ekind (Obj) = E_Constant + and then Is_Entity_Name (Sel) + and then Present (Entity (Sel)) + and then Ekind (Entity (Sel)) = E_Discriminant + then + return True; - Process_Preconditions; + -- A protection field renaming appears as + -- Prot : ... := _object._object; - -- Step 2: Handle all postconditions. This action must come before the - -- processing of pragma Contract_Cases because the pragma appends items - -- to list Stmts. + -- A renamed private component is just a component of + -- _object, with an arbitrary name. - Process_Postconditions (Stmts); + elsif Ekind (Obj) = E_Variable + and then Nkind (Pref) = N_Identifier + and then Chars (Pref) = Name_uObject + and then Nkind (Sel) = N_Identifier + then + return True; + end if; + end if; + end if; - -- Step 3: Handle pragma Contract_Cases. This action must come before - -- the processing of invariants and predicates because those append - -- items to list Stmts. + return False; + end Is_Prologue_Renaming; - Process_Contract_Cases (Stmts); + ------------------------- + -- Merge_Preconditions -- + ------------------------- - -- Step 4: Apply invariant and predicate checks on a function result and - -- all formals. The resulting checks are accumulated in list Stmts. + procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is + function Expression_Arg (Prag : Node_Id) return Node_Id; + -- Return the boolean expression argument of a precondition while + -- updating its parentheses count for the subsequent merge. - Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result); + function Message_Arg (Prag : Node_Id) return Node_Id; + -- Return the message argument of a precondition - -- Step 5: Construct procedure _Postconditions + -------------------- + -- Expression_Arg -- + -------------------- - Build_Postconditions_Procedure (Subp_Id, Stmts, Result); + function Expression_Arg (Prag : Node_Id) return Node_Id is + Args : constant List_Id := Pragma_Argument_Associations (Prag); + Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args))); - if Restore_Scope then - End_Scope; - end if; - end Expand_Subprogram_Contract; + begin + if Paren_Count (Arg) = 0 then + Set_Paren_Count (Arg, 1); + end if; - --------------------------------- - -- Inherit_Subprogram_Contract -- - --------------------------------- + return Arg; + end Expression_Arg; - procedure Inherit_Subprogram_Contract - (Subp : Entity_Id; - From_Subp : Entity_Id) - is - procedure Inherit_Pragma (Prag_Id : Pragma_Id); - -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to - -- Subp's contract. + ----------------- + -- Message_Arg -- + ----------------- - -------------------- - -- Inherit_Pragma -- - -------------------- + function Message_Arg (Prag : Node_Id) return Node_Id is + Args : constant List_Id := Pragma_Argument_Associations (Prag); + begin + return Get_Pragma_Arg (Last (Args)); + end Message_Arg; - procedure Inherit_Pragma (Prag_Id : Pragma_Id) is - Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id); - New_Prag : Node_Id; + -- Local variables - begin - -- A pragma cannot be part of more than one First_Pragma/Next_Pragma - -- chains, therefore the node must be replicated. The new pragma is - -- flagged as inherited for distinction purposes. + From_Expr : constant Node_Id := Expression_Arg (From); + From_Msg : constant Node_Id := Message_Arg (From); + Into_Expr : constant Node_Id := Expression_Arg (Into); + Into_Msg : constant Node_Id := Message_Arg (Into); + Loc : constant Source_Ptr := Sloc (Into); - if Present (Prag) then - New_Prag := New_Copy_Tree (Prag); - Set_Is_Inherited_Pragma (New_Prag); + -- Start of processing for Merge_Preconditions - Add_Contract_Item (New_Prag, Subp); - end if; - end Inherit_Pragma; + begin + -- Merge the two preconditions by "or else"-ing them - -- Start of processing for Inherit_Subprogram_Contract + Rewrite (Into_Expr, + Make_Or_Else (Loc, + Right_Opnd => Relocate_Node (Into_Expr), + Left_Opnd => From_Expr)); - begin - -- Inheritance is carried out only when both entities are subprograms - -- with contracts. + -- Merge the two error messages to produce a single message of the + -- form: - if Is_Subprogram_Or_Generic_Subprogram (Subp) - and then Is_Subprogram_Or_Generic_Subprogram (From_Subp) - and then Present (Contract (From_Subp)) - then - Inherit_Pragma (Pragma_Extensions_Visible); - end if; - end Inherit_Subprogram_Contract; + -- failed precondition from ... + -- also failed inherited precondition from ... - ------------------------------------- - -- Instantiate_Subprogram_Contract -- - ------------------------------------- + if not Exception_Locations_Suppressed then + Start_String (Strval (Into_Msg)); + Store_String_Char (ASCII.LF); + Store_String_Chars (" also "); + Store_String_Chars (Strval (From_Msg)); - procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is - procedure Instantiate_Pragmas (First_Prag : Node_Id); - -- Instantiate all contract-related source pragmas found in the list, - -- starting with pragma First_Prag. Each instantiated pragma is added - -- to list L. + Set_Strval (Into_Msg, End_String); + end if; + end Merge_Preconditions; - ------------------------- - -- Instantiate_Pragmas -- - ------------------------- + ---------------------- + -- Prepend_To_Decls -- + ---------------------- - procedure Instantiate_Pragmas (First_Prag : Node_Id) is - Inst_Prag : Node_Id; - Prag : Node_Id; + procedure Prepend_To_Decls (Item : Node_Id) is + Decls : List_Id := Declarations (Body_Decl); - begin - Prag := First_Prag; - while Present (Prag) loop - if Is_Generic_Contract_Pragma (Prag) then - Inst_Prag := - Copy_Generic_Node (Prag, Empty, Instantiating => True); + begin + -- Ensure that the body has a declarative list - Set_Analyzed (Inst_Prag, False); - Append_To (L, Inst_Prag); + if No (Decls) then + Decls := New_List; + Set_Declarations (Body_Decl, Decls); end if; - Prag := Next_Pragma (Prag); - end loop; - end Instantiate_Pragmas; - - -- Local variables + Prepend_To (Decls, Item); + end Prepend_To_Decls; - Items : constant Node_Id := Contract (Defining_Entity (Templ)); + ------------------------------ + -- Prepend_To_Decls_Or_Save -- + ------------------------------ - -- Start of processing for Instantiate_Subprogram_Contract + procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is + Check_Prag : Node_Id; - begin - if Present (Items) then - Instantiate_Pragmas (Pre_Post_Conditions (Items)); - Instantiate_Pragmas (Contract_Test_Cases (Items)); - Instantiate_Pragmas (Classifications (Items)); - end if; - end Instantiate_Subprogram_Contract; + begin + Check_Prag := Build_Pragma_Check_Equivalent (Prag); - ---------------------------------------- - -- Save_Global_References_In_Contract -- - ---------------------------------------- + -- Save the sole class-wide precondition (if any) for the next + -- step, where it will be merged with inherited preconditions. - procedure Save_Global_References_In_Contract - (Templ : Node_Id; - Gen_Id : Entity_Id) - is - procedure Save_Global_References_In_List (First_Prag : Node_Id); - -- Save all global references in contract-related source pragmas found - -- in the list, starting with pragma First_Prag. + if Class_Present (Prag) then + pragma Assert (No (Class_Pre)); + Class_Pre := Check_Prag; - ------------------------------------ - -- Save_Global_References_In_List -- - ------------------------------------ + -- Accumulate the corresponding Check pragmas at the top of the + -- declarations. Prepending the items ensures that they will be + -- evaluated in their original order. - procedure Save_Global_References_In_List (First_Prag : Node_Id) is - Prag : Node_Id; + else + if Present (Insert_Node) then + Insert_After (Insert_Node, Check_Prag); + else + Prepend_To_Decls (Check_Prag); + end if; - begin - Prag := First_Prag; - while Present (Prag) loop - if Is_Generic_Contract_Pragma (Prag) then - Save_Global_References (Prag); + Analyze (Check_Prag); end if; + end Prepend_To_Decls_Or_Save; - Prag := Next_Pragma (Prag); - end loop; - end Save_Global_References_In_List; - - -- Local variables + ------------------------------------- + -- Process_Inherited_Preconditions -- + ------------------------------------- - Items : constant Node_Id := Contract (Defining_Entity (Templ)); + procedure Process_Inherited_Preconditions is + Subps : constant Subprogram_List := + Inherited_Subprograms (Spec_Id); + Check_Prag : Node_Id; + Items : Node_Id; + Prag : Node_Id; + Subp_Id : Entity_Id; - -- Start of processing for Save_Global_References_In_Contract + begin + -- Process the contracts of all inherited subprograms, looking for + -- class-wide preconditions. - begin - -- The entity of the analyzed generic copy must be on the scope stack - -- to ensure proper detection of global references. + for Index in Subps'Range loop + Subp_Id := Subps (Index); + Items := Contract (Subp_Id); - Push_Scope (Gen_Id); + if Present (Items) then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Precondition + and then Class_Present (Prag) + then + Check_Prag := + Build_Pragma_Check_Equivalent + (Prag => Prag, + Subp_Id => Spec_Id, + Inher_Id => Subp_Id); - if Permits_Aspect_Specifications (Templ) - and then Has_Aspects (Templ) - then - Save_Global_References_In_Aspects (Templ); - end if; + -- The spec of an inherited subprogram already yielded + -- a class-wide precondition. Merge the existing + -- precondition with the current one using "or else". - if Present (Items) then - Save_Global_References_In_List (Pre_Post_Conditions (Items)); - Save_Global_References_In_List (Contract_Test_Cases (Items)); - Save_Global_References_In_List (Classifications (Items)); - end if; + if Present (Class_Pre) then + Merge_Preconditions (Check_Prag, Class_Pre); + else + Class_Pre := Check_Prag; + end if; + end if; - Pop_Scope; - end Save_Global_References_In_Contract; + Prag := Next_Pragma (Prag); + end loop; + end if; + end loop; - ------------------------------------------------- - -- Build_And_Analyze_Contract_Only_Subprograms -- - ------------------------------------------------- + -- Add the merged class-wide preconditions - procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is - procedure Analyze_Contract_Only_Subprograms (L : List_Id); - -- Analyze the contract-only subprograms of L + if Present (Class_Pre) then + Prepend_To_Decls (Class_Pre); + Analyze (Class_Pre); + end if; + end Process_Inherited_Preconditions; - procedure Append_Contract_Only_Subprograms (Subp_List : List_Id); - -- Append the contract-only bodies of Subp_List to its declarations list + ------------------------------- + -- Process_Preconditions_For -- + ------------------------------- - function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id; - -- If E is an entity for a non-imported subprogram specification with - -- pre/postconditions and we are compiling with CodePeer mode, then this - -- procedure will create a wrapper to help Gnat2scil process its - -- contracts. Return Empty if the wrapper cannot be built. + procedure Process_Preconditions_For (Subp_Id : Entity_Id) is + Items : constant Node_Id := Contract (Subp_Id); + Decl : Node_Id; + Prag : Node_Id; + Subp_Decl : Node_Id; - function Build_Contract_Only_Subprograms (L : List_Id) return List_Id; - -- Build the contract-only subprograms of all eligible subprograms found - -- in list L. + begin + -- Process the contract - function Has_Private_Declarations (N : Node_Id) return Boolean; - -- Return True for package specs, task definitions, and protected type - -- definitions whose list of private declarations is not empty. + if Present (Items) then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Precondition then + Prepend_To_Decls_Or_Save (Prag); + end if; - --------------------------------------- - -- Analyze_Contract_Only_Subprograms -- - --------------------------------------- + Prag := Next_Pragma (Prag); + end loop; + end if; - procedure Analyze_Contract_Only_Subprograms (L : List_Id) is - procedure Analyze_Contract_Only_Bodies; - -- Analyze all the contract-only bodies of L + -- The subprogram declaration being processed is actually a body + -- stub. The stub may carry a precondition pragma, in which case + -- it must be taken into account. The pragma appears after the + -- stub. - ---------------------------------- - -- Analyze_Contract_Only_Bodies -- - ---------------------------------- + Subp_Decl := Unit_Declaration_Node (Subp_Id); - procedure Analyze_Contract_Only_Bodies is - Decl : Node_Id; + if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then - begin - Decl := First (L); - while Present (Decl) loop - if Nkind (Decl) = N_Subprogram_Body - and then Is_Contract_Only_Body - (Defining_Unit_Name (Specification (Decl))) - then - Analyze (Decl); - end if; + -- Inspect the declarations following the body stub - Next (Decl); - end loop; - end Analyze_Contract_Only_Bodies; + Decl := Next (Subp_Decl); + while Present (Decl) loop - -- Start of processing for Analyze_Contract_Only_Subprograms + -- Note that non-matching pragmas are skipped - begin - if Ekind (Current_Scope) /= E_Package then - Analyze_Contract_Only_Bodies; + if Nkind (Decl) = N_Pragma then + if Pragma_Name (Decl) = Name_Precondition then + Prepend_To_Decls_Or_Save (Decl); + end if; - else - declare - Pkg_Spec : constant Node_Id := - Package_Specification (Current_Scope); + -- Skip internally generated code - begin - if not Has_Private_Declarations (Pkg_Spec) then - Analyze_Contract_Only_Bodies; + elsif not Comes_From_Source (Decl) then + null; - -- For packages with private declarations, the contract-only - -- bodies of subprograms defined in the visible part of the - -- package are added to its private declarations (to ensure - -- that they do not cause premature freezing of types and also - -- that they are analyzed with proper visibility). Hence they - -- will be analyzed later. + -- Preconditions are usually grouped together. There is no + -- need to inspect the whole declarative list. - elsif Visible_Declarations (Pkg_Spec) = L then - null; + else + exit; + end if; - elsif Private_Declarations (Pkg_Spec) = L then - Analyze_Contract_Only_Bodies; - end if; - end; - end if; - end Analyze_Contract_Only_Subprograms; + Next (Decl); + end loop; + end if; + end Process_Preconditions_For; - -------------------------------------- - -- Append_Contract_Only_Subprograms -- - -------------------------------------- + -- Local variables - procedure Append_Contract_Only_Subprograms (Subp_List : List_Id) is - begin - if No (Subp_List) then - return; - end if; + Decls : constant List_Id := Declarations (Body_Decl); + Decl : Node_Id; - if Ekind (Current_Scope) /= E_Package then - Append_List (Subp_List, To => L); + -- Start of processing for Process_Preconditions - else - declare - Pkg_Spec : constant Node_Id := - Package_Specification (Current_Scope); + begin + -- Find the proper insertion point for all pragma Check equivalents - begin - if not Has_Private_Declarations (Pkg_Spec) then - Append_List (Subp_List, To => L); + if Present (Decls) then + Decl := First (Decls); + while Present (Decl) loop - -- If the package has private declarations then append them to - -- its private declarations; they will be analyzed when the - -- contracts of its private declarations are analyzed. + -- First source declaration terminates the search, because all + -- preconditions must be evaluated prior to it, by definition. - else - Append_List - (List => Subp_List, - To => Private_Declarations (Pkg_Spec)); - end if; - end; - end if; - end Append_Contract_Only_Subprograms; + if Comes_From_Source (Decl) then + exit; - ------------------------------------ - -- Build_Contract_Only_Subprogram -- - ------------------------------------ + -- Certain internally generated object renamings such as those + -- for discriminants and protection fields must be elaborated + -- before the preconditions are evaluated, as their expressions + -- may mention the discriminants. The renamings include those + -- for private components so we need to find the last such. - -- This procedure takes care of building a wrapper to generate better - -- analysis results in the case of a call to a subprogram whose body - -- is unavailable to CodePeer but whose specification includes Pre/Post - -- conditions. The body might be unavailable for any of a number or - -- reasons (it is imported, the .adb file is simply missing, or the - -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis) - -- pragma). The built subprogram has the following contents: - -- * check preconditions - -- * call the subprogram - -- * check postconditions + elsif Is_Prologue_Renaming (Decl) then + while Present (Next (Decl)) + and then Is_Prologue_Renaming (Next (Decl)) + loop + Next (Decl); + end loop; - function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id is - Loc : constant Source_Ptr := Sloc (E); + Insert_Node := Decl; - function Build_Missing_Body_Decls return List_Id; - -- Build the declaration of the missing body subprogram and its - -- corresponding pragma Import. + -- Otherwise the declaration does not come from source. This + -- also terminates the search, because internal code may raise + -- exceptions which should not preempt the preconditions. - function Build_Missing_Body_Subprogram_Call return Node_Id; - -- Build the call to the missing body subprogram + else + exit; + end if; - function Copy_Original_Specification - (Loc : Source_Ptr; - Spec : Node_Id) return Node_Id; - -- Build a copy of the original specification of the given subprogram - -- specification. + Next (Decl); + end loop; + end if; - function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean; - -- Return True if E is a subprogram declared in a nested package that - -- has some formal or return type depending on a private type defined - -- in an enclosing package. + -- The processing of preconditions is done in reverse order (body + -- first), because each pragma Check equivalent is inserted at the + -- top of the declarations. This ensures that the final order is + -- consistent with following diagram: - ------------------------------ - -- Build_Missing_Body_Decls -- - ------------------------------ + -- + -- + -- - function Build_Missing_Body_Decls return List_Id is - Name : constant Name_Id := Get_Contract_Only_Missing_Body_Name (E); - Spec : constant Node_Id := Declaration_Node (E); - Decl : Node_Id; - Prag : Node_Id; + Process_Preconditions_For (Body_Id); - begin - Decl := Make_Subprogram_Declaration (Loc, - Copy_Original_Specification (Loc, Spec)); - Set_Chars (Defining_Unit_Name (Specification (Decl)), Name); + if Present (Spec_Id) then + Process_Preconditions_For (Spec_Id); + Process_Inherited_Preconditions; + end if; + end Process_Preconditions; - Prag := - Make_Pragma (Loc, - Chars => Name_Import, - Pragma_Argument_Associations => New_List ( - Make_Pragma_Argument_Association (Loc, - Expression => Make_Identifier (Loc, Name_Ada)), + -- Local variables - Make_Pragma_Argument_Association (Loc, - Expression => Make_Identifier (Loc, Name)))); + Restore_Scope : Boolean := False; + Result : Entity_Id; + Stmts : List_Id := No_List; + Subp_Id : Entity_Id; - return New_List (Decl, Prag); - end Build_Missing_Body_Decls; + -- Start of processing for Expand_Subprogram_Contract - ---------------------------------------- - -- Build_Missing_Body_Subprogram_Call -- - ---------------------------------------- + begin + -- Obtain the entity of the initial declaration - function Build_Missing_Body_Subprogram_Call return Node_Id is - Forml : Entity_Id; - Parms : List_Id; + if Present (Spec_Id) then + Subp_Id := Spec_Id; + else + Subp_Id := Body_Id; + end if; - begin - -- Build parameter list that we need + -- Do not perform expansion activity when it is not needed - Parms := New_List; - Forml := First_Formal (E); - while Present (Forml) loop - Append_To (Parms, Make_Identifier (Loc, Chars (Forml))); - Next_Formal (Forml); - end loop; + if not Expander_Active then + return; - -- Build the call to the missing body subprogram + -- ASIS requires an unaltered tree - if Ekind_In (E, E_Function, E_Generic_Function) then - return - Make_Simple_Return_Statement (Loc, - Expression => - Make_Function_Call (Loc, - Name => Make_Identifier (Loc, - Get_Contract_Only_Missing_Body_Name (E)), - Parameter_Associations => Parms)); + elsif ASIS_Mode then + return; - else - return - Make_Procedure_Call_Statement (Loc, - Name => Make_Identifier (Loc, - Get_Contract_Only_Missing_Body_Name (E)), - Parameter_Associations => Parms); - end if; - end Build_Missing_Body_Subprogram_Call; + -- GNATprove does not need the executable semantics of a contract - --------------------------------- - -- Copy_Original_Specification -- - --------------------------------- + elsif GNATprove_Mode then + return; - function Copy_Original_Specification - (Loc : Source_Ptr; - Spec : Node_Id) return Node_Id - is - function Copy_Original_Type (N : Node_Id) return Node_Id; - -- Duplicate the original type of a given formal or function - -- result type. + -- The contract of a generic subprogram or one declared in a generic + -- context is not expanded, as the corresponding instance will provide + -- the executable semantics of the contract. - function Copy_Original_Type (N : Node_Id) return Node_Id is - begin - -- For expanded names located in instantiations, copy them with - -- semantic information (avoids visibility problems). + elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then + return; - if In_Instance - and then Nkind (N) = N_Expanded_Name - then - return New_Copy_Tree (N); - else - return Copy_Separate_Tree (Original_Node (N)); - end if; - end Copy_Original_Type; + -- All subprograms carry a contract, but for some it is not significant + -- and should not be processed. This is a small optimization. - -- Local variables + elsif not Has_Significant_Contract (Subp_Id) then + return; - Current_Parameter : Node_Id; - Current_Identifier : Entity_Id; - Current_Type : Node_Id; - New_Identifier : Entity_Id; - Parameters : List_Id := No_List; + -- The contract of an ignored Ghost subprogram does not need expansion, + -- because the subprogram and all calls to it will be removed. - -- Start of processing for Copy_Original_Specification + elsif Is_Ignored_Ghost_Entity (Subp_Id) then + return; + end if; - begin - if Present (Parameter_Specifications (Spec)) then - Parameters := New_List; - Current_Parameter := First (Parameter_Specifications (Spec)); - while Present (Current_Parameter) loop - Current_Identifier := - Defining_Identifier (Current_Parameter); - Current_Type := - Copy_Original_Type (Parameter_Type (Current_Parameter)); - - New_Identifier := Make_Defining_Identifier (Loc, - Chars (Current_Identifier)); - - Append_To (Parameters, - Make_Parameter_Specification (Loc, - Defining_Identifier => New_Identifier, - Parameter_Type => Current_Type, - In_Present => In_Present (Current_Parameter), - Out_Present => Out_Present (Current_Parameter), - Expression => - Copy_Separate_Tree (Expression (Current_Parameter)))); - - Next (Current_Parameter); - end loop; - end if; + -- Do not re-expand the same contract. This scenario occurs when a + -- construct is rewritten into something else during its analysis + -- (expression functions for instance). - case Nkind (Spec) is - when N_Function_Specification => - return - Make_Function_Specification (Loc, - Defining_Unit_Name => - Make_Defining_Identifier (Loc, - Chars => Chars (Defining_Unit_Name (Spec))), - Parameter_Specifications => Parameters, - Result_Definition => - Copy_Original_Type (Result_Definition (Spec))); - - when N_Procedure_Specification => - return - Make_Procedure_Specification (Loc, - Defining_Unit_Name => - Make_Defining_Identifier (Loc, - Chars => Chars (Defining_Unit_Name (Spec))), - Parameter_Specifications => Parameters); - - when others => - raise Program_Error; - end case; - end Copy_Original_Specification; + if Has_Expanded_Contract (Subp_Id) then + return; - ----------------------------------- - -- Skip_Contract_Only_Subprogram -- - ----------------------------------- + -- Otherwise mark the subprogram - function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean - is - function Depends_On_Enclosing_Private_Type return Boolean; - -- Return True if some formal of E (or its return type) are - -- private types defined in an enclosing package. + else + Set_Has_Expanded_Contract (Subp_Id); + end if; - function Some_Enclosing_Package_Has_Private_Decls return Boolean; - -- Return True if some enclosing package of the current scope has - -- private declarations. + -- Ensure that the formal parameters are visible when expanding all + -- contract items. - --------------------------------------- - -- Depends_On_Enclosing_Private_Type -- - --------------------------------------- + if not In_Open_Scopes (Subp_Id) then + Restore_Scope := True; + Push_Scope (Subp_Id); - function Depends_On_Enclosing_Private_Type return Boolean is + if Is_Generic_Subprogram (Subp_Id) then + Install_Generic_Formals (Subp_Id); + else + Install_Formals (Subp_Id); + end if; + end if; - function Defined_In_Enclosing_Package - (Typ : Entity_Id) return Boolean; - -- Return True if Typ is an entity defined in an enclosing - -- package of the current scope. + -- The expansion of a subprogram contract involves the creation of Check + -- pragmas to verify the contract assertions of the spec and body in a + -- particular order. The order is as follows: - ---------------------------------- - -- Defined_In_Enclosing_Package -- - ---------------------------------- + -- function Example (...) return ... is + -- procedure _Postconditions (...) is + -- begin + -- + -- + -- + -- + -- + -- + -- + -- end _Postconditions; - function Defined_In_Enclosing_Package - (Typ : Entity_Id) return Boolean - is - Scop : Entity_Id := Scope (Current_Scope); + -- + -- + -- + -- - begin - while Scop /= Scope (Typ) - and then not Is_Compilation_Unit (Scop) - loop - Scop := Scope (Scop); - end loop; + -- + -- begin + -- - return Scop = Scope (Typ); - end Defined_In_Enclosing_Package; + -- _Preconditions (Result); + -- return Result; + -- end Example; - -- Local variables + -- Routine _Postconditions holds all contract assertions that must be + -- verified on exit from the related subprogram. - Param_E : Entity_Id; - Typ : Entity_Id; - begin - Param_E := First_Entity (E); - while Present (Param_E) loop - Typ := Etype (Param_E); + -- Step 1: Handle all preconditions. This action must come before the + -- processing of pragma Contract_Cases because the pragma prepends items + -- to the body declarations. - if Is_Private_Type (Typ) - and then Defined_In_Enclosing_Package (Typ) - then - return True; - end if; + Process_Preconditions; + + -- Step 2: Handle all postconditions. This action must come before the + -- processing of pragma Contract_Cases because the pragma appends items + -- to list Stmts. - Next_Entity (Param_E); - end loop; + Process_Postconditions (Stmts); - return Ekind (E) = E_Function - and then Is_Private_Type (Etype (E)) - and then Defined_In_Enclosing_Package (Etype (E)); - end Depends_On_Enclosing_Private_Type; + -- Step 3: Handle pragma Contract_Cases. This action must come before + -- the processing of invariants and predicates because those append + -- items to list Stmts. - ---------------------------------------------- - -- Some_Enclosing_Package_Has_Private_Decls -- - ---------------------------------------------- + Process_Contract_Cases (Stmts); - function Some_Enclosing_Package_Has_Private_Decls return Boolean is - Scop : Entity_Id := Current_Scope; - Pkg_Spec : Node_Id := Package_Specification (Scop); + -- Step 4: Apply invariant and predicate checks on a function result and + -- all formals. The resulting checks are accumulated in list Stmts. - begin - loop - if Ekind (Scop) = E_Package - and then - Has_Private_Declarations (Package_Specification (Scop)) - then - Pkg_Spec := Package_Specification (Scop); - end if; + Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result); - exit when Is_Compilation_Unit (Scop); - Scop := Scope (Scop); - end loop; + -- Step 5: Construct procedure _Postconditions - return Pkg_Spec /= Package_Specification (Current_Scope); - end Some_Enclosing_Package_Has_Private_Decls; + Build_Postconditions_Procedure (Subp_Id, Stmts, Result); - -- Start of processing for Skip_Contract_Only_Subprogram + if Restore_Scope then + End_Scope; + end if; + end Expand_Subprogram_Contract; - begin - if Ekind (Current_Scope) = E_Package - and then Some_Enclosing_Package_Has_Private_Decls - and then Depends_On_Enclosing_Private_Type - then - if Debug_Flag_Dot_KK then - declare - Saved_Mode : constant Warning_Mode_Type := Warning_Mode; + --------------------------------- + -- Inherit_Subprogram_Contract -- + --------------------------------- - begin - -- Warnings are disabled by default under CodePeer_Mode - -- (see switch-c). Enable them temporarily. + procedure Inherit_Subprogram_Contract + (Subp : Entity_Id; + From_Subp : Entity_Id) + is + procedure Inherit_Pragma (Prag_Id : Pragma_Id); + -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to + -- Subp's contract. - Warning_Mode := Normal; - Error_Msg_N - ("cannot generate contract-only subprogram?", E); - Warning_Mode := Saved_Mode; - end; - end if; + -------------------- + -- Inherit_Pragma -- + -------------------- - return True; - end if; + procedure Inherit_Pragma (Prag_Id : Pragma_Id) is + Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id); + New_Prag : Node_Id; - return False; - end Skip_Contract_Only_Subprogram; + begin + -- A pragma cannot be part of more than one First_Pragma/Next_Pragma + -- chains, therefore the node must be replicated. The new pragma is + -- flagged as inherited for distinction purposes. - -- Start of processing for Build_Contract_Only_Subprogram + if Present (Prag) then + New_Prag := New_Copy_Tree (Prag); + Set_Is_Inherited_Pragma (New_Prag); - begin - -- Test cases where the wrapper is not needed and cases where we - -- cannot build the wrapper. - - if not CodePeer_Mode - or else Inside_A_Generic - or else not Is_Subprogram (E) - or else Is_Abstract_Subprogram (E) - or else Is_Imported (E) - or else No (Contract (E)) - or else No (Pre_Post_Conditions (Contract (E))) - or else Is_Contract_Only_Body (E) - or else Skip_Contract_Only_Subprogram (E) - or else Convention (E) = Convention_Protected - then - return Empty; + Add_Contract_Item (New_Prag, Subp); end if; + end Inherit_Pragma; - -- Note on calls to Copy_Separate_Tree. The trees we are copying - -- here are fully analyzed, but we definitely want fully syntactic - -- unanalyzed trees in the body we construct, so that the analysis - -- generates the right visibility, and that is exactly what the - -- calls to Copy_Separate_Tree give us. + -- Start of processing for Inherit_Subprogram_Contract - declare - Name : constant Name_Id := Get_Contract_Only_Body_Name (E); - Id : Entity_Id; - Bod : Node_Id; + begin + -- Inheritance is carried out only when both entities are subprograms + -- with contracts. - begin - Bod := - Make_Subprogram_Body (Loc, - Specification => - Copy_Original_Specification (Loc, Declaration_Node (E)), - Declarations => - Build_Missing_Body_Decls, - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => New_List ( - Build_Missing_Body_Subprogram_Call), - End_Label => Make_Identifier (Loc, Name))); + if Is_Subprogram_Or_Generic_Subprogram (Subp) + and then Is_Subprogram_Or_Generic_Subprogram (From_Subp) + and then Present (Contract (From_Subp)) + then + Inherit_Pragma (Pragma_Extensions_Visible); + end if; + end Inherit_Subprogram_Contract; - Id := Defining_Unit_Name (Specification (Bod)); + ------------------------------------- + -- Instantiate_Subprogram_Contract -- + ------------------------------------- - -- Copy only the pre/postconditions of the original contract - -- since it is what we need, but also because pragmas stored in - -- the other fields have N_Pragmas with N_Aspect_Specifications - -- that reference their associated pragma (thus causing an endless - -- loop when trying to copy the subtree). + procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is + procedure Instantiate_Pragmas (First_Prag : Node_Id); + -- Instantiate all contract-related source pragmas found in the list, + -- starting with pragma First_Prag. Each instantiated pragma is added + -- to list L. - declare - New_Contract : constant Node_Id := Make_Contract (Sloc (E)); + ------------------------- + -- Instantiate_Pragmas -- + ------------------------- - begin - Set_Pre_Post_Conditions (New_Contract, - Copy_Separate_Tree (Pre_Post_Conditions (Contract (E)))); - Set_Contract (Id, New_Contract); - end; + procedure Instantiate_Pragmas (First_Prag : Node_Id) is + Inst_Prag : Node_Id; + Prag : Node_Id; - -- Fix the name of this new subprogram and link the original - -- subprogram with its Contract_Only_Body subprogram. + begin + Prag := First_Prag; + while Present (Prag) loop + if Is_Generic_Contract_Pragma (Prag) then + Inst_Prag := + Copy_Generic_Node (Prag, Empty, Instantiating => True); - Set_Chars (Id, Name); - Set_Is_Contract_Only_Body (Id); - Set_Contract_Only_Body (E, Id); + Set_Analyzed (Inst_Prag, False); + Append_To (L, Inst_Prag); + end if; - return Bod; - end; - end Build_Contract_Only_Subprogram; + Prag := Next_Pragma (Prag); + end loop; + end Instantiate_Pragmas; - ------------------------------------- - -- Build_Contract_Only_Subprograms -- - ------------------------------------- + -- Local variables - function Build_Contract_Only_Subprograms (L : List_Id) return List_Id is - Decl : Node_Id; - Subp_Id : Entity_Id; - New_Subp : Node_Id; - Result : List_Id := No_List; + Items : constant Node_Id := Contract (Defining_Entity (Templ)); - begin - Decl := First (L); - while Present (Decl) loop - if Nkind (Decl) = N_Subprogram_Declaration then - Subp_Id := Defining_Unit_Name (Specification (Decl)); - New_Subp := Build_Contract_Only_Subprogram (Subp_Id); + -- Start of processing for Instantiate_Subprogram_Contract - if Present (New_Subp) then - if No (Result) then - Result := New_List; - end if; + begin + if Present (Items) then + Instantiate_Pragmas (Pre_Post_Conditions (Items)); + Instantiate_Pragmas (Contract_Test_Cases (Items)); + Instantiate_Pragmas (Classifications (Items)); + end if; + end Instantiate_Subprogram_Contract; - Append_To (Result, New_Subp); - end if; - end if; + ---------------------------------------- + -- Save_Global_References_In_Contract -- + ---------------------------------------- - Next (Decl); - end loop; + procedure Save_Global_References_In_Contract + (Templ : Node_Id; + Gen_Id : Entity_Id) + is + procedure Save_Global_References_In_List (First_Prag : Node_Id); + -- Save all global references in contract-related source pragmas found + -- in the list, starting with pragma First_Prag. - return Result; - end Build_Contract_Only_Subprograms; + ------------------------------------ + -- Save_Global_References_In_List -- + ------------------------------------ - ------------------------------ - -- Has_Private_Declarations -- - ------------------------------ + procedure Save_Global_References_In_List (First_Prag : Node_Id) is + Prag : Node_Id; - function Has_Private_Declarations (N : Node_Id) return Boolean is begin - if not Nkind_In (N, N_Package_Specification, - N_Task_Definition, - N_Protected_Definition) - then - return False; - else - return Present (Private_Declarations (N)) - and then Is_Non_Empty_List (Private_Declarations (N)); - end if; - end Has_Private_Declarations; + Prag := First_Prag; + while Present (Prag) loop + if Is_Generic_Contract_Pragma (Prag) then + Save_Global_References (Prag); + end if; + + Prag := Next_Pragma (Prag); + end loop; + end Save_Global_References_In_List; -- Local variables - Subp_List : List_Id; + Items : constant Node_Id := Contract (Defining_Entity (Templ)); - -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms + -- Start of processing for Save_Global_References_In_Contract begin - Subp_List := Build_Contract_Only_Subprograms (L); - Append_Contract_Only_Subprograms (Subp_List); - Analyze_Contract_Only_Subprograms (L); - end Build_And_Analyze_Contract_Only_Subprograms; + -- The entity of the analyzed generic copy must be on the scope stack + -- to ensure proper detection of global references. + + Push_Scope (Gen_Id); + + if Permits_Aspect_Specifications (Templ) + and then Has_Aspects (Templ) + then + Save_Global_References_In_Aspects (Templ); + end if; + + if Present (Items) then + Save_Global_References_In_List (Pre_Post_Conditions (Items)); + Save_Global_References_In_List (Contract_Test_Cases (Items)); + Save_Global_References_In_List (Classifications (Items)); + end if; + + Pop_Scope; + end Save_Global_References_In_Contract; end Contracts; diff --git a/gcc/ada/scil_ll.adb b/gcc/ada/scil_ll.adb index eed0d1a5b42..bf9ded7d261 100644 --- a/gcc/ada/scil_ll.adb +++ b/gcc/ada/scil_ll.adb @@ -35,13 +35,6 @@ with Sinfo; use Sinfo; with System.HTable; use System.HTable; package body SCIL_LL is - Contract_Only_Body_Suffix : constant String := "__contract_only"; - -- Suffix of Contract_Only_Body subprograms internally built only under - -- CodePeer mode - - Contract_Only_Missing_Body_Suffix : constant String := "__missing_body"; - -- Suffix of Contract_Only_Missing_Body subprograms internally built only - -- under CodePeer mode procedure Copy_SCIL_Node (Target : Node_Id; Source : Node_Id); -- Copy the SCIL field from Source to Target (it is used as the argument @@ -108,27 +101,6 @@ package body SCIL_LL is end if; end Get_Contract_Only_Body; - --------------------------------- - -- Get_Contract_Only_Body_Name -- - --------------------------------- - - function Get_Contract_Only_Body_Name (E : Entity_Id) return Name_Id is - begin - return Name_Find (Get_Name_String (Chars (E)) & - Contract_Only_Body_Suffix); - end Get_Contract_Only_Body_Name; - - ----------------------------------------- - -- Get_Contract_Only_Missing_Body_Name -- - ----------------------------------------- - - function Get_Contract_Only_Missing_Body_Name (E : Entity_Id) - return Name_Id is - begin - return Name_Find (Get_Name_String (Chars (E)) & - Contract_Only_Missing_Body_Suffix); - end Get_Contract_Only_Missing_Body_Name; - ------------------- -- Get_SCIL_Node -- ------------------- diff --git a/gcc/ada/scil_ll.ads b/gcc/ada/scil_ll.ads index bfac1a05e4d..bebe0e7ffa7 100644 --- a/gcc/ada/scil_ll.ads +++ b/gcc/ada/scil_ll.ads @@ -32,17 +32,10 @@ -- This package extends the tree nodes with fields that are used to reference -- the SCIL node and the Contract_Only_Body of a subprogram with aspects. -with Namet; use Namet; with Types; use Types; package SCIL_LL is - function Get_Contract_Only_Body_Name (E : Entity_Id) return Name_Id; - -- Return the name of the Contract_Only_Body subprogram of E - - function Get_Contract_Only_Missing_Body_Name (E : Entity_Id) return Name_Id; - -- Return the name of the Contract_Only_Missing_Body subprogram of E - function Get_Contract_Only_Body (N : Node_Id) return Node_Id; -- Read the value of attribute Contract_Only_Body -- 2.30.2