summaryrefslogtreecommitdiff
path: root/abstract/abs_interp_edd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/abs_interp_edd.ml')
-rw-r--r--abstract/abs_interp_edd.ml72
1 files changed, 40 insertions, 32 deletions
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 ∊ @[<hov 2>[%a]@]@ "
+ Formula_printer.print_id id
+ (print_list Format.pp_print_string ", ")
+ (D0.eproject final_flat id))
e.ve.all_vars;
Format.printf "@]@."
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-16 19:54:03 +0000