From patchwork Thu Apr 27 10:15:16 2017 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 755944 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org 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 3wDCWs3nVKz9sNJ for ; Thu, 27 Apr 2017 20:15:52 +1000 (AEST) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="lUsq4CR+"; dkim-atps=neutral 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=cdc37AGnjDVWZt4qtLyqeAAaGBQZ/2YY3o7DhCmLkLmfi98cZa 6i83Kw+TwhpkR+KsyFBjkyD2IL+Bz3Tp/Iz68V5Dxo6gMi6UuJuNQ3ts/0755mJL 30ERbNV1+DBQVQJZ0rLhXqPTNbx5I1x44rhg5RntnUyvfaNUu5rFAFhk4= 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=Zaf9DHm5fzMsY3So3zblxrczy0E=; b=lUsq4CR+J9KXNf97KHXs 8DUI3OLXaDPNnAxB93NZI835dBxwiLxqPSvQSIV6LvRl1t3u2UYYgc2XJOuIJY1D OSjkcUlRgm9HdSFWAyMlsrX0XylWyHu2qfOc4psR8LC8EC3yr1+KYQmjeLaLjt6P +eDOz0S8ooR9RBwm0F+wGk4= Received: (qmail 50749 invoked by alias); 27 Apr 2017 10:15:31 -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 50618 invoked by uid 89); 27 Apr 2017 10:15:20 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-10.3 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=(unknown) X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Thu, 27 Apr 2017 10:15:18 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id E178D5A5B3; Thu, 27 Apr 2017 06:15:16 -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 q6UOGYkdpQDK; Thu, 27 Apr 2017 06:15:16 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id CE8B05A59F; Thu, 27 Apr 2017 06:15:16 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id CA52B4F9; Thu, 27 Apr 2017 06:15:16 -0400 (EDT) Date: Thu, 27 Apr 2017 06:15:16 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Fix side-effect removal for GNATprove Message-ID: <20170427101516.GA100543@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) GNATprove relies on side-effects being removed and value being fixed from renamings, which was not the case for the renaming of a qualified expression. Now done. Tested on x86_64-pc-linux-gnu, committed on trunk 2017-04-27 Yannick Moy * exp_util.ads, exp_util.adb (Evaluate_Name): Force evaluation of expression being qualified, when not an object name, or else evaluate the underlying name. Index: exp_util.adb =================================================================== --- exp_util.adb (revision 247293) +++ exp_util.adb (working copy) @@ -4724,72 +4724,85 @@ ------------------- procedure Evaluate_Name (Nam : Node_Id) is - K : constant Node_Kind := Nkind (Nam); - begin - -- For an explicit dereference, we simply force the evaluation of the - -- name expression. The dereference provides a value that is the address - -- for the renamed object, and it is precisely this value that we want - -- to preserve. + -- For an attribute reference or an indexed component, evaluate the + -- prefix, which is itself a name, recursively, and then force the + -- evaluation of all the subscripts (or attribute expressions). - if K = N_Explicit_Dereference then - Force_Evaluation (Prefix (Nam)); + case Nkind (Nam) is + when N_Attribute_Reference + | N_Indexed_Component + => + Evaluate_Name (Prefix (Nam)); - -- For a selected component, we simply evaluate the prefix + declare + E : Node_Id; - elsif K = N_Selected_Component then - Evaluate_Name (Prefix (Nam)); + begin + E := First (Expressions (Nam)); + while Present (E) loop + Force_Evaluation (E); - -- For an indexed component, or an attribute reference, we evaluate the - -- prefix, which is itself a name, recursively, and then force the - -- evaluation of all the subscripts (or attribute expressions). + if Original_Node (E) /= E then + Set_Do_Range_Check (E, + Do_Range_Check (Original_Node (E))); + end if; - elsif Nkind_In (K, N_Indexed_Component, N_Attribute_Reference) then - Evaluate_Name (Prefix (Nam)); + Next (E); + end loop; + end; - declare - E : Node_Id; + -- For an explicit dereference, we simply force the evaluation of + -- the name expression. The dereference provides a value that is the + -- address for the renamed object, and it is precisely this value + -- that we want to preserve. - begin - E := First (Expressions (Nam)); - while Present (E) loop - Force_Evaluation (E); + when N_Explicit_Dereference => + Force_Evaluation (Prefix (Nam)); - if Original_Node (E) /= E then - Set_Do_Range_Check (E, Do_Range_Check (Original_Node (E))); - end if; + -- For a function call, we evaluate the call - Next (E); - end loop; - end; + when N_Function_Call => + Force_Evaluation (Nam); - -- For a slice, we evaluate the prefix, as for the indexed component - -- case and then, if there is a range present, either directly or as the - -- constraint of a discrete subtype indication, we evaluate the two - -- bounds of this range. + -- For a qualified expression, we evaluate the underlying object + -- name if any, otherwise we force the evaluation of the underlying + -- expression. - elsif K = N_Slice then - Evaluate_Name (Prefix (Nam)); - Evaluate_Slice_Bounds (Nam); + when N_Qualified_Expression => + if Is_Object_Reference (Expression (Nam)) then + Evaluate_Name (Expression (Nam)); + else + Force_Evaluation (Expression (Nam)); + end if; - -- For a type conversion, the expression of the conversion must be the - -- name of an object, and we simply need to evaluate this name. + -- For a selected component, we simply evaluate the prefix - elsif K = N_Type_Conversion then - Evaluate_Name (Expression (Nam)); + when N_Selected_Component => + Evaluate_Name (Prefix (Nam)); - -- For a function call, we evaluate the call + -- For a slice, we evaluate the prefix, as for the indexed component + -- case and then, if there is a range present, either directly or as + -- the constraint of a discrete subtype indication, we evaluate the + -- two bounds of this range. - elsif K = N_Function_Call then - Force_Evaluation (Nam); + when N_Slice => + Evaluate_Name (Prefix (Nam)); + Evaluate_Slice_Bounds (Nam); - -- The remaining cases are direct name, operator symbol and character - -- literal. In all these cases, we do nothing, since we want to - -- reevaluate each time the renamed object is used. + -- For a type conversion, the expression of the conversion must be + -- the name of an object, and we simply need to evaluate this name. - else - return; - end if; + when N_Type_Conversion => + Evaluate_Name (Expression (Nam)); + + -- The remaining cases are direct name, operator symbol and character + -- literal. In all these cases, we do nothing, since we want to + -- reevaluate each time the renamed object is used. + + when others => + null; + end case; end Evaluate_Name; --------------------------- @@ -6933,7 +6946,7 @@ -- existing actions of the expression with actions, and should -- never reach here: if actions are inserted on a statement -- within the Actions of an expression with actions, or on some - -- sub-expression of such a statement, then the outermost proper + -- subexpression of such a statement, then the outermost proper -- insertion point is right before the statement, and we should -- never climb up as far as the N_Expression_With_Actions itself. Index: exp_util.ads =================================================================== --- exp_util.ads (revision 247293) +++ exp_util.ads (working copy) @@ -518,8 +518,11 @@ procedure Evaluate_Name (Nam : Node_Id); -- Remove all side effects from a name which appears as part of an object - -- renaming declaration. More comments are needed here that explain how - -- this differs from Force_Evaluation and Remove_Side_Effects ??? + -- renaming declaration. Similarly to Force_Evaluation, it removes the + -- side effects and captures the values of the variables, except for the + -- variable being renamed. Hence this differs from Force_Evaluation and + -- Remove_Side_Effects (but it calls Force_Evaluation on subexpressions + -- whose value needs to be fixed). procedure Evolve_And_Then (Cond : in out Node_Id; Cond1 : Node_Id); -- Rewrites Cond with the expression: Cond and then Cond1. If Cond is