spat_1.3.0_4ad4ab14/src/util/spat-gpr_support.adb

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
------------------------------------------------------------------------------
--  Copyright (C) 2020 by Heisenbug Ltd. (gh+spat@heisenbug.eu)
--
--  This work is free. You can redistribute it and/or modify it under the
--  terms of the Do What The Fuck You Want To Public License, Version 2,
--  as published by Sam Hocevar. See the LICENSE file for more details.
------------------------------------------------------------------------------
pragma License (Unrestricted);

with Ada.Containers.Hashed_Sets;
with Ada.Directories;

with GNATCOLL.Projects;
with SPAT.Log;
with SPAT.Stop_Watch;

package body SPAT.GPR_Support is

   package File_Name_Caches is new
     Ada.Containers.Hashed_Sets
       (Element_Type        => SPARK_File_Name,
        Hash                => SPAT.Hash,
        Equivalent_Elements => "=");

   ---------------------------------------------------------------------------
   --  Add_File
   ---------------------------------------------------------------------------
   procedure Add_File (Project_Tree : in     GNATCOLL.Projects.Project_Tree;
                       Source_File  : in     GNATCOLL.VFS.Virtual_File;
                       Cache        : in out File_Name_Caches.Set;
                       To           : in out SPARK_Source_Maps.Map);

   ---------------------------------------------------------------------------
   --  To_SPARK_Name
   ---------------------------------------------------------------------------
   function To_SPARK_Name
     (Project_Tree : in GNATCOLL.Projects.Project_Tree;
      Source_File  : in GNATCOLL.VFS.Virtual_File) return String;

   ---------------------------------------------------------------------------
   --  Prefer_Body_File
   --
   --  Checks if for the given key a mapping already exists and updates it if
   --  the given Value seems a better fit (i.e. is a body file).
   --  Apparently steps and timeout values should be given to the body file,
   --  if they are specified for the spec, proofs seem to fail, see
   --  https://github.com/HeisenbugLtd/spat/issues/55#issuecomment-657505781
   ---------------------------------------------------------------------------
   procedure Prefer_Body_File
     (File_Map     : in out SPARK_Source_Maps.Map;
      Project_Tree : in     GNATCOLL.Projects.Project_Tree;
      Key          : in     SPARK_File_Name;
      Value        : in     GNATCOLL.VFS.Virtual_File);

   ---------------------------------------------------------------------------
   --  Add_File
   ---------------------------------------------------------------------------
   procedure Add_File (Project_Tree : in     GNATCOLL.Projects.Project_Tree;
                       Source_File  : in     GNATCOLL.VFS.Virtual_File;
                       Cache        : in out File_Name_Caches.Set;
                       To           : in out SPARK_Source_Maps.Map)
   is
      SPARK_Name   : constant String :=
        To_SPARK_Name (Project_Tree => Project_Tree,
                       Source_File  => Source_File);
      As_File_Name : constant SPARK_File_Name :=
        SPARK_File_Name (To_Name (Source => SPARK_Name));
      Simple_Name  : constant String :=
        Ada.Directories.Simple_Name (Name => SPARK_Name);
      Exists       : constant Boolean :=
        Ada.Directories.Exists (Name => SPARK_Name);
      Dummy_Cursor : File_Name_Caches.Cursor; --  Don't care about the position.
      Inserted     : Boolean;
   begin
      --  Prevent adding the same file twice. The caller retrieves all files
      --  from the project, hence in most cases we will encounter both a spec
      --  and a body file which will still result in the same .spark file.
      Cache.Insert (New_Item => As_File_Name,
                    Position => Dummy_Cursor,
                    Inserted => Inserted);

      Log.Debug (Message  =>
                   """" & Simple_Name & """ " &
                   (if Inserted
                    then "added to"
                    else "already in") & " index.");

      --  If the .spark file exists, add it to the result map, possibly
      --  updating the file mapping as we do prefer the spec file.
      if Exists then
         Prefer_Body_File (File_Map     => To,
                           Project_Tree => Project_Tree,
                           Key          => As_File_Name,
                           Value        => Source_File);
      else
         Log.Debug
           (Message =>
              """" & Simple_Name & """ not found on disk, skipped.");
      end if;
   end Add_File;

   ---------------------------------------------------------------------------
   --  Get_SPARK_Files
   ---------------------------------------------------------------------------
   function Get_SPARK_Files
     (GPR_File : GNATCOLL.VFS.Filesystem_String) return SPARK_Source_Maps.Map
   is
      Timer : Stop_Watch.T := Stop_Watch.Create;

      Project_Tree : GNATCOLL.Projects.Project_Tree;
   begin
      Load_Project :
      begin
         Timer.Start; --  Start lap measurement.

         Project_Tree.Load
           (Root_Project_Path =>
              GNATCOLL.VFS.Create (Full_Filename => GPR_File));

         Log.Debug (Message => "GNAT project loaded in " & Timer.Elapsed & ".");
      exception
         when GNATCOLL.Projects.Invalid_Project =>
            Log.Error
              (Message =>
                  "Could not load """ & GNATCOLL.VFS."+" (GPR_File) & """!");
            return SPARK_Source_Maps.Empty_Map;
      end Load_Project;

      Timer.Start; --  Next lap measurement

      Load_Source_Files :
      declare
         --  Retrieve all project files recursively.
         Project_Files : GNATCOLL.VFS.File_Array_Access :=
           Project_Tree.Root_Project.Source_Files (Recursive => True);

         --  Get maximum number of entries we may encounter.
         Capacity : constant Ada.Containers.Count_Type :=
           Project_Files.all'Length;

         --  Initialize the lists.
         Raw_List    : File_Name_Caches.Set;
         --  Stores all encountered files.
         Result_List : SPARK_Source_Maps.Map;
         --  Stores only files that exist on disk.
      begin
         Raw_List.Reserve_Capacity (Capacity => Capacity);

         for F of Project_Files.all loop
            --  TODO: We should probably check the language of the file here, if
            --        it's not Ada, we can likely skip it.
            Log.Debug
              (Message  => "Found """ & F.Display_Base_Name & """...",
               New_Line => False);

            Add_File (Project_Tree => Project_Tree,
                      Source_File  => F,
                      Cache        => Raw_List,
                      To           => Result_List);
         end loop;

         --  Cleanup.
         GNATCOLL.VFS.Unchecked_Free (Arr => Project_Files);
         Project_Tree.Unload;

         Report_Timing :
         declare
            Num_Files : constant Ada.Containers.Count_Type :=
              Result_List.Length;
            use type Ada.Containers.Count_Type;
         begin
            Log.Debug
              (Message =>
                 "Search completed in " & Timer.Elapsed &
                 "," & Num_Files'Image & " file" &
               (if Num_Files /= 1 then "s" else "") & " found.");
         end Report_Timing;

         return Result_List;
      end Load_Source_Files;
   end Get_SPARK_Files;

   ---------------------------------------------------------------------------
   --  Prefer_Body_File
   ---------------------------------------------------------------------------
   procedure Prefer_Body_File
     (File_Map     : in out SPARK_Source_Maps.Map;
      Project_Tree : in     GNATCOLL.Projects.Project_Tree;
      Key          : in     SPARK_File_Name;
      Value        : in     GNATCOLL.VFS.Virtual_File)
   is
      use all type GNATCOLL.Projects.Unit_Parts;
   begin
      if not File_Map.Contains (Key => Key) then
         --  Not yet in map, insert unconditionally.
         File_Map.Insert
           (Key      => Key,
            New_Item => Source_File_Name (To_Name (Value.Display_Base_Name)));
      elsif Project_Tree.Info (File => Value).Unit_Part = Unit_Body then
         --  We already have an entry, but this is (a/the) body, we prefer that.
         File_Map.Include
           (Key      => Key,
            New_Item => Source_File_Name (To_Name (Value.Display_Base_Name)));
      end if;
   end Prefer_Body_File;

   ---------------------------------------------------------------------------
   --  SPARK_Name
   ---------------------------------------------------------------------------
   function To_SPARK_Name
     (Project_Tree : in GNATCOLL.Projects.Project_Tree;
      Source_File  : in GNATCOLL.VFS.Virtual_File) return String
   is
      use type GNATCOLL.VFS.Filesystem_String;

      File_Info : constant GNATCOLL.Projects.File_Info :=
        Project_Tree.Info (File => Source_File);
      Object_Directory : constant String :=
        +GNATCOLL.Projects.Object_Dir (Project => File_Info.Project).Full_Name.all;
   begin
      --  .spark files seem to reside in the "gnatprove" sub-directory of the
      --  object directory defined by the project.  As files might come from
      --  different projects, we query the project associated to the file and
      --  then use this project's object directory instead of using the object
      --  directory from the root project.
      --  This is untested, so maybe we should create some dummy projects to
      --  test this assumption.
      --  TODO: Also, aggregate projects
      --        (GNATCOLL.Projects.Is_Aggregate_Project) do not support the
      --        File_Info call, so there's still something to be done here...
      return
        Ada.Directories.Compose
          (Containing_Directory =>
             Ada.Directories.Compose
               (Containing_Directory => Object_Directory,
                Name                 => "gnatprove"),
           Name                 =>
             Ada.Directories.Base_Name
               (Name => Source_File.Display_Full_Name),
           Extension            => "spark");
   end To_SPARK_Name;

end SPAT.GPR_Support;