diff mbox series

[Ada] Store SPARK cross-references as Entity_Ids, not strings

Message ID 20171108160600.GA6943@adacore.com
State New
Headers show
Series [Ada] Store SPARK cross-references as Entity_Ids, not strings | expand

Commit Message

Pierre-Marie de Rodat Nov. 8, 2017, 4:06 p.m. UTC 
GNATprove now picks frontend cross-references directly from memory and
not from an ALI file), so there is no need to convert them to strings;
it is cleaner and more efficient to store them as Entity_Ids. No test
provided, because the behaviour is not affected.

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-11-08  Piotr Trojanek  <trojanek@adacore.com>

	* spark_xrefs.ads (SPARK_Xref_Record): Referenced object is now
	represented by Entity_Id.
	(SPARK_Scope_Record): Referenced scope (e.g. subprogram) is now
	represented by Entity_Id; this information is not repeated as
	Scope_Entity.
	(Heap): Moved from lib-xref-spark_specific.adb, to reside next to
	Name_Of_Heap_Variable.
	* spark_xrefs.adb (dspark): Adapt debug routine to above changes in
	data types.
	* lib-xref-spark_specific.adb: Adapt routines for populating SPARK
	scope and xrefs tables to above changes in data types.
diff mbox series

Patch

Index: lib-xref-spark_specific.adb
===================================================================
--- lib-xref-spark_specific.adb	(revision 254538)
+++ lib-xref-spark_specific.adb	(working copy)
@@ -66,9 +66,6 @@ 
    -- Local Variables --
    ---------------------
 
-   Heap : Entity_Id := Empty;
-   --  A special entity which denotes the heap object
-
    package Drefs is new Table.Table (
      Table_Component_Type => Xref_Entry,
      Table_Index_Type     => Xref_Entry_Number,
@@ -164,14 +161,13 @@ 
          --  range.
 
          SPARK_Scope_Table.Append
-           ((Scope_Name     => new String'(Unique_Name (E)),
+           ((Scope_Id       => E,
              File_Num       => Dspec,
              Scope_Num      => Scope_Id,
              Spec_File_Num  => 0,
              Spec_Scope_Num => 0,
              From_Xref      => 1,
-             To_Xref        => 0,
-             Scope_Entity   => E));
+             To_Xref        => 0));
 
          Scope_Id := Scope_Id + 1;
       end Add_SPARK_Scope;
@@ -351,7 +347,7 @@ 
 
       function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
       begin
-         return SPARK_Scope_Table.Table (S).Scope_Entity;
+         return SPARK_Scope_Table.Table (S).Scope_Id;
       end Entity_Of_Scope;
 
       -------------------
@@ -423,7 +419,7 @@ 
          function Is_Past_Scope_Entity return Boolean is
          begin
             for Index in SPARK_Scope_Table.First .. S - 1 loop
-               if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
+               if SPARK_Scope_Table.Table (Index).Scope_Id = E then
                   return True;
                end if;
             end loop;
@@ -435,7 +431,7 @@ 
 
       begin
          for Index in S .. SPARK_Scope_Table.Last loop
-            if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
+            if SPARK_Scope_Table.Table (Index).Scope_Id = E then
                return True;
             end if;
          end loop;
@@ -634,7 +630,7 @@ 
          declare
             S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
          begin
-            Set_Scope_Num (S.Scope_Entity, S.Scope_Num);
+            Set_Scope_Num (S.Scope_Id, S.Scope_Num);
          end;
       end loop;
 
@@ -800,10 +796,10 @@ 
             end if;
 
             SPARK_Xref_Table.Append (
-              (Entity_Name => new String'(Unique_Name (Ref.Ent)),
-               File_Num    => Dependency_Num (Ref.Lun),
-               Scope_Num   => Get_Scope_Num (Ref.Ref_Scope),
-               Rtype       => Typ));
+              (Entity    => Unique_Entity (Ref.Ent),
+               File_Num  => Dependency_Num (Ref.Lun),
+               Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
+               Rtype     => Typ));
          end;
       end loop;
 
@@ -948,7 +944,7 @@ 
             declare
                Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
             begin
-               Entity_Hash_Table.Set (Srec.Scope_Entity, S);
+               Entity_Hash_Table.Set (Srec.Scope_Id, S);
             end;
          end loop;
 
@@ -959,14 +955,14 @@ 
                Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
 
                Spec_Entity : constant Entity_Id :=
-                               Unique_Entity (Srec.Scope_Entity);
+                               Unique_Entity (Srec.Scope_Id);
                Spec_Scope  : constant Scope_Index :=
                                Entity_Hash_Table.Get (Spec_Entity);
 
             begin
                --  Generic spec may be missing in which case Spec_Scope is zero
 
-               if Spec_Entity /= Srec.Scope_Entity
+               if Spec_Entity /= Srec.Scope_Id
                  and then Spec_Scope /= 0
                then
                   Srec.Spec_File_Num :=
Index: spark_xrefs.adb
===================================================================
--- spark_xrefs.adb	(revision 254538)
+++ spark_xrefs.adb	(working copy)
@@ -23,7 +23,8 @@ 
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Output; use Output;
+with Output;   use Output;
+with Sem_Util; use Sem_Util;
 
 package body SPARK_Xrefs is
 
@@ -81,17 +82,13 @@ 
             Write_Int (Int (ASR.Scope_Num));
             Write_Str ("  Scope_Name = """);
 
-            if ASR.Scope_Name /= null then
-               Write_Str (ASR.Scope_Name.all);
-            end if;
+            Write_Str (Unique_Name (ASR.Scope_Id));
 
             Write_Char ('"');
             Write_Str  ("  From = ");
             Write_Int  (Int (ASR.From_Xref));
             Write_Str  ("  To = ");
             Write_Int  (Int (ASR.To_Xref));
-            Write_Str  ("  Scope_Entity = ");
-            Write_Int  (Int (ASR.Scope_Entity));
             Write_Eol;
          end;
       end loop;
@@ -111,9 +108,7 @@ 
             Write_Int  (Int (Index));
             Write_Str (".  Entity_Name = """);
 
-            if AXR.Entity_Name /= null then
-               Write_Str (AXR.Entity_Name.all);
-            end if;
+            Write_Str (Unique_Name (AXR.Entity));
 
             Write_Char ('"');
             Write_Str ("  File_Num = ");
Index: spark_xrefs.ads
===================================================================
--- spark_xrefs.ads	(revision 254538)
+++ spark_xrefs.ads	(working copy)
@@ -66,7 +66,7 @@ 
    --  until a proper value is determined.
 
    type SPARK_Xref_Record is record
-      Entity_Name : String_Ptr;
+      Entity : Entity_Id;
       --  Pointer to entity name in ALI file
 
       File_Num : Nat;
@@ -109,7 +109,7 @@ 
    --  determined.
 
    type SPARK_Scope_Record is record
-      Scope_Name : String_Ptr;
+      Scope_Id : Entity_Id;
       --  Pointer to scope name in ALI file
 
       File_Num : Nat;
@@ -131,12 +131,6 @@ 
 
       To_Xref : Xref_Index;
       --  Ending index in Xref table for this scope
-
-      --  The following component is only used in-memory, not printed out in
-      --  ALI file.
-
-      Scope_Entity : Entity_Id := Empty;
-      --  Entity (subprogram or package) for the scope
    end record;
 
    package SPARK_Scope_Table is new Table.Table (
@@ -193,6 +187,11 @@ 
    --  Name of special variable used in effects to denote reads and writes
    --  through explicit dereference.
 
+   Heap : Entity_Id := Empty;
+   --  A special entity which denotes the heap object; it should be considered
+   --  constant, but needs to be variable, because it can only be initialized
+   --  after the node tables are created.
+
    -----------------
    -- Subprograms --
    -----------------