From patchwork Wed Oct 20 19:27:26 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 46449 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 D9DAD3858426 for ; Wed, 20 Oct 2021 19:28:52 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org D9DAD3858426 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1634758132; bh=52tpfij+eWg3rbSzMon3RI3+jciZrBKQ10rX0geBBfk=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=ur1bD1MmEm/AOQmVAIj/fLFFWO58UUFjLC98gDM0XPKiJ4JkR1qWkOorAspWoRXE5 kt4PnPSO20X2RPmI1nzYnPojSk9Mbfv68UYrKuEQHZzeW9B0//NVemDwu98COxmdr9 9GwOfPgpOtuj2SEcoX0CyTUteXIIqOmsVRSDTA1s= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-lf1-x135.google.com (mail-lf1-x135.google.com [IPv6:2a00:1450:4864:20::135]) by sourceware.org (Postfix) with ESMTPS id E4B813857C58 for ; Wed, 20 Oct 2021 19:27:30 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org E4B813857C58 Received: by mail-lf1-x135.google.com with SMTP id i6so332536lfv.9 for ; Wed, 20 Oct 2021 12:27:30 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=52tpfij+eWg3rbSzMon3RI3+jciZrBKQ10rX0geBBfk=; b=7PvCKEAsIf6qv3XHKcssJrDJJmHyqYYT21lqY4PXT5fyoX0FhPZLgN3Cy76rcfZgI5 Krw/IUvhMLmK9zZsJ/zq3AHe14P/vmqmIUkJUEF/xCdEnw8vSJOqnIS/cJhIZ3WTrkeD BEcS7mOMBcvRfHDm35RZy7iCnEjZfCeNhROXE5aeINGQqry+FjIjUV/tFhvMmckgnKM5 LsnIYbpLYWqhsPZrFMeJVcl7wA47nGdN7Ze90941iR7MjC1nyf29y8QmtItWXajP8DhN /8AuMqR1mpRospOHVmmeC+bc0gQgUVcHxB9tEOOy0g0mJqM2djHjUbN//iQzwvgsj3Ps 6ftA== X-Gm-Message-State: AOAM532R3rI4T7xjHiEEhEXrotvcPprGj8I08oymV3vUsVw0zI3ElWQS 4U9oVlaSb96SCewHI6Hq3KY2EPWDNe6fnw== X-Google-Smtp-Source: ABdhPJzQ5YlyrJu3zZzZ0FvoNjkTIRIrzdqazAYfzbbywCT68M1Fq5btJ3IqASWj7/OYDokgmQkx2w== X-Received: by 2002:ac2:5e90:: with SMTP id b16mr1093106lfq.361.1634758049797; Wed, 20 Oct 2021 12:27:29 -0700 (PDT) Received: from adacore.com ([2a02:2ab8:224:2ce:72b5:e8ff:feef:ee60]) by smtp.gmail.com with ESMTPSA id 195sm313209ljf.13.2021.10.20.12.27.28 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 20 Oct 2021 12:27:28 -0700 (PDT) Date: Wed, 20 Oct 2021 19:27:26 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Issue warning on unused quantified expression Message-ID: <20211020192726.GA3154065@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-13.0 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) 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: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Yannick Moy Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" It is common that a quantified expression takes the form of a conjunction or disjunction. In such a case, it is expected that all conjuncts/ disjuncts reference the quantified variable. Not doing so can be either the symptom of an error, or of a non-optimal expression, as that sub-expression could be extracted from the quantified expression. This is beneficial for both execution (speed) and for proof (automation). Issue a warning in such a case. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch4.adb (Analyze_QUantified_Expression): Issue warning on conjunct/disjunct sub-expression of the full expression inside a quantified expression, when it does not reference the quantified variable. diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -4299,21 +4299,67 @@ package body Sem_Ch4 is Loop_Id := Defining_Identifier (Loop_Parameter_Specification (N)); end if; - if Warn_On_Suspicious_Contract - and then not Referenced (Loop_Id, Cond) - and then not Is_Internal_Name (Chars (Loop_Id)) - then - -- Generating C, this check causes spurious warnings on inlined - -- postconditions; we can safely disable it because this check - -- was previously performed when analyzing the internally built - -- postconditions procedure. + declare + type Subexpr_Kind is (Full, Conjunct, Disjunct); - if Modify_Tree_For_C and then In_Inlined_Body then - null; - else - Error_Msg_N ("?T?unused variable &", Loop_Id); + procedure Check_Subexpr (Expr : Node_Id; Kind : Subexpr_Kind); + -- Check that the quantified variable appears in every sub-expression + -- of the quantified expression. If Kind is Full, Expr is the full + -- expression. If Kind is Conjunct (resp. Disjunct), Expr is a + -- conjunct (resp. disjunct) of the full expression. + + ------------------- + -- Check_Subexpr -- + ------------------- + + procedure Check_Subexpr (Expr : Node_Id; Kind : Subexpr_Kind) is + begin + if Nkind (Expr) in N_Op_And | N_And_Then + and then Kind /= Disjunct + then + Check_Subexpr (Left_Opnd (Expr), Conjunct); + Check_Subexpr (Right_Opnd (Expr), Conjunct); + + elsif Nkind (Expr) in N_Op_Or | N_Or_Else + and then Kind /= Conjunct + then + Check_Subexpr (Left_Opnd (Expr), Disjunct); + Check_Subexpr (Right_Opnd (Expr), Disjunct); + + elsif Kind /= Full + and then not Referenced (Loop_Id, Expr) + then + declare + Sub : constant String := + (if Kind = Conjunct then "conjunct" else "disjunct"); + begin + Error_Msg_NE + ("?T?unused variable & in " & Sub, Expr, Loop_Id); + Error_Msg_NE + ("\consider extracting " & Sub & " from quantified " + & "expression", Expr, Loop_Id); + end; + end if; + end Check_Subexpr; + + begin + if Warn_On_Suspicious_Contract + and then not Is_Internal_Name (Chars (Loop_Id)) + + -- Generating C, this check causes spurious warnings on inlined + -- postconditions; we can safely disable it because this check + -- was previously performed when analyzing the internally built + -- postconditions procedure. + + and then not (Modify_Tree_For_C and In_Inlined_Body) + then + if not Referenced (Loop_Id, Cond) then + Error_Msg_N ("?T?unused variable &", Loop_Id); + else + Check_Subexpr (Cond, Kind => Full); + end if; end if; - end if; + end; -- Diagnose a possible misuse of the SOME existential quantifier. When -- we have a quantified expression of the form: