diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index fd8cd6b7b..da1194d6e 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/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 diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 782ab79bf..2b36d9db6 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/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 diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 391f8d860..6fd7cbcdc 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/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, _ -> diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 8c8e669fb..6499d06fd 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/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 diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 1cbfc06a0..d660512f9 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/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.