From a0bae375db74e8d52f63e3d07d0051f57c364590 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 6 Feb 2019 09:41:03 -0800 Subject: [PATCH] [cfg] add option to print CFGs after the fact Summary: Add the `--source-files-cfg` option to emit CFGs as .dot files just as if one had run with `--debug` to begin with. The usual `--source-files-filter` applies. For example: ``` $ cd examples $ infer -- clang -c hello.c $ infer --continue -- javac Hello.java $ infer --continue -- make -C c_hello $ infer explore --source-files --source-files-cfg --source-files-filter ".*\.c$" hello.c c_hello/example.c CFGs written in /home/jul/infer.fb/examples/infer-out/captured/*/icfg.dot ``` Reviewed By: ezgicicek, mbouaziz Differential Revision: D13973062 fbshipit-source-id: 3077e8b91 --- infer/man/man1/infer-explore.txt | 5 +++++ infer/man/man1/infer-full.txt | 5 +++++ infer/man/man1/infer.txt | 5 +++++ infer/src/backend/Procedures.ml | 3 ++- infer/src/base/Config.ml | 11 +++++++++++ infer/src/base/Config.mli | 2 ++ infer/src/base/DB.ml | 4 ++-- infer/src/base/DB.mli | 2 +- infer/src/infer.ml | 21 +++++++++++++++++---- 9 files changed, 50 insertions(+), 8 deletions(-) diff --git a/infer/man/man1/infer-explore.txt b/infer/man/man1/infer-explore.txt index b93bb2f2f..1de4b0030 100644 --- a/infer/man/man1/infer-explore.txt +++ b/infer/man/man1/infer-explore.txt @@ -83,6 +83,11 @@ OPTIONS Activates: Print source files discovered by infer (Conversely: --no-source-files) + --source-files-cfg + Activates: Output a dotty file in infer-out/captured for each + source file in the output of --source-files (Conversely: + --no-source-files-cfg) + --source-files-filter filter With --source-files, only print source files matching the specified filter. The filter is a pattern that should match the diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 9087760ff..c46ef0c68 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -816,6 +816,11 @@ OPTIONS Activates: Print source files discovered by infer (Conversely: --no-source-files) See also infer-explore(1). + --source-files-cfg + Activates: Output a dotty file in infer-out/captured for each + source file in the output of --source-files (Conversely: + --no-source-files-cfg) See also infer-explore(1). + --source-files-filter filter With --source-files, only print source files matching the specified filter. The filter is a pattern that should match the diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index e2421ce77..99488474b 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -816,6 +816,11 @@ OPTIONS Activates: Print source files discovered by infer (Conversely: --no-source-files) See also infer-explore(1). + --source-files-cfg + Activates: Output a dotty file in infer-out/captured for each + source file in the output of --source-files (Conversely: + --no-source-files-cfg) See also infer-explore(1). + --source-files-filter filter With --source-files, only print source files matching the specified filter. The filter is a pattern that should match the diff --git a/infer/src/backend/Procedures.ml b/infer/src/backend/Procedures.ml index 135a1ea71..d6efab677 100644 --- a/infer/src/backend/Procedures.ml +++ b/infer/src/backend/Procedures.ml @@ -46,7 +46,8 @@ let pp_all ~filter ~proc_name:proc_name_cond ~attr_kind ~source_file:source_file 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 * FROM procedures" + Sqlite3.prepare db + "SELECT proc_name, proc_name_hum, attr_kind, source_file, proc_attributes FROM procedures" |> Container.iter ~fold:(SqliteUtils.result_fold_rows db ~log:"print all procedures") ~f:(fun stmt -> let proc_name = Sqlite3.column stmt 0 |> Typ.Procname.SQLite.deserialize in diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index afb6fe940..c636c954a 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1996,6 +1996,15 @@ and source_files = "Print source files discovered by infer" +and source_files_cfg = + CLOpt.mk_bool ~long:"source-files-cfg" + ~in_help:InferCommand.[(Explore, manual_generic)] + (Printf.sprintf + "Output a dotty file in infer-out/%s for each source file in the output of \ + $(b,--source-files)" + captured_dir_name) + + and source_files_filter = CLOpt.mk_string_opt ~long:"source-files-filter" ~meta:"filter" ~in_help:InferCommand.[(Explore, manual_generic)] @@ -2914,6 +2923,8 @@ and source_preview = !source_preview and source_files = !source_files +and source_files_cfg = !source_files_cfg + and source_files_filter = !source_files_filter and source_files_type_environment = !source_files_type_environment diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index c0857a7d2..b02ff569d 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -610,6 +610,8 @@ val skip_translation_headers : string list val source_files : bool +val source_files_cfg : bool + val source_files_filter : string option val source_files_type_environment : bool diff --git a/infer/src/base/DB.ml b/infer/src/base/DB.ml index 5b2a2e05e..02a495b75 100644 --- a/infer/src/base/DB.ml +++ b/infer/src/base/DB.ml @@ -129,9 +129,9 @@ module Results_dir = struct let specs_dir = path_to_filename Abs_root [Config.specs_dir_name] (** initialize the results directory *) - let init source = + let init ?(debug = false) source = if SourceFile.is_invalid source then L.(die InternalError) "Invalid source file passed" ; - if Config.html || Config.debug_mode || Config.frontend_tests then ( + if debug || Config.html || Config.debug_mode || Config.frontend_tests then ( Utils.create_dir (path_to_filename Abs_root [Config.captured_dir_name]) ; Utils.create_dir (path_to_filename (Abs_source_dir source) []) ) diff --git a/infer/src/base/DB.mli b/infer/src/base/DB.mli index b4bb8076f..f9db7caaa 100644 --- a/infer/src/base/DB.mli +++ b/infer/src/base/DB.mli @@ -45,7 +45,7 @@ module Results_dir : sig val specs_dir : filename (** directory of spec files *) - val init : SourceFile.t -> unit + val init : ?debug:bool -> SourceFile.t -> unit (** Initialize the results directory *) val clean_specs_dir : unit -> unit diff --git a/infer/src/infer.ml b/infer/src/infer.ml index 1b4bfd9e9..fbf1212fd 100644 --- a/infer/src/infer.ml +++ b/infer/src/infer.ml @@ -154,13 +154,26 @@ let () = ~source_file:procedures_source_file ~proc_attributes:procedures_attributes) () | Explore when Config.source_files -> + let filter = Lazy.force Filtering.source_files_filter in L.result "%a" - (SourceFiles.pp_all - ~filter:(Lazy.force Filtering.source_files_filter) - ~type_environment:Config.source_files_type_environment + (SourceFiles.pp_all ~filter ~type_environment:Config.source_files_type_environment ~procedure_names:Config.source_files_procedure_names ~freshly_captured:Config.source_files_freshly_captured) - () + () ; + if Config.source_files_cfg then ( + let source_files = SourceFiles.get_all ~filter () in + List.iter source_files ~f:(fun source_file -> + (* create directory in captured/ *) + DB.Results_dir.init ~debug:true source_file ; + (* collect the CFGs for all the procedures in [source_file] *) + let proc_names = SourceFiles.proc_names_of_source source_file in + let cfgs = Typ.Procname.Hash.create (List.length proc_names) in + List.iter proc_names ~f:(fun proc_name -> + Procdesc.load proc_name + |> Option.iter ~f:(fun cfg -> Typ.Procname.Hash.add cfgs proc_name cfg) ) ; + (* emit the dotty file in captured/... *) + Dotty.print_icfg_dotty source_file cfgs ) ; + L.result "CFGs written in %s/*/%s@." Config.captured_dir Config.dotty_output ) | Explore -> let if_some key opt args = match opt with None -> args | Some arg -> key :: string_of_int arg :: args