summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/_constant_domain.ml153
-rw-r--r--abstract/_domain.ml14
-rw-r--r--abstract/interpret.ml28
-rw-r--r--abstract/nonrelational.ml2
4 files changed, 15 insertions, 182 deletions
diff --git a/abstract/_constant_domain.ml b/abstract/_constant_domain.ml
deleted file mode 100644
index 544d2e9..0000000
--- a/abstract/_constant_domain.ml
+++ /dev/null
@@ -1,153 +0,0 @@
-open Util
-open Abstract_syntax_tree
-
-module CD : Domain.S =
- struct
-
- exception DivideByZero
- exception TypeError
- exception Bot
- exception NotImplemented
-
- type tv = (* type for a variable *)
- | Top
- | I of Z.t
-
- type ts = (* type for an environment *)
- | Bot
- | Nb of tv VarMap.t
-
- let top_ts = Nb VarMap.empty
-
- let ts_union a b =
- begin match a, b with
- | Bot, Bot -> Bot
- | Nb a, Bot -> Nb a
- | Bot, Nb b -> Nb b
- | Nb a, Nb b ->
- Nb
- (VarMap.fold
- (fun var value a ->
- try match VarMap.find var a with
- | Top -> a
- | I x ->
- match value with
- | I y when y = x -> a
- | _ -> VarMap.add var Top a
- with
- | Not_found -> VarMap.add var value a)
- b a)
- end
-
- (* must not raise exception *)
- let ts_add_bool_constraint expr (s : ts) =
- s (* TODO, not necessary... *)
-
-
- (* only evaluates numerical statements, raises
- TypeError when result is bool *)
- let rec eval_abs expr (s : tv VarMap.t) =
- match expr with
- | AST_unary(op, (i, _)) ->
- begin match eval_abs i s with
- | Top -> Top
- | I x ->
- match op with
- | AST_UNARY_PLUS -> I x
- | AST_UNARY_MINUS -> I (Z.neg x)
- | _ -> raise TypeError
- end
- | AST_binary(op, (a, _), (b, _)) ->
- begin match eval_abs a s, eval_abs b s with
- | I x, I y ->
- begin match op with
- | AST_PLUS -> I (Z.add x y)
- | AST_MINUS -> I (Z.sub x y)
- | AST_MULTIPLY -> I (Z.mul x y)
- | AST_DIVIDE ->
- if y = Z.zero then raise DivideByZero;
- I (Z.div x y)
- | AST_MODULO ->
- if y = Z.zero then raise DivideByZero;
- I (Z.rem x y)
- | _ -> raise TypeError
- end
- | _ -> Top
- end
- | AST_identifier(id, _) ->
- begin
- try VarMap.find id s
- with _ -> Top
- end
- | AST_int_const(s, _) ->
- I (Z.of_string s)
- | AST_bool_const(_) -> raise TypeError
- | AST_int_rand _ -> Top
- | _ -> raise NotImplemented (* extensions *)
-
- (* returns true if the expression can evaluate to true
- returns false if the expression always evaluates to false *)
- let rec eval_bool_abs expr (s : tv VarMap.t) =
- true (* TODO *)
-
- (* must not raise exception *)
- let rec interp_abs stat s =
- begin match s with
- | Bot -> Bot
- | Nb vars ->
- begin match stat with
- | AST_block b ->
- List.fold_left
- (fun ss (st, _) -> interp_abs st ss)
- s b
- | AST_assign ((id, _), (exp, _)) ->
- begin
- try
- let value = eval_abs exp vars in
- Nb (VarMap.add id value vars)
- with _ -> Bot
- end
- | AST_if ((cond, _), (tb, _), None) ->
- ts_union (Nb vars)
- (interp_abs tb
- (ts_add_bool_constraint cond (Nb vars)))
- | AST_if ((cond, l), (tb, _), Some (eb, _)) ->
- ts_union
- (interp_abs tb
- (ts_add_bool_constraint cond (Nb vars)))
- (interp_abs eb
- (ts_add_bool_constraint
- (AST_unary (AST_NOT, (cond, l)))
- (Nb vars)))
- | AST_while ((cond, _), (body, _)) ->
- let f s =
- ts_union
- s
- (ts_add_bool_constraint cond s)
- in
- fix f (Nb vars)
- | AST_HALT -> Bot
- | AST_assert (cond, _) ->
- if eval_bool_abs cond vars
- then Nb vars
- else begin
- print_string "Assert fail\n";
- Bot
- end
- | AST_print items ->
- List.iter
- (fun (var, _) ->
- print_string (var ^ " = ");
- try
- match VarMap.find var vars with
- | Top -> print_string "T\n"
- | I x -> print_string (Z.to_string x ^ "\n")
- with _ -> print_string "T\n")
- items;
- Nb vars
- | _ -> raise NotImplemented (* extensions *)
- end
- end
-
- end
-
diff --git a/abstract/_domain.ml b/abstract/_domain.ml
deleted file mode 100644
index 643a6ec..0000000
--- a/abstract/_domain.ml
+++ /dev/null
@@ -1,14 +0,0 @@
-open Abstract_syntax_tree
-
-module type S =
- sig
- type tv
- type ts
-
- val top_ts : ts
-
- val interp_abs : stat -> ts -> ts
-
- end
-
-
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index c599a76..2f9f378 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -4,18 +4,18 @@ open Util
module Make (E : ENVIRONMENT_DOMAIN) = struct
- let neg (e, l) =
- (AST_unary(AST_NOT, (e, l))), l
+ let neg e =
+ (AST_unary(AST_NOT, e)), snd e
- 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 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 =
- List.fold_left E.addvar E.bottom
+ let bottom_with_vars vlist =
+ List.fold_left E.addvar E.bottom vlist
let rec condition cond env =
begin match fst cond with
@@ -29,7 +29,7 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
E.join (condition e1 env) (condition e2 env)
(* transformations : remove not *)
- | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) ->
+ | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), _)) ->
condition cond env
| AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
condition
@@ -38,7 +38,7 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
condition
(AST_binary(AST_AND, neg e1, neg e2), x) env
- | AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) ->
+ | AST_unary (AST_NOT, (AST_binary(op, e1, e2), _)) ->
let op2 = match op with
| AST_LESS_EQUAL -> AST_GREATER
| AST_LESS -> AST_GREATER_EQUAL
@@ -88,8 +88,8 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
(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
+ 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 *)
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 39095b0..aa34d14 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -82,7 +82,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
| _ ->
let v1, v2 = eval env e1, eval env e2 in
let v1', v2' = f v1 v2 in
- if V.bottom = v1' ||V.bottom = v2'
+ if V.bottom = v1' || V.bottom = v2'
then Bot
else Env env)
x
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-24 02:18:33 +0000