From patchwork Fri Jul 10 09:44:20 2020 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: 1326608 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=2620:52:3:1:0:246e:9693:128c; helo=sourceware.org; envelope-from=gcc-patches-bounces@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=none (p=none dis=none) header.from=adacore.com Received: from sourceware.org (server2.sourceware.org [IPv6:2620:52:3:1:0:246e:9693:128c]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 4B37Rg4y5mz9sDX for ; Fri, 10 Jul 2020 19:44:31 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 935F938708D6; Fri, 10 Jul 2020 09:44:23 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from rock.gnat.com (rock.gnat.com [205.232.38.15]) by sourceware.org (Postfix) with ESMTP id 7444B385703A for ; Fri, 10 Jul 2020 09:44:20 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.3.2 sourceware.org 7444B385703A Authentication-Results: sourceware.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=derodat@adacore.com Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 3AF4D56120; Fri, 10 Jul 2020 05:44:20 -0400 (EDT) X-Virus-Scanned: Debian amavisd-new at gnat.com 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 7L0W1Mkt5p9E; Fri, 10 Jul 2020 05:44:20 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 27E7C5611F; Fri, 10 Jul 2020 05:44:20 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 27097A6; Fri, 10 Jul 2020 05:44:20 -0400 (EDT) Date: Fri, 10 Jul 2020 05:44:20 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Subject: [Ada] Fix failing assertions related to volatile objects Message-ID: <20200710094420.GA35290@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-Spam-Status: No, score=-8.0 required=5.0 tests=BAYES_00, GIT_PATCH_0, JMQ_SPF_NEUTRAL, KAM_DMARC_STATUS, SPF_HELO_NONE, SPF_PASS, TXREP, WEIRD_QUOTING autolearn=ham autolearn_force=no version=3.4.2 X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) 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: , Cc: Piotr Trojanek Errors-To: gcc-patches-bounces@gcc.gnu.org Sender: "Gcc-patches" Comments for routines No_Caching_Enabled and Is_Effectively_Volatile, which are both related to volatile objects, were not enforced with assertions. As a result, we had failing assertions much deeper in the call tree, far from where the problems occur. This patch adds both the missing assertions and guards to prevent those assertions from failing. In preparation for a main commit that will address a problem related to freezing of Dynamic_Predicate aspect on volatile objects. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch3.adb (Process_Discriminants): Set Ekind of the processed discriminant entity before passing to Is_Effectively_Volatile, which was crashing on a failed assertion. * sem_prag.adb (Analyze_External_Property_In_Decl_Part): Prevent call to No_Caching_Enabled with entities other than variables, which was crashing on a failed assertion. (Analyze_Pragma): Style cleanups. * sem_util.adb (Is_Effectively_Volatile): Enforce comment with an assertion; prevent call to No_Caching_Enabled with entities other than variables. (Is_Effectively_Volatile_Object): Only call Is_Effectively_Volatile on objects, not on types. (No_Caching_Enabled): Enforce comment with an assertion. diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -19977,6 +19977,7 @@ package body Sem_Ch3 is end if; Set_Etype (Defining_Identifier (Discr), Discr_Type); + Set_Ekind (Defining_Identifier (Discr), E_Discriminant); -- If a discriminant specification includes the assignment compound -- delimiter followed by an expression, the expression is the default @@ -20035,7 +20036,7 @@ package body Sem_Ch3 is (Defining_Identifier (Discr), Expression (Discr)); end if; - -- In gnatc or gnatprove mode, make sure set Do_Range_Check flag + -- In gnatc or GNATprove mode, make sure set Do_Range_Check flag -- gets set unless we can be sure that no range check is required. if not Expander_Active @@ -20175,7 +20176,6 @@ package body Sem_Ch3 is Discr_Number := Uint_1; while Present (Discr) loop Id := Defining_Identifier (Discr); - Set_Ekind (Id, E_Discriminant); Init_Component_Location (Id); Init_Esize (Id); Set_Discriminant_Number (Id, Discr_Number); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2122,7 +2122,9 @@ package body Sem_Prag is if Prag_Id /= Pragma_No_Caching and then not Is_Effectively_Volatile (Obj_Id) then - if No_Caching_Enabled (Obj_Id) then + if Ekind (Obj_Id) = E_Variable + and then No_Caching_Enabled (Obj_Id) + then SPARK_Msg_N ("illegal combination of external property % and property " & """No_Caching"" (SPARK RM 7.1.2(6))", N); @@ -13363,7 +13365,7 @@ package body Sem_Prag is -- respective root types. if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration then - if (Prag_Id = Pragma_No_Caching) + if Prag_Id = Pragma_No_Caching or not Nkind_In (Original_Node (Obj_Or_Type_Decl), N_Full_Type_Declaration, N_Private_Type_Declaration, @@ -13383,7 +13385,8 @@ package body Sem_Prag is -- will be done at the end of the declarative region that -- contains the pragma. - if Ekind (Obj_Or_Type_Id) = E_Variable or Is_Type (Obj_Or_Type_Id) + if Ekind (Obj_Or_Type_Id) = E_Variable + or else Is_Type (Obj_Or_Type_Id) then -- In the case of a type, pragma is a type-related diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -15651,12 +15651,14 @@ package body Sem_Util is -- Otherwise Id denotes an object - else + else pragma Assert (Is_Object (Id)); -- A volatile object for which No_Caching is enabled is not -- effectively volatile. return - (Is_Volatile (Id) and then not No_Caching_Enabled (Id)) + (Is_Volatile (Id) + and then not + (Ekind (Id) = E_Variable and then No_Caching_Enabled (Id))) or else Has_Volatile_Components (Id) or else Is_Effectively_Volatile (Etype (Id)); end if; @@ -15669,7 +15671,8 @@ package body Sem_Util is function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean is begin if Is_Entity_Name (N) then - return Is_Effectively_Volatile (Entity (N)); + return Is_Object (Entity (N)) + and then Is_Effectively_Volatile (Entity (N)); elsif Nkind (N) = N_Indexed_Component then return Is_Effectively_Volatile_Object (Prefix (N)); @@ -23289,6 +23292,7 @@ package body Sem_Util is ------------------------ function No_Caching_Enabled (Id : Entity_Id) return Boolean is + pragma Assert (Ekind (Id) = E_Variable); Prag : constant Node_Id := Get_Pragma (Id, Pragma_No_Caching); Arg1 : Node_Id;