summaryrefslogtreecommitdiff
path: root/abstract/enum_domain.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/enum_domain.ml')
-rw-r--r--abstract/enum_domain.ml343
1 files changed, 343 insertions, 0 deletions
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index c8b4ec5..2353049 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -34,6 +34,9 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig
end
+(*
+ Simple domain : one valuation for each variable, or T
+*)
module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
type item = string
@@ -142,3 +145,343 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
Format.fprintf fmt " }@]"
end
+
+
+(*
+ Less simple domain : a set of possible values for each variable, or T
+*)
+
+module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
+ type item = string
+
+ type t = {
+ vars : (id * item list) list;
+ value : item list VarMap.t;
+ }
+
+ let sort = List.sort Pervasives.compare
+ let uniq x = uniq_sorted (sort x)
+
+ let top vars = { vars; value = VarMap.empty }
+
+ let vars x = x.vars
+
+ let forgetvar x id =
+ { x with value = VarMap.remove id x.value }
+ let project x id =
+ try VarMap.find id x.value
+ with Not_found -> List.assoc id x.vars
+
+ 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
+ { x1 with value = v }
+ 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.filter (fun x -> List.mem x b) a with
+ | [] -> raise Bot | l -> Some l end
+ | _ -> None)
+ x1.value x2.value in
+ { x1 with value = v }
+
+ let subset a b =
+ VarMap.for_all
+ (fun id v ->
+ try let v2 = VarMap.find id b.value in
+ List.for_all (fun x -> List.mem x v2) v
+ with Not_found -> true)
+ a.value
+ 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 -> [{ x with value = VarMap.add id vals x.value }]
+ end
+ | EIdent id2 ->
+ let v1 = project x id in
+ let v2 = project x id2 in
+ List.fold_left
+ (fun l v1 ->
+ let v2 = List.filter (op v1) v2 in
+ let x = { x with value = VarMap.add id [v1] x.value } in
+ match v2 with
+ | [] -> l
+ | _ -> { x with value = VarMap.add id2 v2 x.value }::l)
+ [] v1
+
+ let assign x idl =
+ let v = List.fold_left
+ (fun v (id, id2) ->
+ try VarMap.add id (VarMap.find id2 x.value) v
+ with Not_found -> VarMap.remove id v )
+ x.value idl
+ in { x with value = v }
+
+
+ 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
+
+
+(*
+ Complicated domain : a set of values for each variables, plus some
+ constraints on couples of variables
+ (eg. (x, y) in [ tt, tt ; ff, ff ]
+*)
+
+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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 16:56:16 +0000