diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/apron_domain.ml | 143 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 11 |
2 files changed, 147 insertions, 7 deletions
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index a929c0b..58cd544 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -11,7 +11,9 @@ open Apron Mostly direct translation between the two. *) -module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct +(* Polyhedra *) + +module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct (* manager *) type man = Polka.loose Polka.t @@ -127,9 +129,142 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct (* Pretty-printing *) let print fmt x = - Abstract1.minimize manager x; - Abstract1.print fmt x; - Format.fprintf fmt "@?" + if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x; + Format.fprintf fmt "%a@?" Abstract1.print x + + let print_vars fmt x idl = + let prevars = vars x in + let rm_vars_l = List.filter (fun (id, _) -> not (List.mem id idl)) prevars in + let rm_vars = Array.of_list + (List.map (fun (id, _) -> Var.of_string id) rm_vars_l) in + let xx = Abstract1.forget_array manager x rm_vars false in + print fmt xx + + let print_itv = Interval.print + +end + + +(* Octagons *) + +module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct + + (* manager *) + type man = Oct.t + let manager = Oct.manager_alloc() + + type itv = Interval.t + + (* abstract elements *) + type t = man Abstract1.t + + (* direct translation of numerical expressions into Apron tree expressions *) + let rec texpr_of_nexpr = function + | NIdent id -> Texpr1.Var (Var.of_string id) + | NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i)) + | NRealConst r -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_float r)) + | NUnary(AST_UPLUS, e, is_real) -> + Texpr1.Unop( + Texpr1.Cast, + texpr_of_nexpr e, + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) + | NUnary(AST_UMINUS, e, is_real) -> + (* APRON bug ? Unary negate seems to not work correctly... *) + Texpr1.Binop( + Texpr1.Sub, + Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")), + (texpr_of_nexpr e), + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) + | NBinary(op, e1, e2, is_real) -> + let f = match op with + | AST_PLUS -> Texpr1.Add + | AST_MINUS -> Texpr1.Sub + | AST_MUL -> Texpr1.Mul + | AST_DIV -> Texpr1.Div + | AST_MOD -> Texpr1.Mod + in + Texpr1.Binop( + f, + (texpr_of_nexpr e1), + (texpr_of_nexpr e2), + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) + + (* direct translation of constraints into Apron constraints *) + let tcons_of_cons env (eq, op) = + let op = match op with + | CONS_EQ -> Tcons1.EQ + | CONS_NE -> Tcons1.DISEQ + | CONS_GT -> Tcons1.SUP + | CONS_GE -> Tcons1.SUPEQ + in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op + + (* implementation *) + let v_env vars = + let intv = List.map + (fun (s, _) -> Var.of_string s) + (List.filter (fun (_, n) -> not n) vars) in + let realv = List.map + (fun (s, _) -> Var.of_string s) + (List.filter (fun (_, n) -> n) vars) in + (Environment.make (Array.of_list intv) (Array.of_list realv)) + + let top vars = + Abstract1.top manager (v_env vars) + let bottom vars = Abstract1.bottom manager (v_env vars) + let is_bot = Abstract1.is_bottom manager + let is_top = Abstract1.is_top manager + + let forgetvar x id = + let v = [| Var.of_string id |] in + Abstract1.forget_array manager x v false + + let vars x = + let (ivt, fvt) = Environment.vars (Abstract1.env x) in + let ivl = List.map Var.to_string (Array.to_list ivt) in + let fvl = List.map Var.to_string (Array.to_list fvt) in + (List.map (fun x -> x, false) ivl) @ (List.map (fun x -> x, true) fvl) + + let vbottom x = + Abstract1.bottom manager (Abstract1.env x) + + let project x id = + Abstract1.bound_variable manager x (Var.of_string id) + + (* Apply some formula to the environment *) + let apply_cl x cons = + let env = Abstract1.env x in + let tca = Array.of_list (List.map (tcons_of_cons env) cons) in + let ar = Tcons1.array_make env (Array.length tca) in + Array.iteri (Tcons1.array_set ar) tca; + Abstract1.meet_tcons_array manager x ar + + let apply_cons x cons = apply_cl x [cons] + + + let assign x eqs = + let env = Abstract1.env x in + let vars = Array.of_list + (List.map (fun (id, _) -> Var.of_string id) eqs) in + let vals = Array.of_list + (List.map (fun (_, v) -> Texpr1.of_expr env (texpr_of_nexpr v)) eqs) in + Abstract1.assign_texpr_array manager x vars vals None + + + (* Ensemblistic operations *) + let join = Abstract1.join manager + let meet = Abstract1.meet manager + let widen = Abstract1.widening manager + + let subset = Abstract1.is_leq manager + let eq = Abstract1.is_eq manager + + (* Pretty-printing *) + let print fmt x = + if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x; + Format.fprintf fmt "%a@?" Abstract1.print x let print_vars fmt x idl = let prevars = vars x in diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index ed029da..dbc17c9 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -33,9 +33,14 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | 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, _) -> + | NUnary (AST_UPLUS, e, isreal) -> + if isreal then not_implemented "real type for nonrelationnal domain"; + eval env e + | NUnary (AST_UMINUS, e, isreal) -> + if isreal then not_implemented "real type for nonrelationnal domain"; + V.neg (eval env e) + | NBinary (op, e1, e2, isreal) -> + if isreal then not_implemented "real type for nonrelationnal domain"; let f = match op with | AST_PLUS -> V.add | AST_MINUS -> V.sub |