diff options
| -rw-r--r-- | abstract/abs_interp_edd.ml | 256 | ||||
| -rw-r--r-- | abstract/enum_domain_edd.ml | 5 | ||||
| -rw-r--r-- | abstract/transform.ml | 20 | ||||
| -rw-r--r-- | abstract/varenv.ml | 252 |
4 files changed, 292 insertions, 241 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 diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml index a372772..47515eb 100644 --- a/abstract/enum_domain_edd.ml +++ b/abstract/enum_domain_edd.ml @@ -9,7 +9,7 @@ module type ENUM_ENVIRONMENT_DOMAIN2 = sig (* construction *) val top : (id * item list) list -> t - val bot : (id * item list) list -> t + val bottom : (id * item list) list -> t val is_bot : t -> bool (* variable management *) @@ -170,7 +170,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct let order = Hashtbl.create 12 in List.iteri (fun i (id, _) -> Hashtbl.add order id i) vars; { vars; order; root = DTop } - let bot vars = let t = top vars in { t with root = DBot } + + let bottom vars = let t = top vars in { t with root = DBot } (* is_bot : t -> bool diff --git a/abstract/transform.ml b/abstract/transform.ml index 480705f..e0f32c2 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -490,6 +490,26 @@ and f_of_prog rp assume_guarantees = f_and clock_eq scope_f in prog_init, prog_normal + +let f_of_prog_incl_init rp assume_guarantees = + let td = { + rp = rp; + consts = I.consts rp; + } in + + let init_cond = BEnumCons(E_EQ, "L/must_reset", bool_true) in + let no_next_init_cond = BEnumCons(E_EQ, "/must_reset", bool_false) in + + let clock_scope, clock_eq = gen_clock td rp.root_scope true [init_cond] in + + let scope_f = + f_of_scope + true + td td.rp.root_scope + clock_scope + assume_guarantees in + f_and clock_eq (f_and no_next_init_cond scope_f) + diff --git a/abstract/varenv.ml b/abstract/varenv.ml new file mode 100644 index 0000000..1aa17b4 --- /dev/null +++ b/abstract/varenv.ml @@ -0,0 +1,252 @@ +open Ast +open Util +open Typing +open Formula + + + +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; + + last_vars : (bool * id * typ) list; + all_vars : (bool * id * typ) list; + + cycle : (id * id * typ) list; (* s'(x) = s(y) *) + forget : (id * typ) list; (* s'(x) not specified *) +} + + + +(* + 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) + + +(* + Make varenv : takes a program, and extracts + - list of enum variables + - list of num variables + - good order for enum variables + - cycle, forget +*) + +let mk_varenv (rp : rooted_prog) f cl = + (* add variables from LASTs *) + let last_vars = uniq_sorted + (List.sort compare (Transform.extract_last_vars f)) 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 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; + + 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 + + { evars = enum_vars; nvars = num_vars; ev_order; + last_vars; all_vars; cycle; forget } + |