open Abstract_syntax_tree
open Environment_domain
open Util
module Make (E : ENVIRONMENT_DOMAIN) = struct
let neg e =
(AST_unary(AST_NOT, e)), snd e
let binop op e e2 =
(AST_binary (op, e, e2)), snd e
let m1 e =
binop AST_MINUS e (AST_int_const("1", snd e), snd e)
let p1 e =
binop AST_PLUS e (AST_int_const("1", snd e), snd e)
let bottom_with_vars vlist =
List.fold_left E.addvar E.bottom vlist
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_bool_const true -> env
| AST_bool_const false -> E.bottom
(* transformations : remove not *)
| AST_unary(AST_NOT, (AST_bool_const x, _)) ->
condition (AST_bool_const (not x), snd cond) env
| AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), _)) ->
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), _)) ->
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
let rec interp_stmt_a show_asserts env stat =
let interp_stmt = interp_stmt_a show_asserts in
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)
| n ->
let prev_u, u_prev_u = unroll u (n-1) in
interp_stmt (condition cond prev_u) body,
E.join u_prev_u (condition (neg cond) prev_u)
in
let env, u_u = unroll env 3 in
(* widening *)
let widen_delay = 3 in
let fsharp a i =
let next_step = interp_stmt_a a (condition cond i) body in
E.join env next_step
in
let rec iter n i =
let i' =
if n < widen_delay
then E.join i (fsharp show_asserts i)
else E.widen i (fsharp false i)
in
if E.eq i i' then i else iter (n+1) i'
in
let x = iter 0 env in
let y = fix E.eq (fsharp false) x in (* decreasing iteration *)
let z =
if show_asserts then
(* last iteration : show real assert failures *)
fsharp true y
else y in
E.join (condition (neg cond) z) u_u
| AST_HALT -> bottom_with_vars (E.vars env)
| AST_assert cond ->
if show_asserts &&
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 interp_stmt = interp_stmt_a true
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
