[specs] index by procname

Summary:
As preparation for splitting summaries into some of their components, and then iterating over only those when reporting (thus gaining performance) we need procnames in the table.

Also, this fixes the now-broken use case of `infer report` with spec files, by using `--procedures-filter` to restrict printing of summaries accordingly.

Reviewed By: skcho

Differential Revision: D23101853

fbshipit-source-id: 1ae878d8e
master
Nikos Gorogiannis 4 years ago committed by Facebook GitHub Bot
parent b763a9dd7e
commit a9c9d97fb6

@ -179,21 +179,19 @@ module OnDisk = struct
let spec_of_model proc_name = load_from_file (specs_models_filename proc_name)
let spec_of_proc_uid =
let spec_of_procname =
let load_statement =
ResultsDatabase.register_statement "SELECT spec FROM specs WHERE proc_uid = :k"
ResultsDatabase.register_statement "SELECT spec FROM specs WHERE proc_name = :k"
in
fun proc_file ->
fun proc_name ->
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" ;
Sqlite3.bind load_stmt 1 (Procname.SQLite.serialize proc_name)
|> SqliteUtils.check_result_code db ~log:"load proc specs bind proc_name" ;
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 =
@ -239,7 +237,7 @@ module OnDisk = struct
~data:final_summary
else
DBWriter.store_spec
~proc_uid:(Sqlite3.Data.TEXT (Procname.to_unique_id proc_name))
~proc_name:(Procname.SQLite.serialize proc_name)
~spec:(SQLite.serialize final_summary)
@ -273,12 +271,13 @@ module OnDisk = struct
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))
else DBWriter.delete_spec ~proc_name:(Procname.SQLite.serialize pname)
let iter_specs =
let iter_statement =
ResultsDatabase.register_statement "SELECT spec FROM specs ORDER BY proc_uid ASC"
(* NB the order is deterministic, but it is over a serialised value, so it is arbitrary *)
ResultsDatabase.register_statement "SELECT spec FROM specs ORDER BY proc_name ASC"
in
fun ~f ->
ResultsDatabase.with_registered_statement iter_statement ~f:(fun db stmt ->
@ -289,18 +288,23 @@ module OnDisk = struct
() ) )
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 iter_over_filter ~filter ~f =
let db = ResultsDatabase.get_database () in
(* NB the order is deterministic, but it is over a serialised value, so it is arbitrary *)
Sqlite3.prepare db "SELECT proc_name, spec FROM specs ORDER BY proc_name ASC"
|> Container.iter ~fold:(SqliteUtils.result_fold_rows db ~log:"iter over filtered specs")
~f:(fun stmt ->
let proc_name = Sqlite3.column stmt 0 |> Procname.SQLite.deserialize in
let spec = Sqlite3.column stmt 1 |> SQLite.deserialize in
if filter (SourceFile.invalid "invalid") proc_name then f spec )
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. *)
if CLOpt.is_originator && Option.is_some Config.procedures_filter then (
if Config.test_filtering then (
Inferconfig.test () ;
L.exit 0 ) ;
iter_specs_of_proc_uids Config.anon_args ~f )
iter_over_filter ~filter:(Lazy.force Filtering.procedures_filter) ~f )
else iter_specs ~f

@ -137,6 +137,7 @@ val mk_symbol_seq :
val mk_json : Yojson.Basic.t ref t
val mk_anon : unit -> string list ref
[@@warning "-32"]
(** [mk_anon ()] defines a [string list ref] of the anonymous command line arguments, in the reverse
order they appeared on the command line. *)

@ -479,8 +479,6 @@ let get_symbols_regexp json_obj =
can be defined together sharing a reference. See debug and specs_library below for two
different examples. *)
let anon_args = CLOpt.mk_anon ()
let all_checkers = ref []
let disable_all_checkers () = List.iter !all_checkers ~f:(fun (_, _, var) -> var := false)
@ -2609,9 +2607,7 @@ let process_linters_doc_url args =
(** Freeze initialized configuration values *)
let anon_args = !anon_args
and rest = !rest
let rest = !rest
and abs_struct = !abs_struct

@ -164,8 +164,6 @@ val annotation_reachability_cxx_sources : Yojson.Basic.t
val annotation_reachability_custom_pairs : Yojson.Basic.t
val anon_args : string list
val array_level : int
val biabduction_models_mode : bool

@ -66,7 +66,7 @@ module Implementation = struct
ResultsDatabase.register_statement
{|
INSERT OR REPLACE INTO source_files
VALUES (:source, :tenv, :integer_type_widths, :proc_names, :freshly_captured)
VALUES (:source, :tenv, :integer_type_widths, :proc_names, :freshly_captured)
|}
@ -177,12 +177,12 @@ module Implementation = struct
let store_spec =
let store_statement =
ResultsDatabase.register_statement "INSERT OR REPLACE INTO specs VALUES (:proc_uid, :spec)"
ResultsDatabase.register_statement "INSERT OR REPLACE INTO specs VALUES (:proc_name, :spec)"
in
fun ~proc_uid ~spec ->
fun ~proc_name ~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 1 proc_name
|> SqliteUtils.check_result_code db ~log:"store spec bind proc_name" ;
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 )
@ -190,12 +190,12 @@ module Implementation = struct
let delete_spec =
let delete_statement =
ResultsDatabase.register_statement "DELETE FROM specs WHERE proc_uid = :k"
ResultsDatabase.register_statement "DELETE FROM specs WHERE proc_name = :k"
in
fun ~proc_uid ->
fun ~proc_name ->
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" ;
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 )
end
@ -206,11 +206,11 @@ module Command = struct
; tenv: Sqlite3.Data.t
; integer_type_widths: Sqlite3.Data.t
; proc_names: Sqlite3.Data.t }
| DeleteSpec of {proc_uid: Sqlite3.Data.t}
| DeleteSpec of {proc_name: Sqlite3.Data.t}
| Handshake
| MarkAllSourceFilesStale
| Merge of {infer_deps_file: string}
| StoreSpec of {proc_uid: Sqlite3.Data.t; spec: Sqlite3.Data.t}
| StoreSpec of {proc_name: Sqlite3.Data.t; spec: Sqlite3.Data.t}
| ReplaceAttributes of
{ pname_str: string
; pname: Sqlite3.Data.t
@ -251,16 +251,16 @@ 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
| DeleteSpec {proc_uid} ->
Implementation.delete_spec ~proc_uid
| DeleteSpec {proc_name} ->
Implementation.delete_spec ~proc_name
| Handshake ->
()
| MarkAllSourceFilesStale ->
Implementation.mark_all_source_files_stale ()
| Merge {infer_deps_file} ->
Implementation.merge infer_deps_file
| StoreSpec {proc_uid; spec} ->
Implementation.store_spec ~proc_uid ~spec
| StoreSpec {proc_name; spec} ->
Implementation.store_spec ~proc_name ~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
@ -384,6 +384,6 @@ 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 store_spec ~proc_name ~spec = perform (Command.StoreSpec {proc_name; spec})
let delete_spec ~proc_uid = perform (Command.DeleteSpec {proc_uid})
let delete_spec ~proc_name = perform (Command.DeleteSpec {proc_name})

@ -41,6 +41,6 @@ val start : unit -> unit
val stop : unit -> unit
val store_spec : proc_uid:Sqlite3.Data.t -> spec:Sqlite3.Data.t -> unit
val store_spec : proc_name:Sqlite3.Data.t -> spec:Sqlite3.Data.t -> unit
val delete_spec : proc_uid:Sqlite3.Data.t -> unit
val delete_spec : proc_name:Sqlite3.Data.t -> unit

@ -40,7 +40,7 @@ let specs_schema prefix =
Printf.sprintf
{|
CREATE TABLE IF NOT EXISTS %sspecs
( proc_uid TEXT PRIMARY KEY
( proc_name TEXT PRIMARY KEY
, spec BLOB NOT NULL
)|}
prefix

@ -1 +1 @@
templates.cpp, unused_var_template_bad<char>, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]
templates.cpp, unused_var_template_bad<int>, 1, DEAD_STORE, no_bucket, ERROR, [Write of unused value]

@ -2,28 +2,28 @@
digraph callgraph {
N1 [ label = "Test.<init>()", flag = true ];
N5 [ label = "void Test.main(String[])", flag = true ];
N5 [ label = "void PrintStream.println(String)", flag = false ];
N5 -> N3 ;
N0 [ label = "Object.<init>()", flag = false ];
N0 -> N7 ;
N0 -> N2 ;
N0 -> N1 ;
N7 [ label = "Unchanged.<init>()", flag = false ];
N7 [ label = "void Test.complexityIncrease(int)", flag = true ];
N7 -> N8 ;
N6 [ label = "void Test.newMethod(int)", flag = true ];
N6 [ label = "void Test.complexityDecrease(int)", flag = true ];
N6 -> N8 ;
N4 [ label = "void Test.complexityIncrease(int)", flag = true ];
N4 -> N5 ;
N4 [ label = "void Test.newMethod(int)", flag = true ];
N2 [ label = "void Unchanged.orderN(int)", flag = false ];
N2 -> N6 ;
N2 -> N4 ;
N2 -> N3 ;
N2 [ label = "Unchanged.<init>()", flag = false ];
N8 [ label = "void PrintStream.println(String)", flag = false ];
N8 -> N2 ;
N8 [ label = "void Test.main(String[])", flag = true ];
N3 [ label = "void Test.complexityDecrease(int)", flag = true ];
N3 -> N5 ;
N3 [ label = "void Unchanged.orderN(int)", flag = false ];
N3 -> N7 ;
N3 -> N6 ;
N3 -> N4 ;
}

@ -1,2 +1,2 @@
build_systems/codetoanalyze/objc_missing_fld/A.m, badOnlyOneNDA, 5, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure badOnlyOneNDA(),start of procedure predA(),start of procedure implOnlyFn:,return from a call to A.implOnlyFn:,start of procedure delegate,return from a call to A.delegate,Condition is true,return from a call to predA,Taking false branch]
build_systems/codetoanalyze/objc_missing_fld/B.m, badOnlyOneNDB, 5, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure badOnlyOneNDB(),start of procedure predB(),start of procedure implOnlyFn:,return from a call to A.implOnlyFn:,start of procedure delegate,return from a call to A.delegate,Condition is true,return from a call to predB,Taking false branch]
build_systems/codetoanalyze/objc_missing_fld/B.m, badOnlyOneNDB, 5, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure badOnlyOneNDB(),start of procedure predB(),Skipping implOnlyFn:: method has no implementation,start of procedure delegate,return from a call to A.delegate,Condition is true,return from a call to predB,Taking false branch]

Loading…
Cancel
Save