From 77df0b0f119fc70624e4b830320a2b3e1034f7b5 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 21 May 2014 18:07:37 +0200 Subject: Just retab (many lines changed for nothing) --- abstract/interpret.ml | 228 +++++++++++++++++++++++++------------------------- 1 file changed, 114 insertions(+), 114 deletions(-) (limited to 'abstract/interpret.ml') diff --git a/abstract/interpret.ml b/abstract/interpret.ml index 5f03775..c599a76 100644 --- a/abstract/interpret.ml +++ b/abstract/interpret.ml @@ -4,94 +4,94 @@ open Util module Make (E : ENVIRONMENT_DOMAIN) = struct - let neg (e, l) = - (AST_unary(AST_NOT, (e, l))), l + let neg (e, l) = + (AST_unary(AST_NOT, (e, l))), l - let binop op (e, l) e2 = - (AST_binary (op, (e,l), e2)), l - let m1 (e, l) = - binop AST_MINUS (e, l) (AST_int_const("1", l), l) - let p1 (e, l) = - binop AST_PLUS (e, l) (AST_int_const("1", l), l) + let binop op (e, l) e2 = + (AST_binary (op, (e,l), e2)), l + let m1 (e, l) = + binop AST_MINUS (e, l) (AST_int_const("1", l), l) + let p1 (e, l) = + binop AST_PLUS (e, l) (AST_int_const("1", l), l) let bottom_with_vars = List.fold_left E.addvar E.bottom - let rec condition cond env = - begin match fst cond with - | AST_binary (AST_LESS_EQUAL, e1, e2) -> - E.compare_leq env e1 e2 - | AST_binary (AST_EQUAL, e1, e2) -> + let rec condition cond env = + begin match fst cond with + | AST_binary (AST_LESS_EQUAL, e1, e2) -> + E.compare_leq env e1 e2 + | AST_binary (AST_EQUAL, e1, e2) -> E.compare_eq env e1 e2 - | 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) + | 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 : remove not *) - | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) -> - condition cond env - | 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 + (* transformations : remove not *) + | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) -> + condition cond env + | 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 - | AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) -> - let op2 = match op with - | AST_LESS_EQUAL -> AST_GREATER - | AST_LESS -> AST_GREATER_EQUAL - | AST_GREATER_EQUAL -> AST_LESS - | AST_GREATER -> AST_LESS_EQUAL - | AST_EQUAL -> AST_NOT_EQUAL - | AST_NOT_EQUAL -> AST_EQUAL - | _ -> assert false - in - condition (binop op2 e1 e2) env - - (* transformations : encode everything with leq *) - | AST_binary(AST_LESS, e1, e2) -> - condition - (binop AST_AND (binop AST_LESS_EQUAL e1 (m1 e2)) - (binop AST_LESS_EQUAL (p1 e1) e2)) - env - | AST_binary (AST_GREATER_EQUAL, e1, e2) -> - condition - (binop AST_LESS_EQUAL e2 e1) - env - | AST_binary (AST_GREATER, e1, e2) -> - condition - (binop AST_LESS e2 e1) - env - | AST_binary (AST_NOT_EQUAL, e1, e2) -> - condition - (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1)) - env + | AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) -> + let op2 = match op with + | AST_LESS_EQUAL -> AST_GREATER + | AST_LESS -> AST_GREATER_EQUAL + | AST_GREATER_EQUAL -> AST_LESS + | AST_GREATER -> AST_LESS_EQUAL + | AST_EQUAL -> AST_NOT_EQUAL + | AST_NOT_EQUAL -> AST_EQUAL + | _ -> assert false + in + condition (binop op2 e1 e2) env + + (* transformations : encode everything with leq *) + | AST_binary(AST_LESS, e1, e2) -> + condition + (binop AST_AND (binop AST_LESS_EQUAL e1 (m1 e2)) + (binop AST_LESS_EQUAL (p1 e1) e2)) + env + | AST_binary (AST_GREATER_EQUAL, e1, e2) -> + condition + (binop AST_LESS_EQUAL e2 e1) + env + | AST_binary (AST_GREATER, e1, e2) -> + condition + (binop AST_LESS e2 e1) + env + | AST_binary (AST_NOT_EQUAL, e1, e2) -> + condition + (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1)) + env - | _ -> env - end + | _ -> env + end - let rec interp_stmt env stat = - begin match fst stat with - | AST_block b -> - (* remember to remove vars that have gone out of scope at the end *) - let prevars = E.vars env in - let env2 = List.fold_left interp_stmt env b in - let postvars = E.vars env2 in - let rmvars = List.filter (fun x -> not (List.mem x prevars)) postvars in - List.fold_left E.rmvar env2 rmvars - | 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) -> - let e1 = (interp_stmt (condition cond env) tb) in - let e2 = (interp_stmt (condition (neg cond) env) eb) in - E.join e1 e2 - | AST_while (cond, body) -> + let rec interp_stmt env stat = + begin match fst stat with + | AST_block b -> + (* remember to remove vars that have gone out of scope at the end *) + let prevars = E.vars env in + let env2 = List.fold_left interp_stmt env b in + let postvars = E.vars env2 in + let rmvars = List.filter (fun x -> not (List.mem x prevars)) postvars in + List.fold_left E.rmvar env2 rmvars + | 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) -> + let e1 = (interp_stmt (condition cond env) tb) in + let e2 = (interp_stmt (condition (neg cond) env) eb) in + E.join e1 e2 + | AST_while (cond, body) -> (* loop unrolling *) let rec unroll u = function | 0 -> u, bottom_with_vars (E.vars env) @@ -118,40 +118,40 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct let x = iter 0 env in let y = fix fsharp x in (* decreasing iteration *) E.join (condition (neg cond) y) u_u - | AST_HALT -> bottom_with_vars (E.vars env) - | AST_assert cond -> - if not - (E.is_bot (condition (neg cond) env)) - then begin - Format.printf "%s: ERROR: assertion failure@." - (Abstract_syntax_printer.string_of_extent (snd stat)); - end; - condition cond env - | AST_print items -> - Format.printf "%s: %s@." - (Abstract_syntax_printer.string_of_extent (snd stat)) - (E.var_str env (List.map fst items)); - env - | AST_local ((ty, _), vars) -> - List.fold_left - (fun env ((id, _), init) -> - let env2 = E.addvar env id in - match init with - | Some e -> E.assign env2 id e - | None -> env2) - env - vars - | _ -> 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 - Format.printf "Output: %s@." - (E.var_str result (E.vars result)) + | AST_HALT -> bottom_with_vars (E.vars env) + | AST_assert cond -> + if not + (E.is_bot (condition (neg cond) env)) + then begin + Format.printf "%s: ERROR: assertion failure@." + (Abstract_syntax_printer.string_of_extent (snd stat)); + end; + condition cond env + | AST_print items -> + Format.printf "%s: %s@." + (Abstract_syntax_printer.string_of_extent (snd stat)) + (E.var_str env (List.map fst items)); + env + | AST_local ((ty, _), vars) -> + List.fold_left + (fun env ((id, _), init) -> + let env2 = E.addvar env id in + match init with + | Some e -> E.assign env2 id e + | None -> env2) + env + vars + | _ -> 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 + Format.printf "Output: %s@." + (E.var_str result (E.vars result)) end -- cgit v1.2.3