summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--abstract/abs_domain.ml221
1 files changed, 221 insertions, 0 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
new file mode 100644
index 0000000..ce58c3b
--- /dev/null
+++ b/abstract/abs_domain.ml
@@ -0,0 +1,221 @@
+open Ast
+open Formula
+
+open Num_domain
+open Enum_domain
+
+open Varenv
+
+module type ENVIRONMENT_DOMAIN = sig
+ type t
+ type itv
+
+ (* constructors *)
+ val top : varenv -> t
+ val bottom : varenv -> t
+ val is_top : t -> bool
+ val is_bot : t -> bool
+
+ (* variable management *)
+ val varenv : t -> varenv
+
+ val forgetvar : t -> id -> t
+ val forgetvars : t -> id list -> t
+ val nproject : t -> id -> itv (* numerical project *)
+ val eproject : t -> id -> item list
+
+ (* set-theoretic operations *)
+ val join : t -> t -> t
+ val meet : t -> t -> t
+ val widen : t -> t -> t
+
+ val subset : t -> t -> bool
+ val eq : t -> t -> bool
+
+ (* abstract operations *)
+ val apply_ec : t -> enum_cons -> t
+ val apply_ecl : t -> enum_cons list -> t
+ val apply_nc : t -> num_cons -> t
+ val apply_ncl : t -> num_cons list -> t
+ val eassign : t -> (id * id) list -> t
+ val nassign : t -> (id * num_expr) list -> t
+
+ (* pretty-printing *)
+ val print : Format.formatter -> t -> unit
+ val print_vars : Format.formatter -> t -> id list -> unit
+ val print_itv : Format.formatter -> itv -> unit
+
+end
+
+module NumDomainOnly(ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN =
+struct
+
+ type t = varenv * ND.t
+ type itv = ND.itv
+
+ let top ve = (ve, ND.top ve.nvars)
+ let bottom ve = (ve, ND.top ve.nvars)
+ let is_top (_, x) = ND.is_top x
+ let is_bot (_, x) = ND.is_bot x
+
+ let varenv (ve, x) = ve
+
+ let forgetvar (ve, x) id =
+ if List.exists (fun (i, _) -> i = id) ve.nvars
+ then (ve, ND.forgetvar x id)
+ else (ve, x)
+ let forgetvars (ve, x) ids =
+ (ve, List.fold_left ND.forgetvar x
+ (List.filter (fun id -> List.exists (fun (i, _) -> i = id) ve.nvars) ids))
+ let nproject (_, x) id = ND.project x id
+ let eproject (ve, _) id = List.assoc id ve.evars
+
+ let join (ve, a) (_, b) = (ve, ND.join a b)
+ let meet (ve, a) (_, b) = (ve, ND.meet a b)
+ let widen (ve, a) (_, b) = (ve, ND.widen a b)
+
+ let subset (_, a) (_, b) = ND.subset a b
+ let eq (_, a) (_, b) = ND.eq a b
+
+ let apply_ec x _ = x
+ let apply_ecl x _ = x
+ let apply_nc (ve, x) c = (ve, ND.apply_cons x c)
+ let apply_ncl (ve, x) cl = (ve, ND.apply_cl x cl)
+ let eassign x _ = x
+ let nassign (ve, x) ex = (ve, ND.assign x ex)
+
+ let print fmt (_, x) = ND.print fmt x
+ let print_vars fmt (ve, x) ids =
+ ND.print_vars fmt x
+ (List.filter
+ (fun id -> List.exists (fun (i, _) -> i = id) ve.nvars) ids)
+ let print_itv = ND.print_itv
+
+end
+
+module NumEnumDomain
+ (ED : ENUM_ENVIRONMENT_DOMAIN)(ND : NUMERICAL_ENVIRONMENT_DOMAIN)
+ : ENVIRONMENT_DOMAIN
+= struct
+
+ type t =
+ | V of varenv * ED.t * ND.t
+ | Bot of varenv
+ type itv = ND.itv
+
+ let strict = function
+ | V(ve, enum, num) as x ->
+ if ND.is_bot num || ED.is_bot enum
+ then Bot ve
+ else x
+ | b -> b
+ let strict_apply f x = match x with
+ | V(ve, enum, num) ->
+ begin
+ try strict (f (ve, enum, num))
+ with Enum_domain.Bot -> Bot ve
+ end
+ | Bot ve -> Bot ve
+
+ let top ve = V(ve, ED.top ve.evars, ND.top ve.nvars)
+ let bottom ve = Bot ve
+ let is_top x = match strict x with
+ | Bot _ -> false
+ | V(_, enum, num) -> ED.is_top enum && ND.is_top num
+ let is_bot x = match strict x with
+ | Bot _ -> true
+ | _ -> false
+
+ let varenv = function
+ | Bot x -> x
+ | V(ve, _, _) -> ve
+
+ let forgetvar x id =
+ strict_apply (fun (ve, enum, num) ->
+ if List.exists (fun (id2, _) -> id2 = id) ve.evars
+ then V(ve, ED.forgetvar enum id, num)
+ else V(ve, enum, ND.forgetvar num id))
+ x
+
+ let forgetvars x ids =
+ strict_apply (fun (ve, enum, num) ->
+ let efv, nfv = List.fold_left
+ (fun (efv, nfv) id ->
+ if List.exists (fun (id2, _) -> id2 = id) ve.evars
+ then id::efv, nfv
+ else efv, id::nfv)
+ ([], []) ids
+ in
+ V(ve, ED.forgetvars enum efv, List.fold_left ND.forgetvar num nfv))
+ x
+
+ let nproject x id = match x with
+ | V(ve, enum, num) ->
+ ND.project num id
+ | Bot ve -> ND.project (ND.bottom ve.nvars) id
+ let eproject x id = match x with
+ | V(ve, enum, num) ->
+ ED.project enum id
+ | Bot ve -> []
+
+ let join x y = match strict x, strict y with
+ | Bot _, a | a, Bot _ -> a
+ | V(ve, enum, num), V(_, enum', num') ->
+ V(ve, ED.join enum enum', ND.join num num')
+
+ let meet x y = match strict x, strict y with
+ | Bot ve, a | a, Bot ve -> Bot ve
+ | V(ve, enum, num), V(_, enum', num') ->
+ try
+ strict (V(ve, ED.meet enum enum', ND.meet num num'))
+ with Enum_domain.Bot -> Bot ve
+
+ let widen x y = match strict x, strict y with
+ | Bot _, a | a, Bot _ -> a
+ | V(ve, enum, num), V(_, enum', num') ->
+ V(ve, ED.join enum enum', ND.widen num num')
+
+ let subset x y = match strict x, strict y with
+ | Bot _, a -> true
+ | V(_, _, _), Bot _ -> false
+ | V(_, enum, num), V(_, enum', num') ->
+ ED.subset enum enum' && ND.subset num num'
+
+ let eq x y = match strict x, strict y with
+ | Bot _, Bot _ -> true
+ | V(_, enum, num), V(_, enum', num') ->
+ ED.eq enum enum' && ND.eq num num'
+ | _ -> false
+
+ let apply_ec x f =
+ strict_apply
+ (fun (ve, enum, num) -> V(ve, ED.apply_cl enum [f], num))
+ x
+ let apply_ecl x f =
+ strict_apply (fun (ve, enum, num) -> V(ve, ED.apply_cl enum f, num)) x
+ let apply_nc x f =
+ strict_apply (fun (ve, enum, num) -> V(ve, enum, ND.apply_cons num f)) x
+ let apply_ncl x f =
+ strict_apply (fun (ve, enum, num) -> V(ve, enum, ND.apply_cl num f)) x
+ let eassign x ass =
+ strict_apply (fun (ve, enum, num) -> V(ve, ED.assign enum ass, num)) x
+ let nassign x ass =
+ strict_apply (fun (ve, enum, num) -> V(ve, enum, ND.assign num ass)) x
+
+ let print_itv = ND.print_itv
+ let print fmt x = match strict x with
+ | Bot _ -> Format.fprintf fmt "⊥"
+ | V(_, enum, num) ->
+ Format.fprintf fmt "@[<hov 1>(%a,@ %a)@]" ED.print enum ND.print num
+ let print_vars fmt x vars = match strict x with
+ | Bot _ -> Format.fprintf fmt "⊥"
+ | V(ve, enum, num) ->
+ let nvars = List.filter
+ (fun v -> List.exists (fun (x, _) -> x = v) ve.nvars)
+ vars
+ in
+ Format.fprintf fmt "@[<hov 1>(%a,@ " ED.print enum;
+ ND.print_vars fmt num nvars;
+ Format.printf ")@]"
+
+end