From patchwork Wed Jul 7 16:25:31 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: 1501888 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=2620:52:3:1:0:246e:9693:128c; helo=sourceware.org; envelope-from=gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dkim=pass (2048-bit key; unprotected) header.d=adacore-com.20150623.gappssmtp.com header.i=@adacore-com.20150623.gappssmtp.com header.a=rsa-sha256 header.s=20150623 header.b=N2nDilSq; dkim-atps=neutral Received: from sourceware.org (server2.sourceware.org [IPv6:2620:52:3:1:0:246e:9693:128c]) (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 4GKlSY0rksz9sWq for ; Thu, 8 Jul 2021 02:37:01 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id A9D61396E435 for ; Wed, 7 Jul 2021 16:36:58 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-lf1-x132.google.com (mail-lf1-x132.google.com [IPv6:2a00:1450:4864:20::132]) by sourceware.org (Postfix) with ESMTPS id 39B7D385743A for ; Wed, 7 Jul 2021 16:25:34 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 39B7D385743A Authentication-Results: sourceware.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com Received: by mail-lf1-x132.google.com with SMTP id p16so5293734lfc.5 for ; Wed, 07 Jul 2021 09:25:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore-com.20150623.gappssmtp.com; s=20150623; h=date:from:to:cc:subject:message-id:mime-version:content-disposition; bh=Xk4xrzCMgVuPpaB4VdQN7ojQg8h22q+iWkkrGOTfpEw=; b=N2nDilSqG0aAAmA2/VxN9itQghqRPLKEdYXuxK3GBysQbGLI0p/6ra19nV2F2CkQT7 llolWLjH6DiLhRWjVgIchEdUBKSrBJ7qHAZkyIl2Xx5oH9613hsrZpZZNhzqwPxo4xtr uPWE5SZlGY1nesWi2sRrQCX3CRSPE3dbsG1XBgQ32tc8y+6RvKDXHoAVILsCp/LMNQqk GOj4lwmdVPmQCE98Ozy2ozTFe23dciuMyLqfC1v/1iCexZl8qYcG3KKlZBrg2JbMEDro rY26rqZFoRhjGw5Bm7saNqFOwUCYbhtT+Ikqnsniip8cBuOX7nA1L4b4WOvj14D7PEwO BhLg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=Xk4xrzCMgVuPpaB4VdQN7ojQg8h22q+iWkkrGOTfpEw=; b=Y0Mv5QvBy3SxcV77v6nceq897w6CDBJ5QqGJuLBbAn1gMXx9vFi+S72+JOEEmazhOI yhe/Fxq0LqfBKnTVmclEnU7D+0BPFr8syIdlgEB3d2SsF0hKjSkZMbKcHehfIeRCTchJ tL1FJa0/qSEjFXqs5P8WQB4GLkUjmp32ubpFLkVuW70WYLlrOsr8ggRhykCDG+5zQPls +GjN995HyKkOnLXgzF8wcoK/F46a6Wv+a8tPF4OHp8y7cYfm5+IUYAvUnJMwDcuZqCSt IG6C++JViNtOTbAehnzJVfrRpbqhtCAjEuYMLChxwkvQkBVVKLbEXZQuaiESlG27EGw4 fvfA== X-Gm-Message-State: AOAM5321gsxV7/vpGWvT/BTpBcNeX93VUdkLW4t7PqQWp247aNAbEBsx +jrtXZWS1+w0mPcKSXrv5iRqnFQbrYxd4w== X-Google-Smtp-Source: ABdhPJzr1GSWzRvF3LvkfF0qbWaoLs3Au7spOXc9zwtKOZgRWaOGn2jmW9ubw4bwdmN5farxLHJ9lA== X-Received: by 2002:a19:4411:: with SMTP id r17mr20116323lfa.82.1625675133050; Wed, 07 Jul 2021 09:25:33 -0700 (PDT) Received: from adacore.com ([2a02:2ab8:224:2ce:72b5:e8ff:feef:ee60]) by smtp.gmail.com with ESMTPSA id d40sm1632457lfv.217.2021.07.07.09.25.31 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 07 Jul 2021 09:25:32 -0700 (PDT) Date: Wed, 7 Jul 2021 16:25:31 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Subject: [Ada] Implement new legality checks specified by AI12-0412 Message-ID: <20210707162531.GA2543133@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-12.1 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, GIT_PATCH_0, KAM_ASCII_DIVIDERS, KAM_NUMSUBJECT, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) 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+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" Ada 2022, in AI12-0412, specifies that certain uses of primitives of an abstract type that have Pre'Class or Post'Class aspect are illegal when an aspect is given with a nonstatic expression. Specifically, if the primitive is nonabstract and has such aspects, it's illegal to make a nondispatching call to it, as well as to apply 'Access to it or pass it as an actual for a nonabstract formal subprogram. Furthermore, by AI12-0170, as revised by AI12-0412, one can specify class-wide Pre and Post with calls to abstract functions, where any actuals given by a formal parameter of the primitive with the class-wide aspect are reinterpreted using a "notional (nonabstract) type" for any primitive of an abstract type, whether or not the primitive is abstract, and part of these changes now allows such aspects for nonabstract primitive cases that were formerly being rejected (previously GNAT was only allowing this for null procedures). Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * freeze.adb (Check_Inherited_Conditions): Setting of Ekind, LSP_Subprogram, and Is_Wrapper needs to happen for null procedures as well as other wrapper cases, so the code is moved from the else part in front of the if statement. (Fixes a latent bug encountered while working on this set of changes.) * sem_attr.adb (Resolve_Attribute): Report an error for the case of an Access attribute applied to a primitive of an abstract type when the primitive has any nonstatic Pre'Class or Post'Class expressions. * sem_ch8.adb (Analyze_Subprogram_Renaming): Report an error for the case of a actual subprogram associated with a nonabstract formal subprogram when the actual is a primitive of an abstract type and the primitive has any nonstatic Pre'Class or Post'Class expressions. * sem_disp.adb (Check_Dispatching_Context): Remove special testing for null procedures, and replace it with a relaxed test that avoids getting an error about illegal calls to abstract subprograms in cases where RM 6.1.1(7/5) applies in Pre/Post'Class aspects. Also, remove special test for Postcondition, which seems to be unnecessary, update associated comments, and fix a typo in one comment. (Check_Dispatching_Call): Remove an unneeded return statement, and report an error for the case of a nondispatching call to a nonabstract subprogram of an abstract type where the subprogram has nonstatic Pre/Post'Class aspects. * sem_util.ads (Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post): New function. (In_Pre_Post_Condition): Add a flag formal Class_Wide_Only, defaulted to False, for indicating whether the function should only test for the node being within class-wide pre- and postconditions. * sem_util.adb (Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post): New function to determine whether a subprogram is a primitive of an abstract type where the primitive has class-wide Pre/Post'Class aspects specified with nonstatic expressions. (In_Pre_Post_Condition): Extend testing to account for the new formal Class_Wide_Only. diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -1671,6 +1671,12 @@ package body Freeze is -- type declaration that generates inherited operation. For -- a null procedure, the declaration implies a null body. + -- Before insertion, do some minimal decoration of fields + + Mutate_Ekind (New_Id, Ekind (Par_Prim)); + Set_LSP_Subprogram (New_Id, Par_Prim); + Set_Is_Wrapper (New_Id); + if Nkind (New_Spec) = N_Procedure_Specification and then Null_Present (New_Spec) then @@ -1684,12 +1690,6 @@ package body Freeze is Build_Class_Wide_Clone_Call (Loc, Decls, Par_Prim, New_Spec); - -- Adding minimum decoration - - Mutate_Ekind (New_Id, Ekind (Par_Prim)); - Set_LSP_Subprogram (New_Id, Par_Prim); - Set_Is_Wrapper (New_Id); - Insert_List_After_And_Analyze (Par_R, New_List (New_Decl, New_Body)); diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -11499,6 +11499,25 @@ package body Sem_Attr is Error_Msg_F ("context requires a non-protected subprogram", P); end if; + -- AI12-0412: The rule in RM 6.1.1(18.2/5) disallows applying + -- attribute Access to a primitive of an abstract type when the + -- primitive has any Pre'Class or Post'Class aspects specified + -- with nonstatic expressions. + + if Attr_Id = Attribute_Access + and then Ekind (Btyp) in E_Access_Subprogram_Type + | E_Anonymous_Access_Subprogram_Type + and then Is_Entity_Name (P) + and then Is_Dispatching_Operation (Entity (P)) + and then + Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post (Entity (P)) + then + Error_Msg_N + ("attribute not allowed for primitive of abstract type with " + & "nonstatic class-wide pre/postconditions", + N); + end if; + -- The context cannot be a pool-specific type, but this is a -- legality rule, not a resolution rule, so it must be checked -- separately, after possibly disambiguation (see AI-245). diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -3790,15 +3790,31 @@ package body Sem_Ch8 is Set_Has_Delayed_Freeze (New_S, False); Freeze_Before (N, New_S); - -- An abstract subprogram is only allowed as an actual in the case - -- where the formal subprogram is also abstract. - if (Ekind (Old_S) = E_Procedure or else Ekind (Old_S) = E_Function) - and then Is_Abstract_Subprogram (Old_S) and then not Is_Abstract_Subprogram (Formal_Spec) then - Error_Msg_N - ("abstract subprogram not allowed as generic actual", Nam); + -- An abstract subprogram is only allowed as an actual in the + -- case where the formal subprogram is also abstract. + + if Is_Abstract_Subprogram (Old_S) then + Error_Msg_N + ("abstract subprogram not allowed as generic actual", Nam); + end if; + + -- AI12-0412: A primitive of an abstract type with Pre'Class + -- or Post'Class aspects specified with nonstatic expressions + -- is not allowed as actual for a nonabstract formal subprogram + -- (see RM 6.1.1(18.2/5). + + if Is_Dispatching_Operation (Old_S) + and then + Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post (Old_S) + then + Error_Msg_N + ("primitive of abstract type with nonstatic class-wide " + & "pre/postconditions not allowed as actual", + Nam); + end if; end if; end if; 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 @@ -612,29 +612,32 @@ package body Sem_Disp is Set_Entity (Name (N), Alias (Subp)); return; - -- An obscure special case: a null procedure may have a class- - -- wide pre/postcondition that includes a call to an abstract - -- subp. Calls within the expression may not have been rewritten - -- as dispatching calls yet, because the null body appears in - -- the current declarative part. The expression will be properly - -- rewritten/reanalyzed when the postcondition procedure is built. - - -- Similarly, if this is a pre/postcondition for an abstract - -- subprogram, it may call another abstract function which is - -- a primitive of an abstract type. The call is non-dispatching - -- but will be legal in overridings of the operation. However, - -- if the call is tag-indeterminate we want to continue with - -- with the error checking below, as this case is illegal even - -- for abstract subprograms (see AI12-0170). - - elsif (Is_Subprogram (Scop) - or else Chars (Scop) = Name_Postcondition) + -- If this is a pre/postcondition for an abstract subprogram, + -- it may call another abstract function that is a primitive + -- of an abstract type. The call is nondispatching but will be + -- legal in overridings of the operation. However, if the call + -- is tag-indeterminate we want to continue with with the error + -- checking below, as this case is illegal even for abstract + -- subprograms (see AI12-0170). + + -- Similarly, as per AI12-0412, a nonabstract subprogram may + -- have a class-wide pre/postcondition that includes a call to + -- an abstract primitive of the subprogram's controlling type. + -- Certain operations (nondispatching calls, 'Access, use as + -- a generic actual) applied to such a nonabstract subprogram + -- are illegal in the case where the type is abstract (see + -- RM 6.1.1(18.2/5)). + + elsif Is_Subprogram (Scop) + and then not Is_Tag_Indeterminate (N) + and then In_Pre_Post_Condition (Call, Class_Wide_Only => True) + + -- The tagged type associated with the called subprogram must be + -- the same as that of the subprogram with a class-wide aspect. + + and then Is_Dispatching_Operation (Scop) and then - ((Is_Abstract_Subprogram (Scop) - and then not Is_Tag_Indeterminate (N)) - or else - (Nkind (Parent (Scop)) = N_Procedure_Specification - and then Null_Present (Parent (Scop)))) + Find_Dispatching_Type (Subp) = Find_Dispatching_Type (Scop) then null; @@ -663,7 +666,7 @@ package body Sem_Disp is -- provides a tag to make the call dispatching. This requires -- the call to be the actual in an enclosing call, and that -- actual must be controlling. If the call is an operand of - -- equality, the other operand must not ve abstract. + -- equality, the other operand must not be abstract. if not Is_Tagged_Type (Typ) and then not @@ -970,7 +973,6 @@ package body Sem_Disp is end loop; Check_Dispatching_Context (N); - return; elsif Nkind (Parent (N)) in N_Subexpr then Check_Dispatching_Context (N); @@ -985,6 +987,23 @@ package body Sem_Disp is return; end if; + -- If this is a nondispatching call to a nonabstract subprogram + -- and the subprogram has any Pre'Class or Post'Class aspects with + -- nonstatic values, then report an error. This is specified by + -- RM 6.1.1(18.2/5) (by AI12-0412). + + if No (Control) + and then not Is_Abstract_Subprogram (Subp_Entity) + and then + Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post (Subp_Entity) + then + Error_Msg_N + ("nondispatching call to nonabstract subprogram of " + & "abstract type with nonstatic class-wide " + & "pre/postconditions", + N); + end if; + else -- If dispatching on result, the enclosing call, if any, will -- determine the controlling argument. Otherwise this is the diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -13295,6 +13295,44 @@ package body Sem_Util is and then Nkind (Node (First_Elmt (Constits))) = N_Null; end Has_Null_Refinement; + ------------------------------------------ + -- Has_Nonstatic_Class_Wide_Pre_Or_Post -- + ------------------------------------------ + + function Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post + (Subp : Entity_Id) return Boolean + is + Disp_Type : constant Entity_Id := Find_Dispatching_Type (Subp); + Prag : Node_Id; + Pragma_Arg : Node_Id; + + begin + if Present (Disp_Type) + and then Is_Abstract_Type (Disp_Type) + and then Present (Contract (Subp)) + then + Prag := Pre_Post_Conditions (Contract (Subp)); + + while Present (Prag) loop + if Pragma_Name (Prag) in Name_Precondition | Name_Postcondition + and then Class_Present (Prag) + then + Pragma_Arg := + Nlists.First + (Pragma_Argument_Associations (Prag)); + + if not Is_Static_Expression (Expression (Pragma_Arg)) then + return True; + end if; + end if; + + Prag := Next_Pragma (Prag); + end loop; + end if; + + return False; + end Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post; + ------------------------------- -- Has_Overriding_Initialize -- ------------------------------- @@ -14431,7 +14469,9 @@ package body Sem_Util is -- In_Pre_Post_Condition -- --------------------------- - function In_Pre_Post_Condition (N : Node_Id) return Boolean is + function In_Pre_Post_Condition + (N : Node_Id; Class_Wide_Only : Boolean := False) return Boolean + is Par : Node_Id; Prag : Node_Id := Empty; Prag_Id : Pragma_Id; @@ -14457,13 +14497,24 @@ package body Sem_Util is if Present (Prag) then Prag_Id := Get_Pragma_Id (Prag); - return - Prag_Id = Pragma_Post - or else Prag_Id = Pragma_Post_Class - or else Prag_Id = Pragma_Postcondition - or else Prag_Id = Pragma_Pre - or else Prag_Id = Pragma_Pre_Class - or else Prag_Id = Pragma_Precondition; + if Class_Wide_Only then + return + Prag_Id = Pragma_Post_Class + or else Prag_Id = Pragma_Pre_Class + or else (Class_Present (Prag) + and then (Prag_Id = Pragma_Post + or else Prag_Id = Pragma_Postcondition + or else Prag_Id = Pragma_Pre + or else Prag_Id = Pragma_Precondition)); + else + return + Prag_Id = Pragma_Post + or else Prag_Id = Pragma_Post_Class + or else Prag_Id = Pragma_Postcondition + or else Prag_Id = Pragma_Pre + or else Prag_Id = Pragma_Pre_Class + or else Prag_Id = Pragma_Precondition; + end if; -- Otherwise the node is not enclosed by a pre/postcondition pragma diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1516,6 +1516,12 @@ package Sem_Util is -- integer for use in compile-time checking. Note: Level is restricted to -- be non-dynamic. + function Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post + (Subp : Entity_Id) return Boolean; + -- Return True if Subp is a primitive of an abstract type, where the + -- primitive has a class-wide pre- or postcondition whose expression + -- is nonstatic. + function Has_Overriding_Initialize (T : Entity_Id) return Boolean; -- Predicate to determine whether a controlled type has a user-defined -- Initialize primitive (and, in Ada 2012, whether that primitive is @@ -1634,9 +1640,11 @@ package Sem_Util is function In_Pragma_Expression (N : Node_Id; Nam : Name_Id) return Boolean; -- Returns true if the expression N occurs within a pragma with name Nam - function In_Pre_Post_Condition (N : Node_Id) return Boolean; + function In_Pre_Post_Condition + (N : Node_Id; Class_Wide_Only : Boolean := False) return Boolean; -- Returns True if node N appears within a pre/postcondition pragma. Note - -- the pragma Check equivalents are NOT considered. + -- the pragma Check equivalents are NOT considered. If Class_Wide_Only is + -- True, then tests for N appearing within a class-wide pre/postcondition. function In_Quantified_Expression (N : Node_Id) return Boolean; -- Returns true if the expression N occurs within a quantified expression