diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 048376395..190697a54 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -56,14 +56,8 @@ module type WithTop = sig val is_top : t -> bool end -module BottomLifted (Domain : S) = struct - type t = Domain.t bottom_lifted - - let bottom = Bottom - - let is_bottom = function Bottom -> true | NonBottom _ -> false - - let ( <= ) ~lhs ~rhs = +module BottomLiftedUtils = struct + let ( <= ) ~le ~lhs ~rhs = if phys_equal lhs rhs then true else match (lhs, rhs) with @@ -72,9 +66,32 @@ module BottomLifted (Domain : S) = struct | _, Bottom -> false | NonBottom lhs, NonBottom rhs -> - Domain.( <= ) ~lhs ~rhs + le ~lhs ~rhs + let map ~f astate = + match astate with + | Bottom -> + astate + | NonBottom a -> + let a' = f a in + if phys_equal a' a then astate else NonBottom a' + + + let pp_bottom f = F.pp_print_string f SpecialChars.up_tack + + let pp ~pp f = function Bottom -> pp_bottom f | NonBottom astate -> pp f astate +end + +module BottomLifted (Domain : S) = struct + type t = Domain.t bottom_lifted + + let bottom = Bottom + + let is_bottom = function Bottom -> true | NonBottom _ -> false + + let ( <= ) = BottomLiftedUtils.( <= ) ~le:Domain.( <= ) + let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else @@ -99,30 +116,13 @@ module BottomLifted (Domain : S) = struct PhysEqual.optim2 ~res:(NonBottom (Domain.widen ~prev ~next ~num_iters)) prev0 next0 - let map ~f astate = - match astate with - | Bottom -> - astate - | NonBottom a -> - let a' = f a in - if phys_equal a' a then astate else NonBottom a' - + let map = BottomLiftedUtils.map - let pp fmt = function - | Bottom -> - F.pp_print_string fmt SpecialChars.up_tack - | NonBottom astate -> - Domain.pp fmt astate + let pp = BottomLiftedUtils.pp ~pp:Domain.pp end -module TopLifted (Domain : S) = struct - type t = Domain.t top_lifted - - let top = Top - - let is_top = function Top -> true | _ -> false - - let ( <= ) ~lhs ~rhs = +module TopLiftedUtils = struct + let ( <= ) ~le ~lhs ~rhs = if phys_equal lhs rhs then true else match (lhs, rhs) with @@ -131,8 +131,22 @@ module TopLifted (Domain : S) = struct | Top, _ -> false | NonTop lhs, NonTop rhs -> - Domain.( <= ) ~lhs ~rhs + le ~lhs ~rhs + + + let pp_top f = F.pp_print_string f SpecialChars.down_tack + + let pp ~pp f = function Top -> pp_top f | NonTop astate -> pp f astate +end + +module TopLifted (Domain : S) = struct + type t = Domain.t top_lifted + let top = Top + + let is_top = function Top -> true | _ -> false + + let ( <= ) = TopLiftedUtils.( <= ) ~le:Domain.( <= ) let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 @@ -154,11 +168,7 @@ module TopLifted (Domain : S) = struct PhysEqual.optim2 ~res:(NonTop (Domain.widen ~prev ~next ~num_iters)) prev0 next0 - let pp fmt = function - | Top -> - F.pp_print_string fmt SpecialChars.down_tack - | NonTop astate -> - Domain.pp fmt astate + let pp = TopLiftedUtils.pp ~pp:Domain.pp end module Pair (Domain1 : S) (Domain2 : S) = struct @@ -228,11 +238,11 @@ module Flat (V : PrettyPrintable.PrintableEquatableType) = struct let pp f = function | Bot -> - F.pp_print_string f SpecialChars.up_tack + BottomLiftedUtils.pp_bottom f | V v -> V.pp f v | Top -> - F.pp_print_string f SpecialChars.down_tack + TopLiftedUtils.pp_top f let v x = V x diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 7ab192d00..bf2188c2e 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -61,20 +61,22 @@ module type WithTop = sig val is_top : t -> bool end -(** Lift a pre-domain to a domain *) +(** Create a domain with Bottom element from a pre-domain *) module BottomLifted (Domain : S) : sig include WithBottom with type t = Domain.t bottom_lifted val map : f:(Domain.t -> Domain.t) -> t -> t end -(* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) -include - sig - [@@@warning "-60"] +module BottomLiftedUtils : sig + val pp : pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a bottom_lifted -> unit +end + +(** Create a domain with Top element from a pre-domain *) +module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted - (** Create a domain with Top element from a pre-domain *) - module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted +module TopLiftedUtils : sig + val pp_top : Format.formatter -> unit end (** Cartesian product of two domains. *) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 54cec6e9b..005555449 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -130,7 +130,7 @@ module ArrInfo = struct | Java {length} -> F.fprintf f "length : %a" Itv.pp length | Top -> - F.pp_print_string f SpecialChars.down_tack + AbstractDomain.TopLiftedUtils.pp_top f let is_symbolic : t -> bool = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index f280f7039..cb23a367c 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -1591,9 +1591,5 @@ module Mem = struct PowLoc.fold get_c_strlen' locs Val.bot - let pp f = function - | Bottom -> - F.pp_print_string f SpecialChars.down_tack - | NonBottom m -> - MemReach.pp f m + let pp f m = AbstractDomain.BottomLiftedUtils.pp ~pp:MemReach.pp f m end