* [Ada] Skip entity name qualification in GNATprove mode
@ 2019-09-18 8:41 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2019-09-18 8:41 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 1019 bytes --]
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 <moy@adacore.com>
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.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 7239 bytes --]
--- 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)
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2019-09-18 8:41 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-09-18 8:41 [Ada] Skip entity name qualification in GNATprove mode Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).