summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--abstract/abs_interp.ml196
-rw-r--r--abstract/abs_interp_edd.ml14
-rw-r--r--main.ml17
3 files changed, 121 insertions, 106 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
diff --git a/main.ml b/main.ml
index 6cb2c50..2995e24 100644
--- a/main.ml
+++ b/main.ml
@@ -10,10 +10,8 @@ module Interpret = Interpret.I
module ItvND = Nonrelational.ND(Intervals_domain.VD)
-(*
module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND)
-*)
module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND)
@@ -109,9 +107,16 @@ let () =
if !ai_itv || !ai_rel || !ai_itv_edd || !ai_rel_edd then begin
let comma_split = Str.split (Str.regexp ",") in
let select_f x =
- if x = "all"
- then (fun _ -> true)
- else (fun i -> List.mem i (comma_split x))
+ if x = "all" then
+ (fun _ -> true)
+ else if x = "last" then
+ (fun i -> i.[0] = 'L')
+ else if String.length x > 5 && String.sub x 0 5 = "last+" then
+ let psl = comma_split
+ (String.sub x 5 (String.length x - 5)) in
+ (fun i -> i.[0] = 'L' || List.mem i psl)
+ else
+ (fun i -> List.mem i (comma_split x))
in
let rp = Typing.root_prog prog !ai_root
(select_f !ai_no_time_scopes)
@@ -126,10 +131,8 @@ let () =
vverbose_ci = !ai_vvci;
} in
- (*
if !ai_itv then AI_Itv.do_prog opt rp;
if !ai_rel then AI_Rel.do_prog opt rp;
- *)
if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
if !ai_rel_edd then AI_Rel_EDD.do_prog opt rp;