diff options
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 132 |
1 files changed, 65 insertions, 67 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 |