From patchwork Thu Jul 11 08:03:47 2019 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: 1130692 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-504897-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="KWYi/M/E"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 45kpYX2PGxz9sNF for ; Thu, 11 Jul 2019 18:06:56 +1000 (AEST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=oecVfUNUlWK0xQ+YZKQ1TN1xFdSE8Xp9n3sgqPVIMbl94dwvSZ 07bCfML1d1sRh0mu/21d74LkvInCEJe9jocx4COZjN4h+v2ZfqvY1vrac1AffbjH GJ6XQilvNs7mfHDUI++h14V6V2aGYeUMxNqSJZh1ICun/j1/Nanx0gKEY= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=f7cAcCIt9P9tXDO8wETumPHXzcA=; b=KWYi/M/EncFjTfLl2Aic HYiRvTZcqOYTQBV7vI4FiTV2sRjaWc1KwnAs3ToHVYAcfWYfkoiES828nOxkSORq E7TDT2vCqrfQDI7yhjQBN79dDZ+kBV5L1oDNf32W4CKbcknDh1ecZ8BGFs7Mdbul e8fWSwtkGngrZvIw6vpUcwA= Received: (qmail 89175 invoked by alias); 11 Jul 2019 08:04:06 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 88001 invoked by uid 89); 11 Jul 2019 08:03:54 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-10.0 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, SPF_NEUTRAL autolearn=ham version=3.3.1 spammy= X-HELO: eggs.gnu.org Received: from eggs.gnu.org (HELO eggs.gnu.org) (209.51.188.92) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Thu, 11 Jul 2019 08:03:52 +0000 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hlU3Q-0007vr-Lz for gcc-patches@gcc.gnu.org; Thu, 11 Jul 2019 04:03:50 -0400 Received: from rock.gnat.com ([2620:20:4000:0:a9e:1ff:fe9b:1d1]:48505) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1hlU3Q-0007um-Fl for gcc-patches@gcc.gnu.org; Thu, 11 Jul 2019 04:03:48 -0400 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id B9D8F561FF; Thu, 11 Jul 2019 04:03:47 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id P0E8fNhbyDIG; Thu, 11 Jul 2019 04:03:47 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id A83DB56019; Thu, 11 Jul 2019 04:03:47 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id A6E156F7; Thu, 11 Jul 2019 04:03:47 -0400 (EDT) Date: Thu, 11 Jul 2019 04:03:47 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Avoid spurious warning on assertions with Loop_Entry Message-ID: <20190711080347.GA95281@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x X-Received-From: 2620:20:4000:0:a9e:1ff:fe9b:1d1 X-IsSubscribed: yes When the Loop_Entry attribute is used inside a loop invariant or another assertion where it is allowed, it may lead to spurious warnings on conditions that are detected to be always valid. Now fixed. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-07-11 Yannick Moy gcc/ada/ * sem_eval.adb (Is_Same_Value): Add special case for rewritten Loop_Entry attribute. gcc/testsuite/ * gnat.dg/loop_entry1.adb: New testcase. --- gcc/ada/sem_eval.adb +++ gcc/ada/sem_eval.adb @@ -986,6 +986,13 @@ package body Sem_Eval is Lf : constant Node_Id := Compare_Fixup (L); Rf : constant Node_Id := Compare_Fixup (R); + function Is_Rewritten_Loop_Entry (N : Node_Id) return Boolean; + -- An attribute reference to Loop_Entry may have been rewritten into + -- its prefix as a way to avoid generating a constant for that + -- attribute when the corresponding pragma is ignored. These nodes + -- should be ignored when deciding if they can be equal to one + -- another. + function Is_Same_Subscript (L, R : List_Id) return Boolean; -- L, R are the Expressions values from two attribute nodes for First -- or Last attributes. Either may be set to No_List if no expressions @@ -993,6 +1000,19 @@ package body Sem_Eval is -- expressions represent the same subscript (note one case is where -- one subscript is missing and the other is explicitly set to 1). + ----------------------------- + -- Is_Rewritten_Loop_Entry -- + ----------------------------- + + function Is_Rewritten_Loop_Entry (N : Node_Id) return Boolean is + Orig_N : constant Node_Id := Original_Node (N); + begin + return Orig_N /= N + and then Nkind (Orig_N) = N_Attribute_Reference + and then Get_Attribute_Id (Attribute_Name (Orig_N)) = + Attribute_Loop_Entry; + end Is_Rewritten_Loop_Entry; + ----------------------- -- Is_Same_Subscript -- ----------------------- @@ -1018,23 +1038,32 @@ package body Sem_Eval is -- Start of processing for Is_Same_Value begin - -- Values are the same if they refer to the same entity and the - -- entity is non-volatile. This does not however apply to Float - -- types, since we may have two NaN values and they should never - -- compare equal. + -- Loop_Entry nodes rewritten into their prefix inside ignored + -- pragmas should never lead to a decision of equality. - -- If the entity is a discriminant, the two expressions may be bounds - -- of components of objects of the same discriminated type. The - -- values of the discriminants are not static, and therefore the - -- result is unknown. + if Is_Rewritten_Loop_Entry (Lf) + or else Is_Rewritten_Loop_Entry (Rf) + then + return False; - -- It would be better to comment individual branches of this test ??? + -- Values are the same if they refer to the same entity and the + -- entity is nonvolatile. - if Nkind_In (Lf, N_Identifier, N_Expanded_Name) + elsif Nkind_In (Lf, N_Identifier, N_Expanded_Name) and then Nkind_In (Rf, N_Identifier, N_Expanded_Name) and then Entity (Lf) = Entity (Rf) + + -- If the entity is a discriminant, the two expressions may be + -- bounds of components of objects of the same discriminated type. + -- The values of the discriminants are not static, and therefore + -- the result is unknown. + and then Ekind (Entity (Lf)) /= E_Discriminant and then Present (Entity (Lf)) + + -- This does not however apply to Float types, since we may have + -- two NaN values and they should never compare equal. + and then not Is_Floating_Point_Type (Etype (L)) and then not Is_Volatile_Reference (L) and then not Is_Volatile_Reference (R) --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/loop_entry1.adb @@ -0,0 +1,13 @@ +-- { dg-do compile } +-- { dg-options "-gnatwc" } + +procedure Loop_Entry1 (X, Y : in out Integer) is +begin + while X < Y loop + pragma Loop_Invariant + (X >= X'Loop_Entry and then Y <= Y'Loop_Entry); + + X := X + 1; + Y := Y - 1; + end loop; +end Loop_Entry1;