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

1 files changed, 57 insertions, 0 deletions

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