diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/abstractDomain.ml index fc9291b7e..c0c9b50e8 100644 --- a/infer/src/checkers/abstractDomain.ml +++ b/infer/src/checkers/abstractDomain.ml @@ -9,7 +9,7 @@ module F = Format -module type AbstractDomain = sig +module type S = sig type astate val initial : astate @@ -18,45 +18,43 @@ module type AbstractDomain = sig val join : astate -> astate -> astate val widen : prev:astate -> next:astate -> num_iters:int -> astate val pp : F.formatter -> astate -> unit - end -module BottomLiftedAbstractDomain (A : AbstractDomain) : AbstractDomain = struct +module BottomLifted (Domain : S) = struct type astate = | Bottom - | NonBottom of A.astate + | NonBottom of Domain.astate let is_bottom astate = astate = Bottom - let initial = NonBottom A.initial + let initial = NonBottom Domain.initial let (<=) ~lhs ~rhs = match lhs, rhs with | Bottom, _ -> true | _ , Bottom -> false - | NonBottom lhs, NonBottom rhs -> A.(<=) ~lhs ~rhs + | NonBottom lhs, NonBottom rhs -> Domain.(<=) ~lhs ~rhs let join astate1 astate2 = match astate1, astate2 with | Bottom, _ -> astate2 | _, Bottom -> astate1 - | NonBottom a1, NonBottom a2 -> NonBottom (A.join a1 a2) + | NonBottom a1, NonBottom a2 -> NonBottom (Domain.join a1 a2) let widen ~prev ~next ~num_iters = match prev, next with | Bottom, _ -> next | _, Bottom -> prev - | NonBottom prev, NonBottom next -> NonBottom (A.widen ~prev ~next ~num_iters) + | NonBottom prev, NonBottom next -> NonBottom (Domain.widen ~prev ~next ~num_iters) let pp fmt = function | Bottom -> F.fprintf fmt "_|_" - | NonBottom astate -> A.pp fmt astate - + | NonBottom astate -> Domain.pp fmt astate end (* lift a set to a domain. the elements of the set should be drawn from a *finite* collection of possible values, since the widening operator here is just union. *) -module FiniteSetDomain (S : PrettyPrintable.PPSet) = struct +module FiniteSet (S : PrettyPrintable.PPSet) = struct include S type astate = t @@ -65,5 +63,4 @@ module FiniteSetDomain (S : PrettyPrintable.PPSet) = struct let (<=) ~lhs ~rhs = subset lhs rhs let join = union let widen ~prev ~next ~num_iters:_ = union prev next - end diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index 528311fc5..cad0305a0 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -9,14 +9,11 @@ module L = Logging -open AbstractDomain -open TransferFunctions - module Make (C : ProcCfg.Wrapper) (Sched : Scheduler.S) - (A : AbstractDomain) - (T : TransferFunctions with type astate = A.astate) = struct + (A : AbstractDomain.S) + (T : TransferFunctions.S with type astate = A.astate) = struct module S = Sched (C) module M = ProcCfg.NodeIdMap (C) diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 3c094b732..30dfc398a 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -13,7 +13,7 @@ module PvarSet = PrettyPrintable.MakePPSet(struct let pp_element = (Pvar.pp pe_text) end) -module Domain = AbstractDomain.FiniteSetDomain(PvarSet) +module Domain = AbstractDomain.FiniteSet(PvarSet) module TransferFunctions = struct type astate = Domain.astate diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index c6f20786e..d65907845 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -18,7 +18,7 @@ module VarSet = PrettyPrintable.MakePPSet(struct let pp_element = CopyPropagation.pp_var end) -module Domain = AbstractDomain.FiniteSetDomain(VarSet) +module Domain = AbstractDomain.FiniteSet(VarSet) (* compilers 101-style backward transfer functions for liveness analysis. gen a variable when it is read, kill the variable when it is assigned *) diff --git a/infer/src/checkers/transferFunctions.ml b/infer/src/checkers/transferFunctions.ml index dadf57318..c22021b62 100644 --- a/infer/src/checkers/transferFunctions.ml +++ b/infer/src/checkers/transferFunctions.ml @@ -8,7 +8,7 @@ *) -module type TransferFunctions = sig +module type S = sig type astate (* {A} instr {A'}. [caller_pdesc] is the procdesc of the current procedure *) diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 6db3e3e3d..26d0f9363 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -10,9 +10,6 @@ module F = Format module L = Logging -open AbstractDomain -open TransferFunctions - (** utilities for writing abstract domains/transfer function tests *) (** structured language that makes it easy to write small test programs in OCaml *) @@ -126,8 +123,8 @@ end module Make (C : ProcCfg.Wrapper with type node = Cfg.Node.t) (S : Scheduler.S) - (A : AbstractDomain) - (T : TransferFunctions with type astate = A.astate) = struct + (A : AbstractDomain.S) + (T : TransferFunctions.S with type astate = A.astate) = struct open StructuredSil