diff options
Diffstat (limited to 'abstract/abs_interp_dynpart.ml')
| -rw-r--r-- | abstract/abs_interp_dynpart.ml | 110 |
1 files changed, 63 insertions, 47 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml index c47fdc7..1adc430 100644 --- a/abstract/abs_interp_dynpart.ml +++ b/abstract/abs_interp_dynpart.ml @@ -62,7 +62,7 @@ end = struct *) 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) = ND.is_bot n + 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 @@ -75,32 +75,34 @@ end = struct widen : abs_v -> abs_v -> abs_v meet : abs_v -> abs_v -> abs_v *) - let join (e1, n1) (e2, n2) = - if is_bot (e1, n1) then (e2, n2) - else if is_bot (e2, n2) then (e1, n1) - else (ED.join e1 e2, ND.join n1 n2) + 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 (e1, n1) (e2, n2) = - if is_bot (e1, n1) then (e2, n2) - else if is_bot (e2, n2) then (e1, n1) - else (ED.join e1 e2, ND.widen n1 n2) + 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 -> e1, ND.vbottom n1 + with Bot -> ED.vtop e1, ND.vbottom n1 (* eq_v : abs_v -> abs_v -> bool subset_v : abs_v -> abs_v -> bool *) - let eq_v (a, b) (c, d) = (ND.is_bot b && ND.is_bot d) || (ED.eq a c && ND.eq b d) + 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) = - ND.is_bot b || - (not (ND.is_bot d) && ED.subset a c && ND.subset b 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 @@ -109,12 +111,9 @@ end = struct try begin match r with | CLTrue -> - let enum = - fix ED.eq (fun v -> ED.apply_cl v ec) enum - in - (enum, ND.apply_cl num nc) + (ED.apply_cl enum ec, ND.apply_cl num nc) | CLFalse -> - (enum, ND.vbottom num) + (ED.vtop enum, ND.vbottom num) | CLAnd(a, b) -> let enum, num = apply_cl (enum, num) (ec, nc, a) in let enum, num = apply_cl (enum, num) ([], nc, b) in @@ -289,6 +288,23 @@ end = struct meet v tgt (* + print_locs : env -> unit + *) + + let print_locs e = + Hashtbl.iter + (fun id loc -> + Format.printf "@."; + Format.printf "q%d: @[<v 2>[ %a ]@]@." id + (print_list Formula_printer.print_expr " ∧ ") loc.def; + (*Format.printf " F: (%a)@." Formula_printer.print_expr loc.f;*) + Format.printf " %a@." print_v loc.v; + Format.printf " -> @[<hov>[%a]@]@." + (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t; + ) + e.loc + + (* chaotic_iter : env -> unit Fills the values of loc[*].v, and updates out_t and in_t @@ -309,6 +325,8 @@ end = struct loc.v <- bottom e) e.loc; + print_locs e; + (* Iterate *) let it_counter = ref 0 in while !delta <> [] do @@ -323,7 +341,10 @@ end = struct (*Format.printf "I: %a@." print_v i;*) let i' = set_target_case e i loc.def_cl in (*Format.printf "I': %a@." print_v i';*) - let j = join start (apply_cl (apply_cl (pass_cycle e.ve i') loc.def_cl) loc.cl) in + let j = join start + (apply_cl + (apply_cl (pass_cycle e.ve i') loc.def_cl) + loc.cl) in (*Format.printf "J: %a@." print_v j;*) j in @@ -342,28 +363,30 @@ end = struct in let y = iter 0 start in let z = fix eq_v f y in - (*Format.printf "Fixpoint: %a@." print_v z;*) + 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; loc.v <- z; Hashtbl.iter (fun t loc2 -> - let u = pass_cycle e.ve z in let v = apply_cl u loc2.def_cl 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;*) - let r_enum, r_num = w in - if not (is_bot (r_enum, r_num)) then begin - (*Format.printf "%d -> %d with:@. %a@." s t print_v (r_enum, r_num);*) + if not (is_bot w) then begin + if e.opt.verbose_ci then + Format.printf "%d -> %d with:@. %a@." s t print_v 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 (r_enum, r_num) loc2.v) then begin + if not (subset_v w loc2.v) then begin if loc2.in_c < e.opt.widen_delay then - loc2.v <- join (r_enum, r_num) loc2.v + loc2.v <- join w loc2.v else - loc2.v <- widen (r_enum, r_num) loc2.v; + loc2.v <- widen w loc2.v; loc2.in_c <- loc2.in_c + 1; if not (List.mem t !delta) then delta := t::!delta @@ -383,21 +406,11 @@ end = struct useless := i::!useless end) e.loc; - List.iter (Hashtbl.remove e.loc) !useless + List.iter (Hashtbl.remove e.loc) !useless; + + print_locs e - let print_locs e = - Hashtbl.iter - (fun id loc -> - Format.printf "@."; - Format.printf "q%d: @[<v 2>[ %a ]@]@." id - (print_list Formula_printer.print_expr " ∧ ") loc.def; - (*Format.printf " F: (%a)@." Formula_printer.print_expr loc.f;*) - Format.printf " %a@." print_v loc.v; - Format.printf " -> @[<hov>[%a]@]@." - (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t; - ) - e.loc let do_prog opt rp = let e = init_env opt rp in @@ -406,7 +419,6 @@ end = struct Format.printf "@.--------------@.Refinement #%d@." n; chaotic_iter e; - print_locs e; let qc = ref None in @@ -426,8 +438,10 @@ end = struct then BNot cond else cond in - loc.def <- tr::loc.def; - loc.def_cl <- conslist_of_f (f_and_list loc.def); + if not (List.mem tr loc.def) then begin + loc.def <- tr::loc.def; + loc.def_cl <- conslist_of_f (f_and_list loc.def); + end; loc.f <- simplify_k [tr] loc.f; loc.f <- simplify_k (get_root_true loc.f) loc.f; loc.cl <- conslist_of_f loc.f; @@ -445,17 +459,19 @@ end = struct (fun c -> let split_e_case_fold_aux cases c = match c with - | BEnumCons(_, x, EItem _) -> + | BEnumCons(op, x, EItem _) -> + let op = match op with | E_EQ -> (=) | E_NE -> (<>) in (List.map (fun v -> BEnumCons(E_EQ, x, EItem v)) - (List.assoc x e.ve.evars))@cases + (List.filter (op x) (List.assoc x e.ve.evars))) + @cases | _ -> c::cases in let cases_t = List.fold_left split_e_case_fold_aux [] - (split_cases [c]) in + [c] in let cases_f = List.fold_left split_e_case_fold_aux [] - (split_cases [BNot c]) in + [eliminate_not_negate c] in let cases = cases_t @ cases_f in if List.length |