[thread-safety][cleanup] get rid of thumbs_up

Summary: Not using this for now, and it seems good to simplify the complex domain as much as we can.

Reviewed By: jberdine

Differential Revision: D5970233

fbshipit-source-id: a451503

infer/src/checkers/ThreadSafety.ml

@@ -513,8 +513,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     in
     (* we need a more intelligent escape analysis, that branches on whether we own the container *)
     Some
-      { thumbs_up= true
-      ; locks= false
+      { locks= false
       ; threads= ThreadsDomain.Unknown
       ; accesses= callee_accesses
       ; return_ownership= OwnershipAbstractValue.unowned
@@ -629,7 +628,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                     Typ.Procname.pp callee_pname )
             | NoEffect ->
               match get_summary pdesc callee_pname actuals loc tenv with
-              | Some {thumbs_up; threads; locks; accesses; return_ownership; return_attributes}
+              | Some {threads; locks; accesses; return_ownership; return_attributes}
                -> let update_caller_accesses pre callee_accesses caller_accesses =
                     let combined_accesses =
                       PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc)
@@ -637,7 +636,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                     in
                     AccessDomain.add pre combined_accesses caller_accesses
                   in
-                  let thumbs_up = thumbs_up && astate.thumbs_up in
                   let locks = locks || astate.locks in
                   let threads = ThreadsDomain.join threads astate.threads in
                   let unprotected = is_unprotected locks threads pdesc in
@@ -715,7 +713,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                   let ownership, attribute_map =
                     propagate_return ret_opt return_ownership return_attributes actuals astate
                   in
-                  {thumbs_up; locks; threads; accesses; ownership; attribute_map}
+                  {locks; threads; accesses; ownership; attribute_map}
               | None
                -> let should_assume_returns_ownership (call_flags: CallFlags.t) actuals =
                     (* assume non-interface methods with no summary and no parameters return
@@ -954,8 +952,7 @@ let is_thread_safe_method pdesc tenv =
     tenv (Procdesc.get_proc_name pdesc)
 
 let empty_post : ThreadSafetyDomain.summary =
-  { ThreadSafetyDomain.thumbs_up= true
-  ; threads= ThreadSafetyDomain.ThreadsDomain.Unknown
+  { threads= ThreadSafetyDomain.ThreadsDomain.Unknown
   ; locks= false
   ; accesses= ThreadSafetyDomain.AccessDomain.empty
   ; return_ownership= ThreadSafetyDomain.OwnershipAbstractValue.unowned
@@ -1011,7 +1008,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
         ({ThreadSafetyDomain.empty with ownership; threads}, IdAccessPathMapDomain.empty)
     in
     match Analyzer.compute_post proc_data ~initial ~debug:false with
-    | Some ({thumbs_up; threads; locks; accesses; ownership; attribute_map}, _)
+    | Some ({threads; locks; accesses; ownership; attribute_map}, _)
      -> let return_var_ap =
           AccessPath.of_pvar
             (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc))
@@ -1022,7 +1019,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
           try AttributeMapDomain.find return_var_ap attribute_map
           with Not_found -> AttributeSetDomain.empty
         in
-        let post = {thumbs_up; threads; locks; accesses; return_ownership; return_attributes} in
+        let post = {threads; locks; accesses; return_ownership; return_attributes} in
         Summary.update_summary post summary
     | None
      -> summary )

infer/src/checkers/ThreadSafetyDomain.ml

@@ -163,7 +163,6 @@ module ThreadsDomain = struct
   let is_main = function Main -> true | _ -> false
 end
 
-module ThumbsUpDomain = AbstractDomain.BooleanAnd
 module PathDomain = SinkTrace.Make (TraceElem)
 
 module Choice = struct
@@ -329,24 +328,22 @@ module AccessDomain = struct
 end
 
 type astate =
-  { thumbs_up: ThumbsUpDomain.astate
-  ; threads: ThreadsDomain.astate
+  { threads: ThreadsDomain.astate
   ; locks: LocksDomain.astate
   ; accesses: AccessDomain.astate
   ; ownership: OwnershipDomain.astate
   ; attribute_map: AttributeMapDomain.astate }
 
 let empty =
-  let thumbs_up = true in
   let threads = ThreadsDomain.Unknown in
   let locks = false in
   let accesses = AccessDomain.empty in
   let ownership = OwnershipDomain.empty in
   let attribute_map = AttributeMapDomain.empty in
-  {thumbs_up; threads; locks; accesses; ownership; attribute_map}
+  {threads; locks; accesses; ownership; attribute_map}
 
-let is_empty {thumbs_up; threads; locks; accesses; ownership; attribute_map} =
-  thumbs_up && ThreadsDomain.is_unknown threads && not locks && AccessDomain.is_empty accesses
+let is_empty {threads; locks; accesses; ownership; attribute_map} =
+  ThreadsDomain.is_unknown threads && not locks && AccessDomain.is_empty accesses
   && OwnershipDomain.is_empty ownership && AttributeMapDomain.is_empty attribute_map
 
 let ( <= ) ~lhs ~rhs =
@@ -359,18 +356,16 @@ let ( <= ) ~lhs ~rhs =
 let join astate1 astate2 =
   if phys_equal astate1 astate2 then astate1
   else
-    let thumbs_up = ThumbsUpDomain.join astate1.thumbs_up astate2.thumbs_up in
     let threads = ThreadsDomain.join astate1.threads astate2.threads in
     let locks = LocksDomain.join astate1.locks astate2.locks in
     let accesses = AccessDomain.join astate1.accesses astate2.accesses in
     let ownership = OwnershipDomain.join astate1.ownership astate2.ownership in
     let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in
-    {thumbs_up; threads; locks; accesses; ownership; attribute_map}
+    {threads; locks; accesses; ownership; attribute_map}
 
 let widen ~prev ~next ~num_iters =
   if phys_equal prev next then prev
   else
-    let thumbs_up = ThumbsUpDomain.widen ~prev:prev.thumbs_up ~next:next.thumbs_up ~num_iters in
     let threads = ThreadsDomain.widen ~prev:prev.threads ~next:next.threads ~num_iters in
     let locks = LocksDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in
     let accesses = AccessDomain.widen ~prev:prev.accesses ~next:next.accesses ~num_iters in
@@ -378,24 +373,22 @@ let widen ~prev ~next ~num_iters =
     let attribute_map =
       AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters
     in
-    {thumbs_up; threads; locks; accesses; ownership; attribute_map}
+    {threads; locks; accesses; ownership; attribute_map}
 
 type summary =
-  { thumbs_up: ThumbsUpDomain.astate
-  ; threads: ThreadsDomain.astate
+  { threads: ThreadsDomain.astate
   ; locks: LocksDomain.astate
   ; accesses: AccessDomain.astate
   ; return_ownership: OwnershipAbstractValue.astate
   ; return_attributes: AttributeSetDomain.astate }
 
-let pp_summary fmt {thumbs_up; threads; locks; accesses; return_ownership; return_attributes} =
+let pp_summary fmt {threads; locks; accesses; return_ownership; return_attributes} =
   F.fprintf fmt
-    "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\n"
-    ThumbsUpDomain.pp thumbs_up ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp
-    accesses OwnershipAbstractValue.pp return_ownership AttributeSetDomain.pp return_attributes
-
-let pp fmt {thumbs_up; threads; locks; accesses; ownership; attribute_map} =
-  F.fprintf fmt
-    "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\n Ownership: %a @\nAttributes: %a @\n"
-    ThumbsUpDomain.pp thumbs_up ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp
-    accesses OwnershipDomain.pp ownership AttributeMapDomain.pp attribute_map
+    "@\nThreads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\n"
+    ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses
+    OwnershipAbstractValue.pp return_ownership AttributeSetDomain.pp return_attributes
+
+let pp fmt {threads; locks; accesses; ownership; attribute_map} =
+  F.fprintf fmt "Threads: %a, Locks: %a @\nAccesses %a @\n Ownership: %a @\nAttributes: %a @\n"
+    ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp
+    ownership AttributeMapDomain.pp attribute_map

infer/src/checkers/ThreadSafetyDomain.mli

@@ -56,8 +56,6 @@ module ThreadsDomain : sig
   val is_main : astate -> bool
 end
 
-module ThumbsUpDomain : AbstractDomain.S with type astate = bool
-
 module PathDomain : module type of SinkTrace.Make (TraceElem)
 
 (** Powerset domain on the formal indexes in OwnedIf with a distinguished bottom element (Owned) and top element (Unowned) *)
@@ -165,8 +163,7 @@ module AccessDomain : sig
 end
 
 type astate =
-  { thumbs_up: ThumbsUpDomain.astate  (** boolean that is true if we think we have a proof *)
-  ; threads: ThreadsDomain.astate  (** current thread: main, background, or unknown *)
+  { threads: ThreadsDomain.astate  (** current thread: main, background, or unknown *)
   ; locks: LocksDomain.astate  (** boolean that is true if a lock must currently be held *)
   ; accesses: AccessDomain.astate
         (** read and writes accesses performed without ownership permissions *)
@@ -178,8 +175,7 @@ type astate =
     of the ownership/attributes associated with the return value as well as the set of formals which
     may escape *)
 type summary =
-  { thumbs_up: ThumbsUpDomain.astate
-  ; threads: ThreadsDomain.astate
+  { threads: ThreadsDomain.astate
   ; locks: LocksDomain.astate
   ; accesses: AccessDomain.astate
   ; return_ownership: OwnershipAbstractValue.astate