[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

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

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)
+      let cg = Exe_env.get_cg exe_env in
-      then
+      analyze_procedure_aux (Some cg) tenv proc_desc in
-        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
     {
       Ondemand.analyze_ondemand;
       get_proc_desc;

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
 

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

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

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
 

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

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;
+}

infer/tests/codetoanalyze/c/biabduction/issues.exp

@@ -0,0 +1 @@
+codetoanalyze/c/biabduction/example.c, foo, 2, NULL_DEREFERENCE, [start of procedure foo()]