diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 151 |
1 files changed, 80 insertions, 71 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index fd31670..6220a0a 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -280,78 +280,86 @@ end = struct edd_meet : edd_v -> edd_v -> edd_v *) 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 f f_rec na nb = - match na, nb with - | 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 - - | DTop, _ | _, DTop -> DTop - | DBot, DBot -> DBot - - | 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) when rank ve nb < rank ve na -> - 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) - - | _ -> 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) } + if a.root = DBot then b else + if b.root = DBot then a else + if a.root = DTop || b.root = DTop then edd_top a.ve else begin + 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 + | 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 + + | DTop, _ | _, DTop -> DTop + | DBot, DBot -> DBot + + | 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) when rank ve nb < rank ve na -> + 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) + + | _ -> 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) } + end 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 - | 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 - - | DBot, _ | _, DBot -> DBot - | DTop, DTop -> DTop - - | 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) when rank ve nb < rank ve na -> - 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) - - | _ -> assert false (* see above *) - in - { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) } + if a.root = DTop then b else + if b.root = DTop then a else + if a.root = DBot || b.root = DBot then edd_bot a.ve else begin + 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 + | 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 + + | DBot, _ | _, DBot -> DBot + | DTop, DTop -> DTop + + | 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) when rank ve nb < rank ve na -> + 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) + + | _ -> assert false (* see above *) + in + { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) } + end @@ -407,7 +415,8 @@ end = struct | CLFalse -> edd_bot v.ve | CLAnd (a, b) -> let v = edd_apply_cl v ([], nc, a) in - edd_apply_cl v ([], nc, b) + if v.root = DBot then v else + edd_apply_cl v ([], nc, b) | CLOr((eca, nca, ra), (ecb, ncb, rb)) -> edd_join (edd_apply_cl v (eca, nc@nca, ra)) (edd_apply_cl v (ecb, nc@ncb, rb)) |