[specs] store in db

Summary: Implement specs storage in DB, apart from biabduction models which are still left in specs files.

Reviewed By: skcho

Differential Revision: D22795638

fbshipit-source-id: 140801d3f

infer/src/backend/Summary.ml

@@ -118,6 +118,10 @@ let pp_html source fmt summary =
   F.fprintf fmt "</LISTING>@\n"
 
 
+module SQLite = SqliteUtils.MarshalledDataNOTForComparison (struct
+  type nonrec t = t
+end)
+
 module OnDisk = struct
   type cache = t Procname.Hash.t
 
@@ -173,12 +177,29 @@ module OnDisk = struct
     opt
 
 
+  let spec_of_model proc_name = load_from_file (specs_models_filename proc_name)
+
+  let spec_of_proc_uid =
+    let load_statement =
+      ResultsDatabase.register_statement "SELECT spec FROM specs WHERE proc_uid = :k"
+    in
+    fun proc_file ->
+      ResultsDatabase.with_registered_statement load_statement ~f:(fun db load_stmt ->
+          Sqlite3.bind load_stmt 1 (Sqlite3.Data.TEXT proc_file)
+          |> SqliteUtils.check_result_code db ~log:"load proc specs bind proc_file" ;
+          SqliteUtils.result_single_column_option ~finalize:false ~log:"load proc specs run" db
+            load_stmt
+          |> Option.map ~f:SQLite.deserialize )
+
+
+  let spec_of_procname proc_name = spec_of_proc_uid (Procname.to_unique_id proc_name)
+
   (** Load procedure summary for the given procedure name and update spec table *)
   let load_summary_to_spec_table proc_name =
     let summ_opt =
-      match load_from_file (specs_filename_of_procname proc_name) with
+      match spec_of_procname proc_name with
       | None when BiabductionModels.mem proc_name ->
-          load_from_file (specs_models_filename proc_name)
+          spec_of_model proc_name
       | summ_opt ->
           summ_opt
     in
@@ -212,9 +233,14 @@ module OnDisk = struct
     let proc_name = get_proc_name final_summary in
     (* Make sure the summary in memory is identical to the saved one *)
     add proc_name final_summary ;
-    Serialization.write_to_file summary_serializer
-      (specs_filename_of_procname proc_name)
-      ~data:final_summary
+    if Config.biabduction_models_mode then
+      Serialization.write_to_file summary_serializer
+        (specs_filename_of_procname proc_name)
+        ~data:final_summary
+    else
+      DBWriter.store_spec
+        ~proc_uid:(Sqlite3.Data.TEXT (Procname.to_unique_id proc_name))
+        ~spec:(SQLite.serialize final_summary)
 
 
   let reset proc_desc =
@@ -233,72 +259,50 @@ module OnDisk = struct
 
   let reset_all ~filter () =
     let reset proc_name =
-      let filename = specs_filename_of_procname proc_name in
-      BackendStats.incr_summary_file_try_load () ;
-      Serialization.read_from_file summary_serializer filename
+      spec_of_procname proc_name
       |> Option.iter ~f:(fun summary ->
-             BackendStats.incr_summary_read_from_disk () ;
              let blank_summary = reset summary.proc_desc in
-             Serialization.write_to_file summary_serializer filename ~data:blank_summary )
+             store blank_summary )
     in
     Procedures.get_all ~filter () |> List.iter ~f:reset
 
 
   let delete pname =
-    let filename = specs_filename_of_procname pname |> DB.filename_to_string in
-    (* Unix_error is raised if the file isn't present so do nothing in this case *)
-    (try Unix.unlink filename with Unix.Unix_error _ -> ()) ;
-    remove_from_cache pname
+    remove_from_cache pname ;
+    if Config.biabduction_models_mode then
+      let filename = specs_filename_of_procname pname |> DB.filename_to_string in
+      (* Unix_error is raised if the file isn't present so do nothing in this case *)
+      try Unix.unlink filename with Unix.Unix_error _ -> ()
+    else DBWriter.delete_spec ~proc_uid:(Sqlite3.Data.TEXT (Procname.to_unique_id pname))
 
 
-  (** return the list of the .specs files in the results dir *)
-  let load_specfiles () =
-    let is_specs_file fname = Filename.check_suffix fname Config.specs_files_suffix in
-    let do_file acc path = if is_specs_file path then path :: acc else acc in
-    let result_specs_dir = DB.filename_to_string DB.Results_dir.specs_dir in
-    Utils.directory_fold do_file [] result_specs_dir
+  let iter_specs =
+    let iter_statement =
+      ResultsDatabase.register_statement "SELECT spec FROM specs ORDER BY proc_uid ASC"
+    in
+    fun ~f ->
+      ResultsDatabase.with_registered_statement iter_statement ~f:(fun db stmt ->
+          SqliteUtils.result_fold_single_column_rows ~finalize:false db stmt
+            ~log:"iter over all specs" ~init:() ~f:(fun () sqlite_spec ->
+              let summary : t = SQLite.deserialize sqlite_spec in
+              let () = f summary in
+              () ) )
 
 
-  let print_usage_exit err_s =
-    L.user_error "Load Error: %s@\n@." err_s ;
-    Config.print_usage_exit ()
+  let iter_specs_of_proc_uids proc_uids ~f =
+    List.iter proc_uids ~f:(fun proc_file -> spec_of_proc_uid proc_file |> Option.iter ~f)
 
 
-  let spec_files_from_cmdline () =
-    if CLOpt.is_originator then (
+  let iter_specs_from_config ~f =
+    if CLOpt.is_originator && not (List.is_empty Config.anon_args) then (
       (* Find spec files specified by command-line arguments.  Not run at init time since the specs
-         files may be generated between init and report time. *)
-      List.iter
-        ~f:(fun arg ->
-          if
-            (not (Filename.check_suffix arg Config.specs_files_suffix))
-            && not (String.equal arg ".")
-          then print_usage_exit ("file " ^ arg ^ ": arguments must be .specs files") )
-        Config.anon_args ;
+          files may be generated between init and report time. *)
       if Config.test_filtering then (
         Inferconfig.test () ;
         L.exit 0 ) ;
-      if List.is_empty Config.anon_args then load_specfiles () else List.rev Config.anon_args )
-    else load_specfiles ()
-
-
-  (** Create an iterator which loads spec files one at a time *)
-  let summary_iterator spec_files =
-    let sorted_spec_files = List.sort ~compare:String.compare (spec_files ()) in
-    let do_spec f fname =
-      match load_from_file (DB.filename_from_string fname) with
-      | None ->
-          L.(die UserError) "Error: cannot open file %s@." fname
-      | Some summary ->
-          f summary
-    in
-    let iterate f = List.iter ~f:(do_spec f) sorted_spec_files in
-    iterate
-
-
-  let iter_specs_from_config ~f = summary_iterator spec_files_from_cmdline f
+      iter_specs_of_proc_uids Config.anon_args ~f )
+    else iter_specs ~f
 
-  let iter_specs ~f = summary_iterator load_specfiles f
 
   let pp_specs_from_config fmt =
     iter_specs_from_config ~f:(fun summary ->

infer/src/backend/Summary.mli

@@ -85,11 +85,12 @@ module OnDisk : sig
       cache *)
 
   val iter_specs : f:(t -> unit) -> unit
-  (** Iterates over all summaries from the .specs files *)
+  (** Iterates over all stored summaries *)
 
   val iter_specs_from_config : f:(t -> unit) -> unit
-  (** Iterates over all sumaries from the .specs files unless a list of specs files has been passed
-      on the command line *)
+  (** Iterates over all stored summaries, or over the summaries of the list of procedure filenames
+      passed on the command line *)
 
   val pp_specs_from_config : Format.formatter -> unit
+  (** pretty print all stored summaries *)
 end

infer/src/base/Config.ml

@@ -2585,16 +2585,13 @@ let post_parsing_initialization command_opt =
   Option.value ~default:InferCommand.Run command_opt
 
 
-let command, parse_args_and_return_usage_exit =
-  let command_opt, usage_exit =
+let command =
+  let command_opt, _usage_exit =
     CLOpt.parse ?config_file:inferconfig_file ~usage:exe_usage startup_action initial_command
   in
-  let command = post_parsing_initialization command_opt in
-  (command, usage_exit)
+  post_parsing_initialization command_opt
 
 
-let print_usage_exit () = parse_args_and_return_usage_exit 1
-
 let process_linters_doc_url args =
   let linters_doc_url arg =
     match String.lsplit2 ~on:':' arg with

infer/src/base/Config.mli

@@ -647,7 +647,3 @@ val scuba_execution_id : Int64.t option
 (** {2 Global variables with initial values specified by command-line options} *)
 
 val clang_compilation_dbs : [`Escaped of string | `Raw of string] list ref
-
-(** {2 Command Line Interface Documentation} *)
-
-val print_usage_exit : unit -> 'a

infer/src/base/DB.mli

@@ -42,9 +42,6 @@ module Results_dir : sig
   val path_to_filename : path_kind -> path -> filename
   (** convert a path to a filename *)
 
-  val specs_dir : filename
-  (** directory of spec files *)
-
   val init : ?debug:bool -> SourceFile.t -> unit
   (** Initialize the results directory *)
 

infer/src/base/DBWriter.ml

@@ -173,10 +173,44 @@ module Implementation = struct
     SqliteUtils.exec db ~log:"drop procedures table" ~stmt:"DROP TABLE procedures" ;
     SqliteUtils.exec db ~log:"drop source_files table" ~stmt:"DROP TABLE source_files" ;
     ResultsDatabase.create_tables db
+
+
+  let store_spec =
+    let store_statement =
+      ResultsDatabase.register_statement "INSERT OR REPLACE INTO specs VALUES (:proc_uid, :spec)"
+    in
+    fun ~proc_uid ~spec ->
+      ResultsDatabase.with_registered_statement store_statement ~f:(fun db store_stmt ->
+          Sqlite3.bind store_stmt 1 proc_uid
+          |> SqliteUtils.check_result_code db ~log:"store spec bind proc_uid" ;
+          Sqlite3.bind store_stmt 2 spec
+          |> SqliteUtils.check_result_code db ~log:"store spec bind spec" ;
+          SqliteUtils.result_unit ~finalize:false ~log:"store spec" db store_stmt )
+
+
+  let delete_spec =
+    let delete_statement =
+      ResultsDatabase.register_statement "DELETE FROM specs WHERE proc_uid = :k"
+    in
+    fun ~proc_uid ->
+      ResultsDatabase.with_registered_statement delete_statement ~f:(fun db delete_stmt ->
+          Sqlite3.bind delete_stmt 1 proc_uid
+          |> SqliteUtils.check_result_code db ~log:"delete spec bind proc_uid" ;
+          SqliteUtils.result_unit ~finalize:false ~log:"store spec" db delete_stmt )
 end
 
 module Command = struct
   type t =
+    | AddSourceFile of
+        { source_file: Sqlite3.Data.t
+        ; tenv: Sqlite3.Data.t
+        ; integer_type_widths: Sqlite3.Data.t
+        ; proc_names: Sqlite3.Data.t }
+    | DeleteSpec of {proc_uid: Sqlite3.Data.t}
+    | Handshake
+    | MarkAllSourceFilesStale
+    | Merge of {infer_deps_file: string}
+    | StoreSpec of {proc_uid: Sqlite3.Data.t; spec: Sqlite3.Data.t}
     | ReplaceAttributes of
         { pname_str: string
         ; pname: Sqlite3.Data.t
@@ -185,57 +219,57 @@ module Command = struct
         ; attributes: Sqlite3.Data.t
         ; proc_desc: Sqlite3.Data.t
         ; callees: Sqlite3.Data.t }
-    | AddSourceFile of
-        { source_file: Sqlite3.Data.t
-        ; tenv: Sqlite3.Data.t
-        ; integer_type_widths: Sqlite3.Data.t
-        ; proc_names: Sqlite3.Data.t }
-    | MarkAllSourceFilesStale
-    | Merge of {infer_deps_file: string}
-    | Vacuum
     | ResetCaptureTables
-    | Handshake
     | Terminate
+    | Vacuum
 
   let to_string = function
-    | ReplaceAttributes _ ->
-        "ReplaceAttributes"
     | AddSourceFile _ ->
         "AddSourceFile"
+    | DeleteSpec _ ->
+        "DeleteSpec"
+    | Handshake ->
+        "Handshake"
     | MarkAllSourceFilesStale ->
         "MarkAllSourceFilesStale"
     | Merge _ ->
         "Merge"
-    | Vacuum ->
-        "Vacuum"
+    | ReplaceAttributes _ ->
+        "ReplaceAttributes"
     | ResetCaptureTables ->
         "ResetCaptureTables"
-    | Handshake ->
-        "Handshake"
+    | StoreSpec _ ->
+        "StoreSpec"
     | Terminate ->
         "Terminate"
+    | Vacuum ->
+        "Vacuum"
 
 
   let pp fmt cmd = F.pp_print_string fmt (to_string cmd)
 
   let execute = function
-    | ReplaceAttributes {pname_str; pname; akind; source_file; attributes; proc_desc; callees} ->
-        Implementation.replace_attributes ~pname_str ~pname ~akind ~source_file ~attributes
-          ~proc_desc ~callees
     | AddSourceFile {source_file; tenv; integer_type_widths; proc_names} ->
         Implementation.add_source_file ~source_file ~tenv ~integer_type_widths ~proc_names
+    | DeleteSpec {proc_uid} ->
+        Implementation.delete_spec ~proc_uid
+    | Handshake ->
+        ()
     | MarkAllSourceFilesStale ->
         Implementation.mark_all_source_files_stale ()
     | Merge {infer_deps_file} ->
         Implementation.merge infer_deps_file
-    | Vacuum ->
-        Implementation.canonicalize ()
+    | StoreSpec {proc_uid; spec} ->
+        Implementation.store_spec ~proc_uid ~spec
+    | ReplaceAttributes {pname_str; pname; akind; source_file; attributes; proc_desc; callees} ->
+        Implementation.replace_attributes ~pname_str ~pname ~akind ~source_file ~attributes
+          ~proc_desc ~callees
     | ResetCaptureTables ->
         Implementation.reset_capture_tables ()
-    | Handshake ->
-        ()
     | Terminate ->
         ()
+    | Vacuum ->
+        Implementation.canonicalize ()
 end
 
 type response = Ack
@@ -349,3 +383,7 @@ let merge ~infer_deps_file = Command.Merge {infer_deps_file} |> perform
 let canonicalize () = perform Command.Vacuum
 
 let reset_capture_tables () = perform Command.ResetCaptureTables
+
+let store_spec ~proc_uid ~spec = perform (Command.StoreSpec {proc_uid; spec})
+
+let delete_spec ~proc_uid = perform (Command.DeleteSpec {proc_uid})

infer/src/base/DBWriter.mli

@@ -40,3 +40,7 @@ val reset_capture_tables : unit -> unit
 val start : unit -> unit
 
 val stop : unit -> unit
+
+val store_spec : proc_uid:Sqlite3.Data.t -> spec:Sqlite3.Data.t -> unit
+
+val delete_spec : proc_uid:Sqlite3.Data.t -> unit

infer/src/base/ResultsDatabase.ml

@@ -36,7 +36,19 @@ let source_files_schema prefix =
     prefix
 
 
-let schema_hum = Printf.sprintf "%s;\n%s" (procedures_schema "") (source_files_schema "")
+let specs_schema prefix =
+  Printf.sprintf
+    {|
+      CREATE TABLE IF NOT EXISTS %sspecs
+      ( proc_uid TEXT PRIMARY KEY
+      , spec BLOB NOT NULL
+    )|}
+    prefix
+
+
+let schema_hum =
+  String.concat ~sep:";\n" [procedures_schema ""; source_files_schema ""; specs_schema ""]
+
 
 let create_procedures_table ~prefix db =
   (* it would be nice to use "WITHOUT ROWID" here but ancient versions of sqlite do not support
@@ -48,9 +60,14 @@ let create_source_files_table ~prefix db =
   SqliteUtils.exec db ~log:"creating source_files table" ~stmt:(source_files_schema prefix)
 
 
+let create_specs_table ~prefix db =
+  SqliteUtils.exec db ~log:"creating specs table" ~stmt:(specs_schema prefix)
+
+
 let create_tables ?(prefix = "") db =
   create_procedures_table ~prefix db ;
-  create_source_files_table ~prefix db
+  create_source_files_table ~prefix db ;
+  create_specs_table ~prefix db
 
 
 let create_db () =