From 3653c68c8ee4c1a946ec4a3bff321b337f19baaf Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 9 Mar 2020 02:04:44 -0700 Subject: [PATCH] [infer] Add summary-lookup option in infer-explore MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Summary: Problem: `infer report ` 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 | 4 ++++ infer/man/man1/infer-full.txt | 4 ++++ infer/man/man1/infer.txt | 4 ++++ infer/src/backend/Procedures.ml | 33 ++++++++++++++++++++++++++++++++ infer/src/backend/Procedures.mli | 2 ++ infer/src/base/Config.ml | 8 ++++++++ infer/src/base/Config.mli | 2 ++ infer/src/infer.ml | 25 +++++++++++++++++------- 8 files changed, 75 insertions(+), 7 deletions(-) diff --git a/infer/man/man1/infer-explore.txt b/infer/man/man1/infer-explore.txt index b10892640..2297b3984 100644 --- a/infer/man/man1/infer-explore.txt +++ b/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: diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index de83a1f25..f1b2e02bc 100644 --- a/infer/man/man1/infer-full.txt +++ b/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). diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 76848c533..72f290387 100644 --- a/infer/man/man1/infer.txt +++ b/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). diff --git a/infer/src/backend/Procedures.ml b/infer/src/backend/Procedures.ml index 900b87fd9..533ccca71 100644 --- a/infer/src/backend/Procedures.ml +++ b/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 diff --git a/infer/src/backend/Procedures.mli b/infer/src/backend/Procedures.mli index ab0869121..e0c8c47fa 100644 --- a/infer/src/backend/Procedures.mli +++ b/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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 41143d03b..43f6ca4aa 100644 --- a/infer/src/base/Config.ml +++ b/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 = diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 17e31a83e..60d1002af 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/infer.ml b/infer/src/infer.ml index b667544ff..ec66a8f6f 100644 --- a/infer/src/infer.ml +++ b/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"