summaryrefslogtreecommitdiff
path: root/abstract/interpret.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/interpret.ml')
-rw-r--r--abstract/interpret.ml228
1 files changed, 114 insertions, 114 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 13:31:52 +0000