diff options
| -rw-r--r-- | abstract/abs_interp_edd.ml | 223 | ||||
| -rw-r--r-- | abstract/apron_domain.ml | 1 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 3 | ||||
| -rw-r--r-- | abstract/num_domain.ml | 1 | ||||
| -rw-r--r-- | tests/source/uturn.scade | 4 |
5 files changed, 121 insertions, 111 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 863a22d..ebf7549 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -13,6 +13,9 @@ let time id f = Format.printf "] @?"; r + +exception Top + module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig val do_prog : cmdline_opt -> rooted_prog -> unit @@ -39,6 +42,7 @@ end = struct type edd = | DBot + | DTop | DVal of int | DChoice of int * id * (item * edd) list @@ -60,9 +64,10 @@ end = struct Where 'a = 'b = 'c = edd, but it can be adapted. *) let key = function - | DBot -> None - | DVal i -> Some (Left i) - | DChoice(i, _, _) -> Some (Right i) + | DBot -> 0 + | DTop -> 1 + | DVal i -> 2 * i + 2 + | DChoice(i, _, _) -> 2 * i + 3 let memo f = let memo = Hashtbl.create 12 in @@ -84,6 +89,7 @@ end = struct let edd_node_eq = function | DBot, DBot -> true + | DTop, DTop -> true | DVal i, DVal j when i = j -> true | DChoice(i, _, _), DChoice(j, _, _) when i = j -> true | _ -> false @@ -108,6 +114,7 @@ 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; | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n @@ -140,10 +147,7 @@ end = struct (* edd_top : evar list -> nvar list -> edd_v *) - let edd_top ve = - let leaves = Hashtbl.create 1 in - Hashtbl.add leaves 0 (ND.top ve.nvars); - { ve; root = DVal 0; leaves } + let edd_top ve = { ve; root = DTop; leaves = Hashtbl.create 1 } (* edd_of_cons : varenv -> enum_cons -> edd_v @@ -152,14 +156,11 @@ end = struct let op = match op with | E_EQ -> (=) | E_NE -> (<>) in let leaves = Hashtbl.create 1 in - Hashtbl.add leaves 0 (ND.top ve.nvars); - - let bot, top = DBot, DVal 0 in let root = match r with | EItem x -> DChoice(0, vid, - List.map (fun v -> if op v x then v, top else v, bot) + List.map (fun v -> if op v x then v, DTop else v, DBot) (List.assoc vid ve.evars)) | EIdent vid2 -> let a, b = @@ -171,7 +172,7 @@ end = struct let nb x = incr n; DChoice(!n, b, - List.map (fun v -> if op v x then v, top else v, bot) + List.map (fun v -> if op v x then v, DTop else v, DBot) (List.assoc b ve.evars)) in DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a ve.evars)) @@ -179,44 +180,49 @@ 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 a b = + let edd_join_meet op a b = let ve = a.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) + 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 f f_rec na nb = - let dq v l = - let _, x0 = List.hd l in - if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l - then begin - incr nc; DChoice(!nc, v, l) - end else x0 - 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 = match na, nb with + | DTop, _ | _, DTop -> DTop | DBot, DBot -> DBot - | 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 x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in - get_leaf x | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> let kl = List.map2 @@ -234,6 +240,14 @@ end = struct 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 x = 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 @@ -241,44 +255,11 @@ 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) } - - (* - edd_meet : edd_v -> edd_v -> edd_v - *) - let edd_meet a b = - let ve = a.ve in - let lc = ref 0 in - let leaves = Hashtbl.create 12 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 nc = ref 0 in - let f f_rec na nb = - let dq v l = - let _, x0 = List.hd l in - if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l - then begin - incr nc; DChoice(!nc, v, l) - end else x0 - in + let f_meet f_rec na nb = match na, nb with | DBot, _ | _, DBot -> DBot - | DVal u, DVal v -> - let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in - get_leaf x + | DTop, DTop -> DTop | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> let kl = List.map2 @@ -295,6 +276,15 @@ end = struct vb, List.map (fun (k, cb) -> k, f_rec na cb) lb in dq v kl + + | DTop, DVal i -> + get_leaf (Hashtbl.find b.leaves i) + | DVal i, DTop -> + get_leaf (Hashtbl.find a.leaves i) + | DVal u, DVal v -> + let x = ND.meet (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 @@ -302,7 +292,16 @@ end = struct let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in dq vb kl in - { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) } + + 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 + + (* edd_num_apply : edd_v -> (ND.t -> ND.t) -> edd_v @@ -330,6 +329,7 @@ end = struct 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)) | DChoice(n, var, l) -> let l = List.map (fun (k, v) -> k, f_rec v) l in @@ -357,6 +357,7 @@ 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 @@ -381,6 +382,7 @@ end = struct let f f_rec na nb = match na, nb with | DBot, DBot -> true + | DTop, DTop -> true | 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 -> @@ -417,45 +419,48 @@ end = struct let kl = List.sort Pervasives.compare (List.map key l) in try Hashtbl.find memo kl with Not_found -> let r = - let cn, fn = List.fold_left - (fun (cn, fn) node -> match node with - | DBot -> cn, fn - | DVal i -> cn, i::fn - | DChoice (n, v, l) -> (n, v, l)::cn, fn) - ([], []) l in - let cn = List.sort - (fun (n, v1, _) (n, v2, _) -> Pervasives.compare - (Hashtbl.find ve.ev_order v1) (Hashtbl.find ve.ev_order v2)) - cn in - if cn = [] then - if fn = [] then DBot - else - let x = list_fold_op ND.join - (List.map (Hashtbl.find v.leaves) fn) - in get_leaf x - else - 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 - if List.mem dv vars then - (* Do union of all branches branching from nodes on variable dv *) - let ch3 = List.flatten - (List.map (fun (_, _, c) -> List.map snd c) d) in - f (ch1@ch2@ch3) + try + let cn, fn = List.fold_left + (fun (cn, fn) node -> match node with + | DBot -> cn, fn + | DTop -> raise Top + | DVal i -> cn, i::fn + | DChoice (n, v, l) -> (n, v, l)::cn, fn) + ([], []) l in + let cn = List.sort + (fun (n, v1, _) (n, v2, _) -> Pervasives.compare + (Hashtbl.find ve.ev_order v1) (Hashtbl.find ve.ev_order v2)) + cn in + if cn = [] then + if fn = [] then DBot + else + let x = list_fold_op ND.join + (List.map (Hashtbl.find v.leaves) fn) + in get_leaf x else - (* Keep disjunction on variable dv *) + let _, dv, cl = List.hd cn in let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in - let cc = List.map - (fun (c, _) -> - let ch3 = List.map (fun (_, _, cl) -> List.assoc c cl) d in - c, f (ch1@ch2@ch3)) - cl in - 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) - end else x0 + let ch1 = List.map (fun (a, b, c) -> DChoice(a, b, c)) nd in + let ch2 = List.map (fun i -> DVal i) fn in + if List.mem dv vars then + (* Do union of all branches branching from nodes on variable dv *) + let ch3 = List.flatten + (List.map (fun (_, _, c) -> List.map snd c) d) in + f (ch1@ch2@ch3) + else + (* Keep disjunction on variable dv *) + let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in + let cc = List.map + (fun (c, _) -> + let ch3 = List.map (fun (_, _, cl) -> List.assoc c cl) d in + c, f (ch1@ch2@ch3)) + cl in + 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) + end else x0 + with | Top -> DTop in Hashtbl.add memo kl r; r in { leaves; ve; root = f [v.root] } diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index 7a823db..45803fc 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -71,6 +71,7 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct Abstract1.top manager (v_env vars) let bottom vars = Abstract1.bottom manager (v_env vars) let is_bot = Abstract1.is_bottom manager + let is_top = Abstract1.is_top manager let forgetvar x id = let v = [| Var.of_string id |] in diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index b3129c0..7a83303 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -57,6 +57,9 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct let is_bot env = match env with | Bot -> true | Env env -> strict env = Bot + let is_top env = match env with + | Bot -> false + | Env e -> VarMap.for_all (fun _ v -> v = V.top) e let forgetvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x diff --git a/abstract/num_domain.ml b/abstract/num_domain.ml index 96de8bc..285b3c4 100644 --- a/abstract/num_domain.ml +++ b/abstract/num_domain.ml @@ -10,6 +10,7 @@ module type NUMERICAL_ENVIRONMENT_DOMAIN = sig val bottom : (id * bool) list -> t val vbottom : t -> t (* bottom value with same variables *) val is_bot : t -> bool + val is_top : t -> bool (* variable management *) val vars : t -> (id * bool) list diff --git a/tests/source/uturn.scade b/tests/source/uturn.scade index 84c9b51..97c2fdb 100644 --- a/tests/source/uturn.scade +++ b/tests/source/uturn.scade @@ -64,8 +64,8 @@ let assume h3: empty_section -> true; assume h4: true -> implies(edge(not empty_section), pre grant_access); assume h5: true -> implies(edge(on_C), pre grant_exit); - assume h6: implies(edge(not on_A), on_B); - assume h7: implies(edge(not on_B), on_A or on_C); + assume h6: true -> implies(edge(not on_A), on_B); + assume h7: true -> implies(edge(not on_B), on_A or on_C); grant_access, grant_exit, do_AB, do_BC = UMS(on_A, on_B, on_C, ack_AB, ack_BC); |