From patchwork Tue May 23 08:09:28 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: 97883 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:b0ea:0:b0:3b6:4342:cba0 with SMTP id b10csp1980232vqo; Tue, 23 May 2023 01:26:56 -0700 (PDT) X-Google-Smtp-Source: ACHHUZ5Q2jGKvuf9QSxih0Jh2lW6hOAb8LRmDby7ozSjn8Fq5cERy8Rix9Y/oiwmAETaa9O4MrDS X-Received: by 2002:a17:906:4fd0:b0:94f:36a0:da45 with SMTP id i16-20020a1709064fd000b0094f36a0da45mr15542338ejw.29.1684830416720; Tue, 23 May 2023 01:26:56 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1684830416; cv=none; d=google.com; s=arc-20160816; b=0o8jEKiqo1c/h5rTlize9I5AN7mW0UgqBiKD22/RFBgP/y43G0aC+vQCzwJIlmEQrw 5rWH0SPWZJuoFVW1S+UpfsikRIHpXx8x3AzpkMyIB4sQFVKzw6Kn6RGvzqfZOx3Ize6I 0mF8wVVWsxLeB7uNRHhN7RFjbkzx9RAtv+qW8C3T/YG/gbji/j3jua/OGsXy5rTnI26c ekd9po4m+tKn8FxwwMouB5atvKeDexJwXJ9nyUYu7FrEdFqpXQ8F9ub93mpkolupyGTn K1Y7uXlA9vj0WOwYQCX9Fu+eW9yquySBlq9NnOsnOaW7vBEKh7V2FjsyKuPY4ubpO++w CEMQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:reply-to:from:list-subscribe:list-help:list-post :list-archive:list-unsubscribe:list-id:precedence :content-transfer-encoding:mime-version:message-id:date:subject:cc :to:dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=kf2uaDJIUFB7MtRp4EmuP5Tk3iFRuD7mHKFs4Chttfk=; b=EenaXx/LE61uBzfTeOSBle7w+h86MUTBeOdOOE/rPltUcFKZ37zpGJH1b4NZptvm/E kCDtfv+TUMoezkkoOfck+vRaUqF4Uiuc8T/Uj4oWjzZVoMx7UugRF8orESgj8qIB4pyG AbHe70uMmXPlgmLEn/JGf075pCj7NgcLnyPXTz8AVpLYiIvoD6gXj/npPtsdFiWjFFxD R02WYCQ4g7U2TODdvZUW3KON3j7A+9dAElhkOYE63dcTm2/dWPBIWH6bjPDoHWoPxode x+VLAWcGVfxAx9kpJSVM7Fgg6RC1LD4AyvdFCcJW829IWFf771zZIb21kAnGOfkckm85 GLqQ== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=Vf4aKAan; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from sourceware.org (server2.sourceware.org. [8.43.85.97]) by mx.google.com with ESMTPS id jl2-20020a17090775c200b00966592357bcsi336919ejc.36.2023.05.23.01.26.56 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 23 May 2023 01:26:56 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) client-ip=8.43.85.97; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=Vf4aKAan; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id C6D113AA8C20 for ; Tue, 23 May 2023 08:16:53 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org C6D113AA8C20 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1684829813; bh=kf2uaDJIUFB7MtRp4EmuP5Tk3iFRuD7mHKFs4Chttfk=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=Vf4aKAannCzwSkHXAXr/54bzHcWyi/tuqNDql6j8gE31OnEzRrzKn34lwF7FBAGLF yeXP3fEgQKVTtcA2YzJdK4IjHVJXq6FwlPq3rF+XfB21UK9HyvLnQ4c7W6m/Gv+CC9 ie1me5Mn6W8avRTtHYS2QxnjJnPOALrTkigs+WiQ= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x331.google.com (mail-wm1-x331.google.com [IPv6:2a00:1450:4864:20::331]) by sourceware.org (Postfix) with ESMTPS id 65B6B382E6B0 for ; Tue, 23 May 2023 08:09:31 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 65B6B382E6B0 Received: by mail-wm1-x331.google.com with SMTP id 5b1f17b1804b1-3f60b3f32b4so2468275e9.1 for ; Tue, 23 May 2023 01:09:31 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1684829370; x=1687421370; 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=kf2uaDJIUFB7MtRp4EmuP5Tk3iFRuD7mHKFs4Chttfk=; b=BDy1j6hEXx+c2QOVmcSMplSSl9W+JgeRn7CA8jBZYt+IpENCdPGwnMA8ZjC3zZIrdN yzhkHfFVLGUSF5U+PkTRU8+afXy6wzosrL+1jIB+RMPy062wyoG3vjBF1oyFw/5wao2E WMLKobBEwuB0ngTGUQEm3igLrSSmBU3fw5P2BcbWe7zfYJMZu+LfcCDW37y2rGCGRUbE dNv4xuPRAVZyD1uc0N9Yx0IiZchrPoTfaKWA/dhdUFM81sqqch6G2NFGJSL6l935ENs6 lFFbqFwE6cIc2zlcTlNn0JtQeYKl2MrLE471kEHzHl7DjLCbdirLh3zHu8ih6j4vyEzw h4uw== X-Gm-Message-State: AC+VfDwXW4QNme2rjd1YgpZkq+jEXP1p0AXyt4drB6aZVl490F0FYCOz tNMQDyz4bHrM2vt4K2HAcM4Bfk6a39hGK+/rFHw9Lg== X-Received: by 2002:a7b:cd01:0:b0:3f4:2327:53c2 with SMTP id f1-20020a7bcd01000000b003f4232753c2mr10001415wmj.19.1684829370097; Tue, 23 May 2023 01:09:30 -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 n1-20020a05600c294100b003ee74c25f12sm14071399wmd.35.2023.05.23.01.09.29 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 23 May 2023 01:09:29 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [COMMITTED] ada: Accept and analyze new aspect Exceptional_Cases Date: Tue, 23 May 2023 10:09:28 +0200 Message-Id: <20230523080928.1875104-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.2 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_FILL_THIS_FORM_SHORT, 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+ouuuleilei=gmail.com@gcc.gnu.org Sender: "Gcc-patches" X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1766672739080599400?= X-GMAIL-MSGID: =?utf-8?q?1766672739080599400?= From: Piotr Trojanek Add new aspect Exceptional_Cases, which is intended for SPARK and describes in which cases an exception will be raised, and optionally supply a postcondition that shall be verified in this case. The implementation is heavily modeled after Subprogram_Variant, which in turn was heavily modeled after Contract_Cases. Currently the aspect is only analysed; the code infrastructure required to expand it is prepared but empty. This is enough for the aspect to be verified by GNATprove. gcc/ada/ * aspects.ads (Aspect_Id): Add aspect identifier. (Aspect_Argument): New aspect accepts an expression. (Is_Representation_Aspect): New aspect is not a representation aspect. (Aspect_Names): Associate name with the new aspect identifier. (Aspect_Delay): New aspect is never delayed. * contracts.adb (Add_Contract_Item): Store new aspect among contract items. (Analyze_Entry_Or_Subprogram_Contract): Likewise. (Analyze_Subprogram_Body_Stub_Contract): Likewise. (Process_Contract_Cases): Expand new aspect, if present. * contracts.ads (Analyze_Entry_Or_Subprogram_Body_Contract): Mention new aspect in spec. (Analyze_Entry_Or_Subprogram_Contract): Likewise. * einfo-utils.adb (Get_Pragma): Allow new aspect to be picked by the backend. * einfo-utils.ads (Get_Pragma): Mention new aspect in spec. * exp_prag.adb (Expand_Pragma_Exceptional_Cases): Dummy expansion routine. * exp_prag.ads (Expand_Pragma_Exceptional_Cases): Add spec for expansion routine. * inline.adb (Remove_Aspects_And_Pragmas): Remove aspect from bodies to inline. * par-prag.adb (Par.Prag): Accept pragma in the parser, so it will be checked later. * sem_ch12.adb (Implementation of Generic Contracts): Mention new aspect in comment. * sem_ch13.adb (Analyze_Aspect_Specifications): Transform new aspect info a corresponding pragma. * sem_prag.adb (Analyze_Exceptional_Cases_In_Decl_Part): Analyze aspect expression; heavily inspired by the existing code for analysis of Subprogram_Variant and exception handlers. (Analyze_Pragma): Analyze pragma corresponding to the new aspect. (Is_Non_Significant_Pragma_Reference): Add new pragma to the table. * sem_prag.ads (Assertion_Expression_Pragma): New pragma acts as an assertion expression, even though it is not currently expanded. (Analyze_Exceptional_Cases_In_Decl_Part): Add spec. * sem_util.adb (Is_Subprogram_Contract_Annotation): Mark new annotation is a subprogram contract, so the subprogram with it won't be inlined. * sem_util.ads (Is_Subprogram_Contract_Annotation): Mention new aspect in comment. * sinfo.ads (Contract_Test_Cases): Mention new aspect in comment. * snames.ads-tmpl: Add entries for the new name and pragma. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/aspects.ads | 5 + gcc/ada/contracts.adb | 18 +- gcc/ada/contracts.ads | 2 + gcc/ada/einfo-utils.adb | 1 + gcc/ada/einfo-utils.ads | 1 + gcc/ada/exp_prag.adb | 41 ++++ gcc/ada/exp_prag.ads | 4 + gcc/ada/inline.adb | 2 + gcc/ada/par-prag.adb | 1 + gcc/ada/sem_ch12.adb | 3 +- gcc/ada/sem_ch13.adb | 28 ++- gcc/ada/sem_prag.adb | 429 ++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_prag.ads | 8 + gcc/ada/sem_util.adb | 1 + gcc/ada/sem_util.ads | 1 + gcc/ada/sinfo.ads | 4 +- gcc/ada/snames.ads-tmpl | 2 + 17 files changed, 538 insertions(+), 13 deletions(-) diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 36957d466e6..6670b64ca49 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -96,6 +96,7 @@ package Aspects is Aspect_Dynamic_Predicate, Aspect_Effective_Reads, -- GNAT Aspect_Effective_Writes, -- GNAT + Aspect_Exceptional_Cases, -- GNAT Aspect_Extensions_Visible, -- GNAT Aspect_External_Name, Aspect_External_Tag, @@ -389,6 +390,7 @@ package Aspects is Aspect_Dynamic_Predicate => Expression, Aspect_Effective_Reads => Optional_Expression, Aspect_Effective_Writes => Optional_Expression, + Aspect_Exceptional_Cases => Expression, Aspect_Extensions_Visible => Optional_Expression, Aspect_External_Name => Expression, Aspect_External_Tag => Expression, @@ -496,6 +498,7 @@ package Aspects is Aspect_Dynamic_Predicate => False, Aspect_Effective_Reads => False, Aspect_Effective_Writes => False, + Aspect_Exceptional_Cases => False, Aspect_Exclusive_Functions => False, Aspect_Extensions_Visible => False, Aspect_External_Name => False, @@ -653,6 +656,7 @@ package Aspects is Aspect_Effective_Reads => Name_Effective_Reads, Aspect_Effective_Writes => Name_Effective_Writes, Aspect_Elaborate_Body => Name_Elaborate_Body, + Aspect_Exceptional_Cases => Name_Exceptional_Cases, Aspect_Exclusive_Functions => Name_Exclusive_Functions, Aspect_Export => Name_Export, Aspect_Extensions_Visible => Name_Extensions_Visible, @@ -981,6 +985,7 @@ package Aspects is Aspect_Disable_Controlled => Never_Delay, Aspect_Effective_Reads => Never_Delay, Aspect_Effective_Writes => Never_Delay, + Aspect_Exceptional_Cases => Never_Delay, Aspect_Export => Never_Delay, Aspect_Extensions_Visible => Never_Delay, Aspect_Ghost => Never_Delay, diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index b0a0ab20228..c85df0fccc8 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -104,8 +104,9 @@ package body Contracts is procedure Expand_Subprogram_Contract (Body_Id : Entity_Id); -- Expand the contracts of a subprogram body and its correspoding spec (if -- any). This routine processes all [refined] pre- and postconditions as - -- well as Contract_Cases, Subprogram_Variant, invariants and predicates. - -- Body_Id denotes the entity of the subprogram body. + -- well as Contract_Cases, Exceptional_Cases, Subprogram_Variant, + -- invariants and predicates. Body_Id denotes the entity of the + -- subprogram body. procedure Preanalyze_Condition (Subp : Entity_Id; @@ -253,6 +254,7 @@ package body Contracts is Add_Classification; elsif Prag_Nam in Name_Contract_Cases + | Name_Exceptional_Cases | Name_Subprogram_Variant | Name_Test_Case then @@ -629,8 +631,9 @@ package body Contracts is end if; -- Deal with preconditions, [refined] postconditions, Contract_Cases, - -- Subprogram_Variant, invariants and predicates associated with body - -- and its spec. Do not expand the contract of subprogram body stubs. + -- Exceptional_Cases, Subprogram_Variant, invariants and predicates + -- associated with body and its spec. Do not expand the contract of + -- subprogram body stubs. if Nkind (Body_Decl) = N_Subprogram_Body then Expand_Subprogram_Contract (Body_Id); @@ -766,6 +769,9 @@ package body Contracts is Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id); end if; + elsif Prag_Nam = Name_Exceptional_Cases then + Analyze_Exceptional_Cases_In_Decl_Part (Prag); + elsif Prag_Nam = Name_Subprogram_Variant then Analyze_Subprogram_Variant_In_Decl_Part (Prag); @@ -1493,6 +1499,7 @@ package body Contracts is -- The stub acts as its own spec, the applicable pragmas are: -- Contract_Cases -- Depends + -- Exceptional_Cases -- Global -- Postcondition -- Precondition @@ -2830,6 +2837,9 @@ package body Contracts is Decls => Decls, Stmts => Stmts); + elsif Pragma_Name (Prag) = Name_Exceptional_Cases then + Expand_Pragma_Exceptional_Cases (Prag); + elsif Pragma_Name (Prag) = Name_Subprogram_Variant then Expand_Pragma_Subprogram_Variant (Prag => Prag, diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index 0a03d19d431..a53565fe003 100644 --- a/gcc/ada/contracts.ads +++ b/gcc/ada/contracts.ads @@ -81,6 +81,7 @@ package Contracts is -- -- Contract_Cases (stand alone subprogram body) -- Depends (stand alone subprogram body) + -- Exceptional_Cases (stand alone subprogram body) -- Global (stand alone subprogram body) -- Postcondition (stand alone subprogram body) -- Precondition (stand alone subprogram body) @@ -99,6 +100,7 @@ package Contracts is -- -- Contract_Cases -- Depends + -- Exceptional_Cases -- Global -- Postcondition -- Precondition diff --git a/gcc/ada/einfo-utils.adb b/gcc/ada/einfo-utils.adb index 5916188fa84..fa28a9e0100 100644 --- a/gcc/ada/einfo-utils.adb +++ b/gcc/ada/einfo-utils.adb @@ -1018,6 +1018,7 @@ package body Einfo.Utils is Is_CTC : constant Boolean := Id = Pragma_Contract_Cases or else + Id = Pragma_Exceptional_Cases or else Id = Pragma_Subprogram_Variant or else Id = Pragma_Test_Case; diff --git a/gcc/ada/einfo-utils.ads b/gcc/ada/einfo-utils.ads index 174994647bc..e8055020a67 100644 --- a/gcc/ada/einfo-utils.ads +++ b/gcc/ada/einfo-utils.ads @@ -447,6 +447,7 @@ package Einfo.Utils is -- Depends -- Effective_Reads -- Effective_Writes + -- Exceptional_Cases -- Global -- Initial_Condition -- Initializes diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index c6b3bed5425..e660196c0f1 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -1978,6 +1978,47 @@ package body Exp_Prag is In_Assertion_Expr := In_Assertion_Expr - 1; end Expand_Pragma_Contract_Cases; + ------------------------------------- + -- Expand_Pragma_Exceptional_Cases -- + ------------------------------------- + + -- Aspect Exceptional_Cases shoule be expanded in the following manner: + + -- Original declaration + + -- procedure P (...) with + -- Exceptional_Cases => + -- (Exp_1 => True, + -- Exp_2 => Post_4); + + -- Expanded body + + -- procedure P (...) is + -- begin + -- -- normal body of of P + -- declare + -- ... + -- end; + -- + -- exception + -- when Exp1 => + -- pragma Assert (True); + -- raise; + -- when E : Exp2 => + -- pragma Assert (Post_4); + -- raise; + -- when others => + -- pragma Assert (False); + -- raise; + -- end P; + + procedure Expand_Pragma_Exceptional_Cases (Prag : Node_Id) is + begin + -- Currently we don't expand this pragma + + Rewrite (Prag, Make_Null_Statement (Sloc (Prag))); + end Expand_Pragma_Exceptional_Cases; + --------------------------------------- -- Expand_Pragma_Import_Or_Interface -- --------------------------------------- diff --git a/gcc/ada/exp_prag.ads b/gcc/ada/exp_prag.ads index 27c537c46ca..9f810dab227 100644 --- a/gcc/ada/exp_prag.ads +++ b/gcc/ada/exp_prag.ads @@ -42,6 +42,10 @@ package Exp_Prag is -- Subp_Id's body. All generated code is added to list Stmts. If Stmts is -- No_List on entry, a new list is created. + procedure Expand_Pragma_Exceptional_Cases (Prag : Node_Id); + -- Given pragma Exceptional_Cases Prag, create the circuitry needed to + -- catch exceptions and evaluate consequence expressions. + procedure Expand_Pragma_Initial_Condition (Pack_Id : Entity_Id; N : Node_Id); diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index b2ff7c9e405..b7dafde9cf9 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -315,6 +315,7 @@ package body Inline is -- Contract_Cases -- Global -- Depends + -- Exceptional_Cases -- Postcondition -- Precondition -- Refined_Global @@ -5165,6 +5166,7 @@ package body Inline is and then Chars (Item_Id) in Name_Contract_Cases | Name_Global | Name_Depends + | Name_Exceptional_Cases | Name_Postcondition | Name_Precondition | Name_Refined_Global diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 4a3517d2297..ac50c846bf9 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1371,6 +1371,7 @@ begin | Pragma_Elaboration_Checks | Pragma_Eliminate | Pragma_Enable_Atomic_Synchronization + | Pragma_Exceptional_Cases | Pragma_Export | Pragma_Export_Function | Pragma_Export_Object diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 91a1fad444c..b8cd16080fe 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -263,7 +263,8 @@ package body Sem_Ch12 is -- package subprogram [body] -- Abstract_State Contract_Cases -- Initial_Condition Depends - -- Initializes Extensions_Visible + -- Initializes Exceptional_Cases + -- Extensions_Visible -- Global -- package body Post -- Refined_State Post_Class diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 983f877e001..d40c70f6ee4 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1410,6 +1410,7 @@ package body Sem_Ch13 is -- Attach_Handler -- Contract_Cases -- Depends + -- Exceptional_Cases -- Ghost -- Global -- Initial_Condition @@ -1666,10 +1667,10 @@ package body Sem_Ch13 is -- analyzed right now. -- Note that there is a special handling for Pre, Post, Test_Case, - -- Contract_Cases and Subprogram_Variant aspects. In these cases, we do - -- not have to worry about delay issues, since the pragmas themselves - -- deal with delay of visibility for the expression analysis. Thus, we - -- just insert the pragma after the node N. + -- Contract_Cases, Exceptional_Cases and Subprogram_Variant aspects. + -- In these cases, we do not have to worry about delay issues, since the + -- pragmas themselves deal with delay of visibility for the expression + -- analysis. Thus, we just insert the pragma after the node N. -- Loop through aspects @@ -4287,8 +4288,9 @@ package body Sem_Ch13 is -- Case 4: Aspects requiring special handling - -- Pre/Post/Test_Case/Contract_Cases/Subprogram_Variant whose - -- corresponding pragmas take care of the delay. + -- Pre/Post/Test_Case/Contract_Cases/Exceptional_Cases and + -- Subprogram_Variant whose corresponding pragmas take care + -- of the delay. -- Pre/Post @@ -4520,6 +4522,19 @@ package body Sem_Ch13 is Insert_Pragma (Aitem); goto Continue; + -- Exceptional_Cases + + when Aspect_Exceptional_Cases => + Aitem := Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Exceptional_Cases); + + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; + -- Subprogram_Variant when Aspect_Subprogram_Variant => @@ -11280,6 +11295,7 @@ package body Sem_Ch13 is | Aspect_Depends | Aspect_Dimension | Aspect_Dimension_System + | Aspect_Exceptional_Cases | Aspect_Effective_Reads | Aspect_Effective_Writes | Aspect_Extensions_Visible diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index d80f78f4865..963c6dea238 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2104,6 +2104,298 @@ package body Sem_Prag is Set_Is_Analyzed_Pragma (N); end Analyze_Depends_In_Decl_Part; + -------------------------------------------- + -- Analyze_Exceptional_Cases_In_Decl_Part -- + -------------------------------------------- + + -- WARNING: This routine manages Ghost regions. Return statements must be + -- replaced by gotos which jump to the end of the routine and restore the + -- Ghost mode. + + procedure Analyze_Exceptional_Cases_In_Decl_Part + (N : Node_Id; + Freeze_Id : Entity_Id := Empty) + is + Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); + + procedure Analyze_Exceptional_Contract (Exceptional_Contract : Node_Id); + -- Verify the legality of a single exceptional contract + + procedure Check_Duplication (Id : Node_Id; Contracts : List_Id); + -- Iterate through the identifiers in each contract to find duplicates + + ---------------------------------- + -- Analyze_Exceptional_Contract -- + ---------------------------------- + + procedure Analyze_Exceptional_Contract (Exceptional_Contract : Node_Id) + is + Exception_Choice : Node_Id; + Consequence : Node_Id; + Errors : Nat; + + begin + if Nkind (Exceptional_Contract) /= N_Component_Association then + Error_Msg_N + ("wrong syntax in exceptional contract", Exceptional_Contract); + return; + end if; + + Exception_Choice := First (Choices (Exceptional_Contract)); + Consequence := Expression (Exceptional_Contract); + + while Present (Exception_Choice) loop + if Nkind (Exception_Choice) = N_Others_Choice then + if Present (Next (Exception_Choice)) + or else Present (Next (Exceptional_Contract)) + or else Present (Prev (Exception_Choice)) + then + Error_Msg_N + ("OTHERS must appear alone and last", Exception_Choice); + end if; + + else + Analyze (Exception_Choice); + + if Is_Entity_Name (Exception_Choice) + and then Ekind (Entity (Exception_Choice)) = E_Exception + then + if Present (Renamed_Entity (Entity (Exception_Choice))) + and then Entity (Exception_Choice) = Standard_Numeric_Error + then + Check_Restriction + (No_Obsolescent_Features, Exception_Choice); + + if Warn_On_Obsolescent_Feature then + Error_Msg_N + ("Numeric_Error is an obsolescent feature " & + "(RM J.6(1))?j?", + Exception_Choice); + Error_Msg_N + ("\use Constraint_Error instead?j?", + Exception_Choice); + end if; + end if; + + Check_Duplication + (Exception_Choice, List_Containing (Exceptional_Contract)); + + -- Check for exception declared within generic formal + -- package (which is illegal, see RM 11.2(8)). + + declare + Ent : Entity_Id := Entity (Exception_Choice); + Scop : Entity_Id; + + begin + if Present (Renamed_Entity (Ent)) then + Ent := Renamed_Entity (Ent); + end if; + + Scop := Scope (Ent); + while Scop /= Standard_Standard + and then Ekind (Scop) = E_Package + loop + if Nkind (Declaration_Node (Scop)) = + N_Package_Specification + and then + Nkind (Original_Node (Parent + (Declaration_Node (Scop)))) = + N_Formal_Package_Declaration + then + Error_Msg_NE + ("exception& is declared in generic formal " + & "package", Exception_Choice, Ent); + Error_Msg_N + ("\and therefore cannot appear in contract " + & "(RM 11.2(8))", Exception_Choice); + exit; + + -- If the exception is declared in an inner instance, + -- nothing else to check. + + elsif Is_Generic_Instance (Scop) then + exit; + end if; + + Scop := Scope (Scop); + end loop; + end; + else + Error_Msg_N ("exception name expected", Exception_Choice); + end if; + end if; + + Next (Exception_Choice); + end loop; + + -- Now analyze the expressions of this contract + + Errors := Serious_Errors_Detected; + + -- Preanalyze_Assert_Expression, but without enforcing any of the two + -- acceptable types. + + Preanalyze_Assert_Expression (Consequence, Any_Boolean); + + -- Emit a clarification message when the consequence contains at + -- least one undefined reference, possibly due to contract freezing. + + if Errors /= Serious_Errors_Detected + and then Present (Freeze_Id) + and then Has_Undefined_Reference (Consequence) + then + Contract_Freeze_Error (Spec_Id, Freeze_Id); + end if; + end Analyze_Exceptional_Contract; + + ----------------------- + -- Check_Duplication -- + ----------------------- + + procedure Check_Duplication (Id : Node_Id; Contracts : List_Id) is + Contract : Node_Id; + Id1 : Node_Id; + Id_Entity : Entity_Id := Entity (Id); + + begin + if Present (Renamed_Entity (Id_Entity)) then + Id_Entity := Renamed_Entity (Id_Entity); + end if; + + Contract := First (Contracts); + while Present (Contract) loop + Id1 := First (Choices (Contract)); + while Present (Id1) loop + + -- Only check against the exception choices which precede + -- Id in the contract, since the ones that follow Id have not + -- been analyzed yet and will be checked in a subsequent call. + + if Id = Id1 then + return; + + -- Duplication both simple and via a renaming across different + -- exceptional contracts is illegal. + + elsif Nkind (Id1) /= N_Others_Choice + and then + (Id_Entity = Entity (Id1) + or else Id_Entity = Renamed_Entity (Entity (Id1))) + and then Contract /= Parent (Id) + then + Error_Msg_Sloc := Sloc (Id1); + Error_Msg_NE ("exception choice duplicates &#", Id, Id1); + end if; + + Next (Id1); + end loop; + + Next (Contract); + end loop; + end Check_Duplication; + + -- Local variables + + Exceptional_Contracts : constant Node_Id := + Expression (Get_Argument (N, Spec_Id)); + + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit + + Exceptional_Contract : Node_Id; + Restore_Scope : Boolean := False; + + -- Start of processing for Analyze_Subprogram_Variant_In_Decl_Part + + begin + -- Do not analyze the pragma multiple times + + if Is_Analyzed_Pragma (N) then + return; + end if; + + -- Set the Ghost mode in effect from the pragma. Due to the delayed + -- analysis of the pragma, the Ghost mode at point of declaration and + -- point of analysis may not necessarily be the same. Use the mode in + -- effect at the point of declaration. + + Set_Ghost_Mode (N); + + -- Single and multiple contracts must appear in aggregate form. If this + -- is not the case, then either the parser of the analysis of the pragma + -- failed to produce an aggregate, e.g. when the contract is "null" or a + -- "(null record)". + + pragma Assert + (if Nkind (Exceptional_Contracts) = N_Aggregate + then Null_Record_Present (Exceptional_Contracts) + xor (Present (Component_Associations (Exceptional_Contracts)) + or + Present (Expressions (Exceptional_Contracts))) + else Nkind (Exceptional_Contracts) = N_Null); + + -- Only clauses of the following form are allowed: + -- + -- exceptional_contract ::= + -- [choice_parameter_specification:] + -- exception_choice {'|' exception_choice} => consequence + -- + -- where + -- + -- consequence ::= Boolean_expression + + if Nkind (Exceptional_Contracts) = N_Aggregate + and then Present (Component_Associations (Exceptional_Contracts)) + and then No (Expressions (Exceptional_Contracts)) + then + + -- Check that the expression is a proper aggregate (no parentheses) + + if Paren_Count (Exceptional_Contracts) /= 0 then + Error_Msg_F -- CODEFIX + ("redundant parentheses", Exceptional_Contracts); + end if; + + -- Ensure that the formal parameters are visible when analyzing all + -- clauses. This falls out of the general rule of aspects pertaining + -- to subprogram declarations. + + if not In_Open_Scopes (Spec_Id) then + Restore_Scope := True; + Push_Scope (Spec_Id); + + if Is_Generic_Subprogram (Spec_Id) then + Install_Generic_Formals (Spec_Id); + else + Install_Formals (Spec_Id); + end if; + end if; + + Exceptional_Contract := + First (Component_Associations (Exceptional_Contracts)); + while Present (Exceptional_Contract) loop + Analyze_Exceptional_Contract (Exceptional_Contract); + Next (Exceptional_Contract); + end loop; + + if Restore_Scope then + End_Scope; + end if; + + -- Otherwise the pragma is illegal + + else + Error_Msg_N ("wrong syntax for exceptional cases", N); + end if; + + Set_Is_Analyzed_Pragma (N); + + Restore_Ghost_Region (Saved_GM, Saved_IGR); + end Analyze_Exceptional_Cases_In_Decl_Part; + -------------------------------------------- -- Analyze_External_Property_In_Decl_Part -- -------------------------------------------- @@ -16280,6 +16572,142 @@ package body Sem_Prag is GNAT_Pragma; Process_Disable_Enable_Atomic_Sync (Name_Unsuppress); + ----------------------- + -- Exceptional_Cases -- + ----------------------- + + -- pragma Exceptional_Cases ( EXCEPTIONAL_CONTRACT_LIST ); + + -- EXCEPTIONAL_CONTRACT_LIST ::= + -- ( EXCEPTIONAL_CONTRACT {, EXCEPTIONAL_CONTRACT }) + + -- EXCEPTIONAL_CONTRACT ::= + -- EXCEPTION_CHOICE {'|' EXCEPTION_CHOICE} => CONSEQUENCE + -- + -- where + -- + -- CONSEQUENCE ::= boolean_EXPRESSION + + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks preanalyze the + -- expressions in: + + -- Analyze_Exceptional_Cases_In_Decl_Part + + -- * Expansion - The annotation is expanded during the expansion of + -- the related subprogram [body] contract as performed in: + + -- Expand_Subprogram_Contract + + -- * Template - The annotation utilizes the generic template of the + -- related subprogram [body] when it is: + + -- aspect on subprogram declaration + -- aspect on stand-alone subprogram body + -- pragma on stand-alone subprogram body + + -- The annotation must prepare its own template when it is: + + -- pragma on subprogram declaration + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram [body] is instantiated except for + -- the "pragma on subprogram declaration" case. In that scenario + -- the annotation must instantiate itself. + + when Pragma_Exceptional_Cases => Exceptional_Cases : declare + Spec_Id : Entity_Id; + Subp_Decl : Node_Id; + Subp_Spec : Node_Id; + + begin + GNAT_Pragma; + Check_No_Identifiers; + Check_Arg_Count (1); + + -- Ensure the proper placement of the pragma. Exceptional_Cases + -- must be associated with a subprogram declaration or a body that + -- acts as a spec. + + Subp_Decl := + Find_Related_Declaration_Or_Body (N, Do_Checks => True); + + -- Generic subprogram + + if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then + null; + + -- Body acts as spec + + elsif Nkind (Subp_Decl) = N_Subprogram_Body + and then No (Corresponding_Spec (Subp_Decl)) + then + null; + + -- Body stub acts as spec + + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then No (Corresponding_Spec_Of_Stub (Subp_Decl)) + then + null; + + -- Subprogram + + elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then + Subp_Spec := Specification (Subp_Decl); + + -- Pragma Exceptional_Cases is forbidden on null procedures, + -- as this may lead to potential ambiguities in behavior when + -- interface null procedures are involved. Also, it just + -- wouldn't make sense, because null procedures do not raise + -- exceptions. + + if Nkind (Subp_Spec) = N_Procedure_Specification + and then Null_Present (Subp_Spec) + then + Error_Msg_N (Fix_Error + ("pragma % cannot apply to null procedure"), N); + return; + end if; + + else + Pragma_Misplaced; + end if; + + Spec_Id := Unique_Defining_Entity (Subp_Decl); + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Ghost_Pragma (N, Spec_Id); + Ensure_Aggregate_Form (Get_Argument (N, Spec_Id)); + + -- Chain the pragma on the contract for further processing by + -- Analyze_Subprogram_Variant_In_Decl_Part. + + Add_Contract_Item (N, Defining_Entity (Subp_Decl)); + + -- Fully analyze the pragma when it appears inside a subprogram + -- body because it cannot benefit from forward references. + + if Nkind (Subp_Decl) in N_Subprogram_Body + | N_Subprogram_Body_Stub + then + -- The legality checks of pragma Subprogram_Variant are + -- affected by the SPARK mode in effect and the volatility + -- of the context. Analyze all pragmas in a specific order. + + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Volatile_Function); + Analyze_Subprogram_Variant_In_Decl_Part (N); + end if; + end Exceptional_Cases; + ------------ -- Export -- ------------ @@ -31580,6 +32008,7 @@ package body Sem_Prag is Pragma_Elaboration_Checks => 0, Pragma_Eliminate => 0, Pragma_Enable_Atomic_Synchronization => 0, + Pragma_Exceptional_Cases => -1, Pragma_Export => -1, Pragma_Export_Function => -1, Pragma_Export_Object => -1, diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index fa7e7073f5a..993ff7a986b 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -138,6 +138,7 @@ package Sem_Prag is Pragma_Compile_Time_Error => True, Pragma_Contract_Cases => True, Pragma_Default_Initial_Condition => True, + Pragma_Exceptional_Cases => True, Pragma_Initial_Condition => True, Pragma_Invariant => True, Pragma_Loop_Invariant => True, @@ -247,6 +248,13 @@ package Sem_Prag is -- Perform full analysis of delayed pragma Depends. This routine is also -- capable of performing basic analysis of pragma Refined_Depends. + procedure Analyze_Exceptional_Cases_In_Decl_Part + (N : Node_Id; + Freeze_Id : Entity_Id := Empty); + -- Perform full analysis of delayed pragma Exceptional_Cases. Freeze_Id is + -- the entity of [generic] package body or [generic] subprogram body which + -- caused "freezing" of the related contract where the pragma resides. + procedure Analyze_External_Property_In_Decl_Part (N : Node_Id; Expr_Val : out Boolean); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 9a0197cb45c..b28f2899894 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -20576,6 +20576,7 @@ package body Sem_Util is return Nam = Name_Contract_Cases or else Nam = Name_Depends + or else Nam = Name_Exceptional_Cases or else Nam = Name_Extensions_Visible or else Nam = Name_Global or else Nam = Name_Post diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 253d1dadeee..4028d370823 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -2343,6 +2343,7 @@ package Sem_Util is -- following subprogram contract annotations: -- Contract_Cases -- Depends + -- Exceptional_Cases -- Extensions_Visible -- Global -- Post diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index b0ac6f900ed..e6a27e62cc1 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -7963,8 +7963,8 @@ package Sinfo is -- operation) are also in this list. -- Contract_Test_Cases contains a collection of pragmas that correspond - -- to aspects/pragmas Contract_Cases, Test_Case and Subprogram_Variant. - -- The ordering in the list is in LIFO fashion. + -- to aspects/pragmas Contract_Cases, Exceptional_Cases, Test_Case and + -- Subprogram_Variant. The ordering in the list is in LIFO fashion. -- Classifications contains pragmas that either declare, categorize, or -- establish dependencies between subprogram or package inputs and diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index cf2efbbbb63..9868d97b740 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -552,6 +552,7 @@ package Snames is Name_Elaborate : constant Name_Id := N + $; -- Ada 83 Name_Elaborate_All : constant Name_Id := N + $; Name_Elaborate_Body : constant Name_Id := N + $; + Name_Exceptional_Cases : constant Name_Id := N + $; -- GNAT Name_Export : constant Name_Id := N + $; Name_Export_Function : constant Name_Id := N + $; -- GNAT Name_Export_Object : constant Name_Id := N + $; -- GNAT @@ -1848,6 +1849,7 @@ package Snames is Pragma_Elaborate, Pragma_Elaborate_All, Pragma_Elaborate_Body, + Pragma_Exceptional_Cases, Pragma_Export, Pragma_Export_Function, Pragma_Export_Object,