From patchwork Mon May 29 08:28:47 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 70208 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 72BE238498E4 for ; Mon, 29 May 2023 08:29:34 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 72BE238498E4 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1685348974; bh=Tfx6PLDyBkBPwiw0NV0QETTrfsVcc7AFGRuHc2AsfNk=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=rJPxxPf897zZ937kLbnNA8ugZLwl1CF4tMScsucm3j/xdTIkDpFH1bfB2BS2o2YgF rux1udxQpY60MhCtaqA98JBqYUH1VI+WmIrWYAmLdjUlPn7oiNz0/x/KjgEqD3qOX3 3PCmVEgvHq5v/9PmRHjpYABQYFBI4YtZ3kZs3TMw= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x329.google.com (mail-wm1-x329.google.com [IPv6:2a00:1450:4864:20::329]) by sourceware.org (Postfix) with ESMTPS id 348EE3858436 for ; Mon, 29 May 2023 08:28:52 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 348EE3858436 Received: by mail-wm1-x329.google.com with SMTP id 5b1f17b1804b1-3f6094cb2d2so31041805e9.2 for ; Mon, 29 May 2023 01:28:52 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1685348931; x=1687940931; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=Tfx6PLDyBkBPwiw0NV0QETTrfsVcc7AFGRuHc2AsfNk=; b=OgAEiMRdTzARUMekhtBIslvi5Wchon5AkQ0bEGZpqfZH4AZTZHn7tMO/PV6bKz3Bon UGiJmrer2JGs4Oz9/yhf/OH8TH7tGYfCNLfNacLd2XjEDHyTxvVXVLKVSORJatCnZpN8 rRVpP3t8rI0dgbQQwXT2Lq1ZR3I50Z2D69iSDyOtIk4dpfduY5ERNu6ndubTnaFrd0WN 2zUjKBd+rWWTj8siJ8YdF/mToe0Pr3LkdTQedcVPYKFSxeNRcXwvfw/P0bR18o4iqPQg ELZQ0QfamGf2/XRMc/qh/q5vBTy7rWloap84/AlY217XTwDY1K48J/+4Qjb7IJ+DHdNN P70w== X-Gm-Message-State: AC+VfDypwxNC9FjI7H0WYPCtpt0/D7U/NTRZqt6InMkFOeCxfahrvTAK h/GBo1Tl7SO/ZUD+iJxZc3xl3TCn/b0408WDeB7fCQ== X-Google-Smtp-Source: ACHHUZ618qgvRBDytHdUeoqfJqXrQFAhfQ3OnndFSj2TvQyCMd9UGTX6uAnrPgz5mtSyjyQsAWO9OA== X-Received: by 2002:a1c:7216:0:b0:3f6:476:915 with SMTP id n22-20020a1c7216000000b003f604760915mr7516002wmc.6.1685348930778; Mon, 29 May 2023 01:28:50 -0700 (PDT) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id t8-20020adfe448000000b0030aedb8156esm1682101wrm.102.2023.05.29.01.28.49 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 29 May 2023 01:28:50 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [COMMITTED] ada: Analyze pre/post on access-to-subprogram without a wrapper Date: Mon, 29 May 2023 10:28:47 +0200 Message-Id: <20230529082847.2408971-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.7 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) 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-Patchwork-Original-From: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: =?utf-8?q?Marc_Poulhi=C3=A8s?= Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" From: Piotr Trojanek Aspects Pre/Post attached to an access-to-subprogram type were relocated to a spec of a wrapper subprogram and analyzed there; the body of the wrapper was only created with expansion enabled. However, there were several problems with this approach. When switch -gnat2022 was missing, we didn't relocate the Pre/Post aspects to wrapper and complained that their placement is incorrect (because we wrongly assumed that relocation is unconditional). Now we gently inform, that these aspects are Ada 2022 features that require -gnat20222 switch. When switch -gnata was missing, we entirely bypassed analysis of the Pre/Post aspects on access-to-subprogram. This was unlike for Pre/Post aspects on subprograms, which are checked for legality regardless of the -gnata switch. Finally, in the GNATprove backend we were picking the Pre/Post contract on an access-to-subprogram type from the wrapper, which was awkward as otherwise we had to ignore the wrapper specs and special-case for their missing bodies. In general, it is cleaner for GNATprove to extract the aspect expressions from where they originally appear and not from various expansion artifacts like access-to-subprogram wrappers (but the same applies to predication functions, type invariant procedures and default initialization procedures). Now we analyze the Pre/Post aspects on the types where they are originally attached, regardless of the -gnata switch. Once we adapt GNATprove to pick the aspect expression from there, we will stop creating the wrapper spec when expansion is disabled. gcc/ada/ * contracts.adb (Add_Pre_Post_Condition): Adapt to handle pre/post of an access-to-subprogram type. (Analyze_Type_Contract): Analyze pre/post of an access-to-subprogram. * contracts.ads (Analyze_Type_Contract): Adapt comment. * sem_ch3.adb (Build_Access_Subprogram_Wrapper): Copy pre/post aspects to wrapper spec and keep it on the type. * sem_prag.adb (Analyze_Pre_Post_Condition): Expect pre/post aspects on access-to-subprogram and complain if they appear without -gnat2022 switch. (Analyze_Pre_Post_Condition_In_Decl_Part): Adapt to handle pre/post on an access-to-subprogram type entity. * sem_attr.adb (Analyze_Attribute_Old_Result): Likewise. (Result): Likewise. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/contracts.adb | 20 ++++++++++++++++++-- gcc/ada/contracts.ads | 2 ++ gcc/ada/sem_attr.adb | 13 +++++++++++++ gcc/ada/sem_ch3.adb | 15 +++------------ gcc/ada/sem_prag.adb | 22 ++++++++++++++++++---- 5 files changed, 54 insertions(+), 18 deletions(-) diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index d3ceaa92e10..012ea33cf89 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -311,10 +311,13 @@ package body Contracts is -- The four volatility refinement pragmas are ok for all types. -- Part_Of is ok for task types and protected types. -- Depends and Global are ok for task types. + -- + -- Precondition and Postcondition are added separately; they are allowed + -- for access-to-subprogram types. elsif Is_Type (Id) then declare - Is_OK : constant Boolean := + Is_OK_Classification : constant Boolean := Prag_Nam in Name_Async_Readers | Name_Async_Writers | Name_Effective_Reads @@ -326,9 +329,16 @@ package body Contracts is | Name_Global) or else (Ekind (Id) = E_Protected_Type and Prag_Nam = Name_Part_Of); + begin - if Is_OK then + if Is_OK_Classification then Add_Classification; + + elsif Ekind (Id) in Access_Subprogram_Kind + and then Prag_Nam in Name_Precondition + | Name_Postcondition + then + Add_Pre_Post_Condition; else -- The pragma is not a proper contract item @@ -1580,6 +1590,12 @@ package body Contracts is begin Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id => Type_Id); + + -- Analyze Pre/Post on access-to-subprogram type + + if Is_Access_Subprogram_Type (Type_Id) then + Analyze_Entry_Or_Subprogram_Contract (Type_Id); + end if; end Analyze_Type_Contract; --------------------------------------- diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index 0625b9fc029..d52e1aaed4a 100644 --- a/gcc/ada/contracts.ads +++ b/gcc/ada/contracts.ads @@ -139,6 +139,8 @@ package Contracts is -- Async_Writers -- Effective_Reads -- Effective_Writes + -- Postcondition + -- Precondition -- -- In the case of a protected or task type, there will also be -- a call to Analyze_Protected_Contract or Analyze_Task_Contract. diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 8257d4b3536..f5ee275e23f 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -1513,6 +1513,7 @@ package body Sem_Attr is elsif Nkind (Subp_Decl) not in N_Abstract_Subprogram_Declaration | N_Entry_Declaration | N_Expression_Function + | N_Full_Type_Declaration | N_Generic_Subprogram_Declaration | N_Subprogram_Body | N_Subprogram_Body_Stub @@ -6009,6 +6010,18 @@ package body Sem_Attr is ("incorrect prefix for attribute %, expected %", P); end if; + -- If the prefix is an access-to-subprogram type, then it must + -- be the same as the annotated type. + + elsif Is_Access_Subprogram_Type (Pref_Id) then + if Pref_Id = Spec_Id then + Set_Etype (N, Etype (Designated_Type (Spec_Id))); + else + Error_Msg_Name_2 := Chars (Spec_Id); + Error_Attr + ("incorrect prefix for attribute %, expected %", P); + end if; + -- Otherwise the prefix denotes some other form of subprogram -- entity. diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 634b1cb4a38..f360be810b4 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -6848,25 +6848,16 @@ package body Sem_Ch3 is declare Asp : Node_Id; A_Id : Aspect_Id; - Cond : Node_Id; - Expr : Node_Id; begin Asp := First (Aspect_Specifications (Decl)); while Present (Asp) loop A_Id := Get_Aspect_Id (Chars (Identifier (Asp))); if A_Id = Aspect_Pre or else A_Id = Aspect_Post then - Cond := Asp; - Expr := Expression (Cond); - Replace_Type_Name (Expr); - Next (Asp); - - Remove (Cond); - Append (Cond, Contracts); - - else - Next (Asp); + Append (New_Copy_Tree (Asp), Contracts); + Replace_Type_Name (Expression (Last (Contracts))); end if; + Next (Asp); end loop; end; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 5363d2bee80..88dacf5cc57 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -5235,9 +5235,19 @@ package body Sem_Prag is then null; - -- An access-to-subprogram type can have pre/postconditions, but - -- these are transferred to the generated subprogram wrapper and - -- analyzed there. + -- An access-to-subprogram type can have pre/postconditions, which + -- are both analyzed when attached to the type and copied to the + -- generated subprogram wrapper and analyzed there. + + elsif Nkind (Subp_Decl) = N_Full_Type_Declaration + and then Nkind (Type_Definition (Subp_Decl)) in + N_Access_To_Subprogram_Definition + then + if Ada_Version < Ada_2022 then + Error_Msg_Ada_2022_Feature + ("pre/postcondition access-to-subprogram", Loc); + raise Pragma_Exit; + end if; -- Otherwise the placement of the pragma is illegal @@ -26635,11 +26645,15 @@ package body Sem_Prag is if not In_Open_Scopes (Spec_Id) then Restore_Scope := True; - Push_Scope (Spec_Id); if Is_Generic_Subprogram (Spec_Id) then + Push_Scope (Spec_Id); Install_Generic_Formals (Spec_Id); + elsif Is_Access_Subprogram_Type (Spec_Id) then + Push_Scope (Designated_Type (Spec_Id)); + Install_Formals (Designated_Type (Spec_Id)); else + Push_Scope (Spec_Id); Install_Formals (Spec_Id); end if; end if;