diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp_dynpart.ml | 237 | ||||
| -rw-r--r-- | abstract/formula.ml | 18 |
2 files changed, 213 insertions, 42 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml index 28f9238..c47fdc7 100644 --- a/abstract/abs_interp_dynpart.ml +++ b/abstract/abs_interp_dynpart.ml @@ -20,22 +20,21 @@ end = struct type abs_v = ED.t * ND.t type location = { - id : int; + id : int; - def : bool_expr list; (* conjunction of formula *) - def_cl : conslist; - is_init : bool; + mutable def : bool_expr list; (* conjunction of formula *) + mutable def_cl : conslist; + is_init : bool; - f : bool_expr; - cl : conslist; + mutable f : bool_expr; + mutable cl : conslist; (* For chaotic iteration fixpoint *) - mutable star : bool; - mutable in_c : int; - mutable v : abs_v; + mutable in_c : int; + mutable v : abs_v; - mutable out_t : int list; - mutable in_t : int list; + mutable out_t : int list; + mutable in_t : int list; } type env = { @@ -69,16 +68,23 @@ end = struct if is_bot (enum, num) then Format.fprintf fmt "⊥" else - Format.fprintf fmt "@[<hov 4>(%a,@ %a)@]" ED.print enum ND.print num + 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 (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 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 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 @@ -87,13 +93,26 @@ end = struct with Bot -> 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 subset_v (a, b) (c, d) = + ND.is_bot b || + (not (ND.is_bot 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) = try begin match r with | CLTrue -> - (ED.apply_cl enum ec, ND.apply_cl num nc) + let enum = + fix ED.eq (fun v -> ED.apply_cl v ec) enum + in + (enum, ND.apply_cl num nc) | CLFalse -> (enum, ND.vbottom num) | CLAnd(a, b) -> @@ -188,7 +207,6 @@ end = struct f = rstf; cl = conslist_of_f rstf; - star = false; in_c = 0; v = (ED.top ve.evars, ND.bottom ve.nvars); @@ -205,7 +223,6 @@ end = struct f = nrstf; cl = conslist_of_f nrstf; - star = false; in_c = 0; v = (ED.top ve.evars, ND.bottom ve.nvars); @@ -216,6 +233,14 @@ end = struct (* + ternary_conds : bool_expr -> bool_expr list + *) + let rec ternary_conds = function + | BAnd(a, b) -> ternary_conds a @ ternary_conds b + | BTernary(c, a, b) -> [c] + | _ -> [] + + (* pass_cycle : env -> edd_v -> edd_v unpass_cycle : env -> edd_v -> edd_v @@ -276,6 +301,7 @@ end = struct (fun q loc -> loc.out_t <- []; loc.in_t <- []; + loc.in_c <- 0; if loc.is_init then begin loc.v <- apply_cl (top e) loc.cl; delta := q::!delta @@ -302,24 +328,21 @@ end = struct j in - let rec iter n (i_enum, i_num) = - let fi_enum, fi_num = f (i_enum, i_num) in - let j_enum, j_num = - if ND.is_bot fi_num then - i_enum, i_num - else + let rec iter n i = + let fi = f i in + let j = if n < e.opt.widen_delay then - ED.join i_enum fi_enum, ND.join i_num fi_num + join i fi else - ED.join i_enum fi_enum, ND.widen i_num fi_num + widen i fi in - if ED.eq j_enum i_enum && ND.eq j_num i_num - then (i_enum, i_num) - else iter (n+1) (j_enum, j_num) + if eq_v i j + then i + else iter (n+1) j in let y = iter 0 start in - let z = fix (fun (a, b) (c, d) -> ED.eq a c && ND.eq b d) f y in - Format.printf "Fixpoint: %a@." print_v z; + let z = fix eq_v f y in + (*Format.printf "Fixpoint: %a@." print_v z;*) loc.v <- z; @@ -331,16 +354,17 @@ end = struct (*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); + (*Format.printf "%d -> %d with:@. %a@." s t print_v (r_enum, r_num);*) 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; - let enum, num = loc2.v in - let enum2, num2 = join (enum, num) (r_enum, r_num) in - if not (ED.subset enum2 enum) || not (ND.subset num2 num) then - begin - loc2.v <- (enum2, num2); + if not (subset_v (r_enum, r_num) loc2.v) then begin + if loc2.in_c < e.opt.widen_delay then + loc2.v <- join (r_enum, r_num) loc2.v + else + loc2.v <- widen (r_enum, r_num) loc2.v; + loc2.in_c <- loc2.in_c + 1; if not (List.mem t !delta) then delta := t::!delta end @@ -348,18 +372,28 @@ end = struct e.loc; delta := List.filter ((<>) s) !delta; - done + done; + + (* remove useless locations *) + let useless = ref [] in + Hashtbl.iter + (fun i loc -> + if is_bot loc.v then begin + Format.printf "Useless location detected: q%d@." i; + useless := i::!useless + end) + e.loc; + List.iter (Hashtbl.remove e.loc) !useless let print_locs e = Hashtbl.iter (fun id loc -> Format.printf "@."; - Format.printf "q%d: @[<hov 4>[ %a ]@]@." id + Format.printf "q%d: @[<v 2>[ %a ]@]@." id (print_list Formula_printer.print_expr " ∧ ") loc.def; - (*Format.printf "F: %a@." Formula_printer.print_conslist loc.cl;*) - Format.printf " @[<hv 0>%a ∧@ %a@]@." - ED.print (fst loc.v) ND.print (snd loc.v); + (*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; ) @@ -368,8 +402,127 @@ end = struct let do_prog opt rp = let e = init_env opt rp in - Format.printf "@.Initializing.@."; - chaotic_iter e; - print_locs e + let rec iter n = + Format.printf "@.--------------@.Refinement #%d@." n; + + chaotic_iter e; + print_locs e; + + let qc = ref None in + + (* put true or false conditions into location definition *) + Hashtbl.iter + (fun q (loc : location) -> + let rec iter () = + 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)))) + (ternary_conds loc.f) + in + let tr = + if is_bot (apply_cl loc.v (conslist_of_f cond)) + then BNot cond + else cond + in + loc.def <- tr::loc.def; + loc.def_cl <- conslist_of_f (f_and_list loc.def); + 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; + iter() + with Not_found -> () + in iter ()) + e.loc; + + (* find splitting condition *) + Hashtbl.iter + (fun q (loc:location) -> + if !qc = None then + let cs = ternary_conds loc.f in + List.iter + (fun c -> + let split_e_case_fold_aux cases c = + match c with + | BEnumCons(_, x, EItem _) -> + (List.map (fun v -> BEnumCons(E_EQ, x, EItem v)) + (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 + let cases_f = + List.fold_left split_e_case_fold_aux [] + (split_cases [BNot c]) in + let cases = cases_t @ cases_f in + if + List.length + (List.filter + (fun case -> + not (is_bot (apply_cl loc.v (conslist_of_f case)))) + cases) + >= 2 + && + (List.exists + (fun qi -> + let loci = Hashtbl.find e.loc qi in + let v = apply_cl + (apply_cl (pass_cycle e.ve loci.v) loc.def_cl) + loc.cl in + List.exists + (fun case -> is_bot (apply_cl v (conslist_of_f case))) + cases) + loc.in_t + || List.exists + (fun case -> + let v = apply_cl loc.v (conslist_of_f case) in + List.exists + (fun qo -> + let loco = Hashtbl.find e.loc qo in + let w = apply_cl + (apply_cl (pass_cycle e.ve v) loco.def_cl) + loco.cl in + is_bot w) + loc.out_t) + cases) + then + qc := Some(q, c, cases_t, cases_f) + ) + cs + ) + e.loc; + + (*if n < 7 then*) + match !qc with + | None -> + Format.printf "@.Found no more possible refinement." + | Some (q, c, cases_t, cases_f) -> + Format.printf "@.Refine q%d : @[<v 2>[ %a ]@]@." q + (print_list Formula_printer.print_expr ", ") (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 (apply_cl loc.v (conslist_of_f case))) then + let ff = simplify_k [cc] loc.f in + let ff = simplify_k (get_root_true ff) ff in + + let loc2 = + { loc with + id = (incr e.counter; !(e.counter)); + def = case::loc.def; + def_cl = conslist_of_f (f_and_list (case::loc.def)); + f = ff; + cl = conslist_of_f ff } in + Hashtbl.add e.loc loc2.id loc2 + in + List.iter (handle_case c) cases_t; + List.iter (handle_case (BNot c)) cases_f; + + iter (n+1) + in iter 0 end diff --git a/abstract/formula.ml b/abstract/formula.ml index f2a3bd1..5cbe0c9 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -263,3 +263,21 @@ let rec formula_replace_evars repls e = | x -> x + +(* + Extract all cases that make a formula true, to a limited degree + + [A || B; not (A || B)] -> A; (B && (not A)); not A && not B] +*) + +let rec split_cases c = + let c = List.map eliminate_not c in + let u, l = List.fold_left + (fun (u, l) c -> + match c with + | BOr(a, b) -> + true, a::(BAnd(BNot a, b))::l + | x -> u, x::l) + (false, []) c + in + if u then split_cases l else l |