From d4ab85a1a6503cdbcb98c183c3357926d78da8a7 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 7 May 2014 19:04:38 +0200 Subject: implement assert, print --- abstract/interpret.ml | 29 ++++++++++++++++++++++++----- 1 file changed, 24 insertions(+), 5 deletions(-) (limited to 'abstract/interpret.ml') 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 -- cgit v1.2.3