From 4c2ef788a196eca42ca75fe5fcc0486f68bdfcf0 Mon Sep 17 00:00:00 2001 From: Peter O'Hearn Date: Fri, 14 Apr 2017 17:13:03 -0700 Subject: [PATCH] [infer][threadsafety] Use disjunction in the join for threaded Summary: There are false positives in the current analysis due to the use of conjunction in the treatment of threaded. Changing conjunction to disjunction removes these false positives. Some new false negatives arise, but all the old tests pass. This is a stopgap towards a better solution being planned. Reviewed By: sblackshear Differential Revision: D4883280 fbshipit-source-id: c2a7e6e --- infer/src/checkers/AbstractDomain.ml | 14 ++++++++++ infer/src/checkers/AbstractDomain.mli | 6 ++++- infer/src/checkers/ThreadSafetyDomain.ml | 18 ++++++++++--- .../java/threadsafety/Annotations.java | 26 +++++++++++++++++++ .../java/threadsafety/RaceWithMainThread.java | 23 ++++++++++++++++ 5 files changed, 83 insertions(+), 4 deletions(-) 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 + } + } }