From d4ab85a1a6503cdbcb98c183c3357926d78da8a7 Mon Sep 17 00:00:00 2001
From: Alex AUVOLAT <alex.auvolat@ens.fr>
Date: Wed, 7 May 2014 19:04:38 +0200
Subject: implement assert, print

---
 abstract/constant_domain.ml    |  5 +++++
 abstract/environment_domain.ml |  5 +++++
 abstract/interpret.ml          | 29 ++++++++++++++++++++++++-----
 abstract/nonrelational.ml      | 26 ++++++++++++++++++++++++--
 abstract/value_domain.ml       |  3 +++
 5 files changed, 61 insertions(+), 7 deletions(-)

diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml
index 4bd5cf2..d142228 100644
--- a/abstract/constant_domain.ml
+++ b/abstract/constant_domain.ml
@@ -50,4 +50,9 @@ module Constants : VALUE_DOMAIN = struct
 				then Int a, Int b
 				else Bot, Bot
 		| x, y -> x, y
+	
+	let to_string = function
+		| Bot -> "bot"
+		| Top -> "top"
+		| Int i -> "{" ^ (Z.to_string i) ^ "}"
 end
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index f5614fe..254f755 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -6,6 +6,7 @@ module type ENVIRONMENT_DOMAIN = sig
 	(* construction *)
 	val init	: t
 	val bottom	: t
+	val is_bot  : t -> bool
 
 	(* variable management *)
 	val addvar	: t -> id -> t
@@ -22,6 +23,10 @@ module type ENVIRONMENT_DOMAIN = sig
 
 	(* order *)
 	val subset	: t -> t -> bool
+
+	(* pretty-printing *)
+	val var_str			: t -> id list -> string
+	val all_vars_str	: t -> string
 end
 
 
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index 51c7cd6..fe998a6 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -17,7 +17,14 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
 			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 *)
+		(* transformations *)
+		| AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
+			condition
+				(AST_binary(AST_OR, neg e1, neg e2), x) env
+		| AST_unary (AST_NOT, (AST_binary(AST_OR, e1, e2), x)) ->
+			condition
+				(AST_binary(AST_AND, neg e1, neg e2), x) env
+		| _ -> env (* TODO : encode some more transformations *)
 		end
 
 	let rec interp_stmt env stat =
@@ -39,19 +46,31 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
 			env
 		| AST_HALT -> E.bottom
 		| AST_assert (cond, l) ->
-			(* TODO *)
-			env
+			if not
+				(E.is_bot (condition (neg (cond, l)) env))
+			then begin
+				print_string (Abstract_syntax_printer.string_of_extent l);
+				print_string ": ERROR: assertion failure\n"
+			end;
+			condition (cond, l) env
 		| AST_print items ->
-			(* TODO *)
+			print_string (Abstract_syntax_printer.string_of_extent (snd stat));
+			print_string ": ";
+			print_string (E.var_str env (List.map fst items));
+			print_string "\n";
 			env
 		| _ -> assert false (* not implemented *)
 		end
 	
 	let interpret prog =
-		List.fold_left
+		let result = List.fold_left
 			(fun env x -> match x with
 				| AST_stat st -> interp_stmt env st
 				| _ -> env)
 			E.init
 			(fst prog)
+		in
+			print_string "Output: ";
+			print_string (E.all_vars_str result);
+			print_string "\n"
 end
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 6e2ff2b..d4118da 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -16,8 +16,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 	let get_var env id =
 		try VarMap.find id env
 		with Not_found -> V.top
-
-
+	
 	(* utilities *)
 
 	let rec eval env expr =
@@ -52,6 +51,10 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 
 	(* 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 rmvar x id = strict_apply (fun y -> Env (VarMap.remove id y)) x
 
@@ -100,4 +103,23 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 				(fun _ a b -> V.subset a b)
 				m n
 		
+	(* pretty-printing *)
+	let var_str env vars =
+		match env with
+		| Bot -> "bot"
+		| Env env ->
+			let v = List.fold_left
+				(fun s id ->
+					(if s = "" then s else s ^ ", ") ^
+						id ^ " in " ^ (V.to_string (get_var env id))
+					)
+				""
+				vars
+			in
+				"[ " ^ v ^ " ]"
+	
+	let all_vars_str env =
+		match env with
+		| Bot -> "bot"
+		| Env map -> var_str env (List.map fst (VarMap.bindings map))
 end
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
index a0f082f..9cf6d76 100644
--- a/abstract/value_domain.ml
+++ b/abstract/value_domain.ml
@@ -25,4 +25,7 @@ module type VALUE_DOMAIN = sig
 
 	(* 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
-- 
cgit v1.2.3