[racerd] fix lock count treatment at method calls

Reviewed By: sblackshear

Differential Revision: D7055465

fbshipit-source-id: a6dffe0

infer/src/absint/AbstractDomain.ml

@@ -323,6 +323,8 @@ module CountDomain (MaxCount : MaxCount) = struct
 
   let widen ~prev ~next ~num_iters:_ = join prev next
 
+  let add astate1 astate2 = Int.min top (astate1 + astate2)
+
   let increment astate = if is_top astate then top else astate + 1
 
   let decrement astate = if is_empty astate then empty else astate - 1

infer/src/absint/AbstractDomain.mli

@@ -130,4 +130,7 @@ module CountDomain (MaxCount : MaxCount) : sig
 
   val decrement : astate -> astate
   (** descrease the count by one if it is greater than 0 *)
+
+  val add : astate -> astate -> astate
+  (** capped sum of two states *)
 end

infer/src/concurrency/RacerD.ml

@@ -495,7 +495,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                     ; return_ownership
                     ; return_attributes
                     ; wobbly_paths= callee_wps } ->
-                    let locks = LocksDomain.join locks astate.locks in
+                    let locks =
+                      LocksDomain.integrate_summary ~caller_astate:astate.locks
+                        ~callee_astate:locks
+                    in
                     let threads =
                       match (astate.threads, threads) with
                       | _, ThreadsDomain.AnyThreadButSelf | AnyThreadButSelf, _ ->

infer/src/concurrency/RacerDDomain.ml

@@ -169,18 +169,27 @@ module LocksDomain = struct
     not (is_empty astate)
 
 
+  let lookup_count lock astate = try find lock astate with Not_found -> LockCount.empty
+
   let add_lock astate =
-    let count = try find the_only_lock astate with Not_found -> LockCount.empty in
+    let count = lookup_count the_only_lock astate in
     add the_only_lock (LockCount.increment count) astate
 
 
   let remove_lock astate =
+    let count = lookup_count the_only_lock astate in
     try
-      let count = find the_only_lock astate in
       let count' = LockCount.decrement count in
       if LockCount.is_empty count' then remove the_only_lock astate
       else add the_only_lock count' astate
     with Not_found -> astate
+
+
+  let integrate_summary ~caller_astate ~callee_astate =
+    let caller_count = lookup_count the_only_lock caller_astate in
+    let callee_count = lookup_count the_only_lock callee_astate in
+    let sum = LockCount.add caller_count callee_count in
+    if LockCount.is_empty sum then caller_astate else add the_only_lock sum caller_astate
 end
 
 module ThreadsDomain = struct

infer/src/concurrency/RacerDDomain.mli

@@ -64,6 +64,9 @@ module LocksDomain : sig
 
   val remove_lock : astate -> astate
   (** record release of a lock *)
+
+  val integrate_summary : caller_astate:astate -> callee_astate:astate -> astate
+  (** integrate current state with a callee summary *)
 end
 
 (** Abstraction of threads that may run in parallel with the current thread.