From 0aeb33947a9a1da581ba6698a2065b76aaab20bc Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 28 Jul 2020 07:00:42 -0700 Subject: [PATCH] [debug] add --procedures-cfg Summary: New option for `infer debug` to dump individual procedures' CFG after the fact: ``` $ infer -o infer-out -- clang -c examples/hello.c $ infer debug --procedures --procedures-cfg test source_file: examples/hello.c attribute_kind: control-flow graph: '/home/jul/infer/infer-out/captured/hello.c.f19e4797ddf4b23fd1ce68a7e60f3b03/test.098f6bcd4621d373cade4e832627b4f6.dot' ``` Reviewed By: da319 Differential Revision: D22790593 fbshipit-source-id: 2fa2a6371 --- infer/man/man1/infer-debug.txt | 5 +++++ infer/man/man1/infer-full.txt | 6 ++++++ infer/man/man1/infer.txt | 6 ++++++ infer/src/IR/DotCfg.ml | 3 ++- infer/src/IR/DotCfg.mli | 5 +++-- infer/src/backend/Procedures.ml | 17 ++++++++++++++--- infer/src/backend/Procedures.mli | 1 + infer/src/backend/ondemand.ml | 3 ++- infer/src/base/Config.ml | 11 +++++++++++ infer/src/base/Config.mli | 2 ++ infer/src/infer.ml | 3 ++- 11 files changed, 54 insertions(+), 8 deletions(-) diff --git a/infer/man/man1/infer-debug.txt b/infer/man/man1/infer-debug.txt index 381849994..43c2deb0d 100644 --- a/infer/man/man1/infer-debug.txt +++ b/infer/man/man1/infer-debug.txt @@ -46,6 +46,11 @@ DEBUG PROCEDURES Activates: Print the attributes of each procedure in the output of --procedures (Conversely: --no-procedures-attributes) + --procedures-cfg + Activates: Output a dotty file in + infer-out/captured//.dot for each procedure + in the output of --procedures (Conversely: --no-procedures-cfg) + --no-procedures-definedness Deactivates: Include procedures definedness in the output of --procedures, i.e. whether the procedure definition was found, or diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 2471ca821..668de9551 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -824,6 +824,12 @@ OPTIONS --procedures (Conversely: --no-procedures-attributes) See also infer-debug(1). + --procedures-cfg + Activates: Output a dotty file in + infer-out/captured//.dot for each procedure + in the output of --procedures (Conversely: --no-procedures-cfg) + See also infer-debug(1). + --no-procedures-definedness Deactivates: Include procedures definedness in the output of --procedures, i.e. whether the procedure definition was found, or diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 56d2b2b13..d12f6c0c1 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -824,6 +824,12 @@ OPTIONS --procedures (Conversely: --no-procedures-attributes) See also infer-debug(1). + --procedures-cfg + Activates: Output a dotty file in + infer-out/captured//.dot for each procedure + in the output of --procedures (Conversely: --no-procedures-cfg) + See also infer-debug(1). + --no-procedures-definedness Deactivates: Include procedures definedness in the output of --procedures, i.e. whether the procedure definition was found, or diff --git a/infer/src/IR/DotCfg.ml b/infer/src/IR/DotCfg.ml index 43269fcd1..160620092 100644 --- a/infer/src/IR/DotCfg.ml +++ b/infer/src/IR/DotCfg.ml @@ -141,4 +141,5 @@ let emit_proc_desc source proc_desc = in DB.filename_to_string db_name ^ ".dot" in - with_dot_file filename ~pp:(fun fmt -> print_pdesc source fmt proc_desc) + with_dot_file filename ~pp:(fun fmt -> print_pdesc source fmt proc_desc) ; + filename diff --git a/infer/src/IR/DotCfg.mli b/infer/src/IR/DotCfg.mli index 06d7248a7..f2bda9cb9 100644 --- a/infer/src/IR/DotCfg.mli +++ b/infer/src/IR/DotCfg.mli @@ -11,5 +11,6 @@ open! IStd val emit_frontend_cfg : SourceFile.t -> Cfg.t -> unit (** emit the given {!Cfg.t} in the "dot" format to a file determined by {!Config} values *) -val emit_proc_desc : SourceFile.t -> Procdesc.t -> unit -(** emit the given {!Procdesc.t} in the "dot" format to a file in infer-out/captured/ *) +val emit_proc_desc : SourceFile.t -> Procdesc.t -> string +(** emit the given {!Procdesc.t} in the "dot" format to a file in infer-out/captured/ and return the + path to that file *) diff --git a/infer/src/backend/Procedures.ml b/infer/src/backend/Procedures.ml index bdb093a0c..636746806 100644 --- a/infer/src/backend/Procedures.ml +++ b/infer/src/backend/Procedures.ml @@ -52,7 +52,7 @@ let select_proc_names_interactive ~filter = let pp_all ~filter ~proc_name:proc_name_cond ~attr_kind ~source_file:source_file_cond - ~proc_attributes fmt () = + ~proc_attributes ~proc_cfg fmt () = let db = ResultsDatabase.get_database () in let pp_if ?(new_line = false) condition title pp fmt x = if condition then ( @@ -66,7 +66,15 @@ let pp_all ~filter ~proc_name:proc_name_cond ~attr_kind ~source_file:source_file in let pp_row stmt fmt source_file proc_name = let[@warning "-8"] (Sqlite3.Data.TEXT proc_name_hum) = Sqlite3.column stmt 1 in - Format.fprintf fmt "@[%s@,%a%a%a%a@]@\n" proc_name_hum + let dump_cfg fmt cfg_opt = + match cfg_opt with + | None -> + F.pp_print_string fmt "not found" + | Some cfg -> + let path = DotCfg.emit_proc_desc source_file cfg in + F.fprintf fmt "'%s'" path + in + Format.fprintf fmt "@[%s@,%a%a%a%a%a@]@\n" proc_name_hum (pp_if source_file_cond "source_file" SourceFile.pp) source_file (pp_if proc_name_cond "proc_name" Procname.pp) @@ -77,11 +85,14 @@ let pp_all ~filter ~proc_name:proc_name_cond ~attr_kind ~source_file:source_file (pp_column_if stmt ~new_line:true proc_attributes "attributes" ProcAttributes.SQLite.deserialize ProcAttributes.pp) 4 + (pp_column_if stmt ~new_line:false proc_cfg "control-flow graph" Procdesc.SQLite.deserialize + dump_cfg) + 5 in (* we could also register this statement but it's typically used only once per run so just prepare it inside the function *) Sqlite3.prepare db - "SELECT proc_name, proc_name_hum, attr_kind, source_file, proc_attributes FROM procedures" + "SELECT proc_name, proc_name_hum, attr_kind, source_file, proc_attributes, cfg FROM procedures" |> Container.iter ~fold:(SqliteUtils.result_fold_rows db ~log:"print all procedures") ~f:(fun stmt -> let proc_name = Sqlite3.column stmt 0 |> Procname.SQLite.deserialize in diff --git a/infer/src/backend/Procedures.mli b/infer/src/backend/Procedures.mli index e0c8c47fa..8169fe068 100644 --- a/infer/src/backend/Procedures.mli +++ b/infer/src/backend/Procedures.mli @@ -15,6 +15,7 @@ val pp_all : -> attr_kind:bool -> source_file:bool -> proc_attributes:bool + -> proc_cfg:bool -> Format.formatter -> unit -> unit diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 4ebcc803d..5d708c862 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -177,7 +177,8 @@ let run_proc_analysis ~caller_pdesc callee_pdesc = incr nesting ; Preanal.do_preanalysis (Option.value_exn !exe_env_ref) callee_pdesc ; if Config.debug_mode then - DotCfg.emit_proc_desc (Procdesc.get_attributes callee_pdesc).translation_unit callee_pdesc ; + DotCfg.emit_proc_desc (Procdesc.get_attributes callee_pdesc).translation_unit callee_pdesc + |> ignore ; let initial_callee_summary = Summary.OnDisk.reset callee_pdesc in add_active callee_pname ; initial_callee_summary diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 174bf2740..941746540 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1724,6 +1724,15 @@ and procedures_attributes = "Print the attributes of each procedure in the output of $(b,--procedures)" +and procedures_cfg = + CLOpt.mk_bool ~long:"procedures-cfg" + ~in_help:InferCommand.[(Debug, manual_debug_procedures)] + (Printf.sprintf + "Output a dotty file in %s//.dot for each procedure in the output of \ + $(b,--procedures)" + (ResultsDirEntryName.get_path ~results_dir:"infer-out" Debug)) + + and procedures_definedness = CLOpt.mk_bool ~long:"procedures-definedness" ~default:true ~in_help:InferCommand.[(Debug, manual_debug_procedures)] @@ -2924,6 +2933,8 @@ and procedures = !procedures and procedures_attributes = !procedures_attributes +and procedures_cfg = !procedures_cfg + and procedures_definedness = !procedures_definedness and procedures_filter = !procedures_filter diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 20e371137..4ff95491d 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -425,6 +425,8 @@ val procedures : bool val procedures_attributes : bool +val procedures_cfg : bool + val procedures_definedness : bool val procedures_filter : string option diff --git a/infer/src/infer.ml b/infer/src/infer.ml index 567b781c9..6c604aec8 100644 --- a/infer/src/infer.ml +++ b/infer/src/infer.ml @@ -237,7 +237,8 @@ let () = L.result "%a" Config.( Procedures.pp_all ~filter ~proc_name:procedures_name ~attr_kind:procedures_definedness - ~source_file:procedures_source_file ~proc_attributes:procedures_attributes) + ~source_file:procedures_source_file ~proc_attributes:procedures_attributes + ~proc_cfg:procedures_cfg) () ) ; if Config.source_files then ( let filter = Lazy.force Filtering.source_files_filter in