[Ada] Ada_2020 AI12-0220: Pre/Postconditions on Access_To_Subprogram types

Message ID 20200610133540.GA80649@adacore.com
State New
Headers show
Series
  • [Ada] Ada_2020 AI12-0220: Pre/Postconditions on Access_To_Subprogram types
Related show

Commit Message

Pierre-Marie de Rodat June 10, 2020, 1:35 p.m.
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.

Patch

--- 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