diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | abstract/abs_interp.ml | 26 | ||||
| -rw-r--r-- | abstract/environment_domain.ml | 10 | ||||
| -rw-r--r-- | abstract/formula_printer.ml | 9 | ||||
| -rw-r--r-- | abstract/intervals_domain.ml | 158 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 217 | ||||
| -rw-r--r-- | abstract/value_domain.ml | 31 | ||||
| -rw-r--r-- | main.ml | 3 |
8 files changed, 438 insertions, 18 deletions
@@ -14,6 +14,8 @@ SRC= main.ml \ abstract/environment_domain.ml \ abstract/apron_domain.ml \ abstract/abs_interp.ml \ + abstract/nonrelational.ml \ + abstract/intervals_domain.ml \ interpret/interpret.ml \ interpret/ast_util.ml \ interpret/rename.ml diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 1838591..0a330c2 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -88,7 +88,7 @@ end = struct let env = E.apply_f env init_f in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; - Format.printf "Cycle formula: %a@.@." Formula_printer.print_conslist cl; + Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f; { p; root_scope; f; cl; all_vars; env } @@ -116,24 +116,32 @@ end = struct not (List.exists (fun (_, id2, _) -> id2 = "N"^id) vars)) vars) in let e = List.fold_left E.forgetvar e forget_vars in - Format.printf "Pass cycle: %a@.@." E.print_all e; e + (* cycle : st -> env -> env *) + let cycle st i = + let i' = E.apply_cl i st.cl in + i', pass_cycle st.all_vars i' + (* do_prog : prog -> id -> st *) let do_prog p root = let st = init_state p root in - let rec step acc i n = - Format.printf "Step %d: %a@." n E.print_all acc; + let _, acc = cycle st st.env in + + let rec step acc n = if n < 10 then begin - let i' = E.apply_cl (E.join i acc) st.cl in - let j = pass_cycle st.all_vars i' in - let acc' = (if n > 6 then E.widen else E.join) acc j in - step acc' i (n+1) + Format.printf "Step %d: %a@." n E.print_all acc; + let i', j = cycle st acc in + Format.printf " -> %a@." E.print_all i'; + Format.printf "Pass cycle: %a@.@." E.print_all j; + + let acc' = (if n >= 7 then E.widen else E.join) acc j in + step acc' (n+1) end in - step (E.vbottom st.env) st.env 0 + step acc 0 end diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml index 5dbd08f..8b2ee34 100644 --- a/abstract/environment_domain.ml +++ b/abstract/environment_domain.ml @@ -16,11 +16,6 @@ module type ENVIRONMENT_DOMAIN = sig val vars : t -> (id * bool) list val vbottom : t -> t (* bottom value with same environment *) - (* abstract operation *) - val apply_f : t -> bool_expr -> t - val apply_cl : t -> conslist -> t - val assign : t -> (id * num_expr) list -> t - (* set-theoretic operations *) val join : t -> t -> t (* union *) val meet : t -> t -> t (* intersection *) @@ -30,6 +25,11 @@ module type ENVIRONMENT_DOMAIN = sig val subset : t -> t -> bool val eq : t -> t -> bool + (* abstract operation *) + val apply_f : t -> bool_expr -> t + val apply_cl : t -> conslist -> t + val assign : t -> (id * num_expr) list -> t + (* pretty-printing *) val print_vars : Format.formatter -> t -> id list -> unit val print_all : Format.formatter -> t -> unit diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml index 994c82a..25b7b22 100644 --- a/abstract/formula_printer.ml +++ b/abstract/formula_printer.ml @@ -91,15 +91,18 @@ let print_expr fmt e = (* Print constraint list form of formula *) -let print_cons fmt (eq, sg) = +let print_cons_sg fmt sg = let sg_str = match sg with | CONS_EQ -> "=" | CONS_NE -> "≠" | CONS_GT -> ">" | CONS_GE -> "≥" in - Format.fprintf fmt "@[<hv 2>%a %s 0@]" - print_num_expr eq sg_str + Format.fprintf fmt "%s" sg_str + +let print_cons fmt (eq, sg) = + Format.fprintf fmt "@[<hv 2>%a %a 0@]" + print_num_expr eq print_cons_sg sg let rec print_conslist fmt (cons, e) = let rec aux = function diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml new file mode 100644 index 0000000..848f634 --- /dev/null +++ b/abstract/intervals_domain.ml @@ -0,0 +1,158 @@ +open Value_domain + +module VD : VALUE_DOMAIN = struct + type bound = Int of int | 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 -> 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 (a + b) + | _ -> assert false + let bound_mul a b = + match a, b with + | PInf, Int(x) | Int(x), PInf -> + if x > 0 then PInf + else if x < 0 then MInf + else Int 0 + | MInf, Int(x) | Int(x), MInf -> + if x < 0 then PInf + else if x > 0 then MInf + else Int 0 + | Int(x), Int(y) -> Int(x * y) + | MInf, PInf | PInf, MInf -> MInf + | MInf, MInf | PInf, PInf -> PInf + let bound_div a b = + match a, b with + | _, PInf | _, MInf -> Int 0 + | PInf, Int i -> + if i < 0 then MInf + else PInf + | MInf, Int i -> + if i < 0 then PInf + else MInf + | Int i, Int j -> + assert (j != 0); + Int (i / j) + + + 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 (- i) + + let bound_abs a = bound_max a (bound_neg a) + + (* implementation *) + let top = Itv(MInf, PInf) + let bottom = Bot + let const i = Itv(Int i, Int i) + let rand i j = + if 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 + (if bound_leq (Int 0) c then Int 0 else MInf) + else a), + (if not (bound_leq d b) then + (if bound_leq d (Int 0) then Int 0 else 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 = match a, b with + | Bot, _ -> Bot + | Itv(a, b), q -> + let p1 = match meet q (Itv(Int 1, PInf)) with + | Bot -> Bot + | Itv(c, d) -> + Itv(min (bound_div a c) (bound_div a d), max (bound_div b c) (bound_div b d)) + in + let p2 = match meet q (Itv(MInf, Int (-1))) with + | Bot -> Bot + | Itv(c, d) -> + Itv(min (bound_div b c) (bound_div b d), max (bound_div a c) (bound_div a d)) + in + join p1 p2 + let rem a b = match a, b with + | Bot, _ | _, Bot -> Bot + | Itv(a, b), Itv(c, d) -> + Itv( + Int 0, + bound_max (bound_abs c) (bound_abs d) + ) + + 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 -> string_of_int 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 new file mode 100644 index 0000000..f5c9a04 --- /dev/null +++ b/abstract/nonrelational.ml @@ -0,0 +1,217 @@ +open Formula +open Util +open Ast + +open Value_domain +open Environment_domain + +let debug = false + +(* Restricted domain, only support integers *) + +module D (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 = function + | NIdent id -> get_var env id + | NIntConst i -> V.const i + | NRealConst f -> V.const (int_of_float f) (* TODO floats *) + | NUnary (AST_UPLUS, e) -> eval env e + | NUnary (AST_UMINUS, e) -> V.neg (eval env e) + | NBinary (op, e1, e2) -> + let f = match op with + | AST_PLUS -> V.add + | AST_MINUS -> V.sub + | AST_MUL -> V.mul + | AST_DIV -> V.div + | AST_MOD -> V.rem + in f (eval env e1) (eval env e2) + + 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 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 forgetvar 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 vars env = match env with + | Bot -> [] + | Env env -> List.map (fun (k, _) -> (k, false)) (VarMap.bindings env) + let vbottom _ = bottom + + (* Set-theoretic operations *) + 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) + + (* Inclusion and equality *) + let subset a b = match a, b with + | Bot, x -> true + | Env _, Bot -> false + | Env m, Env n -> + VarMap.for_all2o + (fun _ _ -> true) + (fun _ v -> v = V.top) + (fun _ a b -> V.subset a b) + m n + + let eq a b = match a, b with + | Bot, Bot -> true + | Env m, Env n -> + VarMap.for_all2o + (fun _ _ -> false) + (fun _ _ -> false) + (fun _ a b -> a = b) + m n + | _ -> false + + (* Apply some formula to the environment *) + let apply_cons env (expr, sign) = + let inv_op = function + | AST_LT -> AST_GT + | AST_GT -> AST_LT + | AST_LE -> AST_GE + | AST_GE -> AST_LE + | x -> x + in + let rec extract_var (lhs, op, rhs) = + match lhs with + | NIdent i -> [i, op, rhs] + | NIntConst _ | NRealConst _ -> [] + | NUnary(AST_UPLUS, x) -> extract_var (x, op, rhs) + | NUnary(AST_UMINUS, x) -> + extract_var (x, inv_op op, NUnary(AST_UMINUS, x)) + | NBinary(AST_PLUS, a, b) -> + extract_var (a, op, NBinary(AST_MINUS, rhs, b)) @ + extract_var (b, op, NBinary(AST_MINUS, rhs, a)) + | NBinary(AST_MINUS, a, b) -> + extract_var (a, op, NBinary(AST_PLUS, rhs, b)) @ + extract_var (b, inv_op op, NBinary(AST_MINUS, a, rhs)) + | NBinary(AST_MUL, a, b) -> + extract_var (a, op, NBinary(AST_DIV, rhs, b)) @ + extract_var (b, op, NBinary(AST_DIV, rhs, a)) + | NBinary(AST_DIV, a, b) -> + extract_var (a, op, NBinary(AST_MUL, rhs, b)) @ + extract_var (b, inv_op op, NBinary(AST_DIV, a, rhs)) + | NBinary(AST_MOD, _, _) -> [] + in + let zop = match sign with + | CONS_EQ -> AST_EQ | CONS_NE -> AST_NE + | CONS_GT -> AST_GT | CONS_GE -> AST_GE + in + let restrict_var env (i, op, expr) = + strict_apply (fun env -> + let v1, v2 = get_var env i, eval env expr in + let v1' = match op with + | AST_EQ -> V.meet v1 v2 + | AST_NE -> v1 + | AST_LE -> let u, _ = V.leq v1 v2 in u + | AST_GE -> let _, v = V.leq v2 v1 in v + | AST_LT -> let u, _ = V.leq v1 (V.sub v2 (V.const 1)) in u + | AST_GT -> let _, v = V.leq (V.add v2 (V.const 1)) v1 in v + in + if debug then Format.printf + "restrict %s %s @[<hv>%a@] : %s %s -> %s@." i + (Formula_printer.string_of_binary_rel op) + Formula_printer.print_num_expr expr + (V.to_string v1) (V.to_string v2) (V.to_string v1'); + Env (VarMap.add i v1' env)) + env + in + List.fold_left restrict_var env + (extract_var (expr, zop, NIntConst 0)) + + let rec apply_cl x (cons, rest) = + let apply_cl_l x = List.fold_left apply_cons x cons in + + let y = fix eq apply_cl_l x in + if debug then Format.printf "-[@."; + let z = apply_cl_r y rest in + if debug then Format.printf "-]@."; + fix eq apply_cl_l z + + and apply_cl_r x = function + | CLTrue -> x + | CLFalse -> vbottom x + | CLAnd(a, b) -> + let y = apply_cl_r x a in + apply_cl_r y b + | CLOr(a, b) -> + if debug then Format.printf "<<@."; + let y = apply_cl x a in + if debug then Format.printf "\\/@."; + let z = apply_cl x b in + if debug then Format.printf ">>@."; + join y z + + let apply_f x f = apply_cl x (conslist_of_f f) + + (* Assignment *) + let assign x exprs = + let aux env = + let vars = List.map (fun (id, v) -> (id, eval env v)) exprs in + let env2 = + List.fold_left (fun e (id, v) -> VarMap.add id v e) + env vars + in Env env2 + in + strict_apply aux x + + + (* pretty-printing *) + let print_vars fmt env ids = + match env with + | Bot -> Format.fprintf fmt "bottom" + | Env env -> + Format.fprintf fmt "@[<hov 2>["; + let _ = List.fold_left + (fun nf id -> + let v = get_var env id in + if v <> V.top then begin + if nf then Format.fprintf fmt ",@ "; + Format.fprintf fmt "%s in %s" id (V.to_string (get_var env id)); + true + end else nf) + false + ids + in Format.fprintf fmt "]@]" + + let print_all fmt x = + print_vars fmt x (List.map fst (vars x)) + +end diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml new file mode 100644 index 0000000..fb01ac6 --- /dev/null +++ b/abstract/value_domain.ml @@ -0,0 +1,31 @@ +module type VALUE_DOMAIN = sig + type t + + (* constructors *) + val top : t + val bottom : t + val const : int -> t + val rand : int -> int -> 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]) *) + + (* pretty-printing *) + val to_string : t -> string +end @@ -2,7 +2,8 @@ open Ast module Interpret = Interpret.I -module AI = Abs_interp.I(Apron_domain.D) +module IntD = Nonrelational.D(Intervals_domain.VD) +module AI = Abs_interp.I(IntD) (* command line options *) let dump = ref false |