From 9ccef2c0850b73bf3d92f26bfa0aeacf933e1d17 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 7 May 2014 17:41:06 +0200 Subject: Restart anew ; done nonrelational stuff, interpret remains, intervals domain remains --- abstract/interpret.ml | 57 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 abstract/interpret.ml (limited to 'abstract/interpret.ml') 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 -- cgit v1.2.3