diff options
| -rw-r--r-- | abstract/abs_interp.ml | 66 | ||||
| -rw-r--r-- | abstract/apron_domain.ml | 7 | ||||
| -rw-r--r-- | abstract/environment_domain.ml | 3 | ||||
| -rw-r--r-- | abstract/formula.ml | 18 | ||||
| -rw-r--r-- | abstract/formula_printer.ml | 7 | ||||
| -rw-r--r-- | abstract/intervals_domain.ml | 20 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 48 | ||||
| -rw-r--r-- | abstract/value_domain.ml | 44 | ||||
| -rw-r--r-- | tests/source/test4.scade | 2 |
9 files changed, 148 insertions, 67 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 0a330c2..4f66540 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -119,29 +119,61 @@ end = struct 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' + (* cycle : st -> cl -> env -> env *) + let cycle st cl i = + E.apply_cl (pass_cycle st.all_vars i) cl (* - do_prog : prog -> id -> st + loop : st -> cl -> env -> env -> env + *) + let loop st cycle_cl pnew stay = + let pnew = E.apply_cl pnew cycle_cl in + + Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@." + Formula_printer.print_conslist cycle_cl + E.print_all pnew E.print_all stay; + + let add_stay = cycle st cycle_cl pnew in + let acc0 = E.join stay add_stay in + + let fsharp i = + Format.printf "Acc @[<hv>%a@]@." E.print_all i; + let j = cycle st cycle_cl i in + E.join acc0 j + in + + let widen_delay = 2 in + let rec iter n i = + let i' = + if n < widen_delay + then E.join i (fsharp i) + else E.widen i (fsharp i) + in + if E.eq i i' then i else iter (n+1) i' + in + + let x = iter 0 acc0 in + fix E.eq fsharp x (* decreasing iteration *) + + + (* + do_prog : prog -> id -> unit *) let do_prog p root = let st = init_state p root in - let _, acc = cycle st st.env in + let pnew = st.env in - let rec step acc n = - if n < 10 then begin - 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 stay = loop st st.cl pnew (E.vbottom pnew) in - let acc' = (if n >= 7 then E.widen else E.join) acc j in - step acc' (n+1) - end - in - step acc 0 + Format.printf "@[<hov>Final stay %a@]@." + E.print_all stay; + + Format.printf "Probes:@[<hov>"; + + List.iter (fun (p, id, _) -> + if p then Format.printf "@ %a ∊ %a," + Formula_printer.print_id id + E.print_itv (E.var_itv stay id)) + st.all_vars end diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index ad483ec..d13afd7 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -12,6 +12,8 @@ module D : ENVIRONMENT_DOMAIN = struct type man = Polka.loose Polka.t let manager = Polka.manager_alloc_loose () + type itv = Interval.t + (* abstract elements *) type t = man Abstract1.t @@ -87,6 +89,9 @@ module D : ENVIRONMENT_DOMAIN = struct let vbottom x = Abstract1.bottom manager (Abstract1.env x) + let var_itv x id = + Abstract1.bound_variable manager x (Var.of_string id) + (* Apply some formula to the environment *) let rec apply_cl x (cons, rest) = let env = Abstract1.env x in @@ -139,5 +144,7 @@ module D : ENVIRONMENT_DOMAIN = struct let xx = Abstract1.forget_array manager x rm_vars false in print_all fmt xx + let print_itv = Interval.print + end diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml index 8b2ee34..6e84c75 100644 --- a/abstract/environment_domain.ml +++ b/abstract/environment_domain.ml @@ -3,6 +3,7 @@ open Formula module type ENVIRONMENT_DOMAIN = sig type t + type itv (* construction *) val init : t @@ -15,6 +16,7 @@ module type ENVIRONMENT_DOMAIN = sig val rmvar : t -> id -> t val vars : t -> (id * bool) list val vbottom : t -> t (* bottom value with same environment *) + val var_itv : t -> id -> itv (* set-theoretic operations *) val join : t -> t -> t (* union *) @@ -33,6 +35,7 @@ module type ENVIRONMENT_DOMAIN = sig (* pretty-printing *) val print_vars : Format.formatter -> t -> id list -> unit val print_all : Format.formatter -> t -> unit + val print_itv : Format.formatter -> itv -> unit end diff --git a/abstract/formula.ml b/abstract/formula.ml index 2c83b32..262bccb 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -69,13 +69,17 @@ and conslist_bool_expr = let rec conslist_of_f = function | BNot e -> conslist_of_f (eliminate_not_negate e) | BRel (op, a, b) -> - let cons = match op with - | AST_EQ -> NBinary(AST_MINUS, a, b), CONS_EQ - | AST_NE -> NBinary(AST_MINUS, a, b), CONS_NE - | AST_GT -> NBinary(AST_MINUS, a, b), CONS_GT - | AST_GE -> NBinary(AST_MINUS, a, b), CONS_GE - | AST_LT -> NBinary(AST_MINUS, b, a), CONS_GT - | AST_LE -> NBinary(AST_MINUS, b, a), CONS_GE + let x, y, op = match op with + | AST_EQ -> a, b, CONS_EQ + | AST_NE -> a, b, CONS_NE + | AST_GT -> a, b, CONS_GT + | AST_GE -> a, b, CONS_GE + | AST_LT -> b, a, CONS_GT + | AST_LE -> b, a, CONS_GE + in + let cons = if y = NIntConst 0 + then (x, op) + else (NBinary(AST_MINUS, x, y), op) in [cons], CLTrue | BConst x -> [], if x then CLTrue else CLFalse diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml index 25b7b22..53a9b6a 100644 --- a/abstract/formula_printer.ml +++ b/abstract/formula_printer.ml @@ -39,12 +39,15 @@ let print_ah fmt pf fa a fe e = then Format.fprintf fmt "@[<hv 2>(%a)@]" pf a else Format.fprintf fmt "@[<hv 2>%a@]" pf a +let print_id fmt id = + let re = Str.regexp "/" in + Format.fprintf fmt "%s" (Str.global_replace re "·" id) + let rec print_num_expr fmt e = match e with | NIntConst i -> Format.fprintf fmt "%d" i | NRealConst f -> Format.fprintf fmt "%f" f | NIdent id -> - let re = Str.regexp "/" in - Format.fprintf fmt "%s" (Str.global_replace re "·" id) + print_id fmt id | NBinary(op, a, b) -> print_ch fmt print_num_expr ne_prec a ne_prec e; Format.fprintf fmt "@ %s " (string_of_binary_op op); diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index 848f634..181266b 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -1,9 +1,7 @@ open Value_domain module VD : VALUE_DOMAIN = struct - type bound = Int of int | PInf | MInf - - type t = Itv of bound * bound | Bot + type t = itv (* utilities *) let bound_leq a b = (* a <= b ? *) @@ -64,14 +62,18 @@ module VD : VALUE_DOMAIN = struct | MInf -> PInf | Int i -> Int (- i) - let bound_abs a = bound_max a (bound_neg a) + 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 + if i <= j then Itv(Int i, Int j) else Bot + let to_itv x = x + let as_const = function + | Itv(Int i, Int j) when i = j -> Some i + | _ -> None let subset a b = match a, b with | Bot, _ -> true @@ -147,12 +149,6 @@ module VD : VALUE_DOMAIN = struct 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) ^ "]" + let to_string = string_of_itv end diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index f5c9a04..b83edc1 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -13,6 +13,7 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct type env = V.t VarMap.t type t = Env of env | Bot + type itv = Value_domain.itv let init = Env VarMap.empty let bottom = Bot @@ -63,6 +64,10 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct | Env env -> List.map (fun (k, _) -> (k, false)) (VarMap.bindings env) let vbottom _ = bottom + let var_itv x id = match x with + | Bot -> Value_domain.Bot + | Env env -> V.to_itv (get_var env id) + (* Set-theoretic operations *) let join a b = match a, b with | Bot, x | x, Bot -> x @@ -196,22 +201,39 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct (* pretty-printing *) let print_vars fmt env ids = match env with - | Bot -> Format.fprintf fmt "bottom" + | Bot -> Format.fprintf fmt "⊥" | 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 "]@]" + Format.fprintf fmt "@[<v 2>{ "; + let l = List.map (fun id -> (get_var env id, id)) ids in + let s = List.sort Pervasives.compare l in + let rec bl = function + | [] -> [] + | (v, id)::q when v <> V.top -> + begin match bl q with + | (vv, ids)::q when vv = v -> (v, id::ids)::q + | r -> (v, [id])::r + end + | _::q -> bl q + in + let sbl = bl s in + List.iteri + (fun j (v, ids) -> + if j > 0 then Format.fprintf fmt "@ "; + List.iteri + (fun i id -> + if i > 0 then Format.fprintf fmt ", "; + Format.fprintf fmt "%a" Formula_printer.print_id id) + ids; + match V.as_const v with + | Some i -> Format.fprintf fmt " = %d" i + | _ -> Format.fprintf fmt " ∊ %s" (V.to_string v)) + sbl; + Format.fprintf fmt " }@]" let print_all fmt x = print_vars fmt x (List.map fst (vars x)) + + let print_itv fmt x = + Format.fprintf fmt "%s" (string_of_itv x) end diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml index fb01ac6..7b9d557 100644 --- a/abstract/value_domain.ml +++ b/abstract/value_domain.ml @@ -1,30 +1,44 @@ + +type bound = Int of int | PInf | MInf +type itv = Itv of bound * bound | Bot + +let string_of_bound = function + | MInf -> "-oo" + | PInf -> "+oo" + | Int i -> string_of_int i +let string_of_itv = function + | Bot -> "⊥" + | Itv(a, b) -> "[" ^ (string_of_bound a) ^ ";" ^ (string_of_bound b) ^ "]" + module type VALUE_DOMAIN = sig type t (* constructors *) - val top : t - val bottom : t - val const : int -> t - val rand : int -> int -> t + val top : t + val bottom : t + val const : int -> t + val rand : int -> int -> t + val to_itv : t -> itv + val as_const : t -> int option (* order *) - val subset : t -> t -> bool + 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 + 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 + 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]) *) + 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 diff --git a/tests/source/test4.scade b/tests/source/test4.scade index c66a56f..b32a37d 100644 --- a/tests/source/test4.scade +++ b/tests/source/test4.scade @@ -1,7 +1,7 @@ node test(i: int) returns(probe a, b, c: int; exit: bool) let exit = i >= 5; - a = 0 -> (if pre a > 10 then 0 else pre a + 1); + a = 0 -> (if pre a >= 10 then 0 else pre a + 1); b = 0 -> pre i; c = 0; tel |