diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/constant_domain.ml | 128 | ||||
| -rw-r--r-- | abstract/environment_domain.ml | 42 | ||||
| -rw-r--r-- | abstract/interpret.ml | 228 | ||||
| -rw-r--r-- | abstract/intervals_domain.ml | 230 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 226 | ||||
| -rw-r--r-- | abstract/value_domain.ml | 46 |
6 files changed, 450 insertions, 450 deletions
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml index 44a13fc..abc3aa0 100644 --- a/abstract/constant_domain.ml +++ b/abstract/constant_domain.ml @@ -1,71 +1,71 @@ open Value_domain module Constants : VALUE_DOMAIN = struct - type t = - | Top - | Int of Z.t - | Bot - - let top = Top - let bottom = Bot - let const i = Int i - let rand i j = if i > j then Bot else if i <> j then Top else Int i + type t = + | Top + | Int of Z.t + | Bot + + let top = Top + let bottom = Bot + let const i = 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 - | Bot, _ -> true - | Int a, Int b -> a = b - | _, _ -> false - - let join a b = match a, b with - | Bot, x | x, Bot -> x - | Int a, Int b when a = b -> Int a - | _ -> Top - - let meet a b = match a, b with - | Top, x | x, Top -> x - | Int a, Int b when a = b -> Int a - | _ -> Bot - - let widen = join (* pas besoin d'accélerer la convergence au-delà *) + let subset a b = match a, b with + | _, Top -> true + | Bot, _ -> true + | Int a, Int b -> a = b + | _, _ -> false + + let join a b = match a, b with + | Bot, x | x, Bot -> x + | Int a, Int b when a = b -> Int a + | _ -> Top + + let meet a b = match a, b with + | Top, x | x, Top -> x + | Int a, Int b when a = b -> Int a + | _ -> Bot + + let widen = join (* pas besoin d'accélerer la convergence au-delà *) - let neg = function - | Int a -> Int (Z.neg a) - | x -> x - - let b_aux op a b = match a, b with - | Int x, Int y -> Int (op x y) - | Bot, _ | _, Bot -> Bot - | _ -> Top - let add = b_aux Z.add - let sub = b_aux Z.sub - 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 neg = function + | Int a -> Int (Z.neg a) + | x -> x + + let b_aux op a b = match a, b with + | Int x, Int y -> Int (op x y) + | Bot, _ | _, Bot -> Bot + | _ -> Top + let add = b_aux Z.add + let sub = b_aux Z.sub + 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 -> - if Z.leq a b - then Int a, Int b - else Bot, Bot - | x, y -> x, y - - let to_string = function - | Bot -> "bot" - | Top -> "top" - | Int i -> "{" ^ (Z.to_string i) ^ "}" + let leq a b = + match a, b with + | Int a, Int b -> + if Z.leq a b + then Int a, Int b + else Bot, Bot + | x, y -> x, y + + let to_string = function + | Bot -> "bot" + | Top -> "top" + | Int i -> "{" ^ (Z.to_string i) ^ "}" end diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml index 5c00fbd..404548c 100644 --- a/abstract/environment_domain.ml +++ b/abstract/environment_domain.ml @@ -1,33 +1,33 @@ open Abstract_syntax_tree module type ENVIRONMENT_DOMAIN = sig - type t + type t - (* construction *) - val init : t - val bottom : t - val is_bot : t -> bool + (* construction *) + val init : t + val bottom : t + val is_bot : t -> bool - (* variable management *) - val addvar : t -> id -> t - val rmvar : t -> id -> t - val vars : t -> id list + (* 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] *) - val compare_leq : t -> expr ext -> expr ext -> t (* S[expr <= expr ?] *) - val compare_eq : t -> expr ext -> expr ext -> t (* S[expr = expr ?] *) + (* abstract operation *) + val assign : t -> id -> expr ext -> t (* S[id <- expr] *) + val compare_leq : t -> expr ext -> expr ext -> t (* S[expr <= expr ?] *) + val compare_eq : t -> expr ext -> expr ext -> t (* S[expr = expr ?] *) - (* set-theoretic operations *) - val join : t -> t -> t (* union *) - val meet : t -> t -> t (* intersection *) - val widen : t -> t -> t + (* set-theoretic operations *) + val join : t -> t -> t (* union *) + val meet : t -> t -> t (* intersection *) + val widen : t -> t -> t - (* order *) - val subset : t -> t -> bool + (* order *) + val subset : t -> t -> bool - (* pretty-printing *) - val var_str : t -> id list -> string + (* pretty-printing *) + val var_str : t -> id list -> string end 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 diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index 98f4daf..b63f8a9 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -1,122 +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 = + 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) ^ "]" + 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 8ac6a2a..39095b0 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -6,130 +6,130 @@ open Environment_domain module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct - type env = V.t VarMap.t + type env = V.t VarMap.t - type t = Env of env | Bot + type t = Env of env | Bot - let init = Env VarMap.empty - let bottom = Bot + let init = Env VarMap.empty + let bottom = Bot - let get_var env id = - try VarMap.find id env - with Not_found -> V.top - - (* utilities *) + let get_var env id = + try VarMap.find id env + with Not_found -> V.top + + (* utilities *) - let rec eval env expr = - begin match fst expr with - | AST_identifier (id, _) -> get_var env id - | AST_int_const (s, _) -> V.const (Z.of_string s) - | AST_int_rand ((s, _), (t, _)) -> V.rand (Z.of_string s) (Z.of_string t) - | AST_unary (AST_UNARY_PLUS, e) -> eval env e - | AST_unary (AST_UNARY_MINUS, e) -> V.neg (eval env e) - | AST_unary (_, e) -> V.bottom - | AST_binary (op, e1, e2) -> - let f = match op with - | AST_PLUS -> V.add - | AST_MINUS -> V.sub - | AST_MULTIPLY -> V.mul - | AST_DIVIDE -> V.div - | AST_MODULO -> V.rem - | _ -> fun _ _ -> V.bottom - in f (eval env e1) (eval env e2) - | _ -> assert false (* unimplemented extension *) - end + let rec eval env expr = + begin match fst expr with + | AST_identifier (id, _) -> get_var env id + | AST_int_const (s, _) -> V.const (Z.of_string s) + | AST_int_rand ((s, _), (t, _)) -> V.rand (Z.of_string s) (Z.of_string t) + | AST_unary (AST_UNARY_PLUS, e) -> eval env e + | AST_unary (AST_UNARY_MINUS, e) -> V.neg (eval env e) + | AST_unary (_, e) -> V.bottom + | AST_binary (op, e1, e2) -> + let f = match op with + | AST_PLUS -> V.add + | AST_MINUS -> V.sub + | AST_MULTIPLY -> V.mul + | AST_DIVIDE -> V.div + | AST_MODULO -> V.rem + | _ -> fun _ _ -> V.bottom + in f (eval env e1) (eval env e2) + | _ -> assert false (* unimplemented extension *) + end - let strict env = (* env -> t *) - if VarMap.exists (fun _ x -> x = V.bottom) env - then Bot - else Env env - let strict_apply f = function (* (env -> t) -> t -> t *) - | Bot -> Bot - | Env e -> match f e with - | Bot -> Bot - | Env e -> strict e + let strict env = (* env -> t *) + if VarMap.exists (fun _ x -> x = V.bottom) env + then Bot + else Env env + let strict_apply f = function (* (env -> t) -> t -> t *) + | Bot -> Bot + | Env e -> match f e with + | Bot -> Bot + | Env e -> strict e - (* implementation *) + (* implementation *) - let is_bot env = match env with - | Bot -> true - | Env env -> strict env = Bot + let is_bot env = match env with + | Bot -> true + | Env env -> strict env = Bot - let addvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x - let rmvar x id = strict_apply (fun y -> Env (VarMap.remove id y)) x + let addvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x + let rmvar x id = strict_apply (fun y -> Env (VarMap.remove id y)) x - let assign x id expr = strict_apply - (fun env -> Env (VarMap.add id (eval env expr) env)) - x - let compare f x e1 e2 = - strict_apply (fun env -> match fst e1, fst e2 with - | AST_identifier(a, _), AST_identifier(b, _) -> - let v1, v2 = get_var env a, get_var env b in - let v1', v2' = f v1 v2 in - 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' = f 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' = f 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' = f v1 v2 in - if V.bottom = v1' ||V.bottom = v2' - then Bot - else Env env) - x + let assign x id expr = strict_apply + (fun env -> Env (VarMap.add id (eval env expr) env)) + x + let compare f x e1 e2 = + strict_apply (fun env -> match fst e1, fst e2 with + | AST_identifier(a, _), AST_identifier(b, _) -> + let v1, v2 = get_var env a, get_var env b in + let v1', v2' = f v1 v2 in + 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' = f 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' = f 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' = f v1 v2 in + if V.bottom = v1' ||V.bottom = v2' + then Bot + else Env env) + x let compare_leq = compare V.leq let compare_eq = compare (fun x y -> let r = V.meet x y in r, r) - let join a b = match a, b with - | Bot, x | x, Bot -> x - | Env m, Env n -> - strict (VarMap.map2z (fun _ a b -> V.join a b) m n) - - let meet a b = match a, b with - | Bot, _ | _, Bot -> Bot - | Env m, Env n -> - strict (VarMap.map2z (fun _ a b -> V.meet a b) m n) + let join a b = match a, b with + | Bot, x | x, Bot -> x + | Env m, Env n -> + strict (VarMap.map2z (fun _ a b -> V.join a b) m n) + + let meet a b = match a, b with + | Bot, _ | _, Bot -> Bot + | Env m, Env n -> + strict (VarMap.map2z (fun _ a b -> V.meet a b) m n) - let widen a b = match a, b with - | Bot, x | x, Bot -> x - | Env m, Env n -> - strict (VarMap.map2z (fun _ a b -> V.widen a b) m n) - - let subset a b = match a, b with - | Bot, x -> true - | Env _, Bot -> false - | Env m, Env n -> - VarMap.for_all2o - (fun _ _ -> true) - (fun _ _ -> true) - (fun _ a b -> V.subset a b) - m n - - (* pretty-printing *) - let var_str env vars = - match env with - | Bot -> "bottom" - | Env env -> - let v = List.fold_left - (fun s id -> - (if s = "" then s else s ^ ", ") ^ - id ^ " in " ^ (V.to_string (get_var env id)) - ) - "" - vars - in - "[ " ^ v ^ " ]" - - let vars env = match env with - | Bot -> [] - | Env env -> List.map fst (VarMap.bindings env) + let widen a b = match a, b with + | Bot, x | x, Bot -> x + | Env m, Env n -> + strict (VarMap.map2z (fun _ a b -> V.widen a b) m n) + + let subset a b = match a, b with + | Bot, x -> true + | Env _, Bot -> false + | Env m, Env n -> + VarMap.for_all2o + (fun _ _ -> true) + (fun _ _ -> true) + (fun _ a b -> V.subset a b) + m n + + (* pretty-printing *) + let var_str env vars = + match env with + | Bot -> "bottom" + | Env env -> + let v = List.fold_left + (fun s id -> + (if s = "" then s else s ^ ", ") ^ + id ^ " in " ^ (V.to_string (get_var env id)) + ) + "" + vars + in + "[ " ^ v ^ " ]" + + let vars env = match env with + | Bot -> [] + | Env env -> List.map fst (VarMap.bindings env) end diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml index 9cf6d76..da4f481 100644 --- a/abstract/value_domain.ml +++ b/abstract/value_domain.ml @@ -1,31 +1,31 @@ module type VALUE_DOMAIN = sig - type t + type t - (* constructors *) - val top : t - val bottom : t - val const : Z.t -> t - val rand : Z.t -> Z.t -> t + (* constructors *) + val top : t + val bottom : t + val const : Z.t -> t + val rand : Z.t -> Z.t -> t - (* order *) - val subset : t -> t -> bool + (* order *) + val subset : t -> t -> bool - (* set-theoretic operations *) - val join : t -> t -> t (* union *) - val meet : t -> t -> t (* intersection *) - val widen : t -> t -> t + (* set-theoretic operations *) + val join : t -> t -> t (* union *) + val meet : t -> t -> t (* intersection *) + val widen : t -> t -> t - (* arithmetic operations *) - val neg : t -> t - val add : t -> t -> t - val sub : t -> t -> t - val mul : t -> t -> t - val div : t -> t -> t - val rem : t -> t -> t + (* arithmetic operations *) + val neg : t -> t + val add : t -> t -> t + val sub : t -> t -> t + val mul : t -> t -> t + val div : t -> t -> t + val rem : t -> t -> t - (* boolean test *) - val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *) + (* boolean test *) + val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *) - (* pretty-printing *) - val to_string : t -> string + (* pretty-printing *) + val to_string : t -> string end |