[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

@@ -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 ownership =
-        let attribute_map = propagate_attributes lhs_access_path rhs_exp astate.attribute_map in
+          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
+                if bool_value then LocksDomain.acquire_lock acc.locks
-                else LocksDomain.remove_lock acc.locks
+                else LocksDomain.release_lock acc.locks
               in
               {acc with locks}
           | Choice.OnMainThread ->

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} =
+  let is_write {kind} = Access.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_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 =
+    make (Access.make_container_access access_path pname ~is_write) site
-      if is_write then Access.ContainerWrite (access_path, pname)
-      else Access.ContainerRead (access_path, pname)
-    in
-    make access 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
+    if phys_equal astate1 astate2 then astate1
-    | NoThread, astate | astate, NoThread ->
+    else
-        astate
+      match (astate1, astate2) with
-    | AnyThread, _ | _, AnyThread ->
+      | NoThread, astate | astate, NoThread ->
-        AnyThread
+          astate
-    | AnyThreadButSelf, AnyThreadButSelf ->
+      | AnyThread, _ | _, AnyThread ->
-        AnyThreadButSelf
+          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
+    (* precondition is true if the conjunction of owned indexes is empty *)
-  type t = OnMainThread | LockHeld [@@deriving compare]
+    let is_true = function False -> false | Conjunction set -> IntSet.is_empty set
 
-  let pp fmt = function
+    let pp fmt = function
-    | OnMainThread ->
+      | Conjunction indexes ->
-        F.pp_print_string fmt "OnMainThread"
+          F.fprintf fmt "Owned(%a)"
-    | LockHeld ->
+            (PrettyPrintable.pp_collection ~pp_item:Int.pp)
-        F.pp_print_string fmt "LockHeld"
+            (IntSet.elements indexes)
-end
+      | False ->
+          F.pp_print_string fmt "False"
+  end
 
-module Attribute = struct
+  type t =
-  type t = Functional | Choice of Choice.t [@@deriving compare]
+    { access: PathDomain.Sink.t
+    ; thread: ThreadsDomain.astate
+    ; lock: bool
+    ; ownership_precondition: OwnershipPrecondition.t }
+  [@@deriving compare]
 
-  let pp fmt = function
+  let make_from_snapshot access {lock; thread; ownership_precondition} =
-    | Functional ->
+    (* shouldn't be creating metadata for accesses that are known to be owned; we should discard
-        F.pp_print_string fmt "Functional"
+       such accesses *)
-    | Choice choice ->
+    assert (not (OwnershipPrecondition.is_true ownership_precondition)) ;
-        Choice.pp fmt choice
+    {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
+    phys_equal lhs rhs
-    else
+    ||
-      match (lhs, rhs) with
+    match (lhs, rhs) with
-      | _, Unowned ->
+    | _, Unowned ->
-          true (* Unowned is top *)
+        true (* Unowned is top *)
-      | Unowned, _ ->
+    | Unowned, _ ->
-          false
+        false
-      | Owned, _ ->
+    | Owned, _ ->
-          true (* Owned is bottom *)
+        true (* Owned is bottom *)
-      | OwnedIf s1, OwnedIf s2 ->
+    | OwnedIf s1, OwnedIf s2 ->
-          IntSet.subset s1 s2
+        IntSet.subset s1 s2
-      | OwnedIf _, Owned ->
+    | OwnedIf _, Owned ->
-          false
+        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
+      AttributeSetDomain.fold
-        ~f:(function Attribute.Choice c -> Some c | _ -> None)
+        (fun cc acc -> match cc with Attribute.Choice c -> c :: acc | _ -> acc)
-        (AttributeSetDomain.elements attributes)
+        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 rec attributes_of_expr attribute_map e =
-    let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in
+    let open HilExp in
-    make_ access lock thread ownership_precondition
+    match e with
-
+    | HilExp.AccessExpression access_expr -> (
-
+      try find (AccessExpression.to_access_path access_expr) attribute_map with Caml.Not_found ->
-  let is_unprotected {thread; lock; ownership_precondition} =
+        AttributeSetDomain.empty )
-    not (ThreadsDomain.is_any_but_self thread) && not lock
+    | Constant _ ->
-    && not (OwnershipPrecondition.is_true ownership_precondition)
+        AttributeSetDomain.singleton Attribute.Functional
-
+    | Exception expr (* treat exceptions as transparent wrt attributes *) | Cast (_, expr) ->
-
+        attributes_of_expr attribute_map expr
-  let pp fmt {access; thread; lock; ownership_precondition} =
+    | UnaryOperator (_, expr, _) ->
-    F.fprintf fmt "Access: %a Thread: %a Lock: %b Pre: %a" TraceElem.pp access ThreadsDomain.pp
+        attributes_of_expr attribute_map expr
-      thread lock OwnershipPrecondition.pp ownership_precondition
+    | 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

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
+  val acquire_lock : astate -> astate
-    [@@warning "-32"]
-  (** returns true if the number of locks held is greater than zero or Top *)
-
-  val add_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
+  val propagate_assignment : AccessPath.t -> HilExp.t -> astate -> astate
-    { access: PathDomain.Sink.t
+  (** propagate attributes from the leaves to the root of an RHS Hil expression *)
-    ; 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
 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