diff options
| -rw-r--r-- | abstract/abs_interp_dynpart.ml | 179 | ||||
| -rw-r--r-- | abstract/formula.ml | 20 | ||||
| -rw-r--r-- | cmdline.ml | 5 | ||||
| -rw-r--r-- | main.ml | 9 |
4 files changed, 121 insertions, 92 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml index 1adc430..32ed890 100644 --- a/abstract/abs_interp_dynpart.ml +++ b/abstract/abs_interp_dynpart.ml @@ -21,9 +21,9 @@ end = struct type location = { id : int; + depth : int; - mutable def : bool_expr list; (* conjunction of formula *) - mutable def_cl : conslist; + mutable def : abs_v; is_init : bool; mutable f : bool_expr; @@ -108,22 +108,45 @@ end = struct 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) - | CLFalse -> - (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 - enum, num - | 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 + 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 - with Bot -> ED.vtop enum, ND.vbottom num + | CLFalse -> + (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 + enum, num + | 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 + end + + (* + apply_cl_all_cases : abs_v -> conslist -> abs_v 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] + | CLFalse -> + [] + | CLAnd(a, b) -> + let q1 = apply_cl_all_cases v (ec, nc, a) in + List.flatten + (List.map (fun c -> apply_cl_all_cases c ([], [], b)) q1) + | 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) (* *************************** @@ -190,17 +213,17 @@ end = struct loc = Hashtbl.create 2; counter = ref 2; } in (* add initial disjunction : L/must_reset = tt, L/must_reset ≠ tt *) - let rstc = [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] in - let rstf = simplify_k rstc f in + let rstc = BEnumCons(E_EQ, "L/must_reset", EItem bool_true) in + let rstf = simplify_k [rstc] f in let rstf = simplify_k (get_root_true rstf) rstf in - let nrstc = [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] in - let nrstf = simplify_k nrstc f in + let nrstc = BEnumCons(E_NE, "L/must_reset", EItem bool_true) in + let nrstf = simplify_k [nrstc] f in let nrstf = simplify_k (get_root_true nrstf) nrstf in Hashtbl.add env.loc 0 { id = 0; - def = rstc; - def_cl = conslist_of_f (f_and_list rstc); + depth = 0; + def = apply_cl (top env) (conslist_of_f rstc); is_init = true; f = rstf; @@ -215,8 +238,8 @@ end = struct Hashtbl.add env.loc 1 { id = 1; - def = nrstc; - def_cl = conslist_of_f (f_and_list nrstc); + depth = 0; + def = apply_cl (top env) (conslist_of_f nrstc); is_init = false; f = nrstf; @@ -282,23 +305,24 @@ end = struct (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf) - let set_target_case e v cl = - let tgt = (unpass_cycle e (apply_cl (top e) cl)) in - (*Format.printf "Target %a = %a@." Formula_printer.print_conslist cl print_v tgt;*) - meet v tgt - (* print_locs : env -> unit *) + let print_locs_defs e = + Hashtbl.iter + (fun id loc -> + Format.printf "q%d: @[<v 2>%a@]@." id print_v loc.def; + ) + e.loc + 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 "q%d (depth = %d):@. D: @[<v 2>%a@]@." id loc.depth print_v loc.def; (*Format.printf " F: (%a)@." Formula_printer.print_expr loc.f;*) - Format.printf " %a@." print_v loc.v; + Format.printf " V: %a@." print_v loc.v; Format.printf " -> @[<hov>[%a]@]@." (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t; ) @@ -325,7 +349,7 @@ end = struct loc.v <- bottom e) e.loc; - print_locs e; + print_locs_defs e; (* Iterate *) let it_counter = ref 0 in @@ -339,11 +363,11 @@ end = struct let start = loc.v in let f i = (*Format.printf "I: %a@." print_v i;*) - let i' = set_target_case e i loc.def_cl in + let i' = meet i (unpass_cycle e loc.def) in (*Format.printf "I': %a@." print_v i';*) let j = join start (apply_cl - (apply_cl (pass_cycle e.ve i') loc.def_cl) + (meet (pass_cycle e.ve i') loc.def) loc.cl) in (*Format.printf "J: %a@." print_v j;*) j @@ -372,7 +396,7 @@ end = struct Hashtbl.iter (fun t loc2 -> - let v = apply_cl u loc2.def_cl in + let v = 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 @@ -384,9 +408,9 @@ end = struct then loc.out_t <- t::loc.out_t; if not (subset_v w loc2.v) then begin if loc2.in_c < e.opt.widen_delay then - loc2.v <- join w loc2.v + loc2.v <- join loc2.v w else - loc2.v <- widen w loc2.v; + loc2.v <- widen loc2.v w; loc2.in_c <- loc2.in_c + 1; if not (List.mem t !delta) then delta := t::!delta @@ -438,10 +462,7 @@ end = struct then BNot cond else cond in - 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.def <- apply_cl loc.def (conslist_of_f tr); 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; @@ -453,31 +474,17 @@ end = struct (* find splitting condition *) Hashtbl.iter (fun q (loc:location) -> - if !qc = None then + if !qc = None && loc.depth < e.opt.max_dp_depth then let cs = ternary_conds loc.f in List.iter (fun c -> - let split_e_case_fold_aux cases c = - match c with - | 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.filter (op x) (List.assoc x e.ve.evars))) - @cases - | _ -> c::cases - in - let cases_t = - List.fold_left split_e_case_fold_aux [] - [c] in - let cases_f = - List.fold_left split_e_case_fold_aux [] - [eliminate_not_negate c] in + 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 = cases_t @ cases_f in if List.length (List.filter - (fun case -> - not (is_bot (apply_cl loc.v (conslist_of_f case)))) + (fun case -> not (is_bot (meet loc.v case))) cases) >= 2 && @@ -485,20 +492,20 @@ end = struct (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) + (meet (pass_cycle e.ve loci.v) loc.def) loc.cl in List.exists - (fun case -> is_bot (apply_cl v (conslist_of_f case))) + (fun case -> is_bot (meet v case)) cases) loc.in_t || List.exists (fun case -> - let v = apply_cl loc.v (conslist_of_f case) in + let v = meet loc.v 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) + (meet (pass_cycle e.ve v) loco.def) loco.cl in is_bot w) loc.out_t) @@ -510,27 +517,27 @@ end = struct ) e.loc; - (*if n < 7 then*) + if Hashtbl.length e.loc < e.opt.max_dp_width then match !qc with | None -> - Format.printf "@.Found no more possible refinement." + 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); + (print_list print_v ", ") (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 + if not (is_bot (meet loc.v 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)); + depth = loc.depth + 1; + def = meet loc.def case; f = ff; cl = conslist_of_f ff } in Hashtbl.add e.loc loc2.id loc2 @@ -539,6 +546,34 @@ end = struct List.iter (handle_case (BNot c)) cases_f; iter (n+1) - in iter 0 + in iter 0; + + (* Check guarantees *) + let check_guarantee (id, f) = + Format.printf "@[<v 4>"; + let cl = Formula.conslist_of_f f in + Format.printf "%s:@ %a ⇒ ⊥ @ " + id Formula_printer.print_conslist cl; + let violate = ref [] in + Hashtbl.iter + (fun id loc -> + if not (is_bot (apply_cl loc.v cl)) then + violate := id::!violate) + e.loc; + if !violate = [] then + Format.printf "OK" + else + Format.printf "VIOLATED in @[<hov 2>[ %a ]@]" + (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") !violate; + Format.printf "@]@ "; + in + if e.guarantees <> [] then begin + Format.printf "Guarantee @[<v 0>"; + List.iter check_guarantee e.guarantees; + Format.printf "@]@." + end + + + end diff --git a/abstract/formula.ml b/abstract/formula.ml index a124a84..f2a3bd1 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -263,23 +263,3 @@ 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 - | BTernary(c, a, b) -> - true, (BAnd(c, a))::(BAnd(BNot c, b))::l - | x -> u, x::l) - (false, []) c - in - if u then split_cases l else l @@ -2,7 +2,12 @@ open Ast type cmdline_opt = { widen_delay : int; + disjunct : (id -> bool); + verbose_ci : bool; vverbose_ci : bool; + + max_dp_width : int; + max_dp_depth : int; } @@ -47,6 +47,8 @@ let ai_widen_delay = ref 5 let ai_no_time_scopes = ref "all" let ai_init_scopes = ref "all" let ai_disj_v = ref "" +let ai_max_dp_depth = ref 10 +let ai_max_dp_width = ref 100 let ai_vci = ref false let ai_vvci = ref false let ifile = ref "" @@ -91,6 +93,11 @@ let options = [ "--ai-wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3)."; + "--ai-max-dp-depth", Arg.Set_int ai_max_dp_depth, + "Maximum depth in the dynamic partitionning tree."; + "--ai-max-dp-width", Arg.Set_int ai_max_dp_width, + "Maximum number of dynamically partitionned locations."; + "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test)."; "--no-time", Arg.Set_string ai_no_time_scopes, @@ -178,6 +185,8 @@ let () = disjunct = disj; verbose_ci = !ai_vci; vverbose_ci = !ai_vvci; + max_dp_width = !ai_max_dp_width; + max_dp_depth = !ai_max_dp_depth; } in if !ai_itv then AI_Itv.do_prog opt rp; |