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 fcd8bd968..6e6cfa8c2 100644 --- a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java +++ b/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); diff --git a/infer/models/java/src/java/util/concurrent/Lock.java b/infer/models/java/src/java/util/concurrent/Lock.java index d0868b498..e357ee486 100644 --- a/infer/models/java/src/java/util/concurrent/Lock.java +++ b/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); } } diff --git a/infer/models/java/src/java/util/concurrent/ReentrantLock.java b/infer/models/java/src/java/util/concurrent/ReentrantLock.java index 50660ffb5..2106128f1 100644 --- a/infer/models/java/src/java/util/concurrent/ReentrantLock.java +++ b/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); } /** diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 1791ad404..cceaa541a 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/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 diff --git a/infer/src/backend/modelBuiltins.mli b/infer/src/backend/modelBuiltins.mli index c0dc0894b..991d638d1 100644 --- a/infer/src/backend/modelBuiltins.mli +++ b/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 diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 2a122fcef..852d1d5b5 100644 --- a/infer/src/java/jTrans.ml +++ b/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 -> diff --git a/infer/tests/build_systems/expected_outputs/ant_report.json b/infer/tests/build_systems/expected_outputs/ant_report.json index 04e6f9131..ae44d15c9 100644 --- a/infer/tests/build_systems/expected_outputs/ant_report.json +++ b/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", diff --git a/infer/tests/build_systems/expected_outputs/buck_report.json b/infer/tests/build_systems/expected_outputs/buck_report.json index 210b2d7c4..fcf8d7ec4 100644 --- a/infer/tests/build_systems/expected_outputs/buck_report.json +++ b/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", diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java index 520575b46..a66173dd4 100644 --- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java +++ b/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 + } + } diff --git a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java index 8b2cc4f9a..ac3e6834d 100644 --- a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java +++ b/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,