From 93d924bb1017dc26a9735801e1b7f8b7a3f4ef2c Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 30 Jul 2014 15:45:28 +0200 Subject: Refactor some stuff (this code sould be re-read.) --- abstract/abs_interp_dynpart.ml | 207 ++++++++++++++--------------------------- 1 file changed, 69 insertions(+), 138 deletions(-) (limited to 'abstract/abs_interp_dynpart.ml') 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 "@[(%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: @[%a@]@." id print_v loc.def; + Format.printf "q%d: @[%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: @[%a@]@." id loc.depth print_v loc.def; + Format.printf "q%d (depth = %d):@. D: @[%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 " -> @[[%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 : @[[ %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: @["; 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; -- cgit v1.2.3