------------------------------------------------------------------------------
--                                                                          --
--                         GNAT COMPILER COMPONENTS                         --
--                                                                          --
--              L I B . X R E F . S P A R K _ S P E C I F I C               --
--                                                                          --
--                                 B o d y                                  --
--                                                                          --
--          Copyright (C) 2011-2023, 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- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
-- for  more details.  You should have  received  a copy of the GNU General --
-- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license.          --
--                                                                          --
-- GNAT was originally developed  by the GNAT team at  New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc.      --
--                                                                          --
------------------------------------------------------------------------------

with Einfo.Entities; use Einfo.Entities;
with Nmake;          use Nmake;
with SPARK_Xrefs;    use SPARK_Xrefs;

separate (Lib.Xref)
package body SPARK_Specific is

   ---------------------
   -- Local Constants --
   ---------------------

   --  Table of SPARK_Entities, True for each entity kind used in SPARK

   SPARK_Entities : constant array (Entity_Kind) of Boolean :=
     (E_Constant         => True,
      E_Entry            => True,
      E_Function         => True,
      E_In_Out_Parameter => True,
      E_In_Parameter     => True,
      E_Loop_Parameter   => True,
      E_Operator         => True,
      E_Out_Parameter    => True,
      E_Procedure        => True,
      E_Variable         => True,
      others             => False);

   --  True for each reference type used in SPARK

   SPARK_References : constant array (Character) of Boolean :=
     ('m'    => True,
      'r'    => True,
      's'    => True,
      others => False);

   ---------------------
   -- Local Variables --
   ---------------------

   package Drefs is new Table.Table (
     Table_Component_Type => Xref_Entry,
     Table_Index_Type     => Xref_Entry_Number,
     Table_Low_Bound      => 1,
     Table_Initial        => Alloc.Drefs_Initial,
     Table_Increment      => Alloc.Drefs_Increment,
     Table_Name           => "Drefs");
   --  Table of cross-references for reads and writes through explicit
   --  dereferences, that are output as reads/writes to the special variable
   --  "Heap". These references are added to the regular references when
   --  computing SPARK cross-references.

   -------------------------
   -- Iterate_SPARK_Xrefs --
   -------------------------

   procedure Iterate_SPARK_Xrefs is

      procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry);

      function Is_SPARK_Reference
        (E   : Entity_Id;
         Typ : Character) return Boolean;
      --  Return whether entity reference E meets SPARK requirements. Typ is
      --  the reference type.

      function Is_SPARK_Scope (E : Entity_Id) return Boolean;
      --  Return whether the entity or reference scope meets requirements for
      --  being a SPARK scope.

      --------------------
      -- Add_SPARK_Xref --
      --------------------

      procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry) is
         Ref : Xref_Key renames Xref.Key;
      begin
         --  Eliminate entries not appropriate for SPARK

         if SPARK_Entities (Ekind (Ref.Ent))
           and then SPARK_References (Ref.Typ)
           and then Is_SPARK_Scope (Ref.Ent_Scope)
           and then Is_SPARK_Scope (Ref.Ref_Scope)
           and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
         then
            Process
              (Index,
               (Entity    => Ref.Ent,
                Ref_Scope => Ref.Ref_Scope,
                Rtype     => Ref.Typ));
         end if;

      end Add_SPARK_Xref;

      ------------------------
      -- Is_SPARK_Reference --
      ------------------------

      function Is_SPARK_Reference
        (E   : Entity_Id;
         Typ : Character) return Boolean
      is
      begin
         --  The only references of interest on callable entities are calls. On
         --  uncallable entities, the only references of interest are reads and
         --  writes.

         if Ekind (E) in Overloadable_Kind then
            return Typ = 's';

         --  In all other cases, result is true for reference/modify cases,
         --  and false for all other cases.

         else
            return Typ = 'r' or else Typ = 'm';
         end if;
      end Is_SPARK_Reference;

      --------------------
      -- Is_SPARK_Scope --
      --------------------

      function Is_SPARK_Scope (E : Entity_Id) return Boolean is
         Can_Be_Renamed : constant Boolean :=
                            Present (E)
                              and then (Is_Subprogram_Or_Entry (E)
                                         or else Ekind (E) = E_Package);
      begin
         return Present (E)
           and then not Is_Generic_Unit (E)
           and then (not Can_Be_Renamed or else No (Renamed_Entity (E)));
      end Is_SPARK_Scope;

   --  Start of processing for Add_SPARK_Xrefs

   begin
      --  Expose cross-references from private frontend tables to the backend

      for Index in Drefs.First .. Drefs.Last loop
         Add_SPARK_Xref (Index, Drefs.Table (Index));
      end loop;

      for Index in Xrefs.First .. Xrefs.Last loop
         Add_SPARK_Xref (-Index, Xrefs.Table (Index));
      end loop;
   end Iterate_SPARK_Xrefs;

   ---------------------------------------------
   -- Enclosing_Subprogram_Or_Library_Package --
   ---------------------------------------------

   function Enclosing_Subprogram_Or_Library_Package
     (N : Node_Id) return Entity_Id
   is
      Context : Entity_Id;

   begin
      --  If N is the defining identifier for a subprogram, then return the
      --  enclosing subprogram or package, not this subprogram.

      if Nkind (N) in N_Defining_Identifier | N_Defining_Operator_Symbol
        and then Ekind (N) in Entry_Kind
                            | E_Subprogram_Body
                            | Generic_Subprogram_Kind
                            | Subprogram_Kind
      then
         if No (Unit_Declaration_Node (N)) then
            return Empty;
         end if;

         Context := Parent (Unit_Declaration_Node (N));

         --  If this was a library-level subprogram then replace Context with
         --  its Unit, which points to N_Subprogram_* node.

         if Nkind (Context) = N_Compilation_Unit then
            Context := Unit (Context);
         end if;
      else
         Context := N;
      end if;

      while Present (Context) loop
         case Nkind (Context) is
            when N_Package_Body
               | N_Package_Specification
            =>
               --  Only return a library-level package

               if Is_Library_Level_Entity (Defining_Entity (Context)) then
                  Context := Defining_Entity (Context);
                  exit;
               else
                  Context := Parent (Context);
               end if;

            when N_Pragma =>

               --  The enclosing subprogram for a precondition, postcondition,
               --  or contract case should be the declaration preceding the
               --  pragma (skipping any other pragmas between this pragma and
               --  this declaration.

               while Nkind (Context) = N_Pragma
                 and then Is_List_Member (Context)
                 and then Present (Prev (Context))
               loop
                  Context := Prev (Context);
               end loop;

               if Nkind (Context) = N_Pragma then

                  --  When used for cross-references then aspects might not be
                  --  yet linked to pragmas; when used for AST navigation in
                  --  GNATprove this routine is expected to follow those links.

                  if From_Aspect_Specification (Context) then
                     Context := Corresponding_Aspect (Context);
                     pragma Assert (Nkind (Context) = N_Aspect_Specification);
                     Context := Entity (Context);
                  else
                     Context := Parent (Context);
                  end if;
               end if;

            when N_Entry_Body
               | N_Entry_Declaration
               | N_Protected_Type_Declaration
               | N_Subprogram_Body
               | N_Subprogram_Declaration
               | N_Subprogram_Specification
               | N_Task_Body
               | N_Task_Type_Declaration
            =>
               Context := Defining_Entity (Context);
               exit;

            when others =>
               Context := Parent (Context);
         end case;
      end loop;

      if Nkind (Context) = N_Defining_Program_Unit_Name then
         Context := Defining_Identifier (Context);
      end if;

      --  Do not return a scope without a proper location

      if Present (Context)
        and then Sloc (Context) = No_Location
      then
         return Empty;
      end if;

      return Context;
   end Enclosing_Subprogram_Or_Library_Package;

   --------------------------
   -- Generate_Dereference --
   --------------------------

   procedure Generate_Dereference
     (N   : Node_Id;
      Typ : Character := 'r')
   is
      procedure Create_Heap;
      --  Create and decorate the special entity which denotes the heap

      -----------------
      -- Create_Heap --
      -----------------

      procedure Create_Heap is
      begin
         Heap :=
           Make_Defining_Identifier
             (Standard_Location,
              Name_Enter (Name_Of_Heap_Variable));

         Mutate_Ekind    (Heap, E_Variable);
         Set_Is_Internal (Heap, True);
         Set_Etype       (Heap, Standard_Void_Type);
         Set_Scope       (Heap, Standard_Standard);
         Set_Has_Fully_Qualified_Name (Heap);
      end Create_Heap;

      --  Local variables

      Loc : constant Source_Ptr := Sloc (N);

   --  Start of processing for Generate_Dereference

   begin
      if Loc > No_Location then
         Drefs.Increment_Last;

         declare
            Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last);
            Deref       : Xref_Key   renames Deref_Entry.Key;

         begin
            if No (Heap) then
               Create_Heap;
            end if;

            Deref.Ent := Heap;
            Deref.Loc := Loc;
            Deref.Typ := Typ;

            --  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 := Main_Unit;
            Deref.Lun := Get_Top_Level_Code_Unit (Loc);

            Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
            Deref.Ent_Scope := Cunit_Entity (Main_Unit);

            Deref_Entry.Def := No_Location;

            Deref_Entry.Ent_Scope_File := Main_Unit;
         end;
      end if;
   end Generate_Dereference;

end SPARK_Specific;