[AI] kill astate type

Reviewed By: mbouaziz

Differential Revision: D10119192

fbshipit-source-id: 4868cbcb1

infer/src/absint/AbstractDomain.ml

@@ -19,21 +19,17 @@ open! Types
 exception Stop_analysis
 
 module type S = sig
-  type astate
+  include PrettyPrintable.PrintableType
 
-  val ( <= ) : lhs:astate -> rhs:astate -> bool
+  val ( <= ) : lhs:t -> rhs:t -> bool
 
-  (* fst \sqsubseteq snd? *)
+  val join : t -> t -> t
 
-  val join : astate -> astate -> astate
+  val widen : prev:t -> next:t -> num_iters:int -> t
-
-  val widen : prev:astate -> next:astate -> num_iters:int -> astate
-
-  val pp : F.formatter -> astate -> unit
 end
 
-module Empty : S with type astate = unit = struct
+module Empty : S with type t = unit = struct
-  type astate = unit
+  type t = unit
 
   let ( <= ) ~lhs:() ~rhs:() = true
 
@@ -47,19 +43,19 @@ end
 module type WithBottom = sig
   include S
 
-  val empty : astate
+  val empty : t
 
-  val is_empty : astate -> bool
+  val is_empty : t -> bool
 end
 
 module type WithTop = sig
   include S
 
-  val top : astate
+  val top : t
 end
 
 module BottomLifted (Domain : S) = struct
-  type astate = Domain.astate bottom_lifted
+  type t = Domain.t bottom_lifted
 
   let empty = Bottom
 
@@ -109,7 +105,7 @@ module BottomLifted (Domain : S) = struct
 end
 
 module TopLifted (Domain : S) = struct
-  type astate = Domain.astate top_lifted
+  type t = Domain.t top_lifted
 
   let top = Top
 
@@ -153,7 +149,7 @@ module TopLifted (Domain : S) = struct
 end
 
 module Pair (Domain1 : S) (Domain2 : S) = struct
-  type astate = Domain1.astate * Domain2.astate
+  type t = Domain1.t * Domain2.t
 
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true
@@ -177,7 +173,7 @@ module Pair (Domain1 : S) (Domain2 : S) = struct
 end
 
 module Flat (V : PrettyPrintable.PrintableEquatableType) = struct
-  type astate = Bot | V of V.t | Top
+  type t = Bot | V of V.t | Top
 
   let empty = Bot
 
@@ -223,11 +219,15 @@ module Flat (V : PrettyPrintable.PrintableEquatableType) = struct
   let get = function V v -> Some v | Bot | Top -> None
 end
 
+module type FiniteSetS = sig
+  include PrettyPrintable.PPSet
+
+  include WithBottom with type t := t
+end
+
 module FiniteSetOfPPSet (S : PrettyPrintable.PPSet) = struct
   include S
 
-  type astate = t
-
   let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else subset lhs rhs
 
   let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else union astate1 astate2
@@ -238,11 +238,15 @@ end
 module FiniteSet (Element : PrettyPrintable.PrintableOrderedType) =
   FiniteSetOfPPSet (PrettyPrintable.MakePPSet (Element))
 
+module type InvertedSetS = sig
+  include PrettyPrintable.PPSet
+
+  include S with type t := t
+end
+
 module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) = struct
   include PrettyPrintable.MakePPSet (Element)
 
-  type astate = t
-
   let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else subset rhs lhs
 
   let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else inter astate1 astate2
@@ -250,10 +254,18 @@ module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) = struct
   let widen ~prev ~next ~num_iters:_ = join prev next
 end
 
+module type MapS = sig
+  include PrettyPrintable.PPMonoMap
+
+  include WithBottom with type t := t
+end
+
 module MapOfPPMap (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
-  include M
+  include (M : PrettyPrintable.PPMap with type 'a t := 'a M.t and type key = M.key)
 
-  type astate = ValueDomain.astate M.t
+  type t = ValueDomain.t M.t
+
+  type value = ValueDomain.t
 
   (** true if all keys in [lhs] are in [rhs], and each lhs value <= corresponding rhs value *)
   let ( <= ) ~lhs ~rhs =
@@ -298,26 +310,31 @@ module MapOfPPMap (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
   let pp fmt astate = M.pp ~pp_value:ValueDomain.pp fmt astate
 end
 
-module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) =
+module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = struct
-  MapOfPPMap (PrettyPrintable.MakePPMap (Key)) (ValueDomain)
-
-module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = struct
   module M = PrettyPrintable.MakePPMap (Key)
-  include M
+  include MapOfPPMap (M) (ValueDomain)
+end
 
-  type astate = ValueDomain.astate M.t
+module type InvertedMapS = sig
+  include PrettyPrintable.PPMonoMap
+
+  include S with type t := t
+end
+
+module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = struct
+  include PrettyPrintable.MakePPMonoMap (Key) (ValueDomain)
 
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true
     else
-      try M.for_all (fun k rhs_v -> ValueDomain.( <= ) ~lhs:(M.find k lhs) ~rhs:rhs_v) rhs
+      try for_all (fun k rhs_v -> ValueDomain.( <= ) ~lhs:(find k lhs) ~rhs:rhs_v) rhs
       with Caml.Not_found -> false
 
 
   let join astate1 astate2 =
     if phys_equal astate1 astate2 then astate1
     else
-      M.merge
+      merge
         (fun _ v1_opt v2_opt ->
           match (v1_opt, v2_opt) with
           | Some v1, Some v2 ->
@@ -330,7 +347,7 @@ module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S
   let widen ~prev ~next ~num_iters =
     if phys_equal prev next then prev
     else
-      M.merge
+      merge
         (fun _ v1_opt v2_opt ->
           match (v1_opt, v2_opt) with
           | Some v1, Some v2 ->
@@ -338,13 +355,10 @@ module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S
           | _ ->
               None )
         prev next
-
-
-  let pp fmt astate = M.pp ~pp_value:ValueDomain.pp fmt astate
 end
 
 module BooleanAnd = struct
-  type astate = bool
+  type t = bool
 
   let ( <= ) ~lhs ~rhs = lhs || not rhs
 
@@ -356,7 +370,7 @@ module BooleanAnd = struct
 end
 
 module BooleanOr = struct
-  type astate = bool
+  type t = bool
 
   let empty = false
 
@@ -376,7 +390,7 @@ module type MaxCount = sig
 end
 
 module CountDomain (MaxCount : MaxCount) = struct
-  type astate = int
+  type t = int
 
   let top =
     assert (MaxCount.max > 0) ;
@@ -405,7 +419,7 @@ module CountDomain (MaxCount : MaxCount) = struct
 end
 
 module StackDomain (Element : PrettyPrintable.PrintableOrderedType) = struct
-  type astate = Element.t list
+  type t = Element.t list
 
   let push = List.cons
 

infer/src/absint/AbstractDomain.mli

@@ -6,7 +6,6 @@
  *)
 
 open! IStd
-module F = Format
 
 module Types : sig
   type 'astate bottom_lifted = Bottom | NonBottom of 'astate
@@ -23,16 +22,14 @@ exception Stop_analysis
 (** Abstract domains and domain combinators *)
 
 module type S = sig
-  type astate
+  include PrettyPrintable.PrintableType
 
-  val ( <= ) : lhs:astate -> rhs:astate -> bool
+  val ( <= ) : lhs:t -> rhs:t -> bool
   (** the partial order induced by join *)
 
-  val join : astate -> astate -> astate
+  val join : t -> t -> t
 
-  val widen : prev:astate -> next:astate -> num_iters:int -> astate
+  val widen : prev:t -> next:t -> num_iters:int -> t
-
-  val pp : F.formatter -> astate -> unit
 end
 
 include
@@ -41,19 +38,19 @@ include
     [@@@warning "-60"]
 
     (** a trivial domain *)
-    module Empty : S with type astate = unit
+    module Empty : S with type t = unit
 end
 
 (** A domain with an explicit bottom value *)
 module type WithBottom = sig
   include S
 
-  val empty : astate
+  val empty : t
   (** The bottom value of the domain.
       Naming it empty instead of bottom helps to bind the empty
       value for sets and maps to the natural definition for bottom *)
 
-  val is_empty : astate -> bool
+  val is_empty : t -> bool
   (** Return true if this is the bottom value *)
 end
 
@@ -61,106 +58,103 @@ end
 module type WithTop = sig
   include S
 
-  val top : astate
+  val top : t
 end
 
 (** Lift a pre-domain to a domain *)
-module BottomLifted (Domain : S) : sig
+module BottomLifted (Domain : S) : WithBottom with type t = Domain.t bottom_lifted
-  type astate = Domain.astate bottom_lifted
 
-  include WithBottom with type astate := astate
+(* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
-end
 
-(** Create a domain with Top element from a pre-domain *)
 include
   sig
-    (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
-
     [@@@warning "-60"]
 
-    module TopLifted (Domain : S) : sig
+    (** Create a domain with Top element from a pre-domain *)
-      type astate = Domain.astate top_lifted
+    module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted
-
-      include WithTop with type astate := astate
-    end
 end
 
 (** Cartesian product of two domains. *)
-module Pair (Domain1 : S) (Domain2 : S) : S with type astate = Domain1.astate * Domain2.astate
+module Pair (Domain1 : S) (Domain2 : S) : S with type t = Domain1.t * Domain2.t
 
 (** Flat abstract domain: Bottom, Top, and non-comparable elements in between *)
 module Flat (V : PrettyPrintable.PrintableEquatableType) : sig
   include WithBottom
 
-  include WithTop with type astate := astate
+  include WithTop with type t := t
 
-  val v : V.t -> astate
+  val v : V.t -> t
 
-  val get : astate -> V.t option
+  val get : t -> V.t option
 end
 
-(** Lift a PPSet to a powerset domain ordered by subset. The elements of the set should be drawn from
+module type FiniteSetS = sig
-    a *finite* collection of possible values, since the widening operator here is just union. *)
+  include PrettyPrintable.PPSet
-module FiniteSetOfPPSet (PPSet : PrettyPrintable.PPSet) : sig
-  include module type of PPSet with type elt = PPSet.elt
 
-  include WithBottom with type astate = t
+  include WithBottom with type t := t
 end
 
+(** Lift a PPSet to a powerset domain ordered by subset. The elements of the set should be drawn from
+    a *finite* collection of possible values, since the widening operator here is just union. *)
+module FiniteSetOfPPSet (PPSet : PrettyPrintable.PPSet) : FiniteSetS with type elt = PPSet.elt
+
 (** Lift a set to a powerset domain ordered by subset. The elements of the set should be drawn from
     a *finite* collection of possible values, since the widening operator here is just union. *)
-module FiniteSet (Element : PrettyPrintable.PrintableOrderedType) : sig
+module FiniteSet (Element : PrettyPrintable.PrintableOrderedType) :
-  include module type of PrettyPrintable.MakePPSet (Element)
+  FiniteSetS with type elt = Element.t
 
-  include WithBottom with type astate = t
+module type InvertedSetS = sig
+  include PrettyPrintable.PPSet
+
+  include S with type t := t
 end
 
 (** Lift a set to a powerset domain ordered by superset, so the join operator is intersection *)
-module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) : sig
+module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) :
-  include module type of PrettyPrintable.MakePPSet (Element)
+  InvertedSetS with type elt = Element.t
+
+module type MapS = sig
+  include PrettyPrintable.PPMonoMap
 
-  include S with type astate = t
+  include WithBottom with type t := t
 end
 
 (** Map domain ordered by union over the set of bindings, so the bottom element is the empty map.
     Every element implicitly maps to bottom unless it is explicitly bound to something else.
     Uses PPMap as the underlying map *)
-module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) : sig
+module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) :
-  include module type of PPMap with type key = PPMap.key
+  MapS with type key = PPMap.key and type value = ValueDomain.t
-
-  include WithBottom with type astate = ValueDomain.astate t
-end
 
 (** Map domain ordered by union over the set of bindings, so the bottom element is the empty map.
     Every element implicitly maps to bottom unless it is explicitly bound to something else *)
-module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) : sig
+module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) :
-  include module type of PrettyPrintable.MakePPMap (Key)
+  MapS with type key = Key.t and type value = ValueDomain.t
 
-  include WithBottom with type astate = ValueDomain.astate t
+module type InvertedMapS = sig
+  include PrettyPrintable.PPMonoMap
+
+  include S with type t := t
 end
 
 (** Map domain ordered by intersection over the set of bindings, so the top element is the empty
     map. Every element implictly maps to top unless it is explicitly bound to something else *)
-module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) : sig
+module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) :
-  include module type of PrettyPrintable.MakePPMap (Key)
+  InvertedMapS with type key = Key.t and type value = ValueDomain.t
 
-  include S with type astate = ValueDomain.astate t
+(* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
-end
 
-(** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's
-    true in both conditional branches. *)
 include
   sig
-    (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
-
     [@@@warning "-60"]
 
-    module BooleanAnd : S with type astate = bool
+    (** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's
+    true in both conditional branches. *)
+    module BooleanAnd : S with type t = bool
 end
 
 (** Boolean domain ordered by ~p || q. Useful when you want a boolean that's true only when it's
     true in one conditional branch. *)
-module BooleanOr : WithBottom with type astate = bool
+module BooleanOr : WithBottom with type t = bool
 
 module type MaxCount = sig
   val max : int
@@ -170,21 +164,21 @@ end
 (** Domain keeping a non-negative count with a bounded maximum value. The count can be only
     incremented and decremented *)
 module CountDomain (MaxCount : MaxCount) : sig
-  include WithBottom with type astate = private int
+  include WithBottom with type t = private int
 
-  val top : astate [@@warning "-32"]
+  val top : t [@@warning "-32"]
   (** maximum value *)
 
-  val is_top : astate -> bool [@@warning "-32"]
+  val is_top : t -> bool [@@warning "-32"]
   (** return true if this is the maximum value *)
 
-  val increment : astate -> astate
+  val increment : t -> t
   (** bump the count by one if it is less than the max *)
 
-  val decrement : astate -> astate
+  val decrement : t -> t
   (** descrease the count by one if it is greater than 0 *)
 
-  val add : astate -> astate -> astate
+  val add : t -> t -> t
   (** capped sum of two states *)
 end
 
@@ -193,14 +187,14 @@ end
     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 S with type astate = Element.t list
+  include S with type t = Element.t list
 
-  val push : Element.t -> astate -> astate
+  val push : Element.t -> t -> t
 
-  val pop : astate -> astate
+  val pop : t -> t
   (** throws exception on empty *)
 
-  val empty : astate
+  val empty : t
 
-  val is_empty : astate -> bool
+  val is_empty : t -> bool
 end

infer/src/absint/AbstractInterpreter.ml

@@ -51,26 +51,26 @@ module type S = sig
 
   module InvariantMap = TransferFunctions.CFG.Node.IdMap
 
-  type invariant_map = TransferFunctions.Domain.astate State.t InvariantMap.t
+  type invariant_map = TransferFunctions.Domain.t State.t InvariantMap.t
 
   val compute_post :
        ?do_narrowing:bool
-    -> ?pp_instr:(TransferFunctions.Domain.astate -> Sil.instr -> (Format.formatter -> unit) option)
+    -> ?pp_instr:(TransferFunctions.Domain.t -> Sil.instr -> (Format.formatter -> unit) option)
     -> TransferFunctions.extras ProcData.t
-    -> initial:TransferFunctions.Domain.astate
+    -> initial:TransferFunctions.Domain.t
-    -> TransferFunctions.Domain.astate option
+    -> TransferFunctions.Domain.t option
 
   val exec_cfg :
        ?do_narrowing:bool
     -> TransferFunctions.CFG.t
     -> TransferFunctions.extras ProcData.t
-    -> initial:TransferFunctions.Domain.astate
+    -> initial:TransferFunctions.Domain.t
     -> invariant_map
 
   val exec_pdesc :
        ?do_narrowing:bool
     -> TransferFunctions.extras ProcData.t
-    -> initial:TransferFunctions.Domain.astate
+    -> initial:TransferFunctions.Domain.t
     -> invariant_map
 
   val extract_post : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option
@@ -87,7 +87,7 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
   module InvariantMap = TransferFunctions.CFG.Node.IdMap
   module Domain = TransferFunctions.Domain
 
-  type invariant_map = Domain.astate State.t InvariantMap.t
+  type invariant_map = Domain.t State.t InvariantMap.t
 
   (** extract the state of node [n] from [inv_map] *)
   let extract_state node_id inv_map = InvariantMap.find_opt node_id inv_map

infer/src/absint/AbstractInterpreter.mli

@@ -22,14 +22,14 @@ module type S = sig
   module InvariantMap = TransferFunctions.CFG.Node.IdMap
 
   (** invariant map from node id -> state representing postcondition for node id *)
-  type invariant_map = TransferFunctions.Domain.astate State.t InvariantMap.t
+  type invariant_map = TransferFunctions.Domain.t State.t InvariantMap.t
 
   val compute_post :
        ?do_narrowing:bool
-    -> ?pp_instr:(TransferFunctions.Domain.astate -> Sil.instr -> (Format.formatter -> unit) option)
+    -> ?pp_instr:(TransferFunctions.Domain.t -> Sil.instr -> (Format.formatter -> unit) option)
     -> TransferFunctions.extras ProcData.t
-    -> initial:TransferFunctions.Domain.astate
+    -> initial:TransferFunctions.Domain.t
-    -> TransferFunctions.Domain.astate option
+    -> TransferFunctions.Domain.t option
   (** compute and return the postcondition for the given procedure starting from [initial].
       [pp_instr] is used for the debug HTML and passed as a hook to handle both SIL and HIL CFGs. *)
 
@@ -37,14 +37,14 @@ module type S = sig
        ?do_narrowing:bool
     -> TransferFunctions.CFG.t
     -> TransferFunctions.extras ProcData.t
-    -> initial:TransferFunctions.Domain.astate
+    -> initial:TransferFunctions.Domain.t
     -> invariant_map
   (** compute and return invariant map for the given CFG/procedure starting from [initial]. *)
 
   val exec_pdesc :
        ?do_narrowing:bool
     -> TransferFunctions.extras ProcData.t
-    -> initial:TransferFunctions.Domain.astate
+    -> initial:TransferFunctions.Domain.t
     -> invariant_map
   (** compute and return invariant map for the given procedure starting from [initial] *)
 

infer/src/absint/LowerHil.mli

@@ -28,7 +28,7 @@ module Make
 
   type extras = TransferFunctions.extras
 
-  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.astate
+  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.t
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
@@ -44,8 +44,8 @@ module MakeAbstractInterpreterWithConfig
 
   val compute_post :
        Interpreter.TransferFunctions.extras ProcData.t
-    -> initial:MakeTransferFunctions(CFG).Domain.astate
+    -> initial:MakeTransferFunctions(CFG).Domain.t
-    -> MakeTransferFunctions(CFG).Domain.astate option
+    -> MakeTransferFunctions(CFG).Domain.t option
   (** compute and return the postcondition for the given procedure starting from [initial]. If
       [debug] is true, print html debugging output. *)
 end

infer/src/absint/TransferFunctions.ml

@@ -16,7 +16,7 @@ module type S = sig
 
   type instr
 
-  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.astate
+  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end

infer/src/absint/TransferFunctions.mli

@@ -22,7 +22,7 @@ module type S = sig
   (** type of the instructions the transfer functions operate on *)
   type instr
 
-  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.astate
+  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t
   (** {A} instr {A'}. [node] is the node of the current instruction *)
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit

infer/src/backend/Differential.ml

@@ -63,7 +63,7 @@ module CostsSummary = struct
   type previous_current = {previous: int; current: int}
 
   let count costs =
-    let count_aux t (e : CostDomain.BasicCost.astate) =
+    let count_aux t (e : CostDomain.BasicCost.t) =
       match CostDomain.BasicCost.degree e with
       | None ->
           assert (CostDomain.BasicCost.is_top e) ;

infer/src/backend/Payloads.ml

@@ -9,18 +9,18 @@ open! IStd
 module F = Format
 
 type t =
-  { annot_map: AnnotReachabilityDomain.astate option
+  { annot_map: AnnotReachabilityDomain.t option
   ; biabduction: BiabductionSummary.t option
   ; buffer_overrun: BufferOverrunSummary.t option
   ; class_loads: ClassLoadsDomain.summary option
   ; cost: CostDomain.summary option
   ; crashcontext_frame: Stacktree_t.stacktree option
-  ; litho: LithoDomain.astate option
+  ; litho: LithoDomain.t option
   ; purity: PurityDomain.summary option
   ; quandary: QuandarySummary.t option
   ; racerd: RacerDDomain.summary option
   ; resources: ResourceLeakDomain.summary option
-  ; siof: SiofDomain.Summary.astate option
+  ; siof: SiofDomain.Summary.t option
   ; starvation: StarvationDomain.summary option
   ; typestate: TypeState.t option
   ; uninit: UninitDomain.Summary.t option }

infer/src/backend/Payloads.mli

@@ -9,18 +9,18 @@ open! IStd
 
 (** analysis results *)
 type t =
-  { annot_map: AnnotReachabilityDomain.astate option
+  { annot_map: AnnotReachabilityDomain.t option
   ; biabduction: BiabductionSummary.t option
   ; buffer_overrun: BufferOverrunSummary.t option
   ; class_loads: ClassLoadsDomain.summary option
   ; cost: CostDomain.summary option
   ; crashcontext_frame: Stacktree_t.stacktree option
-  ; litho: LithoDomain.astate option
+  ; litho: LithoDomain.t option
   ; purity: PurityDomain.summary option
   ; quandary: QuandarySummary.t option
   ; racerd: RacerDDomain.summary option
   ; resources: ResourceLeakDomain.summary option
-  ; siof: SiofDomain.Summary.astate option
+  ; siof: SiofDomain.Summary.t option
   ; starvation: StarvationDomain.summary option
   ; typestate: TypeState.t option
   ; uninit: UninitDomain.Summary.t option }

infer/src/bufferoverrun/arrayBlk.ml

@@ -15,8 +15,6 @@ module Bound = Bounds.Bound
 module ArrInfo = struct
   type t = {offset: Itv.t; size: Itv.t; stride: Itv.t} [@@deriving compare]
 
-  type astate = t
-
   let top : t = {offset= Itv.top; size= Itv.top; stride= Itv.top}
 
   let make : offset:Itv.t -> size:Itv.t -> stride:Itv.t -> t =
@@ -52,9 +50,9 @@ module ArrInfo = struct
 
   let plus_offset : t -> Itv.t -> t = fun arr i -> {arr with offset= Itv.plus arr.offset i}
 
-  let minus_offset : t -> Itv.astate -> t = fun arr i -> {arr with offset= Itv.minus arr.offset i}
+  let minus_offset : t -> Itv.t -> t = fun arr i -> {arr with offset= Itv.minus arr.offset i}
 
-  let diff : t -> t -> Itv.astate = fun arr1 arr2 -> Itv.minus arr1.offset arr2.offset
+  let diff : t -> t -> Itv.t = fun arr1 arr2 -> Itv.minus arr1.offset arr2.offset
 
   let subst : t -> Bound.eval_sym -> t =
    fun arr eval_sym ->
@@ -113,35 +111,31 @@ end
 
 include AbstractDomain.Map (Allocsite) (ArrInfo)
 
-let bot : astate = empty
+let bot : t = empty
 
-let unknown : astate = add Allocsite.unknown ArrInfo.top bot
+let unknown : t = add Allocsite.unknown ArrInfo.top bot
 
-let is_bot : astate -> bool = is_empty
+let is_bot : t -> bool = is_empty
 
-let make : Allocsite.t -> offset:Itv.t -> size:Itv.t -> stride:Itv.t -> astate =
+let make : Allocsite.t -> offset:Itv.t -> size:Itv.t -> stride:Itv.t -> t =
  fun a ~offset ~size ~stride -> singleton a (ArrInfo.make ~offset ~size ~stride)
 
 
-let offsetof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.offset) a Itv.bot
+let offsetof : t -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.offset) a Itv.bot
 
-let sizeof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.size) a Itv.bot
+let sizeof : t -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.size) a Itv.bot
 
-let strideof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.stride) a Itv.bot
+let strideof : t -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.stride) a Itv.bot
 
-let sizeof_byte : astate -> Itv.t =
+let sizeof_byte : t -> Itv.t =
  fun a -> fold (fun _ arr -> Itv.join (Itv.mult arr.ArrInfo.size arr.ArrInfo.stride)) a Itv.bot
 
 
-let plus_offset : astate -> Itv.t -> astate =
+let plus_offset : t -> Itv.t -> t = fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr
- fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr
-
-
-let minus_offset : astate -> Itv.t -> astate =
- fun arr i -> map (fun a -> ArrInfo.minus_offset a i) arr
 
+let minus_offset : t -> Itv.t -> t = fun arr i -> map (fun a -> ArrInfo.minus_offset a i) arr
 
-let diff : astate -> astate -> Itv.t =
+let diff : t -> t -> Itv.t =
  fun arr1 arr2 ->
   let diff_join k a2 acc =
     match find k arr1 with
@@ -153,24 +147,24 @@ let diff : astate -> astate -> Itv.t =
   fold diff_join arr2 Itv.bot
 
 
-let get_pow_loc : astate -> PowLoc.t =
+let get_pow_loc : t -> PowLoc.t =
  fun array ->
   let pow_loc_of_allocsite k _ acc = PowLoc.add (Loc.of_allocsite k) acc in
   fold pow_loc_of_allocsite array PowLoc.bot
 
 
-let subst : astate -> Bound.eval_sym -> astate =
+let subst : t -> Bound.eval_sym -> t =
  fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a
 
 
-let get_symbols : astate -> Itv.SymbolSet.t =
+let get_symbols : t -> Itv.SymbolSet.t =
  fun a ->
   fold (fun _ ai acc -> Itv.SymbolSet.union acc (ArrInfo.get_symbols ai)) a Itv.SymbolSet.empty
 
 
-let normalize : astate -> astate = fun a -> map ArrInfo.normalize a
+let normalize : t -> t = fun a -> map ArrInfo.normalize a
 
-let do_prune : (ArrInfo.t -> ArrInfo.t -> ArrInfo.t) -> astate -> astate -> astate =
+let do_prune : (ArrInfo.t -> ArrInfo.t -> ArrInfo.t) -> t -> t -> t =
  fun arr_info_prune a1 a2 ->
   match is_singleton_or_more a2 with
   | IContainer.Singleton (k, v2) ->
@@ -179,17 +173,15 @@ let do_prune : (ArrInfo.t -> ArrInfo.t -> ArrInfo.t) -> astate -> astate -> asta
       a1
 
 
-let prune_comp : Binop.t -> astate -> astate -> astate =
+let prune_comp : Binop.t -> t -> t -> t = fun c a1 a2 -> do_prune (ArrInfo.prune_comp c) a1 a2
- fun c a1 a2 -> do_prune (ArrInfo.prune_comp c) a1 a2
-
 
-let prune_eq : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_eq a1 a2
+let prune_eq : t -> t -> t = fun a1 a2 -> do_prune ArrInfo.prune_eq a1 a2
 
-let prune_ne : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2
+let prune_ne : t -> t -> t = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2
 
-let set_length : Itv.t -> astate -> astate = fun length a -> map (ArrInfo.set_length length) a
+let set_length : Itv.t -> t -> t = fun length a -> map (ArrInfo.set_length length) a
 
-let set_stride : Z.t -> astate -> astate = fun stride a -> map (ArrInfo.set_stride stride) a
+let set_stride : Z.t -> t -> t = fun stride a -> map (ArrInfo.set_stride stride) a
 
 let lift_cmp_itv cmp_itv cmp_loc arr1 arr2 =
   match (is_singleton_or_more arr1, is_singleton_or_more arr2) with

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -125,10 +125,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       -> Procdesc.t
       -> Typ.Procname.t
       -> (Exp.t * Typ.t) list
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
       -> BufferOverrunSummary.t
       -> Location.t
-      -> Dom.Mem.astate =
+      -> Dom.Mem.t =
    fun tenv integer_type_widths ret callee_pdesc callee_pname params caller_mem summary location ->
     let callee_exit_mem = BufferOverrunSummary.get_output summary in
     let rel_subst_map =
@@ -147,8 +147,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem
 
 
-  let exec_instr : Dom.Mem.astate -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate
+  let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t =
-      =
    fun mem {pdesc; tenv; extras= {symbol_table; integer_type_widths}} node instr ->
     match instr with
     | Load (id, _, _, _) when Ident.is_none id ->
@@ -369,8 +368,8 @@ module Init = struct
       -> Itv.SymbolTable.t
       -> inst_num:int
       -> (Pvar.t * Typ.t) list
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
-      -> Dom.Mem.astate =
+      -> Dom.Mem.t =
    fun pname tenv integer_type_widths ~node_hash location symbol_table ~inst_num formals mem ->
     let new_sym_num = Counter.make 0 in
     let add_formal (mem, inst_num) (pvar, typ) =
@@ -481,7 +480,7 @@ module Report = struct
       -> e1:Exp.t
       -> e2:Exp.t
       -> Location.t
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
       -> PO.ConditionSet.t
       -> PO.ConditionSet.t =
    fun integer_type_widths ~is_plus ~e1 ~e2 location mem cond_set ->
@@ -500,7 +499,7 @@ module Report = struct
       -> e1:Exp.t
       -> e2:Exp.t
       -> Location.t
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
       -> PO.ConditionSet.t
       -> PO.ConditionSet.t =
    fun integer_type_widths ~bop ~e1 ~e2 location mem cond_set ->
@@ -517,7 +516,7 @@ module Report = struct
          Typ.IntegerWidths.t
       -> Exp.t
       -> Location.t
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
       -> PO.ConditionSet.t
       -> PO.ConditionSet.t =
    fun integer_type_widths exp location mem cond_set ->
@@ -591,7 +590,7 @@ module Report = struct
       -> Typ.IntegerWidths.t
       -> Procdesc.t
       -> (Exp.t * Typ.t) list
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
       -> Payload.t
       -> Location.t
       -> PO.ConditionSet.t =
@@ -616,7 +615,7 @@ module Report = struct
       -> Itv.SymbolTable.t
       -> CFG.Node.t
       -> Sil.instr
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
       -> PO.ConditionSet.t
       -> PO.ConditionSet.t =
    fun pdesc tenv integer_type_widths symbol_table node instr mem cond_set ->
@@ -661,7 +660,7 @@ module Report = struct
         cond_set
 
 
-  let print_debug_info : Sil.instr -> Dom.Mem.astate -> PO.ConditionSet.t -> unit =
+  let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.t -> unit =
    fun instr pre cond_set ->
     L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ;
     L.(debug BufferOverrun Verbose) "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre ;
@@ -680,7 +679,7 @@ module Report = struct
       -> CFG.t
       -> CFG.Node.t
       -> Instrs.not_reversed_t
-      -> Dom.Mem.astate AbstractInterpreter.State.t
+      -> Dom.Mem.t AbstractInterpreter.State.t
       -> PO.ConditionSet.t
       -> PO.ConditionSet.t =
    fun summary pdesc tenv integer_type_widths symbol_table cfg node instrs state cond_set ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -17,18 +17,16 @@ module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
 module Val = struct
-  type astate =
+  type t =
-    { itv: Itv.astate
+    { itv: Itv.t
-    ; sym: Relation.Sym.astate
+    ; sym: Relation.Sym.t
-    ; powloc: PowLoc.astate
+    ; powloc: PowLoc.t
-    ; arrayblk: ArrayBlk.astate
+    ; arrayblk: ArrayBlk.t
-    ; offset_sym: Relation.Sym.astate
+    ; offset_sym: Relation.Sym.t
-    ; size_sym: Relation.Sym.astate
+    ; size_sym: Relation.Sym.t
     ; traces: TraceSet.t
     ; represents_multiple_values: bool }
 
-  type t = astate
-
   let bot : t =
     { itv= Itv.bot
     ; sym= Relation.Sym.bot
@@ -112,21 +110,21 @@ module Val = struct
 
   let get_itv : t -> Itv.t = fun x -> x.itv
 
-  let get_sym : t -> Relation.Sym.astate = fun x -> x.sym
+  let get_sym : t -> Relation.Sym.t = fun x -> x.sym
 
   let get_sym_var : t -> Relation.Var.t option = fun x -> Relation.Sym.get_var x.sym
 
   let get_pow_loc : t -> PowLoc.t = fun x -> x.powloc
 
-  let get_array_blk : t -> ArrayBlk.astate = fun x -> x.arrayblk
+  let get_array_blk : t -> ArrayBlk.t = fun x -> x.arrayblk
 
   let get_array_locs : t -> PowLoc.t = fun x -> ArrayBlk.get_pow_loc x.arrayblk
 
   let get_all_locs : t -> PowLoc.t = fun x -> PowLoc.join x.powloc (get_array_locs x)
 
-  let get_offset_sym : t -> Relation.Sym.astate = fun x -> x.offset_sym
+  let get_offset_sym : t -> Relation.Sym.t = fun x -> x.offset_sym
 
-  let get_size_sym : t -> Relation.Sym.astate = fun x -> x.size_sym
+  let get_size_sym : t -> Relation.Sym.t = fun x -> x.size_sym
 
   let get_traces : t -> TraceSet.t = fun x -> x.traces
 
@@ -253,11 +251,7 @@ module Val = struct
 
 
   let lift_prune2 :
-         (Itv.t -> Itv.t -> Itv.t)
+      (Itv.t -> Itv.t -> Itv.t) -> (ArrayBlk.t -> ArrayBlk.t -> ArrayBlk.t) -> t -> t -> t =
-      -> (ArrayBlk.astate -> ArrayBlk.astate -> ArrayBlk.astate)
-      -> t
-      -> t
-      -> t =
    fun f g x y ->
     warn_against_pruning_multiple_values
       { x with
@@ -282,7 +276,7 @@ module Val = struct
 
   (* In the pointer arithmetics, it returns top, if we cannot
      precisely follow the physical memory model, e.g., (&x + 1). *)
-  let lift_pi : (ArrayBlk.astate -> Itv.t -> ArrayBlk.astate) -> t -> t -> t =
+  let lift_pi : (ArrayBlk.t -> Itv.t -> ArrayBlk.t) -> t -> t -> t =
    fun f x y ->
     let traces = TraceSet.join x.traces y.traces in
     if is_pointer_to_non_array x then {bot with itv= Itv.top; traces}
@@ -371,7 +365,7 @@ module MemPure = struct
 
   let bot = empty
 
-  let range : filter_loc:(Loc.t -> bool) -> astate -> Polynomials.NonNegativePolynomial.astate =
+  let range : filter_loc:(Loc.t -> bool) -> t -> Polynomials.NonNegativePolynomial.t =
    fun ~filter_loc mem ->
     fold
       (fun loc v acc ->
@@ -401,8 +395,6 @@ module AliasTarget = struct
         Option.map (f l) ~f:(fun l -> Empty l)
 
 
-  type astate = t
-
   let ( <= ) ~lhs ~rhs = equal lhs rhs
 
   let join x y =
@@ -430,7 +422,7 @@ end
 module AliasMap = struct
   include AbstractDomain.Map (Ident) (AliasTarget)
 
-  let pp : F.formatter -> astate -> unit =
+  let pp : F.formatter -> t -> unit =
    fun fmt x ->
     if not (is_empty x) then
       let pp_sep fmt () = F.fprintf fmt ", @," in
@@ -438,23 +430,21 @@ module AliasMap = struct
       F.pp_print_list ~pp_sep pp1 fmt (bindings x)
 
 
-  let load : Ident.t -> AliasTarget.astate -> astate -> astate = add
+  let load : Ident.t -> AliasTarget.t -> t -> t = add
 
-  let store : Loc.t -> astate -> astate =
+  let store : Loc.t -> t -> t = fun l m -> filter (fun _ y -> not (AliasTarget.use l y)) m
-   fun l m -> filter (fun _ y -> not (AliasTarget.use l y)) m
 
-
+  let find : Ident.t -> t -> AliasTarget.t option = find_opt
-  let find : Ident.t -> astate -> AliasTarget.astate option = find_opt
 end
 
 module AliasRet = struct
   include AbstractDomain.Flat (AliasTarget)
 
-  let pp : F.formatter -> astate -> unit = fun fmt x -> F.pp_print_string fmt "ret=" ; pp fmt x
+  let pp : F.formatter -> t -> unit = fun fmt x -> F.pp_print_string fmt "ret=" ; pp fmt x
 end
 
 module Alias = struct
-  type astate = {map: AliasMap.astate; ret: AliasRet.astate}
+  type t = {map: AliasMap.t; ret: AliasRet.t}
 
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true
@@ -478,23 +468,19 @@ module Alias = struct
       AliasRet.pp x.ret
 
 
-  let bot : astate = {map= AliasMap.empty; ret= AliasRet.empty}
+  let bot : t = {map= AliasMap.empty; ret= AliasRet.empty}
-
-  let lift_map : (AliasMap.astate -> AliasMap.astate) -> astate -> astate =
-   fun f a -> {a with map= f a.map}
-
 
-  let bind_map : (AliasMap.astate -> 'a) -> astate -> 'a = fun f a -> f a.map
+  let lift_map : (AliasMap.t -> AliasMap.t) -> t -> t = fun f a -> {a with map= f a.map}
 
-  let find : Ident.t -> astate -> AliasTarget.astate option = fun x -> bind_map (AliasMap.find x)
+  let bind_map : (AliasMap.t -> 'a) -> t -> 'a = fun f a -> f a.map
 
-  let find_ret : astate -> AliasTarget.astate option = fun x -> AliasRet.get x.ret
+  let find : Ident.t -> t -> AliasTarget.t option = fun x -> bind_map (AliasMap.find x)
 
-  let load : Ident.t -> AliasTarget.astate -> astate -> astate =
+  let find_ret : t -> AliasTarget.t option = fun x -> AliasRet.get x.ret
-   fun id loc -> lift_map (AliasMap.load id loc)
 
+  let load : Ident.t -> AliasTarget.t -> t -> t = fun id loc -> lift_map (AliasMap.load id loc)
 
-  let store_simple : Loc.t -> Exp.t -> astate -> astate =
+  let store_simple : Loc.t -> Exp.t -> t -> t =
    fun loc e a ->
     let a = lift_map (AliasMap.store loc) a in
     match e with
@@ -505,7 +491,7 @@ module Alias = struct
         a
 
 
-  let store_empty : Val.t -> Loc.t -> astate -> astate =
+  let store_empty : Val.t -> Loc.t -> t -> t =
    fun formal loc a ->
     let a = lift_map (AliasMap.store loc) a in
     let locs = Val.get_all_locs formal in
@@ -516,7 +502,7 @@ module Alias = struct
         a
 
 
-  let remove_temp : Ident.t -> astate -> astate = fun temp -> lift_map (AliasMap.remove temp)
+  let remove_temp : Ident.t -> t -> t = fun temp -> lift_map (AliasMap.remove temp)
 end
 
 (* [PrunePairs] is a map from abstract locations to abstract values that represents pruned results
@@ -541,11 +527,11 @@ module LatestPrune = struct
      prunings.
 
      Top: No information about the latest pruning. *)
-  type astate =
+  type t =
-    | Latest of PrunePairs.astate
+    | Latest of PrunePairs.t
-    | TrueBranch of Pvar.t * PrunePairs.astate
+    | TrueBranch of Pvar.t * PrunePairs.t
-    | FalseBranch of Pvar.t * PrunePairs.astate
+    | FalseBranch of Pvar.t * PrunePairs.t
-    | V of Pvar.t * PrunePairs.astate * PrunePairs.astate
+    | V of Pvar.t * PrunePairs.t * PrunePairs.t
     | Top
 
   let pvar_pp = Pvar.pp Pp.text
@@ -614,14 +600,12 @@ module LatestPrune = struct
 end
 
 module MemReach = struct
-  type astate =
+  type t =
-    { stack_locs: StackLocs.astate
+    { stack_locs: StackLocs.t
-    ; mem_pure: MemPure.astate
+    ; mem_pure: MemPure.t
-    ; alias: Alias.astate
+    ; alias: Alias.t
-    ; latest_prune: LatestPrune.astate
+    ; latest_prune: LatestPrune.t
-    ; relation: Relation.astate }
+    ; relation: Relation.t }
-
-  type t = astate
 
   let init : t =
     { stack_locs= StackLocs.bot
@@ -686,7 +670,7 @@ module MemReach = struct
     PowLoc.fold find_join locs Val.bot
 
 
-  let find_alias : Ident.t -> t -> AliasTarget.astate option = fun k m -> Alias.find k m.alias
+  let find_alias : Ident.t -> t -> AliasTarget.t option = fun k m -> Alias.find k m.alias
 
   let find_simple_alias : Ident.t -> t -> Loc.t option =
    fun k m ->
@@ -697,9 +681,9 @@ module MemReach = struct
         None
 
 
-  let find_ret_alias : t -> AliasTarget.astate option = fun m -> Alias.find_ret m.alias
+  let find_ret_alias : t -> AliasTarget.t option = fun m -> Alias.find_ret m.alias
 
-  let load_alias : Ident.t -> AliasTarget.astate -> t -> t =
+  let load_alias : Ident.t -> AliasTarget.t -> t -> t =
    fun id loc m -> {m with alias= Alias.load id loc m.alias}
 
 
@@ -782,7 +766,7 @@ module MemReach = struct
    fun temps m -> List.fold temps ~init:m ~f:(fun acc temp -> remove_temp temp acc)
 
 
-  let set_prune_pairs : PrunePairs.astate -> t -> t =
+  let set_prune_pairs : PrunePairs.t -> t -> t =
    fun prune_pairs m -> {m with latest_prune= LatestPrune.Latest prune_pairs}
 
 
@@ -827,15 +811,15 @@ module MemReach = struct
     fun locs m -> add_from_locs m.mem_pure locs PowLoc.empty
 
 
-  let range : filter_loc:(Loc.t -> bool) -> t -> Polynomials.NonNegativePolynomial.astate =
+  let range : filter_loc:(Loc.t -> bool) -> t -> Polynomials.NonNegativePolynomial.t =
    fun ~filter_loc {mem_pure} -> MemPure.range ~filter_loc mem_pure
 
 
-  let get_relation : t -> Relation.astate = fun m -> m.relation
+  let get_relation : t -> Relation.t = fun m -> m.relation
 
   let is_relation_unsat : t -> bool = fun m -> Relation.is_unsat m.relation
 
-  let lift_relation : (Relation.astate -> Relation.astate) -> t -> t =
+  let lift_relation : (Relation.t -> Relation.t) -> t -> t =
    fun f m -> {m with relation= f m.relation}
 
 
@@ -871,8 +855,6 @@ end
 module Mem = struct
   include AbstractDomain.BottomLifted (MemReach)
 
-  type t = astate
-
   let bot : t = Bottom
 
   let init : t = NonBottom MemReach.init
@@ -903,7 +885,7 @@ module Mem = struct
    fun k -> f_lift_default ~default:None (MemReach.find_opt k)
 
 
-  let find_alias : Ident.t -> t -> AliasTarget.astate option =
+  let find_alias : Ident.t -> t -> AliasTarget.t option =
    fun k -> f_lift_default ~default:None (MemReach.find_alias k)
 
 
@@ -911,11 +893,11 @@ module Mem = struct
    fun k -> f_lift_default ~default:None (MemReach.find_simple_alias k)
 
 
-  let find_ret_alias : t -> AliasTarget.astate option =
+  let find_ret_alias : t -> AliasTarget.t option =
     f_lift_default ~default:None MemReach.find_ret_alias
 
 
-  let load_alias : Ident.t -> AliasTarget.astate -> t -> t =
+  let load_alias : Ident.t -> AliasTarget.t -> t -> t =
    fun id loc -> f_lift (MemReach.load_alias id loc)
 
 
@@ -962,7 +944,7 @@ module Mem = struct
 
   let remove_temps : Ident.t list -> t -> t = fun temps -> f_lift (MemReach.remove_temps temps)
 
-  let set_prune_pairs : PrunePairs.astate -> t -> t =
+  let set_prune_pairs : PrunePairs.t -> t -> t =
    fun prune_pairs -> f_lift (MemReach.set_prune_pairs prune_pairs)
 
 
@@ -972,7 +954,7 @@ module Mem = struct
    fun e1 e2 -> f_lift (MemReach.update_latest_prune e1 e2)
 
 
-  let get_relation : t -> Relation.astate =
+  let get_relation : t -> Relation.t =
    fun m -> f_lift_default ~default:Relation.bot MemReach.get_relation m
 
 

infer/src/bufferoverrun/bufferOverrunDomainRelation.ml

@@ -20,21 +20,21 @@ module type S = sig
   module Sym : sig
     include AbstractDomain.S
 
-    val bot : astate
+    val bot : t
 
-    val top : astate
+    val top : t
 
-    val of_loc : Loc.t -> astate
+    val of_loc : Loc.t -> t
 
-    val of_loc_offset : Loc.t -> astate
+    val of_loc_offset : Loc.t -> t
 
-    val of_loc_size : Loc.t -> astate
+    val of_loc_size : Loc.t -> t
 
-    val of_allocsite_offset : Allocsite.t -> astate
+    val of_allocsite_offset : Allocsite.t -> t
 
-    val of_allocsite_size : Allocsite.t -> astate
+    val of_allocsite_size : Allocsite.t -> t
 
-    val get_var : astate -> Var.t option
+    val get_var : t -> Var.t option
   end
 
   module SymExp : sig
@@ -44,18 +44,18 @@ module type S = sig
 
     val zero : t
 
-    val of_sym : Sym.astate -> t option
+    val of_sym : Sym.t -> t option
 
-    val of_exp : get_sym_f:(Exp.t -> Sym.astate) -> Exp.t -> t option
+    val of_exp : get_sym_f:(Exp.t -> Sym.t) -> Exp.t -> t option
 
     val of_exps :
-         get_int_sym_f:(Exp.t -> Sym.astate)
+         get_int_sym_f:(Exp.t -> Sym.t)
-      -> get_offset_sym_f:(Exp.t -> Sym.astate)
+      -> get_offset_sym_f:(Exp.t -> Sym.t)
-      -> get_size_sym_f:(Exp.t -> Sym.astate)
+      -> get_size_sym_f:(Exp.t -> Sym.t)
       -> Exp.t
       -> t option * t option * t option
 
-    val of_exp_opt : get_sym_f:(Exp.t -> Sym.astate) -> Exp.t option -> t option
+    val of_exp_opt : get_sym_f:(Exp.t -> Sym.t) -> Exp.t option -> t option
 
     val plus : t -> t -> t
 
@@ -65,7 +65,7 @@ module type S = sig
   module Constraints : sig
     type t
 
-    val of_exp : get_sym_f:(Exp.t -> Sym.astate) -> Exp.t -> t
+    val of_exp : get_sym_f:(Exp.t -> Sym.t) -> Exp.t -> t
   end
 
   module SubstMap : sig
@@ -82,40 +82,35 @@ module type S = sig
 
   val set_deserialize : unit -> unit
 
-  val compare_astate : astate -> astate -> int
+  val compare : t -> t -> int
 
-  val empty : astate
+  val empty : t
 
-  val bot : astate
+  val bot : t
 
-  val is_unsat : astate -> bool
+  val is_unsat : t -> bool
 
-  val lt_sat_opt : SymExp.t option -> SymExp.t option -> astate -> bool
+  val lt_sat_opt : SymExp.t option -> SymExp.t option -> t -> bool
 
-  val le_sat_opt : SymExp.t option -> SymExp.t option -> astate -> bool
+  val le_sat_opt : SymExp.t option -> SymExp.t option -> t -> bool
 
-  val meet_constraints : Constraints.t -> astate -> astate
+  val meet_constraints : Constraints.t -> t -> t
 
-  val store_relation :
+  val store_relation : PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> t -> t
-    PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> astate -> astate
 
-  val init_param : Loc.t -> astate -> astate
+  val init_param : Loc.t -> t -> t
 
   val init_array :
-    Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:SymExp.t option -> astate -> astate
+    Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:SymExp.t option -> t -> t
 
-  val forget_locs : PowLoc.t -> astate -> astate
+  val forget_locs : PowLoc.t -> t -> t
 
-  val instantiate : caller:astate -> callee:astate -> SubstMap.t -> astate
+  val instantiate : caller:t -> callee:t -> SubstMap.t -> t
 end
 
 module NoRelation = struct
   module UnitDom = struct
-    type astate = unit [@@deriving compare]
+    type t = unit [@@deriving compare]
-
-    type t = astate [@@deriving compare]
-
-    let compare_astate _ _ = 0
 
     let f1 _ = ()
 
@@ -944,9 +939,9 @@ module Make (Manager : Manager_S) = struct
   end
 
   module Val = struct
-    type astate = Manager.domain_t Abstract1.t
+    type t = Manager.domain_t Abstract1.t
 
-    let compare_astate = Compares.compare_abstract1
+    let compare = Compares.compare_abstract1
 
     let bot = Abstract1.bottom man Env.empty
 
@@ -1075,7 +1070,7 @@ module Make (Manager : Manager_S) = struct
 
     let le_sat e1 e2 x = sat_tcons (Tcons1.make (SymExp.minus e2 e1) Tcons1.SUPEQ) x
 
-    let subst : forget_free:bool -> SubstMap.t -> astate -> astate =
+    let subst : forget_free:bool -> SubstMap.t -> t -> t =
       let forget_free_vars vars_in_subst_map x =
         let free_vars = VarSet.diff (Env.to_vars_set (Abstract1.env x)) vars_in_subst_map in
         let free_vars = VarSet.remove Var.return free_vars in
@@ -1138,7 +1133,7 @@ module Make (Manager : Manager_S) = struct
   end
 
   module PackedVal = struct
-    type astate = {pack_ids: Pack.t VarMap.t; packs: Val.astate PackMap.t} [@@deriving compare]
+    type t = {pack_ids: Pack.t VarMap.t; packs: Val.t PackMap.t} [@@deriving compare]
 
     let empty = {pack_ids= VarMap.empty; packs= PackMap.empty}
 
@@ -1509,7 +1504,7 @@ module Make (Manager : Manager_S) = struct
 
   include AbstractDomain.BottomLifted (PackedVal)
 
-  let compare_astate x y =
+  let compare x y =
     match (x, y) with
     | Bottom, Bottom ->
         0
@@ -1518,59 +1513,57 @@ module Make (Manager : Manager_S) = struct
     | _, Bottom ->
         1
     | NonBottom x', NonBottom y' ->
-        PackedVal.compare_astate x' y'
+        PackedVal.compare x' y'
 
 
-  let empty : astate = NonBottom PackedVal.empty
+  let empty : t = NonBottom PackedVal.empty
 
-  let bot : astate = Bottom
+  let bot : t = Bottom
 
-  let is_unsat : astate -> bool = function Bottom -> true | NonBottom _ -> false
+  let is_unsat : t -> bool = function Bottom -> true | NonBottom _ -> false
 
-  let lift_default : default:'a -> (PackedVal.astate -> 'a) -> astate -> 'a =
+  let lift_default : default:'a -> (PackedVal.t -> 'a) -> t -> 'a =
    fun ~default f -> function Bottom -> default | NonBottom x -> f x
 
 
-  let lift : (PackedVal.astate -> PackedVal.astate) -> astate -> astate =
+  let lift : (PackedVal.t -> PackedVal.t) -> t -> t =
    fun f -> function Bottom -> Bottom | NonBottom x -> NonBottom (f x)
 
 
-  let lift2 : (PackedVal.astate -> PackedVal.astate -> astate) -> astate -> astate -> astate =
+  let lift2 : (PackedVal.t -> PackedVal.t -> t) -> t -> t -> t =
    fun f x y ->
     match (x, y) with Bottom, _ | _, Bottom -> Bottom | NonBottom x', NonBottom y' -> f x' y'
 
 
-  let lt_sat_opt : SymExp.t option -> SymExp.t option -> astate -> bool =
+  let lt_sat_opt : SymExp.t option -> SymExp.t option -> t -> bool =
    fun e1_opt e2_opt -> lift_default ~default:true (PackedVal.lt_sat_opt e1_opt e2_opt)
 
 
-  let le_sat_opt : SymExp.t option -> SymExp.t option -> astate -> bool =
+  let le_sat_opt : SymExp.t option -> SymExp.t option -> t -> bool =
    fun e1_opt e2_opt -> lift_default ~default:true (PackedVal.le_sat_opt e1_opt e2_opt)
 
 
-  let meet_constraints : Constraints.t -> astate -> astate =
+  let meet_constraints : Constraints.t -> t -> t =
    fun constrs -> lift_default ~default:Bottom (PackedVal.meet_constraints constrs)
 
 
-  let store_relation :
+  let store_relation : PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> t -> t =
-      PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> astate -> astate =
    fun locs texpr_opts -> lift_default ~default:Bottom (PackedVal.store_relation locs texpr_opts)
 
 
-  let init_param : Loc.t -> astate -> astate =
+  let init_param : Loc.t -> t -> t =
    fun loc -> lift_default ~default:Bottom (PackedVal.init_param loc)
 
 
   let init_array :
-      Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:SymExp.t option -> astate -> astate
+      Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:SymExp.t option -> t -> t =
-      =
    fun allocsite ~offset ~size ~size_exp_opt ->
     lift_default ~default:Bottom (PackedVal.init_array allocsite ~offset ~size ~size_exp_opt)
 
 
-  let forget_locs : PowLoc.t -> astate -> astate = fun locs -> lift (PackedVal.forget_locs locs)
+  let forget_locs : PowLoc.t -> t -> t = fun locs -> lift (PackedVal.forget_locs locs)
 
-  let instantiate : caller:astate -> callee:astate -> SubstMap.t -> astate =
+  let instantiate : caller:t -> callee:t -> SubstMap.t -> t =
    fun ~caller ~callee subst_map ->
     lift2 (fun caller callee -> PackedVal.instantiate ~caller ~callee subst_map) caller callee
 end

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -28,9 +28,9 @@ let mk_model_env pname node_hash location tenv integer_type_widths symbol_table
   {pname; node_hash; location; tenv; integer_type_widths; symbol_table}
 
 
-type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
+type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.t -> Dom.Mem.t
 
-type check_fun = model_env -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t
+type check_fun = model_env -> Dom.Mem.t -> PO.ConditionSet.t -> PO.ConditionSet.t
 
 type model = {exec: exec_fun; check: check_fun}
 
@@ -41,8 +41,8 @@ type declare_local_fun =
   -> inst_num:int
   -> represents_multiple_values:bool
   -> dimension:int
-  -> Dom.Mem.astate
+  -> Dom.Mem.t
-  -> Dom.Mem.astate * int
+  -> Dom.Mem.t * int
 
 type declare_symbolic_fun =
      decl_sym_val:BoUtils.Exec.decl_sym_val
@@ -53,8 +53,8 @@ type declare_symbolic_fun =
   -> inst_num:int
   -> new_sym_num:Counter.t
   -> new_alloc_num:Counter.t
-  -> Dom.Mem.astate
+  -> Dom.Mem.t
-  -> Dom.Mem.astate
+  -> Dom.Mem.t
 
 type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun}
 

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -18,7 +18,7 @@ module ValTrace = BufferOverrunTrace
 type checked_condition = {report_issue_type: IssueType.t option; propagate: bool}
 
 module AllocSizeCondition = struct
-  type t = ItvPure.astate
+  type t = ItvPure.t
 
   let get_symbols = ItvPure.get_symbols
 
@@ -101,13 +101,13 @@ end
 
 module ArrayAccessCondition = struct
   type t =
-    { offset: ItvPure.astate
+    { offset: ItvPure.t
-    ; idx: ItvPure.astate
+    ; idx: ItvPure.t
-    ; size: ItvPure.astate
+    ; size: ItvPure.t
     ; is_collection_add: bool
     ; idx_sym_exp: Relation.SymExp.t option
     ; size_sym_exp: Relation.SymExp.t option
-    ; relation: Relation.astate }
+    ; relation: Relation.t }
   [@@deriving compare]
 
   let get_symbols c =
@@ -150,7 +150,7 @@ module ArrayAccessCondition = struct
       -> is_collection_add:bool
       -> idx_sym_exp:Relation.SymExp.t option
       -> size_sym_exp:Relation.SymExp.t option
-      -> relation:Relation.astate
+      -> relation:Relation.t
       -> t option =
    fun ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp ~relation ->
     if ItvPure.is_invalid offset || ItvPure.is_invalid idx || ItvPure.is_invalid size then None
@@ -302,7 +302,7 @@ module ArrayAccessCondition = struct
       {report_issue_type; propagate= is_symbolic}
 
 
-  let subst : Bound.eval_sym -> Relation.SubstMap.t -> Relation.astate -> t -> t option =
+  let subst : Bound.eval_sym -> Relation.SubstMap.t -> Relation.t -> t -> t option =
    fun eval_sym rel_map caller_relation c ->
     match
       (ItvPure.subst c.offset eval_sym, ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym)
@@ -338,8 +338,8 @@ module BinaryOperationCondition = struct
     { binop: binop_t
     ; typ: Typ.ikind
     ; integer_widths: Typ.IntegerWidths.t
-    ; lhs: ItvPure.astate
+    ; lhs: ItvPure.t
-    ; rhs: ItvPure.astate }
+    ; rhs: ItvPure.t }
 
   let get_symbols c = Symb.SymbolSet.union (ItvPure.get_symbols c.lhs) (ItvPure.get_symbols c.rhs)
 

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -35,26 +35,26 @@ module ConditionSet : sig
 
   val add_array_access :
        Location.t
-    -> offset:ItvPure.astate
+    -> offset:ItvPure.t
-    -> idx:ItvPure.astate
+    -> idx:ItvPure.t
-    -> size:ItvPure.astate
+    -> size:ItvPure.t
     -> is_collection_add:bool
     -> idx_sym_exp:Relation.SymExp.t option
     -> size_sym_exp:Relation.SymExp.t option
-    -> relation:Relation.astate
+    -> relation:Relation.t
     -> idx_traces:BufferOverrunTrace.Set.t
     -> arr_traces:BufferOverrunTrace.Set.t
     -> t
     -> t
 
-  val add_alloc_size : Location.t -> length:ItvPure.astate -> BufferOverrunTrace.Set.t -> t -> t
+  val add_alloc_size : Location.t -> length:ItvPure.t -> BufferOverrunTrace.Set.t -> t -> t
 
   val add_binary_operation :
        Typ.IntegerWidths.t
     -> Location.t
     -> Binop.t
-    -> lhs:ItvPure.astate
+    -> lhs:ItvPure.t
-    -> rhs:ItvPure.astate
+    -> rhs:ItvPure.t
     -> lhs_traces:BufferOverrunTrace.Set.t
     -> rhs_traces:BufferOverrunTrace.Set.t
     -> t
@@ -66,7 +66,7 @@ module ConditionSet : sig
        summary_t
     -> Bounds.Bound.eval_sym * (Symb.Symbol.t -> BufferOverrunTrace.Set.t)
     -> Relation.SubstMap.t
-    -> Relation.astate
+    -> Relation.t
     -> Typ.Procname.t
     -> Location.t
     -> t

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -21,7 +21,7 @@ let eval_const : Const.t -> Val.t = function
       Val.Itv.top
 
 
-let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool =
+let rec must_alias : Exp.t -> Exp.t -> Mem.t -> bool =
  fun e1 e2 m ->
   match (e1, e2) with
   | Exp.Var x1, Exp.Var x2 -> (
@@ -56,7 +56,7 @@ let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool =
       false
 
 
-and must_alias_opt : Exp.t option -> Exp.t option -> Mem.astate -> bool =
+and must_alias_opt : Exp.t option -> Exp.t option -> Mem.t -> bool =
  fun e1_opt e2_opt m ->
   match (e1_opt, e2_opt) with
   | Some e1, Some e2 ->
@@ -101,7 +101,7 @@ let comp_not : Binop.t -> Binop.t = function
       assert false
 
 
-let rec must_alias_cmp : Exp.t -> Mem.astate -> bool =
+let rec must_alias_cmp : Exp.t -> Mem.t -> bool =
  fun e m ->
   match e with
   | Exp.BinOp (Binop.Lt, e1, e2) | Exp.BinOp (Binop.Gt, e1, e2) | Exp.BinOp (Binop.Ne, e1, e2) ->
@@ -140,7 +140,7 @@ let set_array_stride integer_type_widths typ v =
       v
 
 
-let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t =
+let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
  fun integer_type_widths exp mem ->
   if must_alias_cmp exp mem then Val.Itv.zero
   else
@@ -201,7 +201,7 @@ and eval_lindex integer_type_widths array_exp index_exp mem =
         Val.plus_pi array_v index_v
 
 
-and eval_unop : Typ.IntegerWidths.t -> Unop.t -> Exp.t -> Mem.astate -> Val.t =
+and eval_unop : Typ.IntegerWidths.t -> Unop.t -> Exp.t -> Mem.t -> Val.t =
  fun integer_type_widths unop e mem ->
   let v = eval integer_type_widths e mem in
   match unop with
@@ -213,7 +213,7 @@ and eval_unop : Typ.IntegerWidths.t -> Unop.t -> Exp.t -> Mem.astate -> Val.t =
       Val.lnot v
 
 
-and eval_binop : Typ.IntegerWidths.t -> Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t =
+and eval_binop : Typ.IntegerWidths.t -> Binop.t -> Exp.t -> Exp.t -> Mem.t -> Val.t =
  fun integer_type_widths binop e1 e2 mem ->
   let v1 = eval integer_type_widths e1 mem in
   let v2 = eval integer_type_widths e2 mem in
@@ -264,7 +264,7 @@ and eval_binop : Typ.IntegerWidths.t -> Binop.t -> Exp.t -> Exp.t -> Mem.astate
    when "x" is a program variable, (eval_arr "x") returns array blocks
    the "x" is pointing to, on the other hand, (eval "x") returns the
    abstract location of "x". *)
-let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t =
+let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
  fun integer_type_widths exp mem ->
   match exp with
   | Exp.Var id -> (
@@ -385,7 +385,7 @@ let get_offset_sym_f integer_type_widths mem e =
 let get_size_sym_f integer_type_widths mem e = Val.get_size_sym (eval integer_type_widths e mem)
 
 module Prune = struct
-  type astate = {prune_pairs: PrunePairs.astate; mem: Mem.astate}
+  type t = {prune_pairs: PrunePairs.t; mem: Mem.t}
 
   let update_mem_in_prune lv v {prune_pairs; mem} =
     let prune_pairs = PrunePairs.add lv v prune_pairs in
@@ -393,7 +393,7 @@ module Prune = struct
     {prune_pairs; mem}
 
 
-  let prune_unop : Exp.t -> astate -> astate =
+  let prune_unop : Exp.t -> t -> t =
    fun e ({mem} as astate) ->
     match e with
     | Exp.Var x -> (
@@ -425,7 +425,7 @@ module Prune = struct
         astate
 
 
-  let rec prune_binop_left : Typ.IntegerWidths.t -> Exp.t -> astate -> astate =
+  let rec prune_binop_left : Typ.IntegerWidths.t -> Exp.t -> t -> t =
    fun integer_type_widths e ({mem} as astate) ->
     match e with
     | Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e')
@@ -480,7 +480,7 @@ module Prune = struct
         astate
 
 
-  let prune_binop_right : Typ.IntegerWidths.t -> Exp.t -> astate -> astate =
+  let prune_binop_right : Typ.IntegerWidths.t -> Exp.t -> t -> t =
    fun integer_type_widths e astate ->
     match e with
     | Exp.BinOp (((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as c), e1, e2)
@@ -490,7 +490,7 @@ module Prune = struct
         astate
 
 
-  let is_unreachable_constant : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> bool =
+  let is_unreachable_constant : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> bool =
    fun integer_type_widths e m ->
     let v = eval integer_type_widths e m in
     Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0)
@@ -498,7 +498,7 @@ module Prune = struct
     && ArrayBlk.is_bot (Val.get_array_blk v)
 
 
-  let prune_unreachable : Typ.IntegerWidths.t -> Exp.t -> astate -> astate =
+  let prune_unreachable : Typ.IntegerWidths.t -> Exp.t -> t -> t =
    fun integer_type_widths e ({mem} as astate) ->
     if is_unreachable_constant integer_type_widths e mem || Mem.is_relation_unsat mem then
       {astate with mem= Mem.bot}
@@ -537,7 +537,7 @@ module Prune = struct
         astate
 
 
-  let prune : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Mem.astate =
+  let prune : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Mem.t =
    fun integer_type_widths e mem ->
     let mem = Mem.apply_latest_prune e mem in
     let mem =
@@ -557,8 +557,8 @@ let get_matching_pairs :
     -> Val.t
     -> Exp.t option
     -> Typ.t
-    -> Mem.astate
+    -> Mem.t
-    -> Mem.astate
+    -> Mem.t
     -> (Relation.Var.t * Relation.SymExp.t option) list =
  fun tenv integer_type_widths callee_v actual actual_exp_opt typ caller_mem callee_exit_mem ->
   let get_offset_sym v = Val.get_offset_sym v in
@@ -649,8 +649,8 @@ let get_subst_map :
     -> Typ.IntegerWidths.t
     -> Procdesc.t
     -> (Exp.t * 'a) list
-    -> Mem.astate
+    -> Mem.t
-    -> Mem.astate
+    -> Mem.t
     -> Relation.SubstMap.t =
  fun tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem ->
   let add_pair (formal, typ) (actual, actual_exp) rel_l =

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -44,8 +44,8 @@ module Exec = struct
     -> inst_num:int
     -> represents_multiple_values:bool
     -> dimension:int
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
-    -> Dom.Mem.astate * int
+    -> Dom.Mem.t * int
 
   let decl_local_array :
          decl_local:decl_local
@@ -59,8 +59,8 @@ module Exec = struct
       -> inst_num:int
       -> represents_multiple_values:bool
       -> dimension:int
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
-      -> Dom.Mem.astate * int =
+      -> Dom.Mem.t * int =
    fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num
        ~represents_multiple_values ~dimension mem ->
     let offset = Itv.zero in
@@ -92,8 +92,8 @@ module Exec = struct
       -> inst_num:int
       -> represents_multiple_values:bool
       -> dimension:int
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
-      -> Dom.Mem.astate * int =
+      -> Dom.Mem.t * int =
    fun pname ~node_hash location loc ~inst_num ~represents_multiple_values ~dimension mem ->
     let path = Loc.get_path loc in
     let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in
@@ -121,8 +121,8 @@ module Exec = struct
     -> depth:int
     -> Loc.t
     -> Typ.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
 
   let decl_sym_arr :
          decl_sym_val:decl_sym_val
@@ -142,8 +142,8 @@ module Exec = struct
       -> inst_num:int
       -> new_sym_num:Counter.t
       -> new_alloc_num:Counter.t
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
-      -> Dom.Mem.astate =
+      -> Dom.Mem.t =
    fun ~decl_sym_val deref_kind pname symbol_table path tenv ~node_hash location ~depth loc typ
        ?offset ?size ?stride ~inst_num ~new_sym_num ~new_alloc_num mem ->
     let offset =
@@ -186,8 +186,8 @@ module Exec = struct
       -> Typ.t
       -> inst_num:int
       -> new_alloc_num:Counter.t
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
-      -> Dom.Mem.astate =
+      -> Dom.Mem.t =
    fun ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num
        mem ->
     let alloc_num = Counter.next new_alloc_num in
@@ -212,8 +212,8 @@ module Exec = struct
       -> Location.t
       -> Loc.t
       -> new_sym_num:Counter.t
-      -> Dom.Mem.astate
+      -> Dom.Mem.t
-      -> Dom.Mem.astate =
+      -> Dom.Mem.t =
    fun pname symbol_table path location loc ~new_sym_num mem ->
     let size =
       let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -12,9 +12,9 @@ module Relation = BufferOverrunDomainRelation
 module PO = BufferOverrunProofObligations
 
 module Exec : sig
-  val get_alist_size : Dom.Val.t -> Dom.Mem.astate -> Dom.Val.astate
+  val get_alist_size : Dom.Val.t -> Dom.Mem.t -> Dom.Val.t
 
-  val load_val : Ident.t -> Dom.Val.astate -> Dom.Mem.astate -> Dom.Mem.astate
+  val load_val : Ident.t -> Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t
 
   type decl_local =
        Typ.Procname.t
@@ -25,8 +25,8 @@ module Exec : sig
     -> inst_num:int
     -> represents_multiple_values:bool
     -> dimension:int
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
-    -> Dom.Mem.astate * int
+    -> Dom.Mem.t * int
 
   val decl_local_array :
        decl_local:decl_local
@@ -40,8 +40,8 @@ module Exec : sig
     -> inst_num:int
     -> represents_multiple_values:bool
     -> dimension:int
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
-    -> Dom.Mem.astate * int
+    -> Dom.Mem.t * int
 
   val decl_local_collection :
        Typ.Procname.t
@@ -51,8 +51,8 @@ module Exec : sig
     -> inst_num:int
     -> represents_multiple_values:bool
     -> dimension:int
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
-    -> Dom.Mem.astate * int
+    -> Dom.Mem.t * int
 
   type decl_sym_val =
        Typ.Procname.t
@@ -63,8 +63,8 @@ module Exec : sig
     -> depth:int
     -> Loc.t
     -> Typ.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
 
   val decl_sym_arr :
        decl_sym_val:decl_sym_val
@@ -84,8 +84,8 @@ module Exec : sig
     -> inst_num:int
     -> new_sym_num:Counter.t
     -> new_alloc_num:Counter.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
 
   val decl_sym_java_ptr :
        decl_sym_val:decl_sym_val
@@ -99,8 +99,8 @@ module Exec : sig
     -> Typ.t
     -> inst_num:int
     -> new_alloc_num:Counter.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
 
   val decl_sym_collection :
        Typ.Procname.t
@@ -109,8 +109,8 @@ module Exec : sig
     -> Location.t
     -> Loc.t
     -> new_sym_num:Counter.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
 
   val init_array_fields :
        Tenv.t
@@ -121,11 +121,10 @@ module Exec : sig
     -> Typ.t
     -> PowLoc.t
     -> ?dyn_length:Exp.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
 
-  val set_dyn_length :
+  val set_dyn_length : Location.t -> Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.t -> Dom.Mem.t
-    Location.t -> Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.astate -> Dom.Mem.astate
 end
 
 module Check : sig
@@ -133,7 +132,7 @@ module Check : sig
        arr:Dom.Val.t
     -> idx:Dom.Val.t
     -> idx_sym_exp:Relation.SymExp.t option
-    -> relation:Relation.astate
+    -> relation:Relation.t
     -> is_plus:bool
     -> Location.t
     -> PO.ConditionSet.t
@@ -143,7 +142,7 @@ module Check : sig
        Typ.IntegerWidths.t
     -> array_exp:Exp.t
     -> index_exp:Exp.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
     -> Location.t
     -> PO.ConditionSet.t
     -> PO.ConditionSet.t
@@ -152,7 +151,7 @@ module Check : sig
        Typ.IntegerWidths.t
     -> array_exp:Exp.t
     -> byte_index_exp:Exp.t
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
     -> Location.t
     -> PO.ConditionSet.t
     -> PO.ConditionSet.t
@@ -162,7 +161,7 @@ module Check : sig
     -> array_exp:Exp.t
     -> index_exp:Exp.t
     -> ?is_collection_add:bool
-    -> Dom.Mem.astate
+    -> Dom.Mem.t
     -> Location.t
     -> PO.ConditionSet.t
     -> PO.ConditionSet.t

infer/src/bufferoverrun/itv.ml

@@ -29,15 +29,13 @@ module ItvRange = struct
     |> Bound.simplify_bound_ends_from_paths |> Bounds.NonNegativeBound.of_bound
 
 
-  let to_top_lifted_polynomial : t -> Polynomials.NonNegativePolynomial.astate =
+  let to_top_lifted_polynomial : t -> Polynomials.NonNegativePolynomial.t =
    fun r -> Polynomials.NonNegativePolynomial.of_non_negative_bound r
 end
 
 module ItvPure = struct
   (** (l, u) represents the closed interval [l; u] (of course infinite bounds are open) *)
-  type astate = Bound.t * Bound.t [@@deriving compare]
+  type t = Bound.t * Bound.t [@@deriving compare]
-
-  type t = astate
 
   let lb : t -> Bound.t = fst
 
@@ -416,8 +414,6 @@ end
 
 include AbstractDomain.BottomLifted (ItvPure)
 
-type t = astate
-
 let compare : t -> t -> int =
  fun x y ->
   match (x, y) with
@@ -428,7 +424,7 @@ let compare : t -> t -> int =
   | _, Bottom ->
       1
   | NonBottom x, NonBottom y ->
-      ItvPure.compare_astate x y
+      ItvPure.compare x y
 
 
 let bot : t = Bottom
@@ -486,13 +482,13 @@ let of_bool = function
       unknown_bool
 
 
-let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n)
+let of_int : int -> t = fun n -> NonBottom (ItvPure.of_int n)
 
-let of_big_int : Z.t -> astate = fun n -> NonBottom (ItvPure.of_big_int n)
+let of_big_int : Z.t -> t = fun n -> NonBottom (ItvPure.of_big_int n)
 
-let of_int_lit : IntLit.t -> astate = fun n -> of_big_int (IntLit.to_big_int n)
+let of_int_lit : IntLit.t -> t = fun n -> of_big_int (IntLit.to_big_int n)
 
-let of_int64 : Int64.t -> astate = fun n -> of_big_int (Z.of_int64 n)
+let of_int64 : Int64.t -> t = fun n -> of_big_int (Z.of_int64 n)
 
 let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false
 
@@ -555,9 +551,9 @@ let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t
   NonBottom (ItvPure.make_sym ~unsigned pname symbol_table path new_sym_num)
 
 
-let is_const : astate -> Z.t option = bind1zo ItvPure.is_const
+let is_const : t -> Z.t option = bind1zo ItvPure.is_const
 
-let eq_const : Z.t -> astate -> bool = fun z -> bind1bool (ItvPure.eq_const z)
+let eq_const : Z.t -> t -> bool = fun z -> bind1bool (ItvPure.eq_const z)
 
 let neg : t -> t = lift1 ItvPure.neg
 

infer/src/bufferoverrun/itv.mli

@@ -16,13 +16,11 @@ module SymbolSet = Symb.SymbolSet
 module ItvRange : sig
   type t
 
-  val to_top_lifted_polynomial : t -> Polynomials.NonNegativePolynomial.astate
+  val to_top_lifted_polynomial : t -> Polynomials.NonNegativePolynomial.t
 end
 
 module ItvPure : sig
-  type astate [@@deriving compare]
+  type t [@@deriving compare]
-
-  type t = astate
 
   val pp : F.formatter -> t -> unit
 
@@ -103,7 +101,7 @@ end
 
 include module type of AbstractDomain.BottomLifted (ItvPure)
 
-type t = astate [@@deriving compare]
+val compare : t -> t -> int
 
 val bot : t
 (** _|_ *)

infer/src/bufferoverrun/polynomials.ml

@@ -105,8 +105,6 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
   *)
   type t = {const: NonNegativeInt.t; terms: t M.t}
 
-  type astate = t
-
   let of_non_negative_int : NonNegativeInt.t -> t = fun const -> {const; terms= M.empty}
 
   let zero = of_non_negative_int NonNegativeInt.zero

infer/src/bufferoverrun/polynomials.mli

@@ -21,37 +21,37 @@ end
 module NonNegativePolynomial : sig
   include AbstractDomain.WithTop
 
-  val zero : astate
+  val zero : t
 
-  val one : astate
+  val one : t
 
-  val of_int_exn : int -> astate
+  val of_int_exn : int -> t
 
-  val is_symbolic : astate -> bool
+  val is_symbolic : t -> bool
 
-  val is_top : astate -> bool
+  val is_top : t -> bool
 
-  val is_zero : astate -> bool
+  val is_zero : t -> bool
 
-  val of_non_negative_bound : Bounds.NonNegativeBound.t -> astate
+  val of_non_negative_bound : Bounds.NonNegativeBound.t -> t
 
-  val plus : astate -> astate -> astate
+  val plus : t -> t -> t
 
-  val mult : astate -> astate -> astate
+  val mult : t -> t -> t
 
-  val min_default_left : astate -> astate -> astate
+  val min_default_left : t -> t -> t
 
-  val subst : astate -> Bound.eval_sym -> astate
+  val subst : t -> Bound.eval_sym -> t
 
-  val degree : astate -> Degree.t option
+  val degree : t -> Degree.t option
 
-  val compare_by_degree : astate -> astate -> int
+  val compare_by_degree : t -> t -> int
 
-  val pp_degree : Format.formatter -> astate -> unit
+  val pp_degree : Format.formatter -> t -> unit
 
-  val pp_degree_hum : Format.formatter -> astate -> unit
+  val pp_degree_hum : Format.formatter -> t -> unit
 
-  val encode : astate -> string
+  val encode : t -> string
 
-  val decode : string -> astate
+  val decode : string -> t
 end

infer/src/checkers/IdAccessPathMapDomain.ml

@@ -9,9 +9,11 @@ open! IStd
 module IdMap = Var.Map
 module L = Logging
 
-type astate = AccessExpression.t IdMap.t
+include (IdMap : module type of IdMap with type 'a t := 'a IdMap.t)
 
-include IdMap
+type t = AccessExpression.t IdMap.t
+
+type value = AccessExpression.t
 
 let pp fmt astate = IdMap.pp ~pp_value:AccessExpression.pp fmt astate
 

infer/src/checkers/IdAccessPathMapDomain.mli

@@ -9,10 +9,4 @@ open! IStd
 
 (** mapping of ids to raw access paths. useful for id-normalizing access paths *)
 
-module IdMap = Var.Map
+include AbstractDomain.MapS with type key = Var.t and type value = AccessExpression.t
-
-type astate = AccessExpression.t IdMap.t
-
-include module type of IdMap
-
-include AbstractDomain.WithBottom with type astate := astate

infer/src/checkers/Litho.ml

@@ -10,7 +10,7 @@ module F = Format
 module Domain = LithoDomain
 
 module Payload = SummaryPayload.Make (struct
-  type t = Domain.astate
+  type t = Domain.t
 
   let update_payloads astate (payloads : Payloads.t) = {payloads with litho= Some astate}
 
@@ -208,7 +208,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         astate
 
 
-  let exec_instr astate (proc_data : extras ProcData.t) _ (instr : HilInstr.t) : Domain.astate =
+  let exec_instr astate (proc_data : extras ProcData.t) _ (instr : HilInstr.t) : Domain.t =
     let caller_pname = Procdesc.get_proc_name proc_data.pdesc in
     match instr with
     | Call
@@ -276,7 +276,7 @@ let checker {Callbacks.summary; proc_desc; tenv} =
   | Some post ->
       if RequiredProps.should_report proc_desc tenv then RequiredProps.report post tenv summary ;
       if GraphQLGetters.should_report proc_desc then GraphQLGetters.report post summary ;
-      let postprocess astate formal_map : Domain.astate =
+      let postprocess astate formal_map : Domain.t =
         let f_sub access_path = Domain.LocalAccessPath.to_formal_option access_path formal_map in
         Domain.substitute ~f_sub astate
       in

infer/src/checkers/LithoDomain.mli

@@ -32,9 +32,9 @@ module CallSet : module type of AbstractDomain.FiniteSet (MethodCall)
 
 include module type of AbstractDomain.Map (LocalAccessPath) (CallSet)
 
-val substitute : f_sub:(LocalAccessPath.t -> LocalAccessPath.t option) -> astate -> astate
+val substitute : f_sub:(LocalAccessPath.t -> LocalAccessPath.t option) -> t -> t
 (** Substitute each access path in the domain using [f_sub]. If [f_sub] returns None, the
     original access path is retained; otherwise, the new one is used *)
 
-val iter_call_chains : f:(AccessPath.t -> Typ.Procname.t list -> unit) -> astate -> unit
+val iter_call_chains : f:(AccessPath.t -> Typ.Procname.t list -> unit) -> t -> unit
-(** Apply [f] to each maximal call chain encoded in [astate] *)
+(** Apply [f] to each maximal call chain encoded in [t] *)

infer/src/checkers/NullabilityCheck.ml

@@ -179,7 +179,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   let find_nullable_ap ap (aps, _) = NullableAP.find ap aps
 
-  let assume_pnames_notnull ap (aps, checked_pnames) : Domain.astate =
+  let assume_pnames_notnull ap (aps, checked_pnames) : Domain.t =
     let remove_call_sites ap aps =
       let add_diff (to_remove : CallSites.t) ap call_sites map =
         let remaining_call_sites = CallSites.diff call_sites to_remove in
@@ -235,7 +235,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         check_nil_in_objc_container proc_data loc other_args astate
 
 
-  let exec_instr ((_, checked_pnames) as astate) proc_data _ (instr : HilInstr.t) : Domain.astate =
+  let exec_instr ((_, checked_pnames) as astate) proc_data _ (instr : HilInstr.t) : Domain.t =
     let is_pointer_assignment tenv lhs rhs =
       (* the rhs has type int when assigning the lhs to null *)
       if HilExp.is_null_literal rhs then true

infer/src/checkers/NullabilitySuggest.ml

@@ -10,13 +10,13 @@ module L = Logging
 module MF = MarkupFormatter
 
 module UseDefChain = struct
-  type astate =
+  type t =
     | DependsOn of (Location.t * AccessPath.t)
     | NullDefCompare of (Location.t * AccessPath.t)
     | NullDefAssign of (Location.t * AccessPath.t)
   [@@deriving compare]
 
-  let ( <= ) ~lhs ~rhs = compare_astate lhs rhs <= 0
+  let ( <= ) ~lhs ~rhs = compare lhs rhs <= 0
 
   (* Keep only one chain in join/widen as we are going to report only one
    * trace to the user eventually. *)
@@ -34,9 +34,9 @@ module UseDefChain = struct
 
 
   module Set = Caml.Set.Make (struct
-    type t = astate
+    type nonrec t = t
 
-    let compare = compare_astate
+    let compare = compare
   end)
 end
 
@@ -90,7 +90,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         None
 
 
-  let exec_instr (astate : Domain.astate) proc_data _ (instr : HilInstr.t) =
+  let exec_instr (astate : Domain.t) proc_data _ (instr : HilInstr.t) =
     match instr with
     | Assume (expr, _, _, loc) -> (
       match extract_null_compare_expr expr with

infer/src/checkers/Ownership.ml

@@ -20,11 +20,11 @@ end
 module VarSet = AbstractDomain.FiniteSet (Base)
 
 module CapabilityDomain = struct
-  type astate =
+  type t =
     | InvalidatedAt of Location.t
         (** neither owned nor borrowed; we can't safely do anything with this value. tagged with the
         location where invalidation occurred. *)
-    | BorrowedFrom of VarSet.astate
+    | BorrowedFrom of VarSet.t
         (** not owned, but borrowed from existing reference(s). for now, permits both reads and writes *)
     | Owned
         (** owned. permits reads, writes, and ownership transfer (e.g. call a destructor, delete, or free) *)
@@ -315,7 +315,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         false
 
 
-  let exec_instr (astate : Domain.astate) (proc_data : extras ProcData.t) _ (instr : HilInstr.t) =
+  let exec_instr (astate : Domain.t) (proc_data : extras ProcData.t) _ (instr : HilInstr.t) =
     let summary = proc_data.extras in
     match instr with
     | Assign (lhs_access_exp, rhs_exp, loc) -> (
@@ -388,7 +388,7 @@ let report_invalid_return post end_loc summary =
            List.mem ~equal:Mangled.equal locals mangled )
   in
   (* look for return values that are borrowed from (now-invalid) local variables *)
-  let report_invalid_return base (capability : CapabilityDomain.astate) =
+  let report_invalid_return base (capability : CapabilityDomain.t) =
     if Var.is_return (fst base) then
       match capability with
       | BorrowedFrom vars ->

infer/src/checkers/PulseDomain.ml

@@ -208,7 +208,7 @@ module Stack =
   AbstractDomain.Map
     (Var)
     (struct
-      type astate = AbstractAddress.t
+      type t = AbstractAddress.t
 
       let ( <= ) ~lhs ~rhs = AbstractAddress.equal lhs rhs
 
@@ -220,7 +220,7 @@ module Stack =
     end)
 
 (** the domain *)
-type t = {heap: Memory.t; stack: Stack.astate}
+type astate = {heap: Memory.t; stack: Stack.t}
 
 let initial =
   { heap=
@@ -230,8 +230,8 @@ let initial =
   ; stack= Stack.empty }
 
 
-module Domain : AbstractDomain.S with type astate = t = struct
+module Domain : AbstractDomain.S with type t = astate = struct
-  type astate = t
+  type t = astate
 
   let piecewise_lessthan lhs rhs =
     Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack

infer/src/checkers/PulseDomain.mli

@@ -15,9 +15,7 @@ module AbstractAddress : sig
   val init : unit -> unit
 end
 
-type t
+include AbstractDomain.S
-
-include AbstractDomain.S with type astate = t
 
 val initial : t
 

infer/src/checkers/SimpleChecker.ml

@@ -14,24 +14,23 @@ module L = Logging
 
 module type Spec = sig
   (** what state do you want to propagate? *)
-  type astate
+  type t
 
-  val initial : astate
+  val initial : t
   (** implement the state the analysis should start from here *)
 
-  val exec_instr :
+  val exec_instr : t -> Sil.instr -> Procdesc.Node.nodekind -> Typ.Procname.t -> Tenv.t -> t
-    astate -> Sil.instr -> Procdesc.Node.nodekind -> Typ.Procname.t -> Tenv.t -> astate
   (** implement how an instruction changes your state here.
       input is the previous state, current instruction, current node kind, current procedure and
       type environment.
   *)
 
-  val report : astate -> Location.t -> Typ.Procname.t -> unit
+  val report : t -> Location.t -> Typ.Procname.t -> unit
   (** log errors here.
       input is a state, location where the state occurs in the source, and the current procedure.
   *)
 
-  val compare : astate -> astate -> int
+  val compare : t -> t -> int
 end
 
 module type S = sig
@@ -40,10 +39,10 @@ module type S = sig
 end
 
 module Make (Spec : Spec) : S = struct
-  (* powerset domain over Spec.astate *)
+  (* powerset domain over Spec.t *)
   module Domain = struct
     include AbstractDomain.FiniteSet (struct
-      type t = Spec.astate
+      type t = Spec.t
 
       let compare = Spec.compare
 

infer/src/checkers/SimpleChecker.mli

@@ -8,16 +8,15 @@
 open! IStd
 
 module type Spec = sig
-  type astate
+  type t
 
-  val initial : astate
+  val initial : t
 
-  val exec_instr :
+  val exec_instr : t -> Sil.instr -> Procdesc.Node.nodekind -> Typ.Procname.t -> Tenv.t -> t
-    astate -> Sil.instr -> Procdesc.Node.nodekind -> Typ.Procname.t -> Tenv.t -> astate
 
-  val report : astate -> Location.t -> Typ.Procname.t -> unit
+  val report : t -> Location.t -> Typ.Procname.t -> unit
 
-  val compare : astate -> astate -> int
+  val compare : t -> t -> int
 end
 
 module type S = sig

infer/src/checkers/Siof.ml

@@ -58,7 +58,7 @@ let is_modelled =
 
 
 module Payload = SummaryPayload.Make (struct
-  type t = SiofDomain.Summary.astate
+  type t = SiofDomain.Summary.t
 
   let update_payloads astate (payloads : Payloads.t) = {payloads with siof= Some astate}
 

infer/src/checkers/Trace.ml

@@ -21,11 +21,7 @@ end
 module type S = sig
   include Spec
 
-  type t
+  include AbstractDomain.WithBottom
-
-  type astate = t
-
-  include AbstractDomain.WithBottom with type astate := astate
 
   module Sources : sig
     module Known : module type of AbstractDomain.FiniteSet (Source)
@@ -36,9 +32,7 @@ module type S = sig
 
     module Sanitizers : module type of AbstractDomain.FiniteSet (Sanitizer)
 
-    type astate = {known: Known.astate; footprint: Footprint.astate; sanitizers: Sanitizers.astate}
+    type t = {known: Known.t; footprint: Footprint.t; sanitizers: Sanitizers.t}
-
-    type t = astate
 
     val empty : t
 
@@ -171,9 +165,7 @@ module Make (Spec : Spec) = struct
     module Footprint = AccessTree.PathSet (FootprintConfig)
     module Sanitizers = AbstractDomain.FiniteSet (Sanitizer)
 
-    type astate = {known: Known.astate; footprint: Footprint.astate; sanitizers: Sanitizers.astate}
+    type t = {known: Known.t; footprint: Footprint.t; sanitizers: Sanitizers.t}
-
-    type t = astate
 
     let ( <= ) ~lhs ~rhs =
       if phys_equal lhs rhs then true
@@ -256,8 +248,6 @@ module Make (Spec : Spec) = struct
           (** last callees in the trace that transitively called a tainted function (if any) *)
     ; passthroughs: Passthrough.Set.t  (** calls that occurred between source and sink *) }
 
-  type astate = t
-
   type path = Passthroughs.t * (Source.t * Passthroughs.t) list * (Sink.t * Passthroughs.t) list
 
   type report =

infer/src/checkers/Trace.mli

@@ -23,11 +23,7 @@ end
 module type S = sig
   include Spec
 
-  type t
+  include AbstractDomain.WithBottom
-
-  type astate = t
-
-  include AbstractDomain.WithBottom with type astate := astate
 
   module Sources : sig
     (** Set of sources returned by callees of the current function *)
@@ -41,9 +37,7 @@ module type S = sig
     (** Set of sanitizers that have been applied to these sources *)
     module Sanitizers : module type of AbstractDomain.FiniteSet (Sanitizer)
 
-    type astate = {known: Known.astate; footprint: Footprint.astate; sanitizers: Sanitizers.astate}
+    type t = {known: Known.t; footprint: Footprint.t; sanitizers: Sanitizers.t}
-
-    type t = astate
 
     val empty : t
 

infer/src/checkers/accessPathDomains.ml

@@ -12,7 +12,7 @@ module Set = struct
 
   (** TODO (12086310): best-case behavior of some operations can be improved by adding "abstracted"
       bool recording whether an abstracted access path has been introduced *)
-  type astate = APSet.t
+  type t = APSet.t
 
   let pp = APSet.pp
 

infer/src/checkers/accessPathDomains.mli

@@ -17,19 +17,19 @@ open! IStd
 module Set : sig
   include AbstractDomain.WithBottom
 
-  val of_list : AccessPath.Abs.t list -> astate
+  val of_list : AccessPath.Abs.t list -> t
 
-  val mem : AccessPath.Abs.t -> astate -> bool
+  val mem : AccessPath.Abs.t -> t -> bool
   (** return true if {% \gamma(\{ap\}) \subseteq \gamma(aps) %}.
       note: this is worst-case linear in the size of the set *)
 
-  val mem_fuzzy : AccessPath.Abs.t -> astate -> bool
+  val mem_fuzzy : AccessPath.Abs.t -> t -> bool
   (** more permissive version of [mem]; return true if {% \gamma(\{a\}) \cap \gamma(aps) != \{\} %}.
       note: this is worst-case linear in the size of the set *)
 
-  val add : AccessPath.Abs.t -> astate -> astate
+  val add : AccessPath.Abs.t -> t -> t
 
-  val normalize : astate -> astate
+  val normalize : t -> t
   (** simplify an access path set to its canonical representation by eliminating redundancies
       between (1) pairs of abstracted access_paths, and (2) exact access paths and abstracted
       access paths. warning: this is quadratic in the size of the set! use sparingly *)

infer/src/checkers/accessTree.ml

@@ -15,36 +15,34 @@ module type S = sig
 
   module BaseMap = AccessPath.BaseMap
 
-  type node = TraceDomain.astate * tree
+  type node = TraceDomain.t * tree
  and tree = Subtree of node AccessMap.t | Star
 
-  type t = node BaseMap.t
+  include AbstractDomain.WithBottom with type t = node BaseMap.t
-
-  include AbstractDomain.WithBottom with type astate = t
 
   val empty_node : node
 
-  val make_node : TraceDomain.astate -> node AccessMap.t -> node
+  val make_node : TraceDomain.t -> node AccessMap.t -> node
 
-  val make_access_node : TraceDomain.astate -> AccessPath.access -> TraceDomain.astate -> node
+  val make_access_node : TraceDomain.t -> AccessPath.access -> TraceDomain.t -> node
 
-  val make_normal_leaf : TraceDomain.astate -> node
+  val make_normal_leaf : TraceDomain.t -> node
 
-  val make_starred_leaf : TraceDomain.astate -> node
+  val make_starred_leaf : TraceDomain.t -> node
 
   val get_node : AccessPath.Abs.t -> t -> node option
 
-  val get_trace : AccessPath.Abs.t -> t -> TraceDomain.astate option
+  val get_trace : AccessPath.Abs.t -> t -> TraceDomain.t option
 
   val add_node : AccessPath.Abs.t -> node -> t -> t
 
-  val add_trace : AccessPath.Abs.t -> TraceDomain.astate -> t -> t
+  val add_trace : AccessPath.Abs.t -> TraceDomain.t -> t -> t
 
   val node_join : node -> node -> node
 
   val fold : ('a -> AccessPath.Abs.t -> node -> 'a) -> t -> 'a -> 'a
 
-  val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a
+  val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.t -> 'a) -> t -> 'a -> 'a
 
   val exists : (AccessPath.Abs.t -> node -> bool) -> t -> bool
 
@@ -90,14 +88,12 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct
 
   module BaseMap = AccessPath.BaseMap
 
-  type node = TraceDomain.astate * tree
+  type node = TraceDomain.t * tree
 
   and tree = Subtree of node AccessMap.t | Star
 
   type t = node BaseMap.t
 
-  type astate = t
-
   let empty = BaseMap.empty
 
   let is_empty = BaseMap.is_empty
@@ -364,7 +360,7 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct
     BaseMap.fold (fun base node acc -> node_fold f base node acc) tree acc_
 
 
-  let trace_fold (f : 'a -> AccessPath.Abs.t -> TraceDomain.astate -> 'a) =
+  let trace_fold (f : 'a -> AccessPath.Abs.t -> TraceDomain.t -> 'a) =
     let f_ acc ap (trace, _) = f acc ap trace in
     fold f_
 

infer/src/checkers/accessTree.mli

@@ -15,7 +15,7 @@ module type S = sig
 
   module BaseMap = AccessPath.BaseMap
 
-  type node = TraceDomain.astate * tree
+  type node = TraceDomain.t * tree
 
   and tree =
     | Subtree of node AccessMap.t
@@ -33,27 +33,26 @@ module type S = sig
                                                         g |-> (T2, Subtree {}) }) }
       ]}
   *)
-  type t = node BaseMap.t
 
-  include AbstractDomain.WithBottom with type astate = t
+  include AbstractDomain.WithBottom with type t = node BaseMap.t
 
   val empty_node : node
 
-  val make_node : TraceDomain.astate -> node AccessMap.t -> node
+  val make_node : TraceDomain.t -> node AccessMap.t -> node
 
-  val make_access_node : TraceDomain.astate -> AccessPath.access -> TraceDomain.astate -> node
+  val make_access_node : TraceDomain.t -> AccessPath.access -> TraceDomain.t -> node
   (** for testing only *)
 
-  val make_normal_leaf : TraceDomain.astate -> node
+  val make_normal_leaf : TraceDomain.t -> node
   (** create a leaf node with no successors *)
 
-  val make_starred_leaf : TraceDomain.astate -> node
+  val make_starred_leaf : TraceDomain.t -> node
   (** create a leaf node with a wildcard successor *)
 
   val get_node : AccessPath.Abs.t -> t -> node option
   (** retrieve the node associated with the given access path *)
 
-  val get_trace : AccessPath.Abs.t -> t -> TraceDomain.astate option
+  val get_trace : AccessPath.Abs.t -> t -> TraceDomain.t option
   (** retrieve the trace associated with the given access path *)
 
   val add_node : AccessPath.Abs.t -> node -> t -> t
@@ -61,7 +60,7 @@ module type S = sig
       if any of the accesses in the path are not already present in the tree, they will be added
       with with empty traces associated with each of the inner nodes. *)
 
-  val add_trace : AccessPath.Abs.t -> TraceDomain.astate -> t -> t
+  val add_trace : AccessPath.Abs.t -> TraceDomain.t -> t -> t
   (** add the given access path to the tree and associate its last access with with the given trace.
       if any of the accesses in the path are not already present in the tree, they will be added
       with with empty traces associated with each of the inner nodes. *)
@@ -72,7 +71,7 @@ module type S = sig
   val fold : ('a -> AccessPath.Abs.t -> node -> 'a) -> t -> 'a -> 'a
   (** apply a function to each (access path, node) pair in the tree. *)
 
-  val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a
+  val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.t -> 'a) -> t -> 'a -> 'a
 
   val exists : (AccessPath.Abs.t -> node -> bool) -> t -> bool
 
@@ -99,5 +98,5 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) :
 module PathSet (Config : Config) : sig
   include module type of Make (AbstractDomain.BooleanOr) (Config)
 
-  val mem : AccessPath.Abs.t -> astate -> bool
+  val mem : AccessPath.Abs.t -> t -> bool
 end

infer/src/checkers/annotationReachability.ml

@@ -36,7 +36,7 @@ module Domain = struct
         else (AnnotReachabilityDomain.add annot sink_map' annot_map, previous_vstate)
 
 
-  let stop_tracking ((annot_map, _) : astate) = (annot_map, Bottom)
+  let stop_tracking ((annot_map, _) : t) = (annot_map, Bottom)
 
   let add_tracking_var var ((annot_map, previous_vstate) as astate) =
     match previous_vstate with
@@ -59,7 +59,7 @@ module Domain = struct
 end
 
 module Payload = SummaryPayload.Make (struct
-  type t = AnnotReachabilityDomain.astate
+  type t = AnnotReachabilityDomain.t
 
   let update_payloads annot_map (payloads : Payloads.t) = {payloads with annot_map= Some annot_map}
 
@@ -236,7 +236,7 @@ module AnnotationSpec = struct
     ; sink_predicate: predicate
     ; sanitizer_predicate: predicate
     ; sink_annotation: Annot.t
-    ; report: Callbacks.proc_callback_args -> AnnotReachabilityDomain.astate -> unit }
+    ; report: Callbacks.proc_callback_args -> AnnotReachabilityDomain.t -> unit }
 
   (* The default sanitizer does not sanitize anything *)
   let default_sanitizer _ _ = false

infer/src/checkers/cost.ml

@@ -67,8 +67,8 @@ module TransferFunctionsNodesBasicCost = struct
   let cost_atomic_instruction = BasicCost.one
 
   let exec_instr_cost integer_type_widths inferbo_mem
-      (astate : CostDomain.NodeInstructionToCostMap.astate) {ProcData.pdesc} (node : CFG.Node.t)
+      (astate : CostDomain.NodeInstructionToCostMap.t) {ProcData.pdesc} (node : CFG.Node.t) instr :
-      instr : CostDomain.NodeInstructionToCostMap.astate =
+      CostDomain.NodeInstructionToCostMap.t =
     let key = CFG.Node.id node in
     let astate' =
       match instr with
@@ -315,7 +315,7 @@ module ControlFlowCost = struct
       { mutable size: int
       ; mutable items: Item.t ARList.t
       ; mutable sums: Sum.t ARList.t
-      ; mutable cost: BasicCost.astate }
+      ; mutable cost: BasicCost.t }
 
     let create e =
       let items, sums =
@@ -387,7 +387,7 @@ module ControlFlowCost = struct
       sum_items t |> List.iter ~f:(fun item -> infer_equalities_by_removing_item ~on_infer t item)
 
 
-    let init_cost : of_node:(Node.id -> BasicCost.astate) -> t -> unit =
+    let init_cost : of_node:(Node.id -> BasicCost.t) -> t -> unit =
      fun ~of_node t ->
       let min_if_node cost item =
         match item with `Node node -> BasicCost.min_default_left cost (of_node node) | _ -> cost
@@ -396,8 +396,8 @@ module ControlFlowCost = struct
 
 
     let improve_cost_from_sums :
-           on_improve:(Sum.t -> BasicCost.astate -> BasicCost.astate -> unit)
+           on_improve:(Sum.t -> BasicCost.t -> BasicCost.t -> unit)
-        -> of_item:(Item.t -> BasicCost.astate)
+        -> of_item:(Item.t -> BasicCost.t)
         -> t
         -> unit =
      fun ~on_improve ~of_item t ->
@@ -604,7 +604,7 @@ module ReportedOnNodes = AbstractDomain.FiniteSetOfPPSet (Node.IdSet)
 
 type extras_TransferFunctionsWCET =
   { basic_cost_map: AnalyzerNodesBasicCost.invariant_map
-  ; get_node_nb_exec: Node.id -> BasicCost.astate
+  ; get_node_nb_exec: Node.id -> BasicCost.t
   ; summary: Summary.t }
 
 let compute_errlog_extras cost =
@@ -669,7 +669,7 @@ module TransferFunctionsWCET = struct
       preds
 
 
-  let map_cost get_node_nb_exec m : BasicCost.astate =
+  let map_cost get_node_nb_exec m : BasicCost.t =
     CostDomain.NodeInstructionToCostMap.fold
       (fun ((node_id, _) as instr_node_id) c acc ->
         let t = get_node_nb_exec node_id in
@@ -685,8 +685,8 @@ module TransferFunctionsWCET = struct
       m BasicCost.zero
 
 
-  let exec_instr ((_, reported_so_far) : Domain.astate) {ProcData.extras} (node : CFG.Node.t) instr
+  let exec_instr ((_, reported_so_far) : Domain.t) {ProcData.extras} (node : CFG.Node.t) instr :
-      : Domain.astate =
+      Domain.t =
     let {basic_cost_map= invariant_map_cost; get_node_nb_exec; summary} = extras in
     let cost_node =
       let instr_node_id = CFG.Node.id node in

infer/src/checkers/cost.mli

@@ -12,8 +12,8 @@ val checker : Callbacks.proc_callback_t
 val instantiate_cost :
      Typ.IntegerWidths.t
   -> caller_pdesc:Procdesc.t
-  -> inferbo_caller_mem:BufferOverrunDomain.Mem.astate option
+  -> inferbo_caller_mem:BufferOverrunDomain.Mem.t option
   -> callee_pname:Typ.Procname.t
   -> params:(Exp.t * 'a) list
-  -> callee_cost:CostDomain.BasicCost.astate
+  -> callee_cost:CostDomain.BasicCost.t
-  -> CostDomain.BasicCost.astate
+  -> CostDomain.BasicCost.t

infer/src/checkers/costDomain.ml

@@ -12,6 +12,6 @@ module BasicCost = Polynomials.NonNegativePolynomial
 (** Map (node,instr) -> basic cost  *)
 module NodeInstructionToCostMap = AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (BasicCost)
 
-type summary = {post: BasicCost.astate}
+type summary = {post: BasicCost.t}
 
 let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" BasicCost.pp post

infer/src/checkers/purity.ml

@@ -93,7 +93,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         Domain.pure
 
 
-  let exec_instr (astate : Domain.astate) {ProcData.pdesc; tenv; ProcData.extras= formals} _
+  let exec_instr (astate : Domain.t) {ProcData.pdesc; tenv; ProcData.extras= formals} _
       (instr : HilInstr.t) =
     match instr with
     | Assign (ae, _, _) when is_heap_access ae ->

infer/src/checkers/purityDomain.ml

@@ -34,6 +34,6 @@ let get_modified_params astate =
       None
 
 
-type summary = Domain.astate
+type summary = Domain.t
 
 let pp_summary fmt astate = F.fprintf fmt "@\n Purity summary: %a @\n" Domain.pp astate

infer/src/checkers/uninit.ml

@@ -162,7 +162,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           let maybe_uninit_vars = MaybeUninitVars.remove access_expr maybe_uninit_vars in
           if remove_fields then
             let base = AccessExpression.get_base access_expr in
-            MaybeUninitVars.remove_init_fields base var_formal maybe_uninit_vars init_formals
+            let init_formals' = MaybeUninitVars.of_list (D.elements init_formals) in
+            MaybeUninitVars.remove_init_fields base var_formal maybe_uninit_vars init_formals'
           else maybe_uninit_vars
       | _ ->
           maybe_uninit_vars )
@@ -179,7 +180,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         false
 
 
-  let exec_instr (astate : Domain.astate) {ProcData.pdesc; extras= {formals; summary}; tenv} _
+  let exec_instr (astate : Domain.t) {ProcData.pdesc; extras= {formals; summary}; tenv} _
       (instr : HilInstr.t) =
     let check_access_expr ~loc rhs_access_expr =
       if should_report_var pdesc tenv astate.maybe_uninit_vars rhs_access_expr then

infer/src/checkers/uninitDomain.ml

@@ -94,10 +94,7 @@ module Record
     (Domain2 : AbstractDomain.S)
     (Domain3 : AbstractDomain.S) =
 struct
-  type astate =
+  type t = {maybe_uninit_vars: Domain1.t; aliased_vars: Domain2.t; prepost: Domain3.t prepost}
-    { maybe_uninit_vars: Domain1.astate
-    ; aliased_vars: Domain2.astate
-    ; prepost: Domain3.astate prepost }
 
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true

infer/src/concurrency/ExplicitTrace.ml

@@ -9,11 +9,9 @@ module F = Format
 module MF = MarkupFormatter
 
 module type FiniteSet = sig
-  include PrettyPrintable.PPSet
+  include AbstractDomain.FiniteSetS
 
-  include AbstractDomain.WithBottom with type astate = t
+  val with_callsite : t -> CallSite.t -> t
-
-  val with_callsite : astate -> CallSite.t -> astate
 end
 
 module type TraceElem = sig

infer/src/concurrency/ExplicitTrace.mli

@@ -9,11 +9,9 @@ open! IStd
 
 (** A powerset domain of traces, with bottom = empty and join = union *)
 module type FiniteSet = sig
-  include PrettyPrintable.PPSet
+  include AbstractDomain.FiniteSetS
 
-  include AbstractDomain.WithBottom with type astate = t
+  val with_callsite : t -> CallSite.t -> t
-
-  val with_callsite : astate -> CallSite.t -> astate
   (** Push given callsite onto all traces in set. Cf [TraceElem.with_callsite] *)
 end
 

infer/src/concurrency/RacerD.ml

@@ -144,7 +144,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 
   let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc
-      (astate : Domain.astate) =
+      (astate : Domain.t) =
     (* create a dummy write that represents mutating the contents of the container *)
     let open Domain in
     let callee_accesses =
@@ -171,7 +171,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     Some {empty_summary with accesses= callee_accesses; return_ownership}
 
 
-  let get_summary caller_pdesc callee_pname actuals callee_loc tenv (astate : Domain.astate) =
+  let get_summary caller_pdesc callee_pname actuals callee_loc tenv (astate : Domain.t) =
     let open RacerDModels in
     let get_receiver_ap actuals =
       match List.hd actuals with
@@ -235,7 +235,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       AccessDomain.map expand_precondition accesses
 
 
-  let add_callee_accesses (caller_astate : Domain.astate) callee_accesses locks threads actuals
+  let add_callee_accesses (caller_astate : Domain.t) callee_accesses locks threads actuals
       callee_pname pdesc loc =
     let open Domain in
     let conjoin_ownership_precondition actual_exp actual_indexes :
@@ -356,8 +356,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     else astate
 
 
-  let exec_instr (astate : Domain.astate) ({ProcData.tenv; pdesc} as proc_data) _
+  let exec_instr (astate : Domain.t) ({ProcData.tenv; pdesc} as proc_data) _ (instr : HilInstr.t) =
-      (instr : HilInstr.t) =
     let open Domain in
     let open RacerDModels in
     let open ConcurrencyModels in
@@ -553,7 +552,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               (* non-boolean expression; can't evaluate it *)
               None
         in
-        let add_choice bool_value (acc : Domain.astate) = function
+        let add_choice bool_value (acc : Domain.t) = function
           | Choice.LockHeld ->
               let locks =
                 if bool_value then LocksDomain.acquire_lock acc.locks
@@ -916,7 +915,7 @@ let make_unprotected_write_description pname final_sink_site initial_sink_site f
 
 
 type reported_access =
-  { threads: RacerDDomain.ThreadsDomain.astate
+  { threads: RacerDDomain.ThreadsDomain.t
   ; snapshot: RacerDDomain.AccessSnapshot.t
   ; tenv: Tenv.t
   ; procdesc: Procdesc.t }

infer/src/concurrency/RacerDDomain.ml

@@ -204,7 +204,7 @@ module LocksDomain = struct
 end
 
 module ThreadsDomain = struct
-  type astate = NoThread | AnyThreadButSelf | AnyThread [@@deriving compare]
+  type t = NoThread | AnyThreadButSelf | AnyThread [@@deriving compare]
 
   let empty = NoThread
 
@@ -222,7 +222,7 @@ module ThreadsDomain = struct
     | AnyThread, _ ->
         false
     | _ ->
-        Int.equal 0 (compare_astate lhs rhs)
+        Int.equal 0 (compare lhs rhs)
 
 
   let join astate1 astate2 =
@@ -285,7 +285,7 @@ module AccessSnapshot = struct
 
   type t =
     { access: PathDomain.Sink.t
-    ; thread: ThreadsDomain.astate
+    ; thread: ThreadsDomain.t
     ; lock: bool
     ; ownership_precondition: OwnershipPrecondition.t }
   [@@deriving compare]
@@ -326,7 +326,7 @@ module AccessDomain = struct
 end
 
 module OwnershipAbstractValue = struct
-  type astate = Owned | OwnedIf of IntSet.t | Unowned [@@deriving compare]
+  type t = Owned | OwnedIf of IntSet.t | Unowned [@@deriving compare]
 
   let owned = Owned
 
@@ -521,12 +521,12 @@ module AttributeMapDomain = struct
     add lhs_access_path rhs_attributes attribute_map
 end
 
-type astate =
+type t =
-  { threads: ThreadsDomain.astate
+  { threads: ThreadsDomain.t
-  ; locks: LocksDomain.astate
+  ; locks: LocksDomain.t
-  ; accesses: AccessDomain.astate
+  ; accesses: AccessDomain.t
-  ; ownership: OwnershipDomain.astate
+  ; ownership: OwnershipDomain.t
-  ; attribute_map: AttributeMapDomain.astate }
+  ; attribute_map: AttributeMapDomain.t }
 
 let empty =
   let threads = ThreadsDomain.empty in
@@ -577,11 +577,11 @@ let widen ~prev ~next ~num_iters =
 
 
 type summary =
-  { threads: ThreadsDomain.astate
+  { threads: ThreadsDomain.t
-  ; locks: LocksDomain.astate
+  ; locks: LocksDomain.t
-  ; accesses: AccessDomain.astate
+  ; accesses: AccessDomain.t
-  ; return_ownership: OwnershipAbstractValue.astate
+  ; return_ownership: OwnershipAbstractValue.t
-  ; return_attributes: AttributeSetDomain.astate }
+  ; return_attributes: AttributeSetDomain.t }
 
 let empty_summary =
   { threads= ThreadsDomain.empty

infer/src/concurrency/RacerDDomain.mli

@@ -53,20 +53,20 @@ module PathDomain :
 module LocksDomain : sig
   include AbstractDomain.WithBottom
 
-  val acquire_lock : astate -> astate
+  val acquire_lock : t -> t
   (** record acquisition of a lock *)
 
-  val release_lock : astate -> astate
+  val release_lock : t -> t
   (** record release of a lock *)
 
-  val integrate_summary : caller_astate:astate -> callee_astate:astate -> astate
+  val integrate_summary : caller_astate:t -> callee_astate:t -> t
   (** integrate current state with a callee summary *)
 end
 
 (** Abstraction of threads that may run in parallel with the current thread.
     NoThread < AnyThreadExceptSelf < AnyThread *)
 module ThreadsDomain : sig
-  type astate =
+  type t =
     | NoThread
         (** No threads can run in parallel with the current thread (concretization: empty set). We
         assume this by default unless we see evidence to the contrary (annotations, use of locks,
@@ -78,14 +78,14 @@ module ThreadsDomain : sig
         (** Current thread can run in parallel with any thread, including itself (concretization:
             set of all TIDs ) *)
 
-  include AbstractDomain.WithBottom with type astate := astate
+  include AbstractDomain.WithBottom with type t := t
 
-  val can_conflict : astate -> astate -> bool
+  val can_conflict : t -> t -> bool
   (** return true if two accesses with these thread values can run concurrently *)
 
-  val is_any : astate -> bool
+  val is_any : t -> bool
 
-  val integrate_summary : caller_astate:astate -> callee_astate:astate -> astate
+  val integrate_summary : caller_astate:t -> callee_astate:t -> t
   (** integrate current state with a callee summary *)
 end
 
@@ -108,7 +108,7 @@ module AccessSnapshot : sig
 
   type t = private
     { access: PathDomain.Sink.t
-    ; thread: ThreadsDomain.astate
+    ; thread: ThreadsDomain.t
     ; lock: bool
     ; ownership_precondition: OwnershipPrecondition.t }
 
@@ -116,8 +116,8 @@ module AccessSnapshot : sig
 
   val make :
        PathDomain.Sink.t
-    -> LocksDomain.astate
+    -> LocksDomain.t
-    -> ThreadsDomain.astate
+    -> ThreadsDomain.t
     -> OwnershipPrecondition.t
     -> Procdesc.t
     -> t
@@ -135,34 +135,33 @@ 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
+  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 *)
     | Unowned  (** Unowned value; top of the lattice *)
   [@@deriving compare]
 
-  val owned : astate
+  val owned : t
 
-  val unowned : astate
+  val unowned : t
 
-  val make_owned_if : int -> astate
+  val make_owned_if : int -> t
 
-  include AbstractDomain.S with type astate := astate
+  include AbstractDomain.S with type t := t
 end
 
 module OwnershipDomain : sig
   include module type of AbstractDomain.Map (AccessPath) (OwnershipAbstractValue)
 
-  val get_owned : AccessPath.t -> astate -> OwnershipAbstractValue.astate
+  val get_owned : AccessPath.t -> t -> OwnershipAbstractValue.t
 
-  val is_owned : AccessPath.t -> astate -> bool
+  val is_owned : AccessPath.t -> t -> bool
 
   val find : [`Use_get_owned_instead] [@@warning "-32"]
 
-  val propagate_assignment : AccessPath.t -> HilExp.t -> astate -> astate
+  val propagate_assignment : AccessPath.t -> HilExp.t -> t -> t
 
-  val propagate_return :
+  val propagate_return : AccessPath.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t
-    AccessPath.t -> OwnershipAbstractValue.astate -> HilExp.t list -> astate -> astate
 end
 
 (** attribute attached to a boolean variable specifying what it means when the boolean is true *)
@@ -187,40 +186,40 @@ module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute
 module AttributeMapDomain : sig
   include module type of AbstractDomain.InvertedMap (AccessPath) (AttributeSetDomain)
 
-  val add : AccessPath.t -> AttributeSetDomain.astate -> astate -> astate
+  val add : AccessPath.t -> AttributeSetDomain.t -> t -> t
 
-  val has_attribute : AccessPath.t -> Attribute.t -> astate -> bool
+  val has_attribute : AccessPath.t -> Attribute.t -> t -> bool
 
-  val get_choices : AccessPath.t -> astate -> Choice.t list
+  val get_choices : AccessPath.t -> t -> Choice.t list
   (** get the choice attributes associated with the given access path *)
 
-  val add_attribute : AccessPath.t -> Attribute.t -> astate -> astate
+  val add_attribute : AccessPath.t -> Attribute.t -> t -> t
 
-  val propagate_assignment : AccessPath.t -> HilExp.t -> astate -> astate
+  val propagate_assignment : AccessPath.t -> HilExp.t -> t -> t
   (** propagate attributes from the leaves to the root of an RHS Hil expression *)
 end
 
-type astate =
+type t =
-  { threads: ThreadsDomain.astate  (** current thread: main, background, or unknown *)
+  { threads: ThreadsDomain.t  (** current thread: main, background, or unknown *)
-  ; locks: LocksDomain.astate  (** boolean that is true if a lock must currently be held *)
+  ; locks: LocksDomain.t  (** boolean that is true if a lock must currently be held *)
-  ; accesses: AccessDomain.astate
+  ; accesses: AccessDomain.t
         (** read and writes accesses performed without ownership permissions *)
-  ; ownership: OwnershipDomain.astate  (** map of access paths to ownership predicates *)
+  ; ownership: OwnershipDomain.t  (** map of access paths to ownership predicates *)
-  ; attribute_map: AttributeMapDomain.astate
+  ; attribute_map: AttributeMapDomain.t
         (** map of access paths to attributes such as owned, functional, ... *) }
 
 (** same as astate, but without [attribute_map] (since these involve locals) and with the addition
     of the ownership/attributes associated with the return value as well as the set of formals which
     may escape *)
 type summary =
-  { threads: ThreadsDomain.astate
+  { threads: ThreadsDomain.t
-  ; locks: LocksDomain.astate
+  ; locks: LocksDomain.t
-  ; accesses: AccessDomain.astate
+  ; accesses: AccessDomain.t
-  ; return_ownership: OwnershipAbstractValue.astate
+  ; return_ownership: OwnershipAbstractValue.t
-  ; return_attributes: AttributeSetDomain.astate }
+  ; return_attributes: AttributeSetDomain.t }
 
 val empty_summary : summary
 
-include AbstractDomain.WithBottom with type astate := astate
+include AbstractDomain.WithBottom with type t := t
 
 val pp_summary : F.formatter -> summary -> unit

infer/src/concurrency/classLoadsDomain.ml

@@ -37,6 +37,6 @@ let integrate_summary callee_pname loc astate callee_summary =
          add new_event astate |> union summary )
 
 
-type summary = astate
+type summary = t
 
 let pp_summary = pp

infer/src/concurrency/classLoadsDomain.mli

@@ -12,12 +12,10 @@ val get_java_class : Typ.Procname.t -> string option
 
 module Event : ExplicitTrace.TraceElem with type elem_t = ClassLoad.t
 
-include AbstractDomain.WithBottom
+include AbstractDomain.FiniteSetS with type elt = Event.t
 
-include PrettyPrintable.PPSet with type t = astate and type elt = Event.t
+type summary = t
-
-type summary = astate
 
 val pp_summary : F.formatter -> summary -> unit
 
-val integrate_summary : Typ.Procname.t -> Location.t -> astate -> summary -> astate
+val integrate_summary : Typ.Procname.t -> Location.t -> t -> summary -> t

infer/src/concurrency/starvation.ml

@@ -55,7 +55,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   type extras = FormalMap.t
 
-  let exec_instr (astate : Domain.astate) {ProcData.pdesc; tenv; extras} _ (instr : HilInstr.t) =
+  let exec_instr (astate : Domain.t) {ProcData.pdesc; tenv; extras} _ (instr : HilInstr.t) =
     let open ConcurrencyModels in
     let open StarvationModels in
     let get_lock_path = function

infer/src/concurrency/starvationDomain.ml

@@ -172,8 +172,6 @@ module UIThreadExplanationDomain = struct
     let pp = String.pp
   end)
 
-  type astate = t
-
   let join lhs rhs = if List.length lhs.trace <= List.length rhs.trace then lhs else rhs
 
   let widen ~prev ~next ~num_iters:_ = join prev next
@@ -200,11 +198,8 @@ module UIThreadDomain = struct
           (UIThreadExplanationDomain.with_callsite ui_explain callsite)
 end
 
-type astate =
+type t =
-  { lock_state: LockState.astate
+  {lock_state: LockState.t; events: EventDomain.t; order: OrderDomain.t; ui: UIThreadDomain.t}
-  ; events: EventDomain.astate
-  ; order: OrderDomain.astate
-  ; ui: UIThreadDomain.astate }
 
 let empty =
   { lock_state= LockState.empty
@@ -312,6 +307,6 @@ let set_on_ui_thread ({ui} as astate) loc explain =
   {astate with ui}
 
 
-type summary = astate
+type summary = t
 
 let pp_summary = pp

infer/src/concurrency/starvationDomain.mli

@@ -67,32 +67,29 @@ end
 
 module UIThreadDomain :
   AbstractDomain.WithBottom
-  with type astate = UIThreadExplanationDomain.t AbstractDomain.Types.bottom_lifted
+  with type t = UIThreadExplanationDomain.t AbstractDomain.Types.bottom_lifted
 
-type astate =
+type t =
-  { lock_state: LockState.astate
+  {lock_state: LockState.t; events: EventDomain.t; order: OrderDomain.t; ui: UIThreadDomain.t}
-  ; events: EventDomain.astate
-  ; order: OrderDomain.astate
-  ; ui: UIThreadDomain.astate }
 
-include AbstractDomain.WithBottom with type astate := astate
+include AbstractDomain.WithBottom with type t := t
 
-val acquire : astate -> Location.t -> Lock.t list -> astate
+val acquire : t -> Location.t -> Lock.t list -> t
 (** simultaneously acquire a number of locks, no-op if list is empty *)
 
-val release : astate -> Lock.t list -> astate
+val release : t -> Lock.t list -> t
 (** simultaneously release a number of locks, no-op if list is empty *)
 
-val blocking_call : Typ.Procname.t -> Event.severity_t -> Location.t -> astate -> astate
+val blocking_call : Typ.Procname.t -> Event.severity_t -> Location.t -> t -> t
 
-val strict_mode_call : Typ.Procname.t -> Location.t -> astate -> astate
+val strict_mode_call : Typ.Procname.t -> Location.t -> t -> t
 
-val set_on_ui_thread : astate -> Location.t -> string -> astate
+val set_on_ui_thread : t -> Location.t -> string -> t
 (** set the property "runs on UI thread" to true by attaching the given explanation string as to
     why this method is thought to do so *)
 
-type summary = astate
+type summary = t
 
 val pp_summary : F.formatter -> summary -> unit
 
-val integrate_summary : astate -> Typ.Procname.t -> Location.t -> summary -> astate
+val integrate_summary : t -> Typ.Procname.t -> Location.t -> summary -> t

infer/src/istd/PrettyPrintable.ml

@@ -10,18 +10,22 @@ module F = Format
 
 (** Wrappers for making pretty-printable modules *)
 
-module type PrintableEquatableType = sig
+module type PrintableType = sig
   type t
 
-  val equal : t -> t -> bool
-
   val pp : F.formatter -> t -> unit
 end
 
+module type PrintableEquatableType = sig
+  include PrintableType
+
+  val equal : t -> t -> bool
+end
+
 module type PrintableOrderedType = sig
   include Caml.Set.OrderedType
 
-  val pp : F.formatter -> t -> unit
+  include PrintableType with type t := t
 end
 
 module type PPSet = sig
@@ -29,9 +33,87 @@ module type PPSet = sig
 
   val is_singleton_or_more : t -> elt IContainer.singleton_or_more
 
+  include PrintableType with type t := t
+
   val pp_element : F.formatter -> elt -> unit
+end
 
-  val pp : F.formatter -> t -> unit
+module type MonoMap = sig
+  type key
+
+  type value
+
+  type t
+
+  val empty : t
+
+  val is_empty : t -> bool
+
+  val mem : key -> t -> bool
+
+  val add : key -> value -> t -> t
+
+  val update : key -> (value option -> value option) -> t -> t
+
+  val singleton : key -> value -> t
+
+  val remove : key -> t -> t
+
+  val merge : (key -> value option -> value option -> value option) -> t -> t -> t
+
+  val union : (key -> value -> value -> value option) -> t -> t -> t
+
+  val compare : (value -> value -> int) -> t -> t -> int
+
+  val equal : (value -> value -> bool) -> t -> t -> bool
+
+  val iter : (key -> value -> unit) -> t -> unit
+
+  val fold : (key -> value -> 'a -> 'a) -> t -> 'a -> 'a
+
+  val for_all : (key -> value -> bool) -> t -> bool
+
+  val exists : (key -> value -> bool) -> t -> bool
+
+  val filter : (key -> value -> bool) -> t -> t
+
+  val partition : (key -> value -> bool) -> t -> t * t
+
+  val cardinal : t -> int
+
+  val bindings : t -> (key * value) list
+
+  val min_binding : t -> key * value
+
+  val min_binding_opt : t -> (key * value) option
+
+  val max_binding : t -> key * value
+
+  val max_binding_opt : t -> (key * value) option
+
+  val choose : t -> key * value
+
+  val choose_opt : t -> (key * value) option
+
+  val split : key -> t -> t * value option * t
+
+  val find : key -> t -> value
+
+  val find_opt : key -> t -> value option
+
+  val find_first : (key -> bool) -> t -> key * value
+
+  val find_first_opt : (key -> bool) -> t -> (key * value) option
+
+  val find_last : (key -> bool) -> t -> key * value
+
+  val find_last_opt : (key -> bool) -> t -> (key * value) option
+
+  val map : (value -> value) -> t -> t
+
+  val mapi : (key -> value -> value) -> t -> t
+
+  val is_singleton_or_more : t -> (key * value) IContainer.singleton_or_more
 end
 
 module type PPMap = sig
@@ -79,3 +161,35 @@ module MakePPMap (Ord : PrintableOrderedType) = struct
     let pp_item fmt (k, v) = F.fprintf fmt "%a -> %a" Ord.pp k pp_value v in
     pp_collection ~pp_item fmt (bindings m)
 end
+
+module type PPMonoMap = sig
+  include MonoMap
+
+  include PrintableType with type t := t
+
+  val pp_key : F.formatter -> key -> unit
+end
+
+module MakePPMonoMap (Ord : PrintableOrderedType) (Val : PrintableType) = struct
+  module M = Caml.Map.Make (Ord)
+
+  include (M : module type of M with type 'a t := 'a M.t)
+
+  type t = Val.t M.t
+
+  type value = Val.t
+
+  let pp_key = Ord.pp
+
+  let pp fmt m =
+    let pp_item fmt (k, v) = F.fprintf fmt "%a -> %a" Ord.pp k Val.pp v in
+    pp_collection ~pp_item fmt (bindings m)
+
+
+  let is_singleton_or_more m =
+    if is_empty m then IContainer.Empty
+    else
+      let ((kmi, _) as binding) = min_binding m in
+      let kma, _ = max_binding m in
+      if phys_equal kmi kma then IContainer.Singleton binding else IContainer.More
+end

infer/src/istd/PrettyPrintable.mli

@@ -12,18 +12,22 @@ module F = Format
 
 val pp_collection : pp_item:(F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
 
-module type PrintableEquatableType = sig
+module type PrintableType = sig
   type t
 
-  val equal : t -> t -> bool
-
   val pp : F.formatter -> t -> unit
 end
 
+module type PrintableEquatableType = sig
+  include PrintableType
+
+  val equal : t -> t -> bool
+end
+
 module type PrintableOrderedType = sig
   include Caml.Set.OrderedType
 
-  val pp : F.formatter -> t -> unit
+  include PrintableType with type t := t
 end
 
 module type PPSet = sig
@@ -31,9 +35,87 @@ module type PPSet = sig
 
   val is_singleton_or_more : t -> elt IContainer.singleton_or_more
 
+  include PrintableType with type t := t
+
   val pp_element : F.formatter -> elt -> unit
+end
 
-  val pp : F.formatter -> t -> unit
+module type MonoMap = sig
+  type key
+
+  type value
+
+  type t
+
+  val empty : t
+
+  val is_empty : t -> bool
+
+  val mem : key -> t -> bool
+
+  val add : key -> value -> t -> t
+
+  val update : key -> (value option -> value option) -> t -> t
+
+  val singleton : key -> value -> t
+
+  val remove : key -> t -> t
+
+  val merge : (key -> value option -> value option -> value option) -> t -> t -> t
+
+  val union : (key -> value -> value -> value option) -> t -> t -> t
+
+  val compare : (value -> value -> int) -> t -> t -> int
+
+  val equal : (value -> value -> bool) -> t -> t -> bool
+
+  val iter : (key -> value -> unit) -> t -> unit
+
+  val fold : (key -> value -> 'a -> 'a) -> t -> 'a -> 'a
+
+  val for_all : (key -> value -> bool) -> t -> bool
+
+  val exists : (key -> value -> bool) -> t -> bool
+
+  val filter : (key -> value -> bool) -> t -> t
+
+  val partition : (key -> value -> bool) -> t -> t * t
+
+  val cardinal : t -> int
+
+  val bindings : t -> (key * value) list
+
+  val min_binding : t -> key * value
+
+  val min_binding_opt : t -> (key * value) option
+
+  val max_binding : t -> key * value
+
+  val max_binding_opt : t -> (key * value) option
+
+  val choose : t -> key * value
+
+  val choose_opt : t -> (key * value) option
+
+  val split : key -> t -> t * value option * t
+
+  val find : key -> t -> value
+
+  val find_opt : key -> t -> value option
+
+  val find_first : (key -> bool) -> t -> key * value
+
+  val find_first_opt : (key -> bool) -> t -> (key * value) option
+
+  val find_last : (key -> bool) -> t -> key * value
+
+  val find_last_opt : (key -> bool) -> t -> (key * value) option
+
+  val map : (value -> value) -> t -> t
+
+  val mapi : (key -> value -> value) -> t -> t
+
+  val is_singleton_or_more : t -> (key * value) IContainer.singleton_or_more
 end
 
 module type PPMap = sig
@@ -46,6 +128,17 @@ module type PPMap = sig
   val pp : pp_value:(F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit
 end
 
+module type PPMonoMap = sig
+  include MonoMap
+
+  include PrintableType with type t := t
+
+  val pp_key : F.formatter -> key -> unit
+end
+
 module MakePPSet (Ord : PrintableOrderedType) : PPSet with type elt = Ord.t
 
 module MakePPMap (Ord : PrintableOrderedType) : PPMap with type key = Ord.t
+
+module MakePPMonoMap (Ord : PrintableOrderedType) (Val : PrintableType) :
+  PPMonoMap with type key = Ord.t and type value = Val.t

infer/src/labs/ResourceLeakDomain.ml

@@ -10,11 +10,11 @@ module F = Format
 
 (* Extremely simple abstraction of resources: count the number of acquired resources. If there's
    not a corresponding number of releases, there may be a leak. *)
-type astate = int
+type t = int
 
 (* 2(a) *)
 (* For now, type of abstract state and summary are the same *)
-type summary = astate
+type summary = t
 
 (* 4(a) *)
 

infer/src/labs/ResourceLeaks.ml

@@ -12,7 +12,7 @@ module Domain = ResourceLeakDomain
 
 (* Boilerplate to write/read our summaries alongside the summaries of other analyzers *)
 module Payload = SummaryPayload.Make (struct
-  type t = Domain.astate
+  type t = Domain.t
 
   let update_payloads resources_payload (payloads : Payloads.t) =
     {payloads with resources= Some resources_payload}
@@ -30,7 +30,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   type nonrec extras = extras
 
   (* Take an abstract state and instruction, produce a new abstract state *)
-  let exec_instr (astate : Domain.astate) {ProcData.pdesc; tenv} _ (instr : HilInstr.t) =
+  let exec_instr (astate : Domain.t) {ProcData.pdesc; tenv} _ (instr : HilInstr.t) =
     let is_closeable procname tenv =
       match procname with
       | Typ.Procname.Java java_procname ->
@@ -109,7 +109,7 @@ let checker {Callbacks.summary; proc_desc; tenv} : Summary.t =
       Reporting.log_error summary ~loc:last_loc IssueType.resource_leak message
   in
   (* Convert the abstract state to a summary. for now, just the identity function *)
-  let convert_to_summary (post : Domain.astate) : Domain.summary =
+  let convert_to_summary (post : Domain.t) : Domain.summary =
     (* 4(a) *)
     post
   in

infer/src/quandary/TaintAnalysis.ml

@@ -444,8 +444,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       TaintDomain.trace_fold add_to_caller_tree summary caller_access_tree
 
 
-    let exec_instr (astate : Domain.astate) (proc_data : extras ProcData.t) _ (instr : HilInstr.t)
+    let exec_instr (astate : Domain.t) (proc_data : extras ProcData.t) _ (instr : HilInstr.t) =
-        =
       (* not all sinks are function calls; we might want to treat an array or field access as a
          sink too. do this by pretending an access is a call to a dummy function and using the
          existing machinery for adding function call sinks *)

infer/src/unit/abstractInterpreterTests.ml

@@ -13,7 +13,7 @@ module F = Format
     you'll diverge at loops if you don't widen *)
 
 module PathCountDomain = struct
-  type astate = PathCount of int | Top
+  type t = PathCount of int | Top
 
   let make_path_count c =
     (* guarding against overflow *)