diff --git a/infer/src/checkers/AbstractDomain.mli b/infer/src/checkers/AbstractDomain.mli new file mode 100644 index 000000000..b7e8bc2a8 --- /dev/null +++ b/infer/src/checkers/AbstractDomain.mli @@ -0,0 +1,49 @@ +(* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! Utils + +module F = Format + +(** Abstract domains and domain combinators *) + +module type S = sig + type astate + + val initial : astate + val (<=) : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *) + val join : astate -> astate -> astate + val widen : prev:astate -> next:astate -> num_iters:int -> astate + val pp : F.formatter -> astate -> unit +end + +(** Lift a pre-domain to a domain *) +module BottomLifted (Domain : S) : sig + type astate = + | Bottom + | NonBottom of Domain.astate + + include S with type astate := astate +end + +(** Cartesian product of two domains. *) +module Pair (Domain1 : S) (Domain2 : S) : S with type astate = Domain1.astate * Domain2.astate + +(** 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 FiniteSet (Set : PrettyPrintable.PPSet) : sig + include PrettyPrintable.PPSet with type t = Set.t and type elt = Set.elt + include S with type astate = t +end + +(** Lift a map whose value type is an abstract domain to a domain. *) +module Map (Map : PrettyPrintable.PPMap) (ValueDomain : S) : sig + include PrettyPrintable.PPMap with type 'a t = 'a Map.t and type key = Map.key + include S with type astate = ValueDomain.astate Map.t +end diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/abstractDomain.ml index 39c0db90c..f20412420 100644 --- a/infer/src/checkers/abstractDomain.ml +++ b/infer/src/checkers/abstractDomain.ml @@ -21,7 +21,6 @@ module type S = sig val pp : F.formatter -> astate -> unit end -(** Lift a domain without bottom to a domain with bottom. *) module BottomLifted (Domain : S) = struct type astate = | Bottom @@ -61,7 +60,6 @@ module BottomLifted (Domain : S) = struct | NonBottom astate -> Domain.pp fmt astate end -(** Cartestian product of two domains. *) module Pair (Domain1 : S) (Domain2 : S) = struct type astate = Domain1.astate * Domain2.astate @@ -89,8 +87,6 @@ module Pair (Domain1 : S) (Domain2 : S) = struct F.fprintf fmt "(%a, %a)" Domain1.pp astate1 Domain2.pp astate2 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 FiniteSet (S : PrettyPrintable.PPSet) = struct include S type astate = t @@ -111,7 +107,6 @@ module FiniteSet (S : PrettyPrintable.PPSet) = struct join prev next end -(** Lift a map whose value type is an abstract domain to a domain. *) module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct include M type astate = ValueDomain.astate M.t