From bc679afc4ac59c256a1b5f200078e495c188d066 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 2 Jul 2014 16:24:12 +0200 Subject: Fix non-termination issue in EDDs --- abstract/abs_interp.ml | 18 +++--- abstract/abs_interp_edd.ml | 147 +++++++++++++++++++++++++-------------------- 2 files changed, 90 insertions(+), 75 deletions(-) (limited to 'abstract') diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index c3b2d79..0db128f 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -174,9 +174,7 @@ end = struct num_vars : (id * bool) list; (* program expressions *) - f : bool_expr; cl : conslist; - f_g : bool_expr; cl_g : conslist; guarantees : (id * bool_expr) list; @@ -237,14 +235,12 @@ end = struct (print_list Ast_printer.print_typed_var ", ") rp.all_vars; - let enum_vars = List.fold_left - (fun v (_, id, t) -> match t with - | TEnum ch -> (id, ch)::v | _ -> v) - [] rp.all_vars in - let num_vars = List.fold_left - (fun v (_, id, t) -> match t with - | TInt -> (id, false)::v | TReal -> (id, true)::v | _ -> v) - [] rp.all_vars in + let num_vars, enum_vars = List.fold_left + (fun (nv, ev) (_, id, t) -> match t with + | TEnum ch -> nv, (id, ch)::ev + | TInt -> (id, false)::nv, ev + | TReal -> (id, true)::nv, ev) + ([], []) rp.all_vars in let init_f = Transform.init_f_of_prog rp in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; @@ -317,7 +313,7 @@ end = struct let st = { rp; opt; enum_vars; num_vars; - f; cl; f_g; cl_g; guarantees; + cl; cl_g; guarantees; cycle; forget; d_vars; top; env; delta; widen } in diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 6e45240..cdcdab2 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -125,6 +125,11 @@ end = struct let leaves, get_leaf = get_leaf_fun_st () in leaves, get_leaf (false, 0) + let rank ve = function + | DChoice(_, x, _) -> Hashtbl.find ve.ev_order x + | _ -> 10000000 (* HYPOTHESIS : program will never have more than + that number of variables *) + (* edd_print : Format.formatter -> edd_v -> unit *) @@ -288,22 +293,14 @@ end = struct 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 | DTop, _ | _, DTop -> DTop | DBot, DBot -> DBot - | DChoice(_,va, la), _ -> + | DChoice(_,va, la), _ when rank ve na < rank ve nb -> let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in dq va kl - | _, DChoice(_, vb, lb) -> + | _, DChoice(_, vb, lb) when rank ve nb < rank ve na -> let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in dq vb kl @@ -314,6 +311,8 @@ end = struct get_leaf (Hashtbl.find a.leaves u) | DBot, DVal(v, _) -> get_leaf (Hashtbl.find b.leaves v) + + | _ -> assert false (* so that OCaml won't complain ; all cases ARE handled *) in { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) } @@ -331,22 +330,14 @@ end = struct 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, _ | _, DBot -> DBot | DTop, DTop -> DTop - | DChoice(_, va, la), _ -> + | DChoice(_, va, la), _ when rank ve na < rank ve nb -> let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in dq va kl - | _, DChoice(_, vb, lb) -> + | _, DChoice(_, vb, lb) when rank ve nb < rank ve na -> let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in dq vb kl @@ -357,6 +348,8 @@ end = struct get_leaf (Hashtbl.find a.leaves u) | DTop, DVal(v, _) -> get_leaf (Hashtbl.find b.leaves v) + + | _ -> assert false (* see above *) in { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) } @@ -455,6 +448,33 @@ end = struct in memo2 f a.root b.root + (* + edd_subset : edd_v -> edd_v -> bool + *) + let edd_subset a b = + let rank = rank a.ve in + let f f_rec na nb = + match na, nb with + | DBot, _ -> true + | _, DTop -> true + | DTop, DBot -> false + + | DVal(i, _), DBot -> ND.is_bot (Hashtbl.find a.leaves i) + | DTop, DVal(i, _) -> ND.is_top (Hashtbl.find b.leaves i) + + | DVal(i, _), DVal(j, _) -> + ND.subset (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) + la lb + | DChoice(_, va, la), _ when rank na < rank nb -> + List.for_all (fun (c, n) -> f_rec n nb) la + | _, DChoice(_, vb, lb) when rank na > rank nb -> + List.for_all (fun (c, n) -> f_rec na n) lb + | _ -> assert false + in memo2 f a.root b.root + (* edd_forget_vars : edd_v -> id list -> edd_v *) @@ -566,9 +586,7 @@ end = struct ve : varenv; (* program expressions *) - f : bool_expr; cl : conslist; - f_g : bool_expr; cl_g : conslist; guarantees : (id * bool_expr) list; @@ -604,7 +622,7 @@ end = struct (* edd_join_widen : edd_v -> edd_v -> edd_v *) - let edd_join_widen (a:edd_v) (b:edd_v) = + let edd_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 @@ -621,14 +639,6 @@ end = struct 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) @@ -643,21 +653,23 @@ end = struct (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in get_leaf x - | DChoice(_,va, la), _ -> + | DChoice(_,va, la), _ when rank ve na < rank ve nb -> let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in dq va kl - | _, DChoice(_, vb, lb) -> + | _, DChoice(_, vb, lb) when rank ve nb < rank ve na -> let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in dq vb kl + + | _ -> assert false in { leaves; ve; root = time "join/W" (fun () -> memo2 f a.root b.root) } (* - edd_join_star : edd_v -> edd_v -> edd_v + edd_accumulate : edd_v -> edd_v -> edd_v - Star in A all things that are in B and not in A. + Sometimes do global widening. *) - let edd_join_star_widen env (a:edd_v) (b:edd_v) = + let edd_accumulate 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 @@ -674,14 +686,6 @@ end = struct 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, 0) (Hashtbl.find b.leaves i) @@ -690,22 +694,38 @@ end = struct | 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 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 + get_leaf (s1, i1 + 1) x - | DChoice(_,va, la), _ -> + | DChoice(_,va, la), _ when rank ve na < rank ve nb -> let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in dq va kl - | _, DChoice(_, vb, lb) -> + | _, DChoice(_, vb, lb) when rank ve nb < rank ve na -> let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in dq vb kl + + | _ -> assert false in { leaves; ve; root = time "join/*" (fun () -> memo2 f a.root b.root) } + (* + edd_star_new : edd_v -> edd_v -> edd_v + + Star in s leaves that were not present in s0 + *) + let edd_star_new s0 s = + let f f_rec = function + | DChoice(n, x, l) -> + DChoice(n, x, List.map (fun (c, x) -> c, f_rec x) l) + | DVal(i, (false, n)) when + not (edd_subset (edd_meet (edd_extract_path s i) s) s0) + -> + DVal(i, (true, n)) + | x -> x + in + { s with root = memo f s.root } + (* pass_cycle : env -> edd_v -> edd_v unpass_cycle : env -> edd_v -> edd_v @@ -842,14 +862,12 @@ end = struct (print_list Ast_printer.print_typed_var ", ") rp.all_vars; - let enum_vars = List.fold_left - (fun v (_, id, t) -> match t with - | TEnum ch -> (id, ch)::v | _ -> v) - [] rp.all_vars in - let num_vars = List.fold_left - (fun v (_, id, t) -> match t with - | TInt -> (id, false)::v | TReal -> (id, true)::v | _ -> v) - [] rp.all_vars in + let num_vars, enum_vars = List.fold_left + (fun (nv, ev) (_, id, t) -> match t with + | TEnum ch -> nv, (id, ch)::ev + | TInt -> (id, false)::nv, ev + | TReal -> (id, true)::nv, ev) + ([], []) rp.all_vars in let init_f = Transform.init_f_of_prog rp in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; @@ -868,6 +886,7 @@ end = struct let cl = Formula.conslist_of_f f in let cl_g = Formula.conslist_of_f f_g in + Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; (* calculate order for enumerated variables *) let evars = List.map fst enum_vars in @@ -909,7 +928,7 @@ end = struct Format.printf "Init: @[%a@]@." edd_print data; { rp; opt; ve; - f; cl; f_g; cl_g; guarantees; + cl; cl_g; guarantees; cycle; forget; data } @@ -927,7 +946,7 @@ end = struct let d2 = edd_apply_cl x e.cl in let dc = pass_cycle e d2 in - let y = edd_join_star_widen e x dc in + let y = edd_star_new x (edd_accumulate e x dc) in if e.opt.vverbose_ci then Format.printf "d2 %a@. dc %a@. y %a@." @@ -965,7 +984,7 @@ end = struct if n < e.opt.widen_delay then edd_join i fi else - edd_join_widen i fi + edd_widen i fi in if edd_eq i j then j else iter (n+1) j in @@ -973,8 +992,8 @@ end = struct 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_widen e x j in + let fj = pass_cycle e (edd_apply_cl z e.cl) in + let r = edd_star_new x (edd_accumulate e x fj) in if e.opt.verbose_ci then Format.printf " -> %a@." edd_print r; @@ -982,7 +1001,7 @@ end = struct ch_it (n+1) r in - let init_acc = edd_join_star_widen e (edd_bot e.data.ve) e.data in + let init_acc = edd_star_new (edd_bot e.data.ve) e.data in (* Dump final state *) let acc = ch_it 0 init_acc in -- cgit v1.2.3