diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | abstract/abs_domain.ml | 221 | ||||
| -rw-r--r-- | abstract/abs_interp_dynpart.ml | 207 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 72 | ||||
| -rw-r--r-- | abstract/enum_domain.ml | 7 | ||||
| -rw-r--r-- | abstract/enum_domain_edd.ml | 2 | ||||
| -rw-r--r-- | main.ml | 29 |
7 files changed, 357 insertions, 182 deletions
@@ -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 @@ -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 |