summaryrefslogtreecommitdiff
path: root/abstract/abs_interp_edd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/abs_interp_edd.ml')
-rw-r--r--abstract/abs_interp_edd.ml141
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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-19 16:42:50 +0000