report errors when all the postconditions are error states

Summary:
The philosophy of the tracing mode reporting is to not report the errors in a method if reaching this error does depend on information that can be false at call site. Typically with:

  void foo(Object obj, int x) {
    if (x == 3) {
      obj.toString();
    }
  }

it may be that we always call `foo` with a non-null parameter or `x != 3`.

Thechnically, the reporting code matches the pairs of the form (precondition, error) and filtering out the cases where the precondtions was not imposing constraints on the calling context, and report the other cases. So the NPE could be reported in the following case:

  void bar() {
    foo(null, 3);
  }

However, we were missing the case where there was anyway no way to call a method in a safe way, i.e. all the preconditions were of the form: (precondition, error), for example:

  void baz(boolean b) {
    if (b) {
      foo(null, 3);
    } else {
      foo(null, 3);
    }
  }

In that case, the summary is of the form

  PRE (1): b = false
  POST: NullPointerException

  PRE (2): b = true
  POST: NullPointerException

In which case it is legit to report  `NullPointerException` in `baz`.

Reviewed By: sblackshear, jberdine

Differential Revision: D3220501

fb-gh-sync-id: 7fb7d70
fbshipit-source-id: 7fb7d70

infer/src/backend/interproc.ml

@@ -1065,24 +1065,24 @@ let reset_global_values proc_desc =
 
 (* Collect all pairs of the kind (precondition, runtime exception) from a summary *)
 let exception_preconditions tenv pname summary =
-  let collect_exceptions pre exns (prop, _) =
+  let collect_exceptions pre (exns, all_post_exn) (prop, _) =
     match Tabulation.prop_get_exn_name pname prop with
     | Some exn_name when PatternMatch.is_runtime_exception tenv exn_name ->
-        (pre, exn_name) :: exns
-    | _ -> exns in
+        ((pre, exn_name) :: exns, all_post_exn)
+    | _ -> (exns, false) in
   let collect_spec errors spec =
     IList.fold_left (collect_exceptions spec.Specs.pre) errors spec.Specs.posts in
-  IList.fold_left collect_spec [] (Specs.get_specs_from_payload summary)
+  IList.fold_left collect_spec ([], true) (Specs.get_specs_from_payload summary)
 
 (* Collect all pairs of the kind (precondition, custom error) from a summary *)
 let custom_error_preconditions summary =
-  let collect_errors pre errors (prop, _) =
+  let collect_errors pre (errors, all_post_error) (prop, _) =
     match Tabulation.lookup_custom_errors prop with
-    | None -> errors
-    | Some e -> (pre, e) :: errors in
+    | None -> (errors, false)
+    | Some e -> ((pre, e) :: errors, all_post_error) in
   let collect_spec errors spec =
     IList.fold_left (collect_errors spec.Specs.pre) errors spec.Specs.posts in
-  IList.fold_left collect_spec [] (Specs.get_specs_from_payload summary)
+  IList.fold_left collect_spec ([], true) (Specs.get_specs_from_payload summary)
 
 
 (* Remove the constrain of the form this != null which is true for all Java virtual calls *)
@@ -1138,8 +1138,10 @@ let report_runtime_exceptions tenv pdesc summary =
     let annotated_signature = Annotations.get_annotated_signature proc_attributes in
     let ret_annotation, _ = annotated_signature.Annotations.ret in
     Annotations.ia_is_verify ret_annotation in
+  let (exn_preconditions, all_post_exn) =
+    exception_preconditions tenv pname summary in
   let should_report pre =
-    is_main || is_annotated || is_unavoidable pre in
+    all_post_exn || is_main || is_annotated || is_unavoidable pre in
   let report (pre, runtime_exception) =
     if should_report pre then
       let pre_str =
@@ -1147,18 +1149,20 @@ let report_runtime_exceptions tenv pdesc summary =
       let exn_desc = Localise.java_unchecked_exn_desc pname runtime_exception pre_str in
       let exn = Exceptions.Java_runtime_exception (runtime_exception, pre_str, exn_desc) in
       Reporting.log_error pname ~pre: (Some (Specs.Jprop.to_prop pre)) exn in
-  IList.iter report (exception_preconditions tenv pname summary)
+  IList.iter report exn_preconditions
 
 
 let report_custom_errors summary =
   let pname = Specs.get_proc_name summary in
+  let error_preconditions, all_post_error =
+    custom_error_preconditions summary in
   let report (pre, custom_error) =
-    if is_unavoidable pre then
+    if all_post_error || is_unavoidable pre then
       let loc = summary.Specs.attributes.ProcAttributes.loc in
       let err_desc = Localise.desc_custom_error loc in
       let exn = Exceptions.Custom_error (custom_error, err_desc) in
       Reporting.log_error pname ~pre: (Some (Specs.Jprop.to_prop pre)) exn in
-  IList.iter report (custom_error_preconditions summary)
+  IList.iter report error_preconditions
 
 module SpecMap = Map.Make (struct
     type t = Prop.normal Specs.Jprop.t

infer/tests/codetoanalyze/c/errors/assertions/assertion_failure.c

@@ -75,3 +75,11 @@ void assignemt_before_check() {
   global = 0;
   check_global();
 }
+
+void failure_on_both_branches(int x) {
+  if (x > 3) {
+    simple_check(x);
+  } else {
+    simple_check(42);
+  }
+}

infer/tests/codetoanalyze/java/tracing/NullPointerExceptionExample.java

@@ -24,4 +24,20 @@ public class NullPointerExceptionExample {
     }
   }
 
+  void callDoesNotLeadToNpe() {
+    callDeref(null, false);
+  }
+
+  void callLeadToNpe() {
+    callDeref(null, true);
+  }
+
+  void npeOnBothBranches(int x) {
+    if (x < 2) {
+      callDeref(null, x < 3);
+    } else {
+      callDeref(null, true);
+    }
+  }
+
 }

infer/tests/endtoend/c/AssertionFailureTest.java

@@ -42,6 +42,7 @@ public class AssertionFailureTest {
         "should_report_assertion_failure",
         "assertion_failure_with_heap",
         "assignemt_before_check",
+        "failure_on_both_branches",
     };
     assertThat(
         "Results should contain " + ASSERTION_FAILURE,

infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java

@@ -42,7 +42,9 @@ public class NullPointerExceptionTest {
   public void matchErrors()
       throws IOException, InterruptedException, InferException {
     String[] methods = {
-        "callDeref"
+        "callDeref",
+        "callLeadToNpe",
+        "npeOnBothBranches",
     };
     assertThat(
         "Results should contain " + NPE,