diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp_dynpart.ml | 375 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 28 | ||||
| -rw-r--r-- | abstract/enum_domain.ml | 29 | ||||
| -rw-r--r-- | abstract/enum_domain_edd.ml | 40 | ||||
| -rw-r--r-- | abstract/varenv.ml | 8 |
5 files changed, 433 insertions, 47 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml new file mode 100644 index 0000000..28f9238 --- /dev/null +++ b/abstract/abs_interp_dynpart.ml @@ -0,0 +1,375 @@ +open Ast +open Ast_util +open Formula +open Typing +open Cmdline + +open Util +open Num_domain +open Enum_domain + +open Varenv + +module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) +: sig + + val do_prog : cmdline_opt -> rooted_prog -> unit + +end = struct + + type abs_v = ED.t * ND.t + + type location = { + id : int; + + def : bool_expr list; (* conjunction of formula *) + def_cl : conslist; + is_init : bool; + + f : bool_expr; + cl : conslist; + + (* For chaotic iteration fixpoint *) + mutable star : bool; + mutable in_c : int; + mutable v : abs_v; + + mutable out_t : int list; + mutable in_t : int list; + } + + type env = { + rp : rooted_prog; + opt : cmdline_opt; + + ve : varenv; + + (* program expressions *) + f : bool_expr; + guarantees : (id * bool_expr) list; + + (* data *) + loc : (int, location) Hashtbl.t; + counter : int ref; + } + + (* ************************** + ABSTRACT VALUES + ************************** *) + + (* + top : env -> abs_v + bottom : env -> abs_v + *) + let top e = (ED.top e.ve.evars, ND.top e.ve.nvars) + let bottom e = (ED.top e.ve.evars, ND.bottom e.ve.nvars) + let is_bot (e, n) = ND.is_bot n + + let print_v fmt (enum, num) = + if is_bot (enum, num) then + Format.fprintf fmt "⊥" + else + Format.fprintf fmt "@[<hov 4>(%a,@ %a)@]" ED.print enum ND.print num + + (* + join : abs_v -> abs_v -> abs_v + meet : abs_v -> abs_v -> abs_v + *) + let join (e1, n1) (e2, n2) = + if is_bot (e1, n1) then (e2, n2) + else if is_bot (e2, n2) then (e1, n1) + else (ED.join e1 e2, ND.join n1 n2) + let meet (e1, n1) (e2, n2) = + if is_bot (e1, n1) then ED.vtop e1, ND.vbottom n1 + else if is_bot (e2, n2) then ED.vtop e2, ND.vbottom n2 + else + try (ED.meet e1 e2 , ND.meet n1 n2) + with Bot -> e1, ND.vbottom n1 + + (* + apply_cl : abs_v -> conslist -> abs_v + *) + let rec apply_cl (enum, num) (ec, nc, r) = + try + begin match r with + | CLTrue -> + (ED.apply_cl enum ec, ND.apply_cl num nc) + | CLFalse -> + (enum, ND.vbottom num) + | CLAnd(a, b) -> + let enum, num = apply_cl (enum, num) (ec, nc, a) in + let enum, num = apply_cl (enum, num) ([], nc, b) in + enum, num + | CLOr((eca, nca, ra), (ecb, ncb, rb)) -> + let a = apply_cl (enum, num) (ec@eca, nc@nca, ra) in + let b = apply_cl (enum, num) (ec@ecb, nc@ncb, rb) in + join a b + end + with Bot -> ED.vtop enum, ND.vbottom num + + + (* *************************** + INTERPRET + *************************** *) + + + + (* + init_env : cmdline_opt -> rooted_prog -> env + *) + let init_env opt rp = + let f = Transform.f_of_prog_incl_init rp false in + + let f = simplify_k (get_root_true f) f in + Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f; + + let facts = get_root_true f in + let f, rp, _ = List.fold_left + (fun (f, (rp : rooted_prog), repls) eq -> + match eq with + | BEnumCons(E_EQ, a, EIdent b) + when a.[0] <> 'L' && b.[0] <> 'L' -> + + let a = try List.assoc a repls with Not_found -> a in + let b = try List.assoc b repls with Not_found -> b in + + if a = b then + f, rp, repls + else begin + let keep, repl = + if String.length a <= String.length b + then a, b + else b, a + in + Format.printf "Replacing %s with %s@." repl keep; + let f = formula_replace_evars [repl, keep; "L"^repl, "L"^keep] f in + let rp = + { rp with all_vars = + List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in + let repls = (repl, keep):: + (List.map (fun (r, k) -> r, if k = repl then keep else k) repls) in + f, rp, repls + end + | _ -> f, rp, repls) + (f, rp, []) facts in + + let f = simplify_k (get_root_true f) f in + + Format.printf "Complete formula after simpl:@.%a@.@." + Formula_printer.print_expr f; + + let guarantees = Transform.guarantees_of_prog rp in + Format.printf "Guarantees:@."; + List.iter (fun (id, f) -> + Format.printf " %s: %a@." id Formula_printer.print_expr f) + guarantees; + Format.printf "@."; + + let ve = mk_varenv rp f (conslist_of_f f) in + + let env = { + rp; opt; ve; f; guarantees; + loc = Hashtbl.create 2; counter = ref 2; } in + + (* add initial disjunction : L/must_reset = tt, L/must_reset ≠ tt *) + let rstc = [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] in + let rstf = simplify_k rstc f in + let rstf = simplify_k (get_root_true rstf) rstf in + let nrstc = [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] in + let nrstf = simplify_k nrstc f in + let nrstf = simplify_k (get_root_true nrstf) nrstf in + Hashtbl.add env.loc 0 + { + id = 0; + def = rstc; + def_cl = conslist_of_f (f_and_list rstc); + is_init = true; + + f = rstf; + cl = conslist_of_f rstf; + + star = false; + in_c = 0; + v = (ED.top ve.evars, ND.bottom ve.nvars); + + out_t = []; + in_t = []; + }; + Hashtbl.add env.loc 1 + { + id = 1; + def = nrstc; + def_cl = conslist_of_f (f_and_list nrstc); + is_init = false; + + f = nrstf; + cl = conslist_of_f nrstf; + + star = false; + in_c = 0; + v = (ED.top ve.evars, ND.bottom ve.nvars); + + out_t = []; + in_t = []; + }; + env + + + (* + pass_cycle : env -> edd_v -> edd_v + unpass_cycle : env -> edd_v -> edd_v + + set_target_case : env -> edd_v -> bool_expr -> edd_v + cycle : env -> edd_v -> conslist -> edd_v + *) + let pass_cycle env (enum, num) = + let assign_e, assign_n = List.fold_left + (fun (ae, an) (a, b, t) -> match t with + | TEnum _ -> (a, b)::ae, an + | TInt | TReal -> ae, (a, NIdent b)::an) + ([], []) env.cycle in + + let enum = ED.assign enum assign_e in + let num = ND.assign num assign_n in + + let ef, nf = List.fold_left + (fun (ef, nf) (var, t) -> match t with + | TEnum _ -> var::ef, nf + | TReal | TInt -> ef, var::nf) + ([], []) env.forget in + + (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf) + + let unpass_cycle env (enum, num) = + let assign_e, assign_n = List.fold_left + (fun (ae, an) (a, b, t) -> match t with + | TEnum _ -> (b, a)::ae, an + | TInt | TReal -> ae, (b, NIdent a)::an) + ([], []) env.ve.cycle in + + let enum = ED.assign enum assign_e in + let num = ND.assign num assign_n in + + let ef, nf = List.fold_left + (fun (ef, nf) (var, t) -> match t with + | TEnum _ -> var::ef, nf + | TReal | TInt -> ef, var::nf) + ([], []) env.ve.forget_inv in + + (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf) + + let set_target_case e v cl = + let tgt = (unpass_cycle e (apply_cl (top e) cl)) in + (*Format.printf "Target %a = %a@." Formula_printer.print_conslist cl print_v tgt;*) + meet v tgt + + (* + chaotic_iter : env -> unit + + Fills the values of loc[*].v, and updates out_t and in_t + *) + let chaotic_iter e = + let delta = ref [] in + + (* Fill up initial states *) + Hashtbl.iter + (fun q loc -> + loc.out_t <- []; + loc.in_t <- []; + if loc.is_init then begin + loc.v <- apply_cl (top e) loc.cl; + delta := q::!delta + end else + loc.v <- bottom e) + e.loc; + + (* Iterate *) + let it_counter = ref 0 in + while !delta <> [] do + let s = List.hd !delta in + let loc = Hashtbl.find e.loc s in + + incr it_counter; + Format.printf "@.Iteration %d: q%d@." !it_counter s; + + let start = loc.v in + let f i = + (*Format.printf "I: %a@." print_v i;*) + let i' = set_target_case e i loc.def_cl in + (*Format.printf "I': %a@." print_v i';*) + let j = join start (apply_cl (apply_cl (pass_cycle e.ve i') loc.def_cl) loc.cl) in + (*Format.printf "J: %a@." print_v j;*) + j + 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 ND.is_bot fi_num then + i_enum, i_num + else + if n < e.opt.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 + Format.printf "Fixpoint: %a@." print_v z; + + loc.v <- z; + + Hashtbl.iter + (fun t loc2 -> + let u = pass_cycle e.ve z in + let v = apply_cl u loc2.def_cl in + let w = apply_cl v loc2.cl in + (*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*) + let r_enum, r_num = w in + if not (is_bot (r_enum, r_num)) then begin + Format.printf "%d -> %d with:@. %a@." s t print_v (r_enum, r_num); + if not (List.mem s loc2.in_t) + then loc2.in_t <- s::loc2.in_t; + if not (List.mem t loc.out_t) + then loc.out_t <- t::loc.out_t; + let enum, num = loc2.v in + let enum2, num2 = join (enum, num) (r_enum, r_num) in + if not (ED.subset enum2 enum) || not (ND.subset num2 num) then + begin + loc2.v <- (enum2, num2); + if not (List.mem t !delta) + then delta := t::!delta + end + end) + e.loc; + + delta := List.filter ((<>) s) !delta; + done + + + let print_locs e = + Hashtbl.iter + (fun id loc -> + Format.printf "@."; + Format.printf "q%d: @[<hov 4>[ %a ]@]@." id + (print_list Formula_printer.print_expr " ∧ ") loc.def; + (*Format.printf "F: %a@." Formula_printer.print_conslist loc.cl;*) + Format.printf " @[<hv 0>%a ∧@ %a@]@." + ED.print (fst loc.v) ND.print (snd loc.v); + Format.printf " -> @[<hov>[%a]@]@." + (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t; + ) + e.loc + + let do_prog opt rp = + let e = init_env opt rp in + + Format.printf "@.Initializing.@."; + chaotic_iter e; + print_locs e + +end diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index a439995..23d4734 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -557,7 +557,8 @@ end = struct last_vars = []; all_vars = []; cycle = []; - forget = []; } in + forget = []; + forget_inv = []; } in Hashtbl.add ve.ev_order "x" 0; Hashtbl.add ve.ev_order "y" 1; Hashtbl.add ve.ev_order "z" 2; @@ -755,13 +756,10 @@ end = struct let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in let ef, nf = List.fold_left - (fun (ef, nf) (_, var, t) -> - if var.[0] <> 'N' then - match t with - | TEnum _ -> var::ef, nf - | TReal | TInt -> ef, var::nf - else ef, nf) - ([], []) env.rp.all_vars in + (fun (ef, nf) (var, t) -> match t with + | TEnum _ -> var::ef, nf + | TReal | TInt -> ef, var::nf) + ([], []) env.ve.forget_inv in let v = edd_forget_vars v ef in edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf) @@ -779,8 +777,9 @@ end = struct (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *) (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *) + (* WHY THE **** AM I SHOUTING LIKE THAT ? *) let facts = get_root_true f in - let f, rp, _ = List.fold_left + let f, rp, repls = List.fold_left (fun (f, (rp : rooted_prog), repls) eq -> match eq with | BEnumCons(E_EQ, a, EIdent b) @@ -802,8 +801,12 @@ end = struct let rp = { rp with all_vars = List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in - let repls = (repl, keep):: - (List.map (fun (r, k) -> r, if k = repl then keep else k) repls) in + let repls = (repl, keep; "L"^repl, "L"^keep):: + (List.map + (fun (r, k) -> r, + if k = repl then keep else + if k = "L"^repl then "L"^keep else k) + repls) in f, rp, repls end | _ -> f, rp, repls) @@ -825,6 +828,9 @@ end = struct Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; let guarantees = Transform.guarantees_of_prog rp in + let guarantees = List.map + (fun (id, f) -> id, formula_replace_evars repls f) + guarantees in Format.printf "Guarantees:@."; List.iter (fun (id, f) -> Format.printf " %s: %a@." id Formula_printer.print_expr f) diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml index ea2b053..4f6aacd 100644 --- a/abstract/enum_domain.ml +++ b/abstract/enum_domain.ml @@ -11,11 +11,15 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig (* construction *) val top : (id * item list) list -> t + val bottom : (id * item list) list -> t + val vtop : t -> t (* top with same vars *) + val is_bot : t -> bool (* variable management *) val vars : t -> (id * item list) list val forgetvar : t -> id -> t + val forgetvars : t -> id list -> t val project : t -> id -> item list (* set-theoretic operations *) @@ -27,6 +31,7 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig (* abstract operations *) val apply_cons : t -> enum_cons -> t list (* may disjunct *) + val apply_cl : t -> enum_cons list -> t (* join any disjunction ; may raise Bot *) val assign : t -> (id * id) list -> t (* pretty-printing *) @@ -47,11 +52,15 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct } let top vars = { vars; value = VarMap.empty } + let vtop x = { x with value = VarMap.empty } + let bottom vars = raise Bot (* we don't represent Bot *) + let is_bot x = false let vars x = x.vars let forgetvar x id = { x with value = VarMap.remove id x.value } + let forgetvars = List.fold_left forgetvar let project x id = try [VarMap.find id x.value] with Not_found -> List.assoc id x.vars @@ -108,7 +117,14 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct (List.filter (cc op s) (List.assoc id2 x.vars)) | Some s, Some t -> if cc op s t then [x] else [] - + + let apply_cl x l = + List.fold_left + (fun k c -> match apply_cons k c with + | [] -> raise Bot + | p::q -> List.fold_left join p q ) + x l + let assign x idl = let v = List.fold_left (fun v (id, id2) -> @@ -163,11 +179,15 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct let uniq x = uniq_sorted (sort x) let top vars = { vars; value = VarMap.empty } + let vtop x = { x with value = VarMap.empty } + let bottom vars = raise Bot (* we don't represent Bot *) + let is_bot x = false let vars x = x.vars let forgetvar x id = { x with value = VarMap.remove id x.value } + let forgetvars = List.fold_left forgetvar let project x id = try VarMap.find id x.value with Not_found -> List.assoc id x.vars @@ -220,6 +240,13 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct | [] -> l | _ -> { x with value = VarMap.add id2 v2 x.value }::l) [] v1 + + let apply_cl x l = + List.fold_left + (fun k c -> match apply_cons k c with + | [] -> raise Bot + | p::q -> List.fold_left join p q ) + x l let assign x idl = let v = List.fold_left diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml index 47515eb..ae71b09 100644 --- a/abstract/enum_domain_edd.ml +++ b/abstract/enum_domain_edd.ml @@ -1,41 +1,10 @@ open Ast open Formula open Util +open Enum_domain -module type ENUM_ENVIRONMENT_DOMAIN2 = sig - type t - type item = string - - (* construction *) - val top : (id * item list) list -> t - val bottom : (id * item list) list -> t - val is_bot : t -> bool - - (* variable management *) - val vars : t -> (id * item list) list - - val forgetvar : t -> id -> t - val forgetvars : t -> id list -> t - val project : t -> id -> item list - - (* set-theoretic operations *) - val join : t -> t -> t (* union *) - val meet : t -> t -> t (* intersection *) - - val subset : t -> t -> bool - val eq : t -> t -> bool - - (* abstract operations *) - val apply_cons : t -> enum_cons -> t - val apply_cl : t -> enum_cons list -> t - val assign : t -> (id * id) list -> t - - (* pretty-printing *) - val print : Format.formatter -> t -> unit -end - -module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct +module EDD : ENUM_ENVIRONMENT_DOMAIN = struct exception Top type item = string @@ -173,6 +142,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct let bottom vars = let t = top vars in { t with root = DBot } + let vtop x = { x with root = DTop } + (* is_bot : t -> bool *) @@ -284,7 +255,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct apply_cl : t -> enum_cons list -> t *) let apply_cons v x = - meet v (of_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 diff --git a/abstract/varenv.ml b/abstract/varenv.ml index 8bd3971..450bef3 100644 --- a/abstract/varenv.ml +++ b/abstract/varenv.ml @@ -20,6 +20,7 @@ type varenv = { cycle : (id * id * typ) list; (* s'(x) = s(y) *) forget : (id * typ) list; (* s'(x) not specified *) + forget_inv : (id * typ) list; } @@ -267,7 +268,12 @@ let mk_varenv (rp : rooted_prog) f cl = [] last_vars in let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in + let forget_inv = List.map (fun (_, id, ty) -> (id, ty)) + (List.filter + (fun (_, id, _) -> + not (List.exists (fun (_, b, _) -> b = id) cycle)) + all_vars) in { evars = enum_vars; nvars = num_vars; ev_order; - last_vars; all_vars; cycle; forget } + last_vars; all_vars; cycle; forget; forget_inv } |