[infer] Add summary-lookup option in infer-explore

Summary:
Problem: `infer report <specs file name>` is called manually sometimes to see analysis results in CLI. However, giving the specs file name is sometimes annoying, because the specs file name may be quite long and include special characters sometimes.

This diff introduces `--procedures-summary` to lookup the summaries interactively in `infer explore`.

example1: There are 8 procedures that include "max" in their names, then I selected one of them by entering a number.

```
$ infer explore --procedures --procedures-filter '.*max.*' --procedures-summary
0: minmax_div_const2_Bad_FN
1: minmax_div_const_Good
2: use_int64_max_Bad
3: use_uint64_max_Good
4: use_int64_max_Good
5: minmax_div_const_Bad
6: minmax_div_const2_Good
7: use_uint64_max_Bad
Select one number (type 'a' for selecting all, 'q' for quit): 2
void use_int64_max_Bad()
Analyzed
ERRORS: BUFFER_OVERRUN_L1
WARNINGS:
FAILURE:NONE SYMOPS:0
BufferOverrunAnalysis: StackLocs: { } MemPure: { } Alias: { ret= }

BufferOverrunChecker: Safety conditions:
                      {  }

```

example2: If there is only one specs file that satisfies the given filter, it reports the summary of that procedure without an interaction.

```
$ infer explore --procedures --procedures-filter '.*add_in_loop_ok.*' --procedures-summary
Selected proc name: void ArrayListTest.add_in_loop_ok()
void void ArrayListTest.add_in_loop_ok()(ArrayListTest* this)
Analyzed
ERRORS:
WARNINGS:
FAILURE:NONE SYMOPS:0
BufferOverrunAnalysis: StackLocs: { } MemPure: { } Alias:
{ i=size(__new-390022197-0-1.elements), ret= }
LatestPrune: latest { i -> (5, { }, { }) by ((5, { }, { }) >= (5, { }, { })),
                      __new-390022197-0-1.elements -> (⊥, { }, { __new-390022197-1-1 -> length : 5 }) by ((5, { }, { }) >= (5, { }, { })) }
BufferOverrunChecker: Safety conditions:
                      {  }
```

Reviewed By: jvillard

Differential Revision: D20284052

fbshipit-source-id: 2131339f1

infer/man/man1/infer-explore.txt

@@ -85,6 +85,10 @@ EXPLORE PROCEDURES
            Deactivates: Include the source file in which the procedure
            definition or declaration was found in the output of --procedures
            (Conversely: --procedures-source-file)
+
+       --procedures-summary
+           Activates: Print the summaries of each procedure in the output of
+           --procedures (Conversely: --no-procedures-summary)
 EXPLORE SOURCE FILES
        --source-files
            Activates: Print source files discovered by infer (Conversely:

infer/man/man1/infer-full.txt

@@ -875,6 +875,10 @@ OPTIONS
            definition or declaration was found in the output of --procedures
            (Conversely: --procedures-source-file)           See also infer-explore(1).
 
+       --procedures-summary
+           Activates: Print the summaries of each procedure in the output of
+           --procedures (Conversely: --no-procedures-summary)           See also infer-explore(1).
+
        --no-progress-bar,-P
            Deactivates: Show a progress bar (Conversely: --progress-bar | -p)       
     See also infer-run(1).

infer/man/man1/infer.txt

@@ -875,6 +875,10 @@ OPTIONS
            definition or declaration was found in the output of --procedures
            (Conversely: --procedures-source-file)           See also infer-explore(1).
 
+       --procedures-summary
+           Activates: Print the summaries of each procedure in the output of
+           --procedures (Conversely: --no-procedures-summary)           See also infer-explore(1).
+
        --no-progress-bar,-P
            Deactivates: Show a progress bar (Conversely: --progress-bar | -p)       
     See also infer-run(1).

infer/src/backend/Procedures.ml

@@ -17,6 +17,39 @@ let get_all ~filter () =
       if filter source_file proc_name then proc_name :: rev_results else rev_results )
 
 
+let select_proc_names_interactive ~filter =
+  let proc_names = get_all ~filter () |> List.rev in
+  match proc_names with
+  | [] ->
+      print_endline "No procedures found" ;
+      None
+  | [proc_name] ->
+      Format.printf "Selected proc name: %a@\n" Procname.pp proc_name ;
+      Format.print_flush () ;
+      Some proc_names
+  | _ ->
+      let proc_names_array = List.to_array proc_names in
+      Array.iteri proc_names_array ~f:(fun i proc_name ->
+          Format.printf "%d: %a@\n" i Procname.pp proc_name ) ;
+      Format.print_flush () ;
+      let rec ask_user_input () =
+        print_string "Select one number (type 'a' for selecting all, 'q' for quit): " ;
+        Out_channel.(flush stdout) ;
+        let input = String.strip In_channel.(input_line_exn stdin) in
+        if String.equal (String.lowercase input) "a" then Some proc_names
+        else if String.equal (String.lowercase input) "q" then (
+          print_endline "Quit interactive mode" ;
+          None )
+        else
+          match int_of_string_opt input with
+          | Some n when 0 <= n && n < Array.length proc_names_array ->
+              Some [proc_names_array.(n)]
+          | _ ->
+              print_endline "Invalid input" ; ask_user_input ()
+      in
+      ask_user_input ()
+
+
 let pp_all ~filter ~proc_name:proc_name_cond ~attr_kind ~source_file:source_file_cond
     ~proc_attributes fmt () =
   let db = ResultsDatabase.get_database () in

infer/src/backend/Procedures.mli

@@ -18,3 +18,5 @@ val pp_all :
   -> Format.formatter
   -> unit
   -> unit
+
+val select_proc_names_interactive : filter:Filtering.procedures_filter -> Procname.t list option

infer/src/base/Config.ml

@@ -1941,6 +1941,12 @@ and procedures_source_file =
      output of $(b,--procedures)"
 
 
+and procedures_summary =
+  CLOpt.mk_bool ~long:"procedures-summary" ~default:false
+    ~in_help:InferCommand.[(Explore, manual_explore_procedures)]
+    "Print the summaries of each procedure in the output of $(b,--procedures)"
+
+
 and process_clang_ast =
   CLOpt.mk_bool ~long:"process-clang-ast" ~default:false
     "process the ast to emit some info about the file (Not available for Java)"
@@ -3087,6 +3093,8 @@ and[@warning "-32"] procedures_per_process = !procedures_per_process
 
 and procedures_source_file = !procedures_source_file
 
+and procedures_summary = !procedures_summary
+
 and process_clang_ast = !process_clang_ast
 
 and progress_bar =

infer/src/base/Config.mli

@@ -547,6 +547,8 @@ val procedures_name : bool
 
 val procedures_source_file : bool
 
+val procedures_summary : bool
+
 val process_clang_ast : bool
 
 val clang_frontend_action_string : string

infer/src/infer.ml

@@ -180,13 +180,24 @@ let () =
     | Explore -> (
       match (Config.procedures, Config.source_files) with
       | true, false ->
-          L.result "%a"
-            Config.(
-              Procedures.pp_all
-                ~filter:(Lazy.force Filtering.procedures_filter)
-                ~proc_name:procedures_name ~attr_kind:procedures_definedness
-                ~source_file:procedures_source_file ~proc_attributes:procedures_attributes)
-            ()
+          let filter = Lazy.force Filtering.procedures_filter in
+          if Config.procedures_summary then
+            let pp_summary fmt proc_name =
+              match Summary.OnDisk.get proc_name with
+              | None ->
+                  Format.fprintf fmt "No summary found: %a@\n" Procname.pp proc_name
+              | Some summary ->
+                  Summary.pp_text fmt summary
+            in
+            Option.iter (Procedures.select_proc_names_interactive ~filter) ~f:(fun proc_names ->
+                L.result "%a" (fun fmt () -> List.iter proc_names ~f:(pp_summary fmt)) () )
+          else
+            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)
+              ()
       | false, true ->
           let filter = Lazy.force Filtering.source_files_filter in
           L.result "%a"