From cfd8a55f3ba2a993a9346fe6964b8ff50b9a0294 Mon Sep 17 00:00:00 2001 From: martinoluca Date: Wed, 29 Jul 2015 16:22:30 -0100 Subject: [PATCH] Add `-lib` flag to InferPrint to read specs files from multiple places Summary: While `-results_dir` is still the main place to look for specs files and to write reports, it's necessary to load specs from multiple folders because some build tools that run Infer with a target-level granularity may need to move specs files around in order to get complete reports, whereas with this change they just need to keep track of the `specs` folders generated for each target, and pass them through `-lib dir1 -lib dir2 ... -lib dirN` --- infer/bin/inferlib.py | 26 ++++++++++++++++++++++++++ infer/src/backend/inferprint.ml | 29 ++++++++++++++++------------- 2 files changed, 42 insertions(+), 13 deletions(-) diff --git a/infer/bin/inferlib.py b/infer/bin/inferlib.py index 358de54c2..acf6ae6ff 100644 --- a/infer/bin/inferlib.py +++ b/infer/bin/inferlib.py @@ -133,6 +133,14 @@ inferJ_group.add_argument('-nt', '--notest', action='store_true', dest='notest', help='Prints output of symbolic execution') +inferJ_group.add_argument('--specs-dir', + metavar='', + action='append', + dest='specs_dirs', + help='add dir to the list of directories to be ' + 'searched for spec files. Repeat the argument ' + 'in case multiple folders are needed') + def detect_javac(args): for index, arg in enumerate(args): if arg == 'javac': @@ -382,6 +390,17 @@ class Infer: self.stats = {'int': {}, 'float': {}} self.timing = {} + if self.args.specs_dirs: + # Each dir passed in input is prepended by '-lib'. + # Convert each path to absolute because when running from + # cluster Makefiles (multicore mode) InferAnalyze creates the wrong + # absolute path from within the multicore folder + self.args.specs_dirs = [item + for argument in + (['-lib', os.path.abspath(path)] for path in + self.args.specs_dirs) + for item in argument] + def clean_exit(self): if os.path.isdir(self.args.infer_out): @@ -472,6 +491,9 @@ class Infer: # '-notest', ] + if self.args.specs_dirs: + infer_options += self.args.specs_dirs + exit_status = os.EX_OK if self.args.buck: @@ -595,6 +617,10 @@ class Infer: '-procs', procs_report, '-analyzer', self.args.analyzer ] + + if self.args.specs_dirs: + infer_print_options += self.args.specs_dirs + exit_status = subprocess.check_call( infer_print_cmd + infer_print_options ) diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index c5aa3533d..09939635b 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -100,6 +100,7 @@ let arg_desc = "-procs", Arg.String (fun s -> procs_csv := create_outfile s), Some "procs.csv", "create file procs.csv containing statistics for each procedure in CSV format"; "-procs_xml", Arg.String (fun s -> procs_xml := create_outfile s), Some "procs.xml", "create file procs.xml containing statistics for each procedure in XML format"; "-results_dir", Arg.String (fun s -> results_dir_cmdline := true; Config.results_dir := s), Some "dir", "read all the .specs files in the results dir"; + "-lib", Arg.String (fun s -> Config.specs_library := filename_to_absolute s :: !Config.specs_library), Some "dir", "add dir to the list of directories to be searched for spec files"; "-q", Arg.Set quiet, None, "quiet: do not print specs on standard output"; "-save_results", Arg.String (fun s -> save_analysis_results := Some s), Some "file.iar", "save analysis results to Infer Analysis Results file file.iar"; "-unit_test", Arg.Set unit_test, None, "print unit test code"; @@ -139,18 +140,20 @@ let print_usage_exit err_s = Arg2.usage arg_desc usage; exit(1) - -(** return the list of the .specs files in the results dir, if it's defined *) -let results_dir_specsfiles () = match !results_dir_cmdline with - | false -> [] - | true -> - let specs_dir = DB.Results_dir.specs_dir () in - let specs_files_in_dir dir = - let is_specs_file fname = not (Sys.is_directory fname) && Filename.check_suffix fname ".specs" in - let all_filenames = Array.to_list (Sys.readdir dir) in - let all_filepaths = list_map (fun fname -> Filename.concat dir fname) all_filenames in - list_filter is_specs_file all_filepaths in - specs_files_in_dir (DB.filename_to_string specs_dir) +(** return the list of the .specs files in the results dir and libs, if they're defined *) +let load_specfiles () = + let specs_files_in_dir dir = + let is_specs_file fname = not (Sys.is_directory fname) && Filename.check_suffix fname ".specs" in + let all_filenames = Array.to_list (Sys.readdir dir) in + let all_filepaths = list_map (fun fname -> Filename.concat dir fname) all_filenames in + list_filter is_specs_file all_filepaths in + let specs_dirs = + if !results_dir_cmdline then + let result_specs_dir = DB.filename_to_string (DB.Results_dir.specs_dir ()) in + result_specs_dir :: !Config.specs_library + else + !Config.specs_library in + list_flatten (list_map specs_files_in_dir specs_dirs) (** Create and initialize latex file *) let begin_latex_file fmt = @@ -872,7 +875,7 @@ module AnalysisResults = struct let all_files = Array.to_list arr in list_filter (fun fname -> (Filename.check_suffix fname ".specs")) all_files end - else !args) (results_dir_specsfiles ()) + else !args) (load_specfiles ()) (** apply [f] to [arg] with the gc compaction disabled during the execution *) let apply_without_gc f arg =