diff options
Diffstat (limited to 'abstract/abs_interp_edd.ml')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 256 |
1 files changed, 17 insertions, 239 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 1b3bb39..b80ca14 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -7,6 +7,7 @@ open Cmdline open Util open Num_domain +open Varenv exception Top @@ -25,18 +26,6 @@ end = struct (* ********************** EDD Domain ********************** *) - - type item = string - - type evar = id * item list - type nvar = id * bool - - type varenv = { - evars : evar list; - nvars : nvar list; - ev_order : (id, int) Hashtbl.t; - } - type edd = | DBot | DTop @@ -564,7 +553,11 @@ end = struct let ve = { evars = ["x", ["tt"; "ff"]; "y", ["tt"; "ff"]; "z", ["tt"; "ff"]]; nvars = []; - ev_order = Hashtbl.create 2 } in + ev_order = Hashtbl.create 2; + last_vars = []; + all_vars = []; + cycle = []; + forget = []; } in Hashtbl.add ve.ev_order "x" 0; Hashtbl.add ve.ev_order "y" 1; Hashtbl.add ve.ev_order "z" 2; @@ -590,8 +583,6 @@ end = struct rp : rooted_prog; opt : cmdline_opt; - last_vars : (bool * id * typ) list; - all_vars : (bool * id * typ) list; ve : varenv; (* program expressions *) @@ -599,10 +590,6 @@ end = struct cl : conslist; 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 *) } @@ -736,7 +723,7 @@ end = struct { s with root = memo f s.root } (* - pass_cycle : env -> edd_v -> edd_v + pass_cycle : varenv -> edd_v -> edd_v unpass_cycle : env -> edd_v -> edd_v *) let pass_cycle env v = @@ -763,7 +750,7 @@ end = struct (fun (ae, an) (a, b, t) -> match t with | TEnum _ -> (b, a)::ae, an | TInt | TReal -> ae, (b, NIdent a)::an) - ([], []) env.cycle in + ([], []) env.ve.cycle in let v = edd_eassign v assign_e in let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in @@ -780,145 +767,7 @@ end = struct 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 - - Extract all pairs of enum-type variable (x, y) appearing in an - equation like x = y or x != y - - A couple may appear several times in the result. - *) - 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_const_vars_root (ecl, _, _) = - List.fold_left - (fun l (_, x, v) -> match v with - | EItem _ -> x::l - | _ -> l) - [] ecl - - (* - scope_constrict : id list -> (id * id) list -> id list - - Orders the variable in the first argument such as to minimize the - sum of the distance between the position of two variables appearing in - a couple of the second list. (minimisation is approximate, this is - an heuristic so that the EDD will not explode in size when expressing - equations such as x = y && u = v && a != b) - *) - let scope_constrict vars cp_id = - let var_i = Array.of_list vars in - let n = Array.length var_i in - - let i_var = Hashtbl.create n in - Array.iteri (fun i v -> Hashtbl.add i_var v i) var_i; - - let cp_i = List.map - (fun (x, y) -> Hashtbl.find i_var x, Hashtbl.find i_var y) - cp_id in - - let eval i = - let r = Array.make n (-1) in - Array.iteri (fun pos var -> r.(var) <- pos) i; - Array.iteri (fun _ x -> assert (x <> (-1))) r; - List.fold_left - (fun s (x, y) -> s + abs (r.(x) - r.(y))) - 0 cp_i - in - - let best = Array.init n (fun i -> i) in - - let usefull = ref true in - Format.printf "SCA"; - while !usefull do - Format.printf ".@?"; - - usefull := false; - let try_s x = - if eval x < eval best then begin - Array.blit x 0 best 0 n; - usefull := true - end - in - - for i = 0 to n-1 do - let tt = Array.copy best in - (* move item i at beginning *) - let temp = tt.(i) in - for j = i downto 1 do tt.(j) <- tt.(j-1) done; - tt.(0) <- temp; - (* try all positions *) - try_s tt; - for j = 1 to n-1 do - let temp = tt.(j-1) in - tt.(j-1) <- tt.(j); - tt.(j) <- temp; - try_s tt - done - done - done; - Format.printf "@."; - - Array.to_list (Array.map (Array.get var_i) best) - - (* - force_ordering : id list -> (float * id list) list -> id list - - Determine a good ordering for enumerate variables based on the FORCE algorithm - *) - let force_ordering vars groups = - let var_i = Array.of_list vars in - let n = Array.length var_i in - - let i_var = Hashtbl.create n in - Array.iteri (fun i v -> Hashtbl.add i_var v i) var_i; - Hashtbl.add i_var "#BEGIN" (-1); - - let ngroups = List.map - (fun (w, l) -> w, List.map (Hashtbl.find i_var) l) - groups in - - let ord = Array.init n (fun i -> i) in - - for iter = 0 to 500 do - let rev = Array.make n (-1) in - for i = 0 to n-1 do rev.(ord.(i)) <- i done; - - let bw = Array.make n 0. in - let w = Array.make n 0. in - let gfun (gw, l) = - let sp = List.fold_left (+.) 0. - (List.map - (fun i -> if i = -1 then -.gw else float_of_int (rev.(i))) l) - in - let b = sp /. float_of_int (List.length l) in - List.iter (fun i -> if i >= 0 then begin - bw.(i) <- bw.(i) +. (gw *. b); - w.(i) <- w.(i) +. gw end) - l - in - List.iter gfun ngroups; - - let b = Array.init n - (fun i -> - if w.(i) = 0. then - float_of_int i - else bw.(i) /. w.(i)) in - - let ol = List.sort - (fun i j -> Pervasives.compare b.(i) b.(j)) - (Array.to_list ord) in - Array.blit (Array.of_list ol) 0 ord 0 n - done; - List.map (Array.get var_i) (Array.to_list ord) (* init_env : cmdline_opt -> rooted_prog -> env @@ -941,81 +790,10 @@ end = struct guarantees; Format.printf "@."; - (* add variables from LASTs *) - let last_vars = uniq_sorted (List.sort compare (Transform.extract_last_vars f_g)) in - let last_vars = List.map - (fun id -> - let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars - in false, id, ty) - last_vars in - let all_vars = last_vars @ rp.all_vars in - - Format.printf "Vars: @[<hov>%a@]@.@." - (print_list Ast_printer.print_typed_var ", ") - all_vars; - - let num_vars, enum_vars = List.fold_left - (fun (nv, ev) (_, id, t) -> match t with - | TEnum ch -> nv, (id, ch)::ev - | TInt -> (id, false)::nv, ev - | TReal -> (id, true)::nv, ev) - ([], []) all_vars in - - - (* calculate order for enumerated variables *) - let evars = List.map fst enum_vars in - - let lv = extract_linked_evars_root cl_g in - let lv = uniq_sorted - (List.sort Pervasives.compare (List.map ord_couple lv)) in - - let lv_f = List.map (fun (a, b) -> (1.0, [a; b])) lv in - let lv_f = lv_f @ (List.map (fun v -> (10.0, ["#BEGIN"; v])) - (extract_const_vars_root cl)) in - let lv_f = lv_f @ (List.map (fun v -> (5.0, ["#BEGIN"; v])) - (List.filter (fun n -> is_suffix n "init") evars)) in - let lv_f = lv_f @ (List.map (fun v -> (3.0, ["#BEGIN"; v])) - (List.filter (fun n -> is_suffix n "state") evars)) in - let lv_f = lv_f @ - (List.map (fun v -> (0.7, [v; "L"^v])) - (List.filter (fun n -> List.mem ("L"^n) evars) evars)) in - let evars_ord = - if true then - time "FORCE" (fun () -> force_ordering evars lv_f) - else - time "SCA" (fun () -> scope_constrict evars lv) - in - - let evars_ord = - if false then - 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 - (List.rev va) @ vb @ vc - else - evars_ord - in - - let ev_order = Hashtbl.create (List.length evars) in - List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord; - let ve = { evars = enum_vars; nvars = num_vars; ev_order } in - - Format.printf "Order for variables: @[<hov>[%a]@]@." - (print_list Formula_printer.print_id ", ") evars_ord; - - (* calculate cycle variables and forget variables *) - let cycle = List.fold_left - (fun q (_, id, ty) -> - if id.[0] = 'L' then - (id, String.sub id 1 (String.length id - 1), ty)::q - else q) - [] last_vars - in - let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in + let ve = mk_varenv rp f_g cl_g in - { rp; opt; ve; last_vars; all_vars; - init_cl; cl; cl_g; guarantees; - cycle; forget } + { rp; opt; ve; init_cl; cl; cl_g; guarantees; } @@ -1031,7 +809,7 @@ end = struct Format.printf "It. %d : full iteration.@." n; let d2 = edd_apply_cl x e.cl in - let dc = pass_cycle e d2 in + let dc = pass_cycle e.ve d2 in if dc.root = DBot then begin Format.printf "@.WARNING: contradictory hypotheses!@.@."; x @@ -1064,7 +842,7 @@ end = struct Format.printf "i %a@.i' %a@.j %a@." edd_print i edd_print i' edd_print j; - let q = edd_join start (pass_cycle e j) in + let q = edd_join start (pass_cycle e.ve j) in edd_meet path q in @@ -1082,7 +860,7 @@ end = struct let z = fix edd_eq f y in - let fj = pass_cycle e (edd_apply_cl z e.cl) in + let fj = pass_cycle e.ve (edd_apply_cl z e.cl) in if fj.root = DBot then begin Format.printf "@.WARNING: contradictory hypotheses!@.@."; x @@ -1098,7 +876,7 @@ end = struct Format.printf "Calculating initial state...@."; let init_acc = edd_star_new (edd_bot e.ve) - (pass_cycle e (edd_apply_cl (edd_top e.ve) e.init_cl)) in + (pass_cycle e.ve (edd_apply_cl (edd_top e.ve) e.init_cl)) in (* Dump final state *) let acc = ch_it 0 init_acc in @@ -1128,13 +906,13 @@ end = struct end; (* Examine probes *) - if List.exists (fun (p, _, _) -> p) e.all_vars then begin + if List.exists (fun (p, _, _) -> p) e.ve.all_vars then begin let final_flat = edd_forget_vars final (List.fold_left (fun l (_, id, ty) -> match ty with | TInt | TReal -> l | TEnum _ -> id::l) - [] e.all_vars) in + [] e.ve.all_vars) in let final_flat = match final_flat.root with | DTop -> ND.top e.ve.nvars | DBot -> ND.bottom e.ve.nvars @@ -1150,7 +928,7 @@ end = struct ND.print_itv (ND.project final_flat id) | TEnum _ -> Format.printf "%a : enum variable@." Formula_printer.print_id id) - e.all_vars; + e.ve.all_vars; Format.printf "@]@." end |