diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml index c66e03534..9e24c656f 100644 --- a/infer/src/checkers/BoundedCallTree.ml +++ b/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; - Domain.add pn astate + let frame = IList.find + 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 \ - formated stack trace." (** TODO: add example file in tests/... *) + must be used when running '-a crashcontext'. This \ + 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; diff --git a/infer/src/harness/stacktrace.ml b/infer/src/harness/stacktrace.ml index 4fdfd95fd..a0571c8c7 100644 --- a/infer/src/harness/stacktrace.ml +++ b/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); diff --git a/infer/src/harness/stacktrace.mli b/infer/src/harness/stacktrace.mli index 511b818ad..71ccbb439 100644 --- a/infer/src/harness/stacktrace.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/java/crashcontext/BranchingCallsExample.java b/infer/tests/codetoanalyze/java/crashcontext/BranchingCallsExample.java new file mode 100644 index 000000000..5edbdd6ac --- /dev/null +++ b/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(); + } + +} diff --git a/infer/tests/codetoanalyze/java/crashcontext/BranchingCallsExample.stacktrace.json b/infer/tests/codetoanalyze/java/crashcontext/BranchingCallsExample.stacktrace.json new file mode 100644 index 000000000..d7c823459 --- /dev/null +++ b/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"]} diff --git a/infer/tests/codetoanalyze/java/crashcontext/MultiStackFrameCrashExample.java b/infer/tests/codetoanalyze/java/crashcontext/MultiStackFrameCrashExample.java new file mode 100644 index 000000000..e47995c53 --- /dev/null +++ b/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(); + } + +} diff --git a/infer/tests/codetoanalyze/java/crashcontext/MultiStackFrameCrashExample.stacktrace.json b/infer/tests/codetoanalyze/java/crashcontext/MultiStackFrameCrashExample.stacktrace.json new file mode 100644 index 000000000..19dea3c86 --- /dev/null +++ b/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"]}