path: root/abstract/interpret.ml

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)
		(* 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 =
		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) ->
			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 ->
			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 =
		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