From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 94F483858296 for ; Tue, 13 Jun 2023 07:38:35 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 94F483858296 Authentication-Results: sourceware.org; dmarc=pass (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 2adb3069b0e04-4f62d93f38aso6397912e87.0 for ; Tue, 13 Jun 2023 00:38:35 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1686641914; x=1689233914; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=mdXpphyU9evnmU4DHqwhM/lcbONKUy6OrvMAV5nnoqw=; b=Djw6qJfeCD4c5R1cjiLWLjj3wDlGAukfKFHdgnX8SPivr6LmjbDWm196UBnqUpuHhq 9fWllhVg7G8UZuV1qRcm9WkKWnZ0GwVGj51goWyDjekDI9hEEnOEniTgvNueAlCMMYpU X2Ig03AwMsKbtShvmiYZ85512bNSLwiC0ADR+9YG55VPL3YB0ogpO+zqG/iPtSPY10E4 6UG54aT5dbFb89dLS29/FaBvP8+S8q9LhLIVl3aTBK/Suan5MD8NKXVIAOfLMO49xuyp 9bvvKgguYqqHBvUNlxE6G4XbUYRAxV/FE0UfuFssG5mvVLSuQHdFU2uIbq2OpnUb6MZQ PLwA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1686641914; x=1689233914; 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=mdXpphyU9evnmU4DHqwhM/lcbONKUy6OrvMAV5nnoqw=; b=ivYdeabtXg3c9BtbQXKSfKypnJKw0gySt/C6KOc1UEP7Tydc1OSqS1eiPTHJFcrCmA yVavukgOkmwQ4JIkGBCqWs0ISpnBE5JwLnLc7ec85ZKWWG8L2pEuuu0WcVIfWOrqd7xN lorAd8T8/DB07C3Ao97sYwlVvkPf252ha+Vbl9csYCJ3DvHSUid8Y7O7uxIzDrjvQoPC n4d57HZIHDN/Hsxbu009CsuVxlp4Gw+2wghsm0XiqvvPCyCh1N5uAFDjzGzVS6Ffa9wp GCoQwprzBHf2HVHAGx/MOf7R6gvSBpQ29ZOlArOYgRAStzHMUC6xRz3czpf9SfSiUkKm KInQ== X-Gm-Message-State: AC+VfDxNIav4MgVpyek9IuUnnB8ALW+KGsMDNyqb7RiakMdj4+r345Vn 48JTEMoZAtV+Cl37XNH5GwAtyzyBpLrIAYXE/UaCxA== X-Google-Smtp-Source: ACHHUZ4Ri8BND2HqQs2dQi7jhDbG8UW7bPxzLCDjQRnIxUf34xkYbVQ8AYehqn87oGQNwHgOy8Hn3w== X-Received: by 2002:ac2:464d:0:b0:4f0:af5:5560 with SMTP id s13-20020ac2464d000000b004f00af55560mr6067955lfo.19.1686641913882; Tue, 13 Jun 2023 00:38:33 -0700 (PDT) Received: from localhost.localdomain ([2001:861:3382:1a90:bfa8:5d29:40e5:cc66]) by smtp.gmail.com with ESMTPSA id k15-20020a7bc40f000000b003f7f1b3aff1sm13541658wmi.26.2023.06.13.00.38.32 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 13 Jun 2023 00:38:33 -0700 (PDT) From: =?UTF-8?q?Marc=20Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [COMMITTED] ada: Implement new aspect Always_Terminates for SPARK Date: Tue, 13 Jun 2023 09:38:31 +0200 Message-Id: <20230613073831.240386-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit 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_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 List-Id: From: Piotr Trojanek This patch allows subprograms to be annotated with aspect Always_Terminates that requires a boolean expression. When this expression evaluates to True, the subprogram is required to terminate or raise an exception, but not loop infinitely. This aspect is only meant to be used by GNATprove and it has no meaningful run-time semantics: either the annotated subprogram terminates and then the aspect expression doesn't matter, or the subprogram loops infinitely and there is nothing we can do. (We could also evaluate the aspect expression just to detect run-time errors in the expression itself, but this can be implemented later, after a backend support for the aspect is added to GNATprove.) Implementation of this aspect is heavily based on the implementation of Subprogram_Variant, which in turn is heavily based on the implementation of Contract_Cases. Since the new aspect is not yet expanded, there is no corresponding assertion kind that would control the expansion. gcc/ada/ * aspects.ads (Aspect_Id): Add new aspect. (Implementation_Defined_Aspect): New aspect is implementation-defined. (Aspect_Argument): New aspect has an expression argument. (Is_Representation_Aspect): New aspect is not a representation aspect. (Aspect_Names): Link new aspect identifier with a name. (Aspect_Delay): New aspect is never delayed. * contracts.adb (Expand_Subprogram_Contract): Mention new aspect in comment. (Add_Contract_Item): Attach pragma corresponding to the new aspect to contract items. (Analyze_Entry_Or_Subprogram_Contract): Analyze pragma corresponding to the new aspect that appears with subprogram spec. (Analyze_Subprogram_Body_Stub_Contract): Expand pragma corresponding to the new aspect. * contracts.ads (Add_Contract_Item, Analyze_Entry_Or_Subprogram_Contract) (Analyze_Entry_Or_Subprogram_Body_Contract) (Analyze_Subprogram_Body_Stub_Contract): Mention new aspect in comment. * einfo-utils.adb (Get_Pragma): Return pragma attached to contract. * einfo-utils.ads (Get_Pragma): Mention new contract in comment. * exp_prag.adb (Expand_Pragma_Always_Terminates): Placeholder for possibly expanding new aspect. * exp_prag.ads (Expand_Pragma_Always_Terminates): Dedicated routine for expansion of the new aspect. * inline.adb (Remove_Aspects_And_Pragmas): Remove aspect from inlined bodies. * par-prag.adb (Prag): Postpone checking of the pragma until analysis. * sem_ch12.adb: Mention new aspect in explanation of handling contracts on generic units. * sem_ch13.adb (Analyze_Aspect_Specifications): Convert new aspect into a corresponding pragma. (Check_Aspect_At_Freeze_Point): Don't expect new aspect. * sem_prag.adb (Analyze_Always_Terminates_In_Decl_Part): Analyze pragma corresponding to the new aspect. (Analyze_Pragma): Handle pragma corresponding to the new aspect. (Is_Non_Significant_Pragma_Reference): Handle references appearing within new aspect. * sem_prag.ads (Aspect_Specifying_Pragma): New aspect can be emulated with a pragma. (Assertion_Expression_Pragma): New aspect has an assertion expression. (Pragma_Significant_To_Subprograms): New aspect is significant to subprograms. (Analyze_Always_Terminates_In_Decl_Part): Add spec for routine that analyses new aspect. (Find_Related_Declaration_Or_Body): Mention new aspect in comment. * sem_util.adb (Is_Subprogram_Contract_Annotation): New aspect is a subprogram contract annotation. * sem_util.ads (Is_Subprogram_Contract_Annotation): Mention new aspect in comment. * sinfo.ads (Is_Generic_Contract_Pragma): New pragma is a generic contract. (Contract): Explain attaching new pragma to subprogram contract. * snames.ads-tmpl (Name_Always_Terminates): New name for the new contract. (Pragma_Always_Terminates): New pragma identifier. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/aspects.ads | 6 ++ gcc/ada/contracts.adb | 29 ++++-- gcc/ada/contracts.ads | 4 + gcc/ada/einfo-utils.adb | 1 + gcc/ada/einfo-utils.ads | 1 + gcc/ada/exp_prag.adb | 10 ++ gcc/ada/exp_prag.ads | 4 + gcc/ada/inline.adb | 4 +- gcc/ada/par-prag.adb | 1 + gcc/ada/sem_ch12.adb | 7 +- gcc/ada/sem_ch13.adb | 30 ++++-- gcc/ada/sem_prag.adb | 199 ++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_prag.ads | 15 ++- gcc/ada/sem_util.adb | 3 +- gcc/ada/sem_util.ads | 1 + gcc/ada/sinfo.ads | 2 + gcc/ada/snames.ads-tmpl | 2 + 17 files changed, 295 insertions(+), 24 deletions(-) diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index bd8e7c61a83..19f7c07130f 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -72,6 +72,7 @@ package Aspects is Aspect_Address, Aspect_Aggregate, Aspect_Alignment, + Aspect_Always_Terminates, -- GNAT Aspect_Annotate, -- GNAT Aspect_Async_Readers, -- GNAT Aspect_Async_Writers, -- GNAT @@ -261,6 +262,7 @@ package Aspects is Implementation_Defined_Aspect : constant array (Aspect_Id) of Boolean := (Aspect_Abstract_State => True, + Aspect_Always_Terminates => True, Aspect_Annotate => True, Aspect_Async_Readers => True, Aspect_Async_Writers => True, @@ -370,6 +372,7 @@ package Aspects is Aspect_Address => Expression, Aspect_Aggregate => Expression, Aspect_Alignment => Expression, + Aspect_Always_Terminates => Expression, Aspect_Annotate => Expression, Aspect_Async_Readers => Optional_Expression, Aspect_Async_Writers => Optional_Expression, @@ -477,6 +480,7 @@ package Aspects is Aspect_Address => True, Aspect_Aggregate => False, Aspect_Alignment => True, + Aspect_Always_Terminates => False, Aspect_Annotate => False, Aspect_Async_Readers => False, Aspect_Async_Writers => False, @@ -630,6 +634,7 @@ package Aspects is Aspect_Aggregate => Name_Aggregate, Aspect_Alignment => Name_Alignment, Aspect_All_Calls_Remote => Name_All_Calls_Remote, + Aspect_Always_Terminates => Name_Always_Terminates, Aspect_Annotate => Name_Annotate, Aspect_Async_Readers => Name_Async_Readers, Aspect_Async_Writers => Name_Async_Writers, @@ -980,6 +985,7 @@ package Aspects is Aspect_Write => Always_Delay, Aspect_Abstract_State => Never_Delay, + Aspect_Always_Terminates => Never_Delay, Aspect_Annotate => Never_Delay, Aspect_Async_Readers => Never_Delay, Aspect_Async_Writers => Never_Delay, diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 19073d1e4d8..0e87cee3ef5 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -109,9 +109,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, Exceptional_Cases, Subprogram_Variant, - -- invariants and predicates. Body_Id denotes the entity of the - -- subprogram body. + -- well as Always_Terminates, Contract_Cases, Exceptional_Cases, + -- Subprogram_Variant, invariants and predicates. Body_Id denotes the + -- entity of the subprogram body. procedure Preanalyze_Condition (Subp : Entity_Id; @@ -225,6 +225,7 @@ package body Contracts is end if; -- Entry or subprogram declarations, the applicable pragmas are: + -- Always_Terminates -- Attach_Handler -- Contract_Cases -- Depends @@ -260,7 +261,8 @@ package body Contracts is then Add_Classification; - elsif Prag_Nam in Name_Contract_Cases + elsif Prag_Nam in Name_Always_Terminates + | Name_Contract_Cases | Name_Exceptional_Cases | Name_Subprogram_Variant | Name_Test_Case @@ -663,10 +665,10 @@ package body Contracts is Gen_Id => Spec_Id); end if; - -- Deal with preconditions, [refined] postconditions, Contract_Cases, - -- Exceptional_Cases, Subprogram_Variant, invariants and predicates - -- associated with body and its spec. Do not expand the contract of - -- subprogram body stubs. + -- Deal with preconditions, [refined] postconditions, Always_Terminates, + -- Contract_Cases, 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); @@ -789,7 +791,10 @@ package body Contracts is while Present (Prag) loop Prag_Nam := Pragma_Name (Prag); - if Prag_Nam = Name_Contract_Cases then + if Prag_Nam = Name_Always_Terminates then + Analyze_Always_Terminates_In_Decl_Part (Prag); + + elsif Prag_Nam = Name_Contract_Cases then -- Do not analyze the contract cases of an entry declaration -- unless annotating the original tree for GNATprove. @@ -1533,6 +1538,7 @@ package body Contracts is Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id); -- The stub acts as its own spec, the applicable pragmas are: + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases @@ -2879,7 +2885,10 @@ package body Contracts is Prag := Contract_Test_Cases (Items); while Present (Prag) loop if Is_Checked (Prag) then - if Pragma_Name (Prag) = Name_Contract_Cases then + if Pragma_Name (Prag) = Name_Always_Terminates then + Expand_Pragma_Always_Terminates (Prag); + + elsif Pragma_Name (Prag) = Name_Contract_Cases then Expand_Pragma_Contract_Cases (CCs => Prag, Subp_Id => Subp_Id, diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index d52e1aaed4a..c3dc5d67734 100644 --- a/gcc/ada/contracts.ads +++ b/gcc/ada/contracts.ads @@ -37,6 +37,7 @@ package Contracts is -- The following are valid pragmas: -- -- Abstract_State + -- Always_Terminates -- Async_Readers -- Async_Writers -- Attach_Handler @@ -81,6 +82,7 @@ package Contracts is -- subprogram body Body_Id as if they appeared at the end of a declarative -- region. Pragmas in question are: -- + -- Always_Terminates (stand alone subprogram body) -- Contract_Cases (stand alone subprogram body) -- Depends (stand alone subprogram body) -- Exceptional_Cases (stand alone subprogram body) @@ -100,6 +102,7 @@ package Contracts is -- subprogram Subp_Id as if they appeared at the end of a declarative -- region. The pragmas in question are: -- + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases @@ -175,6 +178,7 @@ package Contracts is -- stub Stub_Id as if they appeared at the end of a declarative region. The -- pragmas in question are: -- + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases diff --git a/gcc/ada/einfo-utils.adb b/gcc/ada/einfo-utils.adb index d1db66ff697..dad3a654743 100644 --- a/gcc/ada/einfo-utils.adb +++ b/gcc/ada/einfo-utils.adb @@ -1017,6 +1017,7 @@ package body Einfo.Utils is -- Contract / subprogram variant / test case pragmas Is_CTC : constant Boolean := + Id = Pragma_Always_Terminates or else Id = Pragma_Contract_Cases or else Id = Pragma_Exceptional_Cases or else Id = Pragma_Subprogram_Variant or else diff --git a/gcc/ada/einfo-utils.ads b/gcc/ada/einfo-utils.ads index e8055020a67..fee771c20f4 100644 --- a/gcc/ada/einfo-utils.ads +++ b/gcc/ada/einfo-utils.ads @@ -439,6 +439,7 @@ package Einfo.Utils is -- node, otherwise Empty is returned. The following contract pragmas that -- appear in N_Contract nodes are also handled by this routine: -- Abstract_State + -- Always_Terminates -- Async_Readers -- Async_Writers -- Attach_Handler diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index e660196c0f1..1cc4653a3b0 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -269,6 +269,16 @@ package body Exp_Prag is end; end Expand_Pragma_Abort_Defer; + ------------------------------------- + -- Expand_Pragma_Always_Terminates -- + ------------------------------------- + + procedure Expand_Pragma_Always_Terminates (Prag : Node_Id) is + pragma Unreferenced (Prag); + begin + null; + end Expand_Pragma_Always_Terminates; + -------------------------- -- Expand_Pragma_Check -- -------------------------- diff --git a/gcc/ada/exp_prag.ads b/gcc/ada/exp_prag.ads index 9f810dab227..10ccaf70c67 100644 --- a/gcc/ada/exp_prag.ads +++ b/gcc/ada/exp_prag.ads @@ -31,6 +31,10 @@ package Exp_Prag is procedure Expand_N_Pragma (N : Node_Id); + procedure Expand_Pragma_Always_Terminates (Prag : Node_Id); + -- This routine only exists for consistency with other pragmas, since + -- Always_Terminates has no meaningful expansion. + procedure Expand_Pragma_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id; diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index a4c32e984da..edb90a9fe20 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -312,6 +312,7 @@ package body Inline is -- Remove all aspects and/or pragmas that have no meaning in inlined body -- Body_Decl. The analysis of these items is performed on the non-inlined -- body. The items currently removed are: + -- Always_Terminates -- Contract_Cases -- Global -- Depends @@ -5225,7 +5226,8 @@ package body Inline is end if; if Present (Item_Id) - and then Chars (Item_Id) in Name_Contract_Cases + and then Chars (Item_Id) in Name_Always_Terminates + | Name_Contract_Cases | Name_Global | Name_Depends | Name_Exceptional_Cases diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index ac50c846bf9..b1398625fe2 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1315,6 +1315,7 @@ begin | Pragma_Aggregate_Individually_Assign | Pragma_All_Calls_Remote | Pragma_Allow_Integer_Address + | Pragma_Always_Terminates | Pragma_Annotate | Pragma_Assert | Pragma_Assert_And_Cut diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index a38ab284ce7..f584a9f3fb5 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -261,9 +261,10 @@ package body Sem_Ch12 is -- as annotations: -- package subprogram [body] - -- Abstract_State Contract_Cases - -- Initial_Condition Depends - -- Initializes Exceptional_Cases + -- Abstract_State Always_Terminates + -- Initial_Condition Contract_Cases + -- Initializes Depends + -- Exceptional_Cases -- Extensions_Visible -- Global -- package body Post diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 2b8b64aa392..e771c0d2020 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1407,6 +1407,7 @@ package body Sem_Ch13 is Is_Instance : Boolean := False); -- Subsidiary to the analysis of aspects -- Abstract_State + -- Always_Terminates -- Attach_Handler -- Contract_Cases -- Depends @@ -1667,10 +1668,11 @@ package body Sem_Ch13 is -- analyzed right now. -- Note that there is a special handling for Pre, Post, Test_Case, - -- 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. + -- Contract_Cases, Always_Terminates, 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 @@ -4297,9 +4299,9 @@ package body Sem_Ch13 is -- Case 4: Aspects requiring special handling - -- Pre/Post/Test_Case/Contract_Cases/Exceptional_Cases and - -- Subprogram_Variant whose corresponding pragmas take care - -- of the delay. + -- Pre/Post/Test_Case/Contract_Cases/Always_Terminates/ + -- Exceptional_Cases and Subprogram_Variant whose corresponding + -- pragmas take care of the delay. -- Pre/Post @@ -4531,6 +4533,19 @@ package body Sem_Ch13 is Insert_Pragma (Aitem); goto Continue; + -- Always_Terminates + + when Aspect_Always_Terminates => + Aitem := Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Always_Terminates); + + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; + -- Exceptional_Cases when Aspect_Exceptional_Cases => @@ -11315,6 +11330,7 @@ package body Sem_Ch13 is -- Here is the list of aspects that don't require delay analysis when Aspect_Abstract_State + | Aspect_Always_Terminates | Aspect_Annotate | Aspect_Async_Readers | Aspect_Async_Writers diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index abc0e5dbb9d..bca4eb50430 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -420,6 +420,79 @@ package body Sem_Prag is end if; end Adjust_External_Name_Case; + -------------------------------------------- + -- Analyze_Always_Terminates_In_Decl_Part -- + -------------------------------------------- + + procedure Analyze_Always_Terminates_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); + Expr : 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 + + Errors : Nat; + Restore_Scope : Boolean := False; + + 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); + + -- Ensure that the subprogram and its formals are visible when analyzing + -- the expression of the pragma. + + if not In_Open_Scopes (Spec_Id) then + Restore_Scope := True; + + if Is_Generic_Subprogram (Spec_Id) then + Push_Scope (Spec_Id); + Install_Generic_Formals (Spec_Id); + else + Push_Scope (Spec_Id); + Install_Formals (Spec_Id); + end if; + end if; + + Errors := Serious_Errors_Detected; + Preanalyze_Assert_Expression (Expr, Standard_Boolean); + + -- Emit a clarification message when the expression 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 (Expr) + then + Contract_Freeze_Error (Spec_Id, Freeze_Id); + end if; + + if Restore_Scope then + End_Scope; + end if; + + -- Currently it is not possible to inline pre/postconditions on a + -- subprogram subject to pragma Inline_Always. + + Set_Is_Analyzed_Pragma (N); + + Restore_Ghost_Region (Saved_GM, Saved_IGR); + end Analyze_Always_Terminates_In_Decl_Part; + ----------------------------------------- -- Analyze_Contract_Cases_In_Decl_Part -- ----------------------------------------- @@ -13202,6 +13275,131 @@ package body Sem_Prag is Opt.Allow_Integer_Address := True; end if; + ----------------------- + -- Always_Terminates -- + ----------------------- + + -- pragma Always_Terminates (boolean_EXPRESSION); + + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks preanalyze the + -- expressions in: + + -- Analyze_Always_Terminates_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_Always_Terminates => Always_Terminates : 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 Always_Terminates 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 always + -- terminate anyway. + + 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); + + -- Chain the pragma on the contract for further processing by + -- Analyze_Always_Terminates_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 Always_Terminates 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_Always_Terminates_In_Decl_Part (N); + end if; + end Always_Terminates; + -------------- -- Annotate -- -------------- @@ -31990,6 +32188,7 @@ package body Sem_Prag is Pragma_Aggregate_Individually_Assign => 0, Pragma_All_Calls_Remote => -1, Pragma_Allow_Integer_Address => -1, + Pragma_Always_Terminates => -1, Pragma_Annotate => 93, Pragma_Assert => -1, Pragma_Assert_And_Cut => -1, diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 49c1d0b4892..e8e9856d8a3 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -38,6 +38,7 @@ package Sem_Prag is Aspect_Specifying_Pragma : constant array (Pragma_Id) of Boolean := (Pragma_Abstract_State => True, Pragma_All_Calls_Remote => True, + Pragma_Always_Terminates => True, Pragma_Annotate => True, Pragma_Async_Readers => True, Pragma_Async_Writers => True, @@ -133,7 +134,8 @@ package Sem_Prag is -- expression. Assertion_Expression_Pragma : constant array (Pragma_Id) of Boolean := - (Pragma_Assert => True, + (Pragma_Always_Terminates => True, + Pragma_Assert => True, Pragma_Assert_And_Cut => True, Pragma_Assume => True, Pragma_Check => True, @@ -210,7 +212,8 @@ package Sem_Prag is -- of subprogram bodies. Pragma_Significant_To_Subprograms : constant array (Pragma_Id) of Boolean := - (Pragma_Contract_Cases => True, + (Pragma_Always_Terminates => True, + Pragma_Contract_Cases => True, Pragma_Depends => True, Pragma_Exceptional_Cases => True, Pragma_Ghost => True, @@ -241,6 +244,13 @@ package Sem_Prag is procedure Analyze_Pragma (N : Node_Id); -- Analyze procedure for pragma reference node N + procedure Analyze_Always_Terminates_In_Decl_Part + (N : Node_Id; + Freeze_Id : Entity_Id := Empty); + -- Perform full analysis of delayed pragma Always_Terminates. 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_Contract_Cases_In_Decl_Part (N : Node_Id; Freeze_Id : Entity_Id := Empty); @@ -445,6 +455,7 @@ package Sem_Prag is (Prag : Node_Id; Do_Checks : Boolean := False) return Node_Id; -- Subsidiary to the analysis of pragmas + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index c736bc34bb1..b82978ba99e 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -20558,7 +20558,8 @@ package body Sem_Util is Nam := Pragma_Name (Item); end if; - return Nam = Name_Contract_Cases + return Nam = Name_Always_Terminates + or else Nam = Name_Contract_Cases or else Nam = Name_Depends or else Nam = Name_Exceptional_Cases or else Nam = Name_Extensions_Visible diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 539ebebafcb..3751fb73702 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -2349,6 +2349,7 @@ package Sem_Util is function Is_Subprogram_Contract_Annotation (Item : Node_Id) return Boolean; -- Determine whether aspect specification or pragma Item is one of the -- following subprogram contract annotations: + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index b565221f730..0efbd4479e0 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -1711,6 +1711,7 @@ package Sinfo is -- a source construct, applies to a generic unit or its body, and denotes -- one of the following contract-related annotations: -- Abstract_State + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases @@ -7978,6 +7979,7 @@ package Sinfo is -- establish dependencies between subprogram or package inputs and -- outputs. Currently the following pragmas appear in this list: -- Abstract_States + -- Always_Terminates -- Async_Readers -- Async_Writers -- Constant_After_Elaboration diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 135b2533f9b..5044abbc7d0 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -503,6 +503,7 @@ package Snames is Name_Abort_Defer : constant Name_Id := N + $; -- GNAT Name_Abstract_State : constant Name_Id := N + $; -- GNAT Name_All_Calls_Remote : constant Name_Id := N + $; + Name_Always_Terminates : constant Name_Id := N + $; -- GNAT Name_Assert : constant Name_Id := N + $; -- Ada 05 Name_Assert_And_Cut : constant Name_Id := N + $; -- GNAT Name_Assume : constant Name_Id := N + $; -- GNAT @@ -1813,6 +1814,7 @@ package Snames is Pragma_Abort_Defer, Pragma_Abstract_State, Pragma_All_Calls_Remote, + Pragma_Always_Terminates, Pragma_Assert, Pragma_Assert_And_Cut, Pragma_Assume, -- 2.40.0