From 2dc796542a10b3257f608fc7f0a41b64ff5df735 Mon Sep 17 00:00:00 2001 From: jrm Date: Sat, 1 Aug 2015 15:53:10 -0700 Subject: [PATCH] [infer][java] the detection of a resource leak should not prevent the symbolic execution to proceed Summary: When detecting a resource leak, Infer used to raise an Leak exception and then prevent the specs to be computed for the paths containing a leak. This diff prevents resource leak to stop the analysis. --- infer/src/backend/abs.ml | 4 +- .../infer/CloseableAsResourceExample.java | 86 ++++++++++--------- .../java/infer/NullPointerExceptions.java | 8 +- .../java/infer/CloseableAsResourceTest.java | 1 + .../java/infer/NullPointerExceptionTest.java | 3 +- 5 files changed, 58 insertions(+), 44 deletions(-) diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index e9d56c686..887f25a97 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1333,8 +1333,8 @@ let check_junk ?original_prop pname tenv prop = list_mem attr_opt_equal alloc_attribute !leaks_reported in let ignore_leak = !Config.allowleak || ignore_resource || is_undefined || already_reported () in - (* in footprint mode, report leak and continue *) - let report_and_continue = !Config.footprint in + let report_and_continue = + !Sil.curr_language = Sil.Java || !Config.footprint in let report_leak () = if not report_and_continue then raise exn else diff --git a/infer/tests/codetoanalyze/java/infer/CloseableAsResourceExample.java b/infer/tests/codetoanalyze/java/infer/CloseableAsResourceExample.java index ecc34555a..5bda6ff58 100644 --- a/infer/tests/codetoanalyze/java/infer/CloseableAsResourceExample.java +++ b/infer/tests/codetoanalyze/java/infer/CloseableAsResourceExample.java @@ -16,23 +16,54 @@ import java.io.IOException; import java.io.StringReader; -public class CloseableAsResourceExample { +class LocalException extends IOException { +} - native boolean star(); +class SomeResource implements Closeable { - class LocalException extends IOException { + void doSomething() throws LocalException { + if (!CloseableAsResourceExample.star()) { + throw new LocalException(); + } } - class SomeResource implements Closeable { + public void close() {} +} - void doSomething() throws LocalException { - if (!star()) { - throw new LocalException(); - } - } +class Resource implements Closeable { + public Resource() { + } + public void close() {} +} + +class Wrapper implements Closeable { + Resource mR; + public Wrapper(Resource r) { + mR = r; + } + public void close() { + mR.close(); + } +} - public void close() {} +class Sub extends Wrapper { + public Sub(Resource r) { + super(r); } +} + +class ResourceWithException implements Closeable { + + public void close() throws IOException { + if (CloseableAsResourceExample.star()) { + throw new IOException(); + } + } +} + +public class CloseableAsResourceExample { + + native static boolean star(); void closingCloseable() { SomeResource res = new SomeResource(); @@ -59,27 +90,6 @@ public class CloseableAsResourceExample { res.close(); } // should report a resource leak - class Resource implements Closeable { - public Resource() { - } - public void close() {} - } - - class Wrapper implements Closeable { - Resource mR; - public Wrapper(Resource r) { - mR = r; - } - public void close() { - mR.close(); - } - } - - class Sub extends Wrapper { - public Sub(Resource r) { - super(r); - } - } void closingWrapper() { Resource r = new Resource(); @@ -124,15 +134,6 @@ public class CloseableAsResourceExample { } } - class ResourceWithException implements Closeable { - - public void close() throws IOException { - if (star()) { - throw new IOException(); - } - } - } - void noLeakwithExceptionOnClose() throws IOException { ResourceWithException res = new ResourceWithException(); res.close(); @@ -143,4 +144,9 @@ public class CloseableAsResourceExample { Utils.closeQuietly(res); } + static T sourceOfNullWithResourceLeak() { + SomeResource r = new SomeResource(); + return null; + } + } diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java index 96e5ed415..dac363e66 100644 --- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java +++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java @@ -335,10 +335,16 @@ public class NullPointerExceptions { } } + void nullableNonNullStringAfterTextUtilsIsEmptyCheckShouldNotCauseNPE(@Nullable String str) { - if(!TextUtils.isEmpty(str)) { + if (!TextUtils.isEmpty(str)) { str.length(); } } + void someNPEAfterResourceLeak() { + T t = CloseableAsResourceExample.sourceOfNullWithResourceLeak(); + t.f(); + } + } diff --git a/infer/tests/endtoend/java/infer/CloseableAsResourceTest.java b/infer/tests/endtoend/java/infer/CloseableAsResourceTest.java index 3a4c8a2bb..dfcccf240 100644 --- a/infer/tests/endtoend/java/infer/CloseableAsResourceTest.java +++ b/infer/tests/endtoend/java/infer/CloseableAsResourceTest.java @@ -42,6 +42,7 @@ public class CloseableAsResourceTest { "notClosingCloseable", "notClosingWrapper", "failToCloseWithCloseQuietly", + "sourceOfNullWithResourceLeak", }; assertThat( "Results should not contain resource leak errors", diff --git a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java index e54fbe403..0bc0e8ba7 100644 --- a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java +++ b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java @@ -59,7 +59,8 @@ public class NullPointerExceptionTest { "nullableParamNPE", "badCheckShouldCauseNPE", "nullPointerExceptionArrayLength", - "npeWithDollars" + "npeWithDollars", + "someNPEAfterResourceLeak", }; assertThat( "Results should contain " + NULL_DEREFERENCE,