diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index 7ed018c8b..8003b53b9 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -118,6 +118,10 @@ let pp_html source fmt summary = F.fprintf fmt "@\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 -> diff --git a/infer/src/backend/Summary.mli b/infer/src/backend/Summary.mli index b39596bbd..dbed10667 100644 --- a/infer/src/backend/Summary.mli +++ b/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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 468730e5d..aff756a6c 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 3c736579f..ebc9dce7e 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/base/DB.mli b/infer/src/base/DB.mli index e9de8c8c9..616144cb3 100644 --- a/infer/src/base/DB.mli +++ b/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 *) diff --git a/infer/src/base/DBWriter.ml b/infer/src/base/DBWriter.ml index c8a7c271d..6e0f25a6c 100644 --- a/infer/src/base/DBWriter.ml +++ b/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}) diff --git a/infer/src/base/DBWriter.mli b/infer/src/base/DBWriter.mli index 6c50db234..1af37e285 100644 --- a/infer/src/base/DBWriter.mli +++ b/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 diff --git a/infer/src/base/ResultsDatabase.ml b/infer/src/base/ResultsDatabase.ml index a53d4cf44..745629cf5 100644 --- a/infer/src/base/ResultsDatabase.ml +++ b/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 () =