diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 8dad74349..a7be5e327 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -632,46 +632,29 @@ module CountDomain (MaxCount : MaxCount) = struct let pp = Int.pp end -module StackDomain (Element : PrettyPrintable.PrintableOrderedType) = struct - type t = Element.t list +module DownwardIntDomain (MaxCount : MaxCount) = struct + type t = int - let push = List.cons + let bottom = + assert (MaxCount.max > 0) ; + MaxCount.max - let pop = List.tl_exn - let is_top = List.is_empty + let top = 0 - let top = [] + let is_top = Int.equal top - let pp fmt x = Pp.semicolon_seq Element.pp fmt x + let is_bottom = Int.equal bottom - (* is (rev rhs) a prefix of (rev lhs)? *) - let ( <= ) ~lhs ~rhs = - let rec aux lhs rhs = - match (lhs, rhs) with - | _, [] -> - true - | [], _ -> - false - | x :: _, y :: _ when not (Int.equal 0 (Element.compare x y)) -> - false - | _ :: xs, _ :: ys -> - aux xs ys - in - phys_equal lhs rhs || aux (List.rev lhs) (List.rev rhs) + let ( <= ) ~lhs ~rhs = lhs >= rhs + let join astate1 astate2 = Int.min astate1 astate2 - (* compute (rev (longest common prefix)) *) - let join lhs rhs = - let rec aux acc a b = - match (a, b) with - | x :: xs, y :: ys when Int.equal 0 (Element.compare x y) -> - aux (x :: acc) xs ys - | _, _ -> - acc - in - if phys_equal lhs rhs then lhs else aux [] (List.rev lhs) (List.rev rhs) + let widen ~prev ~next ~num_iters:_ = join prev next + let increment astate = if is_bottom astate then astate else astate + 1 - let widen ~prev ~next ~num_iters:_ = join prev next + let decrement astate = if is_top astate then astate else astate - 1 + + let pp = Int.pp end diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 7e19e653c..6d19980a0 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -258,7 +258,7 @@ module type MaxCount = sig end (** Domain keeping a non-negative count with a bounded maximum value. The count can be only - incremented and decremented *) + incremented and decremented. *) module CountDomain (MaxCount : MaxCount) : sig include WithBottom with type t = private int @@ -275,15 +275,18 @@ module CountDomain (MaxCount : MaxCount) : sig (** capped sum of two states *) end -(** Domain whose members are stacks of elements (lists, last pushed is head of the list), - partially ordered by the prefix relation ([c;b;a] <= [b;a]), and whose join computes the - longest common prefix (so [c;b;a] join [f;g;b;c;a] = [a]), so the top element is the empty - stack. *) -module StackDomain (Element : PrettyPrintable.PrintableOrderedType) : sig - include WithTop with type t = Element.t list +(** Domain keeping a non-negative count with a bounded maximum value. + [join] is minimum and [top] is zero. *) +module DownwardIntDomain (MaxCount : MaxCount) : sig + (** top is zero *) + include WithTop with type t = private int - val push : Element.t -> t -> t + (** bottom is the provided maximum *) + include WithBottom with type t := t + + val increment : t -> t + (** bump the count by one if this won't cross the maximum *) - val pop : t -> t - (** throws exception on empty/top *) + val decrement : t -> t + (** decrease the count by one if it is greater than 0 *) end diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index d87bb1b5a..78b6e3088 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -131,8 +131,14 @@ module LockState : sig val get_acquisitions : t -> Acquisitions.t end = struct - module LockStack = AbstractDomain.StackDomain (Acquisition) - module Map = AbstractDomain.InvertedMap (Lock) (LockStack) + (* abstraction limit for lock counts *) + let max_lock_depth_allowed = 5 + + module LockCount = AbstractDomain.DownwardIntDomain (struct + let max = max_lock_depth_allowed + end) + + module Map = AbstractDomain.InvertedMap (Lock) (LockCount) (* [acquisitions] has the currently held locks, so as to avoid a linear fold in [get_acquisitions]. This should also increase sharing across returned values from [get_acquisitions]. *) @@ -170,36 +176,51 @@ end = struct false - let get_stack lock map = Map.find_opt lock map |> Option.value ~default:LockStack.top - let acquire ~procname ~loc lock {map; acquisitions} = - let acquisition = Acquisition.make ~procname ~loc lock in - let current_value = get_stack lock map in - let new_value = LockStack.push acquisition current_value in - let map = Map.add lock new_value map in + let should_add_acquisition = ref false in + let map = + Map.update lock + (function + | None -> + (* lock was not already held, so add it to [acquisitions] *) + should_add_acquisition := true ; + Some LockCount.(increment top) + | Some count -> + Some (LockCount.increment count) ) + map + in let acquisitions = - (* add new acquisition only if lock was not held before *) - if LockStack.is_top current_value then Acquisitions.add acquisition acquisitions + if !should_add_acquisition then + let acquisition = Acquisition.make ~procname ~loc lock in + Acquisitions.add acquisition acquisitions else acquisitions in {map; acquisitions} - let release lock ({map; acquisitions} as astate) = - let current_value = get_stack lock map in - if LockStack.is_top current_value then (* lock was not held *) astate - else - let new_value = LockStack.pop current_value in - if LockStack.is_top new_value then - (* lock is now not held *) - let map = Map.remove lock map in + let release lock {map; acquisitions} = + let should_remove_acquisition = ref false in + let map = + Map.update lock + (function + | None -> + None + | Some count -> + let new_count = LockCount.decrement count in + if LockCount.is_top new_count then ( + (* lock was held, but now it is not, so remove from [aqcuisitions] *) + should_remove_acquisition := true ; + None ) + else Some new_count ) + map + in + let acquisitions = + if !should_remove_acquisition then let acquisition = Acquisition.make_dummy lock in - let acquisitions = Acquisitions.remove acquisition acquisitions in - {map; acquisitions} - else - (* lock is still held as it was acquired more than once *) - let map = Map.add lock new_value map in - {map; acquisitions} + Acquisitions.remove acquisition acquisitions + else acquisitions + in + {map; acquisitions} end module CriticalPairElement = struct