diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_domain.ml | 401 | ||||
| -rw-r--r-- | abstract/abs_interp.ml | 468 | ||||
| -rw-r--r-- | abstract/apron_domain.ml | 38 | ||||
| -rw-r--r-- | abstract/enum_domain.ml | 144 | ||||
| -rw-r--r-- | abstract/intervals_domain.ml | 8 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 33 | ||||
| -rw-r--r-- | abstract/num_domain.ml | 15 | ||||
| -rw-r--r-- | abstract/transform.ml | 14 |
8 files changed, 590 insertions, 531 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml deleted file mode 100644 index d6ff489..0000000 --- a/abstract/abs_domain.ml +++ /dev/null @@ -1,401 +0,0 @@ -open Ast -open Formula -open Num_domain -open Typing -open Util - -type disjunct_policy = - | DAlways - | DNever - | DSometimes - -module type ENVIRONMENT_DOMAIN = sig - type t - type itv - - (* construction *) - val init : t - val bottom : t - val vbottom : t -> t (* bottom value with same environment *) - val is_bot : t -> bool - - (* variable management *) - val addvar : t -> id -> Typing.typ -> t - val rmvar : t -> id -> t - val vars : t -> (id * Typing.typ) list - - val forgetvar : t -> id -> t - val var_itv : t -> id -> itv - val set_disjunct : t -> id -> disjunct_policy -> t - - (* set_theoretic operations *) - val join : t -> t -> t (* union *) - val meet : t -> t -> t (* intersection *) - val widen : t -> t -> t - - val subset : t -> t -> bool - val eq : t -> t -> bool - - (* abstract operations *) - val apply_f : t -> bool_expr -> t - val apply_cl : t -> conslist -> t - val assign : t -> (id * id) list -> t - - (* pretty-printing *) - val print_vars : Format.formatter -> t -> id list -> unit - val print_all : Format.formatter -> t -> unit - val print_itv : Format.formatter -> itv -> unit - -end - - -module D_ignore_enum (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = -struct - type t = ND.t - type itv = ND.itv - - - let init = ND.init - let bottom = ND.bottom - let vbottom = ND.vbottom - let is_bot = ND.is_bot - - let addvar x id ty = ND.addvar x id (ty = TReal) - let rmvar = ND.rmvar - let vars x = List.map (fun (id, r) -> id, if r then TReal else TInt) (ND.vars x) - - let forgetvar = ND.forgetvar - let var_itv = ND.var_itv - let set_disjunct x _ _ = x - - let join = ND.join - let meet = ND.meet - let widen = ND.widen - - let subset = ND.subset - let eq = ND.eq - - let rec apply_cl x (econs, cons, rest) = match rest with - | CLTrue -> - ND.apply_ncl x cons - | CLFalse -> vbottom x - | CLAnd(a, b) -> - let y = apply_cl x (econs, cons, a) in - apply_cl y (econs, cons, b) - | CLOr((eca, ca, ra), (ecb, cb, rb)) -> - let y = apply_cl x (econs@eca, cons@ca, ra) in - let z = apply_cl x (econs@ecb, cons@cb, rb) in - join y z - - let apply_f x f = apply_cl x (conslist_of_f f) - - let assign x v = ND.assign x (List.map (fun (id, id2) -> id, NIdent id2) v) - - let print_vars = ND.print_vars - let print_all = ND.print_all - let print_itv = ND.print_itv -end - -module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct - - module Valuation = struct - type t = string VarMap.t - let compare = VarMap.compare Pervasives.compare - - let subset a b = - VarMap.for_all - (fun id v -> - try v = VarMap.find id b - with Not_found -> true) - a - - let print fmt x = - let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x) in - let s = List.sort Pervasives.compare b in - let rec bl = function - | [] -> [] - | (v, id)::q -> - begin match bl q with - | (vv, ids)::q when vv = v -> (v, id::ids)::q - | r -> (v, [id])::r - end - 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; - Format.fprintf fmt " ≡ %s@]" v) - sbl; - Format.fprintf fmt " }@]" - - end - module VMap = Mapext.Make(Valuation) - - type t = { - nvars : (id * bool) list; - evars : (id * string list) list; - nd_init : ND.t; - nd_bottom : ND.t; - value : ND.t VMap.t; - disj_v : id list; - nodisj_v : id list; - } - type itv = - | IN of ND.itv VMap.t - | IE of SSet.t - - - let init = { - nvars = []; evars = []; disj_v = []; nodisj_v = []; - nd_init = ND.init; - nd_bottom = ND.bottom; - value = VMap.singleton VarMap.empty ND.init; - } - let bottom = { - nvars = []; evars = []; disj_v = []; nodisj_v = []; - nd_init = ND.init; - nd_bottom = ND.bottom; - value = VMap.empty; - } - let vbottom x = { x with value = VMap.empty } - - let is_bot x = VMap.is_empty x.value || VMap.for_all (fun _ v -> ND.is_bot v) x.value - - let strict value = - VMap.filter (fun _ v -> not (ND.is_bot v)) value - - let add_case_w widen x (enum, num) = - let value = x.value in - let enum = VarMap.filter (fun k v -> not (List.mem k x.nodisj_v)) enum in - let v = - if VMap.exists - (fun e0 n0 -> Valuation.subset enum e0 && ND.subset num n0) - value - || ND.is_bot num - then - value - else - try VMap.add enum - ((if widen then ND.widen else ND.join) (VMap.find enum value) num) - value - with Not_found -> VMap.add enum num value - in { x with value = v } - let add_case = add_case_w false - - let addvar x id ty = match ty with - | TInt | TReal -> - let is_real = (ty = TReal) in - { x with - nvars = (id, is_real)::(x.nvars); - nd_init = ND.addvar x.nd_init id is_real; - nd_bottom = ND.addvar x.nd_bottom id is_real; - value = VMap.map (fun v -> ND.addvar v id is_real) x.value - } - | TEnum options -> - { x with - evars = (id, options)::x.evars - } - - let vars x = - List.map (fun (id, r) -> id, if r then TReal else TInt) x.nvars @ - List.map (fun (id, o) -> id, TEnum o) x.evars - - let forgetvar x id = - if List.mem_assoc id x.evars then - VMap.fold - (fun enum num value -> - let enum' = VarMap.remove id enum in - add_case value (enum', num)) - x.value - { x with value = VMap.empty } - else - { x with value = strict @@ VMap.map (fun v -> ND.forgetvar v id) x.value } - - let rmvar x id = - if List.mem_assoc id x.evars then - let y = forgetvar x id in - { y with - evars = List.remove_assoc id x.evars } - else - { x with - nvars = List.remove_assoc id x.nvars; - value = strict @@ VMap.map (fun v -> ND.rmvar v id) x.value } - - let var_itv x id = - if List.mem_assoc id x.nvars - then - let x = List.fold_left - (fun x (v, _) -> - if v.[0] = 'N' || (String.length v > 3 && String.sub v 0 3 = "pre") - then forgetvar x v else x) - x x.evars in - IN (VMap.map (fun v -> ND.var_itv v id) x.value) - else - let all = List.fold_left (fun a b -> SSet.add b a) SSet.empty - (List.assoc id x.evars) in - IE - (VMap.fold - (fun enum _ s -> - try SSet.add (VarMap.find id enum) s - with Not_found -> all) - x.value - SSet.empty) - - let set_disjunct x id p = - { x with - disj_v = (if p = DAlways then id::x.disj_v - else List.filter ((<>) id) x.disj_v); - nodisj_v = (if p = DNever then id::x.nodisj_v - else List.filter ((<>) id) x.nodisj_v); - } - - let join x y = - VMap.fold - (fun enum num value -> add_case value (enum, num)) - y.value - x - let meet x y = not_implemented "meet for enum+num domain" - let widen x y = - let value = VMap.merge - (fun _ a b -> match a, b with - | Some x, None -> Some x - | None, Some y -> Some y - | Some x, Some y -> Some (ND.widen x y) - | _ -> None) - x.value y.value - in { x with value = value } - - (* Some cases of subset/equality not detected *) - let subset a b = - VMap.for_all - (fun enum num -> - VMap.exists - (fun enum_b num_b -> - Valuation.subset enum enum_b && ND.subset num num_b) - b.value) - a.value - let eq a b = subset a b && subset b a - - (* Constraints ! *) - let apply_ec x (op, a, b) = - VMap.fold - (fun enum num value -> - match a, b with - | i, EItem u -> - begin try let v = VarMap.find i enum in - if (if op = E_EQ then u = v else u <> v) - then add_case value (enum, num) - else value - with Not_found -> - if op = E_EQ - then add_case value (VarMap.add i u enum, num) - else (* MAKE A DISJUNCTION *) - List.fold_left - (fun value item -> - add_case value (VarMap.add i item enum, num)) - value - (List.filter ((<>) u) (List.assoc i x.evars)) - end - | i, EIdent j -> - begin - try let x = VarMap.find i enum in - try let y = VarMap.find j enum in - if (if op = E_EQ then x = y else x <> y) - then add_case value (enum, num) - else value - with Not_found (* J not found *) -> - add_case value (VarMap.add j x enum, num) - with Not_found (* I not found *) -> - try let y = VarMap.find j enum in - add_case value (VarMap.add i y enum, num) - with Not_found (* J not found *) -> - if op = E_EQ - then (* MAKE A DISJUNCTION ! *) - List.fold_left - (fun value item -> - let enum = VarMap.add i item enum in - let enum = VarMap.add j item enum in - add_case value (enum, num)) - value - (List.assoc i x.evars) - else - add_case value (enum, num) - end) - x.value - { x with value = VMap.empty } - - let apply_ecl x cons = - let f x = List.fold_left apply_ec x cons in - fix eq f x - - - let apply_ncl x econs = - { x with value = strict @@ VMap.map (fun x -> ND.apply_ncl x econs) x.value } - - let rec apply_cl x (econs, ncons, rest) = match rest with - | CLTrue -> - let y = apply_ecl x econs in - let z = apply_ncl y ncons in - z - | CLFalse -> vbottom x - | CLAnd(a, b) -> - let y = apply_cl x (econs, ncons, a) in - apply_cl y (econs, ncons, b) - | CLOr((eca, ca, ra), (ecb, cb, rb)) -> - let y = apply_cl x (econs@eca, ncons@ca, ra) in - let z = apply_cl x (econs@ecb, ncons@cb, rb) in - join y z - - let apply_f x f = apply_cl x (conslist_of_f f) - - let assign x e = - let ee, ne = List.partition (fun (id, id2) -> List.mem_assoc id x.evars) e in - let ne_e = List.map (fun (id, id2) -> id, NIdent id2) ne in - - VMap.fold - (fun enum0 num value -> - let enum = List.fold_left - (fun enum (id, id2) -> - try let y = VarMap.find id2 enum0 in - VarMap.add id y enum - with Not_found -> - VarMap.remove id enum) - enum0 ee - in - add_case value (enum, ND.assign num ne_e)) - x.value - { x with value = VMap.empty } - - let print_all fmt x = - Format.fprintf fmt "@[<v>"; - VMap.iter - (fun enum num -> - Format.fprintf fmt "@[<hv 2>{ %a ∧@ %a }@]@ " - Valuation.print enum ND.print_all num) - x.value; - Format.fprintf fmt "@]" - - let print_vars fmt x idl = print_all fmt x (* TODO *) - - let print_itv fmt = function - | IN x -> - Format.fprintf fmt "@[<v 0>"; - VMap.iter - (fun enum i -> - Format.fprintf fmt "%a when %a@ " - ND.print_itv i Valuation.print enum) - x; - Format.fprintf fmt "@]" - | IE x -> - Format.fprintf fmt "@[<hov 2>{ "; - SSet.iter (fun x -> Format.fprintf fmt "%s@ " x) x; - Format.fprintf fmt "}@]" - -end diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index a610843..8d5f1c9 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -4,42 +4,244 @@ open Formula open Typing open Util -open Abs_domain open Num_domain +open Enum_domain -module I (E : ENVIRONMENT_DOMAIN) : sig + +module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig type st - val do_prog : int -> rooted_prog -> unit + val do_prog : int -> (id -> bool) -> rooted_prog -> unit end = struct + (* ************************** + Disjunction domain + ************************** *) + + type case_v = ED.t * ND.t + type case = ED.item list + + type dd_v = { + d_vars : id list; + data : (case, case_v) Hashtbl.t; + } + + (* + print_dd : Formatter.t -> dd_v -> unit + *) + let print_aux fmt d_vars env = + let print_it q (enum, num) = + Format.fprintf fmt "@[<hov 4>"; + List.iter2 + (fun id v -> Format.fprintf fmt "%a ≡ %s,@ " + Formula_printer.print_id id v) + d_vars q; + Format.fprintf fmt "@ %a,@ %a@]@." + ED.print enum ND.print num; + in + Hashtbl.iter print_it env + let print_dd fmt dd = print_aux fmt dd.d_vars dd.data + + + (* + dd_bot : id list -> dd_v + *) + let dd_bot d_vars = { d_vars; data = Hashtbl.create 12 } + + (* + dd_add_case : dd_v -> case_v -> unit + *) + let dd_add_case env (enum, num) = + let rec aux enum vals = function + | [] -> + let case = List.rev vals in + begin try let e0, n0 = Hashtbl.find env.data case in + Hashtbl.replace env.data case (ED.join enum e0, ND.join num n0); + with Not_found -> + Hashtbl.add env.data case (enum, num); + end + | p::q -> + List.iter + (fun v -> match ED.apply_cons enum (E_EQ, p, EItem v) with + | [en] -> aux en (v::vals) q + | _ -> assert false) + (ED.project enum p) + in aux enum [] env.d_vars + + (* + dd_singleton : id list -> case_v -> dd_v + *) + let dd_singleton d_vars d = + let v = { d_vars; data = Hashtbl.create 1 } in + dd_add_case v d; + v + + (* + dd_extract_case : dd_v -> case -> dd_v + *) + let dd_extract_case v case = + try dd_singleton v.d_vars (Hashtbl.find v.data case) + with Not_found -> dd_bot v.d_vars + + + (* + dd_apply_ncons : dd_v -> num_cons list -> dd_v + *) + let dd_apply_ncl v ncl = + let vv = dd_bot v.d_vars in + Hashtbl.iter (fun case (enum, num) -> + let num = ND.apply_cl num ncl in + if not (ND.is_bot num) then + Hashtbl.add vv.data case (enum, num)) + v.data; + vv + + (* + dd_apply_econs : dd_v -> enum_cons -> dd_v + *) + let dd_apply_econs v cons = + let vv = dd_bot v.d_vars in + Hashtbl.iter (fun case (enum, num) -> + List.iter + (fun enum -> dd_add_case vv (enum, num)) + (ED.apply_cons enum cons)) + v.data; + vv + + (* + dd_join : dd_v -> dd_v -> dd_v + *) + let dd_join a b = + let vv = { d_vars = a.d_vars; data = Hashtbl.copy a.data } in + Hashtbl.iter (fun case (enum, num) -> + try let e2, n2 = Hashtbl.find vv.data case in + Hashtbl.replace vv.data case (ED.join e2 enum, ND.join n2 num) + with Not_found -> Hashtbl.replace vv.data case (enum, num)) + b.data; + vv + + (* + dd_meet : dd_v -> dd_v -> dd_v + *) + let dd_meet a b = + let vv = dd_bot a.d_vars in + Hashtbl.iter (fun case (enum, num) -> + try let e2, n2 = Hashtbl.find b.data case in + let en, nn = ED.meet enum e2, ND.meet n2 num in + if not (ND.is_bot nn) then Hashtbl.add vv.data case (en, nn) + with _ -> ()) + a.data; + vv + + (* + dd_apply_cl : dd_v -> conslist -> dd_v + *) + let rec apply_cl env (ec, nc, r) = + match r with + | CLTrue -> + let env_ec = List.fold_left dd_apply_econs env ec in + let env_nc = dd_apply_ncl env_ec nc in + (* Format.printf "[[ %a -> %a ]]@." + print_dd env print_dd env_nc; *) + env_nc + | CLFalse -> dd_bot env.d_vars + | CLAnd(a, b) -> + let env = apply_cl env (ec, nc, a) in + apply_cl env (ec, nc, b) + | CLOr((eca, nca, ra), (ecb, ncb, rb)) -> + dd_join (apply_cl env (ec@eca, nc@nca, ra)) + (apply_cl env (ec@ecb, nc@ncb, rb)) + + + (* *************************** + Abstract interpretation + *************************** *) + type st = { rp : rooted_prog; widen_delay : int; - env : E.t; + + enum_vars : (id * ED.item list) list; + num_vars : (id * bool) list; + + (* program expressions *) f : bool_expr; cl : conslist; f_g : bool_expr; cl_g : conslist; guarantees : (id * bool_expr) list; + + (* abstract interpretation *) + cycle : (id * id * typ) list; (* s'(x) = s(y) *) + forget : (id * typ) list; (* s'(x) not specified *) + d_vars : id list; (* disjunction variables *) + top : case_v; + env : (case, case_v) Hashtbl.t; + mutable delta : case list; + widen : (case, int) Hashtbl.t; } + (* + print_st : Formatter.t -> st -> unit + *) + let print_st fmt st = print_aux fmt st.d_vars st.env - (* init state *) - let init_state widen_delay rp = - let env = List.fold_left - (fun env (_, id, ty) -> E.addvar env id ty) - E.init - rp.all_vars - in + (* + add_case : st -> case_v -> unit + *) + let add_case st (enum, num) = + let rec aux enum vals = function + | [] -> + let case = List.rev vals in + begin try let e0, n0 = Hashtbl.find st.env case in + if (not (ED.subset enum e0)) || (not (ND.subset num n0)) then begin + begin try + let n = Hashtbl.find st.widen case in + let jw = if n < st.widen_delay then ND.join else ND.widen in + Hashtbl.replace st.env case (ED.join e0 enum, jw n0 num); + Hashtbl.replace st.widen case (n+1); + with Not_found -> + Hashtbl.replace st.env case (ED.join enum e0, ND.join num n0); + Hashtbl.add st.widen case 0; + end; + if not (List.mem case st.delta) then st.delta <- case::st.delta + end + with Not_found -> + Hashtbl.add st.env case (enum, num); + if not (List.mem case st.delta) then st.delta <- case::st.delta + end + | p::q -> + List.iter + (fun v -> match ED.apply_cons enum (E_EQ, p, EItem v) with + | [en] -> aux en (v::vals) q + | _ -> assert false) + (ED.project enum p) + in aux enum [] st.d_vars + + + + (* + init_state : int -> rooted_prog -> st + *) + let init_state widen_delay disj rp = Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_typed_var ", ") rp.all_vars; + let enum_vars = List.fold_left + (fun v (_, id, t) -> match t with + | TEnum ch -> (id, ch)::v | _ -> v) + [] rp.all_vars in + let num_vars = List.fold_left + (fun v (_, id, t) -> match t with + | TInt -> (id, false)::v | TReal -> (id, true)::v | _ -> v) + [] rp.all_vars in + let init_f = Transform.init_f_of_prog rp in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; + let init_cl = conslist_of_f init_f in let guarantees = Transform.guarantees_of_prog rp in Format.printf "Guarantees:@."; @@ -51,96 +253,192 @@ end = struct let f = Formula.eliminate_not (Transform.f_of_prog rp false) in let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; - Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g; - - let env = E.set_disjunct env "/exit" DNever in - let env = E.apply_f env init_f in + Format.printf "Cycle formula with guarantees:@.%a@.@." + Formula_printer.print_expr f_g; let cl = Formula.conslist_of_f f in let cl_g = Formula.conslist_of_f f_g in - { rp; widen_delay; - f; cl; f_g; cl_g; - guarantees; env } - - (* - pass_cycle : var_def list -> E.t -> E.t - - Does : - - x <- Nx, for all x - - ignore x for all x such that Nx does not exist - *) - let pass_cycle vars e = - let tr_assigns = List.fold_left - (fun q (_, id, _) -> + (* calculate cycle variables and forget variables *) + let cycle = List.fold_left + (fun q (_, id, ty) -> if id.[0] = 'N' then - (String.sub id 1 (String.length id - 1), id)::q - else - q) - [] vars + (String.sub id 1 (String.length id - 1), id, ty)::q + else q) + [] rp.all_vars in - let e = E.assign e tr_assigns in - - let forget_vars = List.map (fun (_, id, _) -> id) + let forget = List.map (fun (_, id, ty) -> (id, ty)) (List.filter - (fun (_, id, _) -> - not (List.exists (fun (_, id2, _) -> id2 = "N"^id) vars)) - vars) in - let e = List.fold_left E.forgetvar e forget_vars in - e + (fun (_, id, _) -> + not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars)) + rp.all_vars) + in + + (* calculate disjunction variables *) + (* first approximation : use all enum variables appearing in init formula *) + let rec calculate_dvars (ec, _, r) = + let a = List.map (fun (_, id, _) -> id) ec in + let rec aux = function + | CLTrue | CLFalse -> [] + | CLAnd(u, v) -> + aux u @ aux v + | CLOr(u, v) -> + calculate_dvars u @ calculate_dvars v + in a @ aux r + in + let d_vars_0 = calculate_dvars init_cl in + let d_vars_1 = List.filter + (fun id -> disj id && not (List.mem id d_vars_0) && id.[0] <> 'N') + (List.map (fun (id, _) -> id) enum_vars) in + let d_vars = d_vars_0 @ d_vars_1 in + + (* setup abstract data *) + let top = ED.top enum_vars, ND.top num_vars in + let delta = [] in + let widen = Hashtbl.create 12 in + (* calculate initial state and environment *) + let init_s = dd_bot d_vars in + + let init_ec, _, _ = init_cl in + let init_ed = List.fold_left + (fun ed cons -> + List.flatten (List.map (fun x -> ED.apply_cons x cons) ed)) + [ED.top enum_vars] (init_ec) in + List.iter (fun ed -> dd_add_case init_s (ed, ND.top num_vars)) init_ed; + let env_dd = apply_cl init_s init_cl in + let env = env_dd.data in + + let st = + { rp; widen_delay; enum_vars; num_vars; + f; cl; f_g; cl_g; guarantees; + cycle; forget; d_vars; top; + env; delta; widen } in + + Hashtbl.iter (fun case _ -> st.delta <- case::st.delta) st.env; + + st - (* cycle : st -> cl -> env -> env *) - let cycle st cl i = - (pass_cycle st.rp.all_vars (E.apply_cl i cl)) (* - loop : st -> env -> env -> env + pass_cycle : st -> case_v -> case_v *) - let loop st acc0 = + let pass_cycle st (enum, num) = + let assign_e = + List.map (fun (a, b, _) -> a, b) + (List.filter + (fun (_, _, t) -> match t with TEnum _ -> true | _ -> false) + st.cycle) in + let assign_n = + List.map (fun (a, b, _) -> a, NIdent b) + (List.filter + (fun (_, _, t) -> match t with TInt | TReal -> true | _ -> false) + st.cycle) in - Format.printf "Loop @[<hv>%a@]@.@." - Formula_printer.print_conslist st.cl; + let enum = ED.assign enum assign_e in + let num = ND.assign num assign_n in - let fsharp cl i = - Format.printf "Acc @[<hv>%a@]@." E.print_all i; - let j = cycle st cl i in - E.join acc0 j - in + List.fold_left + (fun (enum, num) (var, t) -> match t with + | TEnum _ -> ED.forgetvar enum var, num + | TReal | TInt -> enum, ND.forgetvar num var) + (enum, num) st.forget - let rec iter n i = - let i' = - if n < st.widen_delay - then E.join i (fsharp st.cl i) - else E.widen i (fsharp st.cl_g i) - in - if E.eq i i' then i else iter (n+1) i' - in + let dd_pass_cycle st (v : dd_v) = + let vv = dd_bot v.d_vars in + Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data; + vv + + (* + cycle : st -> cl -> dd_v -> dd_v + *) + let cycle st cl env = + let env_f = apply_cl env cl in + (* Format.printf "{{ %a ->@.%a }}@." print_dd env print_dd env_f; *) + dd_pass_cycle st env_f - let x = iter 0 acc0 in - let y = fix E.eq (fsharp st.cl) x in (* decreasing iteration *) - let z = E.apply_cl y st.cl in (* no more guarantee *) - y, z + + (* + set_target_case : st -> dd_v -> case -> dd_v + *) + let set_target_case st env case = + List.fold_left2 + (fun env id v -> + if List.exists (fun (id2, _) -> id2 = "N"^id) st.enum_vars then + dd_apply_econs env (E_EQ, "N"^id, EItem v) + else env) + env st.d_vars case (* do_prog : rooted_prog -> unit *) - let do_prog widen_delay rp = - let st = init_state widen_delay rp in + let do_prog widen_delay disj rp = + let st = init_state widen_delay disj rp in + + Format.printf "Init: %a@." print_st st; + + let n_ch_iter = ref 0 in - let final_nc, final = loop st st.env in + (* chaotic iteration loop *) + while st.delta <> [] do + let case = List.hd st.delta in + + incr n_ch_iter; + Format.printf "Chaotic iteration %d: @[<hov>[%a]@]@." + !n_ch_iter + (Ast_printer.print_list Formula_printer.print_id ", ") case; + + let start = try Hashtbl.find st.env case with Not_found -> assert false in + let start_dd = dd_singleton st.d_vars start in + let f i = + let i = dd_singleton st.d_vars i in + let i' = set_target_case st i case in + let q = dd_join start_dd (cycle st st.cl i') in + try Hashtbl.find q.data case with Not_found -> assert false + in + + let rec iter n (i_enum, i_num) = + let fi_enum, fi_num = f (i_enum, i_num) in + let j_enum, j_num = + if n < st.widen_delay then + ED.join i_enum fi_enum, ND.join i_num fi_num + else + ED.join i_enum fi_enum, ND.widen i_num fi_num + in + if ED.eq j_enum i_enum && ND.eq j_num i_num + then (i_enum, i_num) + else iter (n+1) (j_enum, j_num) + in + let y = iter 0 start in + let z = fix (fun (a, b) (c, d) -> ED.eq a c && ND.eq b d) f y in + + let i = dd_singleton st.d_vars z in + let j = cycle st st.cl i in + let cases = ref [] in + Hashtbl.iter (fun case _ -> cases := case::(!cases)) j.data; + List.iter + (fun case -> + let i' = set_target_case st i case in + let j = cycle st st.cl i' in + Hashtbl.iter (fun _ q -> add_case st q) j.data) + !cases; + + st.delta <- List.filter ((<>) case) st.delta; + + (* Format.printf "Final: %a@." print_st st; *) + + done; + + let final = apply_cl { d_vars = st.d_vars; data = st.env } st.cl in + Format.printf "Accessible: %a@." print_dd final; - Format.printf "@[<hov>F %a@]@.@." - E.print_all final_nc; - Format.printf "@[<hov>F' %a@]@.@." - E.print_all final; let check_guarantee (id, f) = let cl = Formula.conslist_of_f f in Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ " id Formula_printer.print_conslist cl; - let z = E.apply_cl final cl in - if E.is_bot z then + let z = apply_cl final cl in + if Hashtbl.length z.data = 0 then Format.printf "OK@]@ " else Format.printf "FAIL@]@ " @@ -153,12 +451,26 @@ end = struct if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin Format.printf "Probes: @[<v 0>"; - List.iter (fun (p, id, _) -> - if p then Format.printf "%a ∊ %a@ " - Formula_printer.print_id id - E.print_itv (E.var_itv final id)) + List.iter (fun (p, id, ty) -> + if p then begin + Format.printf "%a ∊ @[<v>" Formula_printer.print_id id; + Hashtbl.iter (fun case (enum, num) -> + begin match ty with + | TInt | TReal -> + Format.printf "%a" ND.print_itv (ND.project num id) + | TEnum _ -> + Format.printf "@[<hov>{ %a }@]" + (Ast_printer.print_list Formula_printer.print_id ", ") + (ED.project enum id) + end; + Format.printf " when @[<hov>[%a]@]@ " + (Ast_printer.print_list Formula_printer.print_id ", ") case) + final.data; + Format.printf "@]@ " + end) st.rp.all_vars; Format.printf "@]@." end end + diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index 369f4b7..7a823db 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -58,27 +58,23 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op (* implementation *) - let init = Abstract1.top manager (Environment.make [||] [||]) - let bottom = Abstract1.bottom manager (Environment.make [||] [||]) + let v_env vars = + let intv = List.map + (fun (s, _) -> Var.of_string s) + (List.filter (fun (_, n) -> not n) vars) in + let realv = List.map + (fun (s, _) -> Var.of_string s) + (List.filter (fun (_, n) -> n) vars) in + (Environment.make (Array.of_list intv) (Array.of_list realv)) + + let top vars = + Abstract1.top manager (v_env vars) + let bottom vars = Abstract1.bottom manager (v_env vars) let is_bot = Abstract1.is_bottom manager - let addvar x id isfloat = - let env = Abstract1.env x in - let env2 = if isfloat then - Environment.add env [||] [| Var.of_string id |] - else - Environment.add env [| Var.of_string id |] [||] - in - Abstract1.change_environment manager x env2 false let forgetvar x id = let v = [| Var.of_string id |] in Abstract1.forget_array manager x v false - let rmvar x id = - let v = [| Var.of_string id |] in - let env = Abstract1.env x in - let env2 = Environment.remove env v in - let y = Abstract1.forget_array manager x v false in - Abstract1.change_environment manager y env2 false let vars x = let (ivt, fvt) = Environment.vars (Abstract1.env x) in @@ -89,17 +85,19 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct let vbottom x = Abstract1.bottom manager (Abstract1.env x) - let var_itv x id = + let project x id = Abstract1.bound_variable manager x (Var.of_string id) (* Apply some formula to the environment *) - let rec apply_ncl x cons = + let apply_cl x cons = let env = Abstract1.env x in let tca = Array.of_list (List.map (tcons_of_cons env) cons) in let ar = Tcons1.array_make env (Array.length tca) in Array.iteri (Tcons1.array_set ar) tca; Abstract1.meet_tcons_array manager x ar + let apply_cons x cons = apply_cl x [cons] + let assign x eqs = let env = Abstract1.env x in @@ -119,7 +117,7 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct let eq = Abstract1.is_eq manager (* Pretty-printing *) - let print_all fmt x = + let print fmt x = Abstract1.minimize manager x; Abstract1.print fmt x; Format.fprintf fmt "@?" @@ -130,7 +128,7 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct let rm_vars = Array.of_list (List.map (fun (id, _) -> Var.of_string id) rm_vars_l) in let xx = Abstract1.forget_array manager x rm_vars false in - print_all fmt xx + print fmt xx let print_itv = Interval.print diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml new file mode 100644 index 0000000..c8b4ec5 --- /dev/null +++ b/abstract/enum_domain.ml @@ -0,0 +1,144 @@ +open Ast +open Formula +open Util + +exception Bot + +module type ENUM_ENVIRONMENT_DOMAIN = sig + type t + + type item = string + + (* construction *) + val top : (id * item list) list -> t + + (* variable management *) + val vars : t -> (id * item list) list + + val forgetvar : t -> id -> t + val project : t -> id -> item list + + (* set-theoretic operations *) + val join : t -> t -> t (* union *) + val meet : t -> t -> t (* intersection, may raise Bot *) + + val subset : t -> t -> bool + val eq : t -> t -> bool + + (* abstract operations *) + val apply_cons : t -> enum_cons -> t list (* may disjunct *) + val assign : t -> (id * id) list -> t + + (* pretty-printing *) + val print : Format.formatter -> t -> unit +end + + + +module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct + type item = string + + type t = { + vars : (id * item list) list; + value : item VarMap.t; + } + + 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 when a = b -> Some a + | _ -> 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 -> if a = b then Some a else raise Bot + | _ -> None) + x1.value x2.value in + { x1 with value = v } + + let subset a b = + VarMap.for_all + (fun id v -> + try v = VarMap.find id b.value + with Not_found -> true) + a.value + let eq a b = + VarMap.equal (=) a.value b.value + + let cc op = match op with + | E_EQ -> (=) + | E_NE -> (<>) + + let apply_cons x (op, id, e) = + match e with + | EItem s -> + begin try let t = VarMap.find id x.value in + if cc op s t then [x] else [] + with Not_found -> + List.map (fun v -> { x with value = VarMap.add id v x.value }) + (List.filter (cc op s) (List.assoc id x.vars)) + end + | EIdent id2 -> + match + (try Some (VarMap.find id x.value) with _ -> None), + (try Some (VarMap.find id2 x.value) with _ -> None) + with + | None, None -> [x] + | None, Some s -> + List.map (fun v -> { x with value = VarMap.add id v x.value}) + (List.filter (cc op s) (List.assoc id x.vars)) + | Some s, None -> + List.map (fun v -> { x with value = VarMap.add id2 v x.value}) + (List.filter (cc op s) (List.assoc id2 x.vars)) + | Some s, Some t -> + if cc op s t then [x] else [] + + 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 -> + begin match bl q with + | (vv, ids)::q when vv = v -> (v, id::ids)::q + | r -> (v, [id])::r + end + 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; + Format.fprintf fmt " ≡ %s@]" v) + sbl; + Format.fprintf fmt " }@]" + +end diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index 92d00a2..084e397 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -10,6 +10,8 @@ module VD : VALUE_DOMAIN = struct | Int a, Int b -> a <= b | x, y -> x = y + let bound_lt a b = not (bound_leq b a) (* a < b *) + let bound_add a b = match a, b with | MInf, Int a | Int a, MInf -> MInf @@ -77,7 +79,7 @@ module VD : VALUE_DOMAIN = struct let subset a b = match a, b with | Bot, _ -> true | _, Bot -> false - | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b + | Itv(a, b), Itv(c, d) -> bound_leq c a && bound_leq b d let join a b = match a, b with | Bot, x | x, Bot -> x @@ -96,12 +98,12 @@ module VD : VALUE_DOMAIN = struct | x, Bot | Bot, x -> x | Itv(a, b), Itv(c, d) -> let lb = - if not (bound_leq a c) then + if bound_lt c a then (if bound_leq (Int 0) c then Int 0 else MInf) else a in let ub = - if not (bound_leq d b) then + if bound_lt b d then (if bound_leq d (Int 0) then Int 0 else PInf) else b in diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 6497760..3e978ce 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -15,8 +15,11 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct type t = Env of env | Bot type itv = Value_domain.itv - let init = Env VarMap.empty - let bottom = Bot + let top vars = Env + (List.fold_left + (fun e (v, _) -> VarMap.add v V.top e) + VarMap.empty vars) + let bottom _ = Bot let get_var env id = try VarMap.find id env @@ -55,16 +58,14 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | Bot -> true | Env env -> strict env = Bot - let addvar x id _ = strict_apply (fun y -> Env (VarMap.add id V.top y)) x let forgetvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x - let rmvar x id = strict_apply (fun y -> Env (VarMap.remove id y)) x let vars env = match env with | Bot -> [] | Env env -> List.map (fun (k, _) -> (k, false)) (VarMap.bindings env) - let vbottom _ = bottom + let vbottom _ = Bot - let var_itv x id = match x with + let project x id = match x with | Bot -> Value_domain.Bot | Env env -> V.to_itv (get_var env id) @@ -95,16 +96,20 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | Bot, x -> true | Env _, Bot -> false | Env m, Env n -> - VarMap.for_all2o - (fun _ _ -> true) - (fun _ v -> v = V.top) - (fun _ a b -> V.subset a b) - m n + VarMap.for_all + (fun id vn -> + try let vm = VarMap.find id m in V.subset vm vn + with Not_found -> vn = V.top) + n let eq a b = match a, b with | Bot, Bot -> true | Env m, Env n -> - VarMap.equal (=) m n + VarMap.for_all2o + (fun _ v -> v = V.top) + (fun _ v -> v = V.top) + (fun _ a b -> a = b) + m n | _ -> false (* Apply some formula to the environment *) @@ -163,7 +168,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct List.fold_left restrict_var env (extract_var (expr, zop, NIntConst 0)) - let apply_ncl x cl = + let apply_cl x cl = let f x = List.fold_left apply_cons x cl in fix eq f x @@ -212,7 +217,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct sbl; Format.fprintf fmt " }@]" - let print_all fmt x = + let print fmt x = print_vars fmt x (List.map fst (vars x)) let print_itv fmt x = diff --git a/abstract/num_domain.ml b/abstract/num_domain.ml index 59ed1a0..96de8bc 100644 --- a/abstract/num_domain.ml +++ b/abstract/num_domain.ml @@ -6,18 +6,16 @@ module type NUMERICAL_ENVIRONMENT_DOMAIN = sig type itv (* construction *) - val init : t - val bottom : t - val vbottom : t -> t (* bottom value with same environment *) + val top : (id * bool) list -> t + val bottom : (id * bool) list -> t + val vbottom : t -> t (* bottom value with same variables *) val is_bot : t -> bool (* variable management *) - val addvar : t -> id -> bool -> t (* integer or real variable ? *) - val rmvar : t -> id -> t val vars : t -> (id * bool) list val forgetvar : t -> id -> t (* remove var from constraints *) - val var_itv : t -> id -> itv + val project : t -> id -> itv (* set-theoretic operations *) val join : t -> t -> t (* union *) @@ -29,12 +27,13 @@ module type NUMERICAL_ENVIRONMENT_DOMAIN = sig val eq : t -> t -> bool (* abstract operation *) - val apply_ncl : t -> num_cons list -> t + val apply_cons : t -> num_cons -> t + val apply_cl : t -> num_cons list -> t val assign : t -> (id * num_expr) list -> t (* pretty-printing *) + val print : Format.formatter -> t -> unit val print_vars : Format.formatter -> t -> id list -> unit - val print_all : Format.formatter -> t -> unit val print_itv : Format.formatter -> itv -> unit end diff --git a/abstract/transform.ml b/abstract/transform.ml index b6781a8..82b6731 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -70,7 +70,7 @@ let rec f_of_neexpr td (node, prefix) where expr = | TEnum _ -> EE(EIdent x)) typ) | AST_arrow(a, b) -> - if List.mem (node^"/") td.rp.init_scope + if td.rp.init_scope (node^"/") then f_or (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true)) @@ -306,21 +306,21 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = let time_incr_eq = if active then f_and - (if not (List.mem (node^"/") td.rp.no_time_scope) + (if not (td.rp.no_time_scope (node^"/")) then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time"))) else BConst true) - (if List.mem (node^"/") td.rp.init_scope + (if td.rp.init_scope (node^"/") then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false) else BConst true) else f_and - (if not (List.mem (node^"/") td.rp.no_time_scope) + (if not (td.rp.no_time_scope (node^"/")) then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), NIdent(node^"/"^prefix^"time")) else BConst true) - (if List.mem (node^"/") td.rp.init_scope + (if td.rp.init_scope (node^"/") then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EIdent (node^"/"^prefix^"init")) else BConst true) @@ -373,13 +373,13 @@ let rec init_f_of_scope rp (node, prefix, eqs) = in let time_eq = f_and - (if not (List.mem (node^"/") rp.no_time_scope) + (if not (rp.no_time_scope (node^"/")) then BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0) else BConst true) - (if List.mem (node^"/") rp.init_scope + (if rp.init_scope (node^"/") then f_e_eq (EIdent(node^"/"^prefix^"init")) (EItem bool_true) else BConst true) |