summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/constant_domain.ml25
-rw-r--r--abstract/environment_domain.ml4
-rw-r--r--abstract/interpret.ml124
-rw-r--r--abstract/intervals_domain.ml122
-rw-r--r--abstract/nonrelational.ml38
5 files changed, 267 insertions, 46 deletions
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml
index d142228..44a13fc 100644
--- a/abstract/constant_domain.ml
+++ b/abstract/constant_domain.ml
@@ -9,7 +9,7 @@ module Constants : VALUE_DOMAIN = struct
let top = Top
let bottom = Bot
let const i = Int i
- let rand i j = if i <> j then Top else Int i
+ let rand i j = if i > j then Bot else if i <> j then Top else Int i
let subset a b = match a, b with
| _, Top -> true
@@ -27,7 +27,7 @@ module Constants : VALUE_DOMAIN = struct
| Int a, Int b when a = b -> Int a
| _ -> Bot
- let widen = meet (* pas besoin d'accélerer la convergence au-delà *)
+ let widen = join (* pas besoin d'accélerer la convergence au-delà *)
let neg = function
| Int a -> Int (Z.neg a)
@@ -39,13 +39,26 @@ module Constants : VALUE_DOMAIN = struct
| _ -> Top
let add = b_aux Z.add
let sub = b_aux Z.sub
- let mul = b_aux Z.mul
- let div = b_aux Z.div
- let rem = b_aux Z.rem
+ let mul a b = match a, b with
+ | Int x, Int y -> Int (Z.mul x y)
+ | Bot, _ | _, Bot -> Bot
+ | Int x, _ when x = Z.zero -> Int Z.zero
+ | _, Int x when x = Z.zero -> Int (Z.zero)
+ | _ -> Top
+ let div a b = match a, b with
+ | Int x, Int y -> Int (Z.div x y)
+ | Bot, _ | _, Bot -> Bot
+ | Int x, _ when x = Z.zero -> Int Z.zero
+ | _ -> Top
+ let rem a b = match a, b with
+ | Int x, Int y -> Int (Z.rem x y)
+ | Bot, _ | _, Bot -> Bot
+ | Int x, _ when x = Z.zero -> Int Z.zero
+ | _ -> Top
let leq a b =
match a, b with
- | Int a, Int b when Z.leq a b ->
+ | Int a, Int b ->
if Z.leq a b
then Int a, Int b
else Bot, Bot
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index 254f755..05473aa 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -11,6 +11,7 @@ module type ENVIRONMENT_DOMAIN = sig
(* variable management *)
val addvar : t -> id -> t
val rmvar : t -> id -> t
+ val vars : t -> id list
(* abstract operation *)
val assign : t -> id -> expr ext -> t (* S[id <- expr] *)
@@ -25,8 +26,7 @@ module type ENVIRONMENT_DOMAIN = sig
val subset : t -> t -> bool
(* pretty-printing *)
- val var_str : t -> id list -> string
- val all_vars_str : t -> string
+ val var_str : t -> id list -> string
end
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index fe998a6..79d4d2c 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -7,30 +7,79 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
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 rec condition cond env =
begin match fst cond with
| AST_binary (AST_LESS_EQUAL, e1, e2) ->
E.compare env e1 e2
- | AST_binary (AST_GREATER_EQUAL, e1, e2) ->
- E.compare env e2 e1
| 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 *)
+
+ (* 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
- | _ -> env (* TODO : encode some more transformations *)
+
+ | 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_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))
+ env
+
+ | _ -> env
end
let rec interp_stmt env stat =
begin match fst stat with
| AST_block b ->
- List.fold_left interp_stmt env 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) ->
@@ -38,27 +87,57 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
(interp_stmt (condition cond env) tb)
(condition (neg cond) env)
| AST_if (cond, tb, Some eb) ->
- E.join
- (interp_stmt (condition cond env) tb)
- (interp_stmt (condition (neg cond) env) eb)
- | AST_while (cond, (body, _)) ->
- (* TODO *)
- env
+ 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 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
- | AST_assert (cond, l) ->
+ | AST_assert cond ->
if not
- (E.is_bot (condition (neg (cond, l)) env))
+ (E.is_bot (condition (neg cond) env))
then begin
- print_string (Abstract_syntax_printer.string_of_extent l);
- print_string ": ERROR: assertion failure\n"
+ Format.printf "%s: ERROR: assertion failure@."
+ (Abstract_syntax_printer.string_of_extent (snd stat));
end;
- condition (cond, l) env
+ condition cond env
| AST_print items ->
- print_string (Abstract_syntax_printer.string_of_extent (snd stat));
- print_string ": ";
- print_string (E.var_str env (List.map fst items));
- print_string "\n";
+ 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
@@ -70,7 +149,6 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
E.init
(fst prog)
in
- print_string "Output: ";
- print_string (E.all_vars_str result);
- print_string "\n"
+ Format.printf "Output: %s@."
+ (E.var_str result (E.vars result))
end
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
new file mode 100644
index 0000000..98f4daf
--- /dev/null
+++ b/abstract/intervals_domain.ml
@@ -0,0 +1,122 @@
+open Value_domain
+
+module Intervals : VALUE_DOMAIN = struct
+ type bound = Int of Z.t | PInf | MInf
+
+ type t = Itv of bound * bound | Bot
+
+ (* utilities *)
+ let bound_leq a b = (* a <= b ? *)
+ match a, b with
+ | MInf, _ | _, PInf -> true
+ | Int a, Int b -> Z.leq a b
+ | x, y -> x = y
+
+ let bound_add a b =
+ match a, b with
+ | MInf, Int a | Int a, MInf -> MInf
+ | PInf, Int a | Int a, PInf -> PInf
+ | MInf, MInf -> MInf
+ | PInf, PInf -> PInf
+ | Int a, Int b -> Int (Z.add a b)
+ | _ -> assert false
+ let bound_mul a b =
+ match a, b with
+ | PInf, Int(x) | Int(x), PInf ->
+ if x > Z.zero then PInf
+ else if x < Z.zero then MInf
+ else Int Z.zero
+ | MInf, Int(x) | Int(x), MInf ->
+ if x < Z.zero then PInf
+ else if x > Z.zero then MInf
+ else Int Z.zero
+ | Int(x), Int(y) -> Int(Z.mul x y)
+ | MInf, PInf | PInf, MInf -> MInf
+ | MInf, MInf | PInf, PInf -> PInf
+
+ let bound_min a b = match a, b with
+ | MInf, _ | _, MInf -> MInf
+ | Int a, Int b -> Int (min a b)
+ | Int a, PInf -> Int a
+ | PInf, Int a -> Int a
+ | PInf, PInf -> PInf
+ let bound_max a b = match a, b with
+ | PInf, _ | _, PInf -> PInf
+ | Int a, Int b -> Int (max a b)
+ | Int a, MInf | MInf, Int a -> Int a
+ | MInf, MInf -> MInf
+
+ let bound_neg = function
+ | PInf -> MInf
+ | MInf -> PInf
+ | Int i -> Int (Z.neg i)
+
+ (* implementation *)
+ let top = Itv(MInf, PInf)
+ let bottom = Bot
+ let const i = Itv(Int i, Int i)
+ let rand i j =
+ if Z.leq i j then Itv(Int i, Int j) else Bot
+
+ let subset a b = match a, b with
+ | Bot, _ -> true
+ | _, Bot -> false
+ | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
+
+ let join a b = match a, b with
+ | Bot, x | x, Bot -> x
+ | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)
+
+ let meet a b = match a, b with
+ | Bot, x | x, Bot -> Bot
+ | Itv(a, b), Itv(c, d) ->
+ let u, v = bound_max a c, bound_min b d in
+ if bound_leq u v
+ then Itv(u, v)
+ else Bot
+
+ let widen a b = match a, b with
+ | x, Bot | Bot, x -> x
+ | Itv(a, b), Itv(c, d) ->
+ Itv(
+ (if not (bound_leq a c) then MInf else a),
+ (if not (bound_leq d b) then PInf else b))
+
+ let neg = function
+ | Bot -> Bot
+ | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
+ let add a b = match a, b with
+ | Bot, _ | _, Bot -> Bot
+ | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
+ let sub a b = match a, b with
+ | Bot, _ | _, Bot -> Bot
+ | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
+ let mul a b = match a, b with
+ | Bot, _ | _, Bot -> Bot
+ | Itv(a, b), Itv(c, d) ->
+ Itv(
+ (bound_min (bound_min (bound_mul a c) (bound_mul a d))
+ (bound_min (bound_mul b c) (bound_mul b d))),
+ (bound_max (bound_max (bound_mul a c) (bound_mul a d))
+ (bound_max (bound_mul b c) (bound_mul b d))))
+
+
+ let div a b = top (* TODO *)
+ let rem a b = top (* TODO *)
+
+ let leq a b = match a, b with
+ | Bot, _ | _, Bot -> Bot, Bot
+ | Itv(a, b), Itv(c, d) ->
+ if not (bound_leq a d)
+ then Bot, Bot
+ else Itv(a, bound_min b d), Itv(bound_max a c, d)
+
+ let bound_str = function
+ | MInf -> "-oo"
+ | PInf -> "+oo"
+ | Int i -> Z.to_string i
+ let to_string = function
+ | Bot -> "bot"
+ | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
+
+end
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index d4118da..7221df1 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -66,16 +66,25 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
| AST_identifier(a, _), AST_identifier(b, _) ->
let v1, v2 = get_var env a, get_var env b in
let v1', v2' = V.leq v1 v2 in
- Env (VarMap.add a v1' (VarMap.add b v1' env))
- | AST_identifier(a, _), AST_int_const(s, _) ->
- let v1, v2 = get_var env a, V.const (Z.of_string s) in
- let v1', _ = V.leq v1 v2 in
- Env (VarMap.add a v1' env)
- | AST_int_const(s, _), AST_identifier(b, _) ->
- let v1, v2 = V.const (Z.of_string s), get_var env b in
- let _, v2' = V.leq v1 v2 in
- Env (VarMap.add b v2' env)
- | _ -> Env env)
+ Env (VarMap.add a v1' (VarMap.add b v2' env))
+ | AST_identifier(a, _), _ ->
+ let v1, v2 = get_var env a, eval env e2 in
+ let v1', v2' = V.leq v1 v2 in
+ if V.bottom = v2'
+ then Bot
+ else Env (VarMap.add a v1' env)
+ | _, AST_identifier(b, _) ->
+ let v1, v2 = eval env e1, get_var env b in
+ let v1', v2' = V.leq v1 v2 in
+ if V.bottom = v1'
+ then Bot
+ else Env (VarMap.add b v2' env)
+ | _ ->
+ let v1, v2 = eval env e1, eval env e2 in
+ let v1', v2' = V.leq v1 v2 in
+ if V.bottom = v1' ||V.bottom = v2'
+ then Bot
+ else Env env)
x
let join a b = match a, b with
@@ -106,7 +115,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
(* pretty-printing *)
let var_str env vars =
match env with
- | Bot -> "bot"
+ | Bot -> "bottom"
| Env env ->
let v = List.fold_left
(fun s id ->
@@ -118,8 +127,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
in
"[ " ^ v ^ " ]"
- let all_vars_str env =
- match env with
- | Bot -> "bot"
- | Env map -> var_str env (List.map fst (VarMap.bindings map))
+ let vars env = match env with
+ | Bot -> []
+ | Env env -> List.map fst (VarMap.bindings env)
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 19:34:31 +0000