Add intervals domain ; some interesting analysis works.

6 files changed, 434 insertions, 17 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 1838591..0a330c2 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -88,7 +88,7 @@ end = struct
       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_conslist cl;
+      Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f;
 
       { p; root_scope; f; cl; all_vars; env }
 
@@ -116,24 +116,32 @@ end = struct
                  not (List.exists (fun (_, id2, _) -> id2 = "N"^id) vars))
               vars) in
       let e = List.fold_left E.forgetvar e forget_vars in
-      Format.printf "Pass cycle: %a@.@." E.print_all e;
       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'
+
     (*
       do_prog : prog -> id -> st
     *)
     let do_prog p root =
       let st = init_state p root in
 
-      let rec step acc i n =
-        Format.printf "Step %d: %a@." n E.print_all acc;
+      let _, acc = cycle st st.env in
+
+      let rec step acc n =
         if n < 10 then begin
-          let i' = E.apply_cl (E.join i acc) st.cl in
-          let j = pass_cycle st.all_vars i' in
-          let acc' = (if n > 6 then E.widen else E.join) acc j in
-          step acc' i (n+1)
+          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 acc' = (if n >= 7 then E.widen else E.join) acc j in
+          step acc' (n+1)
         end
       in
-      step (E.vbottom st.env) st.env 0
+      step acc 0
 end
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index 5dbd08f..8b2ee34 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -16,11 +16,6 @@ module type ENVIRONMENT_DOMAIN = sig
     val vars        : t -> (id * bool) list
     val vbottom     : t -> t       (* bottom value with same environment *)
 
-    (* abstract operation *)
-    val apply_f     : t -> bool_expr -> t
-    val apply_cl    : t -> conslist -> t
-    val assign      : t -> (id * num_expr) list -> t
-
     (* set-theoretic operations *)
     val join        : t -> t -> t       (* union *)
     val meet        : t -> t -> t       (* intersection *)
@@ -30,6 +25,11 @@ module type ENVIRONMENT_DOMAIN = sig
     val subset      : t -> t -> bool
     val eq          : t -> t -> bool
 
+    (* abstract operation *)
+    val apply_f     : t -> bool_expr -> t
+    val apply_cl    : t -> conslist -> t
+    val assign      : t -> (id * num_expr) list -> t
+
     (* pretty-printing *)
     val print_vars  : Format.formatter -> t -> id list -> unit
     val print_all   : Format.formatter -> t -> unit
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 994c82a..25b7b22 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -91,15 +91,18 @@ let print_expr fmt e =
 
 (* Print constraint list form of formula *)
 
-let print_cons fmt (eq, sg) =
+let print_cons_sg fmt sg =
   let sg_str = match sg with
   | CONS_EQ -> "="
   | CONS_NE -> "≠"
   | CONS_GT -> ">"
   | CONS_GE -> "≥"
   in
-  Format.fprintf fmt "@[<hv 2>%a %s 0@]"
-    print_num_expr eq sg_str
+  Format.fprintf fmt "%s" sg_str
+
+let print_cons fmt (eq, sg) =
+  Format.fprintf fmt "@[<hv 2>%a %a 0@]"
+    print_num_expr eq print_cons_sg sg
 
 let rec print_conslist fmt (cons, e) =
   let rec aux = function
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
new file mode 100644
index 0000000..848f634
--- /dev/null
+++ b/abstract/intervals_domain.ml
@@ -0,0 +1,158 @@
+open Value_domain
+
+module VD : VALUE_DOMAIN = struct
+    type bound = Int of int | PInf | MInf
+
+    type t = Itv of bound * bound | Bot
+
+    (* utilities *)
+    let bound_leq a b =   (* a <= b ? *)
+        match a, b with
+        | MInf, _ | _, PInf -> true
+        | Int a, Int b -> a <= b
+        | x, y -> x = y
+
+    let bound_add a b =
+        match a, b with
+        | MInf, Int a | Int a, MInf -> MInf
+        | PInf, Int a | Int a, PInf -> PInf
+        | MInf, MInf -> MInf
+        | PInf, PInf -> PInf
+        | Int a, Int b -> Int (a + b)
+        | _ -> assert false
+    let bound_mul a b =
+        match a, b with
+        | PInf, Int(x) | Int(x), PInf ->
+            if x > 0 then PInf
+            else if x < 0 then MInf
+            else Int 0
+        | MInf, Int(x) | Int(x), MInf ->
+            if x < 0 then PInf
+            else if x > 0 then MInf
+            else Int 0
+        | Int(x), Int(y) -> Int(x * y)
+        | MInf, PInf | PInf, MInf -> MInf
+        | MInf, MInf | PInf, PInf -> PInf
+	let bound_div a b =
+		match a, b with
+		| _, PInf | _, MInf -> Int 0
+		| PInf, Int i ->
+			if i < 0 then MInf
+			else PInf
+		| MInf, Int i ->
+			if i < 0 then PInf
+			else MInf
+		| Int i, Int j ->
+			assert (j != 0);
+			Int (i / j)
+
+
+    let bound_min a b = match a, b with
+        | MInf, _ | _, MInf -> MInf
+        | Int a, Int b -> Int (min a b)
+        | Int a, PInf -> Int a
+        | PInf, Int a -> Int a
+        | PInf, PInf -> PInf
+    let bound_max a b = match a, b with
+        | PInf, _ | _, PInf -> PInf
+        | Int a, Int b -> Int (max a b)
+        | Int a, MInf | MInf, Int a -> Int a
+        | MInf, MInf -> MInf
+
+    let bound_neg = function
+        | PInf -> MInf
+        | MInf -> PInf
+        | Int i -> Int (- i)
+	
+	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
+
+    let subset a b = match a, b with
+        | Bot, _ -> true
+        | _, Bot -> false
+        | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
+
+    let join a b = match a, b with
+        | Bot, x | x, Bot -> x
+        | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)
+
+    let meet a b = match a, b with
+        | Bot, x | x, Bot -> Bot
+        | Itv(a, b), Itv(c, d) ->
+            let u, v = bound_max a c, bound_min b d in
+            if bound_leq u v
+            then Itv(u, v)
+            else Bot
+
+    let widen a b = match a, b with
+        | x, Bot | Bot, x -> x
+        | Itv(a, b), Itv(c, d) ->
+            Itv(
+            (if not (bound_leq a c) then
+                (if bound_leq (Int 0) c then Int 0 else MInf)
+              else a),
+            (if not (bound_leq d b) then
+                (if bound_leq d (Int 0) then Int 0 else PInf)
+              else b))
+
+    let neg = function
+        | Bot -> Bot
+        | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
+    let add a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
+    let sub a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
+    let mul a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) ->
+            Itv(
+                (bound_min (bound_min (bound_mul a c) (bound_mul a d))
+                            (bound_min (bound_mul b c) (bound_mul b d))),
+                (bound_max (bound_max (bound_mul a c) (bound_mul a d))
+                            (bound_max (bound_mul b c) (bound_mul b d))))
+    let div a b = match a, b with
+        | Bot, _ -> Bot
+        | Itv(a, b), q ->
+			let p1 = match meet q (Itv(Int 1, PInf)) with
+				| Bot -> Bot
+				| Itv(c, d) ->
+					Itv(min (bound_div a c) (bound_div a d), max (bound_div b c) (bound_div b d))
+			in
+			let p2 = match meet q (Itv(MInf, Int (-1))) with
+				| Bot -> Bot
+				| Itv(c, d) ->
+					Itv(min (bound_div b c) (bound_div b d), max (bound_div a c) (bound_div a d))
+			in
+			join p1 p2
+    let rem a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) ->
+			Itv(
+				Int 0,
+				bound_max (bound_abs c) (bound_abs d)
+			)
+
+    let leq a b = match a, b with
+        | Bot, _ | _, Bot -> Bot, Bot
+        | Itv(a, b), Itv(c, d) ->
+            if not (bound_leq a d)
+            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) ^ "]"
+
+end
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
new file mode 100644
index 0000000..f5c9a04
--- /dev/null
+++ b/abstract/nonrelational.ml
@@ -0,0 +1,217 @@
+open Formula
+open Util
+open Ast
+
+open Value_domain
+open Environment_domain
+
+let debug = false
+
+(* Restricted domain, only support integers *)
+
+module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
+    type env = V.t VarMap.t
+
+    type t = Env of env | Bot
+
+    let init = Env VarMap.empty
+    let bottom = Bot
+
+    let get_var env id =
+        try VarMap.find id env
+        with Not_found -> V.top
+    
+    (* utilities *)
+
+    let rec eval env = function
+        | NIdent id -> get_var env id
+        | NIntConst i -> V.const i
+        | NRealConst f -> V.const (int_of_float f) (* TODO floats *)
+        | NUnary (AST_UPLUS, e) -> eval env e
+        | NUnary (AST_UMINUS, e) -> V.neg (eval env e)
+        | NBinary (op, e1, e2) ->
+            let f = match op with
+            | AST_PLUS -> V.add
+            | AST_MINUS -> V.sub
+            | AST_MUL -> V.mul
+            | AST_DIV -> V.div
+            | AST_MOD -> V.rem
+            in f (eval env e1) (eval env e2)
+
+    let strict env =                    (*      env -> t        *)
+        if VarMap.exists (fun _ x -> x = V.bottom) env
+            then Bot
+            else Env env
+    let strict_apply f = function       (* (env -> t) -> t -> t *)
+        | Bot -> Bot
+        | Env e -> match f e with
+            | Bot -> Bot
+            | Env e -> strict e
+
+    (* implementation *)
+
+    let is_bot env = match env with
+        | Bot -> true
+        | Env env -> strict env = Bot
+
+    let addvar x id _ = strict_apply (fun y -> Env (VarMap.add id V.top y)) x
+    let forgetvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x
+    let rmvar x id = strict_apply (fun y -> Env (VarMap.remove id y)) x
+
+    let vars env = match env with
+        | Bot -> []
+        | Env env -> List.map (fun (k, _) -> (k, false)) (VarMap.bindings env)
+    let vbottom _ = bottom
+
+    (* Set-theoretic operations *)
+    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)
+    
+    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)
+
+    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)
+
+    (* Inclusion and equality *)
+    let subset a b = match a, b with
+        | Bot, x -> true
+        | Env _, Bot -> false
+        | Env m, Env n ->
+            VarMap.for_all2o
+                (fun _ _ -> true)
+                (fun _ v -> v = V.top)
+                (fun _ a b -> V.subset a b)
+                m n
+
+    let eq a b = match a, b with
+        | Bot, Bot -> true
+        | Env m, Env n ->
+            VarMap.for_all2o
+                (fun _ _ -> false)
+                (fun _ _ -> false)
+                (fun _ a b -> a = b)
+                m n
+        | _ -> false
+
+    (* Apply some formula to the environment *)
+    let apply_cons env (expr, sign) =
+        let inv_op = function
+          | AST_LT -> AST_GT
+          | AST_GT -> AST_LT
+          | AST_LE -> AST_GE
+          | AST_GE -> AST_LE
+          | x -> x
+        in
+        let rec extract_var (lhs, op, rhs) =
+          match lhs with
+          | NIdent i -> [i, op, rhs]
+          | NIntConst _ | NRealConst _ -> []
+          | NUnary(AST_UPLUS, x) -> extract_var (x, op, rhs)
+          | NUnary(AST_UMINUS, x) ->
+            extract_var (x, inv_op op, NUnary(AST_UMINUS, x))
+          | NBinary(AST_PLUS, a, b) ->
+            extract_var (a, op, NBinary(AST_MINUS, rhs, b)) @
+            extract_var (b, op, NBinary(AST_MINUS, rhs, a))
+          | NBinary(AST_MINUS, a, b) ->
+            extract_var (a, op, NBinary(AST_PLUS, rhs, b)) @
+            extract_var (b, inv_op op, NBinary(AST_MINUS, a, rhs))
+          | NBinary(AST_MUL, a, b) ->
+            extract_var (a, op, NBinary(AST_DIV, rhs, b)) @
+            extract_var (b, op, NBinary(AST_DIV, rhs, a))
+          | NBinary(AST_DIV, a, b) ->
+            extract_var (a, op, NBinary(AST_MUL, rhs, b)) @
+            extract_var (b, inv_op op, NBinary(AST_DIV, a, rhs))
+          | NBinary(AST_MOD, _, _) -> []
+        in
+        let zop = match sign with
+          | CONS_EQ -> AST_EQ | CONS_NE -> AST_NE
+          | CONS_GT -> AST_GT | CONS_GE -> AST_GE
+        in
+        let restrict_var env (i, op, expr) =
+          strict_apply (fun env ->
+            let v1, v2 = get_var env i, eval env expr in
+            let v1' = match op with
+            | AST_EQ -> V.meet v1 v2
+            | AST_NE -> v1
+            | AST_LE -> let u, _ = V.leq v1 v2 in u
+            | AST_GE -> let _, v = V.leq v2 v1 in v
+            | AST_LT -> let u, _ = V.leq v1 (V.sub v2 (V.const 1)) in u
+            | AST_GT -> let _, v = V.leq (V.add v2 (V.const 1)) v1 in v
+            in
+            if debug then Format.printf
+              "restrict %s %s @[<hv>%a@] : %s %s -> %s@." i 
+              (Formula_printer.string_of_binary_rel op)
+              Formula_printer.print_num_expr expr
+              (V.to_string v1) (V.to_string v2) (V.to_string v1');
+            Env (VarMap.add i v1' env))
+          env
+        in
+        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
+        | 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 ">>@.";
+          join y z
+
+    let apply_f x f = apply_cl x (conslist_of_f f)
+
+    (* Assignment *)
+    let assign x exprs =
+        let aux env =
+          let vars = List.map (fun (id, v) -> (id, eval env v)) exprs in
+          let env2 =
+            List.fold_left (fun e (id, v) -> VarMap.add id v e)
+              env vars
+          in Env env2
+        in
+        strict_apply aux x
+
+        
+    (* pretty-printing *)
+    let print_vars fmt env ids =
+        match env with
+        | Bot -> Format.fprintf fmt "bottom"
+        | 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 "]@]"
+
+    let print_all fmt x =
+        print_vars fmt x (List.map fst (vars x))
+    
+end
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
new file mode 100644
index 0000000..fb01ac6
--- /dev/null
+++ b/abstract/value_domain.ml
@@ -0,0 +1,31 @@
+module type VALUE_DOMAIN = sig
+    type t
+
+    (* constructors *)
+    val top     : t
+    val bottom  : t
+    val const   : int -> t
+    val rand    : int -> int -> t
+
+    (* order *)
+    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
+
+    (* 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
+
+    (* boolean test *)
+    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
+end