diff mbox

[Ada] Fix handling of separate units in GNATprove cross references

Message ID 20160614121248.GA130270@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet June 14, 2016, 12:12 p.m. UTC 
The collect of cross references for computing effects of subprograms
in GNATprove was done incorrectly in the case of separate units. This is
now fixed, by bypassing subunits when computing the unit of interest for
both scopes and cross references.

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

2016-06-14  Yannick Moy  <moy@adacore.com>

	* lib-xref-spark_specific.adb (Add_SPARK_File): Do not traverse
	subunits directly, as they are already traversed as part of the
	top-level unit to which they belong.
	(Add_SPARK_Xrefs): Add assertions to ensure correct sorting.
	(Generate_Dereference): Use unique definition place for special
	variable __HEAP, to ensure correct sorting of references.
	* lib-xref.adb (Generate_Reference): Use top-level unit in case
	of subunits.
	* lib.adb, lib.ads (Get_Top_Level_Code_Unit): New functions that
	compute the top-level code unit for a source location of AST node,
	that go past subunits.
diff mbox

Patch

Index: lib.adb
===================================================================
--- lib.adb	(revision 237429)
+++ lib.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -68,9 +68,12 @@ 
 
    function Get_Code_Or_Source_Unit
      (S                : Source_Ptr;
-      Unwind_Instances : Boolean) return Unit_Number_Type;
-   --  Common code for Get_Code_Unit (get unit of instantiation for location)
-   --  and Get_Source_Unit (get unit of template for location).
+      Unwind_Instances : Boolean;
+      Unwind_Subunits  : Boolean) return Unit_Number_Type;
+   --  Common code for Get_Code_Unit (get unit of instantiation for
+   --  location) Get_Source_Unit (get unit of template for location) and
+   --  Get_Top_Level_Code_Unit (same as Get_Code_Unit but not stopping at
+   --  subunits).
 
    --------------------------------------------
    -- Access Functions for Unit Table Fields --
@@ -573,7 +576,8 @@ 
 
    function Get_Code_Or_Source_Unit
      (S                : Source_Ptr;
-      Unwind_Instances : Boolean) return Unit_Number_Type
+      Unwind_Instances : Boolean;
+      Unwind_Subunits  : Boolean) return Unit_Number_Type
    is
    begin
       --  Search table unless we have No_Location, which can happen if the
@@ -584,6 +588,7 @@ 
          declare
             Source_File : Source_File_Index;
             Source_Unit : Unit_Number_Type;
+            Unit_Node   : Node_Id;
 
          begin
             Source_File := Get_Source_File_Index (S);
@@ -596,6 +601,21 @@ 
 
             Source_Unit := Unit (Source_File);
 
+            if Unwind_Subunits then
+               Unit_Node := Unit (Cunit (Source_Unit));
+
+               while Nkind (Unit_Node) = N_Subunit
+                 and then Present (Corresponding_Stub (Unit_Node))
+               loop
+                  Source_Unit :=
+                    Get_Code_Or_Source_Unit
+                      (Sloc (Corresponding_Stub (Unit_Node)),
+                       Unwind_Instances => Unwind_Instances,
+                       Unwind_Subunits  => Unwind_Subunits);
+                  Unit_Node := Unit (Cunit (Source_Unit));
+               end loop;
+            end if;
+
             if Source_Unit /= No_Unit then
                return Source_Unit;
             end if;
@@ -616,7 +636,7 @@ 
    function Get_Code_Unit (S : Source_Ptr) return Unit_Number_Type is
    begin
       return Get_Code_Or_Source_Unit (Top_Level_Location (S),
-        Unwind_Instances => False);
+        Unwind_Instances => False, Unwind_Subunits => False);
    end Get_Code_Unit;
 
    function Get_Code_Unit (N : Node_Or_Entity_Id) return Unit_Number_Type is
@@ -691,7 +711,8 @@ 
 
    function Get_Source_Unit (S : Source_Ptr) return Unit_Number_Type is
    begin
-      return Get_Code_Or_Source_Unit (S, Unwind_Instances => True);
+      return Get_Code_Or_Source_Unit (S,
+        Unwind_Instances => True, Unwind_Subunits => False);
    end Get_Source_Unit;
 
    function Get_Source_Unit (N : Node_Or_Entity_Id) return Unit_Number_Type is
@@ -699,6 +720,22 @@ 
       return Get_Source_Unit (Sloc (N));
    end Get_Source_Unit;
 
+   -----------------------------
+   -- Get_Top_Level_Code_Unit --
+   -----------------------------
+
+   function Get_Top_Level_Code_Unit (S : Source_Ptr) return Unit_Number_Type is
+   begin
+      return Get_Code_Or_Source_Unit (Top_Level_Location (S),
+        Unwind_Instances => False, Unwind_Subunits => True);
+   end Get_Top_Level_Code_Unit;
+
+   function Get_Top_Level_Code_Unit
+     (N : Node_Or_Entity_Id) return Unit_Number_Type is
+   begin
+      return Get_Top_Level_Code_Unit (Sloc (N));
+   end Get_Top_Level_Code_Unit;
+
    --------------------------------
    -- In_Extended_Main_Code_Unit --
    --------------------------------
Index: lib.ads
===================================================================
--- lib.ads	(revision 237429)
+++ lib.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -541,6 +541,14 @@ 
    --  template, so it returns the unit number containing the code that
    --  corresponds to the node N, or the source location S.
 
+   function Get_Top_Level_Code_Unit
+     (N : Node_Or_Entity_Id) return Unit_Number_Type;
+   pragma Inline (Get_Code_Unit);
+   function Get_Top_Level_Code_Unit (S : Source_Ptr) return Unit_Number_Type;
+   --  This is like Get_Code_Unit, except that in the case of subunits, it
+   --  returns the top-level unit to which the subunit belongs instead of
+   --  the subunit.
+
    function In_Extended_Main_Code_Unit
      (N : Node_Or_Entity_Id) return Boolean;
    --  Return True if the node is in the generated code of the extended main
Index: lib-xref-spark_specific.adb
===================================================================
--- lib-xref-spark_specific.adb	(revision 237429)
+++ lib-xref-spark_specific.adb	(working copy)
@@ -150,6 +150,15 @@ 
          return;
       end if;
 
+      --  Subunits are traversed as part of the top-level unit to which they
+      --  belong.
+
+      if Present (Cunit (Ubody))
+        and then Nkind (Unit (Cunit (Ubody))) = N_Subunit
+      then
+         return;
+      end if;
+
       From := SPARK_Scope_Table.Last + 1;
 
       --  Unit might not have an associated compilation unit, as seen in code
@@ -610,6 +619,8 @@ 
             --  Both entities must be equal at this point
 
             pragma Assert (T1.Key.Ent = T2.Key.Ent);
+            pragma Assert (T1.Key.Ent_Scope = T2.Key.Ent_Scope);
+            pragma Assert (T1.Ent_Scope_File = T2.Ent_Scope_File);
 
             --  Fourth test: if reference is in same unit as entity definition,
             --  sort first.
@@ -1210,18 +1221,20 @@ 
             Deref.Loc := Loc;
             Deref.Typ := Typ;
 
-            --  It is as if the special "Heap" was defined in every scope where
-            --  it is referenced.
+            --  It is as if the special "Heap" was defined in the main unit,
+            --  in the scope of the entity for the main unit. This single
+            --  definition point is required to ensure that sorting cross
+            --  references works for "Heap" references as well.
 
-            Deref.Eun := Get_Code_Unit (Loc);
-            Deref.Lun := Get_Code_Unit (Loc);
+            Deref.Eun := Main_Unit;
+            Deref.Lun := Get_Top_Level_Code_Unit (Loc);
 
             Deref.Ref_Scope := Ref_Scope;
-            Deref.Ent_Scope := Ref_Scope;
+            Deref.Ent_Scope := Cunit_Entity (Main_Unit);
 
             Deref_Entry.Def := No_Location;
 
-            Deref_Entry.Ent_Scope_File := Get_Code_Unit (N);
+            Deref_Entry.Ent_Scope_File := Main_Unit;
          end;
       end if;
    end Generate_Dereference;
Index: lib-xref.adb
===================================================================
--- lib-xref.adb	(revision 237429)
+++ lib-xref.adb	(working copy)
@@ -1075,11 +1075,11 @@ 
               ((Ent       => Ent,
                 Loc       => Ref,
                 Typ       => Actual_Typ,
-                Eun       => Get_Code_Unit (Def),
-                Lun       => Get_Code_Unit (Ref),
+                Eun       => Get_Top_Level_Code_Unit (Def),
+                Lun       => Get_Top_Level_Code_Unit (Ref),
                 Ref_Scope => Ref_Scope,
                 Ent_Scope => Ent_Scope),
-               Ent_Scope_File => Get_Code_Unit (Ent));
+               Ent_Scope_File => Get_Top_Level_Code_Unit (Ent));
 
          else
             Ref := Original_Location (Sloc (Nod));