Pretty printing.

8 files changed, 147 insertions, 66 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 0a330c2..4f66540 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -119,29 +119,61 @@ end = struct
       e
 
 
-    (* cycle : st -> env -> env *)
-    let cycle st i =
-      let i' = E.apply_cl i st.cl in
-      i', pass_cycle st.all_vars i'
+    (* cycle : st -> cl -> env -> env *)
+    let cycle st cl i =
+      E.apply_cl (pass_cycle st.all_vars i) cl
 
     (*
-      do_prog : prog -> id -> st
+      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
+        E.print_all pnew E.print_all stay;
+
+      let add_stay = cycle st cycle_cl pnew in
+      let acc0 = E.join stay add_stay in
+
+      let fsharp i = 
+        Format.printf "Acc @[<hv>%a@]@." E.print_all i;
+        let j = cycle st cycle_cl i in
+        E.join acc0 j
+      in
+
+      let widen_delay = 2 in
+      let rec iter n i =
+        let i' =
+          if n < widen_delay
+            then E.join i (fsharp i)
+            else E.widen i (fsharp 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 *)
+
+
+    (*
+      do_prog : prog -> id -> unit
     *)
     let do_prog p root =
       let st = init_state p root in
 
-      let _, acc = cycle st st.env in
+      let pnew = st.env in
 
-      let rec step acc n =
-        if n < 10 then begin
-          Format.printf "Step %d: %a@." n E.print_all acc;
-          let i', j = cycle st acc in
-          Format.printf " -> %a@." E.print_all i';
-          Format.printf "Pass cycle: %a@.@." E.print_all j;
+      let stay = loop st st.cl pnew (E.vbottom pnew) in
 
-          let acc' = (if n >= 7 then E.widen else E.join) acc j in
-          step acc' (n+1)
-        end
-      in
-      step acc 0
+      Format.printf "@[<hov>Final stay %a@]@."
+        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
 end
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index ad483ec..d13afd7 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -12,6 +12,8 @@ module D : ENVIRONMENT_DOMAIN = struct
     type man = Polka.loose Polka.t
     let manager = Polka.manager_alloc_loose ()
 
+    type itv = Interval.t
+
     (* abstract elements *)
     type t = man Abstract1.t
 
@@ -87,6 +89,9 @@ module D : ENVIRONMENT_DOMAIN = struct
     let vbottom x =
         Abstract1.bottom manager (Abstract1.env x)
 
+    let var_itv x id =
+        Abstract1.bound_variable manager x (Var.of_string id)
+
     (* Apply some formula to the environment *)
     let rec apply_cl x (cons, rest) =
         let env = Abstract1.env x in
@@ -139,5 +144,7 @@ module D : ENVIRONMENT_DOMAIN = struct
         let xx = Abstract1.forget_array manager x rm_vars false in
         print_all fmt xx
 
+    let print_itv = Interval.print
+
 end
 
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index 8b2ee34..6e84c75 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -3,6 +3,7 @@ open Formula
 
 module type ENVIRONMENT_DOMAIN = sig
     type t
+    type itv
 
     (* construction *)
     val init        : t
@@ -15,6 +16,7 @@ module type ENVIRONMENT_DOMAIN = sig
     val rmvar       : t -> id -> t
     val vars        : t -> (id * bool) list
     val vbottom     : t -> t       (* bottom value with same environment *)
+    val var_itv     : t -> id -> itv
 
     (* set-theoretic operations *)
     val join        : t -> t -> t       (* union *)
@@ -33,6 +35,7 @@ module type ENVIRONMENT_DOMAIN = sig
     (* pretty-printing *)
     val print_vars  : Format.formatter -> t -> id list -> unit
     val print_all   : Format.formatter -> t -> unit
+    val print_itv   : Format.formatter -> itv -> unit
 end
 
 
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 2c83b32..262bccb 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -69,13 +69,17 @@ and conslist_bool_expr =
 let rec conslist_of_f = function
   | BNot e -> conslist_of_f (eliminate_not_negate e)
   | BRel (op, a, b) ->
-    let cons = match op with
-      | AST_EQ -> NBinary(AST_MINUS, a, b), CONS_EQ
-      | AST_NE -> NBinary(AST_MINUS, a, b), CONS_NE
-      | AST_GT -> NBinary(AST_MINUS, a, b), CONS_GT
-      | AST_GE -> NBinary(AST_MINUS, a, b), CONS_GE
-      | AST_LT -> NBinary(AST_MINUS, b, a), CONS_GT
-      | AST_LE -> NBinary(AST_MINUS, b, a), CONS_GE
+    let x, y, op = match op with
+      | AST_EQ -> a, b, CONS_EQ
+      | AST_NE -> a, b, CONS_NE
+      | AST_GT -> a, b, CONS_GT
+      | AST_GE -> a, b, CONS_GE
+      | AST_LT -> b, a, CONS_GT
+      | AST_LE -> b, a, CONS_GE
+    in
+    let cons = if y = NIntConst 0
+      then (x, op)
+      else (NBinary(AST_MINUS, x, y), op)
     in [cons], CLTrue
   | BConst x ->
     [], if x then CLTrue else CLFalse
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 25b7b22..53a9b6a 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -39,12 +39,15 @@ let print_ah fmt pf fa a fe e =
     then Format.fprintf fmt "@[<hv 2>(%a)@]" pf a
     else Format.fprintf fmt "@[<hv 2>%a@]" pf a
 
+let print_id fmt id =
+    let re = Str.regexp "/" in
+    Format.fprintf fmt "%s" (Str.global_replace re "·" id)
+
 let rec print_num_expr fmt e = match e with
   | NIntConst i -> Format.fprintf fmt "%d" i
   | NRealConst f -> Format.fprintf fmt "%f" f
   | NIdent id ->
-    let re = Str.regexp "/" in
-    Format.fprintf fmt "%s" (Str.global_replace re "·" id)
+    print_id fmt id
   | NBinary(op, a, b) ->
     print_ch fmt print_num_expr ne_prec a ne_prec e;
     Format.fprintf fmt "@ %s " (string_of_binary_op op);
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
index 848f634..181266b 100644
--- a/abstract/intervals_domain.ml
+++ b/abstract/intervals_domain.ml
@@ -1,9 +1,7 @@
 open Value_domain
 
 module VD : VALUE_DOMAIN = struct
-    type bound = Int of int | PInf | MInf
-
-    type t = Itv of bound * bound | Bot
+    type t = itv
 
     (* utilities *)
     let bound_leq a b =   (* a <= b ? *)
@@ -64,14 +62,18 @@ module VD : VALUE_DOMAIN = struct
         | MInf -> PInf
         | Int i -> Int (- i)
 	
-	let bound_abs a = bound_max a (bound_neg a)
+    let bound_abs a = bound_max a (bound_neg a)
 
     (* implementation *)
     let top = Itv(MInf, PInf)
     let bottom = Bot
     let const i = Itv(Int i, Int i)
     let rand i j =
-    if i <= j then Itv(Int i, Int j) else Bot
+        if i <= j then Itv(Int i, Int j) else Bot
+    let to_itv x = x
+    let as_const = function
+      | Itv(Int i, Int j) when i = j -> Some i
+      | _ -> None
 
     let subset a b = match a, b with
         | Bot, _ -> true
@@ -147,12 +149,6 @@ module VD : VALUE_DOMAIN = struct
             then Bot, Bot
             else Itv(a, bound_min b d), Itv(bound_max a c, d)
 
-    let bound_str = function
-        | MInf -> "-oo"
-        | PInf -> "+oo"
-        | Int i -> string_of_int i
-    let to_string = function
-        | Bot -> "bot"
-        | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
+    let to_string = string_of_itv
 
 end
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index f5c9a04..b83edc1 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -13,6 +13,7 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
     type env = V.t VarMap.t
 
     type t = Env of env | Bot
+    type itv = Value_domain.itv
 
     let init = Env VarMap.empty
     let bottom = Bot
@@ -63,6 +64,10 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
         | Env env -> List.map (fun (k, _) -> (k, false)) (VarMap.bindings env)
     let vbottom _ = bottom
 
+    let var_itv x id = match x with
+        | Bot -> Value_domain.Bot
+        | Env env -> V.to_itv (get_var env id)
+
     (* Set-theoretic operations *)
     let join a b = match a, b with
         | Bot, x | x, Bot -> x
@@ -196,22 +201,39 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
     (* pretty-printing *)
     let print_vars fmt env ids =
         match env with
-        | Bot -> Format.fprintf fmt "bottom"
+        | Bot -> Format.fprintf fmt "⊥"
         | Env env ->
-            Format.fprintf fmt "@[<hov 2>[";
-            let _ = List.fold_left
-                (fun nf id ->
-                  let v = get_var env id in
-                  if v <> V.top then begin
-                    if nf then Format.fprintf fmt ",@ ";
-                    Format.fprintf fmt "%s in %s" id (V.to_string (get_var env id));
-                    true
-                  end else nf)
-                false
-                ids
-            in Format.fprintf fmt "]@]"
+            Format.fprintf fmt "@[<v 2>{ ";
+            let l = List.map (fun id -> (get_var env id, id)) ids in
+            let s = List.sort Pervasives.compare l in
+            let rec bl = function
+              | [] -> []
+              | (v, id)::q when v <> V.top ->
+                begin match bl q with
+                | (vv, ids)::q when vv = v -> (v, id::ids)::q
+                | r -> (v, [id])::r
+                end
+              | _::q -> bl q
+            in
+            let sbl = bl s in
+            List.iteri
+              (fun j (v, ids) ->
+                if j > 0 then Format.fprintf fmt "@ ";
+                List.iteri
+                  (fun i id ->
+                    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))
+              sbl;
+            Format.fprintf fmt " }@]"
 
     let print_all fmt x =
         print_vars fmt x (List.map fst (vars x))
+
+    let print_itv fmt x =
+        Format.fprintf fmt "%s" (string_of_itv x)
     
 end
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
index fb01ac6..7b9d557 100644
--- a/abstract/value_domain.ml
+++ b/abstract/value_domain.ml
@@ -1,30 +1,44 @@
+
+type bound = Int of int | PInf | MInf
+type itv = Itv of bound * bound | Bot
+
+let string_of_bound = function
+    | MInf -> "-oo"
+    | PInf -> "+oo"
+    | Int i -> string_of_int i
+let string_of_itv = function
+    | Bot -> "⊥"
+    | Itv(a, b) -> "[" ^ (string_of_bound a) ^ ";" ^ (string_of_bound b) ^ "]"
+
 module type VALUE_DOMAIN = sig
     type t
 
     (* constructors *)
-    val top     : t
-    val bottom  : t
-    val const   : int -> t
-    val rand    : int -> int -> t
+    val top      : t
+    val bottom   : t
+    val const    : int -> t
+    val rand     : int -> int -> t
+    val to_itv   : t -> itv
+    val as_const : t -> int option
 
     (* order *)
-    val subset  : t -> t -> bool
+    val subset   : t -> t -> bool
 
     (* set-theoretic operations *)
-    val join    : t -> t -> t   (* union *)
-    val meet    : t -> t -> t   (* intersection *)
-    val widen   : t -> t -> t
+    val join     : t -> t -> t   (* union *)
+    val meet     : t -> t -> t   (* intersection *)
+    val widen    : t -> t -> t
 
     (* arithmetic operations *)
-    val neg     : t -> t
-    val add     : t -> t -> t
-    val sub     : t -> t -> t
-    val mul     : t -> t -> t
-    val div     : t -> t -> t
-    val rem     : t -> t -> t
+    val neg      : t -> t
+    val add      : t -> t -> t
+    val sub      : t -> t -> t
+    val mul      : t -> t -> t
+    val div      : t -> t -> t
+    val rem      : t -> t -> t
 
     (* boolean test *)
-    val leq     : t -> t -> t * t   (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *)
+    val leq      : t -> t -> t * t   (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *)
 
     (* pretty-printing *)
     val to_string : t -> string