From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from rock.gnat.com (rock.gnat.com [IPv6:2620:20:4000:0:a9e:1ff:fe9b:1d1]) by sourceware.org (Postfix) with ESMTP id 5D1DC38930D5 for ; Wed, 10 Jun 2020 13:35:41 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.3.2 sourceware.org 5D1DC38930D5 Authentication-Results: sourceware.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=derodat@adacore.com Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 3B6D4117B51; Wed, 10 Jun 2020 09:35:40 -0400 (EDT) X-Virus-Scanned: Debian amavisd-new at gnat.com Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id DSXfzg+nvOJs; Wed, 10 Jun 2020 09:35:40 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [IPv6:2620:20:4000:0:46a8:42ff:fe0e:e294]) by rock.gnat.com (Postfix) with ESMTP id 26AD5117B41; Wed, 10 Jun 2020 09:35:40 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 25B8DE1; Wed, 10 Jun 2020 09:35:40 -0400 (EDT) Date: Wed, 10 Jun 2020 09:35:40 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Ada_2020 AI12-0220: Pre/Postconditions on Access_To_Subprogram types Message-ID: <20200610133540.GA80649@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MGYHOYXEY6WxJCY8" Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-Spam-Status: No, score=-2.4 required=5.0 tests=BAYES_00, JMQ_SPF_NEUTRAL, KAM_ASCII_DIVIDERS, KAM_DMARC_STATUS, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=no autolearn_force=no version=3.4.2 X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 10 Jun 2020 13:35:44 -0000 --MGYHOYXEY6WxJCY8 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline 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 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. --MGYHOYXEY6WxJCY8 Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" --- 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 --MGYHOYXEY6WxJCY8--