Restart anew ; done nonrelational stuff, interpret remains, intervals domain remains

7 files changed, 421 insertions, 153 deletions

diff --git a/abstract/_constant_domain.ml b/abstract/_constant_domain.ml
new file mode 100644
index 0000000..544d2e9
--- /dev/null
+++ b/abstract/_constant_domain.ml
@@ -0,0 +1,153 @@
+open Util
+open Abstract_syntax_tree
+
+module CD : Domain.S =
+  struct
+
+    exception DivideByZero
+    exception TypeError
+    exception Bot
+    exception NotImplemented
+
+    type tv =   (* type for a variable *)
+      | Top
+      | I of Z.t
+
+    type ts =   (* type for an environment *)
+      | Bot
+      | Nb of tv VarMap.t
+
+    let top_ts = Nb VarMap.empty
+
+    let ts_union a b =
+      begin match a, b with
+      | Bot, Bot -> Bot
+      | Nb a, Bot -> Nb a
+      | Bot, Nb b -> Nb b
+      | Nb a, Nb b ->
+        Nb
+          (VarMap.fold
+            (fun var value a ->
+              try match VarMap.find var a with
+                | Top -> a
+                | I x ->
+                  match value with
+                  | I y when y = x -> a
+                  | _ -> VarMap.add var Top a
+              with
+              | Not_found -> VarMap.add var value a)
+          b a)
+      end
+
+    (* must not raise exception *)
+    let ts_add_bool_constraint expr (s : ts) =
+      s (* TODO, not necessary... *)
+
+
+    (* only evaluates numerical statements, raises
+      TypeError when result is bool *)
+    let rec eval_abs expr (s : tv VarMap.t) =
+      match expr with
+      | AST_unary(op, (i, _)) ->
+        begin match eval_abs i s with
+        | Top -> Top
+        | I x ->
+          match op with
+          | AST_UNARY_PLUS -> I x
+          | AST_UNARY_MINUS -> I (Z.neg x)
+          | _ -> raise TypeError
+        end
+      | AST_binary(op, (a, _), (b, _)) ->
+        begin match eval_abs a s, eval_abs b s with
+        | I x, I  y ->
+          begin match op with
+          | AST_PLUS -> I (Z.add x y)
+          | AST_MINUS -> I (Z.sub x y)
+          | AST_MULTIPLY -> I (Z.mul x y)
+          | AST_DIVIDE ->
+            if y = Z.zero then raise DivideByZero;
+            I (Z.div x y)
+          | AST_MODULO ->
+            if y = Z.zero then raise DivideByZero;
+            I (Z.rem x y)
+          | _ -> raise TypeError
+          end
+        | _ -> Top
+        end
+      | AST_identifier(id, _) ->
+        begin
+          try VarMap.find id s
+          with _ -> Top
+        end 
+      | AST_int_const(s, _) ->
+        I (Z.of_string s)
+      | AST_bool_const(_) -> raise TypeError
+      | AST_int_rand _ -> Top
+      | _ -> raise NotImplemented (* extensions *)
+
+    (* returns true if the expression can evaluate to true
+      returns false if the expression always evaluates to false *)
+    let rec eval_bool_abs expr (s : tv VarMap.t) =
+      true (* TODO *)
+
+    (* must not raise exception *)
+    let rec interp_abs stat s =
+      begin match s with
+      | Bot -> Bot
+      | Nb vars ->
+        begin match stat with
+        | AST_block b ->
+          List.fold_left
+            (fun ss (st, _) -> interp_abs st ss)
+            s b
+        | AST_assign ((id, _), (exp, _)) ->
+          begin
+            try
+              let value = eval_abs exp vars in
+              Nb (VarMap.add id value vars)
+            with _ -> Bot
+          end
+        | AST_if ((cond, _), (tb, _), None) ->
+          ts_union (Nb vars)
+            (interp_abs tb
+              (ts_add_bool_constraint cond (Nb vars)))
+        | AST_if ((cond, l), (tb, _), Some (eb, _)) ->
+          ts_union
+            (interp_abs tb
+              (ts_add_bool_constraint cond (Nb vars)))
+            (interp_abs eb
+              (ts_add_bool_constraint 
+                  (AST_unary (AST_NOT, (cond, l)))
+                (Nb vars)))
+        | AST_while ((cond, _), (body, _)) ->
+          let f s =
+            ts_union
+              s
+              (ts_add_bool_constraint cond s)
+          in
+            fix f (Nb vars)
+        | AST_HALT -> Bot
+        | AST_assert (cond, _) ->
+          if eval_bool_abs cond vars
+            then Nb vars
+            else begin
+              print_string "Assert fail\n";
+              Bot
+            end
+        | AST_print items ->
+          List.iter
+            (fun (var, _) ->
+              print_string (var ^ " = ");
+              try
+                match VarMap.find var vars with
+                | Top -> print_string "T\n"
+                | I x -> print_string (Z.to_string x ^ "\n")
+              with _ -> print_string "T\n")
+            items;
+          Nb vars
+        | _ -> raise NotImplemented (* extensions *)
+        end
+      end
+
+  end
+
diff --git a/abstract/domain.ml b/abstract/_domain.ml
index 643a6ec..643a6ec 100644
--- a/abstract/domain.ml
+++ b/abstract/_domain.ml
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml
index 544d2e9..4bd5cf2 100644
--- a/abstract/constant_domain.ml
+++ b/abstract/constant_domain.ml
@@ -1,153 +1,53 @@
-open Util
-open Abstract_syntax_tree
-
-module CD : Domain.S =
-  struct
-
-    exception DivideByZero
-    exception TypeError
-    exception Bot
-    exception NotImplemented
-
-    type tv =   (* type for a variable *)
-      | Top
-      | I of Z.t
-
-    type ts =   (* type for an environment *)
-      | Bot
-      | Nb of tv VarMap.t
-
-    let top_ts = Nb VarMap.empty
-
-    let ts_union a b =
-      begin match a, b with
-      | Bot, Bot -> Bot
-      | Nb a, Bot -> Nb a
-      | Bot, Nb b -> Nb b
-      | Nb a, Nb b ->
-        Nb
-          (VarMap.fold
-            (fun var value a ->
-              try match VarMap.find var a with
-                | Top -> a
-                | I x ->
-                  match value with
-                  | I y when y = x -> a
-                  | _ -> VarMap.add var Top a
-              with
-              | Not_found -> VarMap.add var value a)
-          b a)
-      end
-
-    (* must not raise exception *)
-    let ts_add_bool_constraint expr (s : ts) =
-      s (* TODO, not necessary... *)
-
-
-    (* only evaluates numerical statements, raises
-      TypeError when result is bool *)
-    let rec eval_abs expr (s : tv VarMap.t) =
-      match expr with
-      | AST_unary(op, (i, _)) ->
-        begin match eval_abs i s with
-        | Top -> Top
-        | I x ->
-          match op with
-          | AST_UNARY_PLUS -> I x
-          | AST_UNARY_MINUS -> I (Z.neg x)
-          | _ -> raise TypeError
-        end
-      | AST_binary(op, (a, _), (b, _)) ->
-        begin match eval_abs a s, eval_abs b s with
-        | I x, I  y ->
-          begin match op with
-          | AST_PLUS -> I (Z.add x y)
-          | AST_MINUS -> I (Z.sub x y)
-          | AST_MULTIPLY -> I (Z.mul x y)
-          | AST_DIVIDE ->
-            if y = Z.zero then raise DivideByZero;
-            I (Z.div x y)
-          | AST_MODULO ->
-            if y = Z.zero then raise DivideByZero;
-            I (Z.rem x y)
-          | _ -> raise TypeError
-          end
-        | _ -> Top
-        end
-      | AST_identifier(id, _) ->
-        begin
-          try VarMap.find id s
-          with _ -> Top
-        end 
-      | AST_int_const(s, _) ->
-        I (Z.of_string s)
-      | AST_bool_const(_) -> raise TypeError
-      | AST_int_rand _ -> Top
-      | _ -> raise NotImplemented (* extensions *)
-
-    (* returns true if the expression can evaluate to true
-      returns false if the expression always evaluates to false *)
-    let rec eval_bool_abs expr (s : tv VarMap.t) =
-      true (* TODO *)
-
-    (* must not raise exception *)
-    let rec interp_abs stat s =
-      begin match s with
-      | Bot -> Bot
-      | Nb vars ->
-        begin match stat with
-        | AST_block b ->
-          List.fold_left
-            (fun ss (st, _) -> interp_abs st ss)
-            s b
-        | AST_assign ((id, _), (exp, _)) ->
-          begin
-            try
-              let value = eval_abs exp vars in
-              Nb (VarMap.add id value vars)
-            with _ -> Bot
-          end
-        | AST_if ((cond, _), (tb, _), None) ->
-          ts_union (Nb vars)
-            (interp_abs tb
-              (ts_add_bool_constraint cond (Nb vars)))
-        | AST_if ((cond, l), (tb, _), Some (eb, _)) ->
-          ts_union
-            (interp_abs tb
-              (ts_add_bool_constraint cond (Nb vars)))
-            (interp_abs eb
-              (ts_add_bool_constraint 
-                  (AST_unary (AST_NOT, (cond, l)))
-                (Nb vars)))
-        | AST_while ((cond, _), (body, _)) ->
-          let f s =
-            ts_union
-              s
-              (ts_add_bool_constraint cond s)
-          in
-            fix f (Nb vars)
-        | AST_HALT -> Bot
-        | AST_assert (cond, _) ->
-          if eval_bool_abs cond vars
-            then Nb vars
-            else begin
-              print_string "Assert fail\n";
-              Bot
-            end
-        | AST_print items ->
-          List.iter
-            (fun (var, _) ->
-              print_string (var ^ " = ");
-              try
-                match VarMap.find var vars with
-                | Top -> print_string "T\n"
-                | I x -> print_string (Z.to_string x ^ "\n")
-              with _ -> print_string "T\n")
-            items;
-          Nb vars
-        | _ -> raise NotImplemented (* extensions *)
-        end
-      end
-
-  end
-
+open Value_domain
+
+module Constants : VALUE_DOMAIN = struct
+	type t =
+		| Top
+		| Int of Z.t
+		| Bot
+	
+	let top = Top
+	let bottom = Bot
+	let const i = Int i
+	let rand i j = if i <> j then Top else Int i
+
+	let subset a b = match a, b with
+		| _, Top -> true
+		| Bot, _ -> true
+		| Int a, Int b -> a = b
+		| _, _ -> false
+	
+	let join a b = match a, b with
+		| Bot, x | x, Bot -> x
+		| Int a, Int b when a = b -> Int a
+		| _ -> Top
+	
+	let meet a b = match a, b with
+		| Top, x | x, Top -> x
+		| Int a, Int b when a = b -> Int a
+		| _ -> Bot
+	
+	let widen = meet		(* pas besoin d'accélerer la convergence au-delà *)
+
+	let neg = function
+		| Int a -> Int (Z.neg a)
+		| x -> x
+	
+	let b_aux op a b = match a, b with
+		| Int x, Int y -> Int (op x y)
+		| Bot, _ | _, Bot -> Bot
+		| _ -> Top
+	let add = b_aux Z.add
+	let sub = b_aux Z.sub
+	let mul = b_aux Z.mul
+	let div = b_aux Z.div
+	let rem = b_aux Z.rem
+
+	let leq a b =
+		match a, b with
+		| Int a, Int b when Z.leq a b ->
+			if Z.leq a b
+				then Int a, Int b
+				else Bot, Bot
+		| x, y -> x, y
+end
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
new file mode 100644
index 0000000..f5614fe
--- /dev/null
+++ b/abstract/environment_domain.ml
@@ -0,0 +1,27 @@
+open Abstract_syntax_tree
+
+module type ENVIRONMENT_DOMAIN = sig
+	type t
+
+	(* construction *)
+	val init	: t
+	val bottom	: t
+
+	(* variable management *)
+	val addvar	: t -> id -> t
+	val rmvar	: t -> id -> t
+
+	(* abstract operation *)
+	val assign	: t -> id -> expr ext -> t		(*    S[id <- expr]     *)
+	val compare : t -> expr ext -> expr ext -> t    (*    S[expr <= expr ?] *)
+
+	(* set-theoretic operations *)
+	val join 	: t -> t -> t		(* union *)
+	val meet	: t -> t -> t		(* intersection *)
+	val widen	: t -> t -> t
+
+	(* order *)
+	val subset	: t -> t -> bool
+end
+
+
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
new file mode 100644
index 0000000..51c7cd6
--- /dev/null
+++ b/abstract/interpret.ml
@@ -0,0 +1,57 @@
+open Abstract_syntax_tree
+open Environment_domain
+open Util
+
+module Make (E : ENVIRONMENT_DOMAIN) = struct
+
+	let neg (e, l) =
+		(AST_unary(AST_NOT, (e, l))), l
+
+	let rec condition cond env =
+		begin match fst cond with
+		| AST_binary (AST_LESS_EQUAL, e1, e2) ->
+			E.compare env e1 e2
+		| AST_binary (AST_GREATER_EQUAL, e1, e2) ->
+			E.compare env e2 e1
+		| AST_binary (AST_AND, e1, e2) ->
+			E.meet (condition e1 env) (condition e2 env)
+		| AST_binary (AST_OR, e1, e2) ->
+			E.join (condition e1 env) (condition e2 env)
+		| _ -> env (* TODO : encode some transformations *)
+		end
+
+	let rec interp_stmt env stat =
+		begin match fst stat with
+		| AST_block b ->
+			List.fold_left interp_stmt env b
+		| AST_assign ((id, _), exp) ->
+			E.assign env id exp
+		| AST_if (cond, tb, None) ->
+			E.join
+				(interp_stmt (condition cond env) tb)
+				(condition (neg cond) env)
+		| AST_if (cond, tb, Some eb) ->
+			E.join
+				(interp_stmt (condition cond env) tb)
+				(interp_stmt (condition (neg cond) env) eb)
+		| AST_while (cond, (body, _)) ->
+			(* TODO *)
+			env
+		| AST_HALT -> E.bottom
+		| AST_assert (cond, l) ->
+			(* TODO *)
+			env
+		| AST_print items ->
+			(* TODO *)
+			env
+		| _ -> assert false (* not implemented *)
+		end
+	
+	let interpret prog =
+		List.fold_left
+			(fun env x -> match x with
+				| AST_stat st -> interp_stmt env st
+				| _ -> env)
+			E.init
+			(fst prog)
+end
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
new file mode 100644
index 0000000..6e2ff2b
--- /dev/null
+++ b/abstract/nonrelational.ml
@@ -0,0 +1,103 @@
+open Abstract_syntax_tree
+open Util
+
+open Value_domain
+open Environment_domain
+
+
+module NonRelational (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 expr =
+		begin match fst expr with
+		| AST_identifier (id, _) -> get_var env id
+		| AST_int_const (s, _) -> V.const (Z.of_string s)
+		| AST_int_rand ((s, _), (t, _)) -> V.rand (Z.of_string s) (Z.of_string t)
+		| AST_unary (AST_UNARY_PLUS, e) -> eval env e
+		| AST_unary (AST_UNARY_MINUS, e) -> V.neg (eval env e)
+		| AST_unary (_, e) -> V.bottom
+		| AST_binary (op, e1, e2) ->
+			let f = match op with
+			| AST_PLUS -> V.add
+			| AST_MINUS -> V.sub
+			| AST_MULTIPLY -> V.mul
+			| AST_DIVIDE -> V.div
+			| AST_MODULO -> V.rem
+			| _ -> fun _ _ -> V.bottom
+			in f (eval env e1) (eval env e2)
+		| _ -> assert false (* unimplemented extension *)
+		end
+
+	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 addvar 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 assign x id expr = strict_apply
+		(fun env -> Env (VarMap.add id (eval env expr) env))
+		x
+	let compare x e1 e2 =
+		strict_apply (fun env -> match fst e1, fst e2 with
+				| AST_identifier(a, _), AST_identifier(b, _) ->
+					let v1, v2 = get_var env a, get_var env b in
+					let v1', v2' = V.leq v1 v2 in
+					Env (VarMap.add a v1' (VarMap.add b v1' env))
+				| AST_identifier(a, _), AST_int_const(s, _) ->
+					let v1, v2 = get_var env a, V.const (Z.of_string s) in
+					let v1', _ = V.leq v1 v2 in
+					Env (VarMap.add a v1' env)
+				| AST_int_const(s, _), AST_identifier(b, _) ->
+					let v1, v2 = V.const (Z.of_string s), get_var env b in
+					let _, v2' = V.leq v1 v2 in
+					Env (VarMap.add b v2' env)
+				| _ -> Env env)
+			x
+
+	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)
+	
+	let subset a b = match a, b with
+		| Bot, x -> true
+		| Env _, Bot -> false
+		| Env m, Env n ->
+			VarMap.for_all2o
+				(fun _ _ -> true)
+				(fun _ _ -> true)
+				(fun _ a b -> V.subset a b)
+				m n
+		
+end
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
new file mode 100644
index 0000000..a0f082f
--- /dev/null
+++ b/abstract/value_domain.ml
@@ -0,0 +1,28 @@
+module type VALUE_DOMAIN = sig
+	type t
+
+	(* constructors *)
+	val top		: t
+	val bottom	: t
+	val const	: Z.t -> t
+	val rand	: Z.t -> Z.t -> 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]) *)
+end