diff --git a/infer/src/checkers/AbstractDomain.ml b/infer/src/checkers/AbstractDomain.ml index 6e6ee40ec..077867c76 100644 --- a/infer/src/checkers/AbstractDomain.ml +++ b/infer/src/checkers/AbstractDomain.ml @@ -222,3 +222,17 @@ module BooleanAnd = struct let pp fmt astate = F.fprintf fmt "%b" astate end + +module BooleanOr = struct + type astate = bool + + let (<=) ~lhs ~rhs = not lhs || rhs + + let join = (||) + + let widen ~prev ~next ~num_iters:_ = + join prev next + + let pp fmt astate = + F.fprintf fmt "%b" astate +end diff --git a/infer/src/checkers/AbstractDomain.mli b/infer/src/checkers/AbstractDomain.mli index 77113b3e8..caae8dd66 100644 --- a/infer/src/checkers/AbstractDomain.mli +++ b/infer/src/checkers/AbstractDomain.mli @@ -76,5 +76,9 @@ module InvertedMap (Map : PrettyPrintable.PPMap) (ValueDomain : S) : sig end (** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's - true in both branches. *) + true in both conditional branches. *) module BooleanAnd : S with type astate = bool + +(** Boolean domain ordered by ~p || q. Useful when you want a boolean that's true only when it's + true in one conditional branch. *) +module BooleanOr : S with type astate = bool diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 5c1ff1fef..3d384f006 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -66,11 +66,23 @@ let make_access access_path access_kind loc = let site = CallSite.make Typ.Procname.empty_block loc in TraceElem.make (access_path, access_kind) site +(* In this domain true<=false. The intended denotations [[.]] are + [[true]] = the set of all states where we know according, to annotations + or assertions or lock instructions, that some lock is held. + [[false]] = the empty set + The use of && for join in this domain enforces that, to know a lock is held, one must hold in + all branches. +*) module LocksDomain = AbstractDomain.BooleanAnd -(*At first we are modelling the distinction "true, known to be UI thread" - and "false, don't know definitley to be main tread". Can refine later *) -module ThreadsDomain = AbstractDomain.BooleanAnd +(* In this domain false<=true. The intended denotations [[.]] are + [[true]] = the set of all states where we know according, to annotations + or assertions, that we are on the UI thread (or some oter specific thread). + [[false]] = the set of all states + The use of || for join in this domain enforces that, to not know for sure you are threaded, + it is enough to be unthreaded in one branch. (See RaceWithMainThread.java for examples) +*) +module ThreadsDomain = AbstractDomain.BooleanOr module PathDomain = SinkTrace.Make(TraceElem) diff --git a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java index 7fc8b4721..6fbdd36d4 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java @@ -163,6 +163,32 @@ class Annotations implements Interface { i = zz; } + /* Like in RaceWithMainThread.java with assertMainThread() */ + void conditional_Ok(boolean b){ + if (b) { + write_on_main_thread_Ok(); + } /* BooleanAnd for threaded would hose you here and lead to a report */ + } + + Integer ii; + + @ThreadConfined(ThreadConfined.UI) + void write_on_main_thread_Ok(){ + ii = 22; + } + +/* +fix with a more refined abstract domain (without going all the way to disjuntions) */ + void FN_conditional_Bad(boolean b){ + if (b) + { + write_on_main_thread_Ok(); + } else { + ii = 99; // Using || for threaded hoses this; no report + } + } + + @OnBind public void onBindMethodOk() { this.f = new Object(); diff --git a/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java b/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java index 76050015b..91c9479cf 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java +++ b/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java @@ -89,4 +89,27 @@ class RaceWithMainThread{ holds_lock_OK(); g = 77; } + +/* This was a source of false positives until we interpreted join of threaded +by || instead of &&; see BooleanOr in ThreadSafetyDomain.ml */ + void conditional_Ok(boolean b){ + if (b) + { /*People not literally putting this assert inside if's, + but implicitly by method calls */ + o. assertMainThread(); + f = 88; + } /* BooleanAnd for threaded would hose you here and lead to a report */ + } + +/* On the other hand, BooleanOr leads to false negatives, which we should +fix with a more refined abstract domain (without going all the way to disjuntions) */ + void FN_conditional_Bad(boolean b){ + if (b) + { + o.assertMainThread(); + f = 88; + } else { + f = 99; // Using || hoses this; no report + } + } }