[specs] fix reanalysis

Summary: Moving specs to the DB missed out cleaning out all specs when reanalysing.  This is the fix.

Reviewed By: jvillard

Differential Revision: D23188958

fbshipit-source-id: 5b50fdda8

infer/src/backend/InferAnalyze.ml

@@ -225,7 +225,7 @@ let main ~changed_files =
       L.progress "Invalidating procedures to be reanalyzed@." ;
       Summary.OnDisk.reset_all ~filter:(Lazy.force Filtering.procedures_filter) () ;
       L.progress "Done@." )
-    else if not Config.incremental_analysis then DB.Results_dir.clean_specs_dir () ;
+    else if not Config.incremental_analysis then DBWriter.delete_all_specs () ;
   let source_files = lazy (get_source_files_to_analyze ~changed_files) in
   (* empty all caches to minimize the process heap to have less work to do when forking *)
   clear_caches () ;

infer/src/base/DB.ml

@@ -125,9 +125,6 @@ module Results_dir = struct
     filename_from_base base path
 
 
-  (** directory of spec files *)
-  let specs_dir = ResultsDir.get_path Specs
-
   (** initialize the results directory *)
   let init ?(debug = false) source =
     if SourceFile.is_invalid source then L.(die InternalError) "Invalid source file passed" ;
@@ -136,12 +133,6 @@ module Results_dir = struct
       Utils.create_dir (path_to_filename (Abs_source_dir source) []) )
 
 
-  let clean_specs_dir () =
-    (* create dir just in case it doesn't exist to avoid errors *)
-    Utils.rmtree specs_dir ;
-    Utils.create_dir specs_dir
-
-
   (** create a file at the given path, creating any missing directories *)
   let create_file pk path =
     let rec create = function

infer/src/base/DB.mli

@@ -45,9 +45,6 @@ module Results_dir : sig
   val init : ?debug:bool -> SourceFile.t -> unit
   (** Initialize the results directory *)
 
-  val clean_specs_dir : unit -> unit
-  (** Clean up specs directory *)
-
   val create_file : path_kind -> path -> Unix.File_descr.t
   (** create a file at the given path, creating any missing directories *)
 end

infer/src/base/DBWriter.ml

@@ -200,6 +200,11 @@ module Implementation = struct
           Sqlite3.bind delete_stmt 1 proc_name
           |> SqliteUtils.check_result_code db ~log:"delete spec bind proc_name" ;
           SqliteUtils.result_unit ~finalize:false ~log:"store spec" db delete_stmt )
+
+
+  let delete_all_specs () =
+    let db = ResultsDatabase.get_database () in
+    SqliteUtils.exec db ~log:"drop procedures table" ~stmt:"DELETE FROM specs"
 end
 
 module Command = struct
@@ -209,6 +214,7 @@ module Command = struct
         ; tenv: Sqlite3.Data.t
         ; integer_type_widths: Sqlite3.Data.t
         ; proc_names: Sqlite3.Data.t }
+    | DeleteAllSpecs
     | DeleteSpec of {proc_name: Sqlite3.Data.t}
     | Handshake
     | MarkAllSourceFilesStale
@@ -230,6 +236,8 @@ module Command = struct
   let to_string = function
     | AddSourceFile _ ->
         "AddSourceFile"
+    | DeleteAllSpecs ->
+        "DeleteAllSpecs"
     | DeleteSpec _ ->
         "DeleteSpec"
     | Handshake ->
@@ -255,6 +263,8 @@ module Command = struct
   let execute = function
     | AddSourceFile {source_file; tenv; integer_type_widths; proc_names} ->
         Implementation.add_source_file ~source_file ~tenv ~integer_type_widths ~proc_names
+    | DeleteAllSpecs ->
+        Implementation.delete_all_specs ()
     | DeleteSpec {proc_name} ->
         Implementation.delete_spec ~proc_name
     | Handshake ->
@@ -392,3 +402,5 @@ let store_spec ~proc_name ~analysis_summary ~report_summary =
 
 
 let delete_spec ~proc_name = perform (DeleteSpec {proc_name})
+
+let delete_all_specs () = perform DeleteAllSpecs

infer/src/base/DBWriter.mli

@@ -48,3 +48,5 @@ val store_spec :
   -> unit
 
 val delete_spec : proc_name:Sqlite3.Data.t -> unit
+
+val delete_all_specs : unit -> unit