From 9ccef2c0850b73bf3d92f26bfa0aeacf933e1d17 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 7 May 2014 17:41:06 +0200 Subject: Restart anew ; done nonrelational stuff, interpret remains, intervals domain remains --- abstract/_constant_domain.ml | 153 ++++++++++++++++++++++++++++++ abstract/_domain.ml | 14 +++ abstract/constant_domain.ml | 206 +++++++++++------------------------------ abstract/domain.ml | 14 --- abstract/environment_domain.ml | 27 ++++++ abstract/interpret.ml | 57 ++++++++++++ abstract/nonrelational.ml | 103 +++++++++++++++++++++ abstract/value_domain.ml | 28 ++++++ 8 files changed, 435 insertions(+), 167 deletions(-) create mode 100644 abstract/_constant_domain.ml create mode 100644 abstract/_domain.ml delete mode 100644 abstract/domain.ml create mode 100644 abstract/environment_domain.ml create mode 100644 abstract/interpret.ml create mode 100644 abstract/nonrelational.ml create mode 100644 abstract/value_domain.ml (limited to 'abstract') diff --git a/abstract/_constant_domain.ml b/abstract/_constant_domain.ml new file mode 100644 index 0000000..544d2e9 --- /dev/null +++ b/abstract/_constant_domain.ml @@ -0,0 +1,153 @@ +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 new file mode 100644 index 0000000..643a6ec --- /dev/null +++ b/abstract/_domain.ml @@ -0,0 +1,14 @@ +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/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 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/environment_domain.ml b/abstract/environment_domain.ml new file mode 100644 index 0000000..f5614fe --- /dev/null +++ b/abstract/environment_domain.ml @@ -0,0 +1,27 @@ +open Abstract_syntax_tree + +module type ENVIRONMENT_DOMAIN = sig + type t + + (* construction *) + val init : t + val bottom : t + + (* variable management *) + val addvar : t -> id -> t + val rmvar : t -> id -> t + + (* abstract operation *) + val assign : t -> id -> expr ext -> t (* S[id <- expr] *) + val compare : 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 + + (* order *) + val subset : t -> t -> bool +end + + diff --git a/abstract/interpret.ml b/abstract/interpret.ml new file mode 100644 index 0000000..51c7cd6 --- /dev/null +++ b/abstract/interpret.ml @@ -0,0 +1,57 @@ +open Abstract_syntax_tree +open Environment_domain +open Util + +module Make (E : ENVIRONMENT_DOMAIN) = struct + + let neg (e, l) = + (AST_unary(AST_NOT, (e, 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) + | _ -> env (* TODO : encode some transformations *) + end + + let rec interp_stmt env stat = + begin match fst stat with + | AST_block b -> + List.fold_left interp_stmt env b + | 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) -> + E.join + (interp_stmt (condition cond env) tb) + (interp_stmt (condition (neg cond) env) eb) + | AST_while (cond, (body, _)) -> + (* TODO *) + env + | AST_HALT -> E.bottom + | AST_assert (cond, l) -> + (* TODO *) + env + | AST_print items -> + (* TODO *) + env + | _ -> assert false (* not implemented *) + end + + let interpret prog = + List.fold_left + (fun env x -> match x with + | AST_stat st -> interp_stmt env st + | _ -> env) + E.init + (fst prog) +end diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml new file mode 100644 index 0000000..6e2ff2b --- /dev/null +++ b/abstract/nonrelational.ml @@ -0,0 +1,103 @@ +open Abstract_syntax_tree +open Util + +open Value_domain +open Environment_domain + + +module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct + type env = V.t VarMap.t + + type t = Env of env | 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 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 + + (* implementation *) + + 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 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' = 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) + x + + 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 + +end diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml new file mode 100644 index 0000000..a0f082f --- /dev/null +++ b/abstract/value_domain.ml @@ -0,0 +1,28 @@ +module type VALUE_DOMAIN = sig + type 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 + + (* 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 + + (* boolean test *) + val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *) +end -- cgit v1.2.3