diff options
Diffstat (limited to 'abstract/constant_domain.ml')
| -rw-r--r-- | abstract/constant_domain.ml | 206 |
1 files changed, 53 insertions, 153 deletions
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml index 544d2e9..4bd5cf2 100644 --- a/abstract/constant_domain.ml +++ b/abstract/constant_domain.ml @@ -1,153 +1,53 @@ -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 - +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 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 = meet (* 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 = b_aux Z.mul + let div = b_aux Z.div + let rem = b_aux Z.rem + + let leq a b = + match a, b with + | Int a, Int b when Z.leq a b -> + if Z.leq a b + then Int a, Int b + else Bot, Bot + | x, y -> x, y +end |