summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp_edd.ml438
1 files changed, 329 insertions, 109 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index ebf7549..0dfc6f3 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -7,15 +7,12 @@ open Util
open Num_domain
open Abs_interp
-let time id f =
- Format.printf "%s[@?" id;
- let r = f () in
- Format.printf "] @?";
- r
exception Top
+exception Found_int of int
+
module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
val do_prog : cmdline_opt -> rooted_prog -> unit
@@ -43,7 +40,7 @@ end = struct
type edd =
| DBot
| DTop
- | DVal of int
+ | DVal of int * bool (* bool : new case ? *)
| DChoice of int * id * (item * edd) list
type edd_v = {
@@ -66,7 +63,7 @@ end = struct
let key = function
| DBot -> 0
| DTop -> 1
- | DVal i -> 2 * i + 2
+ | DVal (i, _) -> 2 * i + 2
| DChoice(i, _, _) -> 2 * i + 3
let memo f =
@@ -90,10 +87,43 @@ end = struct
let edd_node_eq = function
| DBot, DBot -> true
| DTop, DTop -> true
- | DVal i, DVal j when i = j -> true
+ | DVal (i, _), DVal (j, _) when i = j -> true
| DChoice(i, _, _), DChoice(j, _, _) when i = j -> true
| _ -> false
+ let new_node_fun () =
+ let nc = ref 0 in
+ let node_memo = Hashtbl.create 12 in
+ fun v l ->
+ let _, x0 = List.hd l in
+ if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
+ then begin
+ let k = (v, List.map (fun (a, b) -> a, key b) l) in
+ let n =
+ try Hashtbl.find node_memo k
+ with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc)
+ in
+ DChoice(n, v, l)
+ end else x0
+
+ let get_leaf_fun_st () =
+ 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
+ try
+ Hashtbl.iter (fun i v -> if ND.eq v x then raise (Found_int i)) leaves;
+ incr lc;
+ Hashtbl.add leaves !lc x;
+ DVal (!lc, st)
+ with Found_int i -> DVal (i, st)
+ in leaves, get_leaf
+
+ let get_leaf_fun () =
+ let leaves, get_leaf = get_leaf_fun_st () in
+ leaves, get_leaf false
+
(*
edd_print : Format.formatter -> edd_v -> unit
*)
@@ -115,11 +145,11 @@ end = struct
let print_n fmt = function
| DBot -> Format.fprintf fmt "⊥";
| DTop -> Format.fprintf fmt "⊤";
- | DVal i -> if i > !max_v then max_v := i;
- Format.fprintf fmt "v%d" i;
+ | DVal (i, s) -> if i > !max_v then max_v := i;
+ Format.fprintf fmt "v%d%s" i (if s then "*" else "");
| DChoice(n, _, _) -> Format.fprintf fmt "n%d" n
in
- Format.fprintf fmt "Root: %a@." print_n v.root;
+ Format.fprintf fmt "%a where:@." print_n v.root;
for id = !max_n downto 0 do
try match Hashtbl.find c_nodes id with
@@ -180,46 +210,15 @@ end = struct
{ ve; root; leaves }
(*
- edd_join_meet : bool -> edd_v -> edd_v -> edd_v
edd_join : edd_v -> edd_v -> edd_v
edd_meet : edd_v -> edd_v -> edd_v
*)
- let edd_join_meet op a b =
+ let edd_join a b =
let ve = a.ve in
+ let leaves, get_leaf = get_leaf_fun () in
+ let dq = new_node_fun () in
- let leaves = Hashtbl.create 12 in
- let lc = ref 0 in
-
- let get_leaf x =
- if ND.is_top x then DTop else
- if ND.is_bot x then DBot else begin
- let id = ref None in
- Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
- match !id with
- | Some i -> DVal i
- | None ->
- incr lc;
- Hashtbl.add leaves !lc x;
- DVal (!lc)
- end
- in
-
- let nc = ref 0 in
- let node_memo = Hashtbl.create 12 in
- let dq v l =
- let _, x0 = List.hd l in
- if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
- then begin
- let k = (v, List.map (fun (a, b) -> a, key b) l) in
- let n =
- try Hashtbl.find node_memo k
- with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc)
- in
- DChoice(n, v, l)
- end else x0
- in
-
- let f_join f_rec na nb =
+ let f f_rec na nb =
match na, nb with
| DTop, _ | _, DTop -> DTop
| DBot, DBot -> DBot
@@ -240,11 +239,11 @@ end = struct
in
dq v kl
- | DBot, DVal i ->
+ | DBot, DVal (i, _) ->
get_leaf (Hashtbl.find b.leaves i)
- | DVal i, DBot ->
+ | DVal (i, _), DBot ->
get_leaf (Hashtbl.find a.leaves i)
- | DVal u, DVal v ->
+ | DVal (u, _), DVal (v, _) ->
let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
get_leaf x
@@ -255,8 +254,14 @@ end = struct
let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
dq vb kl
in
+ { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
- let f_meet f_rec na nb =
+ let edd_meet a b =
+ let ve = a.ve in
+ let leaves, get_leaf = get_leaf_fun () in
+ let dq = new_node_fun () in
+
+ let f f_rec na nb =
match na, nb with
| DBot, _ | _, DBot -> DBot
| DTop, DTop -> DTop
@@ -277,11 +282,11 @@ end = struct
in
dq v kl
- | DTop, DVal i ->
+ | DTop, DVal (i, _) ->
get_leaf (Hashtbl.find b.leaves i)
- | DVal i, DTop ->
+ | DVal (i, _), DTop ->
get_leaf (Hashtbl.find a.leaves i)
- | DVal u, DVal v ->
+ | DVal (u, _) , DVal (v, _) ->
let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
get_leaf x
@@ -292,14 +297,7 @@ end = struct
let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
dq vb kl
in
-
- if op then
- { leaves; ve; root = time "join" (fun () -> memo2 f_join a.root b.root) }
- else
- { leaves; ve; root = time "meet" (fun () -> memo2 f_meet a.root b.root) }
-
- let edd_join = edd_join_meet true
- let edd_meet = edd_join_meet false
+ { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
@@ -310,33 +308,18 @@ end = struct
let edd_num_apply v nfun =
let ve = v.ve in
- let lc = ref 0 in
- let leaves = Hashtbl.create 12 in
+ let leaves, get_leaf = get_leaf_fun () in
- let get_leaf x =
- if ND.is_bot x then DBot else begin
- let id = ref None in
- Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
- match !id with
- | Some i -> DVal i
- | None ->
- incr lc;
- Hashtbl.add leaves !lc x;
- DVal (!lc)
- end
- in
+ let dq = new_node_fun () in
let f f_rec n =
match n with
| DBot -> DBot
| DTop -> get_leaf (nfun (ND.top ve.nvars))
- | DVal i -> get_leaf (nfun (Hashtbl.find v.leaves i))
+ | 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
- let _, x0 = List.hd l in
- if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
- then DChoice(n, var, l)
- else x0
+ dq var l
in
{ leaves; ve; root = memo f v.root }
@@ -375,6 +358,25 @@ end = struct
edd_join (edd_apply_cl v (eca, nc@nca, ra))
(edd_apply_cl v (ecb, nc@ncb, rb))
+
+ (*
+ edd_extract_path : edd_v -> id -> edd_v
+ *)
+ let edd_extract_path v leaf_id =
+ let ve = v.ve in
+
+ let dq = new_node_fun () in
+
+ let f f_rec n =
+ match n with
+ | DVal (i, _) when i = leaf_id -> DTop
+ | DChoice(n, var, l) ->
+ let l = List.map (fun (k, v) -> k, f_rec v) l in
+ dq var l
+ | _ -> DBot
+ in
+ { leaves = Hashtbl.create 1; ve; root = memo f v.root }
+
(*
edd_eq : edd_v -> edd_v -> bool
*)
@@ -383,7 +385,7 @@ end = struct
match na, nb with
| DBot, DBot -> true
| DTop, DTop -> true
- | DVal i, DVal j ->
+ | DVal (i, _), DVal (j, _) ->
ND.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)
@@ -398,23 +400,11 @@ end = struct
let edd_forget_vars v vars =
let ve = v.ve in
- let leaves = Hashtbl.create 12 in
- let lc = ref 0 in
-
- let get_leaf x =
- let id = ref None in
- Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
- begin match !id with
- | Some i -> DVal i
- | None ->
- incr lc;
- Hashtbl.add leaves !lc x;
- DVal (!lc)
- end
- in
+ let leaves, get_leaf = get_leaf_fun () in
let nc = ref 0 in
let memo = Hashtbl.create 12 in
+ let node_memo = Hashtbl.create 12 in
let rec f l =
let kl = List.sort Pervasives.compare (List.map key l) in
try Hashtbl.find memo kl
@@ -424,7 +414,7 @@ end = struct
(fun (cn, fn) node -> match node with
| DBot -> cn, fn
| DTop -> raise Top
- | DVal i -> cn, i::fn
+ | DVal (i, _) -> cn, i::fn
| DChoice (n, v, l) -> (n, v, l)::cn, fn)
([], []) l in
let cn = List.sort
@@ -441,7 +431,7 @@ end = struct
let _, dv, cl = List.hd cn in
let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in
let ch1 = List.map (fun (a, b, c) -> DChoice(a, b, c)) nd in
- let ch2 = List.map (fun i -> DVal i) fn in
+ let ch2 = List.map (fun i -> DVal (i, false)) fn in
if List.mem dv vars then
(* Do union of all branches branching from nodes on variable dv *)
let ch3 = List.flatten
@@ -458,7 +448,12 @@ end = struct
let _, x0 = List.hd cc in
if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) cc
then begin
- incr nc; DChoice(!nc, dv, cc)
+ let k = (dv, List.map (fun (a, b) -> a, key b) cc) in
+ let n =
+ try Hashtbl.find node_memo k
+ with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc)
+ in
+ DChoice(n, dv, cc)
end else x0
with | Top -> DTop
in Hashtbl.add memo kl r; r
@@ -524,7 +519,134 @@ end = struct
(*
+ edd_find_starred : edd_v -> int option
+ edd_unstar : edd_v -> int -> edd_v
+ *)
+ let edd_find_starred v =
+ let f f_rec = function
+ | DVal (i, true) -> raise (Found_int i)
+ | DChoice(_, _, l) -> List.iter (fun (_, x) -> f_rec x) l
+ | _ -> ()
+ in
+ try memo f v.root; None
+ with Found_int i -> Some i
+
+ let edd_unstar v i =
+ let f f_rec = function
+ | DChoice(a, b, l) -> DChoice(a, b, List.map (fun (c, x) -> c, f_rec x) l)
+ | DVal(j, n) when i = j -> DVal(i, false)
+ | x -> x
+ in
+ { v with root = memo f v.root }
+
+
+ (*
+ edd_join_widen : edd_v -> edd_v -> edd_v
+ *)
+ let edd_join_widen (a:edd_v) (b:edd_v) =
+ let ve = a.ve in
+ let leaves, get_leaf = get_leaf_fun () in
+ let dq = new_node_fun () in
+
+ let f f_rec na nb =
+ match na, nb with
+ | DTop, _ | _, DTop -> DTop
+ | DBot, DBot -> DBot
+
+ | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+ let kl = List.map2
+ (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+ ta, f_rec ba bb)
+ la lb
+ in
+ dq va kl
+ | DChoice(_, va, la), DChoice(_, vb, lb) ->
+ let v, kl =
+ if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
+ va, List.map (fun (k, ca) -> k, f_rec ca nb) la
+ else
+ vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
+ in
+ dq v kl
+
+ | DBot, DVal (i, _) ->
+ get_leaf (Hashtbl.find b.leaves i)
+ | DVal (i, _), DBot ->
+ get_leaf (Hashtbl.find a.leaves i)
+ | DVal (u, _), DVal (v, _) ->
+ let p1, p2 = edd_extract_path a u, edd_extract_path b v in
+ let widen =
+ if edd_eq p1 p2 then true else false
+ in
+ let x = (if widen then ND.widen else ND.join)
+ (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+ get_leaf x
+
+ | DChoice(_,va, la), _ ->
+ let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+ dq va kl
+ | _, DChoice(_, vb, lb) ->
+ let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+ dq vb kl
+ in
+ { leaves; ve; root = time "join/W" (fun () -> memo2 f a.root b.root) }
+
+ (*
+ edd_join_star : edd_v -> edd_v -> edd_v
+
+ Star in A all things that are in B and not in A.
+ *)
+ let edd_join_star (a:edd_v) (b:edd_v) =
+ let ve = a.ve in
+ let leaves, get_leaf = get_leaf_fun_st () in
+ let dq = new_node_fun () in
+
+ let f f_rec na nb =
+ match na, nb with
+ | DTop, _ | _, DTop -> DTop
+ | DBot, DBot -> DBot
+
+ | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+ let kl = List.map2
+ (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+ ta, f_rec ba bb)
+ la lb
+ in
+ dq va kl
+ | DChoice(_, va, la), DChoice(_, vb, lb) ->
+ let v, kl =
+ if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
+ va, List.map (fun (k, ca) -> k, f_rec ca nb) la
+ else
+ vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
+ in
+ dq v kl
+
+ | DBot, DVal (i, _) ->
+ get_leaf true (Hashtbl.find b.leaves i)
+ | DVal (i, s), DBot ->
+ get_leaf s (Hashtbl.find a.leaves i)
+ | DVal (u, s1), DVal (v, _) ->
+ 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 star =
+ s1 || not (edd_eq p1 p2) || not (ND.subset d2 d1)
+ in
+ let x = ND.join d1 d2 in
+ get_leaf star x
+
+ | DChoice(_,va, la), _ ->
+ let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+ dq va kl
+ | _, DChoice(_, vb, lb) ->
+ let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+ dq vb kl
+ in
+ { leaves; ve; root = time "join/*" (fun () -> memo2 f a.root b.root) }
+
+ (*
pass_cycle : env -> edd_v -> edd_v
+ unpass_cycle : env -> edd_v -> edd_v
*)
let pass_cycle env v =
let assign_e, assign_n = List.fold_left
@@ -545,6 +667,28 @@ end = struct
let v = edd_forget_vars v ef in
edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
+ let unpass_cycle env v =
+ let assign_e, assign_n = List.fold_left
+ (fun (ae, an) (a, b, t) -> match t with
+ | TEnum _ -> (b, a)::ae, an
+ | TInt | TReal -> ae, (b, NIdent a)::an)
+ ([], []) 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 ef, nf = List.fold_left
+ (fun (ef, nf) (_, var, t) ->
+ if var.[0] <> 'N' then
+ match t with
+ | TEnum _ -> var::ef, nf
+ | TReal | TInt -> ef, var::nf
+ else ef, nf)
+ ([], []) env.rp.all_vars in
+
+ let v = edd_forget_vars v ef in
+ edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
+
(*
extract_linked_evars : conslist -> (id * id) list
@@ -700,7 +844,7 @@ end = struct
(List.sort Pervasives.compare (List.map ord_couple lv1)) in
let lv2 = uniq_sorted
(List.sort Pervasives.compare (List.map ord_couple lv2)) in
- let evars_ord = List.rev @@ scope_constrict evars ( lv1 ) in
+ let evars_ord = List.rev @@ time "SCA" (fun () -> scope_constrict evars ( lv1 )) in
let ev_order = Hashtbl.create (List.length evars) in
List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
@@ -737,20 +881,69 @@ end = struct
let do_prog opt rp =
let e = init_env opt rp in
- let rec f x =
- Format.printf "Apply formula...@.";
- let d2 = edd_apply_cl x e.cl in
- Format.printf "Pass cycle...@.";
- let dc = pass_cycle e d2 in
- Format.printf "Join with init...@.";
- let dcc = edd_join dc e.data in
- Format.printf "@[<hov>%a@]@.@." edd_print dcc;
- if not (edd_eq x dcc) then f dcc else dcc
+
+ (* Do iterations until fixpoint is reached *)
+ let rec ch_it n x =
+ match edd_find_starred x with
+ | None ->
+ Format.printf "Chaotic iteration %d : full iteration.@." n;
+
+ let d2 = edd_apply_cl x e.cl in
+ let dc = pass_cycle e d2 in
+ let y = edd_join_star x dc in
+
+ if e.opt.verbose_ci then
+ Format.printf " -> %a@." edd_print y;
+
+ if not (edd_eq x y) then ch_it (n+1) y else y
+
+ | Some i ->
+ let path = edd_extract_path x i in
+ let x = edd_unstar x i in
+ Format.printf "Chaotic iteration %d: @[<hov>%a@]@." n edd_print path;
+
+ let path_target = unpass_cycle e path in
+ let start = edd_meet path x in
+
+ let f i =
+ let i = edd_meet path i in
+ let i' = edd_meet i path_target in
+ let q = edd_join start (pass_cycle e (edd_apply_cl i' e.cl)) in
+ edd_meet path q
+ in
+
+ let rec iter n i =
+ let fi = f i in
+ let j =
+ if n < e.opt.widen_delay then
+ edd_join i fi
+ else
+ edd_join_widen i fi
+ in
+ if edd_eq i j then j else iter (n+1) j
+ in
+ let y = iter 0 start in
+ let z = fix edd_eq f y in
+
+
+ let j = pass_cycle e (edd_apply_cl z e.cl) in
+ let r = edd_join_star x j in
+
+ if e.opt.verbose_ci then
+ Format.printf " -> %a@." edd_print r;
+
+ ch_it (n+1) r
in
+
+ let init_acc = edd_join_star (edd_bot e.data.ve) e.data in
- let final = edd_apply_cl (f e.data) e.cl in
+ (* Dump final state *)
+ let acc = ch_it 0 init_acc in
+ Format.printf "Finishing up...@.";
+ let final = edd_apply_cl acc e.cl in
(*Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;*)
+ (* Check guarantees *)
let check_guarantee (id, f) =
let cl = Formula.conslist_of_f f in
Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ "
@@ -767,6 +960,33 @@ end = struct
Format.printf "@]@."
end;
+ (* Examine probes *)
+ if List.exists (fun (p, _, _) -> p) e.rp.all_vars then begin
+ let final_flat = edd_forget_vars final
+ (List.fold_left
+ (fun l (_, id, ty) -> match ty with
+ | TInt | TReal -> l
+ | TEnum _ -> id::l)
+ [] e.rp.all_vars) in
+ let final_flat = match final_flat.root with
+ | DTop -> ND.top e.ve.nvars
+ | DBot -> ND.bottom e.ve.nvars
+ | DVal(i, _) -> Hashtbl.find final_flat.leaves i
+ | DChoice _ -> assert false
+ in
+
+ Format.printf "Probes: @[<v 0>";
+ List.iter (fun (p, id, ty) ->
+ 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)
+ e.rp.all_vars;
+ Format.printf "@]@."
+ end
+
end