This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] Removing support for SCIL "contract-only" subprogram bodies
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Javier Miranda <miranda at adacore dot com>
- Date: Fri, 5 Jul 2019 03:08:37 -0400
- Subject: [Ada] Removing support for SCIL "contract-only" subprogram bodies
Remove support added for CodePeer (which was never enabled by default;
it was controlled by the -gnatd.K option) for generation of SCIL
"contract-only" subprogram bodies. These were intended for use when a
subprogram's "real" body is unavailable but the subprogram spec has
pre/post-conditions specified.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-07-05 Javier Miranda <miranda@adacore.com>
gcc/ada/
* debug.adb (-gnatd.K): Leave available this switch.
* contracts.adb (Build_And_Analyze_Contract_Only_Subprograms):
Remove.
* scil_ll.ads, scil_ll.adb (Contract_Only_Body_Flag,
Contract_Only_Body_Nodes, Get_Contract_Only_Body,
Is_Contract_Only_Body, Set_Contract_Only_Body): Remove.
--- gcc/ada/contracts.adb
+++ gcc/ada/contracts.adb
@@ -25,7 +25,6 @@
with Aspects; use Aspects;
with Atree; use Atree;
-with Debug; use Debug;
with Einfo; use Einfo;
with Elists; use Elists;
with Errout; use Errout;
@@ -51,7 +50,6 @@ with Sinfo; use Sinfo;
with Snames; use Snames;
with Stand; use Stand;
with Stringt; use Stringt;
-with SCIL_LL; use SCIL_LL;
with Tbuild; use Tbuild;
package body Contracts is
@@ -63,11 +61,6 @@ package body Contracts is
--
-- Part_Of
- 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
@@ -354,10 +347,6 @@ package body Contracts is
Decl : Node_Id;
begin
- if CodePeer_Mode and then Debug_Flag_Dot_KK then
- Build_And_Analyze_Contract_Only_Subprograms (L);
- end if;
-
Decl := First (L);
while Present (Decl) loop
@@ -1305,490 +1294,6 @@ package body Contracts is
Restore_SPARK_Mode (Saved_SM, Saved_SMP);
end Analyze_Task_Contract;
- -------------------------------------------------
- -- Build_And_Analyze_Contract_Only_Subprograms --
- -------------------------------------------------
-
- procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is
- procedure Analyze_Contract_Only_Subprograms;
- -- 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 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);
-
- Missing_Body_Name : constant Name_Id :=
- New_External_Name (Chars (E), "__missing_body");
-
- 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 Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean;
- -- Return True for cases where the wrapper is not needed or we cannot
- -- build it.
-
- ------------------------------
- -- Build_Missing_Body_Decls --
- ------------------------------
-
- function Build_Missing_Body_Decls return List_Id is
- Spec : constant Node_Id := Declaration_Node (E);
- Decl : Node_Id;
- Prag : Node_Id;
-
- begin
- Decl :=
- Make_Subprogram_Declaration (Loc, Copy_Subprogram_Spec (Spec));
- Set_Chars (Defining_Entity (Decl), Missing_Body_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, Missing_Body_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
- Parms := New_List;
-
- -- Build parameter list that we need
-
- 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, Missing_Body_Name),
- Parameter_Associations => Parms));
-
- 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;
-
- -----------------------------------
- -- 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;
-
- -- Start of processing for Depends_On_Enclosing_Private_Type
-
- 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 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;
-
- -- 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.
-
- 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;
-
- 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 it.
-
- if Skip_Contract_Only_Subprogram (E) 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 :=
- New_External_Name (Chars (E), "__contract_only");
- Id : Entity_Id;
- Bod : Node_Id;
-
- 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)));
-
- 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;
- New_Subp : Node_Id;
- Result : List_Id := No_List;
- Subp_Id : Entity_Id;
-
- 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_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;
-
- -- 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;
- end Build_And_Analyze_Contract_Only_Subprograms;
-
-----------------------------
-- Create_Generic_Contract --
-----------------------------
--- gcc/ada/debug.adb
+++ 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 Relaxed rules for pragma No_Return
- -- d.K Enable generation of contract-only procedures in CodePeer mode
+ -- d.K
-- 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
@@ -904,13 +904,6 @@ package body Debug is
-- for that. If the procedure does in fact return normally, execution
-- is erroneous, and therefore unpredictable.
- -- 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
--- gcc/ada/scil_ll.adb
+++ gcc/ada/scil_ll.adb
@@ -49,25 +49,6 @@ package body SCIL_LL is
-- 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,
@@ -86,21 +67,6 @@ package body SCIL_LL is
Set_SCIL_Node (Target, Get_SCIL_Node (Source));
end Copy_SCIL_Node;
- ----------------------------
- -- Get_Contract_Only_Body --
- ----------------------------
-
- function Get_Contract_Only_Body (N : Node_Id) return Node_Id is
- begin
- if CodePeer_Mode
- and then Present (N)
- then
- return Contract_Only_Body_Nodes.Get (N);
- else
- return Empty;
- end if;
- end Get_Contract_Only_Body;
-
-------------------
-- Get_SCIL_Node --
-------------------
@@ -132,42 +98,9 @@ package body SCIL_LL is
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 --
-------------------
--- gcc/ada/scil_ll.ads
+++ gcc/ada/scil_ll.ads
@@ -30,31 +30,19 @@
------------------------------------------------------------------------------
-- 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.
+-- the SCIL node.
with Types; use Types;
package SCIL_LL is
- 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;