fix treatment of linked list in Java

Summary:
public
The inductive list predicate was not firing during abstraction because of a type mismatch between C and Java. In Java, the second parameter of the `Sil.Sizeof` constructor is always `Sil.Subtype.exact` in C but is `Sil.Subtype.subtypes` in Java. This diff fixes the confution by comparing the `Sil` types only instead of the type expressions.

Reviewed By: jberdine

Differential Revision: D2912493

fb-gh-sync-id: 3f712a8
shipit-source-id: 3f712a8

infer/src/backend/abs.ml

@@ -404,8 +404,8 @@ let mk_rules_for_dll (para : Sil.hpara_dll) : rule list =
 (******************  End of DLL abstraction rules  ******************)
 
 (******************  Start of Predicate Discovery  ******************)
-let typ_get_recursive_flds tenv te =
+let typ_get_recursive_flds tenv typ_exp =
-  let filter (_, t, _) =
+  let filter typ (_, t, _) =
     match t with
     | Sil.Tvar _ | Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ -> false
     | Sil.Tptr (Sil.Tvar tname', _) ->
@@ -414,22 +414,22 @@ let typ_get_recursive_flds tenv te =
               L.err "@.typ_get_recursive: Undefined type %s@." (Typename.to_string tname');
               t
           | Some typ' -> typ' in
-        Sil.exp_equal te (Sil.Sizeof (typ', Sil.Subtype.exact))
+        Sil.typ_equal typ' typ
     | Sil.Tptr _ | Sil.Tstruct _ | Sil.Tarray _ | Sil.Tenum _ ->
         false
   in
-  match te with
+  match typ_exp with
   | Sil.Sizeof (typ, _) ->
       (match typ with
        | Sil.Tvar _ -> assert false (* there should be no indirection *)
        | Sil.Tint _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ | Sil.Tfloat _ | Sil.Tenum _ -> []
        | Sil.Tstruct { Sil.instance_fields } ->
-           IList.map (fun (x, y, z) -> x) (IList.filter filter instance_fields)
+           IList.map (fun (x, y, z) -> x) (IList.filter (filter typ) instance_fields)
        | Sil.Tarray _ -> [])
   | Sil.Var _ -> [] (* type of |-> not known yet *)
   | Sil.Const _ -> []
   | _ ->
-      L.err "@.typ_get_recursive: unexpected type expr: %a@." (Sil.pp_exp pe_text) te;
+      L.err "@.typ_get_recursive: unexpected type expr: %a@." (Sil.pp_exp pe_text) typ_exp;
       assert false
 
 let discover_para_roots p root1 next1 root2 next2 : Sil.hpara option =

infer/tests/ant_report.json

@@ -229,6 +229,11 @@
     "file": "codetoanalyze/java/infer/NullPointerExceptions.java",
     "procedure": "void NullPointerExceptions.derefNullableGetter()"
   },
+  {
+    "bug_type": "NULL_DEREFERENCE",
+    "file": "codetoanalyze/java/infer/NullPointerExceptions.java",
+    "procedure": "void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L)"
+  },
   {
     "bug_type": "RESOURCE_LEAK",
     "file": "codetoanalyze/java/infer/FilterInputStreamLeaks.java",

infer/tests/buck_report.json

@@ -229,6 +229,11 @@
     "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",
     "procedure": "void NullPointerExceptions.derefNullableGetter()"
   },
+  {
+    "bug_type": "NULL_DEREFERENCE",
+    "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",
+    "procedure": "void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L)"
+  },
   {
     "bug_type": "RESOURCE_LEAK",
     "file": "infer/tests/codetoanalyze/java/infer/FilterInputStreamLeaks.java",

infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java

@@ -469,4 +469,20 @@ public class NullPointerExceptions {
     }
   }
 
+  class L {
+    L next;
+  }
+
+  Object returnsNullAfterLoopOnList(L l) {
+    while (l != null) {
+      l = l.next;
+    }
+    return null;
+  }
+
+  void dereferenceAfterLoopOnList(L l) {
+    Object obj = returnsNullAfterLoopOnList(l);
+    obj.toString();
+  }
+
 }

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

@@ -67,7 +67,8 @@ public class NullPointerExceptionTest {
         "derefNull",
         "nullListFiles",
         "nullTryLock",
-        "tryLockThrows"
+        "tryLockThrows",
+        "dereferenceAfterLoopOnList",
     };
     assertThat(
         "Results should contain " + NULL_DEREFERENCE,