From: Yannick Moy Date: Wed, 18 Sep 2019 08:32:28 +0000 (+0000) Subject: [Ada] Skip entity name qualification in GNATprove mode X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d05586dce2ea2ac3bc6f645b7ad79290b327ccae;p=gcc.git [Ada] Skip entity name qualification in GNATprove mode 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. 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. From-SVN: r275850 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index e77725c2c29..a6012fea00e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,16 @@ +2019-09-18 Yannick Moy + + * 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. + 2019-09-18 Nicolas Roche * libgnat/s-valrea.adb (Scan_Integral_Digits): New procedure. diff --git a/gcc/ada/exp_dbug.adb b/gcc/ada/exp_dbug.adb index 3dbe9ad7151..eb5e72b8ce7 100644 --- a/gcc/ada/exp_dbug.adb +++ b/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. diff --git a/gcc/ada/exp_dbug.ads b/gcc/ada/exp_dbug.ads index 93b978378f9..b9f1fd6e7eb 100644 --- a/gcc/ada/exp_dbug.ads +++ b/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 diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb index 2b3f377033c..1cc143a0012 100644 --- a/gcc/ada/frontend.adb +++ b/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. diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 99cdb8da0eb..f66c77f71ae 100644 --- a/gcc/ada/sem_util.adb +++ b/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)