diff options
Diffstat (limited to 'abstract/abs_interp_edd.ml')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 90 |
1 files changed, 48 insertions, 42 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 6220a0a..8ea0012 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -2,10 +2,10 @@ open Ast open Ast_util open Formula open Typing +open Cmdline open Util open Num_domain -open Abs_interp @@ -592,9 +592,12 @@ end = struct rp : rooted_prog; opt : cmdline_opt; + last_vars : (bool * id * typ) list; + all_vars : (bool * id * typ) list; ve : varenv; (* program expressions *) + init_cl : conslist; cl : conslist; cl_g : conslist; guarantees : (id * bool_expr) list; @@ -602,7 +605,6 @@ end = struct (* abstract interpretation *) cycle : (id * id * typ) list; (* s'(x) = s(y) *) forget : (id * typ) list; (* s'(x) not specified *) - mutable data : edd_v; } @@ -924,20 +926,15 @@ end = struct init_env : cmdline_opt -> rooted_prog -> env *) let init_env 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, 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; + Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; - let init_f = Transform.init_f_of_prog rp in - Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_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 + 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:@."; @@ -945,20 +942,32 @@ end = struct 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 -> + 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 - 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; + 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 - 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; (* calculate order for enumerated variables *) let evars = List.map fst enum_vars in - let lv = extract_linked_evars_root init_cl - @ extract_linked_evars_root cl_g in + let lv = extract_linked_evars_root cl_g in let lv = uniq_sorted (List.sort Pervasives.compare (List.map ord_couple lv)) in @@ -969,6 +978,9 @@ end = struct (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) @@ -995,25 +1007,17 @@ end = struct (* 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) + [] last_vars in + let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in - (* calculate initial environment *) - let data = edd_apply_cl (edd_top ve) init_cl in - Format.printf "Init: @[<hov>%a@]@." edd_print data; - { rp; opt; ve; - cl; cl_g; guarantees; - cycle; forget; data } + { rp; opt; ve; last_vars; all_vars; + init_cl; cl; cl_g; guarantees; + cycle; forget } @@ -1094,7 +1098,9 @@ end = struct end in - let init_acc = edd_star_new (edd_bot e.data.ve) e.data in + 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 (* Dump final state *) let acc = ch_it 0 init_acc in @@ -1124,13 +1130,13 @@ end = struct end; (* Examine probes *) - if List.exists (fun (p, _, _) -> p) e.rp.all_vars then begin + if List.exists (fun (p, _, _) -> p) e.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.rp.all_vars) in + [] e.all_vars) in let final_flat = match final_flat.root with | DTop -> ND.top e.ve.nvars | DBot -> ND.bottom e.ve.nvars @@ -1146,7 +1152,7 @@ end = struct ND.print_itv (ND.project final_flat id) | TEnum _ -> Format.printf "%a : enum variable@." Formula_printer.print_id id) - e.rp.all_vars; + e.all_vars; Format.printf "@]@." end |