diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp.ml | 35 |
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 |