summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abstract/abs_interp.ml17
-rw-r--r--abstract/nonrelational.ml40
-rw-r--r--abstract/transform.ml6
-rw-r--r--abstract/value_domain.ml2
-rw-r--r--main.ml2
-rw-r--r--tests/result/limiter.out48
-rw-r--r--tests/source/limiter.scade2
-rw-r--r--tests/source/test4.scade2
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
diff --git a/main.ml b/main.ml
index d063699..aa60c57 100644
--- a/main.ml
+++ b/main.ml
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-19 16:03:15 +0000