summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-10 10:58:56 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-10 10:58:56 +0200
commitfee760b5c08afa9c81b5f28b35afd3514f643770 (patch)
tree526f3e7d2c5da4e0132bf58797c0a9b4dccb8840
parente06a4102e5b2a81c7b1c24323cafc863eefbc0cb (diff)
downloadscade-analyzer-fee760b5c08afa9c81b5f28b35afd3514f643770.tar.gz
scade-analyzer-fee760b5c08afa9c81b5f28b35afd3514f643770.zip
Fix a few things, this doesn't work well.
-rw-r--r--abstract/abs_interp_dynpart.ml110
-rw-r--r--abstract/enum_domain.ml26
-rw-r--r--abstract/formula.ml2
-rw-r--r--main.ml26
-rw-r--r--tests/source/half.scade2
-rw-r--r--tests/source/updown2.scade2
6 files changed, 107 insertions, 61 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index c47fdc7..1adc430 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -62,7 +62,7 @@ end = struct
*)
let top e = (ED.top e.ve.evars, ND.top e.ve.nvars)
let bottom e = (ED.top e.ve.evars, ND.bottom e.ve.nvars)
- let is_bot (e, n) = ND.is_bot n
+ let is_bot (e, n) = ED.is_bot e || ND.is_bot n
let print_v fmt (enum, num) =
if is_bot (enum, num) then
@@ -75,32 +75,34 @@ end = struct
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 join a b =
+ if is_bot a then b
+ else if is_bot b then a
+ else (ED.join (fst a) (fst b), ND.join (snd a) (snd b))
- 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 widen a b =
+ if is_bot a then b
+ else if is_bot b then a
+ else (ED.join (fst a) (fst b), ND.widen (snd a) (snd b))
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
else
try (ED.meet e1 e2 , ND.meet n1 n2)
- with Bot -> e1, ND.vbottom n1
+ with Bot -> ED.vtop 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 eq_v (a, b) (c, d) =
+ (is_bot (a, b) && is_bot (c, 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)
+ (is_bot (a, b)) ||
+ (not (is_bot (c, d)) && ED.subset a c && ND.subset b d)
(*
apply_cl : abs_v -> conslist -> abs_v
@@ -109,12 +111,9 @@ end = struct
try
begin match r with
| CLTrue ->
- let enum =
- fix ED.eq (fun v -> ED.apply_cl v ec) enum
- in
- (enum, ND.apply_cl num nc)
+ (ED.apply_cl enum ec, ND.apply_cl num nc)
| CLFalse ->
- (enum, ND.vbottom num)
+ (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
@@ -289,6 +288,23 @@ end = struct
meet v tgt
(*
+ print_locs : env -> unit
+ *)
+
+ 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 " 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;
+ )
+ e.loc
+
+ (*
chaotic_iter : env -> unit
Fills the values of loc[*].v, and updates out_t and in_t
@@ -309,6 +325,8 @@ end = struct
loc.v <- bottom e)
e.loc;
+ print_locs e;
+
(* Iterate *)
let it_counter = ref 0 in
while !delta <> [] do
@@ -323,7 +341,10 @@ end = struct
(*Format.printf "I: %a@." print_v i;*)
let i' = set_target_case e i loc.def_cl in
(*Format.printf "I': %a@." print_v i';*)
- let j = join start (apply_cl (apply_cl (pass_cycle e.ve i') loc.def_cl) loc.cl) in
+ let j = join start
+ (apply_cl
+ (apply_cl (pass_cycle e.ve i') loc.def_cl)
+ loc.cl) in
(*Format.printf "J: %a@." print_v j;*)
j
in
@@ -342,28 +363,30 @@ end = struct
in
let y = iter 0 start in
let z = fix eq_v f y in
- (*Format.printf "Fixpoint: %a@." print_v z;*)
+ let u = pass_cycle e.ve z in
+
+ if e.opt.verbose_ci then
+ Format.printf "Fixpoint: %a@. mem fp: %a@." print_v z print_v u;
loc.v <- z;
Hashtbl.iter
(fun t loc2 ->
- let u = pass_cycle e.ve z in
let v = apply_cl u loc2.def_cl 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;*)
- 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);*)
+ if not (is_bot w) then begin
+ if e.opt.verbose_ci then
+ Format.printf "%d -> %d with:@. %a@." s t print_v w;
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;
- if not (subset_v (r_enum, r_num) loc2.v) then begin
+ if not (subset_v w loc2.v) then begin
if loc2.in_c < e.opt.widen_delay then
- loc2.v <- join (r_enum, r_num) loc2.v
+ loc2.v <- join w loc2.v
else
- loc2.v <- widen (r_enum, r_num) loc2.v;
+ loc2.v <- widen w loc2.v;
loc2.in_c <- loc2.in_c + 1;
if not (List.mem t !delta)
then delta := t::!delta
@@ -383,21 +406,11 @@ end = struct
useless := i::!useless
end)
e.loc;
- List.iter (Hashtbl.remove e.loc) !useless
+ List.iter (Hashtbl.remove e.loc) !useless;
+
+ print_locs e
- 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 " 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;
- )
- e.loc
let do_prog opt rp =
let e = init_env opt rp in
@@ -406,7 +419,6 @@ end = struct
Format.printf "@.--------------@.Refinement #%d@." n;
chaotic_iter e;
- print_locs e;
let qc = ref None in
@@ -426,8 +438,10 @@ end = struct
then BNot cond
else cond
in
- loc.def <- tr::loc.def;
- loc.def_cl <- conslist_of_f (f_and_list loc.def);
+ 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.f <- simplify_k [tr] loc.f;
loc.f <- simplify_k (get_root_true loc.f) loc.f;
loc.cl <- conslist_of_f loc.f;
@@ -445,17 +459,19 @@ end = struct
(fun c ->
let split_e_case_fold_aux cases c =
match c with
- | BEnumCons(_, x, EItem _) ->
+ | 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.assoc x e.ve.evars))@cases
+ (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 []
- (split_cases [c]) in
+ [c] in
let cases_f =
List.fold_left split_e_case_fold_aux []
- (split_cases [BNot c]) in
+ [eliminate_not_negate c] in
let cases = cases_t @ cases_f in
if
List.length
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index 4f6aacd..77d7e3f 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -119,11 +119,14 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
if cc op s t then [x] else []
let apply_cl x l =
- List.fold_left
- (fun k c -> match apply_cons k c with
- | [] -> raise Bot
- | p::q -> List.fold_left join p q )
- x l
+ let f x =
+ List.fold_left
+ (fun k c -> match apply_cons k c with
+ | [] -> raise Bot
+ | p::q -> List.fold_left join p q )
+ x l
+ in
+ fix eq f x
let assign x idl =
let v = List.fold_left
@@ -242,11 +245,14 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
[] v1
let apply_cl x l =
- List.fold_left
- (fun k c -> match apply_cons k c with
- | [] -> raise Bot
- | p::q -> List.fold_left join p q )
- x l
+ let f x =
+ List.fold_left
+ (fun k c -> match apply_cons k c with
+ | [] -> raise Bot
+ | p::q -> List.fold_left join p q )
+ x l
+ in
+ fix eq f x
let assign x idl =
let v = List.fold_left
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 5cbe0c9..a124a84 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -277,6 +277,8 @@ let rec split_cases 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
diff --git a/main.ml b/main.ml
index 96fb95e..303723d 100644
--- a/main.ml
+++ b/main.ml
@@ -23,6 +23,10 @@ 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)
+module AI_EDD_Itv_DP = Abs_interp_dynpart.I
+ (Enum_domain_edd.EDD)(ItvND)
+module AI_EDD_Rel_DP = Abs_interp_dynpart.I
+ (Enum_domain_edd.EDD)(Apron_domain.ND)
(* command line options *)
let times = ref false
@@ -36,6 +40,8 @@ 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_edd_itv_dp = ref false
+let ai_edd_rel_dp = ref false
let ai_root = ref "test"
let ai_widen_delay = ref 5
let ai_no_time_scopes = ref "all"
@@ -50,28 +56,41 @@ let usage = "usage: analyzer [options] file.scade"
let options = [
"--exec-times", Arg.Set times,
"Show time spent in each function of the analyzer, for some functions";
+
"--dump", Arg.Set dump, "Dump program source.";
"--dump-rn", Arg.Set dumprn, "Dump program source, after renaming.";
+
"--vtest", Arg.Set vtest, "Verbose testing (direct interpret).";
"--test", Arg.Set test, "Simple testing (direct interpret).";
+
"--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
"--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
+
"--ai-itv-edd", Arg.Set ai_itv_edd,
"Do abstract analysis using intervals and EDD disjunction domain.";
"--ai-rel-edd", Arg.Set ai_rel_edd,
"Do abstract analysis using Apron and EDD disjunction domain.";
+
"--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-edd-itv-dp", Arg.Set ai_edd_itv_dp,
+ "Do abstract analysis using dynamic partitionning method, "^
+ "with intervals and EDD domain for enums.";
+ "--ai-edd-rel-dp", Arg.Set ai_edd_rel_dp,
+ "Do abstract analysis using dynamic partitionning method, "^
+ "with Apron and EDD domain for enums.";
+
"--ai-vci", Arg.Set ai_vci,
"Verbose chaotic iterations (show state at each iteration)";
"--ai-vvci", Arg.Set ai_vvci,
"Very verbose chaotic iterations (show everything all the time)";
- "--wd", Arg.Set_int ai_widen_delay,
+ "--ai-wd", Arg.Set_int ai_widen_delay,
"Widening delay in abstract analysis of loops (default: 3).";
+
"--root", Arg.Set_string ai_root,
"Root node for abstract analysis (default: test).";
"--no-time", Arg.Set_string ai_no_time_scopes,
@@ -132,7 +151,8 @@ let () =
if !ai_itv || !ai_rel
|| !ai_itv_edd || !ai_rel_edd
- || !ai_s_itv_dp || !ai_s_rel_dp then
+ || !ai_s_itv_dp || !ai_s_rel_dp
+ || !ai_edd_itv_dp || !ai_edd_rel_dp then
begin
let comma_split = Str.split (Str.regexp ",") in
let select_f x =
@@ -168,6 +188,8 @@ let () =
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;
+ if !ai_edd_itv_dp then AI_EDD_Itv_DP.do_prog opt rp;
+ if !ai_edd_rel_dp then AI_EDD_Rel_DP.do_prog opt rp;
end;
if !vtest then do_test_interpret prog true
diff --git a/tests/source/half.scade b/tests/source/half.scade
index 541e81c..7e0df60 100644
--- a/tests/source/half.scade
+++ b/tests/source/half.scade
@@ -25,5 +25,5 @@ let
c = a - b;
guarantee c_bounded: c >= 0 and c <= 1;
- guarantee link_c_half: (half and c = 1) or ((not half) and c = 0);
+ guarantee link_c_half: if half then (c = 1) else (c = 0);
tel
diff --git a/tests/source/updown2.scade b/tests/source/updown2.scade
index 29c34ff..72d5bed 100644
--- a/tests/source/updown2.scade
+++ b/tests/source/updown2.scade
@@ -30,7 +30,7 @@ let
guarantee y_bounded: y >= -bound and y <= bound;
z = x + y;
- guarantee x_y_opp: z = 0 and (true -> pre (z = 0));
+ guarantee x_y_opp: z = 0;
tel
node test(i: int) returns(a, b, c: int; exit: bool)