From: Pierre-Marie de Rodat <derodat@adacore.com>
To: gcc-patches@gcc.gnu.org
Cc: Ed Schonberg <schonberg@adacore.com>
Subject: [Ada] Ada_2020 AI12-0220: Pre/Postconditions on Access_To_Subprogram types
Date: Wed, 10 Jun 2020 09:35:40 -0400 [thread overview]
Message-ID: <20200610133540.GA80649@adacore.com> (raw)
[-- Attachment #1: Type: text/plain, Size: 1203 bytes --]
This patch implements AI12-0220, which adds contracts to
Access_To_Subprogram types so that pre/postconditions are applied to all
indirect calls through such an access type.
Tested on x86_64-pc-linux-gnu, committed on trunk
2020-06-10 Ed Schonberg <schonberg@adacore.com>
gcc/ada/
* einfo.ads (Access_Subprogram_Wrapper): New attribute of
Subprogram_Type entities. Denotes subprogram constructed for
Access_To_Subprogram types that include pre- and postconditions.
* einfo.adb: Subprogram bodies for Access_Subprogram_Wrapper.
* exp_ch6.adb (Expand_Call): An indirect call through an
Access_To_subprogram that includes contracts is rewritten as a
call to the corresponding Access_ ubprogram_Wrapper. Handle
derived types that inherit contract from parent.
* sem_prag.adb (Build_Access_Subprogram_Wrapper): Build
subprogram declaration for subprogram that incorporates the
contracts of an Access_To_Subprogram type declaration. Build
corresponding body and attach it to freeze actions for type.
* sem_util.ads, sem_util.adb (Is_Access_Subprogram_Wrapper):
Utility that uses signature of the subprogram to determine
whether it is a generated wrapper for an Access_To_Subprogram
type.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 17838 bytes --]
--- gcc/ada/einfo.adb
+++ gcc/ada/einfo.adb
@@ -282,6 +282,7 @@ package body Einfo is
-- SPARK_Pragma Node40
+ -- Access_Subprogram_Wrapper Node41
-- Original_Protected_Subprogram Node41
-- SPARK_Aux_Pragma Node41
@@ -738,6 +739,12 @@ package body Einfo is
return Node30 (Implementation_Base_Type (Id));
end Access_Disp_Table_Elab_Flag;
+ function Access_Subprogram_Wrapper (Id : E) return E is
+ begin
+ pragma Assert (Ekind (Id) = E_Subprogram_Type);
+ return Node41 (Id);
+ end Access_Subprogram_Wrapper;
+
function Activation_Record_Component (Id : E) return E is
begin
pragma Assert (Ekind_In (Id, E_Constant,
@@ -3902,6 +3909,12 @@ package body Einfo is
Set_Node30 (Id, V);
end Set_Access_Disp_Table_Elab_Flag;
+ procedure Set_Access_Subprogram_Wrapper (Id : E; V : E) is
+ begin
+ pragma Assert (Ekind (Id) = E_Subprogram_Type);
+ Set_Node41 (Id, V);
+ end Set_Access_Subprogram_Wrapper;
+
procedure Set_Anonymous_Designated_Type (Id : E; V : E) is
begin
pragma Assert (Ekind (Id) = E_Variable);
@@ -11411,6 +11424,9 @@ package body Einfo is
=>
Write_Str ("SPARK_Aux_Pragma");
+ when E_Subprogram_Type =>
+ Write_Str ("Access_Subprogram_Wrapper");
+
when others =>
Write_Str ("Field41??");
end case;
--- gcc/ada/einfo.ads
+++ gcc/ada/einfo.ads
@@ -372,6 +372,15 @@ package Einfo is
-- on attribute 'Position applied to an object of the type; it is used by
-- the IP routine to avoid performing this elaboration twice.
+-- Access_Subprogram_Wrapper (Node41)
+-- Entity created for access_to_subprogram types that have pre/post
+-- conditions. Wrapper subprogram is created when analyzing corresponding
+-- aspect, and inherits said aspects. Body of subprogram includes code
+-- to check contracts, and a direct call to the designated subprogram.
+-- The body is part of the freeze actions for the type.
+-- The Subprogram_Type created for the Access_To_Subprogram carries the
+-- Access_Subprogram_Wrapper for use in the expansion of indirect calls.
+
-- Activation_Record_Component (Node31)
-- Defined for E_Variable, E_Constant, E_Loop_Parameter, and formal
-- parameter entities. Used in Opt.Unnest_Subprogram_Mode, in which case
@@ -6721,6 +6730,7 @@ package Einfo is
-- Extra_Accessibility_Of_Result (Node19)
-- Directly_Designated_Type (Node20)
-- Extra_Formals (Node28)
+ -- Access_Subprogram_Wrapper (Node41)
-- First_Formal (synth)
-- First_Formal_With_Extras (synth)
-- Last_Formal (synth)
@@ -7068,6 +7078,7 @@ package Einfo is
function Accept_Address (Id : E) return L;
function Access_Disp_Table (Id : E) return L;
function Access_Disp_Table_Elab_Flag (Id : E) return E;
+ function Access_Subprogram_Wrapper (Id : E) return E;
function Activation_Record_Component (Id : E) return E;
function Actual_Subtype (Id : E) return E;
function Address_Taken (Id : E) return B;
@@ -7775,6 +7786,7 @@ package Einfo is
procedure Set_Accept_Address (Id : E; V : L);
procedure Set_Access_Disp_Table (Id : E; V : L);
procedure Set_Access_Disp_Table_Elab_Flag (Id : E; V : E);
+ procedure Set_Access_Subprogram_Wrapper (Id : E; V : E);
procedure Set_Activation_Record_Component (Id : E; V : E);
procedure Set_Actual_Subtype (Id : E; V : E);
procedure Set_Address_Taken (Id : E; V : B := True);
@@ -8606,6 +8618,7 @@ package Einfo is
pragma Inline (Accept_Address);
pragma Inline (Access_Disp_Table);
pragma Inline (Access_Disp_Table_Elab_Flag);
+ pragma Inline (Access_Subprogram_Wrapper);
pragma Inline (Activation_Record_Component);
pragma Inline (Actual_Subtype);
pragma Inline (Address_Taken);
@@ -9222,6 +9235,7 @@ package Einfo is
pragma Inline (Set_Accept_Address);
pragma Inline (Set_Access_Disp_Table);
pragma Inline (Set_Access_Disp_Table_Elab_Flag);
+ pragma Inline (Set_Access_Subprogram_Wrapper);
pragma Inline (Set_Activation_Record_Component);
pragma Inline (Set_Actual_Subtype);
pragma Inline (Set_Address_Taken);
--- gcc/ada/exp_ch6.adb
+++ gcc/ada/exp_ch6.adb
@@ -2380,13 +2380,76 @@ package body Exp_Ch6 is
procedure Expand_Call (N : Node_Id) is
Post_Call : List_Id;
+ -- If this is an indirect call through an Access_To_Subprogram
+ -- with contract specifications, it is rewritten as a call to
+ -- the corresponding Access_Subprogram_Wrapper with the same
+ -- actuals, whose body contains a naked indirect call (which
+ -- itself must not be rewritten, to prevent infinite recursion).
+
+ Must_Rewrite_Indirect_Call : constant Boolean :=
+ Ada_Version >= Ada_2020
+ and then Nkind (Name (N)) = N_Explicit_Dereference
+ and then Ekind (Etype (Name (N))) = E_Subprogram_Type
+ and then Present
+ (Access_Subprogram_Wrapper (Etype (Name (N))));
+
begin
pragma Assert (Nkind_In (N, N_Entry_Call_Statement,
N_Function_Call,
N_Procedure_Call_Statement));
- Expand_Call_Helper (N, Post_Call);
- Insert_Post_Call_Actions (N, Post_Call);
+ -- Check that this is not the call in the body of the wrapper.
+
+ if Must_Rewrite_Indirect_Call
+ and then (not Is_Overloadable (Current_Scope)
+ or else not Is_Access_Subprogram_Wrapper (Current_Scope))
+ then
+ declare
+ Loc : constant Source_Ptr := Sloc (N);
+ Wrapper : constant Entity_Id :=
+ Access_Subprogram_Wrapper (Etype (Name (N)));
+ Ptr : constant Node_Id := Prefix (Name (N));
+ Ptr_Type : constant Entity_Id := Etype (Ptr);
+ Parms : constant List_Id := Parameter_Associations (N);
+ Typ : constant Entity_Id := Etype (N);
+ New_N : Node_Id;
+
+ begin
+ -- The last actual in the call is the pointer itself.
+ -- If the aspect is inherited, convert the pointer to the
+ -- parent type that specifies the contract.
+
+ if Is_Derived_Type (Ptr_Type)
+ and then Ptr_Type /= Etype (Last_Formal (Wrapper))
+ then
+ Append
+ (Make_Type_Conversion (Loc,
+ New_Occurrence_Of
+ (Etype (Last_Formal (Wrapper)), Loc), Ptr),
+ Parms);
+
+ else
+ Append (Ptr, Parms);
+ end if;
+
+ if Nkind (N) = N_Procedure_Call_Statement then
+ New_N := Make_Procedure_Call_Statement (Loc,
+ Name => New_Occurrence_Of (Wrapper, Loc),
+ Parameter_Associations => Parms);
+ else
+ New_N := Make_Function_Call (Loc,
+ Name => New_Occurrence_Of (Wrapper, Loc),
+ Parameter_Associations => Parms);
+ end if;
+
+ Rewrite (N, New_N);
+ Analyze_And_Resolve (N, Typ);
+ end;
+
+ else
+ Expand_Call_Helper (N, Post_Call);
+ Insert_Post_Call_Actions (N, Post_Call);
+ end if;
end Expand_Call;
------------------------
--- gcc/ada/sem_prag.adb
+++ gcc/ada/sem_prag.adb
@@ -4522,6 +4522,185 @@ package body Sem_Prag is
-- a class-wide precondition only if one of its ancestors has an
-- explicit class-wide precondition.
+ procedure Build_Access_Subprogram_Wrapper
+ (Decl : Node_Id;
+ Prag : Node_Id);
+ -- When an access_to_subprogram type has pre/postconditions, we
+ -- build a subprogram that includes these contracts and is invoked
+ -- by any indirect call through the corresponding access type.
+
+ procedure Build_Access_Subprogram_Wrapper_Body
+ (Decl : Node_Id;
+ New_Decl : Node_Id);
+ -- Build the wrapper body, which holds the indirect call through
+ -- an access_to_subprogram, and whose expansion incorporates the
+ -- contracts of the access type declaration.
+
+ -------------------------------------
+ -- Build_Access_Subprogram_Wrapper --
+ -------------------------------------
+
+ procedure Build_Access_Subprogram_Wrapper
+ (Decl : Node_Id;
+ Prag : Node_Id)
+ is
+ Loc : constant Source_Ptr := Sloc (Decl);
+ Id : constant Entity_Id := Defining_Identifier (Decl);
+ Type_Def : constant Node_Id := Type_Definition (Decl);
+ Specs : constant List_Id := Parameter_Specifications (Type_Def);
+ Profile : constant List_Id := New_List;
+
+ Form_P : Node_Id;
+ New_P : Node_Id;
+ New_Decl : Node_Id;
+ Spec : Node_Id;
+ Subp : Entity_Id;
+
+ begin
+ if Ekind_In (Id, E_Access_Subprogram_Type,
+ E_Access_Protected_Subprogram_Type,
+ E_Anonymous_Access_Protected_Subprogram_Type,
+ E_Anonymous_Access_Subprogram_Type)
+ then
+ null;
+
+ else
+ Error_Msg_N
+ ("illegal pre/postcondition on access type", N);
+ return;
+ end if;
+
+ Subp := Make_Temporary (Loc, 'A');
+ Form_P := First (Specs);
+
+ while Present (Form_P) loop
+ New_P := New_Copy_Tree (Form_P);
+ Set_Defining_Identifier (New_P,
+ Make_Defining_Identifier
+ (Loc, Chars (Defining_Identifier (Form_P))));
+ Append (New_P, Profile);
+ Next (Form_P);
+ end loop;
+
+ -- Add to parameter specifications the access parameter that
+ -- is passed from an indirect call.
+
+ Append (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => Make_Temporary (Loc, 'P'),
+ Parameter_Type => New_Occurrence_Of (Id, Loc)),
+ Profile);
+
+ if Nkind (Type_Def) = N_Access_Procedure_Definition then
+ Spec :=
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => Subp,
+ Parameter_Specifications => Profile);
+ else
+ Spec :=
+ Make_Function_Specification (Loc,
+ Defining_Unit_Name => Subp,
+ Parameter_Specifications => Profile,
+ Result_Definition =>
+ New_Copy_Tree
+ (Result_Definition (Type_Definition (Decl))));
+ end if;
+
+ New_Decl :=
+ Make_Subprogram_Declaration (Loc, Specification => Spec);
+ Set_Aspect_Specifications (New_Decl,
+ New_Copy_List_Tree (Aspect_Specifications (Decl)));
+
+ declare
+ Asp : Node_Id;
+
+ begin
+ Asp := First (Aspect_Specifications (New_Decl));
+ while Present (Asp) loop
+ Set_Aspect_Rep_Item (Asp, Empty);
+ Set_Entity (Asp, Empty);
+ Set_Analyzed (Asp, False);
+ Next (Asp);
+ end loop;
+ end;
+
+ Insert_After (Prag, New_Decl);
+ Set_Access_Subprogram_Wrapper (Designated_Type (Id), Subp);
+ Build_Access_Subprogram_Wrapper_Body (Decl, New_Decl);
+ end Build_Access_Subprogram_Wrapper;
+
+ ------------------------------------------
+ -- Build_Access_Subprogram_Wrapper_Body --
+ ------------------------------------------
+
+ procedure Build_Access_Subprogram_Wrapper_Body
+ (Decl : Node_Id;
+ New_Decl : Node_Id)
+ is
+ Loc : constant Source_Ptr := Sloc (Decl);
+ Actuals : constant List_Id := New_List;
+ Type_Def : constant Node_Id := Type_Definition (Decl);
+ Type_Id : constant Entity_Id := Defining_Identifier (Decl);
+ Spec_Node : constant Node_Id :=
+ New_Copy_Tree (Specification (New_Decl));
+
+ Act : Node_Id;
+ Body_Node : Node_Id;
+ Call_Stmt : Node_Id;
+ Ptr : Entity_Id;
+ begin
+ if not Expander_Active then
+ return;
+ end if;
+
+ Set_Defining_Unit_Name (Spec_Node,
+ Make_Defining_Identifier
+ (Loc, Chars (Defining_Unit_Name (Spec_Node))));
+
+ -- Create List of actuals for indirect call. The last
+ -- parameter of the subprogram is the access value itself.
+
+ Act := First (Parameter_Specifications (Spec_Node));
+
+ while Present (Act) loop
+ Append_To (Actuals,
+ Make_Identifier (Loc, Chars (Defining_Identifier (Act))));
+ Next (Act);
+ exit when Act = Last (Parameter_Specifications (Spec_Node));
+ end loop;
+
+ Ptr :=
+ Defining_Identifier
+ (Last (Parameter_Specifications (Spec_Node)));
+
+ if Nkind (Type_Def) = N_Access_Procedure_Definition then
+ Call_Stmt := Make_Procedure_Call_Statement (Loc,
+ Name =>
+ Make_Explicit_Dereference
+ (Loc, New_Occurrence_Of (Ptr, Loc)),
+ Parameter_Associations => Actuals);
+ else
+ Call_Stmt := Make_Simple_Return_Statement (Loc,
+ Expression =>
+ Make_Function_Call (Loc,
+ Name => Make_Explicit_Dereference
+ (Loc, New_Occurrence_Of (Ptr, Loc)),
+ Parameter_Associations => Actuals));
+ end if;
+
+ Body_Node := Make_Subprogram_Body (Loc,
+ Specification => Spec_Node,
+ Declarations => New_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (Call_Stmt)));
+
+ -- Place body in list of freeze actions for the type.
+
+ Ensure_Freeze_Node (Type_Id);
+ Append_Freeze_Actions (Type_Id, New_List (Body_Node));
+ end Build_Access_Subprogram_Wrapper_Body;
+
-----------------------------
-- Inherits_Class_Wide_Pre --
-----------------------------
@@ -4763,6 +4942,16 @@ package body Sem_Prag is
then
null;
+ elsif Ada_Version >= Ada_2020
+ and then Nkind (Subp_Decl) = N_Full_Type_Declaration
+ then
+
+ -- Access_To_Subprogram type has pre/postconditions.
+ -- Build wrapper subprogram to carry the contract items.
+
+ Build_Access_Subprogram_Wrapper (Subp_Decl, N);
+ return;
+
-- Otherwise the placement is illegal
else
@@ -30141,12 +30330,19 @@ package body Sem_Prag is
elsif Present (Generic_Parent (Specification (Stmt))) then
return Stmt;
- -- Ada 2020: contract on formal subprogram
+ -- Ada 2020: contract on formal subprogram or on generated
+ -- Access_Subprogram_Wrapper, which appears after the related
+ -- Access_Subprogram declaration.
elsif Is_Generic_Actual_Subprogram (Defining_Entity (Stmt))
and then Ada_Version >= Ada_2020
then
return Stmt;
+
+ elsif Is_Access_Subprogram_Wrapper (Defining_Entity (Stmt))
+ and then Ada_Version >= Ada_2020
+ then
+ return Stmt;
end if;
end if;
--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -11505,6 +11505,19 @@ package body Sem_Util is
return False;
end Has_Non_Null_Statements;
+ ----------------------------------
+ -- Is_Access_Subprogram_Wrapper --
+ ----------------------------------
+
+ function Is_Access_Subprogram_Wrapper (E : Entity_Id) return Boolean is
+ Formal : constant Entity_Id := Last_Formal (E);
+ begin
+ return Present (Formal)
+ and then Ekind (Etype (Formal)) in Access_Subprogram_Kind
+ and then Access_Subprogram_Wrapper
+ (Directly_Designated_Type (Etype (Formal))) = E;
+ end Is_Access_Subprogram_Wrapper;
+
---------------------------------
-- Side_Effect_Free_Statements --
---------------------------------
--- gcc/ada/sem_util.ads
+++ gcc/ada/sem_util.ads
@@ -1519,6 +1519,10 @@ package Sem_Util is
-- pragma Initialize_Scalars or by the binder. Return an expression created
-- at source location Loc, which denotes the invalid value.
+ function Is_Access_Subprogram_Wrapper (E : Entity_Id) return Boolean;
+ -- True if E is the constructed wrapper for an access_to_subprogram
+ -- type with Pre/Postconditions.
+
function Is_Actual_Out_Parameter (N : Node_Id) return Boolean;
-- Determines if N is an actual parameter of out mode in a subprogram call
next reply other threads:[~2020-06-10 13:35 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2020-06-10 13:35 Pierre-Marie de Rodat [this message]
2020-06-17 8:16 [Ada] Ada_2020 AI12-0220 " Pierre-Marie de Rodat
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20200610133540.GA80649@adacore.com \
--to=derodat@adacore.com \
--cc=gcc-patches@gcc.gnu.org \
--cc=schonberg@adacore.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).