From 8286c7c23a47c166aa87337a3146cdf3b278b144 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Thu, 19 Jun 2014 10:51:59 +0200 Subject: Isolate numerical part of domain. Next: isolate numerical part of equations. --- abstract/abs_domain.ml | 88 ++++++++++++++++++++++++++++++++++++++++++ abstract/abs_interp.ml | 6 +-- abstract/apron_domain.ml | 25 +++--------- abstract/domain.ml | 3 ++ abstract/environment_domain.ml | 41 -------------------- abstract/formula.ml | 20 ++++++---- abstract/nonrelational.ml | 21 +++------- abstract/num_domain.ml | 41 ++++++++++++++++++++ 8 files changed, 159 insertions(+), 86 deletions(-) create mode 100644 abstract/abs_domain.ml create mode 100644 abstract/domain.ml delete mode 100644 abstract/environment_domain.ml create mode 100644 abstract/num_domain.ml (limited to 'abstract') diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml new file mode 100644 index 0000000..ddc34ab --- /dev/null +++ b/abstract/abs_domain.ml @@ -0,0 +1,88 @@ +open Ast +open Formula +open Num_domain +open Typing + +module type ENVIRONMENT_DOMAIN = sig + type t + type itv + + (* construction *) + val init : t + val bottom : t + val vbottom : t -> t (* bottom value with same environment *) + val is_bot : t -> bool + + (* variable management *) + val addvar : t -> id -> Typing.typ -> t + val rmvar : t -> id -> t + val vars : t -> (id * Typing.typ) list + + val forgetvar : t -> id -> t + val var_itv : t -> id -> itv + + (* set_theoretic operations *) + val join : t -> t -> t (* union *) + val meet : t -> t -> t (* intersection *) + val widen : t -> t -> t + + val subset : t -> t -> bool + val eq : t -> t -> bool + + (* abstract operations *) + 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 + val print_itv : Format.formatter -> itv -> unit + +end + +module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct + + type t = ND.t + type itv = ND.itv + + let init = ND.init + let bottom = ND.bottom + let vbottom = ND.vbottom + let is_bot = ND.is_bot + + let addvar x id ty = ND.addvar x id (ty = TReal) + let rmvar = ND.rmvar + let vars x = List.map (fun (id, r) -> id, if r then TReal else TInt) (ND.vars x) + + let forgetvar = ND.forgetvar + let var_itv = ND.var_itv + + let join = ND.join + let meet = ND.meet + let widen = ND.widen + + let subset = ND.subset + let eq = ND.eq + + let rec apply_cl x (cons, rest) = match rest with + | CLTrue -> + ND.apply_ncl x cons + | CLFalse -> vbottom x + | CLAnd(a, b) -> + let y = apply_cl x (cons, a) in + apply_cl y (cons, b) + | CLOr((ca, ra), (cb, rb)) -> + let y = apply_cl x (cons@ca, ra) in + let z = apply_cl x (cons@cb, rb) in + join y z + + let apply_f x f = apply_cl x (conslist_of_f f) + + let assign = ND.assign + + let print_vars = ND.print_vars + let print_all = ND.print_all + let print_itv = ND.print_itv + +end diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index c621734..1d3e20a 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -4,7 +4,8 @@ open Formula open Typing open Util -open Environment_domain +open Abs_domain +open Num_domain module I (E : ENVIRONMENT_DOMAIN) : sig @@ -36,8 +37,7 @@ end = struct let cl_g = Formula.conslist_of_f f_g in let env = List.fold_left - (fun env (_, id, ty) -> - E.addvar env id (ty = TReal)) + (fun env (_, id, ty) -> E.addvar env id ty) E.init rp.all_vars in diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index cef6b66..369f4b7 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -2,11 +2,11 @@ open Formula open Ast open Util -open Environment_domain +open Num_domain open Apron -module D : ENVIRONMENT_DOMAIN = struct +module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct (* manager *) type man = Polka.loose Polka.t @@ -93,27 +93,14 @@ module D : ENVIRONMENT_DOMAIN = struct Abstract1.bound_variable manager x (Var.of_string id) (* Apply some formula to the environment *) - let rec apply_cl x (cons, rest) = + let rec apply_ncl 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; - 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) - + Abstract1.meet_tcons_array manager x ar + + let assign x eqs = let env = Abstract1.env x in let vars = Array.of_list diff --git a/abstract/domain.ml b/abstract/domain.ml new file mode 100644 index 0000000..76635d1 --- /dev/null +++ b/abstract/domain.ml @@ -0,0 +1,3 @@ +open Ast +open Formula + diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml deleted file mode 100644 index 6e84c75..0000000 --- a/abstract/environment_domain.ml +++ /dev/null @@ -1,41 +0,0 @@ -open Ast -open Formula - -module type ENVIRONMENT_DOMAIN = sig - type t - type itv - - (* 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 forgetvar : t -> id -> t (* remove var from constraints *) - 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 *) - val meet : t -> t -> t (* intersection *) - val widen : t -> t -> t - - (* order *) - 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 - val print_itv : Format.formatter -> itv -> unit -end - - diff --git a/abstract/formula.ml b/abstract/formula.ml index f3c1df1..a598750 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -2,6 +2,9 @@ open Ast (* AST for logical formulas *) + +(* Numerical part *) + type num_expr = (* constants *) | NIntConst of int @@ -12,6 +15,13 @@ type num_expr = (* identifier *) | NIdent of id +type num_cons_op = + | CONS_EQ | CONS_NE + | CONS_GT | CONS_GE +type num_cons = num_expr * num_cons_op (* always imply right member = 0 *) + + +(* Logical part *) type bool_expr = (* constants *) @@ -24,7 +34,6 @@ type bool_expr = | BOr of bool_expr * bool_expr | BNot of bool_expr - let f_and a b = match a, b with | BConst false, _ | _, BConst false -> BConst false | BConst true, b -> b @@ -67,17 +76,14 @@ and eliminate_not_negate = function | BOr(a, b) -> BAnd(eliminate_not_negate a, eliminate_not_negate b) + + (* In big ANDs, try to separate levels of /\ and levels of \/ We also use this step to simplify trues and falses that may be present. *) -type cons_op = - | CONS_EQ | CONS_NE - | CONS_GT | CONS_GE -type cons = num_expr * cons_op (* always imply right member = 0 *) - -type conslist = cons list * conslist_bool_expr +type conslist = num_cons list * conslist_bool_expr and conslist_bool_expr = | CLTrue | CLFalse diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 855f970..492b547 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -3,13 +3,13 @@ open Util open Ast open Value_domain -open Environment_domain +open Num_domain let debug = false (* Restricted domain, only support integers *) -module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct +module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct type env = V.t VarMap.t type t = Env of env | Bot @@ -167,20 +167,9 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct List.fold_left restrict_var env (extract_var (expr, zop, NIntConst 0)) - let rec apply_cl x (cons, rest) = match rest with - | CLTrue -> - let apply_cl_l x = List.fold_left apply_cons x cons in - fix eq apply_cl_l x - | CLFalse -> vbottom x - | CLAnd(a, b) -> - let y = apply_cl x (cons, a) in - apply_cl y (cons, b) - | CLOr((ca, ra), (cb, rb)) -> - let y = apply_cl x (cons@ca, ra) in - let z = apply_cl x (cons@cb, rb) in - join y z - - let apply_f x f = apply_cl x (conslist_of_f f) + let apply_ncl x cl = + let f x = List.fold_left apply_cons x cl in + fix eq f x (* Assignment *) let assign x exprs = diff --git a/abstract/num_domain.ml b/abstract/num_domain.ml new file mode 100644 index 0000000..59ed1a0 --- /dev/null +++ b/abstract/num_domain.ml @@ -0,0 +1,41 @@ +open Ast +open Formula + +module type NUMERICAL_ENVIRONMENT_DOMAIN = sig + type t + type itv + + (* construction *) + val init : t + val bottom : t + val vbottom : t -> t (* bottom value with same environment *) + val is_bot : t -> bool + + (* variable management *) + val addvar : t -> id -> bool -> t (* integer or real variable ? *) + val rmvar : t -> id -> t + val vars : t -> (id * bool) list + + val forgetvar : t -> id -> t (* remove var from constraints *) + val var_itv : t -> id -> itv + + (* 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 + + (* abstract operation *) + val apply_ncl : t -> num_cons list -> 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 + val print_itv : Format.formatter -> itv -> unit +end + + -- cgit v1.2.3