From 5f325af2606476be7ef1db50b1a46ab842901bb9 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 12 Jan 2017 14:30:20 +0100 Subject: [PATCH] [multiple changes] 2017-01-12 Yannick Moy * exp_spark.adb (Expand_SPARK_Potential_Renaming): Fix sloc of copied subtree. 2017-01-12 Justin Squirek * exp_attr.adb (Expand_N_Attribute_Reference): Fix Finalization_Size case by properly resolving the type after rewritting the node. 2017-01-12 Hristian Kirtchev * exp_util.adb (Build_DIC_Procedure_Body): Semi-insert the body into the tree. (Build_DIC_Procedure_Declaration): Semi-insert the body into the tree. * binde.adb, exp_ch5.adb, sem_type.adb, sem.ads, sem_res.adb, exp_sel.ads: Minor reformatting. 2017-01-12 Justin Squirek * exp_ch6.adb (Expand_Call): Add guard to prevent invariant checks from being created for internally generated subprograms. 2017-01-12 Bob Duff * lib-writ.ads: Remove incorrect comment. 2017-01-12 Javier Miranda * debug.adb (-gnatd.K): Enable generation of contract-only procedures in CodePeer mode. * contracts.adb (Build_And_Analyze_Contract_Only_Subprograms): New subprogram. (Analyze_Contracts): Generate contract-only procedures if -gnatdK is set. * scil_ll.ads, scil_ll.adb (Get_Contract_Only_Body_Name): New subprogram. (Get_Contract_Only_Missing_Body_Name): New subprogram. (Get_Contract_Only_Body): New subprogram. (Set_Contract_Only_Body): New subprogram. (Is_Contract_Only_Body): New subprogram. (Set_Is_Contract_Only_Body): New subprogram. (SCIL_Nodes): Replace table by hash-table. From-SVN: r244356 --- gcc/ada/ChangeLog | 46 ++++ gcc/ada/binde.adb | 49 +++-- gcc/ada/contracts.adb | 575 +++++++++++++++++++++++++++++++++++++++++++++++++- gcc/ada/debug.adb | 9 +- gcc/ada/exp_attr.adb | 6 +- gcc/ada/exp_ch5.adb | 8 +- gcc/ada/exp_ch6.adb | 32 +-- gcc/ada/exp_sel.ads | 4 +- gcc/ada/exp_spark.adb | 2 +- gcc/ada/exp_util.adb | 26 ++- gcc/ada/lib-writ.ads | 6 +- gcc/ada/scil_ll.adb | 178 ++++++++++++---- gcc/ada/scil_ll.ads | 25 ++- gcc/ada/sem.ads | 4 +- gcc/ada/sem_res.adb | 3 +- gcc/ada/sem_type.adb | 1 - 16 files changed, 873 insertions(+), 101 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 787b324..048b975 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,49 @@ +2017-01-12 Yannick Moy + + * exp_spark.adb (Expand_SPARK_Potential_Renaming): Fix sloc of copied + subtree. + +2017-01-12 Justin Squirek + + * exp_attr.adb (Expand_N_Attribute_Reference): + Fix Finalization_Size case by properly resolving the type after + rewritting the node. + +2017-01-12 Hristian Kirtchev + + * exp_util.adb (Build_DIC_Procedure_Body): Semi-insert the body into + the tree. + (Build_DIC_Procedure_Declaration): Semi-insert the body into the tree. + * binde.adb, exp_ch5.adb, sem_type.adb, sem.ads, sem_res.adb, + exp_sel.ads: Minor reformatting. + +2017-01-12 Justin Squirek + + * exp_ch6.adb (Expand_Call): Add guard to prevent + invariant checks from being created for internally generated + subprograms. + +2017-01-12 Bob Duff + + * lib-writ.ads: Remove incorrect comment. + +2017-01-12 Javier Miranda + + * debug.adb (-gnatd.K): Enable generation of contract-only + procedures in CodePeer mode. + * contracts.adb (Build_And_Analyze_Contract_Only_Subprograms): + New subprogram. + (Analyze_Contracts): Generate contract-only procedures if -gnatdK is + set. + * scil_ll.ads, scil_ll.adb (Get_Contract_Only_Body_Name): New + subprogram. + (Get_Contract_Only_Missing_Body_Name): New subprogram. + (Get_Contract_Only_Body): New subprogram. + (Set_Contract_Only_Body): New subprogram. + (Is_Contract_Only_Body): New subprogram. + (Set_Is_Contract_Only_Body): New subprogram. + (SCIL_Nodes): Replace table by hash-table. + 2017-01-12 Hristian Kirtchev * exp_ch6.adb: Minor reformatting. diff --git a/gcc/ada/binde.adb b/gcc/ada/binde.adb index 7baf685..f655bf2 100644 --- a/gcc/ada/binde.adb +++ b/gcc/ada/binde.adb @@ -1211,14 +1211,18 @@ package body Binde is -- There is a lot of fiddly string manipulation below, because we don't -- want to depend on misc utility packages like Ada.Characters.Handling. - function Read_File (Name : String) return String_Ptr; - -- Read the entire contents of the named file - function Get_Line return String; -- Read the next line from the file content read by Read_File. Strip -- leading and trailing blanks. Convert "(spec)" or "(body)" to -- "%s"/"%b". Remove comments (Ada style; "--" to end of line). + function Read_File (Name : String) return String_Ptr; + -- Read the entire contents of the named file + + --------------- + -- Read_File -- + --------------- + function Read_File (Name : String) return String_Ptr is -- All of the following calls should succeed, because we checked the -- file in Switch.B, but we double check and raise Program_Error on @@ -1232,9 +1236,11 @@ package body Binde is end if; declare - Len : constant Natural := Natural (File_Length (F)); - Result : constant String_Ptr := new String (1 .. Len); - Len_Read : constant Natural := Read (F, Result (1)'Address, Len); + Len : constant Natural := Natural (File_Length (F)); + Result : constant String_Ptr := new String (1 .. Len); + Len_Read : constant Natural := + Read (F, Result (1)'Address, Len); + Status : Boolean; begin @@ -1252,12 +1258,17 @@ package body Binde is end; end Read_File; - S : String_Ptr := Read_File (Force_Elab_Order_File.all); - Cur : Positive := 1; + Cur : Positive := 1; + S : String_Ptr := Read_File (Force_Elab_Order_File.all); + + -------------- + -- Get_Line -- + -------------- function Get_Line return String is First : Positive := Cur; - Last : Natural; + Last : Natural; + begin -- Skip to end of line @@ -1293,12 +1304,16 @@ package body Binde is -- again. declare + Body_String : constant String := "(body)"; + BL : constant Positive := Body_String'Length; + Spec_String : constant String := "(spec)"; + SL : constant Positive := Spec_String'Length; + Line : String renames S (First .. Last); - Spec_String : constant String := "(spec)"; - SL : constant Positive := Spec_String'Length; - Body_String : constant String := "(body)"; - BL : constant Positive := Body_String'Length; - Is_Spec, Is_Body : Boolean := False; + + Is_Body : Boolean := False; + Is_Spec : Boolean := False; + begin if Line'Length >= SL and then Line (Last - SL + 1 .. Last) = Spec_String @@ -1336,8 +1351,12 @@ package body Binde is end; end Get_Line; + -- Local variables + Empty_Name : constant Unit_Name_Type := Name_Find (""); - Prev_Unit : Unit_Id := No_Unit_Id; + Prev_Unit : Unit_Id := No_Unit_Id; + + -- Start of processing for Force_Elab_Order begin -- Loop through the file content, and build a dependency link for each 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; diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index e3c53dd..a045a7b 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -128,7 +128,7 @@ package body Debug is -- d.H GNSA mode for ASIS -- d.I Do not ignore enum representation clauses in CodePeer mode -- d.J Disable parallel SCIL generation mode - -- d.K + -- d.K Enable generation of contract-only procedures in CodePeer mode -- d.L Depend on back end for limited types in if and case expressions -- d.M Relaxed RM semantics -- d.N Add node to all entities @@ -646,6 +646,13 @@ package body Debug is -- done in parallel to speed processing. This switch disables this -- behavior. + -- d.K Enable generation of contract-only procedures in CodePeer mode and + -- report a warning on subprograms for which the contract-only body + -- cannot be built. Currently reported on subprograms defined in + -- nested package specs that have some formal (or return type) whose + -- type is a private type defined in some enclosing package and that + -- have pre/postconditions. + -- d.L Normally the front end generates special expansion for conditional -- expressions of a limited type. This debug flag removes this special -- case expansion, leaving it up to the back end to handle conditional diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb index 57905df..074a5b1 100644 --- a/gcc/ada/exp_attr.adb +++ b/gcc/ada/exp_attr.adb @@ -3244,7 +3244,11 @@ package body Exp_Attr is Rewrite (N, Make_Integer_Literal (Loc, 0)); end if; - Analyze (N); + -- Due to cases where the entity type of the attribute is already + -- resolved the rewritten N must get re-resolved to its appropriate + -- type. + + Analyze_And_Resolve (N, Typ); end Finalization_Size; ----------- diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb index dff953b..ed3703a 100644 --- a/gcc/ada/exp_ch5.adb +++ b/gcc/ada/exp_ch5.adb @@ -2939,7 +2939,7 @@ package body Exp_Ch5 is -- For an element iterator, the Element aspect must be present, -- (this is checked during analysis) and the expansion takes the form: - -- Cursor : Cursor_type := First (Container); + -- Cursor : Cursor_Type := First (Container); -- Elmt : Element_Type; -- while Has_Element (Cursor, Container) loop -- Elmt := Element (Container, Cursor); @@ -2951,10 +2951,10 @@ package body Exp_Ch5 is -- In that case we create a block to hold a variable declaration -- initialized with a call to Element, and generate: - -- Cursor : Cursor_type := First (Container); + -- Cursor : Cursor_Type := First (Container); -- while Has_Element (Cursor, Container) loop -- declare - -- Elmt : Element-Type := Element (Container, Cursor); + -- Elmt : Element_Type := Element (Container, Cursor); -- begin -- -- Cursor := Next (Container, Cursor); @@ -2968,7 +2968,7 @@ package body Exp_Ch5 is Set_Ekind (Cursor, E_Variable); Insert_Action (N, Init); - -- Declaration for Element. + -- Declaration for Element Elmt_Decl := Make_Object_Declaration (Loc, diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 145ae93..7b7e135 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -2264,7 +2264,9 @@ package body Exp_Ch6 is -- expression for the value of the actual, EF is the entity for the -- extra formal. - procedure Check_View_Conversion (Formal : Entity_Id; Actual : Node_Id); + procedure Add_View_Conversion_Invariants + (Formal : Entity_Id; + Actual : Node_Id); -- Adds invariant checks for every intermediate type between the range -- of a view converted argument to its ancestor (from parent to child). @@ -2354,11 +2356,14 @@ package body Exp_Ch6 is end if; end Add_Extra_Actual; - --------------------------- - -- Check_View_Conversion -- - --------------------------- + ------------------------------------ + -- Add_View_Conversion_Invariants -- + ------------------------------------ - procedure Check_View_Conversion (Formal : Entity_Id; Actual : Node_Id) is + procedure Add_View_Conversion_Invariants + (Formal : Entity_Id; + Actual : Node_Id) + is Arg : Entity_Id; Curr_Typ : Entity_Id; Inv_Checks : List_Id; @@ -2407,7 +2412,7 @@ package body Exp_Ch6 is if not Is_Empty_List (Inv_Checks) then Insert_Actions_After (N, Inv_Checks); end if; - end Check_View_Conversion; + end Add_View_Conversion_Invariants; --------------------------- -- Inherited_From_Formal -- @@ -3292,15 +3297,18 @@ package body Exp_Ch6 is Duplicate_Subexpr_Move_Checks (Actual))); end if; - -- Invariant checks are performed for every intermediate type between - -- the range of a view converted argument to its ancestor (from - -- parent to child) if it is passed as an "out" or "in out" parameter - -- after executing the call (RM 7.3.2 (12/3, 13/3, 14/3)). + -- Perform invariant checks for all intermediate types in a view + -- conversion after successful return from a call that passes the + -- view conversion as an IN OUT or OUT parameter (RM 7.3.2 (12/3, + -- 13/3, 14/3)). Consider only source conversion in order to avoid + -- generating spurious checks on complex expansion such as object + -- initialization through an extension aggregate. - if Ekind (Formal) /= E_In_Parameter + if Comes_From_Source (N) + and then Ekind (Formal) /= E_In_Parameter and then Nkind (Actual) = N_Type_Conversion then - Check_View_Conversion (Formal, Actual); + Add_View_Conversion_Invariants (Formal, Actual); end if; -- This label is required when skipping extra actual generation for diff --git a/gcc/ada/exp_sel.ads b/gcc/ada/exp_sel.ads index 440a0ea..0ba7669 100644 --- a/gcc/ada/exp_sel.ads +++ b/gcc/ada/exp_sel.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2011, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -48,7 +48,7 @@ package Exp_Sel is function Build_Abort_Block_Handler (Loc : Source_Ptr) return Node_Id; -- Generate if front-end exception: -- when others => - -- Abort_Under; + -- Abort_Undefer; -- or if back-end exception: -- when others => -- null; diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 6ac38d6..a0721f6 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -140,7 +140,7 @@ package body Exp_SPARK is -- Otherwise the renamed object denotes a name else - Rewrite (N, New_Copy_Tree (Obj_Id)); + Rewrite (N, New_Copy_Tree (Obj_Id, New_Sloc => Loc)); Reset_Analyzed_Flags (N); end if; diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 7791ad46..f19b6e3 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1897,13 +1897,19 @@ package body Exp_Util is Set_Corresponding_Spec (Proc_Body, Proc_Id); -- The body should not be inserted into the tree when the context is - -- ASIS, GNATprove or a generic unit because it is not part of the - -- template. Note that the body must still be generated in order to - -- resolve the DIC assertion expression. + -- ASIS or a generic unit because it is not part of the template. Note + -- that the body must still be generated in order to resolve the DIC + -- assertion expression. - if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then + if ASIS_Mode or Inside_A_Generic then null; + -- Semi-insert the body into the tree for GNATprove by setting its + -- Parent field. This allows for proper upstream tree traversals. + + elsif GNATprove_Mode then + Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ))); + -- Otherwise the body is part of the freezing actions of the working -- type. @@ -2083,16 +2089,20 @@ package body Exp_Util is New_Occurrence_Of (Work_Typ, Loc))))); -- The declaration should not be inserted into the tree when the context - -- is ASIS, GNATprove, or a generic unit because it is not part of the - -- template. + -- is ASIS or a generic unit because it is not part of the template. - if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then + if ASIS_Mode or Inside_A_Generic then null; + -- Semi-insert the declaration into the tree for GNATprove by setting + -- its Parent field. This allows for proper upstream tree traversals. + + elsif GNATprove_Mode then + Set_Parent (Proc_Decl, Parent (Typ_Decl)); + -- Otherwise insert the declaration else - pragma Assert (Present (Typ_Decl)); Insert_After_And_Analyze (Typ_Decl, Proc_Decl); end if; diff --git a/gcc/ada/lib-writ.ads b/gcc/ada/lib-writ.ads index b38003b..0060c9e 100644 --- a/gcc/ada/lib-writ.ads +++ b/gcc/ada/lib-writ.ads @@ -649,10 +649,8 @@ package Lib.Writ is -- AD Elaborate_All_Desirable set for this unit, which means that -- there is no Elaborate_All, but the analysis suggests that -- Program_Error may be raised if the Elaborate_All conditions - -- cannot be satisfied. In dynamic elaboration mode, the binder - -- will attempt to treat AD as EA if it can. In static - -- elaboration mode, the binder will treat AD as EA, even if it - -- introduces cycles. + -- cannot be satisfied. The binder will attempt to treat AD as + -- EA if it can. -- The parameter source-name and lib-name are omitted for the case of a -- generic unit compiled with earlier versions of GNAT which did not diff --git a/gcc/ada/scil_ll.adb b/gcc/ada/scil_ll.adb index 470ac98..eed0d1a 100644 --- a/gcc/ada/scil_ll.adb +++ b/gcc/ada/scil_ll.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2010-2012, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-2016, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -29,63 +29,105 @@ -- -- ------------------------------------------------------------------------------ -with Alloc; use Alloc; -with Atree; use Atree; -with Opt; use Opt; -with Sinfo; use Sinfo; -with Table; +with Atree; use Atree; +with Opt; use Opt; +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 -- for a call to Set_Reporting_Proc in package atree). - function SCIL_Nodes_Table_Size return Pos; - -- Used to initialize the table of SCIL nodes because we do not want - -- to consume memory for this table if it is not required. + type Header_Num is range 1 .. 4096; + + function Hash (N : Node_Id) return Header_Num; + -- Hash function for Node_Ids + + -------------------------- + -- Internal Hash Tables -- + -------------------------- + + package Contract_Only_Body_Flag is new Simple_HTable + (Header_Num => Header_Num, + Element => Boolean, + No_Element => False, + Key => Node_Id, + Hash => Hash, + Equal => "="); + -- This table records the value of flag Is_Contract_Only_Flag of tree nodes + + package Contract_Only_Body_Nodes is new Simple_HTable + (Header_Num => Header_Num, + Element => Node_Id, + No_Element => Empty, + Key => Node_Id, + Hash => Hash, + Equal => "="); + -- This table records the value of attribute Contract_Only_Body of tree + -- nodes. + + package SCIL_Nodes is new Simple_HTable + (Header_Num => Header_Num, + Element => Node_Id, + No_Element => Empty, + Key => Node_Id, + Hash => Hash, + Equal => "="); + -- This table records the value of attribute SCIL_Node of tree nodes. + + -------------------- + -- Copy_SCIL_Node -- + -------------------- + + procedure Copy_SCIL_Node (Target : Node_Id; Source : Node_Id) is + begin + Set_SCIL_Node (Target, Get_SCIL_Node (Source)); + end Copy_SCIL_Node; ---------------------------- - -- SCIL_Nodes_Table_Size -- + -- Get_Contract_Only_Body -- ---------------------------- - function SCIL_Nodes_Table_Size return Pos is + function Get_Contract_Only_Body (N : Node_Id) return Node_Id is begin - if Generate_SCIL then - return Alloc.Orig_Nodes_Initial; + if CodePeer_Mode + and then Present (N) + then + return Contract_Only_Body_Nodes.Get (N); else - return 1; + return Empty; end if; - end SCIL_Nodes_Table_Size; - - package SCIL_Nodes is new Table.Table ( - Table_Component_Type => Node_Id, - Table_Index_Type => Node_Id'Base, - Table_Low_Bound => First_Node_Id, - Table_Initial => SCIL_Nodes_Table_Size, - Table_Increment => Alloc.Orig_Nodes_Increment, - Table_Name => "SCIL_Nodes"); - -- This table records the value of attribute SCIL_Node of all the - -- tree nodes. + end Get_Contract_Only_Body; - -------------------- - -- Copy_SCIL_Node -- - -------------------- + --------------------------------- + -- Get_Contract_Only_Body_Name -- + --------------------------------- - procedure Copy_SCIL_Node (Target : Node_Id; Source : Node_Id) is + function Get_Contract_Only_Body_Name (E : Entity_Id) return Name_Id is begin - Set_SCIL_Node (Target, Get_SCIL_Node (Source)); - end Copy_SCIL_Node; + return Name_Find (Get_Name_String (Chars (E)) & + Contract_Only_Body_Suffix); + end Get_Contract_Only_Body_Name; - ---------------- - -- Initialize -- - ---------------- + ----------------------------------------- + -- Get_Contract_Only_Missing_Body_Name -- + ----------------------------------------- - procedure Initialize is + function Get_Contract_Only_Missing_Body_Name (E : Entity_Id) + return Name_Id is begin - SCIL_Nodes.Init; - Set_Reporting_Proc (Copy_SCIL_Node'Access); - end Initialize; + return Name_Find (Get_Name_String (Chars (E)) & + Contract_Only_Missing_Body_Suffix); + end Get_Contract_Only_Missing_Body_Name; ------------------- -- Get_SCIL_Node -- @@ -96,12 +138,64 @@ package body SCIL_LL is if Generate_SCIL and then Present (N) then - return SCIL_Nodes.Table (N); + return SCIL_Nodes.Get (N); else return Empty; end if; end Get_SCIL_Node; + ---------- + -- Hash -- + ---------- + + function Hash (N : Node_Id) return Header_Num is + begin + return Header_Num (1 + N mod Node_Id (Header_Num'Last)); + end Hash; + + ---------------- + -- Initialize -- + ---------------- + + procedure Initialize is + begin + SCIL_Nodes.Reset; + Contract_Only_Body_Nodes.Reset; + Contract_Only_Body_Flag.Reset; + Set_Reporting_Proc (Copy_SCIL_Node'Access); + end Initialize; + + --------------------------- + -- Is_Contract_Only_Body -- + --------------------------- + + function Is_Contract_Only_Body (E : Entity_Id) return Boolean is + begin + return Contract_Only_Body_Flag.Get (E); + end Is_Contract_Only_Body; + + ---------------------------- + -- Set_Contract_Only_Body -- + ---------------------------- + + procedure Set_Contract_Only_Body (N : Node_Id; Value : Node_Id) is + begin + pragma Assert (CodePeer_Mode + and then Present (N) + and then Is_Contract_Only_Body (Value)); + + Contract_Only_Body_Nodes.Set (N, Value); + end Set_Contract_Only_Body; + + ------------------------------- + -- Set_Is_Contract_Only_Body -- + ------------------------------- + + procedure Set_Is_Contract_Only_Body (E : Entity_Id) is + begin + Contract_Only_Body_Flag.Set (E, True); + end Set_Is_Contract_Only_Body; + ------------------- -- Set_SCIL_Node -- ------------------- @@ -133,11 +227,7 @@ package body SCIL_LL is end case; end if; - if Atree.Last_Node_Id > SCIL_Nodes.Last then - SCIL_Nodes.Set_Last (Atree.Last_Node_Id); - end if; - - SCIL_Nodes.Set_Item (N, Value); + SCIL_Nodes.Set (N, Value); end Set_SCIL_Node; end SCIL_LL; diff --git a/gcc/ada/scil_ll.ads b/gcc/ada/scil_ll.ads index 8265a19..bfac1a0 100644 --- a/gcc/ada/scil_ll.ads +++ b/gcc/ada/scil_ll.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2010, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-2016, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -29,20 +29,39 @@ -- -- ------------------------------------------------------------------------------ --- This package extends the tree nodes with a field that is used to reference --- the SCIL node. +-- 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 + function Get_SCIL_Node (N : Node_Id) return Node_Id; -- Read the value of attribute SCIL node + procedure Set_Contract_Only_Body (N : Node_Id; Value : Node_Id); + -- Set the value of attribute Contract_Only_Body + procedure Set_SCIL_Node (N : Node_Id; Value : Node_Id); -- Set the value of attribute SCIL node procedure Initialize; -- Initialize the table of SCIL nodes + function Is_Contract_Only_Body (E : Entity_Id) return Boolean; + -- Return True if E is a Contract_Only_Body subprogram + + procedure Set_Is_Contract_Only_Body (E : Entity_Id); + -- Set E as Contract_Only_Body subprogram + end SCIL_LL; diff --git a/gcc/ada/sem.ads b/gcc/ada/sem.ads index 9adc8b2..6cd050e 100644 --- a/gcc/ada/sem.ads +++ b/gcc/ada/sem.ads @@ -523,8 +523,8 @@ package Sem is -- See Sem_Ch10 (Install_Parents, Remove_Parents). Node_To_Be_Wrapped : Node_Id; - -- Only used in transient scopes. Records the node which will - -- be wrapped by the transient block. + -- Only used in transient scopes. Records the node which will be wrapped + -- by the transient block. Actions_To_Be_Wrapped : Scope_Actions; -- Actions that have to be inserted at the start, at the end, or as diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index c8ca67c..1c5fe4c 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -11810,8 +11810,7 @@ package body Sem_Res is -- Valid_Array_Conversion -- ---------------------------- - function Valid_Array_Conversion return Boolean - is + function Valid_Array_Conversion return Boolean is Opnd_Comp_Type : constant Entity_Id := Component_Type (Opnd_Type); Opnd_Comp_Base : constant Entity_Id := Base_Type (Opnd_Comp_Type); diff --git a/gcc/ada/sem_type.adb b/gcc/ada/sem_type.adb index 3bc27db..555184a 100644 --- a/gcc/ada/sem_type.adb +++ b/gcc/ada/sem_type.adb @@ -307,7 +307,6 @@ package body Sem_Type is else Get_Next_Interp (I, It); end if; - end loop; All_Interp.Table (All_Interp.Last) := (Name, Typ, Abstr_Op); -- 2.7.4