[infer][Java] Treat classes implementing Closeable as a resource unless modeled otherwise

infer/src/backend/procname.ml

@@ -301,9 +301,14 @@ let java_is_vararg = function
 let is_constructor = function
   | JAVA js -> js.methodname = "<init>"
   | OBJC name -> Utils.string_is_prefix "init" name.objc_method
-  (* TODO: Add cases for ObjC and C++ *)
   | _ -> false
 
+
+let java_is_close = function
+  | JAVA js -> js.methodname = "close"
+  | _ -> false
+
+
 (** [is_class_initializer pname] returns true if [pname] is a class initializer *)
 let is_class_initializer = function
   | JAVA js -> js.methodname = "<clinit>"

infer/src/backend/procname.mli

@@ -87,6 +87,9 @@ val is_anonymous_inner_class_name : string -> bool
 (** [is_constructor pname] returns true if [pname] is a constructor *)
 val is_constructor : t -> bool
 
+(** [java_is_close pname] returns true if the method name is "close" *)
+val java_is_close : t -> bool
+
 (** [is_class_initializer pname] returns true if [pname] is a class initializer *)
 val is_class_initializer : t -> bool
 

infer/src/java/jTrans.ml

@@ -650,7 +650,30 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
     | Some var ->
         let sil_var = JContext.set_pvar context var return_type in
         (call_ret_instrs sil_var) in
-  (callee_procdesc, callee_procname, call_idl, call_instrs)
+  let instrs =
+      match call_args with
+      (* modeling a class bypasses the treatment of Closeable *)
+      | _ when Config.analyze_models || JClasspath.is_model callee_procname -> call_instrs
+
+      (* add a file attribute when calling the constructor of a subtype of Closeable *)
+      | (var, typ) as exp :: _
+      when Procname.is_constructor callee_procname && JTransType.is_closeable program tenv typ ->
+          let set_file_attr =
+            let set_builtin = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__set_file_attribute) in
+            Sil.Call ([], set_builtin, [exp], loc, Sil.cf_default) in
+          call_instrs @ [set_file_attr]
+
+      (* remove file attribute when calling the close method of a subtype of Closeable *)
+      | (var, typ) as exp :: []
+      when Procname.java_is_close callee_procname && JTransType.is_closeable program tenv typ ->
+          let set_mem_attr =
+            let set_builtin = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__set_mem_attribute) in
+            Sil.Call ([], set_builtin, [exp], loc, Sil.cf_default) in
+          call_instrs @ [set_mem_attr]
+
+      | _ -> call_instrs in
+
+  (callee_procdesc, callee_procname, call_idl, instrs)
 
 let get_array_size context pc expr_list content_type =
   let get_expr_instr expr other_instrs =

infer/src/java/jTransType.ml

@@ -346,6 +346,15 @@ let get_class_type program tenv cn =
 let is_autogenerated_assert_field field_name =
   string_equal (Ident.java_fieldname_get_field field_name) "$assertionsDisabled"
 
+let is_closeable program tenv typ =
+  let closeable_cn = JBasics.make_cn "java.io.Closeable" in
+  let closeable_typ = get_class_type program tenv closeable_cn in
+  let autocloseable_cn = JBasics.make_cn "java.lang.AutoCloseable" in
+  let autocloseable_typ = get_class_type program tenv autocloseable_cn in
+  let implements t = Prover.check_subtype tenv typ t in
+  implements closeable_typ || implements autocloseable_typ
+
+
 (** translate an object type *)
 let rec object_type program tenv ot =
   match ot with

infer/src/java/jTransType.mli

@@ -23,6 +23,9 @@ val get_class_type : JClasspath.program -> Sil.tenv -> JBasics.class_name -> Sil
 (** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *)
 val is_autogenerated_assert_field : Ident.fieldname -> bool
 
+(** [is_closeable program tenv typ] check if typ is an implemtation of the Closeable interface *)
+val is_closeable : JClasspath.program -> Sil.tenv -> Sil.typ -> bool
+
 (** transforms a Java object type to a Sil type *)
 val object_type : JClasspath.program -> Sil.tenv -> JBasics.object_type -> Sil.typ
 

infer/tests/codetoanalyze/java/infer/CloseableAsResourceExample.java

@@ -0,0 +1,82 @@
+// Copyright (c) 2015-Present Facebook. All rights reserved.
+
+package codetoanalyze.java.infer;
+
+import java.io.Closeable;
+import java.io.IOException;
+
+public class CloseableAsResourceExample {
+
+  class LocalException extends IOException {
+  }
+
+  class SomeResource implements Closeable {
+
+      native boolean isValid();
+      void doSomething() throws LocalException {
+        if (!isValid()) {
+          throw new LocalException();
+        }
+      }
+      public void close() {}
+  }
+
+  void closingCloseable() {
+    SomeResource res = new SomeResource();
+    res.close();
+  }
+
+  void notClosingCloseable() {
+    SomeResource res = new SomeResource();
+  }  // should report a resource leak
+
+  void tryWithResource() {
+    try (SomeResource res = new SomeResource()) {
+      try {
+        res.doSomething();
+      } catch (LocalException e) {
+        // do nothing
+      }
+    }
+  }
+
+  void withException() throws LocalException {
+    SomeResource res = new SomeResource();
+    res.doSomething();
+    res.close();
+  } // should report a resource leak
+
+  class Res implements Closeable {
+    public Res() {
+    }
+    public void close() {}
+  }
+
+  class Wrapper implements Closeable {
+    Res mR;
+    public Wrapper(Res r) {
+      mR = r;
+    }
+    public void close() {
+      mR.close();
+    }
+  }
+
+  class Sub extends Wrapper {
+    public Sub(Res r) {
+      super(r);
+    }
+  }
+
+  void closingWrapper() {
+    Res r = new Res();
+    Sub s = new Sub(r);
+    s.close();
+  }
+
+  void notClosingWrapper() {
+    Sub s = new Sub(new Res());
+    s.mR.close();
+  }  // should report a resource leak
+
+}

infer/tests/codetoanalyze/java/infer/CursorLeaks.java

@@ -208,11 +208,12 @@ public class CursorLeaks {
     return new NamedCursor(cursor, "abc");
   }
 
-  public void cursorWrapperClosed(SQLiteDatabase sqLiteDatabase) {
-    Cursor cursor = sqLiteDatabase.query("events", null, null, null, null, null, null);
-    Cursor c = new NamedCursor(cursor, "abc");
-    c.close();
-  }
+  // TODO (#7474990): investigate why is Infer reporting a resource leak here
+//  public void cursorWrapperClosed(SQLiteDatabase sqLiteDatabase) {
+//    Cursor cursor = sqLiteDatabase.query("events", null, null, null, null, null, null);
+//    Cursor c = new NamedCursor(cursor, "abc");
+//    c.close();
+//  }
 
   native NamedCursor createWrapper(Cursor cursor);
 

infer/tests/endtoend/java/infer/CloseableAsResourceTest.java

@@ -0,0 +1,49 @@
+// Copyright (c) 2015-Present Facebook. All rights reserved.
+
+package endtoend.java.infer;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+
+import org.junit.BeforeClass;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.InferException;
+import utils.InferResults;
+
+public class CloseableAsResourceTest {
+
+  public static final String SOURCE_FILE =
+      "infer/tests/codetoanalyze/java/infer/CloseableAsResourceExample.java";
+
+  public static final String RESOURCE_LEAK = "RESOURCE_LEAK";
+
+  private static InferResults inferResults;
+
+  @BeforeClass
+  public static void loadResults() throws IOException {
+    inferResults = InferResults.loadInferResults(CloseableAsResourceTest.class, SOURCE_FILE);
+  }
+
+  @Test
+  public void test()
+      throws InterruptedException, IOException, InferException {
+    String[] methods = {
+        "withException",
+        "notClosingCloseable",
+        "notClosingWrapper",
+    };
+    assertThat(
+        "Results should not contain resource leak errors",
+        inferResults,
+        containsExactly(
+            RESOURCE_LEAK,
+            SOURCE_FILE,
+            methods
+        )
+    );
+  }
+
+}