diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp.ml | 15 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 458 |
2 files changed, 318 insertions, 155 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index bed2f2c..a612976 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -328,16 +328,11 @@ end = struct pass_cycle : st -> case_v -> case_v *) let pass_cycle st (enum, num) = - let assign_e = - List.map (fun (a, b, _) -> a, b) - (List.filter - (fun (_, _, t) -> match t with TEnum _ -> true | _ -> false) - st.cycle) in - let assign_n = - List.map (fun (a, b, _) -> a, NIdent b) - (List.filter - (fun (_, _, t) -> match t with TInt | TReal -> true | _ -> false) - st.cycle) in + let assign_e, assign_n = List.fold_left + (fun (ae, an) (a, b, t) -> match t with + | TEnum _ -> (a, b)::ae, an + | TInt | TReal -> ae, (a, NIdent b)::an) + ([], []) st.cycle in let enum = ED.assign enum assign_e in let num = ND.assign num assign_n in diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 4f2ad81..863a22d 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -7,10 +7,18 @@ open Util open Num_domain open Abs_interp +let time id f = + Format.printf "%s[@?" id; + let r = f () in + Format.printf "] @?"; + r + module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig val do_prog : cmdline_opt -> rooted_prog -> unit + val test : unit -> unit + end = struct @@ -29,11 +37,10 @@ end = struct ev_order : (id, int) Hashtbl.t; } - type edd_node = + type edd = | DBot | DVal of int - | DChoice of id * (item * edd) list - and edd = int * edd_node + | DChoice of int * id * (item * edd) list type edd_v = { ve : varenv; @@ -45,41 +52,54 @@ end = struct (* Utility functions for memoization - memo : (((int * 'a) -> (int * 'b)) -> 'a -> 'b) -> (int * 'a) -> (int * 'b) - memo2 : (((int * 'a) -> (int * 'b) -> (int * 'c)) -> 'a -> 'b -> 'c) -> (int * 'a) -> (int * 'b) -> (int * 'c) + memo : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b + -> (int * 'a) -> (int * 'b) + memo2 : (('a -> 'b -> 'c) -> 'a -> 'b -> 'c) + -> 'a -> 'b -> 'c + + Where 'a = 'b = 'c = edd, but it can be adapted. *) + let key = function + | DBot -> None + | DVal i -> Some (Left i) + | DChoice(i, _, _) -> Some (Right i) + let memo f = - let n = ref 0 in let memo = Hashtbl.create 12 in - let rec ff (id, v) = - try Hashtbl.find memo id + let rec ff v = + try Hashtbl.find memo (key v) with Not_found -> let r = f ff v in - incr n; - Hashtbl.add memo id (n, r); - n, r + Hashtbl.add memo (key v) r; r in ff let memo2 f = - let n = ref 0 in let memo = Hashtbl.create 12 in - let rec ff (id1, v1) (id2, v2) = - try Hashtbl.find memo (id1, id2) + let rec ff v1 v2 = + try Hashtbl.find memo (key v1, key v2) with Not_found -> let r = f ff v1 v2 in - incr n; - Hashtbl.add memo (id1, id2) (n, r); - n, r + Hashtbl.add memo (key v1, key v2) r; r in ff + let edd_node_eq = function + | DBot, DBot -> true + | DVal i, DVal j when i = j -> true + | DChoice(i, _, _), DChoice(j, _, _) when i = j -> true + | _ -> false + (* 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 c_nodes = Hashtbl.create 12 in let rec add = function - | n, (DChoice(_, l) as x) -> + | DChoice(n, _, l) as x -> if not (Hashtbl.mem c_nodes n) then begin + if n > !max_n then max_n := n; Hashtbl.add c_nodes n x; List.iter (fun (_, y) -> add y) l end @@ -87,31 +107,35 @@ end = struct in add v.root; let print_n fmt = function - | (_, DBot) -> Format.fprintf fmt "⊥"; - | (_, DVal i) -> Format.fprintf fmt "v%d" i; - | (n, DChoice _) -> Format.fprintf fmt "n%d" n + | DBot -> Format.fprintf fmt "⊥"; + | DVal i -> if i > !max_v then max_v := i; + Format.fprintf fmt "v%d" i; + | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n in Format.fprintf fmt "Root: %a@." print_n v.root; - Hashtbl.iter - (fun id x -> match x with - | DChoice (var, l) -> + for id = !max_n downto 0 do + try match Hashtbl.find c_nodes id with + | DChoice (_, var, l) -> let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in Format.fprintf fmt "n%d: %a ? @[<hov>%a@]@." id Formula_printer.print_id var (print_list p ", ") l - | _ -> assert false) - c_nodes; - Hashtbl.iter - (fun id v -> Format.fprintf fmt "v%d: %a@." id ND.print v) - v.leaves - + | _ -> assert false + with Not_found -> () + done; + + for id = 0 to !max_v do + try let v = Hashtbl.find v.leaves id in + Format.fprintf fmt "v%d: %a@." id ND.print v + with Not_found -> () + done (* edd_bot : varenv -> edd_v *) - let edd_bot ve = { ve; root = (0, DBot); leaves = Hashtbl.create 1 } + let edd_bot ve = { ve; root = DBot; leaves = Hashtbl.create 1 } (* edd_top : evar list -> nvar list -> edd_v @@ -119,7 +143,7 @@ end = struct let edd_top ve = let leaves = Hashtbl.create 1 in Hashtbl.add leaves 0 (ND.top ve.nvars); - { ve; root = (1, DVal 0); leaves } + { ve; root = DVal 0; leaves } (* edd_of_cons : varenv -> enum_cons -> edd_v @@ -130,12 +154,12 @@ end = struct let leaves = Hashtbl.create 1 in Hashtbl.add leaves 0 (ND.top ve.nvars); - let bot, top = (0, DBot), (1, DVal 0) in + let bot, top = DBot, DVal 0 in let root = match r with | EItem x -> - 2, DChoice(vid, - List.map (fun v -> if op v x then v, bot else v, top) + DChoice(0, vid, + List.map (fun v -> if op v x then v, top else v, bot) (List.assoc vid ve.evars)) | EIdent vid2 -> let a, b = @@ -143,14 +167,14 @@ end = struct then vid, vid2 else vid2, vid in - let n = ref 2 in + let n = ref 0 in let nb x = incr n; - !n, DChoice(b, + DChoice(!n, b, List.map (fun v -> if op v x then v, top else v, bot) (List.assoc b ve.evars)) in - 2, DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars)) + DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a ve.evars)) in { ve; root; leaves } @@ -161,61 +185,63 @@ end = struct let ve = a.ve in let leaves = Hashtbl.create 12 in + let lc = ref 0 in - let n = 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 n; - Hashtbl.add leaves !n x; - DVal (!n) + incr lc; + Hashtbl.add leaves !lc x; + DVal (!lc) end in - + let nc = ref 0 in let f f_rec na nb = let dq v l = - let _, (i, x0) = List.hd l in - if List.exists (fun (_, (j, x)) -> j <> i || x <> x0) l - then DChoice(v, l) - else x0 + let _, x0 = List.hd l in + if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l + then begin + incr nc; DChoice(!nc, v, l) + end else x0 in match na, nb with | DBot, DBot -> DBot - | DBot, DVal i -> get_leaf (Hashtbl.find b.leaves i) - | x, DBot -> x + | 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 - | DChoice(va, la), DChoice(vb, lb) when va = vb -> + | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> let kl = List.map2 (fun (ta, ba) (tb, bb) -> assert (ta = tb); - ta, f (ba, bb)) + ta, f_rec ba bb) la lb in dq va kl - | DChoice(va, la), DChoice(vb, lb) -> + | 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 (ca, nb)) la + va, List.map (fun (k, ca) -> k, f_rec ca nb) la else - vb, List.map (fun (k, cb) -> k, f (na, cb)) lb + vb, List.map (fun (k, cb) -> k, f_rec na cb) lb in dq v kl - | DChoice(va, la), _ -> - let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in + | 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 (na, cb)) lb in + | _, 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 in - { leaves; ve; root = memo2 f a.root b.root } + { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) } (* edd_meet : edd_v -> edd_v -> edd_v @@ -223,7 +249,7 @@ end = struct let edd_meet a b = let ve = a.ve in - let n = ref 0 in + let lc = ref 0 in let leaves = Hashtbl.create 12 in let get_leaf x = @@ -233,59 +259,59 @@ end = struct match !id with | Some i -> DVal i | None -> - incr n; - Hashtbl.add leaves !n x; - DVal (!n) + incr lc; + Hashtbl.add leaves !lc x; + DVal (!lc) end in - let memo = Hashtbl.create 12 in - let rec f (na, nb) = - try Hashtbl.find memo (na, nb) - with Not_found -> let r = - let dq v l = - let _, x0 = List.hd l in - if List.exists (fun (_, x) -> x <> x0) l - then DChoice(v, l) - else x0 + let nc = ref 0 in + let f f_rec na nb = + let dq v l = + let _, x0 = List.hd l in + if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l + then begin + incr nc; DChoice(!nc, v, l) + end else x0 + in + match na, nb with + | DBot, _ | _, DBot -> DBot + | DVal u, DVal v -> + let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + get_leaf x + + | 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 - match na, nb with - | 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 (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 (ca, nb)) la - else - vb, List.map (fun (k, cb) -> k, f (na, cb)) lb - in - dq v kl - | DChoice(va, la), _ -> - let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in - dq va kl - | _, DChoice(vb, lb) -> - let kl = List.map (fun (k, cb) -> k, f (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 - in Hashtbl.add memo (na, nb) r; r + 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 + | 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 = f (a.root, b.root) } + { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) } (* + edd_num_apply : edd_v -> (ND.t -> ND.t) -> edd_v edd_apply_ncl : edd_v -> num_cons list -> edd_v *) - let edd_apply_ncl v ncl = + let edd_num_apply v nfun = let ve = v.ve in - let n = ref 0 in + let lc = ref 0 in let leaves = Hashtbl.create 12 in let get_leaf x = @@ -295,36 +321,48 @@ end = struct match !id with | Some i -> DVal i | None -> - incr n; - Hashtbl.add leaves !n x; - DVal (!n) + incr lc; + Hashtbl.add leaves !lc x; + DVal (!lc) end in - let memo = Hashtbl.create 12 in - let rec f n = - try Hashtbl.find memo n - with Not_found -> let r = - match n with - | DBot -> DBot - | DVal i -> get_leaf (ND.apply_cl (Hashtbl.find v.leaves i) ncl) - | DChoice(var, l) -> - let l = List.map (fun (k, v) -> k, f v) l in - let _, x0 = List.hd l in - if List.exists (fun (_, x) -> x <> x0) l - then DChoice(var, l) - else x0 - in Hashtbl.add memo n r; r + let f f_rec n = + match n with + | DBot -> DBot + | 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 + in + { leaves; ve; root = memo f v.root } + + let edd_apply_ncl v ncl = + edd_num_apply v (fun n -> ND.apply_cl n ncl) + + (* + edd_apply_ecl : edd_v -> enum_cons list -> edd_v + *) + let edd_apply_ecl v ec = + let rec cl_k = function + | [] -> edd_top v.ve + | [a] -> edd_of_cons v.ve a + | l -> + let n = ref 0 in + let la, lb = List.partition (fun _ -> incr n; !n mod 2 = 0) l in + edd_meet (cl_k la) (cl_k lb) in - { leaves; ve; root = f v.root } + let cons_edd = cl_k ec in + edd_meet v cons_edd (* edd_apply_cl : edd_v -> conslist -> edd_v *) let rec edd_apply_cl v (ec, nc, r) = - let v = List.fold_left - (fun v cons -> edd_meet v (edd_of_cons v.ve cons)) - v ec in + let v = edd_apply_ecl v ec in match r with | CLTrue -> edd_apply_ncl v nc @@ -340,23 +378,100 @@ end = struct edd_eq : edd_v -> edd_v -> bool *) let edd_eq a b = + let f f_rec na nb = + match na, nb with + | DBot, DBot -> true + | 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) + la lb + | _ -> false + in memo2 f a.root b.root + + + (* + edd_forget_vars : edd_v -> id list -> edd_v + *) + 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 nc = ref 0 in let memo = Hashtbl.create 12 in - let rec f (na, nb) = - try Hashtbl.find memo (na, nb) - with Not_found -> let r = - match na, nb with - | DBot, DBot -> true - | 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 (na, nb)) - la lb - | _ -> false - in Hashtbl.add memo (na, nb) r; r - in f (a.root, b.root) + 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 = + let cn, fn = List.fold_left + (fun (cn, fn) node -> match node with + | DBot -> cn, fn + | DVal i -> cn, i::fn + | DChoice (n, v, l) -> (n, v, l)::cn, fn) + ([], []) l in + let cn = List.sort + (fun (n, v1, _) (n, v2, _) -> Pervasives.compare + (Hashtbl.find ve.ev_order v1) (Hashtbl.find ve.ev_order v2)) + cn in + if cn = [] then + if fn = [] then DBot + else + let x = list_fold_op ND.join + (List.map (Hashtbl.find v.leaves) fn) + in get_leaf x + 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 + let ch2 = List.map (fun i -> DVal i) fn in + if List.mem dv vars then + (* Do union of all branches branching from nodes on variable dv *) + let ch3 = List.flatten + (List.map (fun (_, _, c) -> List.map snd c) d) in + 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 + c, f (ch1@ch2@ch3)) + cl in + 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) + end else x0 + in Hashtbl.add memo kl r; r + in + { leaves; ve; root = f [v.root] } + + (* + edd_eassign : edd_v -> (id * id) list -> edd_v + *) + let edd_eassign v ids = + let v = edd_forget_vars v (List.map fst ids) in + edd_apply_ecl v + (List.map (fun (x, y) -> (E_EQ, x, EIdent y)) ids) (* + Just a function to test EDDs + *) let test () = let ve = { evars = ["x", ["tt"; "ff"]; "y", ["tt"; "ff"]; "z", ["tt"; "ff"]]; @@ -372,8 +487,11 @@ end = struct let w = edd_meet u v in Format.printf "x = y && y != z : @[%a@]@." edd_print w; let t = edd_join u v in - Format.printf "x = y || y != z : @[%a@]@." edd_print t - *) + Format.printf "x = y || y != z : @[%a@]@." edd_print t; + let e = edd_forget_vars w ["y"] in + Format.printf "x = y && y != z ; forget y : @[%a@]@." edd_print e; + let f = edd_forget_vars t ["y"] in + Format.printf "x = y || y != z ; forget y : @[%a@]@." edd_print f (* ****************************** @@ -399,6 +517,29 @@ end = struct mutable data : edd_v; } + + (* + pass_cycle : env -> edd_v -> edd_v + *) + let pass_cycle env v = + let assign_e, assign_n = List.fold_left + (fun (ae, an) (a, b, t) -> match t with + | TEnum _ -> (a, b)::ae, an + | TInt | TReal -> ae, (a, NIdent b)::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) -> match t with + | TEnum _ -> var::ef, nf + | TReal | TInt -> ef, var::nf) + ([], []) env.forget 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 @@ -554,7 +695,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 = scope_constrict evars (lv0 @ lv1 @ lv2) in + let evars_ord = List.rev @@ 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; @@ -591,8 +732,35 @@ end = struct let do_prog opt rp = let e = init_env opt rp in - let d2 = edd_apply_cl e.data e.cl in - Format.printf " -> @[<hov>%a@]@." edd_print d2 + 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 + in + + let final = edd_apply_cl (f e.data) e.cl in + (*Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;*) + + let check_guarantee (id, f) = + let cl = Formula.conslist_of_f f in + Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ " + id Formula_printer.print_conslist cl; + let z = edd_apply_cl final cl in + if z.root = DBot then + Format.printf "OK@]@ " + else + Format.printf "FAIL@]@ " + in + if e.guarantees <> [] then begin + Format.printf "Guarantee @[<v 0>"; + List.iter check_guarantee e.guarantees; + Format.printf "@]@." + end; end |