From patchwork Thu Sep 11 09:18:50 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: 120042 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 7F053385842F for ; Thu, 11 Sep 2025 09:32:16 +0000 (GMT) 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 511663858415 for ; Thu, 11 Sep 2025 09:19:31 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 511663858415 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 511663858415 Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::331 ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1757582371; cv=none; b=M2Jqb3KfzXeRxbDBoFxQI3D2Hq3P3qkCvLp/bXHphqAVwOGvt85pJqVZCw9JSfqvTUy/UQGwU6ydoMr4bNK3ijddz/8J/nrFLTdFY6e/eliYlL4Z2K8OvTCxza1h4fUXd+Pt39nBYPmOWZDtT9cyPuudB5wf+JYWbTP0EXcuOmw= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1757582371; c=relaxed/simple; bh=e0SgPGLNOGJfhQSfLzX0DJdmCBup70AsgYvbXDqEHi0=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=Q2OJ1ReJNpMxm/fcg5gM5Mwvmj5uz9XNQSZZOn3dZPKWlTTJ1pGZJQocefm/TDdoJy9Fdo3cKqcWPojGqcRAFl6fWL65zAnWA8/Wcyyo7qrKUG8wXrJ2HcebSr+atZxKuFUUhaMMNE3uFeZDmjdB2VdB/8HJ5FG9qqkPnPctDGY= ARC-Authentication-Results: i=1; server2.sourceware.org DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 511663858415 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=TS6qqlAN Received: by mail-wm1-x331.google.com with SMTP id 5b1f17b1804b1-45cb6180b60so3361845e9.0 for ; Thu, 11 Sep 2025 02:19:31 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1757582370; x=1758187170; 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=ooT0W1t//rTkSNhPFhJ843TmtY1EynfMVb2Bz803pq0=; b=TS6qqlANA/vx3/wLfEMAqiG8bppdSGAJSCBbJHuwziOFxINeoLNOCCflhZ/2r3G/R0 V5c70cfBVYSICa9SRJYtXCsS37o9DuKgJ8EaU6BItZpSq/FZMSRk87mrcnRLkC2Q4hha 5Gt6llRFuCXEVPDk9KoWOVL7siuCZiQiP13KLVAqCxa86b5UqrgRrprfISCfEoODWWAT KR0nqat35vi82xDOFWKaKP2Qx1zasGLj42r9jZmOHWpeNnbuYKYel84F2Za7IV1C9Ima blE4sGOIzMDzoThzWw6wx3QOvbKo7LA+V/TCTNGz1+zWIOntENB9nxSKtoyOMi/BOgc6 oQyQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1757582370; x=1758187170; 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=ooT0W1t//rTkSNhPFhJ843TmtY1EynfMVb2Bz803pq0=; b=kgDP0Wk8UYvK35J5YpjiAcNd6tg7jN3XNiL+CVZDYAa6kpQ4JixPjYZm92az9edIyK uGjxQ8vcuDYvvOp8SB5qRoJECDMaHCGBIZniVUVv8tD8TpBLqQo0XpokQfIJgqK27F/q am6xOGxS0wvB6RjoZhJcjJbh+n1eRRuQ53wZhPCMLL+yfhGCh0scpeCcjO49PXYXZXfr xQohFnJ2diTJkLPXEiJNFbs7ozP4fJMzddD5U70Ldqg2APxvRISwZ5QcgCkTxA0toqUA 7WoIh0PTam3K6+Yx0+EWmQ3zIcw7dyrJS2iVIdo7TU8pLH48srUGYON5UN1hfKbpTOOX 1B9A== X-Gm-Message-State: AOJu0YyLdi2e9vpNKTPsFeIeVztATOj1ik19TpmscQVcLZae3OnTrqsB mCeuQqZNUBuRQyH49KKSW3ENsQOms+ynNncDYBRPawu6HQ0Qv1sZacYADA3IXYw0+vV0t+lcP8b m7QY= X-Gm-Gg: ASbGncu/g5WuP8YB3P/DpiUC5+ruLQNlJ+S6kdP5rLeX1UW9i+FiaX91RubCzGnMWVX ryIhDsVgVN7UV1i1WkyAdpWLohbeE1ImCKl/aR4y3cnBrIx5eugX49/mnbrBjPIsv/4ozPD9Glk gR0k42KDSjq8h8TT9Xn1OGdEibTdIO12bwBuw+/AF142AW8wndq1r8LCqSBEsrt157JFUu0cFsw G7TVfzlltueTR8QAkqdOtVdavOHoZTz5zdQv8VIYi21rHuSMLMNhJxNtXNWgVHw6NTQu7bAGuAs KfOl4D4Z6gMH3JiQi8UqNDYaWKd7WRPzGU05dRbd5dd94GuYe2EsNGUL4xgsIiBX3DaQCJh7kGr HhVMaEgPUM2lO5qO4hPZ8HjOoRxglrxtgZgy9hG2hRdFE/m7f/hcuhqEg0VLE7hdPLVrolSHeS5 s2h+qSVDeSqMiVHnzEF0Fg+JEOMrrex/Esop3b/g== X-Google-Smtp-Source: AGHT+IEW2q02LXVrhDqTp2un8nfJvmRjYzdsOfGH8I0PyXX1UWfJiiwT5Woz3I26kGOZ4As4Hx6MBA== X-Received: by 2002:a05:600c:34cb:b0:45d:e0cf:41c9 with SMTP id 5b1f17b1804b1-45de0cf447fmr155077625e9.22.1757582369936; Thu, 11 Sep 2025 02:19:29 -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-3e7607cd27dsm1649971f8f.41.2025.09.11.02.19.29 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 11 Sep 2025 02:19:29 -0700 (PDT) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Viljar Indus Subject: [COMMITTED 18/31] ada: Apply ghost regions for assigmnents correctly Date: Thu, 11 Sep 2025 11:18:50 +0200 Message-ID: <20250911091904.1505690-18-poulhies@adacore.com> X-Mailer: git-send-email 2.43.0 In-Reply-To: <20250911091904.1505690-1-poulhies@adacore.com> References: <20250911091904.1505690-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 When frontend is operating in GNATprove mode (where expander is disabled), it should check ghost policy for assignment statements just like it does for other statements. This is because we want ghost policy errors to be reported not just by GNAT, but also by GNATprove. Additionally we need to perform the checks for valid location of ghost assigments based on the region around the assigment before we create the region for the assignment itself. gcc/ada/ChangeLog: * ghost.adb (Mark_And_Set_Ghost_Assignment): Create a ghost region for an assigment irregardless of whether the expander is active. Relocate the Assignment validity checks from Is_OK_Statement to this subprogram. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/ghost.adb | 134 ++++++++++++++++++++-------------------------- 1 file changed, 57 insertions(+), 77 deletions(-) diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 7d8bcc2a96bc..bc646b22fbe5 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -515,15 +515,6 @@ package body Ghost is function Is_OK_Statement (Stmt : Node_Id; Id : Entity_Id; Call_Arg : Node_Id) return Boolean is - procedure Check_Assignment_Policies (Assignee : Entity_Id); - -- Check that: - -- * An ignored entity is not used to modify a checked ghost - -- entity in an assignment. - -- * A checked ghost assignment is not used in an ignored ghost - -- region. - -- * The level of the ghost region depends on the level of the - -- ghost assignment. - procedure Check_Procedure_Call_Policies (Callee : Entity_Id); -- Check that -- * the a checked call argument is not modified by an ignored @@ -537,61 +528,6 @@ package body Ghost is -- Check that Call_Arg was used in the call and that the formal -- for that argument was either out or in-out. - ------------------------------- - -- Check_Assignment_Policies -- - ------------------------------- - - procedure Check_Assignment_Policies (Assignee : Entity_Id) is - A_Policy : constant Name_Id := - Ghost_Policy_In_Effect (Assignee); - A_Level : constant Entity_Id := - Ghost_Assertion_Level (Assignee); - Id_Policy : constant Name_Id := Ghost_Policy_In_Effect (Id); - Region_Policy : constant Ghost_Mode_Type := - Ghost_Config.Ghost_Mode; - Region_Level : constant Entity_Id := - Ghost_Config.Ghost_Mode_Assertion_Level; - begin - if A_Policy = Name_Check and then Id_Policy = Name_Ignore then - Error_Msg_Sloc := Sloc (Ghost_Ref); - - Error_Msg_N (Ghost_Policy_Error_Msg, Ghost_Ref); - Error_Msg_NE ("\& has ghost policy `Ignore`", Ghost_Ref, Id); - Error_Msg_NE - ("\& used # to modify an entity with `Check`", - Ghost_Ref, - Id); - end if; - - if A_Policy = Name_Check and then Region_Policy = Ignore then - Error_Msg_N (Ghost_Policy_Error_Msg, Stmt); - Error_Msg_NE ("\& has ghost policy `Check`", Stmt, Assignee); - Error_Msg_NE - ("\& is modified in a region with `Ignore`", - Stmt, - Assignee); - end if; - - if Present (Region_Level) - and then not Is_Assertion_Level_Dependent - (Region_Level, A_Level) - then - Error_Msg_Sloc := Sloc (Stmt); - - Error_Msg_N (Assertion_Level_Error_Msg, Stmt); - Error_Msg_Name_1 := Chars (A_Level); - Error_Msg_NE ("\& has assertion level %", Stmt, Assignee); - Error_Msg_Name_1 := Chars (Region_Level); - Error_Msg_NE - ("\& is modified within a region with %", Stmt, Id); - Error_Msg_Name_1 := Chars (Region_Level); - Error_Msg_NE - ("\assertion level of & should depend on %", - Stmt, - Assignee); - end if; - end Check_Assignment_Policies; - ----------------------------------- -- Check_Procedure_Call_Policies -- ----------------------------------- @@ -683,9 +619,6 @@ package body Ghost is if Nkind (Stmt) = N_Assignment_Statement then if Is_Ghost_Assignment (Stmt) then - Check_Assignment_Policies - (Get_Enclosing_Ghost_Entity (Name (Stmt))); - return True; end if; @@ -1872,18 +1805,60 @@ package body Ghost is -- where P is a package, X is a record, and Comp is an array, we need -- to check the ghost flags of X. - Orig_Lhs : constant Node_Id := Name (N); - Id : Entity_Id; - Lhs : Node_Id; + procedure Check_Assignment_Policies (Assignee : Entity_Id); + -- Check that: + -- * A checked ghost assignment is not used in an ignored ghost + -- region. + -- * The level of the ghost region depends on the level of the + -- ghost assignment. + + ------------------------------- + -- Check_Assignment_Policies -- + ------------------------------- + + procedure Check_Assignment_Policies (Assignee : Entity_Id) is + Assignee_Policy : constant Name_Id := + Ghost_Policy_In_Effect (Assignee); + Assignee_Level : constant Entity_Id := + Ghost_Assertion_Level (Assignee); + Region_Policy : constant Ghost_Mode_Type := Ghost_Config.Ghost_Mode; + Region_Level : constant Entity_Id := + Ghost_Config.Ghost_Mode_Assertion_Level; + begin + if Assignee_Policy = Name_Check and then Region_Policy = Ignore then + Error_Msg_N (Ghost_Policy_Error_Msg, N); + Error_Msg_NE ("\& has ghost policy `Check`", N, Assignee); + Error_Msg_NE + ("\& is modified in a region with `Ignore`", N, Assignee); + end if; + + if Present (Region_Level) + and then not Is_Assertion_Level_Dependent + (Region_Level, Assignee_Level) + then + Error_Msg_Sloc := Sloc (N); + + Error_Msg_N (Assertion_Level_Error_Msg, N); + Error_Msg_Name_1 := Chars (Assignee_Level); + Error_Msg_NE ("\& has assertion level %", N, Assignee); + Error_Msg_Name_1 := Chars (Region_Level); + Error_Msg_NE + ("\& is modified within a region with %", N, Assignee); + Error_Msg_Name_1 := Chars (Region_Level); + Error_Msg_NE + ("\assertion level of & should depend on %", N, Assignee); + end if; + end Check_Assignment_Policies; + + -- Local variables + + Orig_Lhs : constant Node_Id := Name (N); + Id : Entity_Id; + Lhs : Node_Id; + + -- Start of processing for Mark_And_Set_Ghost_Assignment begin - -- Ghost assignments are irrelevant when the expander is inactive, and - -- processing them in that mode can lead to spurious errors. - - if not Expander_Active then - return; - end if; - -- Cases where full analysis is needed, involving array indexing -- which would otherwise be missing array-bounds checks: @@ -1919,6 +1894,11 @@ package body Ghost is end if; Id := Get_Enclosing_Ghost_Entity (Lhs); + + if Present (Id) and then Is_Ghost_Entity (Id) then + Check_Assignment_Policies (Id); + end if; + Mark_And_Set_Ghost_Region (N, Id); end Mark_And_Set_Ghost_Assignment;