[Ada] Skip entity name qualification in GNATprove mode
diff mbox series

Message ID 20190918083944.GA145116@adacore.com
State New
Headers show
Series
  • [Ada] Skip entity name qualification in GNATprove mode
Related show

Commit Message

Pierre-Marie de Rodat Sept. 18, 2019, 8:39 a.m. UTC
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.

Patch
diff mbox series

--- 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)