diff options
Diffstat (limited to 'gcc/ada/contracts.adb')
| -rw-r--r-- | gcc/ada/contracts.adb | 575 |
1 files changed, 574 insertions, 1 deletions
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index fbfc684..e4e25bf 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -25,6 +25,7 @@ with Aspects; use Aspects; with Atree; use Atree; +with Debug; use Debug; with Einfo; use Einfo; with Elists; use Elists; with Errout; use Errout; @@ -47,10 +48,16 @@ with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; with Snames; use Snames; with Stringt; use Stringt; +with SCIL_LL; use SCIL_LL; 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; @@ -345,6 +352,10 @@ package body Contracts is procedure Analyze_Contracts (L : List_Id) is begin + if CodePeer_Mode and then Debug_Flag_Dot_KK then + Build_And_Analyze_Contract_Only_Subprograms (L); + end if; + Analyze_Contracts (L, Freeze_Nod => Empty, Freeze_Id => Empty); end Analyze_Contracts; @@ -389,7 +400,7 @@ package body Contracts is (Obj_Id => Defining_Entity (Decl), Freeze_Id => Freeze_Id); - -- Protected untis + -- Protected units elsif Nkind_In (Decl, N_Protected_Type_Declaration, N_Single_Protected_Declaration) @@ -2643,4 +2654,566 @@ package body Contracts is Pop_Scope; end Save_Global_References_In_Contract; + ------------------------------------------------- + -- Build_And_Analyze_Contract_Only_Subprograms -- + ------------------------------------------------- + + 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 + + procedure Append_Contract_Only_Subprograms (Subp_List : List_Id); + -- Append the contract-only bodies of Subp_List to its declarations list + + 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. + + function Build_Contract_Only_Subprograms (L : List_Id) return List_Id; + -- Build the contract-only subprograms of all eligible subprograms found + -- in list L. + + 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. + + --------------------------------------- + -- Analyze_Contract_Only_Subprograms -- + --------------------------------------- + + procedure Analyze_Contract_Only_Subprograms (L : List_Id) is + procedure Analyze_Contract_Only_Bodies; + -- Analyze all the contract-only bodies of L + + ---------------------------------- + -- Analyze_Contract_Only_Bodies -- + ---------------------------------- + + procedure Analyze_Contract_Only_Bodies is + Decl : Node_Id; + + 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; + + Next (Decl); + end loop; + end Analyze_Contract_Only_Bodies; + + -- Start of processing for Analyze_Contract_Only_Subprograms + + begin + if Ekind (Current_Scope) /= E_Package then + Analyze_Contract_Only_Bodies; + + else + declare + Pkg_Spec : constant Node_Id := + Package_Specification (Current_Scope); + + begin + if not Has_Private_Declarations (Pkg_Spec) then + Analyze_Contract_Only_Bodies; + + -- 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. + + elsif Visible_Declarations (Pkg_Spec) = L then + null; + + elsif Private_Declarations (Pkg_Spec) = L then + Analyze_Contract_Only_Bodies; + end if; + end; + end if; + end Analyze_Contract_Only_Subprograms; + + -------------------------------------- + -- Append_Contract_Only_Subprograms -- + -------------------------------------- + + procedure Append_Contract_Only_Subprograms (Subp_List : List_Id) is + begin + if No (Subp_List) then + return; + end if; + + if Ekind (Current_Scope) /= E_Package then + Append_List (Subp_List, To => L); + + else + declare + Pkg_Spec : constant Node_Id := + Package_Specification (Current_Scope); + + begin + if not Has_Private_Declarations (Pkg_Spec) then + Append_List (Subp_List, To => L); + + -- 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. + + else + Append_List + (List => Subp_List, + To => Private_Declarations (Pkg_Spec)); + end if; + end; + end if; + end Append_Contract_Only_Subprograms; + + ------------------------------------ + -- Build_Contract_Only_Subprogram -- + ------------------------------------ + + -- 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 + + function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id is + Loc : constant Source_Ptr := Sloc (E); + + function Build_Missing_Body_Decls return List_Id; + -- Build the declaration of the missing body subprogram and its + -- corresponding pragma Import. + + function Build_Missing_Body_Subprogram_Call return Node_Id; + -- Build the call to the missing body subprogram + + 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. + + 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. + + ------------------------------ + -- 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; + + begin + Decl := Make_Subprogram_Declaration (Loc, + Copy_Original_Specification (Loc, Spec)); + Set_Chars (Defining_Unit_Name (Specification (Decl)), Name); + + Prag := + Make_Pragma (Loc, + Chars => Name_Import, + Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Make_Identifier (Loc, Name_Ada)), + + Make_Pragma_Argument_Association (Loc, + Expression => Make_Identifier (Loc, Name)))); + + return New_List (Decl, Prag); + end Build_Missing_Body_Decls; + + ---------------------------------------- + -- Build_Missing_Body_Subprogram_Call -- + ---------------------------------------- + + function Build_Missing_Body_Subprogram_Call return Node_Id is + Forml : Entity_Id; + Parms : List_Id; + + begin + -- Build parameter list that we need + + Parms := New_List; + Forml := First_Formal (E); + while Present (Forml) loop + Append_To (Parms, Make_Identifier (Loc, Chars (Forml))); + Next_Formal (Forml); + end loop; + + -- Build the call to the missing body subprogram + + 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)); + + 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; + + --------------------------------- + -- Copy_Original_Specification -- + --------------------------------- + + 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. + + 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). + + 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; + + -- Local variables + + Current_Parameter : Node_Id; + Current_Identifier : Entity_Id; + Current_Type : Node_Id; + New_Identifier : Entity_Id; + Parameters : List_Id := No_List; + + -- Start of processing for Copy_Original_Specification + + 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; + + 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; + + ----------------------------------- + -- Skip_Contract_Only_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. + + function Some_Enclosing_Package_Has_Private_Decls return Boolean; + -- Return True if some enclosing package of the current scope has + -- private declarations. + + --------------------------------------- + -- Depends_On_Enclosing_Private_Type -- + --------------------------------------- + + 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. + + ---------------------------------- + -- Defined_In_Enclosing_Package -- + ---------------------------------- + + 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; + + return Scop = Scope (Typ); + end Defined_In_Enclosing_Package; + + -- Local variables + + Param_E : Entity_Id; + Typ : Entity_Id; + begin + Param_E := First_Entity (E); + while Present (Param_E) loop + Typ := Etype (Param_E); + + if Is_Private_Type (Typ) + and then Defined_In_Enclosing_Package (Typ) + then + return True; + end if; + + Next_Entity (Param_E); + end loop; + + 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; + + ---------------------------------------------- + -- Some_Enclosing_Package_Has_Private_Decls -- + ---------------------------------------------- + + function Some_Enclosing_Package_Has_Private_Decls return Boolean is + Scop : Entity_Id := Current_Scope; + Pkg_Spec : Node_Id := Package_Specification (Scop); + + begin + loop + if Ekind (Scop) = E_Package + and then + Has_Private_Declarations (Package_Specification (Scop)) + then + Pkg_Spec := Package_Specification (Scop); + end if; + + exit when Is_Compilation_Unit (Scop); + Scop := Scope (Scop); + end loop; + + return Pkg_Spec /= Package_Specification (Current_Scope); + end Some_Enclosing_Package_Has_Private_Decls; + + -- Start of processing for Skip_Contract_Only_Subprogram + + 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; + + begin + -- Warnings are disabled by default under CodePeer_Mode + -- (see switch-c). Enable them temporarily. + + Warning_Mode := Normal; + Error_Msg_N + ("cannot generate contract-only subprogram?", E); + Warning_Mode := Saved_Mode; + end; + end if; + + return True; + end if; + + return False; + end Skip_Contract_Only_Subprogram; + + -- Start of processing for Build_Contract_Only_Subprogram + + 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; + end if; + + -- 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. + + declare + Name : constant Name_Id := Get_Contract_Only_Body_Name (E); + Id : Entity_Id; + Bod : Node_Id; + + 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))); + + Id := Defining_Unit_Name (Specification (Bod)); + + -- 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). + + declare + New_Contract : constant Node_Id := Make_Contract (Sloc (E)); + + begin + Set_Pre_Post_Conditions (New_Contract, + Copy_Separate_Tree (Pre_Post_Conditions (Contract (E)))); + Set_Contract (Id, New_Contract); + end; + + -- Fix the name of this new subprogram and link the original + -- subprogram with its Contract_Only_Body subprogram. + + Set_Chars (Id, Name); + Set_Is_Contract_Only_Body (Id); + Set_Contract_Only_Body (E, Id); + + return Bod; + end; + end Build_Contract_Only_Subprogram; + + ------------------------------------- + -- Build_Contract_Only_Subprograms -- + ------------------------------------- + + 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; + + 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); + + if Present (New_Subp) then + if No (Result) then + Result := New_List; + end if; + + Append_To (Result, New_Subp); + end if; + end if; + + Next (Decl); + end loop; + + return Result; + end Build_Contract_Only_Subprograms; + + ------------------------------ + -- Has_Private_Declarations -- + ------------------------------ + + 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; + + -- Local variables + + Subp_List : List_Id; + + -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms + + 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; + end Contracts; |