Implement '-a crashcontext' and '-st trace' options to invoke BoundedCallTree.ml from the command line.

Reviewed By: sblackshear

Differential Revision: D3606446

fbshipit-source-id: 9ac92fa

infer/lib/python/inferlib/analyze.py

@@ -306,6 +306,8 @@ class AnalyzerWrapper(object):
 
         if self.args.analyzer == config.ANALYZER_ERADICATE:
             infer_options += ['-eradicate']
+        elif self.args.analyzer == config.ANALYZER_CRASHCONTEXT:
+            infer_options += ['-crashcontext']
         elif self.args.analyzer == config.ANALYZER_CHECKERS:
             infer_options += ['-checkers']
         else:

infer/lib/python/inferlib/config.py

@@ -70,11 +70,13 @@ ANALYZER_CHECKERS = 'checkers'
 ANALYZER_CAPTURE = 'capture'
 ANALYZER_COMPILE = 'compile'
 ANALYZER_TRACING = 'tracing'
+ANALYZER_CRASHCONTEXT = 'crashcontext'
 
 ANALYZERS = [
     ANALYZER_CAPTURE,
     ANALYZER_CHECKERS,
     ANALYZER_COMPILE,
+    ANALYZER_CRASHCONTEXT,
     ANALYZER_ERADICATE,
     ANALYZER_INFER,
     ANALYZER_TRACING,

infer/src/backend/config.ml

@@ -18,10 +18,12 @@ module F = Format
 
 
 type analyzer = Capture | Compile | Infer | Eradicate | Checkers | Tracing
+              | Crashcontext
 
 let string_to_analyzer =
   [("capture", Capture); ("compile", Compile);
-   ("infer", Infer); ("eradicate", Eradicate); ("checkers", Checkers); ("tracing", Tracing)]
+   ("infer", Infer); ("eradicate", Eradicate); ("checkers", Checkers);
+   ("tracing", Tracing); ("crashcontext", Crashcontext)]
 
 
 type clang_lang = C | CPP | OBJC | OBJCPP
@@ -681,7 +683,7 @@ and enable_checks =
     "show reports coming from this type of errors"
 
 (** command line option to activate the eradicate checker. *)
-and eradicate, checkers =
+and checkers, eradicate, crashcontext =
   (** command line option: if true, run the analysis in checker mode *)
   let checkers =
     CLOpt.mk_bool ~deprecated:["checkers"] ~long:"checkers"
@@ -692,7 +694,13 @@ and eradicate, checkers =
       "Activate the eradicate checker for java annotations (also sets --checkers)"
       [checkers]
   in
-  (eradicate, checkers)
+  let crashcontext =
+    CLOpt.mk_bool_group ~deprecated:["crashcontext"] ~long:"crashcontext"
+      "Activate the crashcontext checker for java stack trace context \
+       reconstruction (also sets --checkers)"
+      [checkers]
+  in
+  (checkers, eradicate, crashcontext)
 
 and err_file =
   CLOpt.mk_string ~deprecated:["err_file"] ~long:"err-file" ~default:""
@@ -972,6 +980,12 @@ and specs_library =
        searched for spec files" in
   specs_library
 
+(** JSON encoded Java stacktrace file, currently used only for -a crashcontext *)
+and stacktrace =
+  CLOpt.mk_string_opt ~long:"stacktrace" ~short:"st" ~f:resolve ~exes:CLOpt.[Analyze]
+    ~meta:"file" "File path containing a json encoded crash stacktrace. \
+                  Used to guide the analysis (currently acknowledged by -a crashcontext)"
+
 (** If active, enable special treatment of static final fields. *)
 and static_final =
   CLOpt.mk_bool ~deprecated_no:["no-static_final"] ~long:"static-final" ~default:true
@@ -1297,13 +1311,14 @@ and changed_files_index = !changed_files_index
 and calls_csv = !calls_csv
 and checkers = !checkers
 (** should the checkers be run? *)
-and checkers_enabled = not !eradicate
+and checkers_enabled = not (!eradicate || !crashcontext)
 and clang_include_to_override = !clang_include_to_override
 and clang_lang = !clang_lang
 and cluster_cmdline = !cluster
 and code_query = !code_query
 and continue_capture = !continue
 and copy_propagation = !copy_propagation
+and crashcontext = !crashcontext
 and create_harness = !android_harness
 and cxx_experimental = !cxx_experimental
 and debug_mode = !debug
@@ -1369,6 +1384,7 @@ and source_file = !source_file
 and source_file_copy = !source_file_copy
 and spec_abs_level = !spec_abs_level
 and specs_library = !specs_library
+and stacktrace = !stacktrace
 and stats_mode = !stats
 and subtype_multirange = !subtype_multirange
 and svg = !svg

infer/src/backend/config.mli

@@ -16,6 +16,7 @@ open! Utils
 
 (** Various kind of analyzers *)
 type analyzer = Capture | Compile | Infer | Eradicate | Checkers | Tracing
+              | Crashcontext
 
 (** Association list of analyzers and their names *)
 val string_to_analyzer : (string * analyzer) list
@@ -163,6 +164,7 @@ val cluster_cmdline : string option
 val code_query : string option
 val continue_capture : bool
 val copy_propagation : bool
+val crashcontext : bool
 val create_harness : bool
 val cxx_experimental : bool
 val debug_mode : bool
@@ -226,6 +228,7 @@ val source_file : string option
 val source_file_copy : string option
 val spec_abs_level : int
 val specs_library : string list
+val stacktrace : string option
 val stats_mode : bool
 val subtype_multirange : bool
 val svg : bool

infer/src/checkers/BoundedCallTree.ml

@@ -36,7 +36,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         let proc_in_trace = IList.exists
             matches_proc
             proc_data.ProcData.extras.Stacktrace.frames in
-        if proc_in_trace then Domain.add pn astate else astate
+        if proc_in_trace then begin
+          L.stderr "Detected method: %a@." Procname.pp pn;
+          Domain.add pn astate
+        end
+        else
+          astate
     | Sil.Call _ ->
         (** We currently ignore calls through function pointers in C and
          * other potential special kinds of procedure calls to be added later,
@@ -53,5 +58,25 @@ module Analyzer =
     (Scheduler.ReversePostorder)
     (TransferFunctions)
 
-let checker { Callbacks.proc_desc; tenv; } trace =
+(** Stacktrace lookup:
+ * 1) Check if trace_ref is already set and use that.
+ * 2) If not, load trace from the file specified in Config.stacktrace. *)
+let trace_ref = ref None
+
+let load_trace () =
+  (** Check Config.stacktrace is set and points to a file,
+   * 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/... *)
+    | Some fname -> fname in
+  let new_trace = Stacktrace.of_json_file filename in
+  trace_ref := Some new_trace;
+  new_trace
+
+let checker { Callbacks.proc_desc; tenv; } =
+  let trace = match !trace_ref with
+    | None -> load_trace ()
+    | Some t -> t in
   ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv trace))

infer/src/checkers/registerCheckers.ml

@@ -32,6 +32,7 @@ let active_procedure_checkers () =
         FragmentRetainsViewChecker.callback_fragment_retains_view, checkers_enabled;
         SqlChecker.callback_sql, false;
         Eradicate.callback_eradicate, Config.eradicate;
+        BoundedCallTree.checker, Config.crashcontext;
         CodeQuery.code_query_callback, Config.code_query <> None;
         Checkers.callback_check_field_access, false;
         ImmutableChecker.callback_check_immutable_cast, checkers_enabled;

infer/src/harness/stacktrace.ml

@@ -59,3 +59,27 @@ let of_string s =
       let parsed = IList.map parse_stack_frame trace in
       make exception_name parsed
   | [] -> failwith "Empty stack trace"
+
+let of_json json =
+  let exception_name_key = "exception_type" in
+  let frames_key = "stack_trace" in
+  let extract_json_member key =
+    match Yojson.Basic.Util.member key json with
+    | `Null -> failwith ("Missing key in supplied JSON \
+                          data: " ^ key)
+    | item -> item in
+  let exception_name =
+    Yojson.Basic.Util.to_string (extract_json_member exception_name_key) in
+  let frames =
+    Yojson.Basic.Util.to_list (extract_json_member frames_key)
+    |> IList.map Yojson.Basic.Util.to_string
+    |> IList.map String.trim
+    |> IList.filter (fun s -> s <> "")
+    |> IList.map parse_stack_frame in
+  make exception_name frames
+
+let of_json_file filename =
+  match Utils.read_optional_json_file filename with
+  | Ok json -> of_json json
+  | Error msg -> failwith (Printf.sprintf "Could not read or parse the supplied JSON \
+                                           stacktrace file %s :\n %s" filename msg)

infer/src/harness/stacktrace.mli

@@ -26,3 +26,5 @@ val make : string -> frame list -> t
 val make_frame : string -> string -> string -> int -> frame
 
 val of_string : string -> t
+
+val of_json_file : string -> t

infer/tests/codetoanalyze/java/crashcontext/MinimalCrashExample.java

@@ -0,0 +1,19 @@
+/*
+ * 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 MinimalCrashExample {
+
+  public static void main(String[] args) {
+    String s = null;
+    s.toString();
+  }
+
+}

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

@@ -0,0 +1 @@
+{"exception_type": "java.lang.NullPointerException", "stack_trace": ["at endtoend.java.crashcontext.MinimalCrashExample.main(MinimalCrashExample.java:16)",""], "exception_message": "", "normvector_stack": ["endtoend.java.crashcontext.MinimalCrashExample.main"]}