diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp.ml | 196 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 14 |
2 files changed, 111 insertions, 99 deletions
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: @[<hov>%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: @[<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 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,51 +335,26 @@ 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 *) let cycle st cl env = @@ -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 "-> @[<hov>%a@]@." print_st st; - if st.opt.verbose_ci then - Format.printf "-> @[<hov>%a@]@." print_st st; - end + st.delta <- List.filter ((<>) case) st.delta; done; diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 35bdbfb..8ea0012 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -936,6 +936,14 @@ end = struct let init_cl = Formula.conslist_of_f init_f 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) -> + Format.printf " %s: %a@." id Formula_printer.print_expr f) + 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 -> @@ -955,12 +963,6 @@ end = struct | TReal -> (id, true)::nv, ev) ([], []) all_vars in - let guarantees = Transform.guarantees_of_prog rp in - Format.printf "Guarantees:@."; - List.iter (fun (id, f) -> - Format.printf " %s: %a@." id Formula_printer.print_expr f) - guarantees; - Format.printf "@."; (* calculate order for enumerated variables *) let evars = List.map fst enum_vars in |