diff options
| -rw-r--r-- | abstract/abs_interp.ml | 132 | ||||
| -rw-r--r-- | abstract/enum_domain_edd.ml | 48 | ||||
| -rw-r--r-- | main.ml | 6 |
3 files changed, 113 insertions, 73 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index cb5ae9c..10bd33f 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -7,10 +7,11 @@ open Cmdline open Util open Num_domain open Enum_domain +open Enum_domain_edd -module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig +module I (ED : ENUM_ENVIRONMENT_DOMAIN2) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig type st @@ -56,21 +57,22 @@ end = struct dd_add_case : dd_v -> case_v -> unit *) let dd_add_case env (enum, num) = - let rec aux enum vals = function - | [] -> - let case = List.rev vals in - begin try let e0, n0 = Hashtbl.find env.data case in - Hashtbl.replace env.data case (ED.join enum e0, ND.join num n0); - with Not_found -> - Hashtbl.add env.data case (enum, num); - end - | p::q -> - List.iter - (fun v -> match ED.apply_cons enum (E_EQ, p, EItem v) with - | [en] -> aux en (v::vals) q - | _ -> assert false) - (ED.project enum p) - in aux enum [] env.d_vars + if not (ED.is_bot enum || ND.is_bot num) then + let rec aux enum vals = function + | [] -> + let case = List.rev vals in + begin try let e0, n0 = Hashtbl.find env.data case in + Hashtbl.replace env.data case (ED.join enum e0, ND.join num n0); + with Not_found -> + Hashtbl.add env.data case (enum, num); + end + | p::q -> + List.iter + (fun v -> let en = ED.apply_cons enum (E_EQ, p, EItem v) in + assert (not (ED.is_bot en)); + aux en (v::vals) q) + (ED.project enum p) + in aux enum [] env.d_vars (* dd_singleton : id list -> case_v -> dd_v @@ -101,14 +103,12 @@ end = struct vv (* - dd_apply_econs : dd_v -> enum_cons -> dd_v + dd_apply_ecl : dd_v -> enum_cons list -> dd_v *) - let dd_apply_econs v cons = + let dd_apply_ecl v cons = let vv = dd_bot v.d_vars in Hashtbl.iter (fun case (enum, num) -> - List.iter - (fun enum -> dd_add_case vv (enum, num)) - (ED.apply_cons enum cons)) + dd_add_case vv (ED.apply_cl enum cons, num)) v.data; vv @@ -133,7 +133,7 @@ end = struct try let e2, n2 = Hashtbl.find b.data case in let en, nn = ED.meet enum e2, ND.meet n2 num in if not (ND.is_bot nn) then Hashtbl.add vv.data case (en, nn) - with _ -> ()) + with Not_found -> ()) a.data; vv @@ -143,10 +143,8 @@ end = struct let rec apply_cl env (ec, nc, r) = match r with | CLTrue -> - let env_ec = List.fold_left dd_apply_econs env ec in + let env_ec = dd_apply_ecl env ec in let env_nc = dd_apply_ncl env_ec nc in - (* Format.printf "[[ %a -> %a ]]@." - print_dd env print_dd env_nc; *) env_nc | CLFalse -> dd_bot env.d_vars | CLAnd(a, b) -> @@ -194,33 +192,34 @@ end = struct add_case : st -> case_v -> unit *) let add_case st (enum, num) = - let rec aux enum vals = function - | [] -> - let case = List.rev vals in - begin try let e0, n0 = Hashtbl.find st.env case in - if (not (ED.subset enum e0)) || (not (ND.subset num n0)) then begin - begin try - let n = Hashtbl.find st.widen case in - let jw = if n < st.opt.widen_delay then ND.join else ND.widen in - Hashtbl.replace st.env case (ED.join e0 enum, jw n0 num); - Hashtbl.replace st.widen case (n+1); - with Not_found -> - Hashtbl.replace st.env case (ED.join enum e0, ND.join num n0); - Hashtbl.add st.widen case 0; - end; + if not (ED.is_bot enum || ND.is_bot num) then + let rec aux enum vals = function + | [] -> + let case = List.rev vals in + begin try let e0, n0 = Hashtbl.find st.env case in + if (not (ED.subset enum e0)) || (not (ND.subset num n0)) then begin + begin try + let n = Hashtbl.find st.widen case in + let jw = if n < st.opt.widen_delay then ND.join else ND.widen in + Hashtbl.replace st.env case (ED.join e0 enum, jw n0 num); + Hashtbl.replace st.widen case (n+1); + with Not_found -> + Hashtbl.replace st.env case (ED.join enum e0, ND.join num n0); + Hashtbl.add st.widen case 0; + end; + if not (List.mem case st.delta) then st.delta <- case::st.delta + end + with Not_found -> + Hashtbl.add st.env case (enum, num); if not (List.mem case st.delta) then st.delta <- case::st.delta end - with Not_found -> - Hashtbl.add st.env case (enum, num); - if not (List.mem case st.delta) then st.delta <- case::st.delta - end - | p::q -> - List.iter - (fun v -> match ED.apply_cons enum (E_EQ, p, EItem v) with - | [en] -> aux en (v::vals) q - | _ -> assert false) - (ED.project enum p) - in aux enum [] st.acc_d_vars + | p::q -> + List.iter + (fun v -> let en = ED.apply_cons enum (E_EQ, p, EItem v) in + assert (not (ED.is_bot en)); + aux en (v::vals) q) + (ED.project enum p) + in aux enum [] st.acc_d_vars (* @@ -229,10 +228,8 @@ end = struct let rec apply_cl_get_all_cases (enum, num) (ec, nc, r) = match r with | CLTrue -> - let enums = List.fold_left - (fun enums ec -> List.flatten - (List.map (fun e -> ED.apply_cons e ec) enums)) - [enum] ec in + let enum = ED.apply_cl enum ec in + let enums = if ED.is_bot enum then [] else [enum] in let num = ND.apply_cl num nc in List.map (fun ec -> ec, num) enums | CLFalse -> [] @@ -257,13 +254,12 @@ end = struct let enum = ED.assign enum assign_e in let num = ND.assign num assign_n in - List.fold_left - (fun (enum, num) (var, t) -> - let e, n = match t with - | TEnum _ -> ED.forgetvar enum var, num - | TReal | TInt -> enum, ND.forgetvar num var - in e, n) - (enum, num) st.forget + let ef, nf = List.fold_left + (fun (ef, nf) (var, t) -> match t with + | TEnum _ -> var::ef, nf + | TReal | TInt -> ef, var::nf) + ([], []) st.forget in + ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf let dd_pass_cycle st (v : dd_v) = let vv = dd_bot st.acc_d_vars in @@ -363,12 +359,14 @@ end = struct set_target_case : st -> dd_v -> case -> dd_v *) let set_target_case st env case = - List.fold_left2 - (fun env id v -> - if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then - dd_apply_econs env (E_EQ, id, EItem v) - else env) - env st.acc_d_vars case + let cl = + List.fold_left2 + (fun cl id v -> + if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then + (E_EQ, id, EItem v)::cl + else cl) + [] st.acc_d_vars case + in dd_apply_ecl env cl (* do_prog : rooted_prog -> unit diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml index 60f2d3b..a372772 100644 --- a/abstract/enum_domain_edd.ml +++ b/abstract/enum_domain_edd.ml @@ -1,9 +1,41 @@ open Ast open Formula open Util -open Enum_domain -module EDD : ENUM_ENVIRONMENT_DOMAIN = struct +module type ENUM_ENVIRONMENT_DOMAIN2 = sig + type t + + type item = string + + (* construction *) + val top : (id * item list) list -> t + val bot : (id * item list) list -> t + val is_bot : t -> bool + + (* variable management *) + val vars : t -> (id * item list) list + + val forgetvar : t -> id -> t + val forgetvars : t -> id list -> t + val project : t -> id -> item list + + (* set-theoretic operations *) + val join : t -> t -> t (* union *) + val meet : t -> t -> t (* intersection *) + + val subset : t -> t -> bool + val eq : t -> t -> bool + + (* abstract operations *) + val apply_cons : t -> enum_cons -> t + val apply_cl : t -> enum_cons list -> t + val assign : t -> (id * id) list -> t + + (* pretty-printing *) + val print : Format.formatter -> t -> unit +end + +module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct exception Top type item = string @@ -132,11 +164,19 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN = struct (* top : (id * item list) list -> t + bot : (id * item list) list -> t *) let top vars = let order = Hashtbl.create 12 in List.iteri (fun i (id, _) -> Hashtbl.add order id i) vars; { vars; order; root = DTop } + let bot vars = let t = top vars in { t with root = DBot } + + (* + is_bot : t -> bool + *) + let is_bot x = (x.root = DBot) + (* vars : t -> (id * item list) list *) @@ -243,8 +283,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN = struct apply_cl : t -> enum_cons list -> t *) let apply_cons v x = - let v = meet v (of_cons v x) in - if v.root = DBot then [] else [v] + meet v (of_cons v x) + let apply_cl v ec = let rec cl_k = function | [] -> { v with root = DTop } @@ -6,12 +6,14 @@ open Num_domain open Nonrelational open Apron_domain +open Enum_domain_edd + module Interpret = Interpret.I module ItvND = Nonrelational.ND(Intervals_domain.VD) -module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND) -module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND) +module AI_Itv = Abs_interp.I(Enum_domain_edd.EDD)(ItvND) +module AI_Rel = Abs_interp.I(Enum_domain_edd.EDD)(Apron_domain.ND) module AI_Itv_EDD = Abs_interp_edd.I(ItvND) module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND) |