From patchwork Mon Sep 15 13:01:14 2025 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: 120266 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 F16D23857823 for ; Mon, 15 Sep 2025 13:15:07 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org F16D23857823 Authentication-Results: sourceware.org; dkim=pass (2048-bit key, secure) header.d=adacore.com header.i=@adacore.com header.a=rsa-sha256 header.s=google header.b=HId1jnER X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x42a.google.com (mail-wr1-x42a.google.com [IPv6:2a00:1450:4864:20::42a]) by sourceware.org (Postfix) with ESMTPS id 3F4E0385C6C7 for ; Mon, 15 Sep 2025 13:01:57 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 3F4E0385C6C7 Authentication-Results: sourceware.org; dmarc=pass (p=quarantine dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com ARC-Filter: OpenARC Filter v1.0.0 sourceware.org 3F4E0385C6C7 Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::42a ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1757941317; cv=none; b=VXXSsNodhuhlx4RfkWWbsqtNoUvJSR4F/l3wyleyCrA6LNKqLvtOJN5ahZBxM2GbwM3JQS/L39U2tW8WEkDlcadKD669rpAvag7B0+onOKkTfU1eKDGpSxA78N7vpVmdiIAFRdx7NnE9mntgCi/HSOw304f0MvHobQWjuHGE0bc= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1757941317; c=relaxed/simple; bh=UYqJkIzjBei7uQ09eGvfeB9/3MiVtW2taAkpQAATam4=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=bm1PdpqdYr38h+vysBhuFjwkoC9/ZCuXad8FCVs9hKzaJ7s5C5qNqsGr02XNltnxJtUiFqRspEVsinFkhpcrSnA3i7FNIVJg3oWPPOwkP1txNveVGpuvpda2g1XrDpFgmr4Si5Y4V/is/XTZKMN14q7/3NVb3VfAPVpa2T9Ewao= ARC-Authentication-Results: i=1; server2.sourceware.org DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 3F4E0385C6C7 Received: by mail-wr1-x42a.google.com with SMTP id ffacd0b85a97d-3e957ca53d1so1294360f8f.0 for ; Mon, 15 Sep 2025 06:01:57 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1757941316; x=1758546116; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=kWS3zjN2UMMErw3jYRhZy9/DDEVLmKFuqXzrwC9jMrQ=; b=HId1jnERFPSzcHMfFWr2CN1ZbxldwfVTTNAVnc9BccBC5WYxksjEuijZviRkO7zDgc DjwCuojL+AHeoAVS+13jDxkE3l66rr6UV+AFcwvSOq+wwX6k8tr40shLnJPGgU/hjcz5 1yb77QX0EwGAIiekyKZGOmjNJjQumgyljDic0Sxd4eypike7nbjdBmNYZYaLPWG/fs9Q 54RyxIeQsQP9K3CB2RbqstPSP3zWNRU6osou5Z7/XQ0dE75nDqbb/4Jley7MDjdmeSbi EOetSQcPbiGx+9jzOeJMoBqGvn5h+jDIFaeIFlrhbe2KCEtTfXG/45O8GIoecJHTCa0n mcRg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1757941316; x=1758546116; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=kWS3zjN2UMMErw3jYRhZy9/DDEVLmKFuqXzrwC9jMrQ=; b=L0dPN0GTiBbEx2L79Wb3jCevhWcWHRgTdR4rd0AtE+gEKBAu5EtVKXGDyMp7vlXElL x8Qhhf3cHeJxjdBKXEPp9SAtdqRJwIo4QBlwaKRJJ1YguqqahqJcpDY75erHPkSBlr/+ XxTML9TcNtViPK/k4W2JzRROdvAHyU3rsteMPj4BQLreJcFSekGRrtEf4jKcjCLwJGgE 2Ehfb/2LH9tOw1wIo+g309/WR1n/y6bOdDY5CbyTvZSFOINLMiPcd0H5UwYn2IYt2GSm 8abhdCQ5VD5XCSW/+tKTtJA7LJvfT2UJd/u5nb7ooBbBj/2Ec0WMbVuUOR35CXwBAkWx AZOA== X-Gm-Message-State: AOJu0Yy0JrgUsqHSOlFgPYAZBsg9Qt0bGQs29EewB6ZhHsI+Te9xc458 agTUUCTTvsfz6QBRjtriP3+E+Y1LkYuDxMsK/KiG4QiUspuCOn0lhMfwGjDPO6KpCycTSEM6KOo YGyc= X-Gm-Gg: ASbGncs+INGqpmcEuYiA9WMTwTu54owvfoyAI4hGOYvoFFzOKxBMHjOkobntKF1wCg1 BwPNH4/gtMvVc2vsohPTeVonGPKWsppNW42WMjpshRQJMa4DR4m/yFPOFM8jrXfG4AeUpuvdVU/ rzkHdi1X/AImbEALgfdVCD4hWptgDP/lPHpewIMbAxwBMd4RoGaRs8lzzP8dqOQtR6upxnAJGo+ jixoxkBjaMjxAH36FGr7i5cxMcsUCSdL47nG/0S9FRYZz1tItH1uqpCWd0BpOH1dZS+NDMmRL/z hoMfUu8R/XOSKTATfitWFafdgOwBjh8cAPevYnkO7iwwtBlPabGNAM6NaX1G46naNUAy/D27TWl 5SEB+Sf0t5hJQsc1i00uUmsAYD+v5mWEzvQr6YGGkhn4pey9Nsn0mDh8K9ZiDpkDQxLl6NnNeJW Xr5Xu+a2QzknvpuEshLkwNl5lY9Mq5bf2v7tXHbQ== X-Google-Smtp-Source: AGHT+IGGEAw0gaOHYudeVNYimtgP+ZI557lo7lrIjPvjosmkmSVKpwCe/Odn7IslGQnWLsz9KtR9zg== X-Received: by 2002:a05:6000:4287:b0:3e9:b7a5:5dc9 with SMTP id ffacd0b85a97d-3e9b7a56e8emr4734021f8f.23.1757941315578; Mon, 15 Sep 2025 06:01:55 -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 ffacd0b85a97d-3ea4b52b7fcsm5428733f8f.33.2025.09.15.06.01.54 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 15 Sep 2025 06:01:55 -0700 (PDT) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Viljar Indus Subject: [COMMITTED 08/27] ada: Improve ghost region creation for pragmas Date: Mon, 15 Sep 2025 15:01:14 +0200 Message-ID: <20250915130135.2720894-8-poulhies@adacore.com> X-Mailer: git-send-email 2.43.0 In-Reply-To: <20250915130135.2720894-1-poulhies@adacore.com> References: <20250915130135.2720894-1-poulhies@adacore.com> MIME-Version: 1.0 X-Spam-Status: No, score=-13.4 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 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.30 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: gcc-patches-bounces~patchwork=sourceware.org@gcc.gnu.org From: Viljar Indus gcc/ada/ChangeLog: * atree.adb (Mark_New_Ghost_Node): Set Is_Implicit_Ghost for all newly created nodes. * gen_il-fields.ads (Is_Implicit_Ghost): New attribute. * gen_il-gen-gen_entities.adb (Entity_Kind): Add Is_Implicit_Ghost attribute. * ghost.adb (Ghost_Policy_In_Effect): Implicit_Ghost_Entities inside pragmas get the ghost mode from the region isntead of the global ghost policy. (Ghost_Assertion_Level_In_Effect): New function that returns the applicable assertion level for the given entity in a similar manner as Ghost_Policy_In_Effect. (Install_Ghost_Region): Set Is_Inside_Statement_Or_Pragma attribute. (Mark_And_Set_Ghost_Body): Update the logic for deriving the ghost region. (Set_Ghost_Mode): Ignored pragmas attached to checked ghost entities now create an ignored ghost region. Pragmas attached to non-ghost entities create the ghost region based on the policy applied to the given pragma. * opt.ads (Ghost_Config_Type): add new attribute Is_Inside_Statement_Or_Pragama to track whether we should take the active ghost mode from the ghost region for implicit ghost entities. * sem_prag.adb (Analyze_Pragma): Mark entities that have an explicit ghost pragma as non-implicit ghost. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/atree.adb | 2 + gcc/ada/gen_il-fields.ads | 1 + gcc/ada/gen_il-gen-gen_entities.adb | 1 + gcc/ada/ghost.adb | 138 +++++++++++++++++++--------- gcc/ada/opt.ads | 6 ++ gcc/ada/sem_prag.adb | 1 + 6 files changed, 106 insertions(+), 43 deletions(-) diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 197d1ee51210..14d9ba4bb2fd 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -1807,6 +1807,7 @@ package body Atree is Set_Is_Checked_Ghost_Entity (N); Set_Ghost_Assertion_Level (N, Ghost_Config.Ghost_Mode_Assertion_Level); + Set_Is_Implicit_Ghost (N); end if; elsif Ghost_Config.Ghost_Mode = Ignore then @@ -1814,6 +1815,7 @@ package body Atree is Set_Is_Ignored_Ghost_Entity (N); Set_Ghost_Assertion_Level (N, Ghost_Config.Ghost_Mode_Assertion_Level); + Set_Is_Implicit_Ghost (N); end if; Set_Is_Ignored_Ghost_Node (N); diff --git a/gcc/ada/gen_il-fields.ads b/gcc/ada/gen_il-fields.ads index c9f9bc2c5ba6..6ff9866e6431 100644 --- a/gcc/ada/gen_il-fields.ads +++ b/gcc/ada/gen_il-fields.ads @@ -743,6 +743,7 @@ package Gen_IL.Fields is Is_Immediately_Visible, Is_Implementation_Defined, Is_Implicit_Full_View, + Is_Implicit_Ghost, Is_Imported, Is_Independent, Is_Initial_Condition_Procedure, diff --git a/gcc/ada/gen_il-gen-gen_entities.adb b/gcc/ada/gen_il-gen-gen_entities.adb index dd07b7a6e6e5..476e69d22cc0 100644 --- a/gcc/ada/gen_il-gen-gen_entities.adb +++ b/gcc/ada/gen_il-gen-gen_entities.adb @@ -159,6 +159,7 @@ begin -- Gen_IL.Gen.Gen_Entities Sm (Is_Ignored_Ghost_Entity, Flag), Sm (Is_Immediately_Visible, Flag), Sm (Is_Implementation_Defined, Flag), + Sm (Is_Implicit_Ghost, Flag), Sm (Is_Imported, Flag), Sm (Is_Independent, Flag), Sm (Is_Inlined, Flag), diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index ae20ef972c82..bfe6bff0751e 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -94,15 +94,30 @@ package body Ghost is -- Returns the Assertion_Level entity if the node has a Ghost aspect and -- the Ghost aspect is using an Assertion_Level. + function Ghost_Assertion_Level_In_Effect (Id : Entity_Id) return Entity_Id; + -- Returns the ghost level applicable for the given entity Id in a similar + -- manner as Ghost_Policy_In_Effect. + function Ghost_Policy_In_Effect (Id : Entity_Id) return Name_Id; - -- Returns the first Assertion Policy in place for either Ghost or the - -- Assertion_Level associated with Ghost aspect on the the declaration node - -- Decl. + -- Returns the ghost policy applicable for the given entity Id. + -- + -- SPARK RM 6.9 (3): + -- + -- An object declaration which occurs inside an expression in a ghost + -- declaration, statement, assertion pragma or specification aspect + -- declaration is a ghost declaration. + -- + -- If this declaration does not have the Ghost aspect specified, the + -- assertion policy applicable to this declaration comes from the policy + -- applicable to the enclosing declaration, statement, assertion pragma + -- or specification aspect. + -- + -- Otherwise, the assertion policy applicable to an object declaration + -- comes either from its assertion level if any, or from the ghost + -- policy at the point of declaration. procedure Install_Ghost_Region - (Mode : Name_Id; - N : Node_Id; - Level : Entity_Id); + (Mode : Name_Id; N : Node_Id; Level : Entity_Id); pragma Inline (Install_Ghost_Region); -- Install a Ghost region comprised of mode Mode and ignored region start -- node N and Level as the Assertion_Level that was associated with it. @@ -1561,6 +1576,22 @@ package body Ghost is return Empty; end Get_Ghost_Assertion_Level; + ------------------------------------- + -- Ghost_Assertion_Level_In_Effect -- + ------------------------------------- + + function Ghost_Assertion_Level_In_Effect (Id : Entity_Id) return Entity_Id + is + begin + if Ghost_Config.Is_Inside_Statement_Or_Pragma + and then Is_Implicit_Ghost (Id) + then + return Ghost_Config.Ghost_Mode_Assertion_Level; + else + return Ghost_Assertion_Level (Id); + end if; + end Ghost_Assertion_Level_In_Effect; + ---------------------------- -- Ghost_Policy_In_Effect -- ---------------------------- @@ -1570,7 +1601,22 @@ package body Ghost is Level_Nam : constant Name_Id := (if No (Level) then No_Name else Chars (Level)); begin - return Policy_In_Effect (Name_Ghost, Level_Nam); + if Ghost_Config.Is_Inside_Statement_Or_Pragma + and then Is_Implicit_Ghost (Id) + then + case Ghost_Config.Ghost_Mode is + when Check => + return Name_Check; + + when Ignore => + return Name_Ignore; + + when None => + return No_Name; + end case; + else + return Policy_In_Effect (Name_Ghost, Level_Nam); + end if; end Ghost_Policy_In_Effect; -------------------------------- @@ -1642,12 +1688,18 @@ package body Ghost is Ghost_Config.Current_Region := N; Ghost_Config.Ghost_Mode := Mode; Ghost_Config.Ghost_Mode_Assertion_Level := Level; + + if Nkind (Ghost_Config.Current_Region) + in N_Statement_Other_Than_Procedure_Call + | N_Procedure_Call_Statement + | N_Pragma + then + Ghost_Config.Is_Inside_Statement_Or_Pragma := True; + end if; end Install_Ghost_Region; procedure Install_Ghost_Region - (Mode : Name_Id; - N : Node_Id; - Level : Entity_Id) is + (Mode : Name_Id; N : Node_Id; Level : Entity_Id) is begin Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N, Level); end Install_Ghost_Region; @@ -1657,14 +1709,13 @@ package body Ghost is ------------------------- function Is_Assertion_Level_Dependent - (Self : Entity_Id; Other : Entity_Id) return Boolean - is + (Self : Entity_Id; Other : Entity_Id) return Boolean is begin return - Self = Standard_Level_Default - or else Other = Standard_Level_Default - or else Is_Same_Or_Depends_On_Level (Self, Other) - or else Is_Same_Or_Depends_On_Level (Self, Standard_Level_Static); + Self = Standard_Level_Default + or else Other = Standard_Level_Default + or else Is_Same_Or_Depends_On_Level (Self, Other) + or else Is_Same_Or_Depends_On_Level (Self, Standard_Level_Static); end Is_Assertion_Level_Dependent; ------------------------- @@ -1977,10 +2028,7 @@ package body Ghost is -- Mark_And_Set_Ghost_Body -- ----------------------------- - procedure Mark_And_Set_Ghost_Body - (N : Node_Id; - Spec_Id : Entity_Id) - is + procedure Mark_And_Set_Ghost_Body (N : Node_Id; Spec_Id : Entity_Id) is Body_Id : constant Entity_Id := Defining_Entity (N); Level : Entity_Id := Empty; Policy : Name_Id := No_Name; @@ -1991,10 +2039,10 @@ package body Ghost is if Is_Subject_To_Ghost (N) then if Present (Spec_Id) then Policy := Ghost_Policy_In_Effect (Spec_Id); - Level := Ghost_Assertion_Level (Spec_Id); + Level := Ghost_Assertion_Level_In_Effect (Spec_Id); else Policy := Ghost_Policy_In_Effect (Body_Id); - Level := Ghost_Assertion_Level (Body_Id); + Level := Ghost_Assertion_Level_In_Effect (Body_Id); end if; -- A body declared within a Ghost region is automatically Ghost @@ -2002,11 +2050,11 @@ package body Ghost is elsif Ghost_Config.Ghost_Mode = Check then Policy := Name_Check; - Level := Ghost_Config.Ghost_Mode_Assertion_Level; + Level := Ghost_Config.Ghost_Mode_Assertion_Level; elsif Ghost_Config.Ghost_Mode = Ignore then Policy := Name_Ignore; - Level := Ghost_Config.Ghost_Mode_Assertion_Level; + Level := Ghost_Config.Ghost_Mode_Assertion_Level; -- Inherit the "ghostness" of the previous declaration when the body -- acts as a completion. @@ -2025,13 +2073,7 @@ package body Ghost is -- The Ghost policy in effect at the point of declaration and at the -- point of completion must match (SPARK RM 6.9(16)). - Check_Ghost_Completion - (Prev_Id => Spec_Id, - Compl_Id => Body_Id); - - if Present (Level) then - Set_Ghost_Assertion_Level (Body_Id, Level); - end if; + Check_Ghost_Completion (Prev_Id => Spec_Id, Compl_Id => Body_Id); -- Mark the body as its formals as Ghost @@ -2441,16 +2483,15 @@ package body Ghost is end if; end Mark_Ghost_Pragma; - procedure Mark_Ghost_Pragma - (N : Node_Id; - Mode : Ghost_Mode_Type) - is + procedure Mark_Ghost_Pragma (N : Node_Id; Mode : Ghost_Mode_Type) is begin if Mode = Check then - Set_Is_Checked_Ghost_Pragma (N); + Set_Is_Checked_Ghost_Pragma (N, True); + Set_Is_Ignored_Ghost_Pragma (N, False); else - Set_Is_Ignored_Ghost_Pragma (N); + Set_Is_Checked_Ghost_Pragma (N, False); + Set_Is_Ignored_Ghost_Pragma (N, True); Set_Is_Ignored_Ghost_Node (N); Record_Ignored_Ghost_Node (N); end if; @@ -2460,10 +2501,7 @@ package body Ghost is -- Mark_Ghost_Renaming -- ------------------------- - procedure Mark_Ghost_Renaming - (N : Node_Id; - Id : Entity_Id) - is + procedure Mark_Ghost_Renaming (N : Node_Id; Id : Entity_Id) is Policy : Name_Id := No_Name; Level : constant Entity_Id := Ghost_Assertion_Level (Id); begin @@ -2661,12 +2699,26 @@ package body Ghost is elsif Nkind (N) = N_Pragma then Level := Pragma_Ghost_Assertion_Level (N); + if Is_Checked_Ghost_Pragma (N) then - Install_Ghost_Region (Check, N, Level); + + -- Still install an ignored ghost region if the pragma is attached + -- to a checked ghost entity, but the pragma itself is explicitly + -- ignored. + + if Is_Ignored (N) then + Install_Ghost_Region (Ignore, N, Level); + else + Install_Ghost_Region (Check, N, Level); + end if; elsif Is_Ignored_Ghost_Pragma (N) then Install_Ghost_Region (Ignore, N, Level); else - Install_Ghost_Region (None, N, Level); + if Is_Checked (N) then + Install_Ghost_Region (Check, N, Level); + else + Install_Ghost_Region (None, N, Level); + end if; end if; -- The Ghost mode of a procedure call depends on the Ghost mode of the diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 109d28245de9..ea3390e2b482 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -767,6 +767,12 @@ package Opt is Current_Region : Node_Id := Empty; -- Latest ghost region + + Is_Inside_Statement_Or_Pragma : Boolean := False; + -- A flag to tag whether we are currently in a region that originated + -- from a Statement or a pragma. Inside those regions the ghost policy + -- in effect for implicitly defined entities is not the policy for Ghost + -- but instead the policy for the region (SPARK RM 6.9 (3)). end record; Ghost_Config : Ghost_Config_Type; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 00c9b17ff6ee..a17d9d2b8138 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -19428,6 +19428,7 @@ package body Sem_Prag is -- pragma Ghost (False). if Is_Ghost then + Set_Is_Implicit_Ghost (Id, False); Set_Is_Ghost_Entity (Id); end if; end Ghost;