diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp.ml | 132 |
1 files changed, 67 insertions, 65 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 10bd33f..cb5ae9c 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -7,11 +7,10 @@ open Cmdline open Util open Num_domain open Enum_domain -open Enum_domain_edd -module I (ED : ENUM_ENVIRONMENT_DOMAIN2) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig +module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig type st @@ -57,22 +56,21 @@ end = struct dd_add_case : dd_v -> case_v -> unit *) let dd_add_case env (enum, num) = - 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 + 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 (* dd_singleton : id list -> case_v -> dd_v @@ -103,12 +101,14 @@ end = struct vv (* - dd_apply_ecl : dd_v -> enum_cons list -> dd_v + dd_apply_econs : dd_v -> enum_cons -> dd_v *) - let dd_apply_ecl v cons = + let dd_apply_econs v cons = let vv = dd_bot v.d_vars in Hashtbl.iter (fun case (enum, num) -> - dd_add_case vv (ED.apply_cl enum cons, num)) + List.iter + (fun enum -> dd_add_case vv (enum, num)) + (ED.apply_cons enum cons)) 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 Not_found -> ()) + with _ -> ()) a.data; vv @@ -143,8 +143,10 @@ end = struct let rec apply_cl env (ec, nc, r) = match r with | CLTrue -> - let env_ec = dd_apply_ecl env ec in + let env_ec = List.fold_left dd_apply_econs 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) -> @@ -192,34 +194,33 @@ end = struct add_case : st -> case_v -> unit *) let add_case st (enum, num) = - 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); + 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 - | 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 + 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 (* @@ -228,8 +229,10 @@ end = struct let rec apply_cl_get_all_cases (enum, num) (ec, nc, r) = match r with | CLTrue -> - let enum = ED.apply_cl enum ec in - let enums = if ED.is_bot enum then [] else [enum] in + let enums = List.fold_left + (fun enums ec -> List.flatten + (List.map (fun e -> ED.apply_cons e ec) enums)) + [enum] ec in let num = ND.apply_cl num nc in List.map (fun ec -> ec, num) enums | CLFalse -> [] @@ -254,12 +257,13 @@ end = struct let enum = ED.assign enum assign_e in let num = ND.assign num assign_n in - 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 + 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 dd_pass_cycle st (v : dd_v) = let vv = dd_bot st.acc_d_vars in @@ -359,14 +363,12 @@ end = struct set_target_case : st -> dd_v -> case -> dd_v *) let set_target_case st env 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 + 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 (* do_prog : rooted_prog -> unit |