diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 155 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 34 |
2 files changed, 138 insertions, 51 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index a9ecc07..3ff91a6 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -65,14 +65,18 @@ end = struct | DChoice _ as x -> Format.fprintf fmt "n%d" (Hashtbl.find ids x) in Format.fprintf fmt "Root: %a@." print_n v.root; - Hashtbl.iter - (fun x id -> match x with + for id = 1 to !n do + let c = ref None in + Hashtbl.iter (fun u i -> if i = id then c := Some u) ids; + let x = match !c with | Some x -> x | None -> assert false in + match x with | DChoice (var, l) -> let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in - Format.fprintf fmt "n%d: %s ? @[<hov>%a@]@." id var + Format.fprintf fmt "n%d: %a ? @[<hov>%a@]@." + id Formula_printer.print_id var (print_list p ", ") l - | _ -> assert false) - ids; + | _ -> assert false + done; Hashtbl.iter (fun id v -> Format.fprintf fmt "v%d: %a@." id ND.print v) v.leaves @@ -262,22 +266,80 @@ end = struct { leaves; ve; root = f (a.root, b.root) } (* - edd_of_conslist : varenv -> enum_cons list -> edd_v - - Does this by dichotomy so that the EDD meets are done mostly on - small sized EDDs. + edd_apply_ncl : edd_v -> num_cons list -> edd_v *) - let rec edd_of_conslist ve = function - | [] -> edd_top ve - | [a] -> edd_of_cons ve a - | l -> - let rec split = function - | [] -> [], [] - | [a] -> [a], [] - | a::b::q -> let u, v = split q in a::u, b::v + let edd_apply_ncl v ncl = + let ve = v.ve in + + let n = ref 0 in + let leaves = Hashtbl.create 12 in + + let get_leaf x = + if ND.is_bot x then DBot else begin + let id = ref None in + Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves; + match !id with + | Some i -> DVal i + | None -> + incr n; + Hashtbl.add leaves !n x; + DVal (!n) + 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 in - let u, v = split l in - edd_meet (edd_of_conslist ve u) (edd_of_conslist ve v) + { leaves; ve; root = f v.root } + + (* + 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 + match r with + | CLTrue -> + edd_apply_ncl v nc + | CLFalse -> edd_bot v.ve + | CLAnd (a, b) -> + let v = edd_apply_cl v ([], nc, a) in + 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)) + + (* + edd_eq : edd_v -> edd_v -> bool + *) + let edd_eq a b = + 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 test () = @@ -303,21 +365,22 @@ end = struct ******************************* *) type env = { - rp : rooted_prog; - opt : cmdline_opt; + rp : rooted_prog; + opt : cmdline_opt; - ve : varenv; + ve : varenv; (* program expressions *) - f : bool_expr; - cl : conslist; - f_g : bool_expr; - cl_g : conslist; - guarantees : (id * bool_expr) list; + f : bool_expr; + cl : conslist; + f_g : bool_expr; + cl_g : conslist; + guarantees : (id * bool_expr) list; (* abstract interpretation *) - cycle : (id * id * typ) list; (* s'(x) = s(y) *) - forget : (id * typ) list; (* s'(x) not specified *) + cycle : (id * id * typ) list; (* s'(x) = s(y) *) + forget : (id * typ) list; (* s'(x) not specified *) + mutable data : edd_v; } (* @@ -328,7 +391,16 @@ end = struct A couple may appear several times in the result. *) - let rec extract_linked_evars (ecl, _, r) = + let rec extract_linked_evars_root (ecl, _, r) = + let v_ecl = List.fold_left + (fun c (_, x, v) -> match v with + | EIdent y -> (x, y)::c + | _ -> c) + [] ecl + 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 @@ -343,6 +415,7 @@ end = struct in match q with | [x; y] -> [x, y] + | [x; y; z] -> [x, y; y, z; z, x] | _ -> [] in let rec aux = function @@ -457,10 +530,15 @@ end = struct let lv0 = List.map (fun x -> x, "N"^x) (List.filter (fun x -> List.exists (fun y -> y = "N"^x) evars) evars) in - let lv = lv0 @ extract_linked_evars init_cl @ extract_linked_evars cl_g in - let lv = uniq_sorted - (List.sort Pervasives.compare (List.map ord_couple lv)) in - let evars_ord = scope_constrict evars (lv0 @ lv) in + let lv1 = 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 = scope_constrict evars (lv0 @ lv1 @ lv2) in let ev_order = Hashtbl.create (List.length evars) in List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord; @@ -484,16 +562,21 @@ end = struct rp.all_vars) in + (* calculate initial environment *) + let data = edd_apply_cl (edd_top ve) init_cl in + Format.printf "Init: @[<hov>%a@]@." edd_print data; + { rp; opt; ve; f; cl; f_g; cl_g; guarantees; - cycle; forget } + cycle; forget; data } 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 end diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 3e978ce..b3129c0 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -201,21 +201,25 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | _::q -> 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.as_const v with - | Some i -> Format.fprintf fmt " = %d@]" i - | _ -> Format.fprintf fmt " ∊ %s@]" (V.to_string v)) - sbl; - Format.fprintf fmt " }@]" + if sbl = [] then + Format.fprintf fmt "⊤" + else begin + 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.as_const v with + | Some i -> Format.fprintf fmt " = %d@]" i + | _ -> Format.fprintf fmt " ∊ %s@]" (V.to_string v)) + sbl; + Format.fprintf fmt " }@]" + end let print fmt x = print_vars fmt x (List.map fst (vars x)) |