summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp.ml35
1 files changed, 15 insertions, 20 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 787c6d6..cb5ae9c 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -177,7 +177,8 @@ end = struct
(* abstract interpretation *)
cycle : (id * id * typ) list; (* s'(x) = s(y) *)
forget : (id * typ) list; (* s'(x) not specified *)
- d_vars : id list; (* disjunction variables *)
+ d_vars : id list; (* disjunction variables when calculating *)
+ acc_d_vars : id list; (* disjunction variables in accumulator *)
top : case_v;
env : (case, case_v) Hashtbl.t;
mutable delta : case list;
@@ -187,7 +188,7 @@ end = struct
(*
print_st : Formatter.t -> st -> unit
*)
- let print_st fmt st = print_aux fmt st.d_vars st.env
+ let print_st fmt st = print_aux fmt st.acc_d_vars st.env
(*
add_case : st -> case_v -> unit
@@ -219,7 +220,7 @@ end = struct
| [en] -> aux en (v::vals) q
| _ -> assert false)
(ED.project enum p)
- in aux enum [] st.d_vars
+ in aux enum [] st.acc_d_vars
(*
@@ -265,7 +266,7 @@ end = struct
(enum, num) st.forget
let dd_pass_cycle st (v : dd_v) =
- let vv = dd_bot v.d_vars in
+ let vv = dd_bot st.acc_d_vars in
Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
vv
@@ -326,29 +327,23 @@ end = struct
(* actually, don't calculate them, rely on user input *)
let d_vars = List.filter (fun k -> k <> "/init" && opt.disjunct k)
(List.map (fun (id, _) -> id) enum_vars) in
+ let acc_d_vars = List.filter (fun i -> i.[0] = 'L') d_vars in
(* setup abstract data *)
let top = ED.top enum_vars, ND.top num_vars in
let delta = [] in
let widen = Hashtbl.create 12 in
- (* calculate initial state and environment *)
- let init_s = dd_bot d_vars in
-
- List.iter (fun ed -> dd_add_case init_s ed)
- (apply_cl_get_all_cases top init_cl);
-
- let env_dd = apply_cl init_s init_cl in (* useless refinement ? *)
-
let st =
{ rp; opt; enum_vars; num_vars; all_vars;
cl; cl_g; guarantees;
- cycle; forget; d_vars; top;
- env = Hashtbl.create 1; delta; widen } in
+ cycle; forget; acc_d_vars; d_vars; top;
+ env = Hashtbl.create 12; delta; widen } in
- let env_dd_pass = dd_pass_cycle st env_dd in
+ (* calculate initial state and environment *)
+ List.iter (fun ed -> add_case st (pass_cycle st ed))
+ (apply_cl_get_all_cases top init_cl);
- let st = { st with env = env_dd_pass.data } in
Hashtbl.iter (fun case _ -> st.delta <- case::st.delta) st.env;
st
@@ -370,10 +365,10 @@ end = struct
let set_target_case st env case =
List.fold_left2
(fun env id v ->
- if List.exists (fun (id2, _) -> id2 = "N"^id) st.enum_vars then
- dd_apply_econs env (E_EQ, "N"^id, EItem v)
+ if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then
+ dd_apply_econs env (E_EQ, id, EItem v)
else env)
- env st.d_vars case
+ env st.acc_d_vars case
(*
do_prog : rooted_prog -> unit
@@ -395,7 +390,7 @@ end = struct
(print_list Formula_printer.print_id ", ") case;
let start = try Hashtbl.find st.env case with Not_found -> assert false in
- let start_dd = dd_singleton st.d_vars start in
+ let start_dd = dd_singleton st.acc_d_vars start in
let f i =
let i = dd_singleton st.d_vars i in
let i' = set_target_case st i case in