From 818d35967518b16c0093101c03676d5c1253a877 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 17 May 2018 03:18:13 -0700 Subject: [PATCH] [racerd] reorg domain module Summary: - Reorder modules in mli for readability. - Match mli module order in the implementation. - Move some functions that operate on domains from RacerD.ml to the domain file. - Kill some module type invocation. - Use standard module signatures. Reviewed By: mbouaziz Differential Revision: D8026386 fbshipit-source-id: ee2af22 --- infer/src/concurrency/RacerD.ml | 39 +--- infer/src/concurrency/RacerDDomain.ml | 306 +++++++++++++------------ infer/src/concurrency/RacerDDomain.mli | 116 +++++----- 3 files changed, 230 insertions(+), 231 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index a765d8515..8b54bd936 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -26,20 +26,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = Typ.Procname.t -> Procdesc.t option - let propagate_attributes lhs_access_path rhs_exp attribute_map = - let rhs_attributes = Domain.attributes_of_expr attribute_map rhs_exp in - Domain.AttributeMapDomain.add lhs_access_path rhs_attributes attribute_map - - - let propagate_ownership ((lhs_root, _) as lhs_access_path) rhs_exp ownership = - if Var.is_global (fst lhs_root) then - (* do not assign ownership to access paths rooted at globals *) - ownership - else - let rhs_ownership_value = Domain.ownership_of_expr rhs_exp ownership in - Domain.OwnershipDomain.add lhs_access_path rhs_ownership_value ownership - - let propagate_return return ret_ownership ret_attributes actuals {Domain.ownership; attribute_map} = let open Domain in @@ -286,7 +272,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let expand_precondition (snapshot: AccessSnapshot.t) = let access = TraceElem.map ~f:expand_path snapshot.access in - AccessSnapshot.make_ access snapshot.lock snapshot.thread snapshot.ownership_precondition + AccessSnapshot.make_from_snapshot access snapshot in AccessDomain.map expand_precondition accesses @@ -340,7 +326,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let update_callee_access (snapshot: AccessSnapshot.t) acc = let access = TraceElem.with_callsite snapshot.access (CallSite.make callee_pname loc) in - let locks = if snapshot.lock then LocksDomain.add_lock locks else locks in + let locks = if snapshot.lock then LocksDomain.acquire_lock locks else locks in let thread = ThreadsDomain.integrate_summary ~callee_astate:snapshot.thread ~caller_astate:threads in @@ -365,11 +351,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses - (***********************************************************************) - (* Wobbly paths and where to find them. *) - (***********************************************************************) - (***********************************************************************) - let exec_instr (astate: Domain.astate) ({ProcData.tenv; extras; pdesc} as proc_data) _ (instr: HilInstr.t) = let open Domain in @@ -436,11 +417,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match Models.get_lock callee_pname actuals with | Lock -> { astate with - locks= LocksDomain.add_lock astate.locks + locks= LocksDomain.acquire_lock astate.locks ; threads= update_for_lock_use astate.threads } | Unlock -> { astate with - locks= LocksDomain.remove_lock astate.locks + locks= LocksDomain.release_lock astate.locks ; threads= update_for_lock_use astate.threads } | LockedIfTrue -> let attribute_map = @@ -574,8 +555,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_access (AccessExpression lhs_access_expr) loc ~is_write_access:true rhs_accesses astate.locks astate.threads astate.ownership proc_data in - let ownership = propagate_ownership lhs_access_path rhs_exp astate.ownership in - let attribute_map = propagate_attributes lhs_access_path rhs_exp astate.attribute_map in + let ownership = + OwnershipDomain.propagate_assignment lhs_access_path rhs_exp astate.ownership + in + let attribute_map = + AttributeMapDomain.propagate_assignment lhs_access_path rhs_exp astate.attribute_map + in (* [TODO] Do not add this path as wobbly, if it's the _first_ initialization of a local variable (e.g. A z = getA(); --> now z is considered wobbly). @@ -621,8 +606,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let add_choice bool_value (acc: Domain.astate) = function | Choice.LockHeld -> let locks = - if bool_value then LocksDomain.add_lock acc.locks - else LocksDomain.remove_lock acc.locks + if bool_value then LocksDomain.acquire_lock acc.locks + else LocksDomain.release_lock acc.locks in {acc with locks} | Choice.OnMainThread -> diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index ae6a31035..c5e68929d 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -19,6 +19,8 @@ module Access = struct | InterfaceCall of Typ.Procname.t [@@deriving compare] + let equal = [%compare.equal : t] + let suffix_matches (_, accesses1) (_, accesses2) = match (List.rev accesses1, List.rev accesses2) with | access1 :: _, access2 :: _ -> @@ -44,6 +46,24 @@ module Access = struct if is_write then Write access_path else Read access_path + let make_container_access access_path pname ~is_write = + if is_write then ContainerWrite (access_path, pname) else ContainerRead (access_path, pname) + + + let is_write = function + | InterfaceCall _ | Read _ | ContainerRead _ -> + false + | ContainerWrite _ | Write _ -> + true + + + let is_container_write = function + | InterfaceCall _ | Read _ | Write _ | ContainerRead _ -> + false + | ContainerWrite _ -> + true + + let get_access_path = function | Read access_path | Write access_path @@ -67,8 +87,6 @@ module Access = struct intfcall - let equal t1 t2 = Int.equal (compare t1 t2) 0 - let pp fmt = function | Read access_path -> F.fprintf fmt "Read of %a" AccessPath.pp access_path @@ -88,21 +106,9 @@ module TraceElem = struct type t = {site: CallSite.t; kind: Kind.t} [@@deriving compare] - let is_write {kind} = - match kind with - | InterfaceCall _ | Read _ | ContainerRead _ -> - false - | ContainerWrite _ | Write _ -> - true - - - let is_container_write {kind} = - match kind with - | InterfaceCall _ | Read _ | Write _ | ContainerRead _ -> - false - | ContainerWrite _ -> - true + let is_write {kind} = Access.is_write kind + let is_container_write {kind} = Access.is_container_write kind let call_site {site} = site @@ -126,7 +132,7 @@ module TraceElem = struct let dummy_pname = Typ.Procname.empty_block - let make_dummy_site = CallSite.make dummy_pname + let make_dummy_site loc = CallSite.make dummy_pname loc (* all trace elems are created with a dummy call site. any trace elem without a dummy call site represents a call that leads to an access rather than a direct access *) @@ -134,11 +140,7 @@ module TraceElem = struct let make_container_access access_path pname ~is_write loc = let site = make_dummy_site loc in - let access = - if is_write then Access.ContainerWrite (access_path, pname) - else Access.ContainerRead (access_path, pname) - in - make access site + make (Access.make_container_access access_path pname ~is_write) site let make_field_access access_path ~is_write loc = @@ -151,6 +153,8 @@ module TraceElem = struct make (Access.InterfaceCall pname) site end +module PathDomain = SinkTrace.Make (TraceElem) + module LockCount = AbstractDomain.CountDomain (struct let max = 5 @@ -160,7 +164,7 @@ end) module LocksDomain = struct include AbstractDomain.Map (AccessPath) (LockCount) - (* TODO: eventually, we'll ask add_lock/remove_lock to pass the lock name. for now, this is a hack + (* TODO: eventually, we'll ask acquire_lock/release_lock to pass the lock name. for now, this is a hack to model having a single lock used everywhere *) let the_only_lock = ((Var.of_id (Ident.create Ident.knormal 0), Typ.void_star), []) @@ -171,12 +175,12 @@ module LocksDomain = struct let lookup_count lock astate = try find lock astate with Caml.Not_found -> LockCount.empty - let add_lock astate = + let acquire_lock astate = let count = lookup_count the_only_lock astate in add the_only_lock (LockCount.increment count) astate - let remove_lock astate = + let release_lock astate = let count = lookup_count the_only_lock astate in try let count' = LockCount.decrement count in @@ -199,6 +203,8 @@ module ThreadsDomain = struct (* NoThread < AnyThreadButSelf < Any *) let ( <= ) ~lhs ~rhs = + phys_equal lhs rhs + || match (lhs, rhs) with | NoThread, _ -> true @@ -213,13 +219,15 @@ module ThreadsDomain = struct let join astate1 astate2 = - match (astate1, astate2) with - | NoThread, astate | astate, NoThread -> - astate - | AnyThread, _ | _, AnyThread -> - AnyThread - | AnyThreadButSelf, AnyThreadButSelf -> - AnyThreadButSelf + if phys_equal astate1 astate2 then astate1 + else + match (astate1, astate2) with + | NoThread, astate | astate, NoThread -> + astate + | AnyThread, _ | _, AnyThread -> + AnyThread + | AnyThreadButSelf, AnyThreadButSelf -> + AnyThreadButSelf let widen ~prev ~next ~num_iters:_ = join prev next @@ -252,29 +260,53 @@ module ThreadsDomain = struct match callee_astate with AnyThreadButSelf -> callee_astate | _ -> caller_astate end -module PathDomain = SinkTrace.Make (TraceElem) +module AccessSnapshot = struct + module OwnershipPrecondition = struct + type t = Conjunction of IntSet.t | False [@@deriving compare] -module Choice = struct - type t = OnMainThread | LockHeld [@@deriving compare] + (* precondition is true if the conjunction of owned indexes is empty *) + let is_true = function False -> false | Conjunction set -> IntSet.is_empty set - let pp fmt = function - | OnMainThread -> - F.pp_print_string fmt "OnMainThread" - | LockHeld -> - F.pp_print_string fmt "LockHeld" -end + let pp fmt = function + | Conjunction indexes -> + F.fprintf fmt "Owned(%a)" + (PrettyPrintable.pp_collection ~pp_item:Int.pp) + (IntSet.elements indexes) + | False -> + F.pp_print_string fmt "False" + end -module Attribute = struct - type t = Functional | Choice of Choice.t [@@deriving compare] + type t = + { access: PathDomain.Sink.t + ; thread: ThreadsDomain.astate + ; lock: bool + ; ownership_precondition: OwnershipPrecondition.t } + [@@deriving compare] - let pp fmt = function - | Functional -> - F.pp_print_string fmt "Functional" - | Choice choice -> - Choice.pp fmt choice + 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} + + + 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} + + + let is_unprotected {thread; lock; ownership_precondition} = + not (ThreadsDomain.is_any_but_self thread) && not lock + && not (OwnershipPrecondition.is_true ownership_precondition) + + + let pp fmt {access; thread; lock; ownership_precondition} = + F.fprintf fmt "Access: %a Thread: %a Lock: %b Pre: %a" TraceElem.pp access ThreadsDomain.pp + thread lock OwnershipPrecondition.pp ownership_precondition end -module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute) +module AccessDomain = AbstractDomain.FiniteSet (AccessSnapshot) module OwnershipAbstractValue = struct type astate = Owned | OwnedIf of IntSet.t | Unowned [@@deriving compare] @@ -286,19 +318,19 @@ module OwnershipAbstractValue = struct let make_owned_if formal_index = OwnedIf (IntSet.singleton formal_index) let ( <= ) ~lhs ~rhs = - if phys_equal lhs rhs then true - else - match (lhs, rhs) with - | _, Unowned -> - true (* Unowned is top *) - | Unowned, _ -> - false - | Owned, _ -> - true (* Owned is bottom *) - | OwnedIf s1, OwnedIf s2 -> - IntSet.subset s1 s2 - | OwnedIf _, Owned -> - false + phys_equal lhs rhs + || + match (lhs, rhs) with + | _, Unowned -> + 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 = @@ -357,8 +389,51 @@ module OwnershipDomain = struct let find = `Use_get_owned_instead + + let rec ownership_of_expr expr ownership = + let open HilExp in + match expr with + | AccessExpression access_expr -> + get_owned (AccessExpression.to_access_path access_expr) ownership + | Constant _ -> + OwnershipAbstractValue.owned + | Exception e (* treat exceptions as transparent wrt ownership *) | Cast (_, e) -> + ownership_of_expr e ownership + | _ -> + OwnershipAbstractValue.unowned + + + let propagate_assignment ((lhs_root, _) as lhs_access_path) rhs_exp ownership = + if Var.is_global (fst lhs_root) then + (* do not assign ownership to access paths rooted at globals *) + ownership + else + let rhs_ownership_value = ownership_of_expr rhs_exp ownership in + add lhs_access_path rhs_ownership_value ownership +end + +module Choice = struct + type t = OnMainThread | LockHeld [@@deriving compare] + + let pp fmt = function + | OnMainThread -> + F.pp_print_string fmt "OnMainThread" + | LockHeld -> + F.pp_print_string fmt "LockHeld" end +module Attribute = struct + type t = Functional | Choice of Choice.t [@@deriving compare] + + let pp fmt = function + | Functional -> + F.pp_print_string fmt "Functional" + | Choice choice -> + Choice.pp fmt choice +end + +module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute) + module AttributeMapDomain = struct include AbstractDomain.InvertedMap (AccessPath) (AttributeSetDomain) @@ -373,9 +448,9 @@ module AttributeMapDomain = struct let get_choices access_path t = try let attributes = find access_path t in - List.filter_map - ~f:(function Attribute.Choice c -> Some c | _ -> None) - (AttributeSetDomain.elements attributes) + AttributeSetDomain.fold + (fun cc acc -> match cc with Attribute.Choice c -> c :: acc | _ -> acc) + attributes [] with Caml.Not_found -> [] @@ -385,55 +460,33 @@ module AttributeMapDomain = struct |> AttributeSetDomain.add attribute in add access_path attribute_set t -end - -module AccessSnapshot = struct - module OwnershipPrecondition = struct - type t = Conjunction of IntSet.t | False [@@deriving compare] - - (* precondition is true if the conjunction of owned indexes is empty *) - let is_true = function False -> false | Conjunction set -> IntSet.is_empty set - - let pp fmt = function - | Conjunction indexes -> - F.fprintf fmt "Owned(%a)" - (PrettyPrintable.pp_collection ~pp_item:Int.pp) - (IntSet.elements indexes) - | False -> - F.pp_print_string fmt "False" - end - - type t = - { access: PathDomain.Sink.t - ; thread: ThreadsDomain.astate - ; lock: bool - ; ownership_precondition: OwnershipPrecondition.t } - [@@deriving compare] - - let make_ 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} - let make access lock thread ownership_precondition pdesc = - let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in - make_ access lock thread ownership_precondition - - - let is_unprotected {thread; lock; ownership_precondition} = - not (ThreadsDomain.is_any_but_self thread) && not lock - && not (OwnershipPrecondition.is_true ownership_precondition) - - - let pp fmt {access; thread; lock; ownership_precondition} = - F.fprintf fmt "Access: %a Thread: %a Lock: %b Pre: %a" TraceElem.pp access ThreadsDomain.pp - thread lock OwnershipPrecondition.pp ownership_precondition + let rec attributes_of_expr attribute_map e = + let open HilExp in + match e with + | HilExp.AccessExpression access_expr -> ( + try find (AccessExpression.to_access_path access_expr) attribute_map with Caml.Not_found -> + AttributeSetDomain.empty ) + | Constant _ -> + AttributeSetDomain.singleton Attribute.Functional + | Exception expr (* treat exceptions as transparent wrt attributes *) | Cast (_, expr) -> + attributes_of_expr attribute_map expr + | UnaryOperator (_, expr, _) -> + attributes_of_expr attribute_map expr + | BinaryOperator (_, expr1, expr2) -> + let attributes1 = attributes_of_expr attribute_map expr1 in + let attributes2 = attributes_of_expr attribute_map expr2 in + AttributeSetDomain.join attributes1 attributes2 + | Closure _ | Sizeof _ -> + AttributeSetDomain.empty + + + let propagate_assignment lhs_access_path rhs_exp attribute_map = + let rhs_attributes = attributes_of_expr attribute_map rhs_exp in + add lhs_access_path rhs_attributes attribute_map end -module AccessDomain = AbstractDomain.FiniteSet (AccessSnapshot) - module StabilityDomain = struct include AccessTree.PathSet (AccessTree.DefaultConfig) @@ -629,36 +682,3 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map; wobbly_paths} = Non-stable Paths: %a@\n" ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp ownership AttributeMapDomain.pp attribute_map StabilityDomain.pp wobbly_paths - - -let rec attributes_of_expr attribute_map e = - let open HilExp in - match e with - | HilExp.AccessExpression access_expr -> ( - try AttributeMapDomain.find (AccessExpression.to_access_path access_expr) attribute_map - with Caml.Not_found -> AttributeSetDomain.empty ) - | Constant _ -> - AttributeSetDomain.of_list [Attribute.Functional] - | Exception expr (* treat exceptions as transparent wrt attributes *) | Cast (_, expr) -> - attributes_of_expr attribute_map expr - | UnaryOperator (_, expr, _) -> - attributes_of_expr attribute_map expr - | BinaryOperator (_, expr1, expr2) -> - let attributes1 = attributes_of_expr attribute_map expr1 in - let attributes2 = attributes_of_expr attribute_map expr2 in - AttributeSetDomain.join attributes1 attributes2 - | Closure _ | Sizeof _ -> - AttributeSetDomain.empty - - -let rec ownership_of_expr expr ownership = - let open HilExp in - match expr with - | AccessExpression access_expr -> - OwnershipDomain.get_owned (AccessExpression.to_access_path access_expr) ownership - | Constant _ -> - OwnershipAbstractValue.owned - | Exception e (* treat exceptions as transparent wrt ownership *) | Cast (_, e) -> - ownership_of_expr e ownership - | _ -> - OwnershipAbstractValue.unowned diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index ac141751a..16d6132f4 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -18,7 +18,8 @@ module Access : sig | ContainerWrite of AccessPath.t * Typ.Procname.t (** Write to container object *) | InterfaceCall of Typ.Procname.t (** Call to method of interface not annotated with @ThreadSafe *) - [@@deriving compare] + + include PrettyPrintable.PrintableOrderedType with type t := t val matches : caller:t -> callee:t -> bool (** returns true if the caller access matches the callee access after accounting for mismatch @@ -27,8 +28,6 @@ module Access : sig val get_access_path : t -> AccessPath.t option val equal : t -> t -> bool - - val pp : F.formatter -> t -> unit end module TraceElem : sig @@ -51,18 +50,17 @@ module TraceElem : sig val make_unannotated_call_access : Typ.Procname.t -> Location.t -> t end +module PathDomain : + SinkTrace.S with module Source = Source.Dummy and module Sink = SinkTrace.MakeSink(TraceElem) + (** Overapproximation of number of locks that are currently held *) module LocksDomain : sig include AbstractDomain.WithBottom - val is_locked : astate -> bool - [@@warning "-32"] - (** returns true if the number of locks held is greater than zero or Top *) - - val add_lock : astate -> astate + val acquire_lock : astate -> astate (** record acquisition of a lock *) - val remove_lock : astate -> astate + val release_lock : astate -> astate (** record release of a lock *) val integrate_summary : caller_astate:astate -> callee_astate:astate -> astate @@ -81,7 +79,7 @@ module ThreadsDomain : sig (** Current thread can run in parallel with other threads, but not with a copy of itself. (concretization : { t | t \in TIDs ^ t != t_cur } ) *) | AnyThread - (** Current thread can run in parallel with any thread, including itself (concretization: + (** Current thread can run in parallel with any thread, including itself (concretization: set of all TIDs ) *) include AbstractDomain.WithBottom with type astate := astate @@ -95,9 +93,47 @@ module ThreadsDomain : sig (** integrate current state with a callee summary *) end -module PathDomain : module type of SinkTrace.Make (TraceElem) +(** 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 + + include PrettyPrintable.PrintableOrderedType with type t := t + + val is_true : t -> bool + (** return [true] if the precondition evaluates to true *) + end -(** Powerset domain on the formal indexes in OwnedIf with a distinguished bottom element (Owned) and top element (Unowned) *) + type t = private + { access: PathDomain.Sink.t + ; thread: ThreadsDomain.astate + ; lock: bool + ; ownership_precondition: OwnershipPrecondition.t } + + include PrettyPrintable.PrintableOrderedType with type t := t + + val make : + PathDomain.Sink.t -> LocksDomain.astate -> ThreadsDomain.astate -> OwnershipPrecondition.t + -> Procdesc.t -> t + + val make_from_snapshot : PathDomain.Sink.t -> t -> t + + val is_unprotected : t -> bool + (** return true if not protected by lock, thread, or ownership *) +end + +(** map of access metadata |-> set of accesses. the map should hold all accesses to a + possibly-unowned access path *) +module AccessDomain : module type of AbstractDomain.FiniteSet (AccessSnapshot) + +(** Powerset domain on the formal indexes in OwnedIf with a distinguished bottom element (Owned) + and top element (Unowned) *) module OwnershipAbstractValue : sig type astate = private | Owned (** Owned value; bottom of the lattice *) @@ -122,6 +158,8 @@ module OwnershipDomain : sig val is_owned : AccessPath.t -> astate -> bool val find : [`Use_get_owned_instead] [@@warning "-32"] + + val propagate_assignment : AccessPath.t -> HilExp.t -> astate -> astate end (** attribute attached to a boolean variable specifying what it means when the boolean is true *) @@ -129,16 +167,16 @@ module Choice : sig type t = | OnMainThread (** the current procedure is running on the main thread *) | LockHeld (** a lock is currently held *) - [@@deriving compare] + + include PrettyPrintable.PrintableOrderedType with type t := t end module Attribute : sig type t = | Functional (** holds a value returned from a callee marked @Functional *) | Choice of Choice.t (** holds a boolean choice variable *) - [@@deriving compare] - val pp : F.formatter -> t -> unit + include PrettyPrintable.PrintableOrderedType with type t := t end module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute) @@ -154,48 +192,11 @@ module AttributeMapDomain : sig (** get the choice attributes associated with the given access path *) val add_attribute : AccessPath.t -> Attribute.t -> astate -> astate -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 - [@@deriving compare] - - val is_true : t -> bool - (** return [true] if the precondition evaluates to true *) - - val pp : F.formatter -> t -> unit [@@warning "-32"] - end - type t = private - { access: PathDomain.Sink.t - ; thread: ThreadsDomain.astate - ; lock: bool - ; ownership_precondition: OwnershipPrecondition.t } - [@@deriving compare] - - val make : - PathDomain.Sink.t -> LocksDomain.astate -> ThreadsDomain.astate -> OwnershipPrecondition.t - -> Procdesc.t -> t - - val make_ : PathDomain.Sink.t -> bool -> ThreadsDomain.astate -> OwnershipPrecondition.t -> t - - val is_unprotected : t -> bool - (** return true if not protected by lock, thread, or ownership *) - - val pp : F.formatter -> t -> unit + val propagate_assignment : AccessPath.t -> HilExp.t -> astate -> astate + (** propagate attributes from the leaves to the root of an RHS Hil expression *) end -(** map of access metadata |-> set of accesses. the map should hold all accesses to a - possibly-unowned access path *) -module AccessDomain : module type of AbstractDomain.FiniteSet (AccessSnapshot) - module StabilityDomain : sig include module type of AccessTree.PathSet (AccessTree.DefaultConfig) @@ -233,10 +234,3 @@ type summary = include AbstractDomain.WithBottom with type astate := astate val pp_summary : F.formatter -> summary -> unit - -val attributes_of_expr : - AttributeSetDomain.t AttributeMapDomain.t -> HilExp.t -> AttributeSetDomain.t -(** propagate attributes from the leaves to the root of an RHS Hil expression *) - -val ownership_of_expr : - HilExp.t -> OwnershipAbstractValue.astate AttributeMapDomain.t -> OwnershipAbstractValue.astate