From patchwork Wed Sep 18 08:39:44 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: 1163849 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-509188-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="E4ojlPQy"; 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 46YD7S6Bc9z9s4Y for ; Wed, 18 Sep 2019 18:44:52 +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=HkESvE516BIqbpgzZT8MT4Is2OUKbB51ILvBPQeLk6GX95uUmp P2BskWUt9jfLJBeoGgRS45HzVctC/KJjyYJ7j1IKutm8HHsU8ZaVhSklGhB2mJoC A31MYpS22n8TcMkL0Ip2jTPl5V3CEKLkZ0NVeAsDbUfovgNY+xiTxucJ8= 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=JG9w+U8m8n++nGY2JsGDxTZZ/5M=; b=E4ojlPQySSRKwim7ZH9y 9I3BKwI9lBP0RNO1PHYgwbOO299pFlZq813h/PV8qJqpPVQn1k8vD320PSp6fi3p 7QLP009Wl345EmTjVr7W0wRHtm9iK84a/Jdpi07Y3Vu5FwjaUH0ZncTE+0j+CtmB v8MugxLHmkJxDZRLi6EoHoA= Received: (qmail 110945 invoked by alias); 18 Sep 2019 08:41:16 -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 110877 invoked by uid 89); 18 Sep 2019 08:41:15 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-10.4 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=yannick, qualify, identifying, moy 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; Wed, 18 Sep 2019 08:41:13 +0000 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iAVVC-0008I4-5m for gcc-patches@gcc.gnu.org; Wed, 18 Sep 2019 04:39:55 -0400 Received: from rock.gnat.com ([205.232.38.15]:43761) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1iAVVA-0008EU-A4 for gcc-patches@gcc.gnu.org; Wed, 18 Sep 2019 04:39:53 -0400 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 1B063117CF0; Wed, 18 Sep 2019 04:39:45 -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 9bro1kXHra+F; Wed, 18 Sep 2019 04:39:45 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id F3D34117C70; Wed, 18 Sep 2019 04:39:44 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id F2B9C702; Wed, 18 Sep 2019 04:39:44 -0400 (EDT) Date: Wed, 18 Sep 2019 04:39:44 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Skip entity name qualification in GNATprove mode Message-ID: <20190918083944.GA145116@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: 205.232.38.15 X-IsSubscribed: yes GNATprove was using the qualification of names for entities with local homonyms in the same scope, requiring the use of a suffix to differentiate them. This caused problems for correctly identifying primitive equality operators. This case is now handled like the rest of entities in GNATprove, by instead updating Unique_Name to append the suffix on-the-fly where needed. There is no impact on compilation and hence no test. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-09-18 Yannick Moy gcc/ada/ * exp_dbug.adb (Append_Homonym_Number): Use new function Get_Homonym_Number. (Get_Homonym_Number): New function to return the homonym number. (Qualify_Entity_Name): Remove special case for GNATprove. * exp_dbug.ads (Get_Homonym_Number): Make the new function public for use in GNATprove. * frontend.adb (Frontend): Do not qualify names in GNATprove mode. * sem_util.adb (Unique_Name): Append homonym suffix where needed for entities which have local homonyms in the same scope. --- gcc/ada/exp_dbug.adb +++ gcc/ada/exp_dbug.adb @@ -219,26 +219,12 @@ package body Exp_Dbug is begin if Has_Homonym (E) then - declare - H : Entity_Id := Homonym (E); - Nr : Nat := 1; - - begin - while Present (H) loop - if Scope (H) = Scope (E) then - Nr := Nr + 1; - end if; - - H := Homonym (H); - end loop; - - if Homonym_Len > 0 then - Homonym_Len := Homonym_Len + 1; - Homonym_Numbers (Homonym_Len) := '_'; - end if; + if Homonym_Len > 0 then + Homonym_Len := Homonym_Len + 1; + Homonym_Numbers (Homonym_Len) := '_'; + end if; - Add_Nat_To_H (Nr); - end; + Add_Nat_To_H (Get_Homonym_Number (E)); end if; end Append_Homonym_Number; @@ -1068,6 +1054,26 @@ package body Exp_Dbug is end loop; end Build_Subprogram_Instance_Renamings; + ------------------------ + -- Get_Homonym_Number -- + ------------------------ + + function Get_Homonym_Number (E : Entity_Id) return Nat is + H : Entity_Id := Homonym (E); + Nr : Nat := 1; + + begin + while Present (H) loop + if Scope (H) = Scope (E) then + Nr := Nr + 1; + end if; + + H := Homonym (H); + end loop; + + return Nr; + end Get_Homonym_Number; + ------------------------------------ -- Get_Secondary_DT_External_Name -- ------------------------------------ @@ -1451,25 +1457,6 @@ package body Exp_Dbug is if Has_Qualified_Name (Ent) then return; - -- In formal verification mode, simply append a suffix for homonyms. - -- We used to qualify entity names as full expansion does, but this was - -- removed as this prevents the verification back-end from using a short - -- name for debugging and user interaction. The verification back-end - -- already takes care of qualifying names when needed. Still mark the - -- name as being qualified, as Qualify_Entity_Name may be called more - -- than once on the same entity. - - elsif GNATprove_Mode then - if Has_Homonym (Ent) then - Get_Name_String (Chars (Ent)); - Append_Homonym_Number (Ent); - Output_Homonym_Numbers_Suffix; - Set_Chars (Ent, Name_Enter); - end if; - - Set_Has_Qualified_Name (Ent); - return; - -- If the entity is a variable encoding the debug name for an object -- renaming, then the qualified name of the entity associated with the -- renamed object can now be incorporated in the debug name. --- gcc/ada/exp_dbug.ads +++ gcc/ada/exp_dbug.ads @@ -460,6 +460,10 @@ package Exp_Dbug is -- Subprograms for Handling Qualification -- -------------------------------------------- + function Get_Homonym_Number (E : Entity_Id) return Nat; + -- Return the homonym number for E, which is its position in the homonym + -- chain starting at 1. This is exported for use in GNATprove. + procedure Qualify_Entity_Names (N : Node_Id); -- Given a node N, that represents a block, subprogram body, or package -- body or spec, or protected or task type, sets a fully qualified name --- gcc/ada/frontend.adb +++ gcc/ada/frontend.adb @@ -492,7 +492,9 @@ begin -- Qualify all entity names in inner packages, package bodies, etc - Exp_Dbug.Qualify_All_Entity_Names; + if not GNATprove_Mode then + Exp_Dbug.Qualify_All_Entity_Names; + end if; -- SCIL backend requirement. Check that SCIL nodes associated with -- dispatching calls reference subprogram calls. --- gcc/ada/sem_util.adb +++ gcc/ada/sem_util.adb @@ -33,6 +33,7 @@ with Elists; use Elists; with Errout; use Errout; with Erroutc; use Erroutc; with Exp_Ch11; use Exp_Ch11; +with Exp_Dbug; use Exp_Dbug; with Exp_Util; use Exp_Util; with Fname; use Fname; with Freeze; use Freeze; @@ -26154,24 +26155,59 @@ package body Sem_Util is function Unique_Name (E : Entity_Id) return String is - -- Names in E_Subprogram_Body or E_Package_Body entities are not - -- reliable, as they may not include the overloading suffix. Instead, - -- when looking for the name of E or one of its enclosing scope, we get - -- the name of the corresponding Unique_Entity. + -- Local subprograms - U : constant Entity_Id := Unique_Entity (E); + function Add_Homonym_Suffix (E : Entity_Id) return String; function This_Name return String; + ------------------------ + -- Add_Homonym_Suffix -- + ------------------------ + + function Add_Homonym_Suffix (E : Entity_Id) return String is + + -- Names in E_Subprogram_Body or E_Package_Body entities are not + -- reliable, as they may not include the overloading suffix. + -- Instead, when looking for the name of E or one of its enclosing + -- scope, we get the name of the corresponding Unique_Entity. + + U : constant Entity_Id := Unique_Entity (E); + Nam : constant String := Get_Name_String (Chars (U)); + + begin + -- If E has homonyms but is not fully qualified, as done in + -- GNATprove mode, append the homonym number on the fly. Strip the + -- leading space character in the image of natural numbers. Also do + -- not print the homonym value of 1. + + if Has_Homonym (U) then + declare + N : constant Nat := Get_Homonym_Number (U); + S : constant String := N'Img; + begin + if N > 1 then + return Nam & "__" & S (2 .. S'Last); + end if; + end; + end if; + + return Nam; + end Add_Homonym_Suffix; + --------------- -- This_Name -- --------------- function This_Name return String is begin - return Get_Name_String (Chars (U)); + return Add_Homonym_Suffix (E); end This_Name; + -- Local variables + + U : constant Entity_Id := Unique_Entity (E); + -- Start of processing for Unique_Name begin @@ -26201,16 +26237,17 @@ package body Sem_Util is end if; -- For intances of generic subprograms use the name of the related - -- instace and skip the scope of its wrapper package. + -- instance and skip the scope of its wrapper package. elsif Is_Wrapper_Package (S) then pragma Assert (Scope (S) = Scope (Related_Instance (S))); -- Wrapper package and the instantiation are in the same scope declare + Related_Name : constant String := + Add_Homonym_Suffix (Related_Instance (S)); Enclosing_Name : constant String := - Unique_Name (Scope (S)) & "__" & - Get_Name_String (Chars (Related_Instance (S))); + Unique_Name (Scope (S)) & "__" & Related_Name; begin if Is_Subprogram (U)