From patchwork Wed Apr 28 09:41:39 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 1471048 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=8.43.85.97; helo=sourceware.org; envelope-from=gcc-patches-bounces@gcc.gnu.org; receiver=) Received: from sourceware.org (server2.sourceware.org [8.43.85.97]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 4FVYZh65RKz9sX2 for ; Wed, 28 Apr 2021 19:42:35 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 144893A8C820; Wed, 28 Apr 2021 09:41:51 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from rock.gnat.com (rock.gnat.com [205.232.38.15]) by sourceware.org (Postfix) with ESMTP id 0BA57385700D for ; Wed, 28 Apr 2021 09:41:42 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.3.2 sourceware.org 0BA57385700D 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 DED455613A; Wed, 28 Apr 2021 05:41:39 -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 bh-vXTYdCUtq; Wed, 28 Apr 2021 05:41:39 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id B93E156147; Wed, 28 Apr 2021 05:41:39 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id B6EFE12D; Wed, 28 Apr 2021 05:41:39 -0400 (EDT) Date: Wed, 28 Apr 2021 05:41:39 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Subject: [Ada] AI12-0397: Default_Initial_Condition expressions for derived types Message-ID: <20210428094139.GA139840@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-Spam-Status: No, score=-11.9 required=5.0 tests=BAYES_00, GIT_PATCH_0, KAM_ASCII_DIVIDERS, KAM_DMARC_STATUS, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham 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: , Cc: Gary Dismukes Errors-To: gcc-patches-bounces@gcc.gnu.org Sender: "Gcc-patches" AI12-0397 specifies new rules for the resolution of expressions for the Default_Intial_Condition aspect, based on defining that a reference to the current instance of a type with DIC is a notional (nonabstract) formal derived type (making DIC similar to how Postcondition and Type_Invariant are defined). This clarifies how calls with actuals given by the current instance of a type with DIC are resolved. Basically, the only operations of such a notional formal derived type correspond to the primitives of the type with DIC, so the current instance can only be passed as an actual when the callee is a primitive or the formal is class-wide. Calls to nonprimitives can be made, but only by converting the current instance. Also, the new rules make it possible to specify a DIC aspect for an abstract type, and pass current instances to an abstract operation of the type, because the operation is interpreted as being of the notional formal derived type. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_util.adb (Add_Own_DIC): Suppress expansion of a DIC pragma when the pragma occurs for an abstract type, since that could lead to a call to an abstract function, and such DIC checks can never be performed for abstract types in any case. * sem_disp.adb (Check_Dispatching_Context): Suppress the check for illegal calls to abstract subprograms when the call occurs within a Default_Initial_Condition aspect and the call is passed the current instance as an actual. (Has_Controlling_Current_Instance_Actual): New function to test a call to see if it has any actuals given by direct references to a current instance of a type * sem_res.adb (Resolve_Actuals): Issue an error for a call within a DIC aspect to a nonprimitive subprogram with an actual given by the name of the DIC type's current instance (which will show up as a reference to the formal parameter of a DIC procedure). diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1854,12 +1854,18 @@ package body Exp_Util is end if; -- Once the DIC assertion expression is fully processed, add a check - -- to the statements of the DIC procedure. - - Add_DIC_Check - (DIC_Prag => DIC_Prag, - DIC_Expr => Expr, - Stmts => Stmts); + -- to the statements of the DIC procedure (unless the type is an + -- abstract type, in which case we don't want the possibility of + -- generating a call to an abstract function of the type; such DIC + -- procedures can never be called in any case, so not generating the + -- check at all is OK). + + if not Is_Abstract_Type (DIC_Typ) then + Add_DIC_Check + (DIC_Prag => DIC_Prag, + DIC_Expr => Expr, + Stmts => Stmts); + end if; end Add_Own_DIC; --------------------- diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb --- a/gcc/ada/sem_disp.adb +++ b/gcc/ada/sem_disp.adb @@ -517,6 +517,12 @@ package body Sem_Disp is procedure Abstract_Context_Error; -- Error for abstract call dispatching on result is not dispatching + function Has_Controlling_Current_Instance_Actual_In_DIC + (Call : Node_Id) return Boolean; + -- Return True if the subprogram call Call has a controlling actual + -- given directly by a current instance referenced within a DIC + -- aspect. + ---------------------------- -- Abstract_Context_Error -- ---------------------------- @@ -536,6 +542,44 @@ package body Sem_Disp is end if; end Abstract_Context_Error; + ---------------------------------------- + -- Has_Current_Instance_Actual_In_DIC -- + ---------------------------------------- + + function Has_Controlling_Current_Instance_Actual_In_DIC + (Call : Node_Id) return Boolean + is + A : Node_Id; + F : Entity_Id; + begin + F := First_Formal (Subp_Entity); + A := First_Actual (Call); + + while Present (F) loop + + -- Return True if the actual denotes a current instance (which + -- will be represented by an in-mode formal of the enclosing + -- DIC_Procedure) passed to a controlling formal. We don't have + -- to worry about controlling access formals here, because its + -- illegal to apply Access (etc.) attributes to a current + -- instance within an aspect (by AI12-0068). + + if Is_Controlling_Formal (F) + and then Nkind (A) = N_Identifier + and then Ekind (Entity (A)) = E_In_Parameter + and then Is_Subprogram (Scope (Entity (A))) + and then Is_DIC_Procedure (Scope (Entity (A))) + then + return True; + end if; + + Next_Formal (F); + Next_Actual (A); + end loop; + + return False; + end Has_Controlling_Current_Instance_Actual_In_DIC; + -- Local variables Scop : constant Entity_Id := Current_Scope_No_Loops; @@ -591,6 +635,20 @@ package body Sem_Disp is then null; + -- Similarly to the dispensation for postconditions, a call to + -- an abstract function within a Default_Initial_Condition aspect + -- can be legal when passed a current instance of the type. Such + -- a call will be effectively mapped to a call to a primitive of + -- a descendant type (see AI12-0397, as well as AI12-0170), so + -- doesn't need to be dispatching. We test for being within a DIC + -- procedure, since that's where the call will be analyzed. + + elsif Is_Subprogram (Scop) + and then Is_DIC_Procedure (Scop) + and then Has_Controlling_Current_Instance_Actual_In_DIC (Call) + then + null; + elsif Ekind (Current_Scope) = E_Function and then Nkind (Unit_Declaration_Node (Scop)) = N_Generic_Subprogram_Declaration diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -5036,6 +5036,41 @@ package body Sem_Res is end if; end if; + -- (AI12-0397): The target of a subprogram call that occurs within + -- the expression of an Default_Initial_Condition aspect and has + -- an actual that is the current instance of the type must be + -- either a primitive of the type or a class-wide subprogram, + -- because the type of the current instance in such an aspect is + -- considered to be a notional formal derived type whose only + -- operations correspond to the primitives of the enclosing type. + -- Nonprimitives can be called, but the current instance must be + -- converted rather than passed directly. Note that a current + -- instance of a type with DIC will occur as a reference to an + -- in-mode formal of an enclosing DIC procedure or partial DIC + -- procedure. (It seems that this check should perhaps also apply + -- to calls within Type_Invariant'Class, but not Type_Invariant, + -- aspects???) + + if Nkind (A) = N_Identifier + and then Ekind (Entity (A)) = E_In_Parameter + + and then Is_Subprogram (Scope (Entity (A))) + and then Is_DIC_Procedure (Scope (Entity (A))) + + -- We check Comes_From_Source to exclude inherited primitives + -- from being flagged, because such subprograms turn out to not + -- always have the Is_Primitive flag set. ??? + + and then Comes_From_Source (Nam) + + and then not Is_Primitive (Nam) + and then not Is_Class_Wide_Type (Etype (F)) + then + Error_Msg_NE + ("call to nonprimitive & with current instance not allowed " & + "for aspect", A, Nam); + end if; + Next_Actual (A); -- Case where actual is not present