diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 2 | ||||
| -rw-r--r-- | abstract/enum_domain.ml | 230 | ||||
| -rw-r--r-- | abstract/enum_domain_edd.ml | 371 | ||||
| -rw-r--r--[-rwxr-xr-x] | tests/source/counters.scade | 0 |
5 files changed, 372 insertions, 232 deletions
@@ -18,6 +18,7 @@ SRC= main.ml \ abstract/apron_domain.ml \ abstract/num_domain.ml \ abstract/enum_domain.ml \ + abstract/enum_domain_edd.ml \ \ abstract/formula.ml \ abstract/formula_printer.ml \ diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 8ea0012..1b3bb39 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -47,7 +47,6 @@ end = struct ve : varenv; root : edd; leaves : (int, ND.t) Hashtbl.t; - (* add here eventual annotations *) } (* @@ -529,7 +528,6 @@ end = struct f (ch1@ch2@ch3) else (* Keep disjunction on variable dv *) - let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in let cc = List.map (fun (c, _) -> let ch3 = List.map (fun (_, _, cl) -> List.assoc c cl) d in diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml index d216276..ea2b053 100644 --- a/abstract/enum_domain.ml +++ b/abstract/enum_domain.ml @@ -264,233 +264,3 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct end -(* - Complicated domain : a set of values for each variables, plus some - constraints on couples of variables - (eg. (x, y) in [ tt, tt ; ff, ff ] - - WARNING : This domain is not proved to be safe. In particular, it may represent - a set of contraints that imply Bot (ie that are impossible) without raising the - Bot exception. (there is potentially exponential cost in the checking that all - the constraints are coherent, and I have no idea of an algorithm for doing that - check.) - - Therefore, do not use this domain unless you know what you are doing (which is - probably not the case anyway). -*) - -module MultiValuationCCons : ENUM_ENVIRONMENT_DOMAIN = struct - - module VarC = struct - type t = id * id - let compare = Pervasives.compare - end - module VarCMap = Mapext.Make(VarC) - - type item = string - - type t = { - vars : (id * item list) list; - value : item list VarMap.t; - - (* in ccond (x, y) -> l, must have x < y (textual order on identifiers) -> unicity *) - ccons : (item * item) list VarCMap.t; - } - - let sort = List.sort Pervasives.compare - let uniq x = uniq_sorted (sort x) - let list_inter x y = List.filter (fun k -> List.mem k y) x - - let all_couples l1 l2 = - List.flatten - (List.map (fun x -> List.map (fun y -> x, y) l2) l1) - - let top vars = { vars; value = VarMap.empty; ccons = VarCMap.empty } - - let vars x = x.vars - - let forgetvar x id = - (* TODO : try to find a substitution variable so that some contraints can be propagated. - this is important so that cycle passing can be done correctly ! *) - { x with - value = VarMap.remove id x.value; - ccons = VarCMap.filter (fun (a, b) _ -> a <> id && b <> id) x.ccons } - - let project x id = - try VarMap.find id x.value - with Not_found -> List.assoc id x.vars - - let project2 x id1 id2 = - try - let id1', id2' = ord_couple (id1, id2) in - if id1' = id1 then - VarCMap.find (id1, id2) x.ccons - else - List.map (fun (a, b) -> b, a) (VarCMap.find (id1', id2') x.ccons) - with _ -> - let v1, v2 = project x id1, project x id2 in - all_couples v1 v2 - - let strict x = - let rec f x = - (* - - if (x, y) in [ a, b1 ; a, b2 ; ... ; a, bn ], - replace this by x = a and y in { b1, ..., bn } - - filter (x, y) in [ ... ] with x in specified itv, y in specified itv - *) - let usefull, vv, cc = - VarCMap.fold - (fun (x, y) l (usefull, vv, cc) -> - let p1, p2 = uniq (List.map fst l), uniq (List.map snd l) in - let p1 = try list_inter p1 (VarMap.find x vv) with _ -> p1 in - let p2 = try list_inter p2 (VarMap.find y vv) with _ -> p2 in - - if p1 = [] || p2 = [] then raise Bot; - let vv = VarMap.add x p1 (VarMap.add y p2 vv) in - - if List.length p1 = 1 || List.length p2 = 1 - then - true, vv, cc - else - match List.filter (fun (u, v) -> List.mem u p1 && List.mem v p2) l with - | [] -> raise Bot - | l2 -> List.length l2 < List.length l, vv, VarCMap.add (x, y) l2 cc) - x.ccons (false, x.value, VarCMap.empty) in - - let x = { x with value = vv; ccons = cc } in - if usefull then f x else x - in - f x - - let join x1 x2 = - let v = VarMap.merge - (fun _ a b -> match a, b with - | Some a, Some b -> Some (uniq (a@b)) - | _ -> None) - x1.value x2.value in - let x = { x1 with value = v } in - - let cc = VarCMap.merge - (fun (id1, id2) l1 l2 -> - let v1, v2 = project x1 id1, project x id2 in - let ac = all_couples v1 v2 in - let c = List.filter - (fun q -> - (match l1 with Some l -> List.mem q l | _ -> true) || - (match l2 with Some l -> List.mem q l | _ -> true)) - ac in - if List.length c < List.length ac then Some c else None) - x1.ccons x2.ccons in - - strict { x with ccons = cc } - - let meet x1 x2 = - let v = VarMap.merge - (fun _ a b -> match a, b with - | Some a, None | None, Some a -> Some a - | Some a, Some b -> - begin match list_inter a b with - | [] -> raise Bot | l -> Some l end - | _ -> None) - x1.value x2.value in - let x = { x1 with value = v } in - - let cc = VarCMap.merge - (fun (id1, id2) l1 l2 -> - let v1, v2 = project x id1, project x id2 in - let ac = all_couples v1 v2 in - let c1 = match l1 with Some l -> list_inter l ac | None -> ac in - let c2 = match l2 with Some l -> list_inter l ac | None -> ac in - match list_inter c1 c2 with - | [] -> raise Bot - | l -> if List.length l < List.length ac then Some l else None) - x1.ccons x2.ccons in - - strict { x with ccons = cc } - - let subset a b = - VarMap.for_all - (fun id v -> - let vs = project a id in - List.for_all (fun c -> List.mem c vs) v) - b.value - && - VarCMap.for_all - (fun (id1, id2) l -> - let l2 = project2 a id1 id2 in - List.for_all (fun c -> List.mem c l) l2) - b.ccons - let eq a b = - subset a b && subset b a - - let apply_cons x (op, id, e) = - let op = match op with | E_EQ -> (=) | E_NE -> (<>) in - - match e with - | EItem s -> - let pv = project x id in - begin match List.filter (op s) pv with - | [] -> [] - | vals -> try [strict { x with value = VarMap.add id vals x.value }] with Bot -> [] - end - | EIdent id2 -> - let id, id2 = ord_couple (id, id2) in - let c = project2 x id id2 in - let ok_c = List.filter (fun (a, b) -> op a b) c in - try - [match uniq (List.map fst ok_c), uniq (List.map snd ok_c) with - | [], _ | _, [] -> raise Bot - | [a], q -> strict { x with value = VarMap.add id [a] (VarMap.add id2 q x.value) } - | q, [b] -> strict { x with value = VarMap.add id q (VarMap.add id2 [b] x.value) } - | _ -> strict { x with ccons = VarCMap.add (id, id2) ok_c x.ccons} - ] - with Bot -> [] - - let assign x idl = - let x2 = List.fold_left (fun x (v, _) -> forgetvar x v) x idl in - let v = List.fold_left - (fun v (id, id2) -> - try VarMap.add id (VarMap.find id2 x.value) v - with Not_found -> v) - x2.value idl in - let c = VarCMap.fold - (fun (v1, v2) l c -> - let v1' = try List.assoc v1 idl with _ -> v1 in - let v2' = try List.assoc v2 idl with _ -> v2 in - VarCMap.add (v1', v2') l c) - x.ccons x2.ccons in - strict { x with value = v; ccons = c } - - - let print fmt x = - let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x.value) in - let s = List.sort Pervasives.compare b in - let rec bl = function - | [] -> [] - | (v, id)::q -> - let v = sort v in - if v <> sort (List.assoc id x.vars) then - match bl q with - | (vv, ids)::q when vv = v -> (v, id::ids)::q - | r -> (v, [id])::r - else - bl q - in - let sbl = bl s in - Format.fprintf fmt "@[<v 2>{ "; - List.iteri - (fun j (v, ids) -> - if j > 0 then Format.fprintf fmt "@ "; - Format.fprintf fmt "@[<hov 4>"; - List.iteri - (fun i id -> - if i > 0 then Format.fprintf fmt ",@ "; - Format.fprintf fmt "%a" Formula_printer.print_id id) - ids; - match v with - | [v0] -> Format.fprintf fmt " ≡ %s@]" v0 - | l -> Format.fprintf fmt " ∊ @[<hov>{ %a }@]@]" (print_list Format.pp_print_string ", ") l) - sbl; - Format.fprintf fmt " }@]" - -end diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml new file mode 100644 index 0000000..60f2d3b --- /dev/null +++ b/abstract/enum_domain_edd.ml @@ -0,0 +1,371 @@ +open Ast +open Formula +open Util +open Enum_domain + +module EDD : ENUM_ENVIRONMENT_DOMAIN = struct + exception Top + + type item = string + + type edd = + | DBot + | DTop + | DChoice of int * id * (item * edd) list + + type t = { + vars : (id * item list) list; + order : (id, int) Hashtbl.t; + root : edd; + } + + (* Utility functions for memoization *) + let key = function + | DBot -> -1 + | DTop -> -2 + | DChoice(i, _, _) -> i + + let memo f = + let memo = Hashtbl.create 12 in + let rec ff v = + try Hashtbl.find memo (key v) + with Not_found -> + let r = f ff v in + Hashtbl.add memo (key v) r; r + in ff + + let memo2 f = + let memo = Hashtbl.create 12 in + let rec ff v1 v2 = + try Hashtbl.find memo (key v1, key v2) + with Not_found -> + let r = f ff v1 v2 in + Hashtbl.add memo (key v1, key v2) r; r + in ff + + let edd_node_eq = function + | DBot, DBot -> true + | DTop, DTop -> true + | DChoice(i, _, _), DChoice(j, _, _) -> i = j + | _ -> 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 rank v = function + | DChoice(_, x, _) -> Hashtbl.find v.order x + | _ -> 10000000 + + + (* + print : Format.formatter -> t -> unit + *) + let print fmt v = + 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 "⊤"; + | 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 "@[<v 4>{ @[<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; + Format.fprintf fmt " }@]" + + (* + top : (id * item list) list -> t + *) + let top vars = + let order = Hashtbl.create 12 in + List.iteri (fun i (id, _) -> Hashtbl.add order id i) vars; + { vars; order; root = DTop } + (* + vars : t -> (id * item list) list + *) + let vars x = x.vars + + (* + of_cons : t -> enum_cons -> t + The first t is NOT used as a decision function, here we only use + the variable ordering it provides. + *) + let of_cons v0 (op, vid, r) = + let op = match op with | E_EQ -> (=) | E_NE -> (<>) in + + let root = match r with + | EItem x -> + DChoice(0, vid, + List.map (fun v -> if op v x then v, DTop else v, DBot) + (List.assoc vid v0.vars)) + | EIdent vid2 -> + let a, b = + if Hashtbl.find v0.order vid < Hashtbl.find v0.order vid2 + then vid, vid2 + else vid2, vid + in + let nc = ref 0 in + let nb x = + incr nc; + DChoice(!nc, b, + List.map (fun v -> if op v x then v, DTop else v, DBot) + (List.assoc b v0.vars)) + in + DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a v0.vars)) + in + { v0 with root = root } + + (* + join : t -> t -> t + meet : t -> t -> t + *) + let join a b = + if a.root = DBot then b else + if b.root = DBot then a else + if a.root = DTop || b.root = DTop then { a with root = DTop } else begin + 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 a na < rank a nb -> + let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in + dq va kl + | _, DChoice(_, vb, lb) when rank a nb < rank a na -> + let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in + dq vb kl + + | _ -> assert false + in + { a with root = memo2 f a.root b.root } + end + + let meet a b = + if a.root = DTop then b else + if b.root = DTop then a else + if a.root = DBot || b.root = DBot then { a with root = DBot } else begin + 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 a na < rank a nb -> + let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in + dq va kl + | _, DChoice(_, vb, lb) when rank a nb < rank a na -> + let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in + dq vb kl + + | _ -> assert false + in + {a with root = memo2 f a.root b.root } + end + + (* + apply_cons : t -> enum_cons -> t + apply_cl : t -> enum_cons list -> t + *) + let apply_cons v x = + let v = meet v (of_cons v x) in + if v.root = DBot then [] else [v] + let apply_cl v ec = + let rec cl_k = function + | [] -> { v with root = DTop } + | [a] -> of_cons v a + | l -> + let n = ref 0 in + let la, lb = List.partition (fun _ -> incr n; !n mod 2 = 0) l in + meet (cl_k la) (cl_k lb) + in + let cons_edd = cl_k ec in + meet v cons_edd + + (* + eq : edd_v -> edd_v -> bool + *) + let eq a b = + let f f_rec na nb = + match na, nb with + | DBot, DBot -> true + | DTop, DTop -> true + | 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 + | _ -> false + in memo2 f a.root b.root + + (* + subset : edd_v -> edd_v -> bool + *) + let subset a b = + let rank = rank a in + let f f_rec na nb = + match na, nb with + | DBot, _ -> true + | _, DTop -> true + | DTop, DBot -> false + + | 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 + + (* + forgetvars : t -> id list -> t + *) + let forgetvars v vars = + let dq = new_node_fun () in + + let 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 + with Not_found -> let r = + try + let cn = List.fold_left + (fun cn node -> match node with + | DBot -> cn + | DTop -> raise Top + | DChoice (n, v, l) -> (n, v, l)::cn) + [] l in + let cn = List.sort + (fun (n, v1, _) (n, v2, _) -> Pervasives.compare + (Hashtbl.find v.order v1) (Hashtbl.find v.order v2)) + cn in + if cn = [] then + DBot + else + 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 + if List.mem dv vars then + (* Do union of all branches branching from nodes on variable dv *) + let ch2 = List.flatten + (List.map (fun (_, _, c) -> List.map snd c) d) in + f (ch1@ch2) + else + (* Keep disjunction on variable dv *) + let cc = List.map + (fun (c, _) -> + let ch2 = List.map (fun (_, _, cl) -> List.assoc c cl) d in + c, f (ch1@ch2)) + cl in + dq dv cc + with | Top -> DTop + in Hashtbl.add memo kl r; r + in + { v with root = f [v.root] } + + let forgetvar v x = forgetvars v [x] + + (* + project : t -> id -> item list + *) + let project v x = + try + let vals = ref [] in + let f f_rec = function + | DBot -> () + | DChoice(_, var, l) when + Hashtbl.find v.order var < Hashtbl.find v.order x -> + List.iter (fun (_, c) -> f_rec c) l + | DChoice(_, var, l) when var = x -> + List.iter + (fun (v, l) -> + if l <> DBot && not (List.mem v !vals) then vals := v::(!vals)) + l + | _ -> raise Top + in + memo f v.root; !vals + with Top -> List.assoc x v.vars + + (* + assign : t -> (id * id) list -> t + *) + let assign v ids = + let v = forgetvars v (List.map fst ids) in + apply_cl v (List.map (fun (x, y) -> (E_EQ, x, EIdent y)) ids) + +end diff --git a/tests/source/counters.scade b/tests/source/counters.scade index 334bca1..334bca1 100755..100644 --- a/tests/source/counters.scade +++ b/tests/source/counters.scade |