diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index e409dd526..0a8972f62 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -40,7 +40,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else let is_write = List.is_empty access_list && is_write_access in let access = TraceElem.make_field_access prefix_path' ~is_write loc in - let pre = OwnershipDomain.get_precondition prefix_path ownership in + let pre = OwnershipDomain.get_owned prefix_path ownership in let snapshot_opt = AccessSnapshot.make formals access locks threads pre in let access_acc' = AccessDomain.add_opt snapshot_opt acc in add_field_accesses prefix_path' access_acc' access_list @@ -59,7 +59,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let container_access = TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc in - let ownership_pre = OwnershipDomain.get_precondition receiver_ap astate.ownership in + let ownership_pre = OwnershipDomain.get_owned receiver_ap astate.ownership in AccessSnapshot.make formals container_access astate.locks astate.threads ownership_pre in let ownership_value = OwnershipDomain.get_owned receiver_ap astate.ownership in @@ -118,33 +118,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let add_callee_accesses formals (caller_astate : Domain.t) callee_accesses locks threads actuals callee_pname loc = let open Domain in - let conjoin_ownership_precondition actual_indexes actual_exp : - AccessSnapshot.OwnershipPrecondition.t = - match actual_exp with - | HilExp.Constant _ -> - (* the actual is a constant, so it's owned in the caller. *) - Conjunction actual_indexes - | HilExp.AccessExpression access_expr -> ( - match OwnershipDomain.get_owned access_expr caller_astate.ownership with - | OwnedIf formal_indexes -> - (* conditionally owned if [formal_indexes] are owned *) - Conjunction (IntSet.union formal_indexes actual_indexes) - | Unowned -> - (* not rooted in a formal and not conditionally owned *) - False ) - | _ -> - (* couldn't find access expr, don't know if it's owned. assume not *) - False - in - let update_ownership_precondition actual_index (acc : AccessSnapshot.OwnershipPrecondition.t) = + let update_ownership_precondition actual_index (acc : OwnershipAbstractValue.t) = match acc with - | False -> - (* precondition can't be satisfied *) + | Unowned -> + (* optimisation -- already unowned, don't compute ownership of remaining actuals *) acc - | Conjunction actual_indexes -> - List.nth actuals actual_index - (* optional args can result into missing actuals so simply ignore *) - |> Option.value_map ~default:acc ~f:(conjoin_ownership_precondition actual_indexes) + | actuals_ownership -> ( + match List.nth actuals actual_index with + | None -> + (* vararg methods can result into missing actuals so simply ignore *) + acc + | Some actual_exp -> + OwnershipDomain.ownership_of_expr actual_exp caller_astate.ownership + |> OwnershipAbstractValue.join actuals_ownership ) in let update_callee_access (snapshot : AccessSnapshot.t) acc = let access = TraceElem.with_callsite snapshot.access (CallSite.make callee_pname loc) in @@ -155,20 +141,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* update precondition with caller ownership info *) let ownership_precondition = match snapshot.ownership_precondition with - | Conjunction indexes -> - let empty_precondition = - AccessSnapshot.OwnershipPrecondition.Conjunction IntSet.empty - in - IntSet.fold update_ownership_precondition indexes empty_precondition - | False -> + | OwnedIf indexes -> + IntSet.fold update_ownership_precondition indexes OwnershipAbstractValue.owned + | Unowned -> snapshot.ownership_precondition in - if AccessSnapshot.OwnershipPrecondition.is_true ownership_precondition then - (* discard accesses to owned memory *) - acc - else - let snapshot_opt = AccessSnapshot.make formals access locks thread ownership_precondition in - AccessDomain.add_opt snapshot_opt acc + let snapshot_opt = AccessSnapshot.make formals access locks thread ownership_precondition in + AccessDomain.add_opt snapshot_opt acc in AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 0b58e04fe..13eae324c 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -260,32 +260,63 @@ module ThreadsDomain = struct match callee_astate with AnyThreadButSelf -> callee_astate | _ -> caller_astate end -module AccessSnapshot = struct - module OwnershipPrecondition = struct - type t = Conjunction of IntSet.t | False [@@deriving compare] +module OwnershipAbstractValue = struct + type t = OwnedIf of IntSet.t | Unowned [@@deriving compare] + + let owned = OwnedIf IntSet.empty + + let is_owned = function OwnedIf set -> IntSet.is_empty set | _ -> false - (* precondition is true if the conjunction of owned indexes is empty *) - let is_true = function False -> false | Conjunction set -> IntSet.is_empty set + let unowned = Unowned + + let make_owned_if formal_index = OwnedIf (IntSet.singleton formal_index) - let pp fmt = function - | Conjunction indexes -> - F.fprintf fmt "Owned(%a)" + let leq ~lhs ~rhs = + phys_equal lhs rhs + || + match (lhs, rhs) with + | _, Unowned -> + true (* Unowned is top *) + | Unowned, _ -> + false + | OwnedIf s1, OwnedIf s2 -> + IntSet.subset s1 s2 + + + let join astate1 astate2 = + if phys_equal astate1 astate2 then astate1 + else + match (astate1, astate2) with + | _, Unowned | Unowned, _ -> + Unowned + | OwnedIf s1, OwnedIf s2 -> + OwnedIf (IntSet.union s1 s2) + + + let widen ~prev ~next ~num_iters:_ = join prev next + + let pp fmt = function + | Unowned -> + F.pp_print_string fmt "Unowned" + | OwnedIf s -> + if IntSet.is_empty s then F.pp_print_string fmt "Owned" + else + F.fprintf fmt "OwnedIf%a" (PrettyPrintable.pp_collection ~pp_item:Int.pp) - (IntSet.elements indexes) - | False -> - F.pp_print_string fmt "False" - end + (IntSet.elements s) +end +module AccessSnapshot = struct type t = { access: TraceElem.t ; thread: ThreadsDomain.t ; lock: bool - ; ownership_precondition: OwnershipPrecondition.t } + ; ownership_precondition: OwnershipAbstractValue.t } [@@deriving compare] let make_if_not_owned formals access lock thread ownership_precondition = if - (not (OwnershipPrecondition.is_true ownership_precondition)) + (not (OwnershipAbstractValue.is_owned ownership_precondition)) && TraceElem.should_keep formals access then Some {access; lock; thread; ownership_precondition} else None @@ -303,13 +334,13 @@ module AccessSnapshot = struct let is_unprotected {thread; lock; ownership_precondition} = (not (ThreadsDomain.is_any_but_self thread)) && (not lock) - && not (OwnershipPrecondition.is_true ownership_precondition) + && not (OwnershipAbstractValue.is_owned ownership_precondition) let pp fmt {access; thread; lock; ownership_precondition} = F.fprintf fmt "Loc: %a Access: %a Thread: %a Lock: %b Pre: %a" Location.pp (TraceElem.get_loc access) TraceElem.pp access ThreadsDomain.pp thread lock - OwnershipPrecondition.pp ownership_precondition + OwnershipAbstractValue.pp ownership_precondition end module AccessDomain = struct @@ -327,50 +358,6 @@ module AccessDomain = struct Option.fold snapshot_opt ~init:astate ~f:(fun acc s -> add s acc) end -module OwnershipAbstractValue = struct - type t = OwnedIf of IntSet.t | Unowned [@@deriving compare] - - let owned = OwnedIf IntSet.empty - - let unowned = Unowned - - let make_owned_if formal_index = OwnedIf (IntSet.singleton formal_index) - - let leq ~lhs ~rhs = - phys_equal lhs rhs - || - match (lhs, rhs) with - | _, Unowned -> - true (* Unowned is top *) - | Unowned, _ -> - false - | OwnedIf s1, OwnedIf s2 -> - IntSet.subset s1 s2 - - - let join astate1 astate2 = - if phys_equal astate1 astate2 then astate1 - else - match (astate1, astate2) with - | _, Unowned | Unowned, _ -> - Unowned - | OwnedIf s1, OwnedIf s2 -> - OwnedIf (IntSet.union s1 s2) - - - let widen ~prev ~next ~num_iters:_ = join prev next - - let pp fmt = function - | Unowned -> - F.pp_print_string fmt "Unowned" - | OwnedIf s -> - if IntSet.is_empty s then F.pp_print_string fmt "Owned" - else - F.fprintf fmt "OwnedIf%a" - (PrettyPrintable.pp_collection ~pp_item:Int.pp) - (IntSet.elements s) -end - module OwnershipDomain = struct include AbstractDomain.Map (AccessExpression) (OwnershipAbstractValue) @@ -426,16 +413,6 @@ module OwnershipDomain = struct IntSet.fold get_ownership formal_indexes OwnershipAbstractValue.owned in add ret_access_exp ret_ownership_wrt_actuals ownership - - - let get_precondition exp t = - match get_owned exp t with - | OwnedIf formal_indexes -> - (* access expression conditionally owned if [formal_indexes] are owned *) - AccessSnapshot.OwnershipPrecondition.Conjunction formal_indexes - | Unowned -> - (* access expression not rooted in a formal and not conditionally owned *) - AccessSnapshot.OwnershipPrecondition.False end module Attribute = struct @@ -582,5 +559,5 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map} = let add_unannotated_call_access formals pname loc (astate : t) = let access = TraceElem.make_unannotated_call_access pname loc in - let snapshot = AccessSnapshot.make formals access astate.locks astate.threads False in + let snapshot = AccessSnapshot.make formals access astate.locks astate.threads Unowned in {astate with accesses= AccessDomain.add_opt snapshot astate.accesses} diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 3164c51bf..dc68bf712 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -83,27 +83,30 @@ module ThreadsDomain : sig (** integrate current state with a callee summary *) end -(** snapshot of the relevant state at the time of a heap access: concurrent thread(s), lock(s) held, - ownership precondition *) -module AccessSnapshot : sig - (** precondition for owned access; access is owned if it evaluates to true *) - module OwnershipPrecondition : sig - type t = - | Conjunction of IntSet.t - (** Conjunction of "formal index must be owned" predicates. true if empty *) - | False +module OwnershipAbstractValue : sig + type t = private + | OwnedIf of IntSet.t + (** Owned if the formals at the given indexes are owned in the caller; unconditionally owned + if the set of formals is empty = bottom of the lattice *) + | Unowned (** Unowned value; top of the lattice *) + + val owned : t - include PrettyPrintable.PrintableOrderedType with type t := t + val is_owned : t -> bool - val is_true : t -> bool - (** return [true] if the precondition evaluates to true *) - end + val make_owned_if : int -> t + val join : t -> t -> t +end + +(** snapshot of the relevant state at the time of a heap access: concurrent thread(s), lock(s) held, + ownership precondition *) +module AccessSnapshot : sig type t = private { access: TraceElem.t ; thread: ThreadsDomain.t ; lock: bool - ; ownership_precondition: OwnershipPrecondition.t } + ; ownership_precondition: OwnershipAbstractValue.t } include PrettyPrintable.PrintableOrderedType with type t := t @@ -112,7 +115,7 @@ module AccessSnapshot : sig -> TraceElem.t -> LocksDomain.t -> ThreadsDomain.t - -> OwnershipPrecondition.t + -> OwnershipAbstractValue.t -> t option val make_from_snapshot : FormalMap.t -> TraceElem.t -> t -> t option @@ -129,19 +132,6 @@ module AccessDomain : sig val add_opt : elt option -> t -> t end -module OwnershipAbstractValue : sig - type t = private - | OwnedIf of IntSet.t - (** Owned if the formals at the given indexes are owned in the caller; unconditionally owned - if the set of formals is empty = bottom of the lattice *) - | Unowned (** Unowned value; top of the lattice *) - [@@deriving compare] - - val owned : t - - val make_owned_if : int -> t -end - module OwnershipDomain : sig type t @@ -155,7 +145,7 @@ module OwnershipDomain : sig val propagate_return : AccessExpression.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t - val get_precondition : AccessExpression.t -> t -> AccessSnapshot.OwnershipPrecondition.t + val ownership_of_expr : HilExp.t -> t -> OwnershipAbstractValue.t end module Attribute : sig