[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

@@ -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

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

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

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

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

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

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) []) )
 

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

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