summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-10 13:29:01 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-10 13:29:01 +0200
commit354e8ed50b1fc1b6dadc1a2a8d54837b5b47e6be (patch)
treed03fdc47b1ce033be3edf79c8c0248bc7704f691
parentfee760b5c08afa9c81b5f28b35afd3514f643770 (diff)
downloadscade-analyzer-354e8ed50b1fc1b6dadc1a2a8d54837b5b47e6be.tar.gz
scade-analyzer-354e8ed50b1fc1b6dadc1a2a8d54837b5b47e6be.zip
DP locations defined by abstract values and not by formula.
-rw-r--r--abstract/abs_interp_dynpart.ml179
-rw-r--r--abstract/formula.ml20
-rw-r--r--cmdline.ml5
-rw-r--r--main.ml9
4 files changed, 121 insertions, 92 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 1adc430..32ed890 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -21,9 +21,9 @@ end = struct
type location = {
id : int;
+ depth : int;
- mutable def : bool_expr list; (* conjunction of formula *)
- mutable def_cl : conslist;
+ mutable def : abs_v;
is_init : bool;
mutable f : bool_expr;
@@ -108,22 +108,45 @@ end = struct
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)
- | CLFalse ->
- (ED.vtop enum, ND.vbottom num)
- | CLAnd(a, b) ->
- let enum, num = apply_cl (enum, num) (ec, nc, a) in
- let enum, num = apply_cl (enum, num) ([], nc, b) in
- enum, num
- | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
- let a = apply_cl (enum, num) (ec@eca, nc@nca, ra) in
- let b = apply_cl (enum, num) (ec@ecb, nc@ncb, rb) in
- join a b
+ begin match r with
+ | CLTrue ->
+ begin
+ try (ED.apply_cl enum ec, ND.apply_cl num nc)
+ with Bot -> ED.vtop enum, ND.vbottom num
end
- with Bot -> ED.vtop enum, ND.vbottom num
+ | CLFalse ->
+ (ED.vtop enum, ND.vbottom num)
+ | CLAnd(a, b) ->
+ let enum, num = apply_cl (enum, num) (ec, nc, a) in
+ let enum, num = apply_cl (enum, num) ([], nc, b) in
+ enum, num
+ | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+ let a = apply_cl (enum, num) (ec@eca, nc@nca, ra) in
+ let b = apply_cl (enum, num) (ec@ecb, nc@ncb, rb) in
+ join a b
+ end
+
+ (*
+ apply_cl_all_cases : abs_v -> conslist -> abs_v list
+ *)
+ let rec apply_cl_all_cases v (ec, nc, r) =
+ match r with
+ | CLTrue ->
+ let v =
+ try ED.apply_cl (fst v) ec, ND.apply_cl (snd v) nc
+ with Bot -> ED.vtop (fst v), ND.vbottom (snd v)
+ in
+ if is_bot v then [] else [v]
+ | CLFalse ->
+ []
+ | CLAnd(a, b) ->
+ let q1 = apply_cl_all_cases v (ec, nc, a) in
+ List.flatten
+ (List.map (fun c -> apply_cl_all_cases c ([], [], b)) q1)
+ | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+ let la = apply_cl_all_cases v (ec@eca, nc@nca, ra) in
+ let lb = apply_cl_all_cases v (ec@ecb, nc@ncb, rb) in
+ lb@(List.filter (fun a -> not (List.exists (fun b -> eq_v a b) lb)) la)
(* ***************************
@@ -190,17 +213,17 @@ end = struct
loc = Hashtbl.create 2; counter = ref 2; } in
(* add initial disjunction : L/must_reset = tt, L/must_reset ≠ tt *)
- let rstc = [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] in
- let rstf = simplify_k rstc f in
+ let rstc = BEnumCons(E_EQ, "L/must_reset", EItem bool_true) in
+ let rstf = simplify_k [rstc] f in
let rstf = simplify_k (get_root_true rstf) rstf in
- let nrstc = [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] in
- let nrstf = simplify_k nrstc f in
+ let nrstc = BEnumCons(E_NE, "L/must_reset", EItem bool_true) in
+ let nrstf = simplify_k [nrstc] f in
let nrstf = simplify_k (get_root_true nrstf) nrstf in
Hashtbl.add env.loc 0
{
id = 0;
- def = rstc;
- def_cl = conslist_of_f (f_and_list rstc);
+ depth = 0;
+ def = apply_cl (top env) (conslist_of_f rstc);
is_init = true;
f = rstf;
@@ -215,8 +238,8 @@ end = struct
Hashtbl.add env.loc 1
{
id = 1;
- def = nrstc;
- def_cl = conslist_of_f (f_and_list nrstc);
+ depth = 0;
+ def = apply_cl (top env) (conslist_of_f nrstc);
is_init = false;
f = nrstf;
@@ -282,23 +305,24 @@ end = struct
(ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
- let set_target_case e v cl =
- let tgt = (unpass_cycle e (apply_cl (top e) cl)) in
- (*Format.printf "Target %a = %a@." Formula_printer.print_conslist cl print_v tgt;*)
- meet v tgt
-
(*
print_locs : env -> unit
*)
+ let print_locs_defs e =
+ Hashtbl.iter
+ (fun id loc ->
+ Format.printf "q%d: @[<v 2>%a@]@." id print_v loc.def;
+ )
+ e.loc
+
let print_locs e =
Hashtbl.iter
(fun id loc ->
Format.printf "@.";
- Format.printf "q%d: @[<v 2>[ %a ]@]@." id
- (print_list Formula_printer.print_expr " ∧ ") loc.def;
+ Format.printf "q%d (depth = %d):@. D: @[<v 2>%a@]@." id loc.depth print_v loc.def;
(*Format.printf " F: (%a)@." Formula_printer.print_expr loc.f;*)
- Format.printf " %a@." print_v loc.v;
+ Format.printf " V: %a@." print_v loc.v;
Format.printf " -> @[<hov>[%a]@]@."
(print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
)
@@ -325,7 +349,7 @@ end = struct
loc.v <- bottom e)
e.loc;
- print_locs e;
+ print_locs_defs e;
(* Iterate *)
let it_counter = ref 0 in
@@ -339,11 +363,11 @@ end = struct
let start = loc.v in
let f i =
(*Format.printf "I: %a@." print_v i;*)
- let i' = set_target_case e i loc.def_cl in
+ let i' = meet i (unpass_cycle e loc.def) in
(*Format.printf "I': %a@." print_v i';*)
let j = join start
(apply_cl
- (apply_cl (pass_cycle e.ve i') loc.def_cl)
+ (meet (pass_cycle e.ve i') loc.def)
loc.cl) in
(*Format.printf "J: %a@." print_v j;*)
j
@@ -372,7 +396,7 @@ end = struct
Hashtbl.iter
(fun t loc2 ->
- let v = apply_cl u loc2.def_cl in
+ let v = meet u loc2.def in
let w = apply_cl v loc2.cl in
(*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*)
if not (is_bot w) then begin
@@ -384,9 +408,9 @@ end = struct
then loc.out_t <- t::loc.out_t;
if not (subset_v w loc2.v) then begin
if loc2.in_c < e.opt.widen_delay then
- loc2.v <- join w loc2.v
+ loc2.v <- join loc2.v w
else
- loc2.v <- widen w loc2.v;
+ loc2.v <- widen loc2.v w;
loc2.in_c <- loc2.in_c + 1;
if not (List.mem t !delta)
then delta := t::!delta
@@ -438,10 +462,7 @@ end = struct
then BNot cond
else cond
in
- if not (List.mem tr loc.def) then begin
- loc.def <- tr::loc.def;
- loc.def_cl <- conslist_of_f (f_and_list loc.def);
- end;
+ loc.def <- apply_cl loc.def (conslist_of_f tr);
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;
@@ -453,31 +474,17 @@ end = struct
(* find splitting condition *)
Hashtbl.iter
(fun q (loc:location) ->
- if !qc = None then
+ if !qc = None && loc.depth < e.opt.max_dp_depth then
let cs = ternary_conds loc.f in
List.iter
(fun c ->
- let split_e_case_fold_aux cases c =
- match c with
- | BEnumCons(op, x, EItem _) ->
- let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
- (List.map (fun v -> BEnumCons(E_EQ, x, EItem v))
- (List.filter (op x) (List.assoc x e.ve.evars)))
- @cases
- | _ -> c::cases
- in
- let cases_t =
- List.fold_left split_e_case_fold_aux []
- [c] in
- let cases_f =
- List.fold_left split_e_case_fold_aux []
- [eliminate_not_negate c] in
+ let cases_t = apply_cl_all_cases (top e) (conslist_of_f c) in
+ let cases_f = apply_cl_all_cases (top e) (conslist_of_f (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))))
+ (fun case -> not (is_bot (meet loc.v case)))
cases)
>= 2
&&
@@ -485,20 +492,20 @@ end = struct
(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)
+ (meet (pass_cycle e.ve loci.v) loc.def)
loc.cl in
List.exists
- (fun case -> is_bot (apply_cl v (conslist_of_f case)))
+ (fun case -> is_bot (meet v case))
cases)
loc.in_t
|| List.exists
(fun case ->
- let v = apply_cl loc.v (conslist_of_f case) in
+ let v = meet loc.v 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)
+ (meet (pass_cycle e.ve v) loco.def)
loco.cl in
is_bot w)
loc.out_t)
@@ -510,27 +517,27 @@ end = struct
)
e.loc;
- (*if n < 7 then*)
+ if Hashtbl.length e.loc < e.opt.max_dp_width then
match !qc with
| None ->
- Format.printf "@.Found no more possible refinement."
+ 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);
+ (print_list print_v ", ") (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
+ if not (is_bot (meet loc.v 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));
+ depth = loc.depth + 1;
+ def = meet loc.def case;
f = ff;
cl = conslist_of_f ff } in
Hashtbl.add e.loc loc2.id loc2
@@ -539,6 +546,34 @@ end = struct
List.iter (handle_case (BNot c)) cases_f;
iter (n+1)
- in iter 0
+ in iter 0;
+
+ (* Check guarantees *)
+ let check_guarantee (id, f) =
+ Format.printf "@[<v 4>";
+ let cl = Formula.conslist_of_f f in
+ Format.printf "%s:@ %a ⇒ ⊥ @ "
+ id Formula_printer.print_conslist cl;
+ let violate = ref [] in
+ Hashtbl.iter
+ (fun id loc ->
+ if not (is_bot (apply_cl loc.v cl)) then
+ violate := id::!violate)
+ e.loc;
+ if !violate = [] then
+ Format.printf "OK"
+ else
+ Format.printf "VIOLATED in @[<hov 2>[ %a ]@]"
+ (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") !violate;
+ Format.printf "@]@ ";
+ in
+ if e.guarantees <> [] then begin
+ Format.printf "Guarantee @[<v 0>";
+ List.iter check_guarantee e.guarantees;
+ Format.printf "@]@."
+ end
+
+
+
end
diff --git a/abstract/formula.ml b/abstract/formula.ml
index a124a84..f2a3bd1 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -263,23 +263,3 @@ 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
- | BTernary(c, a, b) ->
- true, (BAnd(c, a))::(BAnd(BNot c, b))::l
- | x -> u, x::l)
- (false, []) c
- in
- if u then split_cases l else l
diff --git a/cmdline.ml b/cmdline.ml
index b8f8ea8..c82b35b 100644
--- a/cmdline.ml
+++ b/cmdline.ml
@@ -2,7 +2,12 @@ open Ast
type cmdline_opt = {
widen_delay : int;
+
disjunct : (id -> bool);
+
verbose_ci : bool;
vverbose_ci : bool;
+
+ max_dp_width : int;
+ max_dp_depth : int;
}
diff --git a/main.ml b/main.ml
index 303723d..f85f6fb 100644
--- a/main.ml
+++ b/main.ml
@@ -47,6 +47,8 @@ let ai_widen_delay = ref 5
let ai_no_time_scopes = ref "all"
let ai_init_scopes = ref "all"
let ai_disj_v = ref ""
+let ai_max_dp_depth = ref 10
+let ai_max_dp_width = ref 100
let ai_vci = ref false
let ai_vvci = ref false
let ifile = ref ""
@@ -91,6 +93,11 @@ let options = [
"--ai-wd", Arg.Set_int ai_widen_delay,
"Widening delay in abstract analysis of loops (default: 3).";
+ "--ai-max-dp-depth", Arg.Set_int ai_max_dp_depth,
+ "Maximum depth in the dynamic partitionning tree.";
+ "--ai-max-dp-width", Arg.Set_int ai_max_dp_width,
+ "Maximum number of dynamically partitionned locations.";
+
"--root", Arg.Set_string ai_root,
"Root node for abstract analysis (default: test).";
"--no-time", Arg.Set_string ai_no_time_scopes,
@@ -178,6 +185,8 @@ let () =
disjunct = disj;
verbose_ci = !ai_vci;
vverbose_ci = !ai_vvci;
+ max_dp_width = !ai_max_dp_width;
+ max_dp_depth = !ai_max_dp_depth;
} in
if !ai_itv then AI_Itv.do_prog opt rp;