From 0097d8a5cb8a09bc91af2e482757d68f66beb704 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Thu, 4 May 2017 12:47:06 -0700 Subject: [PATCH] [infer] First step to the biabduction analysis using the checkers framework Summary: This gives the option to run the biabduction analysis together with the other Clang-based checkers with the command: infer -a checkers --biabduction -- ... The filtering does not work yet because the filtering for the biabduction analysis matches the analyzer `Infer`, and does not filter much when the analyzer is `Checkers`, which is the case here. Reviewed By: sblackshear Differential Revision: D4773834 fbshipit-source-id: 16300cc --- infer/src/backend/callbacks.ml | 11 ++++- infer/src/backend/interproc.ml | 42 +++++++++++-------- infer/src/backend/interproc.mli | 3 ++ infer/src/base/Config.ml | 5 +++ infer/src/base/Config.mli | 1 + infer/src/checkers/registerCheckers.ml | 1 + .../codetoanalyze/c/biabduction/Makefile | 18 ++++++++ .../codetoanalyze/c/biabduction/example.c | 12 ++++++ .../codetoanalyze/c/biabduction/issues.exp | 1 + 9 files changed, 76 insertions(+), 18 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/biabduction/Makefile create mode 100644 infer/tests/codetoanalyze/c/biabduction/example.c create mode 100644 infer/tests/codetoanalyze/c/biabduction/issues.exp diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 77fcd7a5b..d26f06c34 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -8,6 +8,7 @@ *) open! IStd +open! PVariant module L = Logging @@ -134,9 +135,17 @@ let iterate_callbacks call_graph exe_env = let proc_name = Procdesc.get_proc_name proc_desc in iterate_procedure_callbacks exe_env summary proc_name in + let get_proc_desc proc_name = + match Exe_env.get_proc_desc exe_env proc_name with + | Some pdesc -> Some pdesc + | None when Config.dynamic_dispatch = `Lazy -> + Option.bind (Specs.get_summary proc_name) + (fun summary -> summary.Specs.proc_desc_option) + | None -> None in + let callbacks = { Ondemand.analyze_ondemand; - get_proc_desc = Exe_env.get_proc_desc exe_env + get_proc_desc; } in (* Create and register on-demand analysis callback *) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index c0cba0097..1e67e65a8 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1394,6 +1394,29 @@ let interprocedural_algorithm_closures ~prepare_proc exe_env : Tasks.closure lis fun () -> process_one_proc proc_name in List.map ~f:create_closure procs_to_analyze +let analyze_procedure_aux cg_opt tenv proc_desc = + let proc_name = Procdesc.get_proc_name proc_desc in + if not (Procdesc.did_preanalysis proc_desc) + then + begin + Preanal.do_liveness proc_desc tenv; + Preanal.do_abstraction proc_desc; + Option.iter cg_opt ~f:(fun cg -> Preanal.do_dynamic_dispatch proc_desc cg tenv); + end; + let summaryfp = + Config.run_in_footprint_mode (analyze_proc tenv) proc_desc in + Specs.add_summary proc_name summaryfp; + perform_transition proc_desc tenv proc_name; + let summaryre = + Config.run_in_re_execution_mode (analyze_proc tenv) proc_desc in + Specs.add_summary proc_name summaryre; + summaryre + +let analyze_procedure { Callbacks.summary; proc_desc; tenv } : Specs.summary = + let proc_name = Procdesc.get_proc_name proc_desc in + Specs.add_summary proc_name summary; + ignore (analyze_procedure_aux None tenv proc_desc); + Specs.get_summary_unsafe __FILE__ proc_name (** Create closures to perform the analysis of an exe_env *) let do_analysis_closures exe_env : Tasks.closure list = @@ -1432,23 +1455,8 @@ let do_analysis_closures exe_env : Tasks.closure list = let analyze_ondemand _ proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in let tenv = Exe_env.get_tenv exe_env proc_name in - if not (Procdesc.did_preanalysis proc_desc) - then - begin - Preanal.do_liveness proc_desc tenv; - Preanal.do_abstraction proc_desc; - Preanal.do_dynamic_dispatch proc_desc (Exe_env.get_cg exe_env) tenv - end; - let summaryfp = - Config.run_in_footprint_mode (analyze_proc tenv) proc_desc in - Specs.add_summary proc_name summaryfp; - - perform_transition proc_desc tenv proc_name; - - let summaryre = - Config.run_in_re_execution_mode (analyze_proc tenv) proc_desc in - Specs.add_summary proc_name summaryre; - summaryre in + let cg = Exe_env.get_cg exe_env in + analyze_procedure_aux (Some cg) tenv proc_desc in { Ondemand.analyze_ondemand; get_proc_desc; diff --git a/infer/src/backend/interproc.mli b/infer/src/backend/interproc.mli index e1fc2cf29..ce1c3b83b 100644 --- a/infer/src/backend/interproc.mli +++ b/infer/src/backend/interproc.mli @@ -12,6 +12,9 @@ open! IStd (** Interprocedural Analysis *) +(** Run the biabduction analysis on the given procedure *) +val analyze_procedure : Callbacks.proc_callback_t + (** Create closures to perform the analysis of an exe_env *) val do_analysis_closures : Exe_env.t -> Tasks.closure list diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index bc2cdb932..4eccf2f4b 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -589,6 +589,10 @@ and changed_files_index = "Specify the file containing the list of source files from which reactive analysis should \ start. Source files should be specified relative to project root or be absolute" +let biabduction = + CLOpt.mk_bool ~long:"biabduction" + "Activate the separation logic based bi-abduction analysis using the checkers framework" + and bufferoverrun, checkers, checkers_repeated_calls, crashcontext, eradicate, quandary, siof, threadsafety = let checkers = @@ -1620,6 +1624,7 @@ and angelic_execution = !angelic_execution and annotation_reachability = !annotation_reachability and array_level = !array_level and ast_file = !ast_file +and biabduction = !biabduction and blacklist = !blacklist and bootclasspath = !bootclasspath and bo_debug = !bo_debug diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 26b7c226f..c502d2043 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -172,6 +172,7 @@ val angelic_execution : bool val annotation_reachability : Yojson.Basic.json val array_level : int val ast_file : string option +val biabduction : bool val blacklist : string option val bootclasspath : string option val bo_debug : int diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index c06949219..81def7dbd 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -54,6 +54,7 @@ let active_procedure_checkers () = Siof.checker, Config.siof; ThreadSafety.analyze_procedure, Config.threadsafety; BufferOverrunChecker.checker, Config.bufferoverrun; + Interproc.analyze_procedure, Config.biabduction; ] in List.map ~f:(fun (x, y) -> (x, y, Some Config.Clang)) l in diff --git a/infer/tests/codetoanalyze/c/biabduction/Makefile b/infer/tests/codetoanalyze/c/biabduction/Makefile new file mode 100644 index 000000000..cb42c7093 --- /dev/null +++ b/infer/tests/codetoanalyze/c/biabduction/Makefile @@ -0,0 +1,18 @@ +# Copyright (c) 2016 - present Facebook, Inc. +# All rights reserved. +# +# This source code is licensed under the BSD style license found in the +# LICENSE file in the root directory of this source tree. An additional grant +# of patent rights can be found in the PATENTS file in the same directory. + +TESTS_DIR = ../../.. + +ANALYZER = checkers +CLANG_OPTIONS = -c +INFER_OPTIONS = --biabduction --project-root $(TESTS_DIR) + +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard *.c) + +include $(TESTS_DIR)/clang.make diff --git a/infer/tests/codetoanalyze/c/biabduction/example.c b/infer/tests/codetoanalyze/c/biabduction/example.c new file mode 100644 index 000000000..66dd7e5ea --- /dev/null +++ b/infer/tests/codetoanalyze/c/biabduction/example.c @@ -0,0 +1,12 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +void foo() { + int* p = 0; + *p = 42; +} diff --git a/infer/tests/codetoanalyze/c/biabduction/issues.exp b/infer/tests/codetoanalyze/c/biabduction/issues.exp new file mode 100644 index 000000000..2dd25ef22 --- /dev/null +++ b/infer/tests/codetoanalyze/c/biabduction/issues.exp @@ -0,0 +1 @@ +codetoanalyze/c/biabduction/example.c, foo, 2, NULL_DEREFERENCE, [start of procedure foo()]