diff --git a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java b/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java index f084bd78c..ffa378911 100644 --- a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java +++ b/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); diff --git a/infer/models/java/src/java/util/concurrent/Lock.java b/infer/models/java/src/java/util/concurrent/Lock.java new file mode 100644 index 000000000..d0868b498 --- /dev/null +++ b/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); + } + +} diff --git a/infer/models/java/src/java/util/concurrent/ReentrantLock.java b/infer/models/java/src/java/util/concurrent/ReentrantLock.java new file mode 100644 index 000000000..50660ffb5 --- /dev/null +++ b/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() { + */ +} diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index dadc23f07..b3bd22624 100644 --- a/infer/src/backend/sil.ml +++ b/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 = diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index 8841c5d8c..1caa2b808 100644 --- a/infer/src/backend/sil.mli +++ b/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 diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 548b22b2a..510342ee1 100644 --- a/infer/src/backend/symExec.ml +++ b/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" *)