From b9a5a3b5ade912303aa9710eb3baffff050d3e65 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A1zaro=20Clapp=20Jim=C3=A9nez=20Labora?=
 <lazaroclapp@fb.com>
Date: Fri, 15 Jul 2016 18:53:27 -0700
Subject: [PATCH] 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  | 50 +++++++++++++++++++++++++
 infer/src/checkers/registerCheckers.ml |  1 +
 infer/src/unit/BoundedCallTreeTests.ml | 52 ++++++++++++++++++++++++++
 infer/src/unit/inferunit.ml            |  1 +
 4 files changed, 104 insertions(+)
 create mode 100644 infer/src/checkers/BoundedCallTree.ml
 create mode 100644 infer/src/unit/BoundedCallTreeTests.ml

diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml
new file mode 100644
index 000000000..bb0bfea71
--- /dev/null
+++ b/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))
diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml
index 269e9a5be..66618e28b 100644
--- a/infer/src/checkers/registerCheckers.ml
+++ b/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 =
diff --git a/infer/src/unit/BoundedCallTreeTests.ml b/infer/src/unit/BoundedCallTreeTests.ml
new file mode 100644
index 000000000..291a11a30
--- /dev/null
+++ b/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
diff --git a/infer/src/unit/inferunit.ml b/infer/src/unit/inferunit.ml
index a7a5d6405..957f31b84 100644
--- a/infer/src/unit/inferunit.ml
+++ b/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