|
|
|
@ -12,47 +12,47 @@ module F = Format
|
|
|
|
|
module type AbstractDomain = sig
|
|
|
|
|
type astate
|
|
|
|
|
|
|
|
|
|
val init : astate (* the initial state *)
|
|
|
|
|
val bot : astate
|
|
|
|
|
val is_bot : astate -> bool
|
|
|
|
|
val lteq : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *)
|
|
|
|
|
val initial : astate
|
|
|
|
|
val bottom : astate
|
|
|
|
|
val is_bottom : astate -> bool
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
module BotLiftedAbstractDomain (A : AbstractDomain) : AbstractDomain = struct
|
|
|
|
|
module BottomLiftedAbstractDomain (A : AbstractDomain) : AbstractDomain = struct
|
|
|
|
|
type astate =
|
|
|
|
|
| Bot
|
|
|
|
|
| NonBot of A.astate
|
|
|
|
|
| Bottom
|
|
|
|
|
| NonBottom of A.astate
|
|
|
|
|
|
|
|
|
|
let bot = Bot
|
|
|
|
|
let bottom = Bottom
|
|
|
|
|
|
|
|
|
|
let is_bot astate =
|
|
|
|
|
astate = Bot
|
|
|
|
|
let is_bottom astate =
|
|
|
|
|
astate = Bottom
|
|
|
|
|
|
|
|
|
|
let init = NonBot A.init
|
|
|
|
|
let initial = NonBottom A.initial
|
|
|
|
|
|
|
|
|
|
let lteq ~lhs ~rhs = match lhs, rhs with
|
|
|
|
|
| Bot, _ -> true
|
|
|
|
|
| _ , Bot -> false
|
|
|
|
|
| NonBot lhs, NonBot rhs -> A.lteq ~lhs ~rhs
|
|
|
|
|
let (<=) ~lhs ~rhs = match lhs, rhs with
|
|
|
|
|
| Bottom, _ -> true
|
|
|
|
|
| _ , Bottom -> false
|
|
|
|
|
| NonBottom lhs, NonBottom rhs -> A.(<=) ~lhs ~rhs
|
|
|
|
|
|
|
|
|
|
let join astate1 astate2 =
|
|
|
|
|
match astate1, astate2 with
|
|
|
|
|
| Bot, _ -> astate2
|
|
|
|
|
| _, Bot -> astate1
|
|
|
|
|
| NonBot a1, NonBot a2 -> NonBot (A.join a1 a2)
|
|
|
|
|
| Bottom, _ -> astate2
|
|
|
|
|
| _, Bottom -> astate1
|
|
|
|
|
| NonBottom a1, NonBottom a2 -> NonBottom (A.join a1 a2)
|
|
|
|
|
|
|
|
|
|
let widen ~prev ~next ~num_iters =
|
|
|
|
|
match prev, next with
|
|
|
|
|
| Bot, _ -> next
|
|
|
|
|
| _, Bot -> prev
|
|
|
|
|
| NonBot prev, NonBot next -> NonBot (A.widen ~prev ~next ~num_iters)
|
|
|
|
|
| Bottom, _ -> next
|
|
|
|
|
| _, Bottom -> prev
|
|
|
|
|
| NonBottom prev, NonBottom next -> NonBottom (A.widen ~prev ~next ~num_iters)
|
|
|
|
|
|
|
|
|
|
let pp fmt = function
|
|
|
|
|
| Bot -> F.fprintf fmt "_|_"
|
|
|
|
|
| NonBot astate -> A.pp fmt astate
|
|
|
|
|
| Bottom -> F.fprintf fmt "_|_"
|
|
|
|
|
| NonBottom astate -> A.pp fmt astate
|
|
|
|
|
|
|
|
|
|
end
|
|
|
|
|