Add gilbreath suite ; booleans are not represented in a good way.

13 files changed, 201 insertions, 89 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 4c3fddb..feaf037 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -9,12 +9,13 @@ module I (E : ENVIRONMENT_DOMAIN) : sig
 
     type st
 
-    val do_prog     : prog -> id -> unit
+    val do_prog     : int -> prog -> id -> unit
 
 end = struct
 
     type st = {
         p           : prog;
+        widen_delay : int;
         root_scope  : scope;
         all_vars    : var_def list;
         env         : E.t;
@@ -69,7 +70,7 @@ end = struct
         (List.flatten (List.map vars_of_eq eqs))
 
     (* init state *)
-    let init_state p root =
+    let init_state widen_delay p root =
       let root_scope = get_root_scope p root in
 
       let f = Formula.eliminate_not (Transform.f_of_prog p root) in
@@ -86,11 +87,11 @@ end = struct
       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;
+      Format.printf "Vars: @[<hov>%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 }
+      { p; root_scope; widen_delay; f; cl; all_vars; env }
 
     (*
       pass_cycle : var_def list -> E.t -> E.t
@@ -121,13 +122,12 @@ end = struct
 
     (* cycle : st -> cl -> env -> env *)
     let cycle st cl i =
-      E.apply_cl (pass_cycle st.all_vars i) cl
+      (pass_cycle st.all_vars (E.apply_cl i cl)) 
 
     (*
       loop : st -> cl -> env -> env -> env
     *)
     let loop st cycle_cl pnew stay =
-      let pnew = E.apply_cl pnew cycle_cl in
 
       Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
         Formula_printer.print_conslist cycle_cl
@@ -142,10 +142,9 @@ end = struct
         E.join acc0 j
       in
 
-      let widen_delay = 10 in
       let rec iter n i =
         let i' =
-          if n < widen_delay
+          if n < st.widen_delay
             then E.join i (fsharp i)
             else E.widen i (fsharp i)
         in
@@ -159,21 +158,23 @@ end = struct
     (*
       do_prog : prog -> id -> unit
     *)
-    let do_prog p root =
-      let st = init_state p root in
+    let do_prog widen_delay p root =
+      let st = init_state widen_delay p root in
 
       let pnew = st.env in
 
       let stay = loop st st.cl pnew (E.vbottom pnew) in
 
-      Format.printf "@[<hov>Final stay %a@]@."
-        E.print_all stay;
+      let final = E.join (E.apply_cl pnew st.cl) (E.apply_cl stay st.cl) in
+
+      Format.printf "@[<hov>Final %a@]@."
+        E.print_all final;
 
       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))
+              E.print_itv (E.var_itv final id))
         st.all_vars;
       Format.printf "@]@."
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 262bccb..44495c4 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -12,17 +12,31 @@ type num_expr =
   (* identifier *)
   | NIdent of id
 
+
 type bool_expr =
   (* constants *)
   | BConst of bool
   (* operators from numeric values to boolean values *)
   | BRel of binary_rel_op * num_expr * num_expr
+  | BBoolEq of id * bool
   (* boolean operators *)
   | BAnd of bool_expr * bool_expr
   | BOr of bool_expr * bool_expr
   | BNot of bool_expr
 
 
+let f_and a b = match a, b with
+  | BConst false, _ | _, BConst false -> BConst false
+  | BConst true, b -> b
+  | a, BConst true -> a
+  | a, b -> BAnd(a, b)
+
+let f_or a b = match a, b with
+  | BConst true, _ | _, BConst true -> BConst true
+  | BConst false, b -> b
+  | a, BConst false -> a
+  | a, b -> BOr(a, b)
+
 
 (* Write all formula without using the NOT operator *)
 
@@ -33,6 +47,7 @@ let rec eliminate_not = function
   | x -> x
 and eliminate_not_negate = function
   | BConst x -> BConst(not x)
+  | BBoolEq(id, v) -> BBoolEq(id, not v)
   | BNot e -> eliminate_not e
   | BRel(r, a, b) ->
     let r' = match r with
@@ -83,6 +98,11 @@ let rec conslist_of_f = function
     in [cons], CLTrue
   | BConst x ->
     [], if x then CLTrue else CLFalse
+  | BBoolEq(id, v) ->
+    if v then
+      [NBinary(AST_MINUS, NIdent id, NIntConst 1), CONS_EQ], CLTrue
+    else
+      [NIdent id, CONS_EQ], CLTrue
   | BOr(a, b) ->
     let ca, ra = conslist_of_f a in
     let cb, rb = conslist_of_f b in
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 53a9b6a..1b31ba1 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -60,6 +60,11 @@ let rec print_num_expr fmt e = match e with
 
 let rec print_bool_expr fmt e = match e with
   | BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false")
+  | BBoolEq(id, v) ->
+    if v then
+      Format.fprintf fmt "%a" print_id id
+    else
+      Format.fprintf fmt "¬%a" print_id id
   | BRel(op, a, b) ->
     print_ch fmt print_num_expr ne_prec a be_prec e;
     Format.fprintf fmt "@ %s " (string_of_binary_rel op);
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 3cdcc31..855f970 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -215,14 +215,15 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
             List.iteri
               (fun j (v, ids) ->
                 if j > 0 then Format.fprintf fmt "@ ";
+                Format.fprintf fmt "@[<hov 4>";
                 List.iteri
                   (fun i id ->
-                    if i > 0 then Format.fprintf fmt ", ";
+                    if i > 0 then Format.fprintf fmt ",@ ";
                     Format.fprintf fmt "%a" Formula_printer.print_id id)
                   ids;
                 match V.as_const v with
-                | Some i -> Format.fprintf fmt " = %d" i
-                | _ -> Format.fprintf fmt " ∊ %s" (V.to_string v))
+                | Some i -> Format.fprintf fmt " = %d@]" i
+                | _ -> Format.fprintf fmt " ∊ %s@]" (V.to_string v))
               sbl;
             Format.fprintf fmt " }@]"
 
diff --git a/abstract/transform.ml b/abstract/transform.ml
index b141cc6..87da1bd 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -18,11 +18,6 @@ type transform_data = {
     (* future : the automata state *)
 }
 
-let f_and a b =
-  if a = BConst true then b
-    else if b = BConst true then a
-      else BAnd(a, b)
-
 
 (* f_of_nexpr :
     transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a
@@ -55,48 +50,76 @@ let rec f_of_nexpr td (node, prefix) where expr =
   (* temporal *)
   | AST_pre(_, id) -> where [NIdent id]
   | AST_arrow(a, b) ->
-      BOr(
-        BAnd(BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0),
-          sub where a),
-        BAnd(BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1),
-          sub where b))
+    f_or
+      (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+        (sub where a))
+      (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+        (sub where b))
   (* other *)
   | AST_if(c, a, b) ->
-    BOr(
-      BAnd(f_of_bexpr td (node, prefix) c, sub where a),
-      BAnd(BNot(f_of_bexpr td (node, prefix) c), sub where b))
+    f_or
+      (f_and (f_of_expr td (node, prefix) c) (sub where a))
+      (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
   | AST_instance ((f, _), args, nid) ->
     let (n, _) = find_node_decl td.p f in
     where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret)
     
   (* boolean values treated as integers *)
   | _ ->
-    BOr(
-      BAnd ((f_of_bexpr td (node, prefix) expr), where [NIntConst 1]),
-      BAnd (BNot(f_of_bexpr td (node, prefix) expr), where [NIntConst 0])
-    )
+    f_or
+      (f_and ((f_of_expr td (node, prefix) expr)) (where [NIntConst 1]))
+      (f_and (BNot(f_of_expr td (node, prefix) expr)) (where [NIntConst 0]))
+
 
-(* f_of_expr :
+(* 
+  f_of_expr :
     transform_data -> (string, string) -> expr -> bool_expr
+  f_of_bexpr :
+    transform_data -> (string, string) -> (bool_expr -> 'a) -> expr -> 'a
 *)
-and f_of_bexpr td (node, prefix) expr =
+and f_of_bexpr td (node, prefix) where expr =
   let sub = f_of_bexpr td (node, prefix) in
   match fst expr with
-  | AST_bool_const b -> BConst b
-  | AST_binary_bool(AST_AND, a, b) -> BAnd(sub a, sub b)
-  | AST_binary_bool(AST_OR, a, b) -> BOr(sub a, sub b)
-  | AST_not(a) -> BNot(sub a)
+  | AST_bool_const b -> where (BConst b)
+  | AST_binary_bool(AST_AND, a, b) -> f_and (sub where a) (sub where b)
+  | AST_binary_bool(AST_OR, a, b) -> f_or (sub where a) (sub where b)
+  | AST_not(a) -> BNot(sub where a)
   | AST_binary_rel(rel, a, b) ->
-    f_of_nexpr td (node, prefix)
-      (function
-        | [x] -> f_of_nexpr td (node, prefix)
-          (function
-            | [y] -> BRel(rel, x, y)
-            | _ -> invalid_arity "boolean relation") b
-        | _ -> invalid_arity "boolean relation")
-      a
-  | _ -> loc_error (snd expr) error "Invalid type : expected boolean value"
-  
+    where
+      (f_of_nexpr td (node, prefix)
+        (function
+          | [x] -> f_of_nexpr td (node, prefix)
+            (function
+              | [y] -> BRel(rel, x, y)
+              | _ -> invalid_arity "boolean relation") b
+          | _ -> invalid_arity "boolean relation")
+        a)
+  | AST_identifier (id, _) ->
+    let id = node^"/"^id in
+    f_or
+      (f_and (BBoolEq(id, true)) (where (BConst true)))
+      (f_and (BBoolEq(id, false)) (where (BConst false)))
+  (* temporal *)
+  | AST_pre(_, id) ->
+    f_or
+      (f_and (BBoolEq(id, true)) (where (BConst true)))
+      (f_and (BBoolEq(id, false)) (where (BConst false)))
+  | AST_arrow(a, b) ->
+      f_or
+        (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
+          (sub where a))
+        (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
+          (sub where b))
+  (* other *)
+  | AST_if(c, a, b) ->
+    f_or
+      (f_and (f_of_expr td (node, prefix) c) (sub where a))
+      (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
+
+  | _ -> loc_error (snd expr) error "Expected boolean value."
+
+and f_of_expr td (node, prefix) expr =
+    f_of_bexpr td (node, prefix) (fun x -> x) expr
   
 
 and f_of_scope active td (node, prefix, eqs) =
@@ -148,7 +171,7 @@ and f_of_scope active td (node, prefix, eqs) =
     | AST_assume (_, e) ->
       let assume_eq = 
         if active then
-          f_of_bexpr td (node, prefix) e
+          f_of_expr td (node, prefix) e
         else
           BConst true
       in
@@ -166,12 +189,11 @@ and f_of_scope active td (node, prefix, eqs) =
         | AST_activate_body b ->
             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)
-              (f_and (do_tree_act a) (do_tree_inact b)),
-            f_and (BNot(f_of_bexpr td (node, prefix) c))
-              (f_and (do_tree_act b) (do_tree_inact a))
-          )
+          f_or
+            (f_and (f_of_expr td (node, prefix) c)
+              (f_and (do_tree_act a) (do_tree_inact b)))
+            (f_and (BNot(f_of_expr td (node, prefix) c))
+              (f_and (do_tree_act b) (do_tree_inact a)))
       and do_tree_inact = function
         | AST_activate_body b ->
           f_of_scope false td (node, b.act_id^".", b.body)
@@ -202,10 +224,6 @@ and f_of_prog p root =
     } in
 
     f_of_scope true td td.root_scope
-  
-
-
-
 
 
 
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index c14d0d1..3ac881e 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -72,7 +72,7 @@ let print_list f sep fmt l =
   let rec aux = function
     | [] -> ()
     | [a] -> f fmt a
-    | a::b -> f fmt a; Format.pp_print_string fmt sep; aux b
+    | a::b -> f fmt a; Format.fprintf fmt "%s@," sep; aux b
   in
   aux l
 
diff --git a/main.ml b/main.ml
index aa60c57..0ddf91c 100644
--- a/main.ml
+++ b/main.ml
@@ -3,13 +3,18 @@ open Ast
 module Interpret = Interpret.I
 
 module IntD = Nonrelational.D(Intervals_domain.VD)
-module AI = Abs_interp.I(Apron_domain.D)
+module AI_Int = Abs_interp.I(IntD)
+module AI_Rel = Abs_interp.I(Apron_domain.D)
 
 (* command line options *)
 let dump = ref false
 let dumprn = ref false
 let test = ref false
 let vtest = ref false
+let ai_int = ref false
+let ai_rel = ref false
+let ai_root = ref "test"
+let ai_widen_delay = ref 3
 let ifile = ref ""
 
 let usage = "usage: analyzer [options] file.scade"
@@ -19,6 +24,10 @@ let options = [
     "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming.";
     "--vtest", Arg.Set vtest, "Verbose testing.";
     "--test", Arg.Set test, "Simple testing.";
+    "--ai-int", Arg.Set ai_int, "Do abstract analysis using intervals.";
+    "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
+    "--ai-root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test).";
+    "--ai-wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
 ]
 
 let do_test_interpret prog verbose =
@@ -66,7 +75,8 @@ let () =
       let prog = Rename.rename_prog prog in
       if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
 
-      let () = AI.do_prog prog "test" in
+      if !ai_int then AI_Int.do_prog !ai_widen_delay prog !ai_root;
+      if !ai_rel then AI_Rel.do_prog !ai_widen_delay prog !ai_root;
 
       if !vtest then do_test_interpret prog true
       else if !test then do_test_interpret prog false;
diff --git a/tests/Makefile b/tests/Makefile
index f51eb61..7d5aac0 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -2,7 +2,8 @@ ALL_OUT=result/limiter.out result/limitera.out result/locals.out \
 		result/test4.out result/test5.out result/test7.out \
 		result/train.out result/updown.out result/updown_fail.out \
 		result/test0.out result/test1.out result/test2.out result/test3.out \
-		result/test6.out result/testc.out
+		result/test6.out result/testc.out \
+		result/gilbreath.out
 
 bin/%.test: source/%.scade test.c
 	rm kcg/*
diff --git a/tests/result/gilbreath.out b/tests/result/gilbreath.out
new file mode 100644
index 0000000..d6a0fa4
--- /dev/null
+++ b/tests/result/gilbreath.out
@@ -0,0 +1,21 @@
+0. 0 1 1
+1. 1 1 0
+2. 0 1 0
+3. 1 1 1
+4. 1 1 0
+5. 0 1 0
+6. 0 1 1
+7. 1 1 0
+8. 0 1 0
+9. 1 1 0
+10. 0 1 0
+11. 1 1 0
+12. 1 1 1
+13. 0 1 0
+14. 1 1 0
+15. 0 1 1
+16. 0 1 0
+17. 1 1 0
+18. 1 1 1
+19. 0 1 0
+20. 1 1 0
diff --git a/tests/result/limitera.out b/tests/result/limitera.out
index 1851c7d..f047b8f 100644
--- a/tests/result/limitera.out
+++ b/tests/result/limitera.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/gilbreath.scade b/tests/source/gilbreath.scade
new file mode 100644
index 0000000..2723f9f
--- /dev/null
+++ b/tests/source/gilbreath.scade
@@ -0,0 +1,34 @@
+node gilbreath_stream(c: bool) returns (o, probe property: bool)
+var
+  half: bool;
+let
+  activate
+    if c then
+      let
+        o = false -> not pre o;
+      tel 
+    else
+      let
+        o = true -> not pre o;
+      tel
+  returns o;
+
+  half = false -> not pre half;
+
+  property = true -> not (half and (o = pre o));
+tel
+
+node test(i: int) returns (a, b, c: int; exit: bool)
+var
+  cond: bool;
+  o, prop: bool;
+let
+  exit = i >= 20;
+  cond = i mod 3 = 0 and not (i mod 7 = 2);
+  c = if cond then 1 else 0;
+  o, prop = gilbreath_stream(cond);
+  a = if o then 1 else 0;
+  b = if prop then 1 else 0;
+tel
+
+  
diff --git a/tests/source/limiter.scade b/tests/source/limiter.scade
index ff60567..fc9fb30 100644
--- a/tests/source/limiter.scade
+++ b/tests/source/limiter.scade
@@ -4,6 +4,7 @@ node limiter(x: int; d: int) returns (probe y: int)
     var s, r: int;
     let
         assume in_bounded: x >= -bound and x <= bound;
+        assume d_bounded: d >= 0 and d >= 16;
         guarantee out_bounded: y >= -bound and y <= bound;
         s = 0 -> pre y;
         r = x - s;
diff --git a/tests/source/limitera.scade b/tests/source/limitera.scade
index 1e4927e..e6db4e2 100644
--- a/tests/source/limitera.scade
+++ b/tests/source/limitera.scade
@@ -20,7 +20,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