From 6aba4b7ca2974be84653e905cf17dd6c9d9a5e5e Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Mon, 26 Nov 2018 02:50:09 -0800 Subject: [PATCH] [AI] kill astate type Reviewed By: mbouaziz Differential Revision: D10119192 fbshipit-source-id: 4868cbcb1 --- infer/src/absint/AbstractDomain.ml | 92 +++++++------ infer/src/absint/AbstractDomain.mli | 128 +++++++++--------- infer/src/absint/AbstractInterpreter.ml | 14 +- infer/src/absint/AbstractInterpreter.mli | 12 +- infer/src/absint/LowerHil.mli | 6 +- infer/src/absint/TransferFunctions.ml | 2 +- infer/src/absint/TransferFunctions.mli | 2 +- infer/src/backend/Differential.ml | 2 +- infer/src/backend/Payloads.ml | 6 +- infer/src/backend/Payloads.mli | 6 +- infer/src/bufferoverrun/arrayBlk.ml | 54 ++++---- .../src/bufferoverrun/bufferOverrunChecker.ml | 25 ++-- .../src/bufferoverrun/bufferOverrunDomain.ml | 122 +++++++---------- .../bufferOverrunDomainRelation.ml | 103 +++++++------- .../src/bufferoverrun/bufferOverrunModels.ml | 12 +- .../bufferOverrunProofObligations.ml | 18 +-- .../bufferOverrunProofObligations.mli | 16 +-- .../bufferoverrun/bufferOverrunSemantics.ml | 36 ++--- infer/src/bufferoverrun/bufferOverrunUtils.ml | 28 ++-- .../src/bufferoverrun/bufferOverrunUtils.mli | 47 ++++--- infer/src/bufferoverrun/itv.ml | 22 ++- infer/src/bufferoverrun/itv.mli | 8 +- infer/src/bufferoverrun/polynomials.ml | 2 - infer/src/bufferoverrun/polynomials.mli | 34 ++--- infer/src/checkers/IdAccessPathMapDomain.ml | 6 +- infer/src/checkers/IdAccessPathMapDomain.mli | 8 +- infer/src/checkers/Litho.ml | 6 +- infer/src/checkers/LithoDomain.mli | 6 +- infer/src/checkers/NullabilityCheck.ml | 4 +- infer/src/checkers/NullabilitySuggest.ml | 10 +- infer/src/checkers/Ownership.ml | 8 +- infer/src/checkers/PulseDomain.ml | 8 +- infer/src/checkers/PulseDomain.mli | 4 +- infer/src/checkers/SimpleChecker.ml | 15 +- infer/src/checkers/SimpleChecker.mli | 11 +- infer/src/checkers/Siof.ml | 2 +- infer/src/checkers/Trace.ml | 16 +-- infer/src/checkers/Trace.mli | 10 +- infer/src/checkers/accessPathDomains.ml | 2 +- infer/src/checkers/accessPathDomains.mli | 10 +- infer/src/checkers/accessTree.ml | 26 ++-- infer/src/checkers/accessTree.mli | 21 ++- infer/src/checkers/annotationReachability.ml | 6 +- infer/src/checkers/cost.ml | 20 +-- infer/src/checkers/cost.mli | 6 +- infer/src/checkers/costDomain.ml | 2 +- infer/src/checkers/purity.ml | 2 +- infer/src/checkers/purityDomain.ml | 2 +- infer/src/checkers/uninit.ml | 5 +- infer/src/checkers/uninitDomain.ml | 5 +- infer/src/concurrency/ExplicitTrace.ml | 6 +- infer/src/concurrency/ExplicitTrace.mli | 6 +- infer/src/concurrency/RacerD.ml | 13 +- infer/src/concurrency/RacerDDomain.ml | 30 ++-- infer/src/concurrency/RacerDDomain.mli | 75 +++++----- infer/src/concurrency/classLoadsDomain.ml | 2 +- infer/src/concurrency/classLoadsDomain.mli | 8 +- infer/src/concurrency/starvation.ml | 2 +- infer/src/concurrency/starvationDomain.ml | 11 +- infer/src/concurrency/starvationDomain.mli | 25 ++-- infer/src/istd/PrettyPrintable.ml | 124 ++++++++++++++++- infer/src/istd/PrettyPrintable.mli | 103 +++++++++++++- infer/src/labs/ResourceLeakDomain.ml | 4 +- infer/src/labs/ResourceLeaks.ml | 6 +- infer/src/quandary/TaintAnalysis.ml | 3 +- infer/src/unit/abstractInterpreterTests.ml | 2 +- 66 files changed, 781 insertions(+), 657 deletions(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 435538475..f040995e9 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/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:astate -> next:astate -> num_iters:int -> astate - - val pp : F.formatter -> astate -> unit + val widen : prev:t -> next:t -> num_iters:int -> t end -module Empty : S with type astate = unit = struct - type astate = unit +module Empty : S with type t = unit = struct + 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) = - MapOfPPMap (PrettyPrintable.MakePPMap (Key)) (ValueDomain) - -module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = struct +module Map (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 diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index b68cc5d38..c68d58e62 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/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 pp : F.formatter -> astate -> unit + val widen : prev:t -> next:t -> num_iters:int -> t 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 - type astate = Domain.astate bottom_lifted +module BottomLifted (Domain : S) : WithBottom with type t = Domain.t bottom_lifted - include WithBottom with type astate := astate -end +(* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) -(** 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 - type astate = Domain.astate top_lifted - - include WithTop with type astate := astate - end + (** Create a domain with Top element from a pre-domain *) + module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted 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 - a *finite* collection of possible values, since the widening operator here is just union. *) -module FiniteSetOfPPSet (PPSet : PrettyPrintable.PPSet) : sig - include module type of PPSet with type elt = PPSet.elt +module type FiniteSetS = sig + include PrettyPrintable.PPSet - 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 - include module type of PrettyPrintable.MakePPSet (Element) +module FiniteSet (Element : PrettyPrintable.PrintableOrderedType) : + 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 - include module type of PrettyPrintable.MakePPSet (Element) +module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) : + 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 - include module type of PPMap with type key = PPMap.key - - include WithBottom with type astate = ValueDomain.astate t -end +module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) : + MapS with type key = PPMap.key and type value = ValueDomain.t (** 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 - include module type of PrettyPrintable.MakePPMap (Key) +module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) : + MapS with type key = Key.t and type value = ValueDomain.t + +module type InvertedMapS = sig + include PrettyPrintable.PPMonoMap - include WithBottom with type astate = ValueDomain.astate t + 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 - include module type of PrettyPrintable.MakePPMap (Key) +module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) : + InvertedMapS with type key = Key.t and type value = ValueDomain.t - include S with type astate = ValueDomain.astate t -end +(* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) -(** 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 diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 3304319ec..715632145 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/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 - -> TransferFunctions.Domain.astate option + -> initial:TransferFunctions.Domain.t + -> 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 diff --git a/infer/src/absint/AbstractInterpreter.mli b/infer/src/absint/AbstractInterpreter.mli index 607ddf5a9..42dc68364 100644 --- a/infer/src/absint/AbstractInterpreter.mli +++ b/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 - -> TransferFunctions.Domain.astate option + -> initial:TransferFunctions.Domain.t + -> 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] *) diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index abb9eb352..a37a974b3 100644 --- a/infer/src/absint/LowerHil.mli +++ b/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 - -> MakeTransferFunctions(CFG).Domain.astate option + -> initial:MakeTransferFunctions(CFG).Domain.t + -> 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 diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 4c974e38a..875d0911a 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/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 diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 2d54136dc..3c43a61bb 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/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 diff --git a/infer/src/backend/Differential.ml b/infer/src/backend/Differential.ml index 24a840d0f..431c872e7 100644 --- a/infer/src/backend/Differential.ml +++ b/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) ; diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 331b9d675..46a8bcbcc 100644 --- a/infer/src/backend/Payloads.ml +++ b/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 } diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index 44f0497ee..745c8343e 100644 --- a/infer/src/backend/Payloads.mli +++ b/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 } diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 37b8e18f7..325c51506 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/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 = - fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr - +let plus_offset : t -> Itv.t -> t = 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 = - fun c a1 a2 -> do_prune (ArrInfo.prune_comp c) a1 a2 - +let prune_comp : Binop.t -> t -> t -> t = 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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index a5b2edea8..7ed9c57d5 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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.astate = + -> Dom.Mem.t + -> 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) "@[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 -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index d1905fd9a..6509c48cd 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -17,18 +17,16 @@ module Trace = BufferOverrunTrace module TraceSet = Trace.Set module Val = struct - type astate = - { itv: Itv.astate - ; sym: Relation.Sym.astate - ; powloc: PowLoc.astate - ; arrayblk: ArrayBlk.astate - ; offset_sym: Relation.Sym.astate - ; size_sym: Relation.Sym.astate + type t = + { itv: Itv.t + ; sym: Relation.Sym.t + ; powloc: PowLoc.t + ; arrayblk: ArrayBlk.t + ; offset_sym: Relation.Sym.t + ; 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) - -> (ArrayBlk.astate -> ArrayBlk.astate -> ArrayBlk.astate) - -> t - -> t - -> t = + (Itv.t -> Itv.t -> Itv.t) -> (ArrayBlk.t -> ArrayBlk.t -> ArrayBlk.t) -> 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 = - fun l m -> filter (fun _ y -> not (AliasTarget.use l y)) m + let store : Loc.t -> t -> t = fun l m -> filter (fun _ y -> not (AliasTarget.use l y)) m - - let find : Ident.t -> astate -> AliasTarget.astate option = find_opt + let find : Ident.t -> t -> AliasTarget.t 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 lift_map : (AliasMap.astate -> AliasMap.astate) -> astate -> astate = - fun f a -> {a with map= f a.map} - + let bot : t = {map= AliasMap.empty; ret= AliasRet.empty} - 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 = - fun id loc -> lift_map (AliasMap.load id loc) + let find_ret : t -> AliasTarget.t option = fun x -> AliasRet.get x.ret + 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 = - | Latest of PrunePairs.astate - | TrueBranch of Pvar.t * PrunePairs.astate - | FalseBranch of Pvar.t * PrunePairs.astate - | V of Pvar.t * PrunePairs.astate * PrunePairs.astate + type t = + | Latest of PrunePairs.t + | TrueBranch of Pvar.t * PrunePairs.t + | FalseBranch of Pvar.t * PrunePairs.t + | 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 = - { stack_locs: StackLocs.astate - ; mem_pure: MemPure.astate - ; alias: Alias.astate - ; latest_prune: LatestPrune.astate - ; relation: Relation.astate } - - type t = astate + type t = + { stack_locs: StackLocs.t + ; mem_pure: MemPure.t + ; alias: Alias.t + ; latest_prune: LatestPrune.t + ; relation: Relation.t } 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 diff --git a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml index a2cd94287..3922d5b6f 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml +++ b/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_offset_sym_f:(Exp.t -> Sym.astate) - -> get_size_sym_f:(Exp.t -> Sym.astate) + get_int_sym_f:(Exp.t -> Sym.t) + -> get_offset_sym_f:(Exp.t -> Sym.t) + -> 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 : - PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> astate -> astate + val store_relation : PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> t -> t - 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 = astate [@@deriving compare] - - let compare_astate _ _ = 0 + type t = unit [@@deriving compare] 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 : - PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> astate -> astate = + let store_relation : PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> t -> t = 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 diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index ebdae84b1..d080b97c4 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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.astate * int + -> Dom.Mem.t + -> 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.astate + -> Dom.Mem.t + -> Dom.Mem.t type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun} diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index aee51d1a9..21cdeeaeb 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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 - ; idx: ItvPure.astate - ; size: ItvPure.astate + { offset: ItvPure.t + ; idx: ItvPure.t + ; 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 - ; rhs: ItvPure.astate } + ; lhs: ItvPure.t + ; rhs: ItvPure.t } let get_symbols c = Symb.SymbolSet.union (ItvPure.get_symbols c.lhs) (ItvPure.get_symbols c.rhs) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 520f1e8fd..49de0edea 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -35,26 +35,26 @@ module ConditionSet : sig val add_array_access : Location.t - -> offset:ItvPure.astate - -> idx:ItvPure.astate - -> size:ItvPure.astate + -> offset:ItvPure.t + -> idx:ItvPure.t + -> 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 - -> rhs:ItvPure.astate + -> lhs:ItvPure.t + -> 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 diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index bd26fcbe9..fc347b607 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/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.astate + -> Mem.t + -> 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.astate + -> Mem.t + -> 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 = diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 9eceb223d..3ef02f293 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/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.astate * int + -> Dom.Mem.t + -> 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.astate * int = + -> Dom.Mem.t + -> 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.astate * int = + -> Dom.Mem.t + -> 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.astate + -> Dom.Mem.t + -> 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.astate = + -> Dom.Mem.t + -> 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.astate = + -> Dom.Mem.t + -> 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.astate = + -> Dom.Mem.t + -> 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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 2e997cd99..d1502ea6b 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/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.astate * int + -> Dom.Mem.t + -> 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.astate * int + -> Dom.Mem.t + -> 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.astate * int + -> Dom.Mem.t + -> 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.astate + -> Dom.Mem.t + -> 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.astate + -> Dom.Mem.t + -> 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.astate + -> Dom.Mem.t + -> 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.astate + -> Dom.Mem.t + -> 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.astate + -> Dom.Mem.t + -> Dom.Mem.t - val set_dyn_length : - Location.t -> Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.astate -> Dom.Mem.astate + val set_dyn_length : Location.t -> Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.t -> Dom.Mem.t 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 diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index c3b62d238..2207da1b0 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/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 = astate + type t = Bound.t * Bound.t [@@deriving compare] 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 diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index e6d2f3f13..26e7f0276 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/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 = astate + type t [@@deriving compare] 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 (** _|_ *) diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index bd7d206a2..9b73399a4 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/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 diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli index d988c6752..d86a952b1 100644 --- a/infer/src/bufferoverrun/polynomials.mli +++ b/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 diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index e5c7b15e1..48435ef92 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/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 diff --git a/infer/src/checkers/IdAccessPathMapDomain.mli b/infer/src/checkers/IdAccessPathMapDomain.mli index 38dab719d..0ad101f1e 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.mli +++ b/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 - -type astate = AccessExpression.t IdMap.t - -include module type of IdMap - -include AbstractDomain.WithBottom with type astate := astate +include AbstractDomain.MapS with type key = Var.t and type value = AccessExpression.t diff --git a/infer/src/checkers/Litho.ml b/infer/src/checkers/Litho.ml index 2e22f3dac..a1d931748 100644 --- a/infer/src/checkers/Litho.ml +++ b/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 diff --git a/infer/src/checkers/LithoDomain.mli b/infer/src/checkers/LithoDomain.mli index 338a8ba85..007a2bb63 100644 --- a/infer/src/checkers/LithoDomain.mli +++ b/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 -(** Apply [f] to each maximal call chain encoded in [astate] *) +val iter_call_chains : f:(AccessPath.t -> Typ.Procname.t list -> unit) -> t -> unit +(** Apply [f] to each maximal call chain encoded in [t] *) diff --git a/infer/src/checkers/NullabilityCheck.ml b/infer/src/checkers/NullabilityCheck.ml index 4dc1e042a..65dd18c78 100644 --- a/infer/src/checkers/NullabilityCheck.ml +++ b/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 diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index e55b3d8da..30d11c18d 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/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 diff --git a/infer/src/checkers/Ownership.ml b/infer/src/checkers/Ownership.ml index c5225dee5..209e7df76 100644 --- a/infer/src/checkers/Ownership.ml +++ b/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 -> diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 384a6e7da..21206de83 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/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 - type astate = t +module Domain : AbstractDomain.S with type t = astate = struct + type t = astate let piecewise_lessthan lhs rhs = Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 45eccf7e3..246f9e8f6 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -15,9 +15,7 @@ module AbstractAddress : sig val init : unit -> unit end -type t - -include AbstractDomain.S with type astate = t +include AbstractDomain.S val initial : t diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml index 893f6c605..088966c09 100644 --- a/infer/src/checkers/SimpleChecker.ml +++ b/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 : - astate -> Sil.instr -> Procdesc.Node.nodekind -> Typ.Procname.t -> Tenv.t -> astate + val exec_instr : t -> Sil.instr -> Procdesc.Node.nodekind -> Typ.Procname.t -> Tenv.t -> t (** 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 diff --git a/infer/src/checkers/SimpleChecker.mli b/infer/src/checkers/SimpleChecker.mli index e48aba280..df6e4f4f9 100644 --- a/infer/src/checkers/SimpleChecker.mli +++ b/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 : - astate -> Sil.instr -> Procdesc.Node.nodekind -> Typ.Procname.t -> Tenv.t -> astate + val exec_instr : t -> Sil.instr -> Procdesc.Node.nodekind -> Typ.Procname.t -> Tenv.t -> t - 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 diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index 9d8858767..8c97f451f 100644 --- a/infer/src/checkers/Siof.ml +++ b/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} diff --git a/infer/src/checkers/Trace.ml b/infer/src/checkers/Trace.ml index d981aa159..89119a2ca 100644 --- a/infer/src/checkers/Trace.ml +++ b/infer/src/checkers/Trace.ml @@ -21,11 +21,7 @@ end module type S = sig include Spec - type t - - type astate = t - - include AbstractDomain.WithBottom with type astate := astate + include AbstractDomain.WithBottom 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 = astate + type t = {known: Known.t; footprint: Footprint.t; sanitizers: Sanitizers.t} 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 = astate + type t = {known: Known.t; footprint: Footprint.t; sanitizers: Sanitizers.t} 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 = diff --git a/infer/src/checkers/Trace.mli b/infer/src/checkers/Trace.mli index 6289e7222..e864c172f 100644 --- a/infer/src/checkers/Trace.mli +++ b/infer/src/checkers/Trace.mli @@ -23,11 +23,7 @@ end module type S = sig include Spec - type t - - type astate = t - - include AbstractDomain.WithBottom with type astate := astate + include AbstractDomain.WithBottom 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 = astate + type t = {known: Known.t; footprint: Footprint.t; sanitizers: Sanitizers.t} val empty : t diff --git a/infer/src/checkers/accessPathDomains.ml b/infer/src/checkers/accessPathDomains.ml index d03b204ca..bcbecd215 100644 --- a/infer/src/checkers/accessPathDomains.ml +++ b/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 diff --git a/infer/src/checkers/accessPathDomains.mli b/infer/src/checkers/accessPathDomains.mli index 2a03145b2..1d14e477f 100644 --- a/infer/src/checkers/accessPathDomains.mli +++ b/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 *) diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index 9462d60d5..967100226 100644 --- a/infer/src/checkers/accessTree.ml +++ b/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 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 - 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_ diff --git a/infer/src/checkers/accessTree.mli b/infer/src/checkers/accessTree.mli index b8043f496..a50c88260 100644 --- a/infer/src/checkers/accessTree.mli +++ b/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 diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index fb572b09a..66ccebbf1 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/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 diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 99e0fecad..1512aaf69 100644 --- a/infer/src/checkers/cost.ml +++ b/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) - instr : CostDomain.NodeInstructionToCostMap.astate = + (astate : CostDomain.NodeInstructionToCostMap.t) {ProcData.pdesc} (node : CFG.Node.t) instr : + 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) - -> of_item:(Item.t -> BasicCost.astate) + on_improve:(Sum.t -> BasicCost.t -> BasicCost.t -> unit) + -> 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 - : Domain.astate = + let exec_instr ((_, reported_so_far) : Domain.t) {ProcData.extras} (node : CFG.Node.t) instr : + 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 diff --git a/infer/src/checkers/cost.mli b/infer/src/checkers/cost.mli index bcf39764f..0d0dc3bdd 100644 --- a/infer/src/checkers/cost.mli +++ b/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 - -> CostDomain.BasicCost.astate + -> callee_cost:CostDomain.BasicCost.t + -> CostDomain.BasicCost.t diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml index 9b21f1b2f..e258ef8b5 100644 --- a/infer/src/checkers/costDomain.ml +++ b/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 diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index f8193ef1d..fdc3cd31d 100644 --- a/infer/src/checkers/purity.ml +++ b/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 -> diff --git a/infer/src/checkers/purityDomain.ml b/infer/src/checkers/purityDomain.ml index 43ca3473b..4c768759d 100644 --- a/infer/src/checkers/purityDomain.ml +++ b/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 diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index 6006e4829..ef085c70e 100644 --- a/infer/src/checkers/uninit.ml +++ b/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 diff --git a/infer/src/checkers/uninitDomain.ml b/infer/src/checkers/uninitDomain.ml index f31de59eb..435649494 100644 --- a/infer/src/checkers/uninitDomain.ml +++ b/infer/src/checkers/uninitDomain.ml @@ -94,10 +94,7 @@ module Record (Domain2 : AbstractDomain.S) (Domain3 : AbstractDomain.S) = struct - type astate = - { maybe_uninit_vars: Domain1.astate - ; aliased_vars: Domain2.astate - ; prepost: Domain3.astate prepost } + type t = {maybe_uninit_vars: Domain1.t; aliased_vars: Domain2.t; prepost: Domain3.t prepost} let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true diff --git a/infer/src/concurrency/ExplicitTrace.ml b/infer/src/concurrency/ExplicitTrace.ml index f6254adaf..1fac42dae 100644 --- a/infer/src/concurrency/ExplicitTrace.ml +++ b/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 : astate -> CallSite.t -> astate + val with_callsite : t -> CallSite.t -> t end module type TraceElem = sig diff --git a/infer/src/concurrency/ExplicitTrace.mli b/infer/src/concurrency/ExplicitTrace.mli index 941291c42..bb56be4df 100644 --- a/infer/src/concurrency/ExplicitTrace.mli +++ b/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 : astate -> CallSite.t -> astate + val with_callsite : t -> CallSite.t -> t (** Push given callsite onto all traces in set. Cf [TraceElem.with_callsite] *) end diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 47abe21fa..cf20d3c00 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/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) _ - (instr : HilInstr.t) = + let exec_instr (astate : Domain.t) ({ProcData.tenv; pdesc} as proc_data) _ (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 } diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 3f7166053..1828e1abf 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/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 = - { threads: ThreadsDomain.astate - ; locks: LocksDomain.astate - ; accesses: AccessDomain.astate - ; ownership: OwnershipDomain.astate - ; attribute_map: AttributeMapDomain.astate } +type t = + { threads: ThreadsDomain.t + ; locks: LocksDomain.t + ; accesses: AccessDomain.t + ; ownership: OwnershipDomain.t + ; 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 - ; locks: LocksDomain.astate - ; accesses: AccessDomain.astate - ; return_ownership: OwnershipAbstractValue.astate - ; return_attributes: AttributeSetDomain.astate } + { threads: ThreadsDomain.t + ; locks: LocksDomain.t + ; accesses: AccessDomain.t + ; return_ownership: OwnershipAbstractValue.t + ; return_attributes: AttributeSetDomain.t } let empty_summary = { threads= ThreadsDomain.empty diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 69a3f0097..d1500fe7d 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/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 - -> ThreadsDomain.astate + -> LocksDomain.t + -> 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 : - AccessPath.t -> OwnershipAbstractValue.astate -> HilExp.t list -> astate -> astate + val propagate_return : AccessPath.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t 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 = - { threads: ThreadsDomain.astate (** current thread: main, background, or unknown *) - ; locks: LocksDomain.astate (** boolean that is true if a lock must currently be held *) - ; accesses: AccessDomain.astate +type t = + { threads: ThreadsDomain.t (** current thread: main, background, or unknown *) + ; locks: LocksDomain.t (** boolean that is true if a lock must currently be held *) + ; accesses: AccessDomain.t (** read and writes accesses performed without ownership permissions *) - ; ownership: OwnershipDomain.astate (** map of access paths to ownership predicates *) - ; attribute_map: AttributeMapDomain.astate + ; ownership: OwnershipDomain.t (** map of access paths to ownership predicates *) + ; 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 - ; locks: LocksDomain.astate - ; accesses: AccessDomain.astate - ; return_ownership: OwnershipAbstractValue.astate - ; return_attributes: AttributeSetDomain.astate } + { threads: ThreadsDomain.t + ; locks: LocksDomain.t + ; accesses: AccessDomain.t + ; return_ownership: OwnershipAbstractValue.t + ; 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 diff --git a/infer/src/concurrency/classLoadsDomain.ml b/infer/src/concurrency/classLoadsDomain.ml index da121dfe7..39b86f617 100644 --- a/infer/src/concurrency/classLoadsDomain.ml +++ b/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 diff --git a/infer/src/concurrency/classLoadsDomain.mli b/infer/src/concurrency/classLoadsDomain.mli index b8c7995aa..52f1baaeb 100644 --- a/infer/src/concurrency/classLoadsDomain.mli +++ b/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 = astate +type summary = t 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 diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index a0dad6e6d..690789c2d 100644 --- a/infer/src/concurrency/starvation.ml +++ b/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 diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 1d797a821..a0d771c4e 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/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 = - { lock_state: LockState.astate - ; events: EventDomain.astate - ; order: OrderDomain.astate - ; ui: UIThreadDomain.astate } +type t = + {lock_state: LockState.t; events: EventDomain.t; order: OrderDomain.t; ui: UIThreadDomain.t} 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 diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 74d7a5b22..745efe2a7 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/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 = - { lock_state: LockState.astate - ; events: EventDomain.astate - ; order: OrderDomain.astate - ; ui: UIThreadDomain.astate } +type t = + {lock_state: LockState.t; events: EventDomain.t; order: OrderDomain.t; ui: UIThreadDomain.t} -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 diff --git a/infer/src/istd/PrettyPrintable.ml b/infer/src/istd/PrettyPrintable.ml index eeb76ad0b..48e08c5fb 100644 --- a/infer/src/istd/PrettyPrintable.ml +++ b/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 diff --git a/infer/src/istd/PrettyPrintable.mli b/infer/src/istd/PrettyPrintable.mli index a021794e5..941cf1396 100644 --- a/infer/src/istd/PrettyPrintable.mli +++ b/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 diff --git a/infer/src/labs/ResourceLeakDomain.ml b/infer/src/labs/ResourceLeakDomain.ml index fc9d3fb3c..4226b1c9e 100644 --- a/infer/src/labs/ResourceLeakDomain.ml +++ b/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) *) diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index 8b2af7c53..fa1cc745a 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/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 diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 245b8626f..db6945c75 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/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 *) diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index 56c4f40b2..15857e420 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/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 *)