diff options
author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-18 12:13:17 +0200 |
---|---|---|
committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-18 12:13:17 +0200 |
commit | 0caa1ebe947646459295c6a66da6bf19f399c21e (patch) | |
tree | 715b4e786a7df2a3f847230baaa8d26f9ed9e680 | |
parent | 5ac14cee1bdb9f2ccc40ad6eb1841b5c2ed584d1 (diff) | |
download | scade-analyzer-0caa1ebe947646459295c6a66da6bf19f399c21e.tar.gz scade-analyzer-0caa1ebe947646459295c6a66da6bf19f399c21e.zip |
Abstract interpretation gives good results on the limiter example.
-rw-r--r-- | abstract/abs_interp.ml | 17 | ||||
-rw-r--r-- | abstract/nonrelational.ml | 40 | ||||
-rw-r--r-- | abstract/transform.ml | 6 | ||||
-rw-r--r-- | abstract/value_domain.ml | 2 | ||||
-rw-r--r-- | main.ml | 2 | ||||
-rw-r--r-- | tests/result/limiter.out | 48 | ||||
-rw-r--r-- | tests/source/limiter.scade | 2 | ||||
-rw-r--r-- | tests/source/test4.scade | 2 |
8 files changed, 58 insertions, 61 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 4f66540..4c3fddb 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -56,7 +56,7 @@ end = struct | AST_activate (b, _) -> let rec do_branch = function | AST_activate_body b -> - List.map (fun (p, id, t) -> p, node^"/"^b.act_id^"."^id, t) b.act_locals + List.map (fun (p, id, t) -> p, node^"/"^id, t) b.act_locals @ extract_all_vars p (node, b.act_id^".", b.body) | AST_activate_if(c, a, b) -> @@ -81,15 +81,15 @@ end = struct E.init all_vars in - - - let init_f = Transform.init_f_of_prog p root in - let env = E.apply_f env init_f in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f; + Format.printf "Vars: %a@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars; + + let env = E.apply_f env init_f in + { p; root_scope; f; cl; all_vars; env } (* @@ -142,7 +142,7 @@ end = struct E.join acc0 j in - let widen_delay = 2 in + let widen_delay = 10 in let rec iter n i = let i' = if n < widen_delay @@ -170,10 +170,11 @@ end = struct E.print_all stay; Format.printf "Probes:@[<hov>"; - List.iter (fun (p, id, _) -> if p then Format.printf "@ %a ∊ %a," Formula_printer.print_id id E.print_itv (E.var_itv stay id)) - st.all_vars + st.all_vars; + Format.printf "@]@." + end diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index b83edc1..3cdcc31 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -69,20 +69,26 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct | Env env -> V.to_itv (get_var env id) (* Set-theoretic operations *) + let f_in_merge f _ a b = match a, b with + | Some a, None -> Some a + | None, Some b -> Some b + | Some a, Some b -> Some (f a b) + | _ -> assert false + let join a b = match a, b with | Bot, x | x, Bot -> x | Env m, Env n -> - strict (VarMap.map2z (fun _ a b -> V.join a b) m n) + strict (VarMap.merge (f_in_merge V.join) m n) let meet a b = match a, b with | Bot, _ | _, Bot -> Bot | Env m, Env n -> - strict (VarMap.map2z (fun _ a b -> V.meet a b) m n) + strict (VarMap.merge (f_in_merge V.meet) m n) let widen a b = match a, b with | Bot, x | x, Bot -> x | Env m, Env n -> - strict (VarMap.map2z (fun _ a b -> V.widen a b) m n) + strict (VarMap.merge (f_in_merge V.widen) m n) (* Inclusion and equality *) let subset a b = match a, b with @@ -161,27 +167,17 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct List.fold_left restrict_var env (extract_var (expr, zop, NIntConst 0)) - let rec apply_cl x (cons, rest) = - let apply_cl_l x = List.fold_left apply_cons x cons in - - let y = fix eq apply_cl_l x in - if debug then Format.printf "-[@."; - let z = apply_cl_r y rest in - if debug then Format.printf "-]@."; - fix eq apply_cl_l z - - and apply_cl_r x = function - | CLTrue -> x + let rec apply_cl x (cons, rest) = match rest with + | CLTrue -> + let apply_cl_l x = List.fold_left apply_cons x cons in + fix eq apply_cl_l x | CLFalse -> vbottom x | CLAnd(a, b) -> - let y = apply_cl_r x a in - apply_cl_r y b - | CLOr(a, b) -> - if debug then Format.printf "<<@."; - let y = apply_cl x a in - if debug then Format.printf "\\/@."; - let z = apply_cl x b in - if debug then Format.printf ">>@."; + let y = apply_cl x (cons, a) in + apply_cl y (cons, b) + | CLOr((ca, ra), (cb, rb)) -> + let y = apply_cl x (cons@ca, ra) in + let z = apply_cl x (cons@cb, rb) in join y z let apply_f x f = apply_cl x (conslist_of_f f) diff --git a/abstract/transform.ml b/abstract/transform.ml index 40390dd..b141cc6 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -164,7 +164,7 @@ and f_of_scope active td (node, prefix, eqs) = in let rec do_tree_act = function | AST_activate_body b -> - f_of_scope true td (node, b.act_id^"_", b.body) + f_of_scope true td (node, b.act_id^".", b.body) | AST_activate_if(c, a, b) -> BOr( f_and (f_of_bexpr td (node, prefix) c) @@ -174,7 +174,7 @@ and f_of_scope active td (node, prefix, eqs) = ) and do_tree_inact = function | AST_activate_body b -> - f_of_scope false td (node, b.act_id^"_", b.body) + f_of_scope false td (node, b.act_id^".", b.body) | AST_activate_if(_, a, b) -> f_and (do_tree_inact a) (do_tree_inact b) in @@ -223,7 +223,7 @@ let rec init_f_of_scope p (node, prefix, eqs) = | AST_activate (b, _) -> let rec cond_eq = function | AST_activate_body b -> - init_f_of_scope p (node, b.act_id^"_", b.body) + init_f_of_scope p (node, b.act_id^".", b.body) | AST_activate_if(c, a, b) -> f_and (expr_eq c) (f_and (cond_eq a) (cond_eq b)) diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml index 7b9d557..bb27126 100644 --- a/abstract/value_domain.ml +++ b/abstract/value_domain.ml @@ -8,7 +8,7 @@ let string_of_bound = function | Int i -> string_of_int i let string_of_itv = function | Bot -> "⊥" - | Itv(a, b) -> "[" ^ (string_of_bound a) ^ ";" ^ (string_of_bound b) ^ "]" + | Itv(a, b) -> "[" ^ (string_of_bound a) ^ "; " ^ (string_of_bound b) ^ "]" module type VALUE_DOMAIN = sig type t @@ -3,7 +3,7 @@ open Ast module Interpret = Interpret.I module IntD = Nonrelational.D(Intervals_domain.VD) -module AI = Abs_interp.I(IntD) +module AI = Abs_interp.I(Apron_domain.D) (* command line options *) let dump = ref false diff --git a/tests/result/limiter.out b/tests/result/limiter.out index 1851c7d..f047b8f 100644 --- a/tests/result/limiter.out +++ b/tests/result/limiter.out @@ -5,27 +5,27 @@ 4. 78 16 58 5. 99 16 74 6. 120 16 90 -7. -115 16 74 -8. -94 16 58 -9. -73 16 42 -10. -52 16 26 -11. -31 16 10 -12. -10 16 -6 -13. 11 16 10 -14. 32 16 26 -15. 53 16 42 -16. 74 16 58 -17. 95 16 74 -18. 116 16 90 -19. -119 16 74 -20. -98 16 58 -21. -77 16 42 -22. -56 16 26 -23. -35 16 10 -24. -14 16 -6 -25. 7 16 7 -26. 28 16 23 -27. 49 16 39 -28. 70 16 55 -29. 91 16 71 -30. 112 16 87 +7. -116 16 74 +8. -95 16 58 +9. -74 16 42 +10. -53 16 26 +11. -32 16 10 +12. -11 16 -6 +13. 10 16 10 +14. 31 16 26 +15. 52 16 42 +16. 73 16 58 +17. 94 16 74 +18. 115 16 90 +19. -121 16 74 +20. -100 16 58 +21. -79 16 42 +22. -58 16 26 +23. -37 16 10 +24. -16 16 -6 +25. 5 16 5 +26. 26 16 21 +27. 47 16 37 +28. 68 16 53 +29. 89 16 69 +30. 110 16 85 diff --git a/tests/source/limiter.scade b/tests/source/limiter.scade index a611d98..ff60567 100644 --- a/tests/source/limiter.scade +++ b/tests/source/limiter.scade @@ -15,7 +15,7 @@ node limiter(x: int; d: int) returns (probe y: int) node test(i: int) returns(a, b, c: int; exit: bool) let exit = i >= 30; - a = (i * 21 + 122) mod (2 * bound) - bound; -- not really random + a = (i * 21 + 122) mod (2 * bound + 1) - bound; -- not really random b = 16; c = limiter(a, b); tel diff --git a/tests/source/test4.scade b/tests/source/test4.scade index b32a37d..843302f 100644 --- a/tests/source/test4.scade +++ b/tests/source/test4.scade @@ -1,7 +1,7 @@ node test(i: int) returns(probe a, b, c: int; exit: bool) let exit = i >= 5; - a = 0 -> (if pre a >= 10 then 0 else pre a + 1); + a = 0 -> (if pre a >= 5 then 0 else pre a + 1); b = 0 -> pre i; c = 0; tel |