diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_domain.ml | 308 | ||||
| -rw-r--r-- | abstract/abs_interp.ml | 37 | ||||
| -rw-r--r-- | abstract/formula_printer.ml | 2 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 2 | ||||
| -rw-r--r-- | abstract/transform.ml | 63 |
5 files changed, 363 insertions, 49 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml index a7f5455..a30713a 100644 --- a/abstract/abs_domain.ml +++ b/abstract/abs_domain.ml @@ -4,6 +4,11 @@ open Num_domain open Typing open Util +type disjunct_policy = + | DAlways + | DNever + | DSometimes + module type ENVIRONMENT_DOMAIN = sig type t type itv @@ -21,6 +26,7 @@ module type ENVIRONMENT_DOMAIN = sig 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 *) @@ -33,7 +39,7 @@ module type ENVIRONMENT_DOMAIN = sig (* abstract operations *) val apply_f : t -> bool_expr -> t val apply_cl : t -> conslist -> t - val assign : t -> (id * num_expr) list -> t + val assign : t -> (id * id) list -> t (* pretty-printing *) val print_vars : Format.formatter -> t -> id list -> unit @@ -42,19 +48,13 @@ module type ENVIRONMENT_DOMAIN = sig end -module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct - - type enum_valuation = (string * string) list - - module VMapKey = struct - type t = enum_valuation VarMap.t - let compare = VarMap.compare (fun a b -> Pervasives.compare (List.sort Pervasives.compare a) (List.sort Pervasives.compare b)) - end - module VMap = Mapext.Make(VMapKey) +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 @@ -66,6 +66,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let forgetvar = ND.forgetvar let var_itv = ND.var_itv + let set_disjunct x _ _ = x let join = ND.join let meet = ND.meet @@ -88,10 +89,295 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let apply_f x f = apply_cl x (conslist_of_f f) - let assign = ND.assign + 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 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 (ND.join num (VMap.find enum value)) value + with Not_found -> VMap.add enum num value + in { x with value = v } + + 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 IN (VMap.map (fun v -> ND.var_itv v id) x.value) + else not_implemented "var_itv for enum variable" + + 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)) + x.value + y + let meet x y = not_implemented "meet for enum+num domain" + let widen x y = + { x with + value = VMap.merge + (fun _ a b -> match a, b with + | None, Some a -> Some a + | Some a, None -> Some a + | Some a, Some b -> Some (ND.widen a b) + | _ -> assert false) + x.value y.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 + | EItem x, EItem y -> + if (x = y && op = E_EQ) || (x <> y && op = E_NE) + then add_case value (enum, num) + else value + | EItem u, EIdent i | EIdent i, EItem u -> + begin try let y = VarMap.find i enum in + if (u = y && op = E_EQ) || (u <> y && op = E_NE) + 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 + | EIdent i, EIdent j -> + begin + try let x = VarMap.find i enum in + try let y = VarMap.find j enum in + if (x = y && op = E_EQ) || (x <> y && op = E_NE) + 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 0>"; + 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 7950144..7a53134 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -52,6 +52,7 @@ end = struct guarantees; Format.printf "@."; + let env = E.set_disjunct env "/exit" DNever in let env = E.apply_f env init_f in let cl = Formula.conslist_of_f f in @@ -72,7 +73,7 @@ end = struct let tr_assigns = List.fold_left (fun q (_, id, _) -> if id.[0] = 'N' then - (String.sub id 1 (String.length id - 1), NIdent id)::q + (String.sub id 1 (String.length id - 1), id)::q else q) [] vars @@ -95,14 +96,10 @@ end = struct (* loop : st -> env -> env -> env *) - let loop st pnew stay = + let loop st acc0 = - Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@." - Formula_printer.print_conslist st.cl - E.print_all pnew E.print_all stay; - - let add_stay = cycle st st.cl pnew in - let acc0 = E.join stay add_stay in + Format.printf "Loop @[<hv>%a@]@.@." + Formula_printer.print_conslist st.cl; let fsharp cl i = Format.printf "Acc @[<hv>%a@]@." E.print_all i; @@ -121,7 +118,7 @@ end = struct let x = iter 0 acc0 in let y = fix E.eq (fsharp st.cl_g) x in (* decreasing iteration *) - let z = E.apply_cl y st.cl in + let z = E.apply_cl y st.cl in (* no more guarantee *) y, z (* @@ -130,20 +127,14 @@ end = struct let do_prog widen_delay rp = let st = init_state widen_delay rp in - let pnew = st.env in - let pnew_c = E.apply_cl pnew st.cl in - - let stay, stay_c = loop st pnew (E.vbottom pnew) in - - Format.printf "@.@[<hov>New %a@]@.@." - E.print_all pnew_c; - Format.printf "@[<hov>Stay %a@]@.@." - E.print_all stay_c; - - let final = E.join pnew_c stay_c in + let final, final_c = loop st st.env in - Format.printf "@[<hov>Final %a@]@.@." + Format.printf "@[<hov>F %a@]@.@." E.print_all final; + (* + Format.printf "@[<hov>F' %a@]@.@." + E.print_all final_c; + *) let check_guarantee (id, f) = let cl = Formula.conslist_of_f f in @@ -162,9 +153,9 @@ end = struct end; if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin - Format.printf "Probes:@[<v>"; + Format.printf "Probes: @[<v 0>"; List.iter (fun (p, id, _) -> - if p then Format.printf " %a ∊ %a@ " + if p then Format.printf "%a ∊ %a@ " Formula_printer.print_id id E.print_itv (E.var_itv final id)) st.rp.all_vars; diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml index 44f2d39..0c7d65e 100644 --- a/abstract/formula_printer.ml +++ b/abstract/formula_printer.ml @@ -59,7 +59,7 @@ let rec print_num_expr fmt e = match e with (* Enumeated expressions *) let print_enum_expr fmt = function - | EIdent id -> Format.fprintf fmt "%s" id + | EIdent id -> print_id fmt id | EItem x -> Format.fprintf fmt "%s" x let str_of_enum_op = function diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 492b547..bbdc875 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -188,7 +188,6 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct match env with | Bot -> Format.fprintf fmt "⊥" | Env env -> - Format.fprintf fmt "@[<v 2>{ "; let l = List.map (fun id -> (get_var env id, id)) ids in let s = List.sort Pervasives.compare l in let rec bl = function @@ -201,6 +200,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | _::q -> 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 "@ "; diff --git a/abstract/transform.ml b/abstract/transform.ml index 708456e..64fd8d8 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -70,11 +70,19 @@ let rec f_of_neexpr td (node, prefix) where expr = | TEnum _ -> EE(EIdent x)) typ) | AST_arrow(a, b) -> - f_or - (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) - (sub where a)) - (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1)) - (sub where b)) + if List.mem (node^"/") td.rp.init_scope + then + f_or + (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true)) + (sub where a)) + (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_false)) + (sub where b)) + else + f_or + (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) + (sub where a)) + (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1)) + (sub where b)) (* other *) | AST_if(c, a, b) -> f_or @@ -261,12 +269,33 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = in let time_incr_eq = if active then - BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), - NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time"))) + f_and + (if not (List.mem (node^"/") td.rp.no_time_scope) + then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), + NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time"))) + else BConst true) + (f_and + (if List.mem (node^"/") td.rp.act_scope + then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_true) + else BConst true) + (if List.mem (node^"/") td.rp.init_scope + then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false) + else BConst true)) else - BRel(AST_EQ, - NIdent("N"^node^"/"^prefix^"time"), - NIdent(node^"/"^prefix^"time")) + f_and + (if not (List.mem (node^"/") td.rp.no_time_scope) + then BRel(AST_EQ, + NIdent("N"^node^"/"^prefix^"time"), + NIdent(node^"/"^prefix^"time")) + else BConst true) + (f_and + (if List.mem (node^"/") td.rp.act_scope + then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_false) + else BConst true) + (if List.mem (node^"/") td.rp.init_scope + then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) + (EIdent (node^"/"^prefix^"init")) + else BConst true)) in List.fold_left f_and time_incr_eq @@ -306,9 +335,17 @@ let rec init_f_of_scope rp (node, prefix, eqs) = | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton" in let time_eq = - BRel(AST_EQ, - NIdent(node^"/"^prefix^"time"), - NIntConst 0) + f_and + (if not (List.mem (node^"/") rp.no_time_scope) + then + BRel(AST_EQ, + NIdent(node^"/"^prefix^"time"), + NIntConst 0) + else BConst true) + (if List.mem (node^"/") rp.init_scope + then + f_e_eq (EIdent(node^"/"^prefix^"init")) (EItem bool_true) + else BConst true) in List.fold_left f_and time_eq (List.map do_eq eqs) |