diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 83 |
1 files changed, 28 insertions, 55 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 5b3b0ec..f08be44 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -91,6 +91,7 @@ end = struct | 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 @@ -128,7 +129,6 @@ end = struct edd_print : Format.formatter -> edd_v -> unit *) let edd_print fmt v = - let max_n = ref 0 in let max_v = ref 0 in let print_nodes = Queue.create () in @@ -248,10 +248,10 @@ end = struct then vid, vid2 else vid2, vid in - let n = ref 0 in + let nc = ref 0 in let nb x = - incr n; - DChoice(!n, b, + incr nc; + DChoice(!nc, b, List.map (fun v -> if op v x then v, DTop else v, DBot) (List.assoc b ve.evars)) in @@ -270,9 +270,6 @@ end = struct 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); @@ -289,13 +286,8 @@ end = struct 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 x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in - get_leaf x + | DTop, _ | _, DTop -> DTop + | DBot, DBot -> DBot | DChoice(_,va, la), _ -> let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in @@ -303,6 +295,14 @@ end = struct | _, DChoice(_, vb, lb) -> let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in dq vb kl + + | DVal (u, _), DVal (v, _) -> + let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + get_leaf x + | DVal(u, _), DBot -> + get_leaf (Hashtbl.find a.leaves u) + | DBot, DVal(v, _) -> + get_leaf (Hashtbl.find b.leaves v) in { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) } @@ -313,9 +313,6 @@ end = struct let f f_rec na nb = match na, nb with - | DBot, _ | _, DBot -> DBot - | DTop, DTop -> DTop - | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> let kl = List.map2 (fun (ta, ba) (tb, bb) -> assert (ta = tb); @@ -332,13 +329,8 @@ end = struct in dq v kl - | DTop, DVal (i, _) -> - get_leaf (Hashtbl.find b.leaves i) - | DVal (i, _), DTop -> - get_leaf (Hashtbl.find a.leaves i) - | DVal (u, _) , DVal (v, _) -> - let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in - get_leaf x + | DBot, _ | _, DBot -> DBot + | DTop, DTop -> DTop | DChoice(_, va, la), _ -> let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in @@ -346,6 +338,14 @@ end = struct | _, DChoice(_, vb, lb) -> let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in dq vb kl + + | DVal (u, _) , DVal (v, _) -> + let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + get_leaf x + | DVal(u, _), DTop -> + get_leaf (Hashtbl.find a.leaves u) + | DTop, DVal(v, _) -> + get_leaf (Hashtbl.find b.leaves v) in { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) } @@ -757,30 +757,6 @@ end = struct in v_ecl - let rec extract_linked_evars(ecl, _, r) = - let v_ecl = List.fold_left - (fun c (_, x, v) -> match v with - | EIdent y -> (x, y)::c - | _ -> c) - [] ecl - in - let v_ecl2 = - let q = List.fold_left - (fun c (_, x, v) -> match v with - | EItem _ -> x::c | _ -> c) - [] ecl - in - match q with - | [x; y] -> [x, y] - | [x; y; z] -> [x, y; y, z; z, x] - | _ -> [] - in - let rec aux = function - | CLTrue | CLFalse -> [] - | CLAnd(a, b) -> aux a @ aux b - | CLOr(a, b) -> extract_linked_evars a @ extract_linked_evars b - in - v_ecl @ v_ecl2 @ aux r (* scope_constrict : id list -> (id * id) list -> id list @@ -885,15 +861,12 @@ end = struct (* calculate order for enumerated variables *) let evars = List.map fst enum_vars in - let lv1 = extract_linked_evars_root init_cl + let lv = 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 - let lv1 = uniq_sorted - (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 = time "SCA" (fun () -> scope_constrict evars ( lv1 )) in + let lv = uniq_sorted + (List.sort Pervasives.compare (List.map ord_couple lv)) in + let evars_ord = time "SCA" (fun () -> scope_constrict evars lv) 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 |