Simple model for locks

Reviewed By: sblackshear

Differential Revision: D2895513

fb-gh-sync-id: 9b4f805

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

@@ -18,6 +18,10 @@ public class InferBuiltins {
 
     public native static void __set_lock_attribute(Object o);
 
+    public native static void __set_locked_attribute(Object o);
+
+    public native static void __set_unlocked_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

@@ -0,0 +1,68 @@
+/*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package java.util.concurrent.locks;
+import java.util.concurrent.TimeUnit;
+import com.facebook.infer.models.InferBuiltins;
+import com.facebook.infer.models.InferUndefined;
+
+/*
+Lock is in actuality an interface, but is implemented here as an abstract class for
+modelling reasons. Note that we don't provide a model here for the newCondition() method.
+*/
+
+public abstract class Lock {
+
+   void lock() {
+      InferBuiltins.__set_locked_attribute(this);
+    }
+
+    /**
+      Sometimes doesn't get a lock.
+     */
+    public void lockInterruptibly() throws InterruptedException {
+      if (InferUndefined.boolean_undefined()) {
+          InferBuiltins.__set_locked_attribute(this);
+        } else {
+            throw new InterruptedException();
+        }
+    }
+
+    /**
+      Again, doesn't always succeed
+     */
+    public boolean tryLock() {
+      if (InferUndefined.boolean_undefined()) {
+          InferBuiltins.__set_locked_attribute(this);
+          return true;
+        } else {
+          return false; /*Could add unlocked, but not for now*/
+        }
+    }
+
+    public boolean tryLock(long timeout, TimeUnit unit) throws InterruptedException {
+      if (InferUndefined.boolean_undefined()) {throw new InterruptedException();}
+
+      if (InferUndefined.boolean_undefined()) {
+          InferBuiltins.__set_locked_attribute(this);
+          return true;
+        } else {
+          return false; /*Could add unlocked, but not for not*/
+        }
+    }
+
+    /**
+     * In some implementations (like ReentrantLock) an exception is thrown if the lock
+     * is not held by the current thread. This model does not consider that possibility.
+     */
+    public void unlock() {
+        InferBuiltins.__set_unlocked_attribute(this);
+    }
+
+}

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

@@ -0,0 +1,61 @@
+/*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+/* Reentrant Lock model
+* This is a partial model. Several methods such as getowner(),  hasQueueThread(),
+* getQueueLength() are not modelled.
+* 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
+* when the lock is held by another thread, not considered here..
+*
+*/
+
+package java.util.concurrent.locks;
+import com.facebook.infer.models.InferBuiltins;
+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
+    */
+    public void lock() {
+      InferBuiltins.__set_locked_attribute(this);
+    }
+
+     /**
+     * In some implementations (like ReentrantLock) an exception is thrown if the lock
+     * is not held by the current thread. This model does not consider that possibility.
+     * We should be able to delete this and inherit from the modle in Lock.java,
+     * when improved treatment of dynamic dispatch lands
+     */
+    public void unlock() {
+      InferBuiltins.__set_unlocked_attribute(this);
+    }
+
+     /**
+      *  TODO. This requires us to abduce lockedness. Do later.
+     public boolean isLocked() {
+     */
+}

infer/src/backend/sil.ml

@@ -618,6 +618,8 @@ and attribute =
   | Aundef of Procname.t * Location.t * path_pos
   | Ataint of Procname.t (** Procname is the source of the taint *)
   | Auntaint
+  | Alocked
+  | Aunlocked
   (** value appeared in second argument of division at given path position *)
   | Adiv0 of path_pos
   (** the exp. is null because of a call to a method with exp as a null receiver *)
@@ -630,6 +632,7 @@ and attribute_category =
   | ACresource
   | ACautorelease
   | ACtaint
+  | AClock
   | ACdiv0
   | ACobjc_null
   | ACundef
@@ -1170,6 +1173,8 @@ let attribute_to_category att =
   | Adangling _ -> ACresource
   | Ataint _
   | Auntaint -> ACtaint
+  | Alocked
+  | Aunlocked -> AClock
   | Aautorelease -> ACautorelease
   | Adiv0 _ -> ACdiv0
   | Aobjc_null _ -> ACobjc_null
@@ -1376,6 +1381,12 @@ and attribute_compare (att1 : attribute) (att2 : attribute) : int =
   | Auntaint, Auntaint -> 0
   | Auntaint, _ -> -1
   | _, Auntaint -> 1
+  | Alocked, Alocked -> 0
+  | Alocked, _ -> -1
+  | _, Alocked -> 1
+  | Aunlocked, Aunlocked -> 0
+  | Aunlocked, _ -> -1
+  | _, Aunlocked -> 1
   | Adiv0 pp1, Adiv0 pp2 ->
       path_pos_compare pp1 pp2
   | Adiv0 _, _ -> -1
@@ -1940,6 +1951,8 @@ and attribute_to_string pe = function
       (str_binop pe Gt) ^ ":" ^ (string_of_int loc.Location.line)
   | Ataint pn -> "TAINTED[" ^ (Procname.to_string pn) ^ "]"
   | Auntaint -> "UNTAINTED"
+  | Alocked -> "LOCKED"
+  | Aunlocked -> "UNLOCKED"
   | Adiv0 (pn, nd_id) -> "DIV0"
   | Aobjc_null exp ->
       let info_s =

infer/src/backend/sil.mli

@@ -248,6 +248,8 @@ and attribute =
   | Aundef of Procname.t * Location.t * path_pos
   | Ataint of Procname.t (** Procname is the source of the taint *)
   | Auntaint
+  | Alocked
+  | Aunlocked
   (** value appeared in second argument of division at given path position *)
   | Adiv0 of path_pos
   (** the exp. is null because of a call to a method with exp as a null receiver *)
@@ -260,6 +262,7 @@ and attribute_category =
   | ACresource
   | ACautorelease
   | ACtaint
+  | AClock
   | ACdiv0
   | ACobjc_null
   | ACundef

infer/src/backend/symExec.ml

@@ -2018,6 +2018,27 @@ module ModelBuiltins = struct
         [(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Auntaint), path)]
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
+  (** Set the attibute of the value as locked*)
+  let execute___set_locked_attribute cfg pdesc instr tenv _prop path ret_ids args callee_name loc
+    : Builtin.ret_typ =
+    match args, ret_ids with
+    | [(lexp, typ)], _ ->
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
+        [(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Alocked), path)]
+    | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
+
+  (** Set the attibute of the value as unlocked*)
+  let execute___set_unlocked_attribute cfg pdesc instr tenv _prop path ret_ids args callee_name loc
+    : Builtin.ret_typ =
+    match args, ret_ids with
+    | [(lexp, typ)], _ ->
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
+        [(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Aunlocked), path)]
+    | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
+
+
   (** report an error if [lexp] is tainted; otherwise, add untained([lexp]) as a precondition *)
   let execute___check_untainted cfg pdesc instr tenv prop path ret_ids args callee_pname loc
     : Builtin.ret_typ =
@@ -2511,9 +2532,16 @@ module ModelBuiltins = struct
   let __infer_fail = Builtin.register "__infer_fail" execute___infer_fail
   let __assert_fail = Builtin.register "__assert_fail" execute___assert_fail
 
-  let _ = Builtin.register "__set_hidden_field" execute___set_hidden_field  (* set a hidden field in the struct to the given value *)
-  let _ = Builtin.register "__set_taint_attribute" execute___set_taint_attribute (* set the attribute of the parameter as tainted *)
-  let _ = Builtin.register "__set_untaint_attribute" execute___set_untaint_attribute (* set the attribute of the parameter as tainted *)
+  (* set a hidden field in the struct to the given value *)
+  let _ = Builtin.register "__set_hidden_field" execute___set_hidden_field  
+  (* set the attribute of the parameter as tainted *)
+  let _ = Builtin.register "__set_taint_attribute" execute___set_taint_attribute 
+  (* set the attribute of the parameter as untainted *)
+  let _ = Builtin.register "__set_untaint_attribute" execute___set_untaint_attribute 
+  (* set the attribute of the parameter as locked *)
+  let _ = Builtin.register "__set_locked_attribute" execute___set_locked_attribute 
+  (* set the attribute of the parameter as unlocked *)
+  let _ = Builtin.register "__set_unlocked_attribute" execute___set_unlocked_attribute 
   let _ = Builtin.register "__check_untainted" execute___check_untainted (* report a taint error if the parameter is tainted, and assume it is untainted afterward *)
   let __objc_retain = Builtin.register "__objc_retain" execute___objc_retain (* objective-c "retain" *)
   let __objc_release = Builtin.register "__objc_release" execute___objc_release (* objective-c "release" *)