From 8072d2c1e568e4eed25776a1253017d45a12a54f Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Tue, 26 Apr 2016 17:02:08 -0700 Subject: [PATCH] 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 | 28 +++++++++++-------- .../c/errors/assertions/assertion_failure.c | 8 ++++++ .../tracing/NullPointerExceptionExample.java | 16 +++++++++++ .../endtoend/c/AssertionFailureTest.java | 1 + .../tracing/NullPointerExceptionTest.java | 4 ++- 5 files changed, 44 insertions(+), 13 deletions(-) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 423a9ddad..54465cdde 100644 --- a/infer/src/backend/interproc.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/errors/assertions/assertion_failure.c b/infer/tests/codetoanalyze/c/errors/assertions/assertion_failure.c index b61e693b1..50e63413f 100644 --- a/infer/tests/codetoanalyze/c/errors/assertions/assertion_failure.c +++ b/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); + } +} diff --git a/infer/tests/codetoanalyze/java/tracing/NullPointerExceptionExample.java b/infer/tests/codetoanalyze/java/tracing/NullPointerExceptionExample.java index cc28aff7f..2ea4f71ab 100644 --- a/infer/tests/codetoanalyze/java/tracing/NullPointerExceptionExample.java +++ b/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); + } + } + } diff --git a/infer/tests/endtoend/c/AssertionFailureTest.java b/infer/tests/endtoend/c/AssertionFailureTest.java index 075aeae88..b95a2e02b 100644 --- a/infer/tests/endtoend/c/AssertionFailureTest.java +++ b/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, diff --git a/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java b/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java index c30b98eaf..943d83e1b 100644 --- a/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java +++ b/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,