From a30fa47b4272f8c79948b741f7c388dad53c8eea Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 28 May 2014 16:45:46 +0200 Subject: RETAB, CLEANUP --- TODO | 6 -- abstract/_constant_domain.ml | 153 ------------------------------------------- abstract/_domain.ml | 14 ---- abstract/interpret.ml | 28 ++++---- abstract/nonrelational.ml | 2 +- 5 files changed, 15 insertions(+), 188 deletions(-) delete mode 100644 TODO delete mode 100644 abstract/_constant_domain.ml delete mode 100644 abstract/_domain.ml diff --git a/TODO b/TODO deleted file mode 100644 index 7b30877..0000000 --- a/TODO +++ /dev/null @@ -1,6 +0,0 @@ -1. Définir un type pour décrire les valeurs abstraites - ie. définir le domaine abstrait - - Constantes + bot + top : bool et int - - Intervalles + bot + top : int - -2. Interprète abstrait 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 -- cgit v1.2.3