summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--abstract/abs_interp_dynpart.ml237
-rw-r--r--abstract/formula.ml18
-rw-r--r--main.ml9
3 files changed, 221 insertions, 43 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 28f9238..c47fdc7 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -20,22 +20,21 @@ end = struct
type abs_v = ED.t * ND.t
type location = {
- id : int;
+ id : int;
- def : bool_expr list; (* conjunction of formula *)
- def_cl : conslist;
- is_init : bool;
+ mutable def : bool_expr list; (* conjunction of formula *)
+ mutable def_cl : conslist;
+ is_init : bool;
- f : bool_expr;
- cl : conslist;
+ mutable f : bool_expr;
+ mutable cl : conslist;
(* For chaotic iteration fixpoint *)
- mutable star : bool;
- mutable in_c : int;
- mutable v : abs_v;
+ mutable in_c : int;
+ mutable v : abs_v;
- mutable out_t : int list;
- mutable in_t : int list;
+ mutable out_t : int list;
+ mutable in_t : int list;
}
type env = {
@@ -69,16 +68,23 @@ end = struct
if is_bot (enum, num) then
Format.fprintf fmt "⊥"
else
- Format.fprintf fmt "@[<hov 4>(%a,@ %a)@]" ED.print enum ND.print num
+ Format.fprintf fmt "@[<hov 1>(%a,@ %a)@]" ED.print enum ND.print num
(*
join : abs_v -> abs_v -> abs_v
+ widen : abs_v -> abs_v -> abs_v
meet : abs_v -> abs_v -> abs_v
*)
let join (e1, n1) (e2, n2) =
if is_bot (e1, n1) then (e2, n2)
else if is_bot (e2, n2) then (e1, n1)
else (ED.join e1 e2, ND.join n1 n2)
+
+ let widen (e1, n1) (e2, n2) =
+ if is_bot (e1, n1) then (e2, n2)
+ else if is_bot (e2, n2) then (e1, n1)
+ else (ED.join e1 e2, ND.widen n1 n2)
+
let meet (e1, n1) (e2, n2) =
if is_bot (e1, n1) then ED.vtop e1, ND.vbottom n1
else if is_bot (e2, n2) then ED.vtop e2, ND.vbottom n2
@@ -87,13 +93,26 @@ end = struct
with Bot -> e1, ND.vbottom n1
(*
+ eq_v : abs_v -> abs_v -> bool
+ subset_v : abs_v -> abs_v -> bool
+ *)
+ let eq_v (a, b) (c, d) = (ND.is_bot b && ND.is_bot d) || (ED.eq a c && ND.eq b d)
+
+ let subset_v (a, b) (c, d) =
+ ND.is_bot b ||
+ (not (ND.is_bot d) && ED.subset a c && ND.subset b d)
+
+ (*
apply_cl : abs_v -> conslist -> abs_v
*)
let rec apply_cl (enum, num) (ec, nc, r) =
try
begin match r with
| CLTrue ->
- (ED.apply_cl enum ec, ND.apply_cl num nc)
+ let enum =
+ fix ED.eq (fun v -> ED.apply_cl v ec) enum
+ in
+ (enum, ND.apply_cl num nc)
| CLFalse ->
(enum, ND.vbottom num)
| CLAnd(a, b) ->
@@ -188,7 +207,6 @@ end = struct
f = rstf;
cl = conslist_of_f rstf;
- star = false;
in_c = 0;
v = (ED.top ve.evars, ND.bottom ve.nvars);
@@ -205,7 +223,6 @@ end = struct
f = nrstf;
cl = conslist_of_f nrstf;
- star = false;
in_c = 0;
v = (ED.top ve.evars, ND.bottom ve.nvars);
@@ -216,6 +233,14 @@ end = struct
(*
+ ternary_conds : bool_expr -> bool_expr list
+ *)
+ let rec ternary_conds = function
+ | BAnd(a, b) -> ternary_conds a @ ternary_conds b
+ | BTernary(c, a, b) -> [c]
+ | _ -> []
+
+ (*
pass_cycle : env -> edd_v -> edd_v
unpass_cycle : env -> edd_v -> edd_v
@@ -276,6 +301,7 @@ end = struct
(fun q loc ->
loc.out_t <- [];
loc.in_t <- [];
+ loc.in_c <- 0;
if loc.is_init then begin
loc.v <- apply_cl (top e) loc.cl;
delta := q::!delta
@@ -302,24 +328,21 @@ end = struct
j
in
- let rec iter n (i_enum, i_num) =
- let fi_enum, fi_num = f (i_enum, i_num) in
- let j_enum, j_num =
- if ND.is_bot fi_num then
- i_enum, i_num
- else
+ let rec iter n i =
+ let fi = f i in
+ let j =
if n < e.opt.widen_delay then
- ED.join i_enum fi_enum, ND.join i_num fi_num
+ join i fi
else
- ED.join i_enum fi_enum, ND.widen i_num fi_num
+ widen i fi
in
- if ED.eq j_enum i_enum && ND.eq j_num i_num
- then (i_enum, i_num)
- else iter (n+1) (j_enum, j_num)
+ if eq_v i j
+ then i
+ else iter (n+1) j
in
let y = iter 0 start in
- let z = fix (fun (a, b) (c, d) -> ED.eq a c && ND.eq b d) f y in
- Format.printf "Fixpoint: %a@." print_v z;
+ let z = fix eq_v f y in
+ (*Format.printf "Fixpoint: %a@." print_v z;*)
loc.v <- z;
@@ -331,16 +354,17 @@ end = struct
(*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*)
let r_enum, r_num = w in
if not (is_bot (r_enum, r_num)) then begin
- Format.printf "%d -> %d with:@. %a@." s t print_v (r_enum, r_num);
+ (*Format.printf "%d -> %d with:@. %a@." s t print_v (r_enum, r_num);*)
if not (List.mem s loc2.in_t)
then loc2.in_t <- s::loc2.in_t;
if not (List.mem t loc.out_t)
then loc.out_t <- t::loc.out_t;
- let enum, num = loc2.v in
- let enum2, num2 = join (enum, num) (r_enum, r_num) in
- if not (ED.subset enum2 enum) || not (ND.subset num2 num) then
- begin
- loc2.v <- (enum2, num2);
+ if not (subset_v (r_enum, r_num) loc2.v) then begin
+ if loc2.in_c < e.opt.widen_delay then
+ loc2.v <- join (r_enum, r_num) loc2.v
+ else
+ loc2.v <- widen (r_enum, r_num) loc2.v;
+ loc2.in_c <- loc2.in_c + 1;
if not (List.mem t !delta)
then delta := t::!delta
end
@@ -348,18 +372,28 @@ end = struct
e.loc;
delta := List.filter ((<>) s) !delta;
- done
+ done;
+
+ (* remove useless locations *)
+ let useless = ref [] in
+ Hashtbl.iter
+ (fun i loc ->
+ if is_bot loc.v then begin
+ Format.printf "Useless location detected: q%d@." i;
+ useless := i::!useless
+ end)
+ e.loc;
+ List.iter (Hashtbl.remove e.loc) !useless
let print_locs e =
Hashtbl.iter
(fun id loc ->
Format.printf "@.";
- Format.printf "q%d: @[<hov 4>[ %a ]@]@." id
+ Format.printf "q%d: @[<v 2>[ %a ]@]@." id
(print_list Formula_printer.print_expr " ∧ ") loc.def;
- (*Format.printf "F: %a@." Formula_printer.print_conslist loc.cl;*)
- Format.printf " @[<hv 0>%a ∧@ %a@]@."
- ED.print (fst loc.v) ND.print (snd loc.v);
+ (*Format.printf " F: (%a)@." Formula_printer.print_expr loc.f;*)
+ Format.printf " %a@." print_v loc.v;
Format.printf " -> @[<hov>[%a]@]@."
(print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
)
@@ -368,8 +402,127 @@ end = struct
let do_prog opt rp =
let e = init_env opt rp in
- Format.printf "@.Initializing.@.";
- chaotic_iter e;
- print_locs e
+ let rec iter n =
+ Format.printf "@.--------------@.Refinement #%d@." n;
+
+ chaotic_iter e;
+ print_locs e;
+
+ let qc = ref None in
+
+ (* put true or false conditions into location definition *)
+ Hashtbl.iter
+ (fun q (loc : location) ->
+ let rec iter () =
+ try
+ let cond = List.find
+ (fun c ->
+ is_bot (apply_cl loc.v (conslist_of_f c))
+ || is_bot (apply_cl loc.v (conslist_of_f (BNot c))))
+ (ternary_conds loc.f)
+ in
+ let tr =
+ if is_bot (apply_cl loc.v (conslist_of_f cond))
+ then BNot cond
+ else cond
+ in
+ loc.def <- tr::loc.def;
+ loc.def_cl <- conslist_of_f (f_and_list loc.def);
+ loc.f <- simplify_k [tr] loc.f;
+ loc.f <- simplify_k (get_root_true loc.f) loc.f;
+ loc.cl <- conslist_of_f loc.f;
+ iter()
+ with Not_found -> ()
+ in iter ())
+ e.loc;
+
+ (* find splitting condition *)
+ Hashtbl.iter
+ (fun q (loc:location) ->
+ if !qc = None then
+ let cs = ternary_conds loc.f in
+ List.iter
+ (fun c ->
+ let split_e_case_fold_aux cases c =
+ match c with
+ | BEnumCons(_, x, EItem _) ->
+ (List.map (fun v -> BEnumCons(E_EQ, x, EItem v))
+ (List.assoc x e.ve.evars))@cases
+ | _ -> c::cases
+ in
+ let cases_t =
+ List.fold_left split_e_case_fold_aux []
+ (split_cases [c]) in
+ let cases_f =
+ List.fold_left split_e_case_fold_aux []
+ (split_cases [BNot c]) in
+ let cases = cases_t @ cases_f in
+ if
+ List.length
+ (List.filter
+ (fun case ->
+ not (is_bot (apply_cl loc.v (conslist_of_f case))))
+ cases)
+ >= 2
+ &&
+ (List.exists
+ (fun qi ->
+ let loci = Hashtbl.find e.loc qi in
+ let v = apply_cl
+ (apply_cl (pass_cycle e.ve loci.v) loc.def_cl)
+ loc.cl in
+ List.exists
+ (fun case -> is_bot (apply_cl v (conslist_of_f case)))
+ cases)
+ loc.in_t
+ || List.exists
+ (fun case ->
+ let v = apply_cl loc.v (conslist_of_f case) in
+ List.exists
+ (fun qo ->
+ let loco = Hashtbl.find e.loc qo in
+ let w = apply_cl
+ (apply_cl (pass_cycle e.ve v) loco.def_cl)
+ loco.cl in
+ is_bot w)
+ loc.out_t)
+ cases)
+ then
+ qc := Some(q, c, cases_t, cases_f)
+ )
+ cs
+ )
+ e.loc;
+
+ (*if n < 7 then*)
+ match !qc with
+ | None ->
+ Format.printf "@.Found no more possible refinement."
+ | Some (q, c, cases_t, cases_f) ->
+ Format.printf "@.Refine q%d : @[<v 2>[ %a ]@]@." q
+ (print_list Formula_printer.print_expr ", ") (cases_t@cases_f);
+
+ let loc = Hashtbl.find e.loc q in
+ Hashtbl.remove e.loc loc.id;
+
+ let handle_case cc case =
+ if not (is_bot (apply_cl loc.v (conslist_of_f case))) then
+ let ff = simplify_k [cc] loc.f in
+ let ff = simplify_k (get_root_true ff) ff in
+
+ let loc2 =
+ { loc with
+ id = (incr e.counter; !(e.counter));
+ def = case::loc.def;
+ def_cl = conslist_of_f (f_and_list (case::loc.def));
+ f = ff;
+ cl = conslist_of_f ff } in
+ Hashtbl.add e.loc loc2.id loc2
+ in
+ List.iter (handle_case c) cases_t;
+ List.iter (handle_case (BNot c)) cases_f;
+
+ iter (n+1)
+ in iter 0
end
diff --git a/abstract/formula.ml b/abstract/formula.ml
index f2a3bd1..5cbe0c9 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -263,3 +263,21 @@ let rec formula_replace_evars repls e =
| x -> x
+
+(*
+ Extract all cases that make a formula true, to a limited degree
+
+ [A || B; not (A || B)] -> A; (B && (not A)); not A && not B]
+*)
+
+let rec split_cases c =
+ let c = List.map eliminate_not c in
+ let u, l = List.fold_left
+ (fun (u, l) c ->
+ match c with
+ | BOr(a, b) ->
+ true, a::(BAnd(BNot a, b))::l
+ | x -> u, x::l)
+ (false, []) c
+ in
+ if u then split_cases l else l
diff --git a/main.ml b/main.ml
index 339a433..96fb95e 100644
--- a/main.ml
+++ b/main.ml
@@ -21,6 +21,8 @@ module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND)
module AI_S_Itv_DP = Abs_interp_dynpart.I
(Enum_domain.MultiValuation)(ItvND)
+module AI_S_Rel_DP = Abs_interp_dynpart.I
+ (Enum_domain.MultiValuation)(Apron_domain.ND)
(* command line options *)
let times = ref false
@@ -33,6 +35,7 @@ let ai_rel = ref false
let ai_itv_edd = ref false
let ai_rel_edd = ref false
let ai_s_itv_dp = ref false
+let ai_s_rel_dp = ref false
let ai_root = ref "test"
let ai_widen_delay = ref 5
let ai_no_time_scopes = ref "all"
@@ -60,6 +63,9 @@ let options = [
"--ai-s-itv-dp", Arg.Set ai_s_itv_dp,
"Do abstract analysis using dynamic partitionning method, "^
"with intervals and valuation domain for enums.";
+ "--ai-s-rel-dp", Arg.Set ai_s_rel_dp,
+ "Do abstract analysis using dynamic partitionning method, "^
+ "with Apron and valuation domain for enums.";
"--ai-vci", Arg.Set ai_vci,
"Verbose chaotic iterations (show state at each iteration)";
"--ai-vvci", Arg.Set ai_vvci,
@@ -126,7 +132,7 @@ let () =
if !ai_itv || !ai_rel
|| !ai_itv_edd || !ai_rel_edd
- || !ai_s_itv_dp then
+ || !ai_s_itv_dp || !ai_s_rel_dp then
begin
let comma_split = Str.split (Str.regexp ",") in
let select_f x =
@@ -161,6 +167,7 @@ let () =
if !ai_rel_edd then AI_Rel_EDD.do_prog opt rp;
if !ai_s_itv_dp then AI_S_Itv_DP.do_prog opt rp;
+ if !ai_s_rel_dp then AI_S_Rel_DP.do_prog opt rp;
end;
if !vtest then do_test_interpret prog true