diff options
Diffstat (limited to 'abstract')
-rw-r--r-- | abstract/abs_interp_edd.ml | 141 |
1 files changed, 98 insertions, 43 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 0dfc6f3..5b3b0ec 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -40,7 +40,7 @@ end = struct type edd = | DBot | DTop - | DVal of int * bool (* bool : new case ? *) + | DVal of int * (bool * int) (* bool*int : new case ? iterations before widen ? *) | DChoice of int * id * (item * edd) list type edd_v = { @@ -122,7 +122,7 @@ end = struct let get_leaf_fun () = let leaves, get_leaf = get_leaf_fun_st () in - leaves, get_leaf false + leaves, get_leaf (false, 0) (* edd_print : Format.formatter -> edd_v -> unit @@ -131,35 +131,62 @@ end = struct let max_n = ref 0 in let max_v = ref 0 in - let c_nodes = Hashtbl.create 12 in - let rec add = function - | DChoice(n, _, l) as x -> - if not (Hashtbl.mem c_nodes n) then begin - if n > !max_n then max_n := n; - Hashtbl.add c_nodes n x; - List.iter (fun (_, y) -> add y) l - end - | _ -> () - in add v.root; - - let print_n fmt = function + let print_nodes = Queue.create () in + let a = Hashtbl.create 12 in + + let node_pc = Hashtbl.create 12 in + let f f_rec = function + | DChoice(_, _, l) -> + List.iter + (fun (_, c) -> match c with + | DChoice(n, _, _) -> + begin try Hashtbl.add node_pc n (Hashtbl.find node_pc n + 1) + with Not_found -> Hashtbl.add node_pc n 1 end + | _ -> ()) + l; + List.iter (fun (_, c) -> f_rec c) l + | _ -> () + in memo f v.root; + + let rec print_n fmt = function | DBot -> Format.fprintf fmt "⊥"; | DTop -> Format.fprintf fmt "⊤"; - | DVal (i, s) -> if i > !max_v then max_v := i; + | DVal (i, (s, _)) -> if i > !max_v then max_v := i; Format.fprintf fmt "v%d%s" i (if s then "*" else ""); - | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n + | DChoice(_, v, l) -> + match List.filter (fun (_, x) -> x <> DBot) l with + | [(c, nn)] -> + let aux fmt = function + | DChoice(nn, _, _) as i when Hashtbl.find node_pc nn >= 2 -> + if Hashtbl.mem a nn then () else begin + Queue.push i print_nodes; + Hashtbl.add a nn () + end; + Format.fprintf fmt "n%d" nn + | x -> print_n fmt x + in + Format.fprintf fmt "%a = %s,@ %a" Formula_printer.print_id v c aux nn + | _ -> + Format.fprintf fmt "%a ? " Formula_printer.print_id v; + let print_u fmt (c, i) = + Format.fprintf fmt "%s → " c; + match i with + | DChoice(nn, v, l) -> + if Hashtbl.mem a nn then () else begin + Queue.push i print_nodes; + Hashtbl.add a nn () + end; + Format.fprintf fmt "n%d" nn + | _ -> Format.fprintf fmt "%a" print_n i + in + Format.fprintf fmt "@[<h>%a@]" (print_list print_u ", ") l; in - Format.fprintf fmt "%a where:@." print_n v.root; - - for id = !max_n downto 0 do - try match Hashtbl.find c_nodes id with - | DChoice (_, var, l) -> - let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in - Format.fprintf fmt "n%d: %a ? @[<hov>%a@]@." - id Formula_printer.print_id var - (print_list p ", ") l - | _ -> assert false - with Not_found -> () + Format.fprintf fmt "@[<hov>%a@]@." print_n v.root; + while not (Queue.is_empty print_nodes) do + match Queue.pop print_nodes with + | DChoice(n, v, l) as x -> + Format.fprintf fmt "n%d: @[<hov>%a@]@." n print_n x + | _ -> assert false done; for id = 0 to !max_v do @@ -168,6 +195,29 @@ end = struct with Not_found -> () done + let edd_dump_graphviz v file = + let o = open_out file in + let fmt = Format.formatter_of_out_channel o in + Format.fprintf fmt "digraph G {@[<v 4>@,"; + + let f f_rec = function + | DChoice(n, v, x) -> + let aux fmt = function + | DBot -> Format.fprintf fmt "bot" + | DTop -> Format.fprintf fmt "top" + | DVal(i, _) -> Format.fprintf fmt "v%d" i + | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n + in + Format.fprintf fmt "n%d [label=\"%s\"];@ " n v; + List.iter (fun (i, c) -> + if c <> DBot then Format.fprintf fmt "n%d -> %a [label=\"%s\"];@ " n aux c i; + f_rec c) x + | _ -> () + in memo f v.root; + Format.fprintf fmt "@]}@."; + + close_out o + (* edd_bot : varenv -> edd_v @@ -431,7 +481,7 @@ end = struct let _, dv, cl = List.hd cn in let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in let ch1 = List.map (fun (a, b, c) -> DChoice(a, b, c)) nd in - let ch2 = List.map (fun i -> DVal (i, false)) fn in + let ch2 = List.map (fun i -> DVal (i, (false, 0))) fn in if List.mem dv vars then (* Do union of all branches branching from nodes on variable dv *) let ch3 = List.flatten @@ -524,7 +574,7 @@ end = struct *) let edd_find_starred v = let f f_rec = function - | DVal (i, true) -> raise (Found_int i) + | DVal (i, (true, _)) -> raise (Found_int i) | DChoice(_, _, l) -> List.iter (fun (_, x) -> f_rec x) l | _ -> () in @@ -534,7 +584,7 @@ end = struct let edd_unstar v i = let f f_rec = function | DChoice(a, b, l) -> DChoice(a, b, List.map (fun (c, x) -> c, f_rec x) l) - | DVal(j, n) when i = j -> DVal(i, false) + | DVal(j, (s, n)) when i = j -> DVal(i, (false, n)) | x -> x in { v with root = memo f v.root } @@ -596,7 +646,7 @@ end = struct Star in A all things that are in B and not in A. *) - let edd_join_star (a:edd_v) (b:edd_v) = + let edd_join_star_widen env (a:edd_v) (b:edd_v) = let ve = a.ve in let leaves, get_leaf = get_leaf_fun_st () in let dq = new_node_fun () in @@ -623,17 +673,18 @@ end = struct dq v kl | DBot, DVal (i, _) -> - get_leaf true (Hashtbl.find b.leaves i) + get_leaf (true, 0) (Hashtbl.find b.leaves i) | DVal (i, s), DBot -> get_leaf s (Hashtbl.find a.leaves i) - | DVal (u, s1), DVal (v, _) -> + | DVal (u, (s1, i1)), DVal (v, _) -> 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 star = s1 || not (edd_eq p1 p2) || not (ND.subset d2 d1) in - let x = ND.join d1 d2 in - get_leaf star x + 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 + get_leaf (star, i1 + 1) x | DChoice(_,va, la), _ -> let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in @@ -834,8 +885,6 @@ end = struct (* calculate order for enumerated variables *) let evars = List.map fst enum_vars in - let lv0 = List.map (fun x -> x, "N"^x) - (List.filter (fun x -> List.exists (fun y -> y = "N"^x) evars) evars) in let lv1 = extract_linked_evars_root init_cl @ extract_linked_evars_root cl_g in let lv2 = extract_linked_evars init_cl @ extract_linked_evars cl_g in @@ -844,7 +893,10 @@ end = struct (List.sort Pervasives.compare (List.map ord_couple lv1)) in let lv2 = uniq_sorted (List.sort Pervasives.compare (List.map ord_couple lv2)) in - let evars_ord = List.rev @@ time "SCA" (fun () -> scope_constrict evars ( lv1 )) in + let evars_ord = time "SCA" (fun () -> scope_constrict evars ( lv1 )) in + let va, vb = List.partition (fun n -> is_suffix n "init") evars_ord in + let vb, vc = List.partition (fun n -> is_suffix n "state") vb in + let evars_ord = (List.rev va) @ vb @ vc in let ev_order = Hashtbl.create (List.length evars) in List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord; @@ -884,13 +936,14 @@ end = struct (* Do iterations until fixpoint is reached *) let rec ch_it n x = + edd_dump_graphviz x (Format.sprintf "/tmp/graph-it%d.dot" n); match edd_find_starred x with | None -> - Format.printf "Chaotic iteration %d : full iteration.@." n; + Format.printf "It. %d : full iteration.@." n; let d2 = edd_apply_cl x e.cl in let dc = pass_cycle e d2 in - let y = edd_join_star x dc in + let y = edd_join_star_widen e x dc in if e.opt.verbose_ci then Format.printf " -> %a@." edd_print y; @@ -900,7 +953,7 @@ end = struct | Some i -> let path = edd_extract_path x i in let x = edd_unstar x i in - Format.printf "Chaotic iteration %d: @[<hov>%a@]@." n edd_print path; + Format.printf "It. %d: @[<hov>%a@]@." n edd_print path; let path_target = unpass_cycle e path in let start = edd_meet path x in @@ -927,7 +980,7 @@ end = struct let j = pass_cycle e (edd_apply_cl z e.cl) in - let r = edd_join_star x j in + let r = edd_join_star_widen e x j in if e.opt.verbose_ci then Format.printf " -> %a@." edd_print r; @@ -935,12 +988,14 @@ end = struct ch_it (n+1) r in - let init_acc = edd_join_star (edd_bot e.data.ve) e.data in + let init_acc = edd_join_star_widen e (edd_bot e.data.ve) e.data in (* Dump final state *) let acc = ch_it 0 init_acc in + edd_dump_graphviz acc "/tmp/graph-final0.dot"; Format.printf "Finishing up...@."; let final = edd_apply_cl acc e.cl in + edd_dump_graphviz final "/tmp/graph-final.dot"; (*Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;*) (* Check guarantees *) |