summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile1
-rw-r--r--abstract/abs_domain.ml221
-rw-r--r--abstract/abs_interp_dynpart.ml207
-rw-r--r--abstract/abs_interp_edd.ml72
-rw-r--r--abstract/enum_domain.ml7
-rw-r--r--abstract/enum_domain_edd.ml2
-rw-r--r--main.ml29
7 files changed, 357 insertions, 182 deletions
diff --git a/Makefile b/Makefile
index 07daf1d..3955694 100644
--- a/Makefile
+++ b/Makefile
@@ -19,6 +19,7 @@ SRC= main.ml \
abstract/num_domain.ml \
abstract/enum_domain.ml \
abstract/enum_domain_edd.ml \
+ abstract/abs_domain.ml \
\
abstract/formula.ml \
abstract/formula_printer.ml \
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
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index bbd8d19..0f6bbbf 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -5,20 +5,17 @@ open Typing
open Cmdline
open Util
-open Num_domain
-open Enum_domain
+open Abs_domain
open Varenv
-module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN)
+module I (D0 : ENVIRONMENT_DOMAIN)
: sig
val do_prog : cmdline_opt -> rooted_prog -> unit
end = struct
- type abs_v = ED.t * ND.t
-
(*
Abstract analysis based on dynamic partitionning of the state space.
Idea : use somme conditions appearing in the text of the program as
@@ -32,7 +29,7 @@ end = struct
id : int;
depth : int;
- mutable def : abs_v;
+ mutable def : D0.t;
is_init : bool;
mutable f : bool_expr;
@@ -40,7 +37,7 @@ end = struct
(* For chaotic iteration fixpoint *)
mutable in_c : int;
- mutable v : abs_v;
+ mutable v : D0.t;
mutable out_t : int list;
mutable in_t : int list;
@@ -69,86 +66,32 @@ end = struct
************************** *)
(*
- top : env -> abs_v
- bottom : env -> abs_v
- *)
- let top e = (ED.top e.ve.evars, ND.top e.ve.nvars)
- let bottom e = (ED.top e.ve.evars, ND.bottom e.ve.nvars)
- let is_bot (e, n) = ED.is_bot e || ND.is_bot n
-
- let print_v fmt (enum, num) =
- if is_bot (enum, num) then
- Format.fprintf fmt "⊥"
- else
- Format.fprintf fmt "@[<hov 1>(%a,@ %a)@]" ED.print enum ND.print num
-
- (*
- join : abs_v -> abs_v -> abs_v
- widen : abs_v -> abs_v -> abs_v
- meet : abs_v -> abs_v -> abs_v
- *)
- let join a b =
- if is_bot a then b
- else if is_bot b then a
- else (ED.join (fst a) (fst b), ND.join (snd a) (snd b))
-
- let widen a b =
- if is_bot a then b
- else if is_bot b then a
- else (ED.join (fst a) (fst b), ND.widen (snd a) (snd b))
-
- let meet (e1, n1) (e2, n2) =
- if is_bot (e1, n1) then ED.vtop e1, ND.vbottom n1
- else if is_bot (e2, n2) then ED.vtop e2, ND.vbottom n2
- else
- try (ED.meet e1 e2 , ND.meet n1 n2)
- with Bot -> ED.vtop e1, ND.vbottom n1
-
- (*
- eq_v : abs_v -> abs_v -> bool
- subset_v : abs_v -> abs_v -> bool
+ apply_cl : D0.t -> conslist -> D0.t
*)
- let eq_v (a, b) (c, d) =
- (is_bot (a, b) && is_bot (c, d))
- || (ED.eq a c && ND.eq b d)
-
- let subset_v (a, b) (c, d) =
- (is_bot (a, b)) ||
- (not (is_bot (c, d)) && ED.subset a c && ND.subset b d)
-
- (*
- apply_cl : abs_v -> conslist -> abs_v
- *)
- let rec apply_cl (enum, num) (ec, nc, r) =
+ let rec apply_cl v (ec, nc, r) =
begin match r with
| CLTrue ->
- begin
- try (ED.apply_cl enum ec, ND.apply_cl num nc)
- with Bot -> ED.vtop enum, ND.vbottom num
- end
+ D0.apply_ncl (D0.apply_ecl v ec) nc
| CLFalse ->
- (ED.vtop enum, ND.vbottom num)
+ D0.bottom (D0.varenv v)
| CLAnd(a, b) ->
- let enum, num = apply_cl (enum, num) (ec, nc, a) in
- let enum, num = apply_cl (enum, num) ([], nc, b) in
- enum, num
+ let v = apply_cl v (ec, nc, a) in
+ let v = apply_cl v ([], nc, b) in
+ v
| CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
- let a = apply_cl (enum, num) (ec@eca, nc@nca, ra) in
- let b = apply_cl (enum, num) (ec@ecb, nc@ncb, rb) in
- join a b
+ let a = apply_cl v (ec@eca, nc@nca, ra) in
+ let b = apply_cl v (ec@ecb, nc@ncb, rb) in
+ D0.join a b
end
(*
- apply_cl_all_cases : abs_v -> conslist -> abs_v list
+ apply_cl_all_cases : D0.t -> conslist -> D0.t list
*)
let rec apply_cl_all_cases v (ec, nc, r) =
match r with
| CLTrue ->
- let v =
- try ED.apply_cl (fst v) ec, ND.apply_cl (snd v) nc
- with Bot -> ED.vtop (fst v), ND.vbottom (snd v)
- in
- if is_bot v then [] else [v]
+ let v = D0.apply_ncl (D0.apply_ecl v ec) nc in
+ if D0.is_bot v then [] else [v]
| CLFalse ->
[]
| CLAnd(a, b) ->
@@ -158,7 +101,7 @@ end = struct
| CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
let la = apply_cl_all_cases v (ec@eca, nc@nca, ra) in
let lb = apply_cl_all_cases v (ec@ecb, nc@ncb, rb) in
- lb@(List.filter (fun a -> not (List.exists (fun b -> eq_v a b) lb)) la)
+ lb@(List.filter (fun a -> not (List.exists (fun b -> D0.eq a b) lb)) la)
(* ***************************
@@ -237,14 +180,14 @@ end = struct
{
id;
depth = 0;
- def = apply_cl (top env) (conslist_of_f cf);
+ def = apply_cl (D0.top env.ve) (conslist_of_f cf);
is_init;
f = cf;
cl = conslist_of_f cf;
in_c = 0;
- v = bottom env;
+ v = D0.bottom env.ve;
out_t = [];
in_t = [];
@@ -281,41 +224,29 @@ end = struct
set_target_case : env -> edd_v -> bool_expr -> edd_v
cycle : env -> edd_v -> conslist -> edd_v
*)
- let pass_cycle env (enum, num) =
+ let pass_cycle env v =
let assign_e, assign_n = List.fold_left
(fun (ae, an) (a, b, t) -> match t with
| TEnum _ -> (a, b)::ae, an
| TInt | TReal -> ae, (a, NIdent b)::an)
([], []) env.cycle in
- let enum = ED.assign enum assign_e in
- let num = ND.assign num assign_n in
+ let v = D0.eassign v assign_e in
+ let v = D0.nassign v assign_n in
- let ef, nf = List.fold_left
- (fun (ef, nf) (var, t) -> match t with
- | TEnum _ -> var::ef, nf
- | TReal | TInt -> ef, var::nf)
- ([], []) env.forget in
+ D0.forgetvars v (List.map fst env.forget)
- (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
-
- let unpass_cycle env (enum, num) =
+ let unpass_cycle env v =
let assign_e, assign_n = List.fold_left
(fun (ae, an) (a, b, t) -> match t with
| TEnum _ -> (b, a)::ae, an
| TInt | TReal -> ae, (b, NIdent a)::an)
([], []) env.ve.cycle in
- let enum = ED.assign enum assign_e in
- let num = ND.assign num assign_n in
-
- let ef, nf = List.fold_left
- (fun (ef, nf) (var, t) -> match t with
- | TEnum _ -> var::ef, nf
- | TReal | TInt -> ef, var::nf)
- ([], []) env.ve.forget_inv in
+ let v = D0.eassign v assign_e in
+ let v = D0.nassign v assign_n in
- (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
+ D0.forgetvars v (List.map fst env.ve.forget_inv)
(*
print_locs : env -> unit
@@ -324,7 +255,7 @@ end = struct
let print_locs_defs e =
Hashtbl.iter
(fun id loc ->
- Format.printf "q%d: @[<v 2>%a@]@." id print_v loc.def;
+ Format.printf "q%d: @[<v 2>%a@]@." id D0.print loc.def;
)
e.loc
@@ -332,9 +263,9 @@ end = struct
Hashtbl.iter
(fun id loc ->
Format.printf "@.";
- Format.printf "q%d (depth = %d):@. D: @[<v 2>%a@]@." id loc.depth print_v loc.def;
+ Format.printf "q%d (depth = %d):@. D: @[<v 2>%a@]@." id loc.depth D0.print loc.def;
(*Format.printf " F: (%a)@." Formula_printer.print_expr loc.f;*)
- Format.printf " V: %a@." print_v loc.v;
+ Format.printf " V: %a@." D0.print loc.v;
Format.printf " -> @[<hov>[%a]@]@."
(print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
)
@@ -385,10 +316,10 @@ end = struct
loc.in_t <- [];
loc.in_c <- 0;
if loc.is_init then begin
- loc.v <- apply_cl (top e) loc.cl;
+ loc.v <- apply_cl (D0.top e.ve) loc.cl;
delta := q::!delta
end else
- loc.v <- bottom e)
+ loc.v <- D0.bottom e.ve)
e.loc;
(*print_locs_defs e;*)
@@ -404,14 +335,14 @@ end = struct
let start = loc.v in
let f i =
- (*Format.printf "I: %a@." print_v i;*)
- let i' = meet i (unpass_cycle e loc.def) in
- (*Format.printf "I': %a@." print_v i';*)
- let j = join start
+ (*Format.printf "I: %a@." D0.print i;*)
+ let i' = D0.meet i (unpass_cycle e loc.def) in
+ (*Format.printf "I': %a@." D0.print i';*)
+ let j = D0.join start
(apply_cl
- (meet (pass_cycle e.ve i') loc.def)
+ (D0.meet (pass_cycle e.ve i') loc.def)
loc.cl) in
- (*Format.printf "J: %a@." print_v j;*)
+ (*Format.printf "J: %a@." D0.print j;*)
j
in
@@ -419,11 +350,11 @@ end = struct
let fi = f i in
let j =
if n < e.opt.widen_delay then
- join i fi
+ D0.join i fi
else
- widen i fi
+ D0.widen i fi
in
- if eq_v i j
+ if D0.eq i j
then i
else iter (n+1) j
in
@@ -432,27 +363,27 @@ end = struct
let u = pass_cycle e.ve z in
if e.opt.verbose_ci then
- Format.printf "Fixpoint: %a@. mem fp: %a@." print_v z print_v u;
+ Format.printf "Fixpoint: %a@. mem fp: %a@." D0.print z D0.print u;
loc.v <- z;
Hashtbl.iter
(fun t loc2 ->
- let v = meet u loc2.def in
+ let v = D0.meet u loc2.def in
let w = apply_cl v loc2.cl in
- (*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*)
- if not (is_bot w) then begin
+ (*Format.printf "u: %a@.v: %a@. w: %a@." D0.print u D0.print v D0.print w;*)
+ if not (D0.is_bot w) then begin
if e.opt.verbose_ci then
- Format.printf "%d -> %d with:@. %a@." s t print_v w;
+ Format.printf "%d -> %d with:@. %a@." s t D0.print w;
if not (List.mem s loc2.in_t)
then loc2.in_t <- s::loc2.in_t;
if not (List.mem t loc.out_t)
then loc.out_t <- t::loc.out_t;
- if not (subset_v w loc2.v) then begin
+ if not (D0.subset w loc2.v) then begin
if loc2.in_c < e.opt.widen_delay then
- loc2.v <- join loc2.v w
+ loc2.v <- D0.join loc2.v w
else
- loc2.v <- widen loc2.v w;
+ loc2.v <- D0.widen loc2.v w;
loc2.in_c <- loc2.in_c + 1;
if not (List.mem t !delta)
then delta := t::!delta
@@ -467,7 +398,7 @@ end = struct
let useless = ref [] in
Hashtbl.iter
(fun i loc ->
- if is_bot loc.v then begin
+ if D0.is_bot loc.v then begin
Format.printf "Useless location detected: q%d@." i;
useless := i::!useless
end)
@@ -479,7 +410,7 @@ end = struct
(fun _ loc ->
let verif, violate = List.partition
(fun (_, f, _) ->
- is_bot (apply_cl loc.v (conslist_of_f f)))
+ D0.is_bot (apply_cl loc.v (conslist_of_f f)))
e.guarantees
in
loc.verif_g <- List.map (fun (a, b, c) -> a) verif;
@@ -511,12 +442,12 @@ end = struct
try
let cond, _ = List.find
(fun (c, _) ->
- is_bot (apply_cl loc.v (conslist_of_f c))
- || is_bot (apply_cl loc.v (conslist_of_f (BNot c))))
+ D0.is_bot (apply_cl loc.v (conslist_of_f c))
+ || D0.is_bot (apply_cl loc.v (conslist_of_f (BNot c))))
(ternary_conds loc.f)
in
let tr =
- if is_bot (apply_cl loc.v (conslist_of_f cond))
+ if D0.is_bot (apply_cl loc.v (conslist_of_f cond))
then BNot cond
else cond
in
@@ -538,13 +469,13 @@ end = struct
let cs = ternary_conds loc.f in
List.iter
(fun (c, exprs) ->
- let cases_t = apply_cl_all_cases (top e) (conslist_of_f c) in
- let cases_f = apply_cl_all_cases (top e) (conslist_of_f (BNot c)) in
+ let cases_t = apply_cl_all_cases (D0.top e.ve) (conslist_of_f c) in
+ let cases_f = apply_cl_all_cases (D0.top e.ve) (conslist_of_f (BNot c)) in
let cases = List.mapi (fun i c -> i, c) (cases_t @ cases_f) in
if
List.length
(List.filter
- (fun (_, case) -> not (is_bot (meet loc.v case)))
+ (fun (_, case) -> not (D0.is_bot (D0.meet loc.v case)))
cases)
>= 2
then
@@ -554,10 +485,10 @@ end = struct
(fun qi ->
let loci = Hashtbl.find e.loc qi in
let v = apply_cl
- (meet (pass_cycle e.ve loci.v) loc.def)
+ (D0.meet (pass_cycle e.ve loci.v) loc.def)
loc.cl in
List.map
- (fun (ci, case) -> qi, ci, not (is_bot (meet v case)))
+ (fun (ci, case) -> qi, ci, not (D0.is_bot (D0.meet v case)))
cases)
loc.in_t
in
@@ -565,14 +496,14 @@ end = struct
let out_tc =
List.flatten @@ List.map
(fun (ci, case) ->
- let v = meet loc.v case in
+ let v = D0.meet loc.v case in
List.map
(fun qo ->
let loco = Hashtbl.find e.loc qo in
let w = apply_cl
- (meet (pass_cycle e.ve v) loco.def)
+ (D0.meet (pass_cycle e.ve v) loco.def)
loco.cl
- in qo, ci, not (is_bot w))
+ in qo, ci, not (D0.is_bot w))
loc.out_t)
cases
in
@@ -672,13 +603,13 @@ end = struct
Format.printf "@.Found no more possible refinement.@.@."
| Some (score, q, c, cases_t, cases_f) ->
Format.printf "@.Refine q%d : @[<v 2>[ %a ]@]@." q
- (print_list print_v ", ") (cases_t@cases_f);
+ (print_list D0.print ", ") (cases_t@cases_f);
let loc = Hashtbl.find e.loc q in
Hashtbl.remove e.loc loc.id;
let handle_case cc case =
- if not (is_bot (meet loc.v case)) then
+ if not (D0.is_bot (D0.meet loc.v case)) then
let ff = simplify_k [cc] loc.f in
let ff = simplify_k (get_root_true ff) ff in
@@ -686,7 +617,7 @@ end = struct
{ loc with
id = (incr e.counter; !(e.counter));
depth = loc.depth + 1;
- def = meet loc.def case;
+ def = D0.meet loc.def case;
f = ff;
cl = conslist_of_f ff } in
Hashtbl.add e.loc loc2.id loc2
@@ -727,15 +658,15 @@ end = struct
if List.exists (fun (p, _, _) -> p) e.ve.all_vars then begin
let final =
Hashtbl.fold
- (fun _ loc v -> join v loc.v)
- e.loc (bottom e) in
+ (fun _ loc v -> D0.join v loc.v)
+ e.loc (D0.bottom e.ve) in
Format.printf "Probes: @[<v 0>";
List.iter (fun (p, id, ty) ->
if p then match ty with
| TInt | TReal ->
Format.printf "%a ∊ %a@ " Formula_printer.print_id id
- ND.print_itv (ND.project (snd final) id)
+ D0.print_itv (D0.nproject final id)
| TEnum _ -> Format.printf "%a : enum variable@ "
Formula_printer.print_id id)
e.ve.all_vars;
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index cdf3c7e..074987f 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -5,7 +5,7 @@ open Typing
open Cmdline
open Util
-open Num_domain
+open Abs_domain
open Varenv
@@ -14,7 +14,7 @@ exception Top
exception Found_int of int
-module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
+module I (D0 : ENVIRONMENT_DOMAIN) : sig
val do_prog : cmdline_opt -> rooted_prog -> unit
@@ -56,7 +56,7 @@ end = struct
type edd_v = {
ve : varenv;
root : edd;
- leaves : (int, ND.t) Hashtbl.t;
+ leaves : (int, D0.t) Hashtbl.t;
}
(*
@@ -120,10 +120,10 @@ end = struct
let leaves = Hashtbl.create 12 in
let lc = ref 0 in
let get_leaf st x =
- if ND.is_top x then DTop else
- if ND.is_bot x then DBot else
+ if D0.is_top x then DTop else
+ if D0.is_bot x then DBot else
try
- Hashtbl.iter (fun i v -> if ND.eq v x then raise (Found_int i)) leaves;
+ Hashtbl.iter (fun i v -> if D0.eq v x then raise (Found_int i)) leaves;
incr lc;
Hashtbl.add leaves !lc x;
DVal (!lc, st)
@@ -205,7 +205,7 @@ end = struct
for id = 0 to !max_v do
try let v = Hashtbl.find v.leaves id in
- Format.fprintf fmt "v%d: %a@." id ND.print v
+ Format.fprintf fmt "v%d: %a@." id D0.print v
with Not_found -> ()
done
@@ -324,7 +324,7 @@ end = struct
dq vb kl
| DVal (u, _), DVal (v, _) ->
- let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+ let x = D0.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
get_leaf x
| DVal(u, _), DBot ->
get_leaf (Hashtbl.find a.leaves u)
@@ -365,7 +365,7 @@ end = struct
dq vb kl
| DVal (u, _) , DVal (v, _) ->
- let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+ let x = D0.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
get_leaf x
| DVal(u, _), DTop ->
get_leaf (Hashtbl.find a.leaves u)
@@ -380,10 +380,10 @@ end = struct
(*
- edd_num_apply : edd_v -> (ND.t -> ND.t) -> edd_v
+ edd_leaf_apply : edd_v -> (D0.t -> D0.t) -> edd_v
edd_apply_ncl : edd_v -> num_cons list -> edd_v
*)
- let edd_num_apply v nfun =
+ let edd_leaf_apply v nfun =
let ve = v.ve in
let leaves, get_leaf = get_leaf_fun () in
@@ -393,7 +393,7 @@ end = struct
let f f_rec n =
match n with
| DBot -> DBot
- | DTop -> get_leaf (nfun (ND.top ve.nvars))
+ | DTop -> get_leaf (nfun (D0.top ve))
| DVal (i, _) -> get_leaf (nfun (Hashtbl.find v.leaves i))
| DChoice(n, var, l) ->
let l = List.map (fun (k, v) -> k, f_rec v) l in
@@ -402,7 +402,7 @@ end = struct
{ leaves; ve; root = memo f v.root }
let edd_apply_ncl v ncl =
- edd_num_apply v (fun n -> ND.apply_cl n ncl)
+ edd_leaf_apply v (fun n -> D0.apply_ncl n ncl)
(*
edd_apply_ecl : edd_v -> enum_cons list -> edd_v
@@ -418,13 +418,15 @@ end = struct
in
let cons_edd = cl_k ec in
edd_meet v cons_edd
- (*List.fold_left (fun v c -> edd_meet v (edd_of_cons v.ve c)) v ec*)
(*
edd_apply_cl : edd_v -> conslist -> edd_v
*)
let rec edd_apply_cl v (ec, nc, r) =
- let v = edd_apply_ecl v ec in
+ let v = edd_leaf_apply
+ (edd_apply_ecl v ec)
+ (fun k -> D0.apply_ecl k ec)
+ in
match r with
| CLTrue ->
edd_apply_ncl v nc
@@ -465,7 +467,7 @@ end = struct
| DBot, DBot -> true
| DTop, DTop -> true
| DVal (i, _), DVal (j, _) ->
- ND.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
+ D0.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
| DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
la lb
@@ -484,11 +486,11 @@ end = struct
| _, DTop -> true
| DTop, DBot -> false
- | DVal(i, _), DBot -> ND.is_bot (Hashtbl.find a.leaves i)
- | DTop, DVal(i, _) -> ND.is_top (Hashtbl.find b.leaves i)
+ | DVal(i, _), DBot -> D0.is_bot (Hashtbl.find a.leaves i)
+ | DTop, DVal(i, _) -> D0.is_top (Hashtbl.find b.leaves i)
| DVal(i, _), DVal(j, _) ->
- ND.subset (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
+ D0.subset (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
| DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
@@ -530,8 +532,10 @@ end = struct
if cn = [] then
if fn = [] then DBot
else
- let x = list_fold_op ND.join
- (List.map (Hashtbl.find v.leaves) fn)
+ let x = list_fold_op D0.join
+ (List.map
+ (fun i -> D0.forgetvars (Hashtbl.find v.leaves i) vars)
+ fn)
in get_leaf x
else
let _, dv, cl = List.hd cn in
@@ -665,7 +669,7 @@ end = struct
let widen =
if edd_eq p1 p2 then true else false
in
- let x = (if widen then ND.widen else ND.join)
+ let x = (if widen then D0.widen else D0.join)
(Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
get_leaf x
@@ -711,7 +715,7 @@ end = struct
let p1, p2 = edd_extract_path a u, edd_extract_path b v in
let d1, d2 = Hashtbl.find a.leaves u, Hashtbl.find b.leaves v in
let widen = edd_eq p1 p2 && i1 >= env.opt.widen_delay in
- let x = (if widen then ND.widen else ND.join) d1 d2 in
+ let x = (if widen then D0.widen else D0.join) d1 d2 in
get_leaf (s1, i1 + 1) x
| DChoice(_,va, la), _ when rank ve na < rank ve nb ->
@@ -754,7 +758,7 @@ end = struct
([], []) env.cycle in
let v = edd_eassign v assign_e in
- let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in
+ let v = edd_leaf_apply v (fun nv -> D0.nassign nv assign_n) in
let ef, nf = List.fold_left
(fun (ef, nf) (var, t) -> match t with
@@ -763,7 +767,7 @@ end = struct
([], []) env.forget in
let v = edd_forget_vars v ef in
- edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
+ edd_leaf_apply v (fun nv -> D0.forgetvars nv nf)
let unpass_cycle env v =
let assign_e, assign_n = List.fold_left
@@ -773,7 +777,7 @@ end = struct
([], []) env.ve.cycle in
let v = edd_eassign v assign_e in
- let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in
+ let v = edd_leaf_apply v (fun nv -> D0.nassign nv assign_n) in
let ef, nf = List.fold_left
(fun (ef, nf) (var, t) -> match t with
@@ -782,7 +786,7 @@ end = struct
([], []) env.ve.forget_inv in
let v = edd_forget_vars v ef in
- edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
+ edd_leaf_apply v (fun nv -> D0.forgetvars nv nf)
@@ -988,8 +992,8 @@ end = struct
| TEnum _ -> id::l)
[] e.ve.all_vars) in
let final_flat = match final_flat.root with
- | DTop -> ND.top e.ve.nvars
- | DBot -> ND.bottom e.ve.nvars
+ | DTop -> D0.top e.ve
+ | DBot -> D0.bottom e.ve
| DVal(i, _) -> Hashtbl.find final_flat.leaves i
| DChoice _ -> assert false
in
@@ -999,9 +1003,13 @@ end = struct
if p then match ty with
| TInt | TReal ->
Format.printf "%a ∊ %a@ " Formula_printer.print_id id
- ND.print_itv (ND.project final_flat id)
- | TEnum _ -> Format.printf "%a : enum variable@ "
- Formula_printer.print_id id)
+ D0.print_itv (D0.nproject final_flat id)
+ | TEnum _ ->
+ (* not precise : does not take into account info from decision graph *)
+ Format.printf "%a ∊ @[<hov 2>[%a]@]@ "
+ Formula_printer.print_id id
+ (print_list Format.pp_print_string ", ")
+ (D0.eproject final_flat id))
e.ve.all_vars;
Format.printf "@]@."
end
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index 68b04f5..b035cc0 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -26,6 +26,7 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig
val bottom : (id * item list) list -> t
val vtop : t -> t (* top with same vars *)
val is_bot : t -> bool
+ val is_top : t -> bool
(* variable management *)
val vars : t -> (id * item list) list
@@ -67,6 +68,7 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
let vtop x = { x with value = VarMap.empty }
let bottom vars = raise Bot (* we don't represent Bot *)
let is_bot x = false
+ let is_top x = VarMap.is_empty x.value
let vars x = x.vars
@@ -197,6 +199,11 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
let vtop x = { x with value = VarMap.empty }
let bottom vars = raise Bot (* we don't represent Bot *)
let is_bot x = false
+ let is_top x =
+ VarMap.for_all
+ (fun k v -> List.for_all (fun vv -> List.mem vv v)
+ (List.assoc k x.vars))
+ x.value
let vars x = x.vars
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
index 3e03d59..ed13798 100644
--- a/abstract/enum_domain_edd.ml
+++ b/abstract/enum_domain_edd.ml
@@ -150,8 +150,10 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
(*
is_bot : t -> bool
+ is_top : t -> bool
*)
let is_bot x = (x.root = DBot)
+ let is_top x = (x.root = DTop)
(*
vars : t -> (id * item list) list
diff --git a/main.ml b/main.ml
index f130b6c..0dc0408 100644
--- a/main.ml
+++ b/main.ml
@@ -8,6 +8,8 @@ open Num_domain
open Nonrelational
open Apron_domain
+open Abs_domain
+
open Enum_domain_edd
open Abs_interp_dynpart
@@ -16,23 +18,26 @@ module Interpret = Interpret.I
module ItvND = Apron_domain.ND_Box (* Nonrelational.ND(Intervals_domain.VD) *)
module PolyND = Apron_domain.ND_Poly
module OctND = Apron_domain.ND_Oct
+module ItvOND = NumDomainOnly(ItvND)
+module PolyOND = NumDomainOnly(PolyND)
+module OctOND = NumDomainOnly(OctND)
+module ItvEND = NumEnumDomain(Enum_domain.MultiValuation)(ItvND)
+module PolyEND = NumEnumDomain(Enum_domain.MultiValuation)(PolyND)
+module ItvENDEdd = NumEnumDomain(Enum_domain_edd.EDD)(ItvND)
+module PolyENDEdd = NumEnumDomain(Enum_domain_edd.EDD)(PolyND)
module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(PolyND)
module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(OctND)
-module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
-module AI_Poly_EDD = Abs_interp_edd.I(PolyND)
-module AI_Oct_EDD = Abs_interp_edd.I(OctND)
-
-module AI_S_Itv_DP = Abs_interp_dynpart.I
- (Enum_domain.MultiValuation)(ItvND)
-module AI_S_Rel_DP = Abs_interp_dynpart.I
- (Enum_domain.MultiValuation)(PolyND)
-module AI_EDD_Itv_DP = Abs_interp_dynpart.I
- (Enum_domain_edd.EDD)(ItvND)
-module AI_EDD_Rel_DP = Abs_interp_dynpart.I
- (Enum_domain_edd.EDD)(PolyND)
+module AI_Itv_EDD = Abs_interp_edd.I(ItvOND)
+module AI_Poly_EDD = Abs_interp_edd.I(PolyOND)
+module AI_Oct_EDD = Abs_interp_edd.I(OctOND)
+
+module AI_S_Itv_DP = Abs_interp_dynpart.I(ItvEND)
+module AI_S_Rel_DP = Abs_interp_dynpart.I(PolyEND)
+module AI_EDD_Itv_DP = Abs_interp_dynpart.I(ItvENDEdd)
+module AI_EDD_Rel_DP = Abs_interp_dynpart.I(PolyENDEdd)
(* command line options *)
let times = ref false