diff options
Diffstat (limited to 'abstract/interpret.ml')
| -rw-r--r-- | abstract/interpret.ml | 63 |
1 files changed, 33 insertions, 30 deletions
diff --git a/abstract/interpret.ml b/abstract/interpret.ml index 79d4d2c..5f03775 100644 --- a/abstract/interpret.ml +++ b/abstract/interpret.ml @@ -14,10 +14,15 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct 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 env 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) -> @@ -59,10 +64,6 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct condition (binop AST_LESS e2 e1) env - | AST_binary (AST_EQUAL, e1, e2) -> - condition - (binop AST_AND (binop AST_LESS_EQUAL e1 e2) (binop AST_LESS_EQUAL e2 e1)) - env | AST_binary (AST_NOT_EQUAL, e1, e2) -> condition (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1)) @@ -91,31 +92,33 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct let e2 = (interp_stmt (condition (neg cond) env) eb) in E.join e1 e2 | AST_while (cond, body) -> - let unroll_count = 3 in - let rec iter n i x = - (* Format.printf "(iter %d) i:%s x:%s @." n (E.var_str i (E.vars i)) - (E.var_str x (E.vars x)); *) - let out_state = condition (neg cond) i in - let next_step = interp_stmt (condition cond i) body in - (* Format.printf ". next step: %s@." (E.var_str next_step (E.vars next_step)); *) - if n < unroll_count then - E.join - out_state - (iter (n+1) next_step x) - else - let env2 = - E.widen - i - next_step - in - if env2 = i - then env2 - else E.join - out_state - (iter (n+1) env2 x) - in - condition (neg cond) (iter 0 env env) - | AST_HALT -> E.bottom + (* 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 i = + let next_step = interp_stmt (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 else E.widen) + i + (fsharp i) + in + if i = i' then i else iter (n+1) i' + in + 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)) |