Add initial version (k=1, undirected) of the bounder calltree analysis checker for the Semantic Blame project

Reviewed By: sblackshear

Differential Revision: D3568420

fbshipit-source-id: cc58a93

infer/src/checkers/BoundedCallTree.ml

@@ -0,0 +1,50 @@
+(*
+ * 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.
+ *)
+
+open! Utils
+
+module F = Format
+module L = Logging
+
+(** find transitive procedure calls for each procedure *)
+
+module ProcnameSet = PrettyPrintable.MakePPSet(struct
+    type t = Procname.t
+    let compare = Procname.compare
+    let pp_element = Procname.pp
+  end)
+
+module Domain = AbstractDomain.FiniteSet(ProcnameSet)
+
+module TransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = Domain
+  type extras = ProcData.no_extras
+
+  let exec_instr astate _ _ = function
+    | Sil.Call (_, Const (Const.Cfun pn), _, _, _) ->
+        Domain.add pn astate
+    | Sil.Call _ ->
+        (** We currently ignore calls through function pointers in C and
+         * other potential special kinds of procedure calls to be added later,
+         * e.g. Java reflection. *)
+        astate
+    | Sil.Letderef _ | Set _ | Prune _ | Declare_locals _
+    | Stackop _ | Remove_temps _ | Abstract _ | Nullify _ ->
+        astate
+end
+
+module Analyzer =
+  AbstractInterpreter.Make
+    (ProcCfg.Exceptional)
+    (Scheduler.ReversePostorder)
+    (TransferFunctions)
+
+let checker { Callbacks.proc_desc; tenv; } =
+  ignore(Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv))

infer/src/checkers/registerCheckers.ml

@@ -39,6 +39,7 @@ let active_procedure_checkers () =
         PrintfArgs.callback_printf_args, checkers_enabled;
         AnnotationReachability.Interprocedural.check_and_report, checkers_enabled;
         Checkers.callback_print_access_to_globals, false;
+        BoundedCallTree.checker, false;
       ] in
     IList.map (fun (x, y) -> (x, y, Some Config.Java)) l in
   let c_cpp_checkers =

infer/src/unit/BoundedCallTreeTests.ml

@@ -0,0 +1,52 @@
+(*
+ * 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.
+ *)
+
+open! Utils
+
+module F = Format
+
+module TestInterpreter = AnalyzerTester.Make
+    (ProcCfg.Exceptional)
+    (Scheduler.ReversePostorder)
+    (BoundedCallTree.TransferFunctions)
+
+let tests =
+  let open OUnit2 in
+  let open AnalyzerTester.StructuredSil in
+  let f_proc_name = Procname.from_string_c_fun "f" in
+  let g_proc_name = Procname.from_string_c_fun "g" in
+  let g_args = [((Sil.Const (Const.Cint (IntLit.one))), (Typ.Tint IInt))] in
+  let g_ret_ids = [(ident_of_str "r")] in
+  let test_list = [
+    "on_call_add_proc_name",
+    [
+      make_call ~procname:f_proc_name [] []; (* means f() *)
+      invariant "{ f }"
+    ];
+    "on_call_add_proc_name_w_args",
+    [
+      make_call ~procname:g_proc_name g_ret_ids g_args; (* means r = a.g(1) *)
+      invariant "{ g }"
+    ];
+    "handle_two_proc_calls",
+    [
+      make_call ~procname:f_proc_name [] [];
+      invariant "{ f }";
+      make_call ~procname:g_proc_name g_ret_ids g_args;
+      invariant "{ f, g }"
+    ];
+    "dont_record_procs_twice",
+    [
+      make_call ~procname:f_proc_name [] [];
+      invariant "{ f }";
+      make_call ~procname:f_proc_name [] [];
+      invariant "{ f }"
+    ];
+  ] |> TestInterpreter.create_tests ProcData.empty_extras in
+  "bounded_calltree_test_suite">:::test_list

infer/src/unit/inferunit.ml

@@ -22,6 +22,7 @@ let () =
     ProcCfgTests.tests;
     LivenessTests.tests;
     SchedulerTests.tests;
+    BoundedCallTreeTests.tests;
   ] in
   let test_suite = "all" >::: tests in
   OUnit2.run_test_tt_main test_suite