[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

@@ -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

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

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"
+(* In this domain false<=true. The intended denotations [[.]] are
-  and "false, don't know definitley to be main tread". Can refine later *)
+   [[true]] = the set of all states where we know according, to annotations
-module ThreadsDomain = AbstractDomain.BooleanAnd
+             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)
 

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();

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
+   }
+ }
 }