summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp_edd.ml256
-rw-r--r--abstract/enum_domain_edd.ml5
-rw-r--r--abstract/transform.ml20
-rw-r--r--abstract/varenv.ml252
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 }
+