From 9e91c9298b0f76d66fd030199c1d87c7902baf4b Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 10 Jan 2019 13:06:50 -0800 Subject: [PATCH] [racerd] remove redundant ownership constructor/state Reviewed By: jeremydubreil Differential Revision: D13489018 fbshipit-source-id: b94c50664 --- infer/src/concurrency/RacerD.ml | 28 ++++++----------- infer/src/concurrency/RacerDDomain.ml | 42 +++++++++++++------------- infer/src/concurrency/RacerDDomain.mli | 15 ++++++--- 3 files changed, 41 insertions(+), 44 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 59e2182b9..744951201 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -33,7 +33,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | access :: access_list -> ( let prefix_path' = (fst prefix_path, snd prefix_path @ [access]) in let add_field_access pre = - let access_acc' = AccessDomain.add pre access_acc in + let access_acc' = AccessDomain.add_opt pre access_acc in add_field_accesses prefix_path' access_acc' access_list in if RacerDModels.is_safe_access access prefix_path proc_data.tenv then @@ -49,17 +49,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct proc_data.pdesc in add_field_access pre - | OwnershipAbstractValue.Owned -> - add_field_accesses prefix_path' access_acc access_list | OwnershipAbstractValue.Unowned -> let pre = AccessSnapshot.make access locks threads False proc_data.pdesc in add_field_access pre ) in - List.fold - ~f:(fun acc access_expr -> + List.fold (HilExp.get_access_exprs exp) ~init:accesses ~f:(fun acc access_expr -> let base, accesses = HilExp.AccessExpression.to_access_path access_expr in add_field_accesses (base, []) acc accesses ) - ~init:accesses (HilExp.get_access_exprs exp) let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc @@ -78,7 +74,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (AccessSnapshot.OwnershipPrecondition.Conjunction (IntSet.singleton 0)) caller_pdesc in - AccessDomain.singleton snapshot + AccessDomain.add_opt snapshot AccessDomain.empty in (* if a container c is owned in cpp, make c[i] owned for all i *) let return_ownership = @@ -148,12 +144,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | None -> path in - let expand_precondition (snapshot : AccessSnapshot.t) = - let access' = TraceElem.map ~f:expand_path snapshot.access in - if phys_equal snapshot.access access' then snapshot - else AccessSnapshot.make_from_snapshot access' snapshot + let add snapshot acc = + let access' = TraceElem.map ~f:expand_path snapshot.AccessSnapshot.access in + let snapshot_opt' = AccessSnapshot.make_from_snapshot access' snapshot in + AccessDomain.add_opt snapshot_opt' acc in - AccessDomain.map expand_precondition accesses + AccessDomain.fold add accesses AccessDomain.empty let add_callee_accesses (caller_astate : Domain.t) callee_accesses locks threads actuals @@ -168,10 +164,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | HilExp.AccessExpression access_expr -> ( let actual_access_path = HilExp.AccessExpression.to_access_path access_expr in match OwnershipDomain.get_owned actual_access_path caller_astate.ownership with - | Owned -> - (* the actual passed to the current callee is owned. drop all the conditional - accesses for that actual, since they're all safe *) - Conjunction actual_indexes | OwnedIf formal_indexes -> (* access path conditionally owned if [formal_indexes] are owned *) Conjunction (IntSet.union formal_indexes actual_indexes) @@ -214,8 +206,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* discard accesses to owned memory *) acc else - let snapshot = AccessSnapshot.make access locks thread ownership_precondition pdesc in - AccessDomain.add snapshot acc + let snapshot_opt = AccessSnapshot.make access locks thread ownership_precondition pdesc 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 c5eb16208..1e83f237b 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -291,14 +291,16 @@ module AccessSnapshot = struct let make_from_snapshot access {lock; thread; ownership_precondition} = (* shouldn't be creating metadata for accesses that are known to be owned; we should discard such accesses *) - assert (not (OwnershipPrecondition.is_true ownership_precondition)) ; - {access; thread; lock; ownership_precondition} + Option.some_if + (not (OwnershipPrecondition.is_true ownership_precondition)) + {access; thread; lock; ownership_precondition} let make access lock thread ownership_precondition pdesc = - assert (not (OwnershipPrecondition.is_true ownership_precondition)) ; - let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in - {access; lock; thread; ownership_precondition} + if not (OwnershipPrecondition.is_true ownership_precondition) then + let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in + Some {access; lock; thread; ownership_precondition} + else None let is_unprotected {thread; lock; ownership_precondition} = @@ -321,12 +323,16 @@ module AccessDomain = struct |> Option.value_map ~default:false ~f:(fun ((v, _), _) -> should_skip_var v) in if skip then astate else add s astate + + + let add_opt snapshot_opt astate = + Option.fold snapshot_opt ~init:astate ~f:(fun acc s -> add s acc) end module OwnershipAbstractValue = struct - type t = Owned | OwnedIf of IntSet.t | Unowned [@@deriving compare] + type t = OwnedIf of IntSet.t | Unowned [@@deriving compare] - let owned = Owned + let owned = OwnedIf IntSet.empty let unowned = Unowned @@ -340,12 +346,8 @@ module OwnershipAbstractValue = struct true (* Unowned is top *) | Unowned, _ -> false - | Owned, _ -> - true (* Owned is bottom *) | OwnedIf s1, OwnedIf s2 -> IntSet.subset s1 s2 - | OwnedIf _, Owned -> - false let join astate1 astate2 = @@ -354,8 +356,6 @@ module OwnershipAbstractValue = struct match (astate1, astate2) with | _, Unowned | Unowned, _ -> Unowned - | astate, Owned | Owned, astate -> - astate | OwnedIf s1, OwnedIf s2 -> OwnedIf (IntSet.union s1 s2) @@ -366,11 +366,11 @@ module OwnershipAbstractValue = struct | Unowned -> F.pp_print_string fmt "Unowned" | OwnedIf s -> - F.fprintf fmt "OwnedIf%a" - (PrettyPrintable.pp_collection ~pp_item:Int.pp) - (IntSet.elements s) - | Owned -> - F.pp_print_string fmt "Owned" + 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 @@ -387,7 +387,7 @@ module OwnershipDomain = struct OwnershipAbstractValue.Unowned in match find access_path astate with - | (OwnershipAbstractValue.Owned | OwnedIf _) as v -> + | OwnershipAbstractValue.OwnedIf _ as v -> v | OwnershipAbstractValue.Unowned -> keep_looking access_path astate @@ -426,7 +426,7 @@ module OwnershipDomain = struct in let ret_ownership_wrt_actuals = match return_ownership with - | OwnershipAbstractValue.Owned | Unowned -> + | OwnershipAbstractValue.Unowned -> return_ownership | OwnershipAbstractValue.OwnedIf formal_indexes -> IntSet.fold get_ownership formal_indexes OwnershipAbstractValue.owned @@ -595,4 +595,4 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map} = let add_unannotated_call_access pname loc pdesc (astate : t) = let access = TraceElem.make_unannotated_call_access pname loc in let snapshot = AccessSnapshot.make access astate.locks astate.threads False pdesc in - {astate with accesses= AccessDomain.add snapshot astate.accesses} + {astate with accesses= AccessDomain.add_opt snapshot astate.accesses} diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 1a4fd672a..2559b0790 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -116,9 +116,9 @@ module AccessSnapshot : sig -> ThreadsDomain.t -> OwnershipPrecondition.t -> Procdesc.t - -> t + -> t option - val make_from_snapshot : PathDomain.Sink.t -> t -> t + val make_from_snapshot : PathDomain.Sink.t -> t -> t option val is_unprotected : t -> bool (** return true if not protected by lock, thread, or ownership *) @@ -126,12 +126,17 @@ end (** map of access metadata |-> set of accesses. the map should hold all accesses to a possibly-unowned access path *) -module AccessDomain : AbstractDomain.FiniteSetS with type elt = AccessSnapshot.t +module AccessDomain : sig + include AbstractDomain.FiniteSetS with type elt = AccessSnapshot.t + + val add_opt : elt option -> t -> t +end module OwnershipAbstractValue : sig type t = private - | Owned (** Owned value; bottom of the lattice *) - | OwnedIf of IntSet.t (** Owned if the formals at the given indexes are owned in the caller *) + | 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]