Output the callee sumaries of -a crashcontext to per-method files.

Reviewed By: sblackshear

Differential Revision: D3612488

fbshipit-source-id: a068803

infer/src/checkers/BoundedCallTree.ml

@@ -27,8 +27,34 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module Domain = Domain
   type extras = Stacktrace.t
 
+  let json_of_summary caller astate loc loc_type =
+    let procs = Domain.elements astate in
+    let json = `Assoc [
+        ("caller", `String (Procname.to_string caller));
+        ("location", `Assoc [
+            ("type", `String loc_type);
+            ("file", `String (DB.source_file_to_string loc.Location.file));
+            ("line", `Int loc.Location.line);
+          ]);
+        ("callees", `List (IList.map
+                             (fun pn -> `String (Procname.to_string pn))
+                             procs))
+      ] in
+    json
+
+  let output_summary caller astate loc loc_type =
+    let json = json_of_summary caller astate loc loc_type in
+    let dir = Filename.concat Config.results_dir "crashcontext" in
+    let suffix = F.sprintf "%s_%d" loc_type loc.Location.line in
+    let fname = F.sprintf "%s.%s.json"
+        (Procname.to_filename caller)
+        suffix in
+    let fpath = Filename.concat dir fname in
+    DB.create_dir dir;
+    Utils.write_json_to_file fpath json
+
   let exec_instr astate proc_data _ = function
-    | Sil.Call (_, Const (Const.Cfun pn), _, _, _) ->
+    | Sil.Call (_, Const (Const.Cfun pn), _, loc, _) ->
         (** TODO: Match class. *)
         let caller = Cfg.Procdesc.get_proc_name proc_data.ProcData.pdesc in
         let matches_proc frame =
@@ -37,8 +63,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             matches_proc
             proc_data.ProcData.extras.Stacktrace.frames in
         if proc_in_trace then begin
-          L.stderr "Detected method: %a@." Procname.pp pn;
+          let frame = IList.find
-          Domain.add pn astate
+              matches_proc
+              proc_data.ProcData.extras.Stacktrace.frames in
+          let new_astate = Domain.add pn astate in
+          if Stacktrace.frame_matches_location frame loc then begin
+            output_summary caller new_astate loc "call_site"
+          end;
+          new_astate
         end
         else
           astate
@@ -68,8 +100,10 @@ let load_trace () =
    * call Stacktrace.of_json_file  *)
   let filename = match Config.stacktrace with
     | None -> failwith "Missing command line option: '--stacktrace stack.json' \
-                        must be used when running '-a crashcontext'. This option expects a JSON \
+                        must be used when running '-a crashcontext'. This \
-                        formated stack trace." (** TODO: add example file in tests/... *)
+                        option expects a JSON formated stack trace. See \
+                        tests/codetoanalyze/java/crashcontext/*.json for \
+                        examples of the expected format."
     | Some fname -> fname in
   let new_trace = Stacktrace.of_json_file filename in
   trace_ref := Some new_trace;

infer/src/harness/stacktrace.ml

@@ -28,6 +28,11 @@ let make exception_name frames = { exception_name; frames; }
 let make_frame class_str method_str file_str line_num =
   { class_str; method_str; file_str; line_num; }
 
+let frame_matches_location frame_obj loc =
+  let lfname = DB.source_file_to_string loc.Location.file in
+  Utils.string_is_suffix frame_obj.file_str lfname &&
+  frame_obj.line_num = loc.Location.line
+
 let parse_stack_frame frame_str =
   (* separate the qualified method name and the parenthesized text/line number*)
   ignore(Str.string_match (Str.regexp "\t*at \\(.*\\)(\\(.*\\))") frame_str 0);

infer/src/harness/stacktrace.mli

@@ -25,6 +25,8 @@ val make : string -> frame list -> t
 
 val make_frame : string -> string -> string -> int -> frame
 
+val frame_matches_location : frame -> Location.t -> bool
+
 val of_string : string -> t
 
 val of_json_file : string -> t

infer/tests/codetoanalyze/java/crashcontext/BranchingCallsExample.java

@@ -0,0 +1,37 @@
+/*
+ * 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.
+ */
+
+package codetoanalyze.java.crashcontext;
+
+public class BranchingCallsExample {
+
+  public static void pre_bar() {
+    System.out.println("This runs before the crash.");
+  }
+
+  public static void post_bar() {
+    System.out.println("This doesn't.");
+  }
+
+  public static void bar() {
+    String s = null;
+    s.toString();
+  }
+
+  public static void foo() {
+    pre_bar();
+    bar();
+    post_bar();
+  }
+
+  public static void main(String[] args) {
+    foo();
+  }
+
+}

infer/tests/codetoanalyze/java/crashcontext/BranchingCallsExample.stacktrace.json

@@ -0,0 +1 @@
+{"exception_type": "java.lang.NullPointerException", "stack_trace": ["at codetoanalyze.java.crashcontext.BranchingCallsExample.bar(BranchingCallsExample.java:24)","at codetoanalyze.java.crashcontext.BranchingCallsExample.foo(BranchingCallsExample.java:29)","at codetoanalyze.java.crashcontext.BranchingCallsExample.main(BranchingCallsExample.java:34)",""], "exception_message": "", "normvector_stack": ["codetoanalyze.java.crashcontext.BranchingCallsExample.bar","codetoanalyze.java.crashcontext.BranchingCallsExample.foo","endtoend.java.crashcontext.BranchingCallsExample.main"]}

infer/tests/codetoanalyze/java/crashcontext/MultiStackFrameCrashExample.java

@@ -0,0 +1,27 @@
+/*
+ * 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.
+ */
+
+package codetoanalyze.java.crashcontext;
+
+public class MultiStackFrameCrashExample {
+
+  public static void bar() {
+    String s = null;
+    s.toString();
+  }
+
+  public static void foo() {
+    bar();
+  }
+
+  public static void main(String[] args) {
+    foo();
+  }
+
+}

infer/tests/codetoanalyze/java/crashcontext/MultiStackFrameCrashExample.stacktrace.json

@@ -0,0 +1 @@
+{"exception_type": "java.lang.NullPointerException", "stack_trace": ["at codetoanalyze.java.crashcontext.MultiStackFrameCrashExample.bar(MultiStackFrameCrashExample.java:16)","at codetoanalyze.java.crashcontext.MultiStackFrameCrashExample.foo(MultiStackFrameCrashExample.java:20)","at codetoanalyze.java.crashcontext.MultiStackFrameCrashExample.main(MultiStackFrameCrashExample.java:24)",""], "exception_message": "", "normvector_stack": ["codetoanalyze.java.crashcontext.MultiStackFrameCrashExample.bar","codetoanalyze.java.crashcontext.MultiStackFrameCrashExample.foo","endtoend.java.crashcontext.MultiStackFrameCrashExample.main"]}