alloc/dealloc model for locks

Reviewed By: sblackshear

Differential Revision: D3207043

fb-gh-sync-id: 6e45d03
fbshipit-source-id: 6e45d03

infer/models/java/src/com/facebook/infer/models/InferBuiltins.java

@@ -22,6 +22,8 @@ public class InferBuiltins {
 
     public native static void __set_unlocked_attribute(Object o);
 
+    public native static void __delete_locked_attribute(Object o);
+
     public native static void _exit();
 
     private native static void __infer_assume(boolean condition);

infer/models/java/src/java/util/concurrent/Lock.java

@@ -42,7 +42,7 @@ public abstract class Lock {
           InferBuiltins.__set_locked_attribute(this);
           return true;
         } else {
-          return false; /*Could add unlocked, but not for now*/
+          return false;
         }
     }
 
@@ -53,7 +53,7 @@ public abstract class Lock {
           InferBuiltins.__set_locked_attribute(this);
           return true;
         } else {
-          return false; /*Could add unlocked, but not for not*/
+          return false;
         }
     }
 
@@ -62,7 +62,7 @@ public abstract class Lock {
      * is not held by the current thread. This model does not consider that possibility.
      */
     public void unlock() {
-        InferBuiltins.__set_unlocked_attribute(this);
+        InferBuiltins.__delete_locked_attribute(this);
     }
 
 }

infer/models/java/src/java/util/concurrent/ReentrantLock.java

@@ -13,7 +13,7 @@
 * A reentrant lock is one where if you try to lock() a lock already held by
 * the current thread, you succeed and continue. In a non-reentrant lock you could deadlock.
 * This is not reflected.  java.util.concurrent ReentrantLocks have some fairness
-* guarantees and some tings about scheduling
+* guarantees and some things about scheduling
 * when the lock is held by another thread, not considered here..
 *
 */
@@ -24,18 +24,6 @@ import com.facebook.infer.models.InferUndefined;
 
 public abstract class ReentrantLock extends Lock implements java.io.Serializable {
 
-   /* Assuming a lock starts off in this "unlocked" state */
-    public ReentrantLock() {
-      InferBuiltins.__set_unlocked_attribute(this);
-    }
-
-    /**
-     ignoring fairness (hey, this is partial corretness!)
-     */
-    public ReentrantLock(boolean fair) {
-      InferBuiltins.__set_unlocked_attribute(this);
-    }
-
     /**
     * We should be able to delete this and inherit from the modle in Lock.java,
     * when improved treatment of dynamic dispatch lands
@@ -51,7 +39,7 @@ public abstract class ReentrantLock extends Lock implements java.io.Serializable
      * when improved treatment of dynamic dispatch lands
      */
     public void unlock() {
-      InferBuiltins.__set_unlocked_attribute(this);
+      InferBuiltins.__delete_locked_attribute(this);
     }
 
      /**

infer/src/backend/modelBuiltins.ml

@@ -588,6 +588,12 @@ let set_attr pdesc prop path exp attr =
   let n_lexp, prop = check_arith_norm_exp pname exp prop in
   [(Prop.add_or_replace_exp_attribute prop n_lexp attr, path)]
 
+let delete_attr pdesc prop path exp attr =
+  let pname = Cfg.Procdesc.get_proc_name pdesc in
+  let n_lexp, prop = check_arith_norm_exp pname exp prop in
+  [(Prop.remove_attribute_from_exp attr prop n_lexp, path)]
+
+
 (** Set attibute att *)
 let execute___set_attr attr { Builtin.pdesc; prop_; path; args; }
   : Builtin.ret_typ =
@@ -609,6 +615,21 @@ let execute___set_locked_attribute
     ra_vpath = None; } in
   execute___set_attr (Sil.Aresource ra) builtin_args
 
+(** Delete the resource/locked attibute of the value, if it is locked*)
+let execute___delete_locked_attribute { Builtin.pdesc; loc; prop_; path; args; }
+  : Builtin.ret_typ =
+  let pname = Cfg.Procdesc.get_proc_name pdesc in
+  (* ra_kind = Racquire in following indicates locked *)
+  let ra = {
+    Sil.ra_kind = Sil.Racquire;
+    ra_res = Sil.Rlock;
+    ra_pname = pname;
+    ra_loc = loc;
+    ra_vpath = None; } in
+  match args with
+  | [(lexp, _)] -> delete_attr pdesc prop_ path lexp (Sil.Aresource ra)
+  | _ -> raise (Exceptions.Wrong_argument_number __POS__)
+
 (** Set the attibute of the value as resource/unlocked*)
 let execute___set_unlocked_attribute
     ({ Builtin.pdesc; loc; } as builtin_args)
@@ -1061,6 +1082,9 @@ let __set_locked_attribute = Builtin.register
 let __set_unlocked_attribute = Builtin.register
     (* set the attribute of the parameter as unlocked *)
     "__set_unlocked_attribute" execute___set_unlocked_attribute
+let __delete_locked_attribute = Builtin.register
+    (* delete the locked attribute, when it exists *)
+    "__delete_locked_attribute" execute___delete_locked_attribute
 let _ = Builtin.register
     "__throw" execute_skip
 let __unwrap_exception = Builtin.register

infer/src/backend/modelBuiltins.mli

@@ -32,6 +32,7 @@ val __set_file_attribute : Procname.t
 val __set_mem_attribute : Procname.t
 val __set_locked_attribute : Procname.t
 val __set_unlocked_attribute : Procname.t
+val __delete_locked_attribute : Procname.t
 val __infer_assume : Procname.t
 val __objc_retain : Procname.t
 val __objc_release : Procname.t

infer/src/java/jTrans.ml

@@ -1128,7 +1128,7 @@ let rec instruction context pc instr : translation =
 
     | JBir.MonitorExit expr ->
         trans_monitor_enter_exit
-          context expr pc loc ModelBuiltins.__set_unlocked_attribute "MonitorExit"
+          context expr pc loc ModelBuiltins.__delete_locked_attribute "MonitorExit"
 
     | _ -> Skip
   with Frontend_error s ->

infer/tests/build_systems/expected_outputs/ant_report.json

@@ -254,6 +254,16 @@
     "file": "codetoanalyze/java/infer/NullPointerExceptions.java",
     "procedure": "void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L)"
   },
+  {
+    "bug_type": "NULL_DEREFERENCE",
+    "file": "codetoanalyze/java/infer/NullPointerExceptions.java",
+    "procedure": "void NullPointerExceptions.dereferenceAfterUnlock1(Lock)"
+  },
+  {
+    "bug_type": "NULL_DEREFERENCE",
+    "file": "codetoanalyze/java/infer/NullPointerExceptions.java",
+    "procedure": "void NullPointerExceptions.dereferenceAfterUnlock2(Lock)"
+  },
   {
     "bug_type": "RESOURCE_LEAK",
     "file": "codetoanalyze/java/infer/FilterInputStreamLeaks.java",

infer/tests/build_systems/expected_outputs/buck_report.json

@@ -254,6 +254,16 @@
     "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",
     "procedure": "void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L)"
   },
+  {
+    "bug_type": "NULL_DEREFERENCE",
+    "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",
+    "procedure": "void NullPointerExceptions.dereferenceAfterUnlock1(Lock)"
+  },
+  {
+    "bug_type": "NULL_DEREFERENCE",
+    "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",
+    "procedure": "void NullPointerExceptions.dereferenceAfterUnlock2(Lock)"
+  },
   {
     "bug_type": "RESOURCE_LEAK",
     "file": "infer/tests/codetoanalyze/java/infer/FilterInputStreamLeaks.java",

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

@@ -27,6 +27,7 @@ import java.io.IOException;
 import java.nio.channels.FileChannel;
 import java.nio.channels.FileLock;
 import java.lang.System;
+import java.util.concurrent.locks.Lock;
 import java.util.HashMap;
 
 public class NullPointerExceptions {
@@ -518,4 +519,20 @@ public class NullPointerExceptions {
     obj.toString();
   }
 
+  void dereferenceAfterUnlock1(Lock l) {
+    l.unlock();
+    String s = l.toString();
+    s = null;
+    s.toString(); // Expect NPE here
+  }
+
+  void dereferenceAfterUnlock2(Lock l) {
+    synchronized(l){
+      String b = null;
+    }
+    String s = l.toString();
+    s = null;
+    s.toString(); // Expect NPE here
+  }
+
 }

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

@@ -72,6 +72,8 @@ public class NullPointerExceptionTest {
         "nullTryLock",
         "tryLockThrows",
         "dereferenceAfterLoopOnList",
+        "dereferenceAfterUnlock1",
+        "dereferenceAfterUnlock2",
     };
     assertThat(
         "Results should contain " + NULL_DEREFERENCE,