From 2cbaba6f00d40d5c6c9659678d0156f14b7e3780 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 4 Jul 2014 11:10:13 +0200 Subject: Use LAST instead of NEXT (only EDD implementation works at the moment) --- abstract/abs_interp.ml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'abstract/abs_interp.ml') diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index c3db657..26b788b 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -2,17 +2,12 @@ open Ast open Ast_util open Formula open Typing +open Cmdline open Util open Num_domain open Enum_domain -type cmdline_opt = { - widen_delay : int; - disjunct : (id -> bool); - verbose_ci : bool; - vverbose_ci : bool; -} module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig -- cgit v1.2.3 From 108f38029404e8eb4b37c8892345917edfb3cac7 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 4 Jul 2014 17:20:51 +0200 Subject: Adapt domain with non-EDD disjunctions ; it doesn't work very well ! --- abstract/abs_interp.ml | 196 ++++++++++++++++++++++++++----------------------- 1 file changed, 103 insertions(+), 93 deletions(-) (limited to 'abstract/abs_interp.ml') diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 26b788b..787c6d6 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -165,6 +165,7 @@ end = struct rp : rooted_prog; opt : cmdline_opt; + all_vars : (bool * id * typ) list; enum_vars : (id * ED.item list) list; num_vars : (id * bool) list; @@ -220,27 +221,68 @@ end = struct (ED.project enum p) in aux enum [] st.d_vars + + (* + dd_apply_cl : dd_v -> conslist -> dd_v + *) + let rec apply_cl_get_all_cases (enum, num) (ec, nc, r) = + match r with + | CLTrue -> + let enums = List.fold_left + (fun enums ec -> List.flatten + (List.map (fun e -> ED.apply_cons e ec) enums)) + [enum] ec in + let num = ND.apply_cl num nc in + List.map (fun ec -> ec, num) enums + | CLFalse -> [] + | CLAnd(a, b) -> + let envs = apply_cl_get_all_cases (enum, num) (ec, nc, a) in + List.flatten + (List.map (fun e -> apply_cl_get_all_cases e (ec, nc, b)) envs) + | CLOr((eca, nca, ra), (ecb, ncb, rb)) -> + apply_cl_get_all_cases (enum, num) (ec@eca, nc@nca, ra) @ + apply_cl_get_all_cases (enum, num) (ec@ecb, nc@ncb, rb) + + (* + pass_cycle : st -> case_v -> case_v + *) + let pass_cycle st (enum, num) = + let assign_e, assign_n = List.fold_left + (fun (ae, an) (a, b, t) -> match t with + | TEnum _ -> (a, b)::ae, an + | TInt | TReal -> ae, (a, NIdent b)::an) + ([], []) st.cycle in + + let enum = ED.assign enum assign_e in + let num = ND.assign num assign_n in + + List.fold_left + (fun (enum, num) (var, t) -> + let e, n = match t with + | TEnum _ -> ED.forgetvar enum var, num + | TReal | TInt -> enum, ND.forgetvar num var + in e, n) + (enum, num) st.forget + let dd_pass_cycle st (v : dd_v) = + let vv = dd_bot v.d_vars in + Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data; + vv (* init_state : int -> rooted_prog -> st *) let init_state opt rp = - Format.printf "Vars: @[%a@]@.@." - (print_list Ast_printer.print_typed_var ", ") - rp.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) - ([], []) rp.all_vars in - - let init_f = Transform.init_f_of_prog rp in + let init_f, f = Transform.f_of_prog rp false in + let _, f_g = Transform.f_of_prog rp true in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; - let init_cl = conslist_of_f init_f in + Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; + let init_cl = conslist_of_f init_f in + let cl = Formula.conslist_of_f f in + let cl_g = Formula.conslist_of_f f_g in + Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; + let guarantees = Transform.guarantees_of_prog rp in Format.printf "Guarantees:@."; List.iter (fun (id, f) -> @@ -248,46 +290,42 @@ end = struct guarantees; Format.printf "@."; - let f = Formula.eliminate_not (Transform.f_of_prog rp false) in - let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in - Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; - let cl = Formula.conslist_of_f f in - let cl_g = Formula.conslist_of_f f_g in - Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; + (* 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: @[%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 cycle variables and forget variables *) let cycle = List.fold_left (fun q (_, id, ty) -> - if id.[0] = 'N' then - (String.sub id 1 (String.length id - 1), id, ty)::q + if id.[0] = 'L' then + (id, String.sub id 1 (String.length id - 1), ty)::q else q) - [] rp.all_vars - in - let forget = List.map (fun (_, id, ty) -> (id, ty)) - (List.filter - (fun (_, id, _) -> - not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars)) - rp.all_vars) + [] all_vars in + let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in (* calculate disjunction variables *) - (* first approximation : use all enum variables appearing in init formula *) - let rec calculate_dvars (ec, _, r) = - let a = List.map (fun (_, id, _) -> id) ec in - let rec aux = function - | CLTrue | CLFalse -> [] - | CLAnd(u, v) -> - aux u @ aux v - | CLOr(u, v) -> - calculate_dvars u @ calculate_dvars v - in a @ aux r - in - let d_vars_0 = calculate_dvars init_cl in - let d_vars_1 = List.filter - (fun id -> opt.disjunct id && not (List.mem id d_vars_0) && id.[0] <> 'N') + (* 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 d_vars = d_vars_0 @ d_vars_1 in (* setup abstract data *) let top = ED.top enum_vars, ND.top num_vars in @@ -297,50 +335,25 @@ end = struct (* calculate initial state and environment *) let init_s = dd_bot d_vars in - let init_ec, _, _ = init_cl in - let init_ed = List.fold_left - (fun ed cons -> - List.flatten (List.map (fun x -> ED.apply_cons x cons) ed)) - [ED.top enum_vars] (init_ec) in - List.iter (fun ed -> dd_add_case init_s (ed, ND.top num_vars)) init_ed; - let env_dd = apply_cl init_s init_cl in - let env = env_dd.data 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; + { rp; opt; enum_vars; num_vars; all_vars; cl; cl_g; guarantees; cycle; forget; d_vars; top; - env; delta; widen } in + env = Hashtbl.create 1; delta; widen } in + + let env_dd_pass = dd_pass_cycle st env_dd in + let st = { st with env = env_dd_pass.data } in Hashtbl.iter (fun case _ -> st.delta <- case::st.delta) st.env; st - (* - pass_cycle : st -> case_v -> case_v - *) - let pass_cycle st (enum, num) = - let assign_e, assign_n = List.fold_left - (fun (ae, an) (a, b, t) -> match t with - | TEnum _ -> (a, b)::ae, an - | TInt | TReal -> ae, (a, NIdent b)::an) - ([], []) st.cycle in - - let enum = ED.assign enum assign_e in - let num = ND.assign num assign_n in - - List.fold_left - (fun (enum, num) (var, t) -> match t with - | TEnum _ -> ED.forgetvar enum var, num - | TReal | TInt -> enum, ND.forgetvar num var) - (enum, num) st.forget - - let dd_pass_cycle st (v : dd_v) = - let vv = dd_bot v.d_vars in - Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data; - vv - (* cycle : st -> cl -> dd_v -> dd_v *) @@ -407,23 +420,20 @@ end = struct let i = dd_singleton st.d_vars z in let j = cycle st st.cl i in - if Hashtbl.length j.data = 0 then - Format.printf "@.WARNING: contradictory hypotheses!@.@." - else begin - let cases = ref [] in - Hashtbl.iter (fun case _ -> cases := case::(!cases)) j.data; - List.iter - (fun case -> - let i' = set_target_case st i case in - let j = cycle st st.cl i' in - Hashtbl.iter (fun _ q -> add_case st q) j.data) - !cases; - st.delta <- List.filter ((<>) case) st.delta; + let cases = ref [] in + Hashtbl.iter (fun case _ -> cases := case::(!cases)) j.data; + List.iter + (fun case -> + let i' = set_target_case st i case in + let j = cycle st st.cl i' in + Hashtbl.iter (fun _ q -> add_case st q) j.data) + !cases; + + if st.opt.verbose_ci then + Format.printf "-> @[%a@]@." print_st st; - if st.opt.verbose_ci then - Format.printf "-> @[%a@]@." print_st st; - end + st.delta <- List.filter ((<>) case) st.delta; done; -- cgit v1.2.3 From 696d07415d52b092c9c69a9b1042a8bc9cd51a90 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 4 Jul 2014 17:48:09 +0200 Subject: Adapt non-EDD disjunction interpret to use two set of disjunction vars. --- abstract/abs_interp.ml | 35 +++++++++++++++-------------------- 1 file changed, 15 insertions(+), 20 deletions(-) (limited to 'abstract/abs_interp.ml') 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 -- cgit v1.2.3