|
|
|
@ -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
|
|
|
|
|