diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 438 |
1 files changed, 329 insertions, 109 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index ebf7549..0dfc6f3 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -7,15 +7,12 @@ open Util open Num_domain open Abs_interp -let time id f = - Format.printf "%s[@?" id; - let r = f () in - Format.printf "] @?"; - r exception Top +exception Found_int of int + module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig val do_prog : cmdline_opt -> rooted_prog -> unit @@ -43,7 +40,7 @@ end = struct type edd = | DBot | DTop - | DVal of int + | DVal of int * bool (* bool : new case ? *) | DChoice of int * id * (item * edd) list type edd_v = { @@ -66,7 +63,7 @@ end = struct let key = function | DBot -> 0 | DTop -> 1 - | DVal i -> 2 * i + 2 + | DVal (i, _) -> 2 * i + 2 | DChoice(i, _, _) -> 2 * i + 3 let memo f = @@ -90,10 +87,43 @@ end = struct let edd_node_eq = function | DBot, DBot -> true | DTop, DTop -> true - | DVal i, DVal j when i = j -> true + | DVal (i, _), DVal (j, _) when i = j -> true | DChoice(i, _, _), DChoice(j, _, _) when i = j -> true | _ -> false + let new_node_fun () = + let nc = ref 0 in + let node_memo = Hashtbl.create 12 in + fun v l -> + let _, x0 = List.hd l in + if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l + then begin + let k = (v, List.map (fun (a, b) -> a, key b) l) in + let n = + try Hashtbl.find node_memo k + with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc) + in + DChoice(n, v, l) + end else x0 + + let get_leaf_fun_st () = + let leaves = Hashtbl.create 12 in + let lc = ref 0 in + let get_leaf st x = + if ND.is_top x then DTop else + if ND.is_bot x then DBot else + try + Hashtbl.iter (fun i v -> if ND.eq v x then raise (Found_int i)) leaves; + incr lc; + Hashtbl.add leaves !lc x; + DVal (!lc, st) + with Found_int i -> DVal (i, st) + in leaves, get_leaf + + let get_leaf_fun () = + let leaves, get_leaf = get_leaf_fun_st () in + leaves, get_leaf false + (* edd_print : Format.formatter -> edd_v -> unit *) @@ -115,11 +145,11 @@ end = struct let print_n fmt = function | DBot -> Format.fprintf fmt "⊥"; | DTop -> Format.fprintf fmt "⊤"; - | DVal i -> if i > !max_v then max_v := i; - Format.fprintf fmt "v%d" 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 in - Format.fprintf fmt "Root: %a@." print_n v.root; + Format.fprintf fmt "%a where:@." print_n v.root; for id = !max_n downto 0 do try match Hashtbl.find c_nodes id with @@ -180,46 +210,15 @@ end = struct { ve; root; leaves } (* - edd_join_meet : bool -> edd_v -> edd_v -> edd_v edd_join : edd_v -> edd_v -> edd_v edd_meet : edd_v -> edd_v -> edd_v *) - let edd_join_meet op a b = + let edd_join a b = let ve = a.ve in + let leaves, get_leaf = get_leaf_fun () in + let dq = new_node_fun () in - let leaves = Hashtbl.create 12 in - let lc = ref 0 in - - let get_leaf x = - if ND.is_top x then DTop else - if ND.is_bot x then DBot else begin - let id = ref None in - Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves; - match !id with - | Some i -> DVal i - | None -> - incr lc; - Hashtbl.add leaves !lc x; - DVal (!lc) - end - in - - let nc = ref 0 in - let node_memo = Hashtbl.create 12 in - let dq v l = - let _, x0 = List.hd l in - if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l - then begin - let k = (v, List.map (fun (a, b) -> a, key b) l) in - let n = - try Hashtbl.find node_memo k - with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc) - in - DChoice(n, v, l) - end else x0 - in - - let f_join f_rec na nb = + let f f_rec na nb = match na, nb with | DTop, _ | _, DTop -> DTop | DBot, DBot -> DBot @@ -240,11 +239,11 @@ end = struct in dq v kl - | DBot, DVal i -> + | DBot, DVal (i, _) -> get_leaf (Hashtbl.find b.leaves i) - | DVal i, DBot -> + | DVal (i, _), DBot -> get_leaf (Hashtbl.find a.leaves i) - | DVal u, DVal v -> + | DVal (u, _), DVal (v, _) -> let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in get_leaf x @@ -255,8 +254,14 @@ end = struct let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in dq vb kl in + { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) } - let f_meet f_rec na nb = + let edd_meet a b = + let ve = a.ve in + let leaves, get_leaf = get_leaf_fun () in + let dq = new_node_fun () in + + let f f_rec na nb = match na, nb with | DBot, _ | _, DBot -> DBot | DTop, DTop -> DTop @@ -277,11 +282,11 @@ end = struct in dq v kl - | DTop, DVal i -> + | DTop, DVal (i, _) -> get_leaf (Hashtbl.find b.leaves i) - | DVal i, DTop -> + | DVal (i, _), DTop -> get_leaf (Hashtbl.find a.leaves i) - | DVal u, DVal v -> + | DVal (u, _) , DVal (v, _) -> let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in get_leaf x @@ -292,14 +297,7 @@ end = struct let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in dq vb kl in - - if op then - { leaves; ve; root = time "join" (fun () -> memo2 f_join a.root b.root) } - else - { leaves; ve; root = time "meet" (fun () -> memo2 f_meet a.root b.root) } - - let edd_join = edd_join_meet true - let edd_meet = edd_join_meet false + { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) } @@ -310,33 +308,18 @@ end = struct let edd_num_apply v nfun = let ve = v.ve in - let lc = ref 0 in - let leaves = Hashtbl.create 12 in + let leaves, get_leaf = get_leaf_fun () in - let get_leaf x = - if ND.is_bot x then DBot else begin - let id = ref None in - Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves; - match !id with - | Some i -> DVal i - | None -> - incr lc; - Hashtbl.add leaves !lc x; - DVal (!lc) - end - in + let dq = new_node_fun () in let f f_rec n = match n with | DBot -> DBot | DTop -> get_leaf (nfun (ND.top ve.nvars)) - | DVal i -> get_leaf (nfun (Hashtbl.find v.leaves i)) + | DVal (i, _) -> get_leaf (nfun (Hashtbl.find v.leaves i)) | DChoice(n, var, l) -> let l = List.map (fun (k, v) -> k, f_rec v) l in - let _, x0 = List.hd l in - if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l - then DChoice(n, var, l) - else x0 + dq var l in { leaves; ve; root = memo f v.root } @@ -375,6 +358,25 @@ end = struct edd_join (edd_apply_cl v (eca, nc@nca, ra)) (edd_apply_cl v (ecb, nc@ncb, rb)) + + (* + edd_extract_path : edd_v -> id -> edd_v + *) + let edd_extract_path v leaf_id = + let ve = v.ve in + + let dq = new_node_fun () in + + let f f_rec n = + match n with + | DVal (i, _) when i = leaf_id -> DTop + | DChoice(n, var, l) -> + let l = List.map (fun (k, v) -> k, f_rec v) l in + dq var l + | _ -> DBot + in + { leaves = Hashtbl.create 1; ve; root = memo f v.root } + (* edd_eq : edd_v -> edd_v -> bool *) @@ -383,7 +385,7 @@ end = struct match na, nb with | DBot, DBot -> true | DTop, DTop -> true - | DVal i, DVal j -> + | DVal (i, _), DVal (j, _) -> ND.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j) | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb) @@ -398,23 +400,11 @@ end = struct let edd_forget_vars v vars = let ve = v.ve in - let leaves = Hashtbl.create 12 in - let lc = ref 0 in - - let get_leaf x = - let id = ref None in - Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves; - begin match !id with - | Some i -> DVal i - | None -> - incr lc; - Hashtbl.add leaves !lc x; - DVal (!lc) - end - in + let leaves, get_leaf = get_leaf_fun () in let nc = ref 0 in let memo = Hashtbl.create 12 in + let node_memo = Hashtbl.create 12 in let rec f l = let kl = List.sort Pervasives.compare (List.map key l) in try Hashtbl.find memo kl @@ -424,7 +414,7 @@ end = struct (fun (cn, fn) node -> match node with | DBot -> cn, fn | DTop -> raise Top - | DVal i -> cn, i::fn + | DVal (i, _) -> cn, i::fn | DChoice (n, v, l) -> (n, v, l)::cn, fn) ([], []) l in let cn = List.sort @@ -441,7 +431,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) fn in + let ch2 = List.map (fun i -> DVal (i, false)) fn in if List.mem dv vars then (* Do union of all branches branching from nodes on variable dv *) let ch3 = List.flatten @@ -458,7 +448,12 @@ end = struct let _, x0 = List.hd cc in if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) cc then begin - incr nc; DChoice(!nc, dv, cc) + let k = (dv, List.map (fun (a, b) -> a, key b) cc) in + let n = + try Hashtbl.find node_memo k + with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc) + in + DChoice(n, dv, cc) end else x0 with | Top -> DTop in Hashtbl.add memo kl r; r @@ -524,7 +519,134 @@ end = struct (* + edd_find_starred : edd_v -> int option + edd_unstar : edd_v -> int -> edd_v + *) + let edd_find_starred v = + let f f_rec = function + | DVal (i, true) -> raise (Found_int i) + | DChoice(_, _, l) -> List.iter (fun (_, x) -> f_rec x) l + | _ -> () + in + try memo f v.root; None + with Found_int i -> Some i + + 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) + | x -> x + in + { v with root = memo f v.root } + + + (* + edd_join_widen : edd_v -> edd_v -> edd_v + *) + let edd_join_widen (a:edd_v) (b:edd_v) = + let ve = a.ve in + let leaves, get_leaf = get_leaf_fun () in + let dq = new_node_fun () in + + let f f_rec na nb = + match na, nb with + | DTop, _ | _, DTop -> DTop + | DBot, DBot -> DBot + + | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> + let kl = List.map2 + (fun (ta, ba) (tb, bb) -> assert (ta = tb); + ta, f_rec ba bb) + la lb + in + dq va kl + | DChoice(_, va, la), DChoice(_, vb, lb) -> + let v, kl = + if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then + va, List.map (fun (k, ca) -> k, f_rec ca nb) la + else + vb, List.map (fun (k, cb) -> k, f_rec na cb) lb + in + dq v kl + + | DBot, DVal (i, _) -> + get_leaf (Hashtbl.find b.leaves i) + | DVal (i, _), DBot -> + get_leaf (Hashtbl.find a.leaves i) + | DVal (u, _), DVal (v, _) -> + let p1, p2 = edd_extract_path a u, edd_extract_path b v in + let widen = + if edd_eq p1 p2 then true else false + in + let x = (if widen then ND.widen else ND.join) + (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + get_leaf x + + | DChoice(_,va, la), _ -> + let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in + dq va kl + | _, DChoice(_, vb, lb) -> + let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in + dq vb kl + in + { leaves; ve; root = time "join/W" (fun () -> memo2 f a.root b.root) } + + (* + edd_join_star : edd_v -> edd_v -> edd_v + + Star in A all things that are in B and not in A. + *) + let edd_join_star (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 + + let f f_rec na nb = + match na, nb with + | DTop, _ | _, DTop -> DTop + | DBot, DBot -> DBot + + | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> + let kl = List.map2 + (fun (ta, ba) (tb, bb) -> assert (ta = tb); + ta, f_rec ba bb) + la lb + in + dq va kl + | DChoice(_, va, la), DChoice(_, vb, lb) -> + let v, kl = + if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then + va, List.map (fun (k, ca) -> k, f_rec ca nb) la + else + vb, List.map (fun (k, cb) -> k, f_rec na cb) lb + in + dq v kl + + | DBot, DVal (i, _) -> + get_leaf true (Hashtbl.find b.leaves i) + | DVal (i, s), DBot -> + get_leaf s (Hashtbl.find a.leaves i) + | DVal (u, s1), 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 + + | DChoice(_,va, la), _ -> + let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in + dq va kl + | _, DChoice(_, vb, lb) -> + let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in + dq vb kl + in + { leaves; ve; root = time "join/*" (fun () -> memo2 f a.root b.root) } + + (* pass_cycle : env -> edd_v -> edd_v + unpass_cycle : env -> edd_v -> edd_v *) let pass_cycle env v = let assign_e, assign_n = List.fold_left @@ -545,6 +667,28 @@ end = struct let v = edd_forget_vars v ef in edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf) + let unpass_cycle env v = + let assign_e, assign_n = List.fold_left + (fun (ae, an) (a, b, t) -> match t with + | TEnum _ -> (b, a)::ae, an + | TInt | TReal -> ae, (b, NIdent a)::an) + ([], []) env.cycle in + + let v = edd_eassign v assign_e in + let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in + + let ef, nf = List.fold_left + (fun (ef, nf) (_, var, t) -> + if var.[0] <> 'N' then + match t with + | TEnum _ -> var::ef, nf + | TReal | TInt -> ef, var::nf + else ef, nf) + ([], []) env.rp.all_vars in + + let v = edd_forget_vars v ef in + edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf) + (* extract_linked_evars : conslist -> (id * id) list @@ -700,7 +844,7 @@ 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 @@ scope_constrict evars ( lv1 ) in + let evars_ord = List.rev @@ time "SCA" (fun () -> scope_constrict evars ( lv1 )) in let ev_order = Hashtbl.create (List.length evars) in List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord; @@ -737,20 +881,69 @@ end = struct let do_prog opt rp = let e = init_env opt rp in - let rec f x = - Format.printf "Apply formula...@."; - let d2 = edd_apply_cl x e.cl in - Format.printf "Pass cycle...@."; - let dc = pass_cycle e d2 in - Format.printf "Join with init...@."; - let dcc = edd_join dc e.data in - Format.printf "@[<hov>%a@]@.@." edd_print dcc; - if not (edd_eq x dcc) then f dcc else dcc + + (* Do iterations until fixpoint is reached *) + let rec ch_it n x = + match edd_find_starred x with + | None -> + Format.printf "Chaotic iteration %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 + + if e.opt.verbose_ci then + Format.printf " -> %a@." edd_print y; + + if not (edd_eq x y) then ch_it (n+1) y else y + + | 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; + + let path_target = unpass_cycle e path in + let start = edd_meet path x in + + let f i = + let i = edd_meet path i in + let i' = edd_meet i path_target in + let q = edd_join start (pass_cycle e (edd_apply_cl i' e.cl)) in + edd_meet path q + in + + let rec iter n i = + let fi = f i in + let j = + if n < e.opt.widen_delay then + edd_join i fi + else + edd_join_widen i fi + in + if edd_eq i j then j else iter (n+1) j + in + let y = iter 0 start in + let z = fix edd_eq f y in + + + let j = pass_cycle e (edd_apply_cl z e.cl) in + let r = edd_join_star x j in + + if e.opt.verbose_ci then + Format.printf " -> %a@." edd_print r; + + ch_it (n+1) r in + + let init_acc = edd_join_star (edd_bot e.data.ve) e.data in - let final = edd_apply_cl (f e.data) e.cl in + (* Dump final state *) + let acc = ch_it 0 init_acc in + Format.printf "Finishing up...@."; + let final = edd_apply_cl acc e.cl in (*Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;*) + (* Check guarantees *) let check_guarantee (id, f) = let cl = Formula.conslist_of_f f in Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ " @@ -767,6 +960,33 @@ end = struct Format.printf "@]@." end; + (* Examine probes *) + if List.exists (fun (p, _, _) -> p) e.rp.all_vars then begin + let final_flat = edd_forget_vars final + (List.fold_left + (fun l (_, id, ty) -> match ty with + | TInt | TReal -> l + | TEnum _ -> id::l) + [] e.rp.all_vars) in + let final_flat = match final_flat.root with + | DTop -> ND.top e.ve.nvars + | DBot -> ND.bottom e.ve.nvars + | DVal(i, _) -> Hashtbl.find final_flat.leaves i + | DChoice _ -> assert false + in + + Format.printf "Probes: @[<v 0>"; + List.iter (fun (p, id, ty) -> + if p then match ty with + | TInt | TReal -> + Format.printf "%a ∊ %a@." Formula_printer.print_id id + ND.print_itv (ND.project final_flat id) + | TEnum _ -> Format.printf "%a : enum variable@." + Formula_printer.print_id id) + e.rp.all_vars; + Format.printf "@]@." + end + end |