From 93d924bb1017dc26a9735801e1b7f8b7a3f4ef2c Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 30 Jul 2014 15:45:28 +0200 Subject: Refactor some stuff (this code sould be re-read.) --- abstract/abs_interp_edd.ml | 72 +++++++++++++++++++++++++--------------------- 1 file changed, 40 insertions(+), 32 deletions(-) (limited to 'abstract/abs_interp_edd.ml') diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index cdf3c7e..074987f 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -5,7 +5,7 @@ open Typing open Cmdline open Util -open Num_domain +open Abs_domain open Varenv @@ -14,7 +14,7 @@ exception Top exception Found_int of int -module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig +module I (D0 : ENVIRONMENT_DOMAIN) : sig val do_prog : cmdline_opt -> rooted_prog -> unit @@ -56,7 +56,7 @@ end = struct type edd_v = { ve : varenv; root : edd; - leaves : (int, ND.t) Hashtbl.t; + leaves : (int, D0.t) Hashtbl.t; } (* @@ -120,10 +120,10 @@ end = struct let leaves = Hashtbl.create 12 in let lc = ref 0 in let get_leaf st x = - if ND.is_top x then DTop else - if ND.is_bot x then DBot else + if D0.is_top x then DTop else + if D0.is_bot x then DBot else try - Hashtbl.iter (fun i v -> if ND.eq v x then raise (Found_int i)) leaves; + Hashtbl.iter (fun i v -> if D0.eq v x then raise (Found_int i)) leaves; incr lc; Hashtbl.add leaves !lc x; DVal (!lc, st) @@ -205,7 +205,7 @@ end = struct for id = 0 to !max_v do try let v = Hashtbl.find v.leaves id in - Format.fprintf fmt "v%d: %a@." id ND.print v + Format.fprintf fmt "v%d: %a@." id D0.print v with Not_found -> () done @@ -324,7 +324,7 @@ end = struct dq vb kl | DVal (u, _), DVal (v, _) -> - let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + let x = D0.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in get_leaf x | DVal(u, _), DBot -> get_leaf (Hashtbl.find a.leaves u) @@ -365,7 +365,7 @@ end = struct dq vb kl | DVal (u, _) , DVal (v, _) -> - let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + let x = D0.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in get_leaf x | DVal(u, _), DTop -> get_leaf (Hashtbl.find a.leaves u) @@ -380,10 +380,10 @@ end = struct (* - edd_num_apply : edd_v -> (ND.t -> ND.t) -> edd_v + edd_leaf_apply : edd_v -> (D0.t -> D0.t) -> edd_v edd_apply_ncl : edd_v -> num_cons list -> edd_v *) - let edd_num_apply v nfun = + let edd_leaf_apply v nfun = let ve = v.ve in let leaves, get_leaf = get_leaf_fun () in @@ -393,7 +393,7 @@ end = struct let f f_rec n = match n with | DBot -> DBot - | DTop -> get_leaf (nfun (ND.top ve.nvars)) + | DTop -> get_leaf (nfun (D0.top ve)) | DVal (i, _) -> get_leaf (nfun (Hashtbl.find v.leaves i)) | DChoice(n, var, l) -> let l = List.map (fun (k, v) -> k, f_rec v) l in @@ -402,7 +402,7 @@ end = struct { leaves; ve; root = memo f v.root } let edd_apply_ncl v ncl = - edd_num_apply v (fun n -> ND.apply_cl n ncl) + edd_leaf_apply v (fun n -> D0.apply_ncl n ncl) (* edd_apply_ecl : edd_v -> enum_cons list -> edd_v @@ -418,13 +418,15 @@ end = struct in let cons_edd = cl_k ec in edd_meet v cons_edd - (*List.fold_left (fun v c -> edd_meet v (edd_of_cons v.ve c)) v ec*) (* edd_apply_cl : edd_v -> conslist -> edd_v *) let rec edd_apply_cl v (ec, nc, r) = - let v = edd_apply_ecl v ec in + let v = edd_leaf_apply + (edd_apply_ecl v ec) + (fun k -> D0.apply_ecl k ec) + in match r with | CLTrue -> edd_apply_ncl v nc @@ -465,7 +467,7 @@ end = struct | DBot, DBot -> true | DTop, DTop -> true | DVal (i, _), DVal (j, _) -> - ND.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j) + D0.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j) | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb) la lb @@ -484,11 +486,11 @@ end = struct | _, DTop -> true | DTop, DBot -> false - | DVal(i, _), DBot -> ND.is_bot (Hashtbl.find a.leaves i) - | DTop, DVal(i, _) -> ND.is_top (Hashtbl.find b.leaves i) + | DVal(i, _), DBot -> D0.is_bot (Hashtbl.find a.leaves i) + | DTop, DVal(i, _) -> D0.is_top (Hashtbl.find b.leaves i) | DVal(i, _), DVal(j, _) -> - ND.subset (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j) + D0.subset (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j) | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb) @@ -530,8 +532,10 @@ end = struct if cn = [] then if fn = [] then DBot else - let x = list_fold_op ND.join - (List.map (Hashtbl.find v.leaves) fn) + let x = list_fold_op D0.join + (List.map + (fun i -> D0.forgetvars (Hashtbl.find v.leaves i) vars) + fn) in get_leaf x else let _, dv, cl = List.hd cn in @@ -665,7 +669,7 @@ end = struct let widen = if edd_eq p1 p2 then true else false in - let x = (if widen then ND.widen else ND.join) + let x = (if widen then D0.widen else D0.join) (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in get_leaf x @@ -711,7 +715,7 @@ end = struct let p1, p2 = edd_extract_path a u, edd_extract_path b v in let d1, d2 = Hashtbl.find a.leaves u, Hashtbl.find b.leaves v in let widen = edd_eq p1 p2 && i1 >= env.opt.widen_delay in - let x = (if widen then ND.widen else ND.join) d1 d2 in + let x = (if widen then D0.widen else D0.join) d1 d2 in get_leaf (s1, i1 + 1) x | DChoice(_,va, la), _ when rank ve na < rank ve nb -> @@ -754,7 +758,7 @@ end = struct ([], []) env.cycle in let v = edd_eassign v assign_e in - let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in + let v = edd_leaf_apply v (fun nv -> D0.nassign nv assign_n) in let ef, nf = List.fold_left (fun (ef, nf) (var, t) -> match t with @@ -763,7 +767,7 @@ end = struct ([], []) env.forget in let v = edd_forget_vars v ef in - edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf) + edd_leaf_apply v (fun nv -> D0.forgetvars nv nf) let unpass_cycle env v = let assign_e, assign_n = List.fold_left @@ -773,7 +777,7 @@ end = struct ([], []) env.ve.cycle in let v = edd_eassign v assign_e in - let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in + let v = edd_leaf_apply v (fun nv -> D0.nassign nv assign_n) in let ef, nf = List.fold_left (fun (ef, nf) (var, t) -> match t with @@ -782,7 +786,7 @@ end = struct ([], []) env.ve.forget_inv in let v = edd_forget_vars v ef in - edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf) + edd_leaf_apply v (fun nv -> D0.forgetvars nv nf) @@ -988,8 +992,8 @@ end = struct | TEnum _ -> id::l) [] e.ve.all_vars) in let final_flat = match final_flat.root with - | DTop -> ND.top e.ve.nvars - | DBot -> ND.bottom e.ve.nvars + | DTop -> D0.top e.ve + | DBot -> D0.bottom e.ve | DVal(i, _) -> Hashtbl.find final_flat.leaves i | DChoice _ -> assert false in @@ -999,9 +1003,13 @@ end = struct if p then match ty with | TInt | TReal -> Format.printf "%a ∊ %a@ " Formula_printer.print_id id - ND.print_itv (ND.project final_flat id) - | TEnum _ -> Format.printf "%a : enum variable@ " - Formula_printer.print_id id) + D0.print_itv (D0.nproject final_flat id) + | TEnum _ -> + (* not precise : does not take into account info from decision graph *) + Format.printf "%a ∊ @[[%a]@]@ " + Formula_printer.print_id id + (print_list Format.pp_print_string ", ") + (D0.eproject final_flat id)) e.ve.all_vars; Format.printf "@]@." end -- cgit v1.2.3