Nice view of guarantees ; add half test, proved.

11 files changed, 180 insertions, 44 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index feaf037..d706f35 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -21,6 +21,9 @@ end = struct
         env         : E.t;
         f           : bool_expr;
         cl          : conslist;
+        f_g         : bool_expr;
+        cl_g        : conslist;
+        guarantees  : (id * bool_expr) list;
     }
 
 
@@ -73,8 +76,11 @@ end = struct
     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
+      let f = Formula.eliminate_not (Transform.f_of_prog p root false) in
       let cl = Formula.conslist_of_f f in
+      let f_g = Formula.eliminate_not (Transform.f_of_prog p root true) in
+      let cl_g = Formula.conslist_of_f f_g in
+
       let all_vars = node_vars p root "" @ extract_all_vars p root_scope in
       let env = List.fold_left
         (fun env (_, id, ty) ->
@@ -83,15 +89,25 @@ end = struct
         all_vars
       in
       let init_f = Transform.init_f_of_prog p root in
+      let guarantees = Transform.guarantees_of_prog p root in
 
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
-      Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f;
+      Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
+      Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
 
       Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
 
+      Format.printf "Guarantees:@.";
+      List.iter (fun (id, f) ->
+          Format.printf "  %s: %a@." id Formula_printer.print_expr f)
+        guarantees;
+      Format.printf "@.";
+
       let env = E.apply_f env init_f in
 
-      { p; root_scope; widen_delay; f; cl; all_vars; env }
+      { p; root_scope; widen_delay;
+        f; cl; f_g; cl_g;
+        guarantees; all_vars; env }
 
     (*
       pass_cycle : var_def list -> E.t -> E.t
@@ -125,35 +141,36 @@ end = struct
       (pass_cycle st.all_vars (E.apply_cl i cl)) 
 
     (*
-      loop : st -> cl -> env -> env -> env
+      loop : st -> env -> env -> env
     *)
-    let loop st cycle_cl pnew stay =
+    let loop st pnew stay =
 
       Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
-        Formula_printer.print_conslist cycle_cl
+        Formula_printer.print_conslist st.cl
         E.print_all pnew E.print_all stay;
 
-      let add_stay = cycle st cycle_cl pnew in
+      let add_stay = cycle st st.cl pnew in
       let acc0 = E.join stay add_stay in
 
-      let fsharp i = 
+      let fsharp cl i = 
         Format.printf "Acc @[<hv>%a@]@." E.print_all i;
-        let j = cycle st cycle_cl i in
+        let j = cycle st cl i in
         E.join acc0 j
       in
 
       let rec iter n i =
         let i' =
           if n < st.widen_delay
-            then E.join i (fsharp i)
-            else E.widen i (fsharp i)
+            then E.join i (fsharp st.cl_g i)
+            else E.widen i (fsharp st.cl_g i)
         in
         if E.eq i i' then i else iter (n+1) i'
       in
 
       let x = iter 0 acc0 in
-      fix E.eq fsharp x   (* decreasing iteration *)
-
+      let y = fix E.eq (fsharp st.cl_g) x in    (* decreasing iteration *)
+      let z = E.apply_cl y st.cl in
+      y, z
 
     (*
       do_prog : prog -> id -> unit
@@ -163,16 +180,29 @@ end = struct
 
       let pnew = st.env in
 
-      let stay = loop st st.cl pnew (E.vbottom pnew) in
+      let stay, stay_c = loop st pnew (E.vbottom pnew) in
 
-      let final = E.join (E.apply_cl pnew st.cl) (E.apply_cl stay st.cl) in
+      let final = E.join (E.apply_cl pnew st.cl) stay_c in
 
-      Format.printf "@[<hov>Final %a@]@."
+      Format.printf "@[<hov>Final %a@]@.@."
         E.print_all final;
 
-      Format.printf "Probes:@[<hov>";
+      let check_guarantee (id, f) =
+        Format.printf "@[<hv>%s:@ %a@ "
+          id Formula_printer.print_expr f;
+        let z = E.apply_f final (BAnd(f, st.f)) in
+        if E.is_bot z then
+          Format.printf "OK@]@ "
+        else
+          Format.printf "FAIL@]@ "
+      in
+      Format.printf "Guarantees: @[<v 0>";
+      List.iter check_guarantee st.guarantees;
+      Format.printf "@]@.";
+
+      Format.printf "Probes:@[<v>";
       List.iter (fun (p, id, _) ->
-        if p then Format.printf "@ %a ∊ %a,"
+        if p then Format.printf " %a ∊ %a@ "
               Formula_printer.print_id id
               E.print_itv (E.var_itv final id))
         st.all_vars;
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index d13afd7..cef6b66 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -133,6 +133,7 @@ module D : ENVIRONMENT_DOMAIN = struct
 
     (* Pretty-printing *)
     let print_all fmt x =
+        Abstract1.minimize manager x;
         Abstract1.print fmt x;
         Format.fprintf fmt "@?"
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 44495c4..f3c1df1 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -50,15 +50,18 @@ and eliminate_not_negate = function
   | BBoolEq(id, v) -> BBoolEq(id, not v)
   | BNot e -> eliminate_not e
   | BRel(r, a, b) ->
-    let r' = match r with
-    | AST_EQ -> AST_NE
-    | AST_NE -> AST_EQ
-    | AST_LT -> AST_GE
-    | AST_LE -> AST_GT
-    | AST_GT -> AST_LE
-    | AST_GE -> AST_LT
-    in
-    BRel(r', a, b)
+    if r = AST_EQ then
+      BOr(BRel(AST_LT, a, b), BRel(AST_GT, a, b))
+    else
+      let r' = match r with
+      | AST_EQ -> AST_NE
+      | AST_NE -> AST_EQ
+      | AST_LT -> AST_GE
+      | AST_LE -> AST_GT
+      | AST_GT -> AST_LE
+      | AST_GE -> AST_LT
+      in
+      BRel(r', a, b)
   | BAnd(a, b) ->
     BOr(eliminate_not_negate a, eliminate_not_negate b)
   | BOr(a, b) ->
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 87da1bd..25e4b43 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -18,7 +18,6 @@ type transform_data = {
     (* future : the automata state *)
 }
 
-
 (* f_of_nexpr :
     transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a
 *)
@@ -122,10 +121,13 @@ 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) =
+(*
+    Translate program into one big formula
+*)
+let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
   let expr_eq e eq =
     let instance_eq (_, id, eqs, args) =
-      let eq = f_of_scope active td (node^"/"^id, "", eqs) in
+      let eq = f_of_scope active td (node^"/"^id, "", eqs) assume_guarantees in
       if active then
         List.fold_left (fun eq ((_,argname,_), expr) ->
             let eq_arg = f_of_nexpr td (node, prefix) (function
@@ -177,7 +179,13 @@ and f_of_scope active td (node, prefix, eqs) =
       in
         expr_eq e assume_eq
     | AST_guarantee (_, e) ->
-      expr_eq e (BConst true)
+      let guarantee_eq =
+        if active && assume_guarantees then
+          f_of_expr td (node, prefix) e
+        else
+          BConst true
+      in
+        expr_eq e guarantee_eq
     | AST_activate (b, _) ->
       let rec cond_eq = function
         | AST_activate_body b -> BConst true
@@ -187,7 +195,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) assume_guarantees
         | AST_activate_if(c, a, b) ->
           f_or
             (f_and (f_of_expr td (node, prefix) c)
@@ -196,7 +204,7 @@ and f_of_scope active td (node, prefix, eqs) =
               (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)
+          f_of_scope false td (node, b.act_id^".", b.body) assume_guarantees
         | AST_activate_if(_, a, b) ->
           f_and (do_tree_inact a) (do_tree_inact b)
       in
@@ -216,17 +224,18 @@ and f_of_scope active td (node, prefix, eqs) =
     time_incr_eq
     (List.map do_eq eqs)
 
-and f_of_prog p root =
+and f_of_prog p root assume_guarantees =
     let td = {
       root_scope = get_root_scope p root;
       p = p;
       consts = I.consts p root;
     } in
 
-    f_of_scope true td td.root_scope
-
-
+    f_of_scope true td td.root_scope assume_guarantees
 
+(*
+    Translate init state into a formula
+*)
 let rec init_f_of_scope p (node, prefix, eqs) =
   let expr_eq e =
     let instance_eq (_, id, eqs, args) =
@@ -258,3 +267,43 @@ let rec init_f_of_scope p (node, prefix, eqs) =
 
 and init_f_of_prog p root =
     init_f_of_scope p (get_root_scope p root)
+
+(*
+    Get expressions for guarantee violation
+*)
+let rec g_of_scope td (node, prefix, eqs) cond =
+  let expr_g e =
+    let instance_g (_, id, eqs, args) =
+        g_of_scope td (node^"/"^id, "", eqs) cond
+    in
+    List.fold_left (fun x i -> (instance_g i) @ x)
+      [] (extract_instances td.p e)
+  in
+  let do_eq eq = match fst eq with
+    | AST_assign(_, e) | AST_assume(_, e) ->
+        expr_g e
+    | AST_guarantee((id, _), e) ->
+        (id, f_and cond (f_of_expr td (node, prefix) (AST_not(e), snd e)))
+          :: (expr_g e)
+    | AST_activate (b, _) ->
+      let rec cond_g cond = function
+        | AST_activate_body b ->
+          g_of_scope td (node, b.act_id^".", b.body) cond
+        | AST_activate_if(c, a, b) ->
+          (cond_g (f_and cond (f_of_expr td (node, prefix) c)) a) @
+          (cond_g (f_and cond (f_of_expr td (node, prefix) (AST_not(c), snd c))) b) @
+          (expr_g c)
+      in
+      cond_g cond b
+    | AST_automaton _ -> not_implemented "g_of_scope automaton"
+  in
+  List.fold_left (@) [] (List.map do_eq eqs)
+
+and guarantees_of_prog p root =
+    let td = {
+      root_scope = get_root_scope p root;
+      p = p;
+      consts = I.consts p root;
+    } in
+
+    g_of_scope td (get_root_scope p root) (BConst true)
diff --git a/main.ml b/main.ml
index 0ddf91c..e98dd5f 100644
--- a/main.ml
+++ b/main.ml
@@ -2,8 +2,8 @@ open Ast
 
 module Interpret = Interpret.I
 
-module IntD = Nonrelational.D(Intervals_domain.VD)
-module AI_Int = Abs_interp.I(IntD)
+module ItvD = Nonrelational.D(Intervals_domain.VD)
+module AI_Itv = Abs_interp.I(ItvD)
 module AI_Rel = Abs_interp.I(Apron_domain.D)
 
 (* command line options *)
@@ -11,7 +11,7 @@ let dump = ref false
 let dumprn = ref false
 let test = ref false
 let vtest = ref false
-let ai_int = ref false
+let ai_itv = ref false
 let ai_rel = ref false
 let ai_root = ref "test"
 let ai_widen_delay = ref 3
@@ -24,7 +24,7 @@ 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-itv", Arg.Set ai_itv, "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).";
@@ -75,7 +75,7 @@ let () =
       let prog = Rename.rename_prog prog in
       if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
 
-      if !ai_int then AI_Int.do_prog !ai_widen_delay prog !ai_root;
+      if !ai_itv then AI_Itv.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
diff --git a/tests/Makefile b/tests/Makefile
index 7d5aac0..165f4ec 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -3,7 +3,7 @@ ALL_OUT=result/limiter.out result/limitera.out result/locals.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/gilbreath.out
+		result/gilbreath.out result/half.out
 
 bin/%.test: source/%.scade test.c
 	rm kcg/*
diff --git a/tests/result/half.out b/tests/result/half.out
new file mode 100644
index 0000000..c2085c5
--- /dev/null
+++ b/tests/result/half.out
@@ -0,0 +1,21 @@
+0. 1 0 1
+1. 1 1 0
+2. 2 1 1
+3. 2 2 0
+4. 3 2 1
+5. 3 3 0
+6. 4 3 1
+7. 4 4 0
+8. 5 4 1
+9. 5 5 0
+10. 6 5 1
+11. 6 6 0
+12. 7 6 1
+13. 7 7 0
+14. 8 7 1
+15. 8 8 0
+16. 9 8 1
+17. 9 9 0
+18. 10 9 1
+19. 10 10 0
+20. 11 10 1
diff --git a/tests/source/gilbreath.scade b/tests/source/gilbreath.scade
index 2723f9f..e0b7245 100644
--- a/tests/source/gilbreath.scade
+++ b/tests/source/gilbreath.scade
@@ -16,6 +16,8 @@ let
   half = false -> not pre half;
 
   property = true -> not (half and (o = pre o));
+
+  guarantee p_true : property;
 tel
 
 node test(i: int) returns (a, b, c: int; exit: bool)
diff --git a/tests/source/half.scade b/tests/source/half.scade
new file mode 100644
index 0000000..da90586
--- /dev/null
+++ b/tests/source/half.scade
@@ -0,0 +1,29 @@
+node test(i: int) returns (a, b, probe c: int; exit: bool)
+var
+  la, lb: int;
+  half: bool;
+let
+  exit = i >= 20;
+
+  half = true -> not pre half;
+
+  la = 0 -> pre a;
+  lb = 0 -> pre b;
+  activate
+    if half then
+      let
+        a = la + 1;
+        b = lb;
+      tel
+    else
+      let
+        a = la;
+        b = lb + 1;
+      tel
+  returns a, b;
+
+  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);
+tel
diff --git a/tests/source/limiter.scade b/tests/source/limiter.scade
index fc9fb30..05cb2b7 100644
--- a/tests/source/limiter.scade
+++ b/tests/source/limiter.scade
@@ -4,7 +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;
+        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 e6db4e2..2b87278 100644
--- a/tests/source/limitera.scade
+++ b/tests/source/limitera.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 = 16;
         guarantee out_bounded: y >= -bound and y <= bound;
         s = 0 -> pre y;
         r = x - s;