diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp.ml | 14 | ||||
| -rw-r--r-- | abstract/apron_domain.ml | 132 | ||||
| -rw-r--r-- | abstract/environment_domain.ml | 36 | ||||
| -rw-r--r-- | abstract/transform.ml | 4 |
4 files changed, 183 insertions, 3 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml new file mode 100644 index 0000000..403e3e8 --- /dev/null +++ b/abstract/abs_interp.ml @@ -0,0 +1,14 @@ +open Ast +open Formula + +open Util +open Environment_domain + +module I (E : ENVIRONMENT_DOMAIN) : sig + + val init_state : prog -> id -> E.t + val do_step : prog -> id -> E.t -> E.t + +end = struct + +end diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml new file mode 100644 index 0000000..1cc418e --- /dev/null +++ b/abstract/apron_domain.ml @@ -0,0 +1,132 @@ +open Formula +open Ast + +open Util +open Environment_domain + +open Apron + +module D : ENVIRONMENT_DOMAIN = struct + + (* manager *) + type man = Polka.loose Polka.t + let manager = Polka.manager_alloc_loose () + + (* abstract elements *) + type t = man Abstract1.t + + (* direct translation of numerical expressions into Apron tree expressions *) + (* TODO : some variables have type real and not int... *) + 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) -> + texpr_of_nexpr e + | NUnary(AST_UMINUS, e) -> + (* 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), + Texpr1.Int, + Texpr1.Zero) + | NBinary(op, e1, e2) -> + 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), + Texpr1.Int, + Texpr1.Zero) + + (* 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 init = Abstract1.top manager (Environment.make [||] [||]) + let bottom = Abstract1.bottom manager (Environment.make [||] [||]) + let is_bot = Abstract1.is_bottom manager + + let addvar x id isfloat = + let env = Abstract1.env x in + let env2 = if isfloat then + Environment.add env [||] [| Var.of_string id |] + else + Environment.add env [| Var.of_string id |] [||] + in + Abstract1.change_environment manager x env2 false + let rmvar x id = + let v = [| Var.of_string id |] in + let env = Abstract1.env x in + let env2 = Environment.remove env v in + let y = Abstract1.forget_array manager x v false in + Abstract1.change_environment manager y env2 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) + + (* Apply some formula to the environment *) + let rec apply_cl x (cons, rest) = + 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; + let y = Abstract1.meet_tcons_array manager x ar in + apply_cl_r y rest + + 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) -> + let y = apply_cl x a in + let z = apply_cl x b in + Abstract1.join manager y z + + let apply_f x f = apply_cl x (conslist_of_f f) + + + (* 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_all fmt x = + Abstract1.print fmt x; + Format.fprintf fmt "@?" + + 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_all fmt xx + +end + diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml new file mode 100644 index 0000000..5664474 --- /dev/null +++ b/abstract/environment_domain.ml @@ -0,0 +1,36 @@ +open Ast +open Formula + +module type ENVIRONMENT_DOMAIN = sig + type t + + (* construction *) + val init : t + val bottom : t + val is_bot : t -> bool + + (* variable management *) + val addvar : t -> id -> bool -> t (* integer or float variable ? *) + val rmvar : t -> id -> t + 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 + + (* 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 + val eq : t -> t -> bool + + (* pretty-printing *) + val print_vars : Format.formatter -> t -> id list -> unit + val print_all : Format.formatter -> t -> unit +end + + diff --git a/abstract/transform.ml b/abstract/transform.ml index 56d54ce..e6886b8 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -191,10 +191,8 @@ and f_of_scope active td (node, prefix, eqs) = (List.map do_eq eqs) and f_of_prog p root = - let (n, _) = find_node_decl p root in - let root_scope = ("", "", n.body) in let td = { - root_scope = root_scope; + root_scope = get_root_scope p root; p = p; consts = I.consts p root; } in |