summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-08 10:27:23 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-08 10:27:23 +0200
commit3b647cab0d3ac143b97524e6b0a406c349898db5 (patch)
tree6f22cf4916a5096b193df73f242dcb64edb54b56
parent3f53be86214bb9a7873a6cf3377c49e5f84d9729 (diff)
downloadscade-analyzer-3b647cab0d3ac143b97524e6b0a406c349898db5.tar.gz
scade-analyzer-3b647cab0d3ac143b97524e6b0a406c349898db5.zip
Implement stand-alone EDDs
-rw-r--r--Makefile1
-rw-r--r--abstract/abs_interp_edd.ml2
-rw-r--r--abstract/enum_domain.ml230
-rw-r--r--abstract/enum_domain_edd.ml371
-rw-r--r--[-rwxr-xr-x]tests/source/counters.scade0
5 files changed, 372 insertions, 232 deletions
diff --git a/Makefile b/Makefile
index 3e5d01a..a6cc2d8 100644
--- a/Makefile
+++ b/Makefile
@@ -18,6 +18,7 @@ SRC= main.ml \
abstract/apron_domain.ml \
abstract/num_domain.ml \
abstract/enum_domain.ml \
+ abstract/enum_domain_edd.ml \
\
abstract/formula.ml \
abstract/formula_printer.ml \
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 8ea0012..1b3bb39 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -47,7 +47,6 @@ end = struct
ve : varenv;
root : edd;
leaves : (int, ND.t) Hashtbl.t;
- (* add here eventual annotations *)
}
(*
@@ -529,7 +528,6 @@ end = struct
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
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index d216276..ea2b053 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -264,233 +264,3 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
end
-(*
- Complicated domain : a set of values for each variables, plus some
- constraints on couples of variables
- (eg. (x, y) in [ tt, tt ; ff, ff ]
-
- WARNING : This domain is not proved to be safe. In particular, it may represent
- a set of contraints that imply Bot (ie that are impossible) without raising the
- Bot exception. (there is potentially exponential cost in the checking that all
- the constraints are coherent, and I have no idea of an algorithm for doing that
- check.)
-
- Therefore, do not use this domain unless you know what you are doing (which is
- probably not the case anyway).
-*)
-
-module MultiValuationCCons : ENUM_ENVIRONMENT_DOMAIN = struct
-
- module VarC = struct
- type t = id * id
- let compare = Pervasives.compare
- end
- module VarCMap = Mapext.Make(VarC)
-
- type item = string
-
- type t = {
- vars : (id * item list) list;
- value : item list VarMap.t;
-
- (* in ccond (x, y) -> l, must have x < y (textual order on identifiers) -> unicity *)
- ccons : (item * item) list VarCMap.t;
- }
-
- let sort = List.sort Pervasives.compare
- let uniq x = uniq_sorted (sort x)
- let list_inter x y = List.filter (fun k -> List.mem k y) x
-
- let all_couples l1 l2 =
- List.flatten
- (List.map (fun x -> List.map (fun y -> x, y) l2) l1)
-
- let top vars = { vars; value = VarMap.empty; ccons = VarCMap.empty }
-
- let vars x = x.vars
-
- let forgetvar x id =
- (* TODO : try to find a substitution variable so that some contraints can be propagated.
- this is important so that cycle passing can be done correctly ! *)
- { x with
- value = VarMap.remove id x.value;
- ccons = VarCMap.filter (fun (a, b) _ -> a <> id && b <> id) x.ccons }
-
- let project x id =
- try VarMap.find id x.value
- with Not_found -> List.assoc id x.vars
-
- let project2 x id1 id2 =
- try
- let id1', id2' = ord_couple (id1, id2) in
- if id1' = id1 then
- VarCMap.find (id1, id2) x.ccons
- else
- List.map (fun (a, b) -> b, a) (VarCMap.find (id1', id2') x.ccons)
- with _ ->
- let v1, v2 = project x id1, project x id2 in
- all_couples v1 v2
-
- let strict x =
- let rec f x =
- (*
- - if (x, y) in [ a, b1 ; a, b2 ; ... ; a, bn ],
- replace this by x = a and y in { b1, ..., bn }
- - filter (x, y) in [ ... ] with x in specified itv, y in specified itv
- *)
- let usefull, vv, cc =
- VarCMap.fold
- (fun (x, y) l (usefull, vv, cc) ->
- let p1, p2 = uniq (List.map fst l), uniq (List.map snd l) in
- let p1 = try list_inter p1 (VarMap.find x vv) with _ -> p1 in
- let p2 = try list_inter p2 (VarMap.find y vv) with _ -> p2 in
-
- if p1 = [] || p2 = [] then raise Bot;
- let vv = VarMap.add x p1 (VarMap.add y p2 vv) in
-
- if List.length p1 = 1 || List.length p2 = 1
- then
- true, vv, cc
- else
- match List.filter (fun (u, v) -> List.mem u p1 && List.mem v p2) l with
- | [] -> raise Bot
- | l2 -> List.length l2 < List.length l, vv, VarCMap.add (x, y) l2 cc)
- x.ccons (false, x.value, VarCMap.empty) in
-
- let x = { x with value = vv; ccons = cc } in
- if usefull then f x else x
- in
- f x
-
- let join x1 x2 =
- let v = VarMap.merge
- (fun _ a b -> match a, b with
- | Some a, Some b -> Some (uniq (a@b))
- | _ -> None)
- x1.value x2.value in
- let x = { x1 with value = v } in
-
- let cc = VarCMap.merge
- (fun (id1, id2) l1 l2 ->
- let v1, v2 = project x1 id1, project x id2 in
- let ac = all_couples v1 v2 in
- let c = List.filter
- (fun q ->
- (match l1 with Some l -> List.mem q l | _ -> true) ||
- (match l2 with Some l -> List.mem q l | _ -> true))
- ac in
- if List.length c < List.length ac then Some c else None)
- x1.ccons x2.ccons in
-
- strict { x with ccons = cc }
-
- let meet x1 x2 =
- let v = VarMap.merge
- (fun _ a b -> match a, b with
- | Some a, None | None, Some a -> Some a
- | Some a, Some b ->
- begin match list_inter a b with
- | [] -> raise Bot | l -> Some l end
- | _ -> None)
- x1.value x2.value in
- let x = { x1 with value = v } in
-
- let cc = VarCMap.merge
- (fun (id1, id2) l1 l2 ->
- let v1, v2 = project x id1, project x id2 in
- let ac = all_couples v1 v2 in
- let c1 = match l1 with Some l -> list_inter l ac | None -> ac in
- let c2 = match l2 with Some l -> list_inter l ac | None -> ac in
- match list_inter c1 c2 with
- | [] -> raise Bot
- | l -> if List.length l < List.length ac then Some l else None)
- x1.ccons x2.ccons in
-
- strict { x with ccons = cc }
-
- let subset a b =
- VarMap.for_all
- (fun id v ->
- let vs = project a id in
- List.for_all (fun c -> List.mem c vs) v)
- b.value
- &&
- VarCMap.for_all
- (fun (id1, id2) l ->
- let l2 = project2 a id1 id2 in
- List.for_all (fun c -> List.mem c l) l2)
- b.ccons
- let eq a b =
- subset a b && subset b a
-
- let apply_cons x (op, id, e) =
- let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
-
- match e with
- | EItem s ->
- let pv = project x id in
- begin match List.filter (op s) pv with
- | [] -> []
- | vals -> try [strict { x with value = VarMap.add id vals x.value }] with Bot -> []
- end
- | EIdent id2 ->
- let id, id2 = ord_couple (id, id2) in
- let c = project2 x id id2 in
- let ok_c = List.filter (fun (a, b) -> op a b) c in
- try
- [match uniq (List.map fst ok_c), uniq (List.map snd ok_c) with
- | [], _ | _, [] -> raise Bot
- | [a], q -> strict { x with value = VarMap.add id [a] (VarMap.add id2 q x.value) }
- | q, [b] -> strict { x with value = VarMap.add id q (VarMap.add id2 [b] x.value) }
- | _ -> strict { x with ccons = VarCMap.add (id, id2) ok_c x.ccons}
- ]
- with Bot -> []
-
- let assign x idl =
- let x2 = List.fold_left (fun x (v, _) -> forgetvar x v) x idl in
- let v = List.fold_left
- (fun v (id, id2) ->
- try VarMap.add id (VarMap.find id2 x.value) v
- with Not_found -> v)
- x2.value idl in
- let c = VarCMap.fold
- (fun (v1, v2) l c ->
- let v1' = try List.assoc v1 idl with _ -> v1 in
- let v2' = try List.assoc v2 idl with _ -> v2 in
- VarCMap.add (v1', v2') l c)
- x.ccons x2.ccons in
- strict { x with value = v; ccons = c }
-
-
- let print fmt x =
- let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x.value) in
- let s = List.sort Pervasives.compare b in
- let rec bl = function
- | [] -> []
- | (v, id)::q ->
- let v = sort v in
- if v <> sort (List.assoc id x.vars) then
- match bl q with
- | (vv, ids)::q when vv = v -> (v, id::ids)::q
- | r -> (v, [id])::r
- else
- bl q
- in
- let sbl = bl s in
- Format.fprintf fmt "@[<v 2>{ ";
- List.iteri
- (fun j (v, ids) ->
- if j > 0 then Format.fprintf fmt "@ ";
- Format.fprintf fmt "@[<hov 4>";
- List.iteri
- (fun i id ->
- if i > 0 then Format.fprintf fmt ",@ ";
- Format.fprintf fmt "%a" Formula_printer.print_id id)
- ids;
- match v with
- | [v0] -> Format.fprintf fmt " ≡ %s@]" v0
- | l -> Format.fprintf fmt " ∊ @[<hov>{ %a }@]@]" (print_list Format.pp_print_string ", ") l)
- sbl;
- Format.fprintf fmt " }@]"
-
-end
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
new file mode 100644
index 0000000..60f2d3b
--- /dev/null
+++ b/abstract/enum_domain_edd.ml
@@ -0,0 +1,371 @@
+open Ast
+open Formula
+open Util
+open Enum_domain
+
+module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
+ exception Top
+
+ type item = string
+
+ type edd =
+ | DBot
+ | DTop
+ | DChoice of int * id * (item * edd) list
+
+ type t = {
+ vars : (id * item list) list;
+ order : (id, int) Hashtbl.t;
+ root : edd;
+ }
+
+ (* Utility functions for memoization *)
+ let key = function
+ | DBot -> -1
+ | DTop -> -2
+ | DChoice(i, _, _) -> i
+
+ let memo f =
+ let memo = Hashtbl.create 12 in
+ let rec ff v =
+ try Hashtbl.find memo (key v)
+ with Not_found ->
+ let r = f ff v in
+ Hashtbl.add memo (key v) r; r
+ in ff
+
+ let memo2 f =
+ let memo = Hashtbl.create 12 in
+ let rec ff v1 v2 =
+ try Hashtbl.find memo (key v1, key v2)
+ with Not_found ->
+ let r = f ff v1 v2 in
+ Hashtbl.add memo (key v1, key v2) r; r
+ in ff
+
+ let edd_node_eq = function
+ | DBot, DBot -> true
+ | DTop, DTop -> true
+ | DChoice(i, _, _), DChoice(j, _, _) -> i = j
+ | _ -> 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 rank v = function
+ | DChoice(_, x, _) -> Hashtbl.find v.order x
+ | _ -> 10000000
+
+
+ (*
+ print : Format.formatter -> t -> unit
+ *)
+ let print fmt v =
+ let print_nodes = Queue.create () in
+ let a = Hashtbl.create 12 in
+
+ let node_pc = Hashtbl.create 12 in
+ let f f_rec = function
+ | DChoice(_, _, l) ->
+ List.iter
+ (fun (_, c) -> match c with
+ | DChoice(n, _, _) ->
+ begin try Hashtbl.add node_pc n (Hashtbl.find node_pc n + 1)
+ with Not_found -> Hashtbl.add node_pc n 1 end
+ | _ -> ())
+ l;
+ List.iter (fun (_, c) -> f_rec c) l
+ | _ -> ()
+ in memo f v.root;
+
+ let rec print_n fmt = function
+ | DBot -> Format.fprintf fmt "⊥";
+ | DTop -> Format.fprintf fmt "⊤";
+ | DChoice(_, v, l) ->
+ match List.filter (fun (_, x) -> x <> DBot) l with
+ | [(c, nn)] ->
+ let aux fmt = function
+ | DChoice(nn, _, _) as i when Hashtbl.find node_pc nn >= 2 ->
+ if Hashtbl.mem a nn then () else begin
+ Queue.push i print_nodes;
+ Hashtbl.add a nn ()
+ end;
+ Format.fprintf fmt "n%d" nn
+ | x -> print_n fmt x
+ in
+ Format.fprintf fmt "%a = %s,@ %a" Formula_printer.print_id v c aux nn
+ | _ ->
+ Format.fprintf fmt "%a ? " Formula_printer.print_id v;
+ let print_u fmt (c, i) =
+ Format.fprintf fmt "%s → " c;
+ match i with
+ | DChoice(nn, v, l) ->
+ if Hashtbl.mem a nn then () else begin
+ Queue.push i print_nodes;
+ Hashtbl.add a nn ()
+ end;
+ Format.fprintf fmt "n%d" nn
+ | _ -> Format.fprintf fmt "%a" print_n i
+ in
+ Format.fprintf fmt "@[<h>%a@]" (print_list print_u ", ") l;
+ in
+ Format.fprintf fmt "@[<v 4>{ @[<hov>%a@]" print_n v.root;
+ while not (Queue.is_empty print_nodes) do
+ match Queue.pop print_nodes with
+ | DChoice(n, v, l) as x ->
+ Format.fprintf fmt "@ n%d: @[<hov>%a@]" n print_n x
+ | _ -> assert false
+ done;
+ Format.fprintf fmt " }@]"
+
+ (*
+ top : (id * item list) list -> t
+ *)
+ let top vars =
+ let order = Hashtbl.create 12 in
+ List.iteri (fun i (id, _) -> Hashtbl.add order id i) vars;
+ { vars; order; root = DTop }
+ (*
+ vars : t -> (id * item list) list
+ *)
+ let vars x = x.vars
+
+ (*
+ of_cons : t -> enum_cons -> t
+ The first t is NOT used as a decision function, here we only use
+ the variable ordering it provides.
+ *)
+ let of_cons v0 (op, vid, r) =
+ let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
+
+ let root = match r with
+ | EItem x ->
+ DChoice(0, vid,
+ List.map (fun v -> if op v x then v, DTop else v, DBot)
+ (List.assoc vid v0.vars))
+ | EIdent vid2 ->
+ let a, b =
+ if Hashtbl.find v0.order vid < Hashtbl.find v0.order vid2
+ then vid, vid2
+ else vid2, vid
+ in
+ let nc = ref 0 in
+ let nb x =
+ incr nc;
+ DChoice(!nc, b,
+ List.map (fun v -> if op v x then v, DTop else v, DBot)
+ (List.assoc b v0.vars))
+ in
+ DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a v0.vars))
+ in
+ { v0 with root = root }
+
+ (*
+ join : t -> t -> t
+ meet : t -> t -> t
+ *)
+ let join a b =
+ if a.root = DBot then b else
+ if b.root = DBot then a else
+ if a.root = DTop || b.root = DTop then { a with root = DTop } else begin
+ let dq = new_node_fun () in
+
+ let f f_rec na nb =
+ match na, nb with
+ | 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
+
+ | DTop, _ | _, DTop -> DTop
+ | DBot, DBot -> DBot
+
+ | DChoice(_,va, la), _ when rank a na < rank a nb ->
+ let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+ dq va kl
+ | _, DChoice(_, vb, lb) when rank a nb < rank a na ->
+ let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+ dq vb kl
+
+ | _ -> assert false
+ in
+ { a with root = memo2 f a.root b.root }
+ end
+
+ let meet a b =
+ if a.root = DTop then b else
+ if b.root = DTop then a else
+ if a.root = DBot || b.root = DBot then { a with root = DBot } else begin
+ let dq = new_node_fun () in
+
+ let f f_rec na nb =
+ match na, nb with
+ | 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
+
+ | DBot, _ | _, DBot -> DBot
+ | DTop, DTop -> DTop
+
+ | DChoice(_, va, la), _ when rank a na < rank a nb ->
+ let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+ dq va kl
+ | _, DChoice(_, vb, lb) when rank a nb < rank a na ->
+ let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+ dq vb kl
+
+ | _ -> assert false
+ in
+ {a with root = memo2 f a.root b.root }
+ end
+
+ (*
+ apply_cons : t -> enum_cons -> t
+ apply_cl : t -> enum_cons list -> t
+ *)
+ let apply_cons v x =
+ let v = meet v (of_cons v x) in
+ if v.root = DBot then [] else [v]
+ let apply_cl v ec =
+ let rec cl_k = function
+ | [] -> { v with root = DTop }
+ | [a] -> of_cons v a
+ | l ->
+ let n = ref 0 in
+ let la, lb = List.partition (fun _ -> incr n; !n mod 2 = 0) l in
+ meet (cl_k la) (cl_k lb)
+ in
+ let cons_edd = cl_k ec in
+ meet v cons_edd
+
+ (*
+ eq : edd_v -> edd_v -> bool
+ *)
+ let eq a b =
+ let f f_rec na nb =
+ match na, nb with
+ | DBot, DBot -> true
+ | DTop, DTop -> true
+ | 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
+ | _ -> false
+ in memo2 f a.root b.root
+
+ (*
+ subset : edd_v -> edd_v -> bool
+ *)
+ let subset a b =
+ let rank = rank a in
+ let f f_rec na nb =
+ match na, nb with
+ | DBot, _ -> true
+ | _, DTop -> true
+ | DTop, DBot -> false
+
+ | 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
+ | DChoice(_, va, la), _ when rank na < rank nb ->
+ List.for_all (fun (c, n) -> f_rec n nb) la
+ | _, DChoice(_, vb, lb) when rank na > rank nb ->
+ List.for_all (fun (c, n) -> f_rec na n) lb
+ | _ -> assert false
+ in memo2 f a.root b.root
+
+ (*
+ forgetvars : t -> id list -> t
+ *)
+ let forgetvars v vars =
+ let dq = new_node_fun () in
+
+ let 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
+ with Not_found -> let r =
+ try
+ let cn = List.fold_left
+ (fun cn node -> match node with
+ | DBot -> cn
+ | DTop -> raise Top
+ | DChoice (n, v, l) -> (n, v, l)::cn)
+ [] l in
+ let cn = List.sort
+ (fun (n, v1, _) (n, v2, _) -> Pervasives.compare
+ (Hashtbl.find v.order v1) (Hashtbl.find v.order v2))
+ cn in
+ if cn = [] then
+ DBot
+ 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
+ if List.mem dv vars then
+ (* Do union of all branches branching from nodes on variable dv *)
+ let ch2 = List.flatten
+ (List.map (fun (_, _, c) -> List.map snd c) d) in
+ f (ch1@ch2)
+ else
+ (* Keep disjunction on variable dv *)
+ let cc = List.map
+ (fun (c, _) ->
+ let ch2 = List.map (fun (_, _, cl) -> List.assoc c cl) d in
+ c, f (ch1@ch2))
+ cl in
+ dq dv cc
+ with | Top -> DTop
+ in Hashtbl.add memo kl r; r
+ in
+ { v with root = f [v.root] }
+
+ let forgetvar v x = forgetvars v [x]
+
+ (*
+ project : t -> id -> item list
+ *)
+ let project v x =
+ try
+ let vals = ref [] in
+ let f f_rec = function
+ | DBot -> ()
+ | DChoice(_, var, l) when
+ Hashtbl.find v.order var < Hashtbl.find v.order x ->
+ List.iter (fun (_, c) -> f_rec c) l
+ | DChoice(_, var, l) when var = x ->
+ List.iter
+ (fun (v, l) ->
+ if l <> DBot && not (List.mem v !vals) then vals := v::(!vals))
+ l
+ | _ -> raise Top
+ in
+ memo f v.root; !vals
+ with Top -> List.assoc x v.vars
+
+ (*
+ assign : t -> (id * id) list -> t
+ *)
+ let assign v ids =
+ let v = forgetvars v (List.map fst ids) in
+ apply_cl v (List.map (fun (x, y) -> (E_EQ, x, EIdent y)) ids)
+
+end
diff --git a/tests/source/counters.scade b/tests/source/counters.scade
index 334bca1..334bca1 100755..100644
--- a/tests/source/counters.scade
+++ b/tests/source/counters.scade