open Ast
open Ast_util
open Formula
open Typing
open Cmdline
open Util
open Abs_domain
open Varenv
module I (D0 : ENVIRONMENT_DOMAIN)
: sig
val do_prog : cmdline_opt -> rooted_prog -> unit
end = struct
(*
Abstract analysis based on dynamic partitionning of the state space.
Idea : use somme conditions appearing in the text of the program as
disjunctions. We don't want to consider them all at once in the first
place because it would be way too costly ; instead we try to dynamically
partition tye system. But we haven't got a very good heuristic for that,
so it doesn't work very well.
*)
type location = {
id : int;
depth : int;
mutable def : D0.t;
is_init : bool;
mutable f : bool_expr;
mutable cl : conslist;
(* For chaotic iteration fixpoint *)
mutable in_c : int;
mutable v : D0.t;
mutable out_t : int list;
mutable in_t : int list;
mutable verif_g : id list;
mutable violate_g : id list;
}
type env = {
rp : rooted_prog;
opt : cmdline_opt;
ve : varenv;
(* program expressions *)
f : bool_expr;
guarantees : (id * bool_expr * id) list;
(* data *)
loc : (int, location) Hashtbl.t;
counter : int ref;
}
(* **************************
ABSTRACT VALUES
************************** *)
(*
apply_cl : D0.t -> conslist -> D0.t
*)
let rec apply_cl v (ec, nc, r) =
begin match r with
| CLTrue ->
D0.apply_ncl (D0.apply_ecl v ec) nc
| CLFalse ->
D0.bottom (D0.varenv v)
| CLAnd(a, b) ->
let v = apply_cl v (ec, nc, a) in
let v = apply_cl v ([], nc, b) in
v
| CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
let a = apply_cl v (ec@eca, nc@nca, ra) in
let b = apply_cl v (ec@ecb, nc@ncb, rb) in
D0.join a b
end
(*
apply_cl_all_cases : D0.t -> conslist -> D0.t list
*)
let rec apply_cl_all_cases v (ec, nc, r) =
match r with
| CLTrue ->
let v = D0.apply_ncl (D0.apply_ecl v ec) nc in
if D0.is_bot v then [] else [v]
| CLFalse ->
[]
| CLAnd(a, b) ->
let q1 = apply_cl_all_cases v (ec, nc, a) in
List.flatten
(List.map (fun c -> apply_cl_all_cases c ([], [], b)) q1)
| CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
let la = apply_cl_all_cases v (ec@eca, nc@nca, ra) in
let lb = apply_cl_all_cases v (ec@ecb, nc@ncb, rb) in
lb@(List.filter (fun a -> not (List.exists (fun b -> D0.eq a b) lb)) la)
(* ***************************
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, repls = 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; "L"^repl, "L"^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
let guarantees = List.map
(fun (id, f, v) -> id, formula_replace_evars repls f, v)
guarantees 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 opt.disjunct 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 id = let i = ref 0 in fun () -> (incr i; !i) in
let add_loc is_init conds =
let cf = simplify_k conds f in
let cf = simplify_k (get_root_true cf) cf in
let id = id() in
Hashtbl.add env.loc id
{
id;
depth = 0;
def = apply_cl (D0.top env.ve) (conslist_of_f cf);
is_init;
f = cf;
cl = conslist_of_f cf;
in_c = 0;
v = D0.bottom env.ve;
out_t = [];
in_t = [];
verif_g = [];
violate_g = [];
};
in
add_loc true [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)];
let rec div_g conds = function
| [] -> add_loc false conds
| (_, _, v)::r ->
add_loc false ((BEnumCons(E_NE, v, EItem bool_true))::conds);
div_g ((BEnumCons(E_EQ, v, EItem bool_true))::conds) r
in
div_g [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] env.guarantees;
env
(*
ternary_conds : bool_expr -> bool_expr list
*)
let rec ternary_conds = function
| BAnd(a, b) -> ternary_conds a @ ternary_conds b
| BTernary(c, a, b) as x -> [c, x]
| _ -> []
(*
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 v =
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 v = D0.eassign v assign_e in
let v = D0.nassign v assign_n in
D0.forgetvars v (List.map fst env.forget)
let unpass_cycle env v =
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 v = D0.eassign v assign_e in
let v = D0.nassign v assign_n in
D0.forgetvars v (List.map fst env.ve.forget_inv)
(*
print_locs : env -> unit
*)
let print_locs_defs e =
Hashtbl.iter
(fun id loc ->
Format.printf "q%d: @[<v 2>%a@]@." id D0.print loc.def;
)
e.loc
let print_locs e =
Hashtbl.iter
(fun id loc ->
Format.printf "@.";
Format.printf "q%d (depth = %d):@. D: @[<v 2>%a@]@." id loc.depth D0.print loc.def;
(*Format.printf " F: (%a)@." Formula_printer.print_expr loc.f;*)
Format.printf " V: %a@." D0.print loc.v;
Format.printf " -> @[<hov>[%a]@]@."
(print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
)
e.loc
let dump_graphwiz_trans_graph e file =
let o = open_out file in
let fmt = Format.formatter_of_out_channel o in
Format.fprintf fmt "digraph G{@.";
Hashtbl.iter
(fun id loc ->
if loc.is_init then
Format.fprintf fmt " q%d [shape=doublecircle, label=\"q%d [%a]\"];@."
id id (print_list Format.pp_print_string ", ") loc.violate_g
else
Format.fprintf fmt " q%d [label=\"q%d [%a]\"];@."
id id (print_list Format.pp_print_string ", ") loc.violate_g;
let n1 = List.length loc.violate_g in
List.iter
(fun v ->
let n2 = List.length (Hashtbl.find e.loc v).violate_g in
let c, w =
if n2 > n1 then "#770000", 1
else "black", 2
in
Format.fprintf fmt " q%d -> q%d [color = \"%s\", weight = %d];@."
id v c w)
loc.out_t)
e.loc;
Format.fprintf fmt "}@.";
close_out o
(*
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 <- [];
loc.in_c <- 0;
if loc.is_init then begin
loc.v <- apply_cl (D0.top e.ve) loc.cl;
delta := q::!delta
end else
loc.v <- D0.bottom e.ve)
e.loc;
(*print_locs_defs e;*)
(* 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@." D0.print i;*)
let i' = D0.meet i (unpass_cycle e loc.def) in
(*Format.printf "I': %a@." D0.print i';*)
let j = D0.join start
(apply_cl
(D0.meet (pass_cycle e.ve i') loc.def)
loc.cl) in
(*Format.printf "J: %a@." D0.print j;*)
j
in
let rec iter n i =
let fi = f i in
let j =
if n < e.opt.widen_delay then
D0.join i fi
else
D0.widen i fi
in
if D0.eq i j
then i
else iter (n+1) j
in
let y = iter 0 start in
let z = f y in
let u = pass_cycle e.ve z in
if e.opt.verbose_ci then
Format.printf "Fixpoint: %a@. mem fp: %a@." D0.print z D0.print u;
loc.v <- z;
Hashtbl.iter
(fun t loc2 ->
let v = D0.meet u loc2.def in
let w = apply_cl v loc2.cl in
(*Format.printf "u: %a@.v: %a@. w: %a@." D0.print u D0.print v D0.print w;*)
if not (D0.is_bot w) then begin
if e.opt.verbose_ci then
Format.printf "%d -> %d with:@. %a@." s t D0.print w;
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;
if not (D0.subset w loc2.v) then begin
if loc2.in_c < e.opt.widen_delay then
loc2.v <- D0.join loc2.v w
else
loc2.v <- D0.widen loc2.v w;
loc2.in_c <- loc2.in_c + 1;
if not (List.mem t !delta)
then delta := t::!delta
end
end)
e.loc;
delta := List.filter ((<>) s) !delta;
done;
(* remove useless locations *)
let useless = ref [] in
Hashtbl.iter
(fun i loc ->
if D0.is_bot loc.v then begin
Format.printf "Useless location detected: q%d@." i;
useless := i::!useless
end)
e.loc;
List.iter (Hashtbl.remove e.loc) !useless;
(* check which states verify/violate guarantees *)
Hashtbl.iter
(fun _ loc ->
let verif, violate = List.partition
(fun (_, f, _) ->
D0.is_bot (apply_cl loc.v (conslist_of_f f)))
e.guarantees
in
loc.verif_g <- List.map (fun (a, b, c) -> a) verif;
loc.violate_g <- List.map (fun (a, b, c) -> a) violate)
e.loc;
print_locs e;
()
let do_prog opt rp =
let e = init_env opt rp in
let rec iter n =
Format.printf "@.--------------@.Refinement #%d@." n;
chaotic_iter e;
dump_graphwiz_trans_graph e (Format.sprintf "/tmp/part%03d.dot" n);
let qc = ref None in
if Hashtbl.length e.loc < e.opt.max_dp_width then begin
(* put true or false conditions into location definition *)
Hashtbl.iter
(fun q (loc : location) ->
let rec iter () =
try
let cond, _ = List.find
(fun (c, _) ->
D0.is_bot (apply_cl loc.v (conslist_of_f c))
|| D0.is_bot (apply_cl loc.v (conslist_of_f (BNot c))))
(ternary_conds loc.f)
in
let tr =
if D0.is_bot (apply_cl loc.v (conslist_of_f cond))
then BNot cond
else cond
in
loc.def <- apply_cl loc.def (conslist_of_f tr);
loc.f <- simplify_k [tr] loc.f;
loc.f <- simplify_k (get_root_true loc.f) loc.f;
loc.cl <- conslist_of_f loc.f;
iter()
with Not_found -> ()
in iter ())
e.loc;
(* find splitting condition *)
let voi = List.map (fun (a, b, c) -> c) e.guarantees in
Hashtbl.iter
(fun q (loc:location) ->
if loc.depth < e.opt.max_dp_depth then
let cs = ternary_conds loc.f in
List.iter
(fun (c, exprs) ->
let cases_t = apply_cl_all_cases (D0.top e.ve) (conslist_of_f c) in
let cases_f = apply_cl_all_cases (D0.top e.ve) (conslist_of_f (BNot c)) in
let cases = List.mapi (fun i c -> i, c) (cases_t @ cases_f) in
if
List.length
(List.filter
(fun (_, case) -> not (D0.is_bot (D0.meet loc.v case)))
cases)
>= 2
then
(* calculate which transitions qi -> q stay or are destroyed (approximation) *)
let in_tc =
List.flatten @@ List.map
(fun qi ->
let loci = Hashtbl.find e.loc qi in
let v = apply_cl
(D0.meet (pass_cycle e.ve loci.v) loc.def)
loc.cl in
List.map
(fun (ci, case) -> qi, ci, not (D0.is_bot (D0.meet v case)))
cases)
loc.in_t
in
(* calculate which transitions q -> qo stay or are destroyed (approximation) *)
let out_tc =
List.flatten @@ List.map
(fun (ci, case) ->
let v = D0.meet loc.v case in
List.map
(fun qo ->
let loco = Hashtbl.find e.loc qo in
let w = apply_cl
(D0.meet (pass_cycle e.ve v) loco.def)
loco.cl
in qo, ci, not (D0.is_bot w))
loc.out_t)
cases
in
(* calculate which cases have a good number of disappearing transitions *)
let fa =
let cs_sc =
List.map
(fun (ci, case) ->
let a =
List.length
(List.filter (fun (qi, c, a) -> not a && c = ci) in_tc)
in
let b =
List.length
(List.filter (fun (qo, c, a) -> not a && c = ci) out_tc)
in
a + b + a * b)
cases
in
let a = List.fold_left max 0 cs_sc in
let b = if a = 0 then 0 else
List.length @@ List.filter
(fun qi ->
let qos = List.flatten @@ List.map
(fun (cid, c) ->
if List.exists (fun (qi0, c0, a) -> a && qi0 = qi && c0 = cid) in_tc
then
List.map (fun (qo, _, _) -> qo) @@
List.filter (fun (_, c1, a) -> a && cid = c1) out_tc
else [])
cases
in
List.exists (fun qo -> not (List.mem qo qos)) loc.out_t)
loc.in_t
in
5 * a + 17 * b
in
if fa <> 0 then begin
(* calculate which states become inaccessible *)
let fb =
if List.for_all (fun (_, _, a) -> a) out_tc
then 0
else
let ff id = (* transition function for new graph *)
if id >= 1000000 then
let case = id - 1000000 in
List.map (fun (qo, _, _) -> qo)
(List.filter (fun (_, c, a) -> c = case && a) out_tc)
else
let out_t = (Hashtbl.find e.loc id).out_t in
if List.mem loc.id out_t then
(List.map (fun (_, c, _) -> c + 1000000)
(List.filter (fun (qi, _, a) -> qi = id && a) in_tc))
@ (List.filter ((<>) id) out_t)
else out_t
in
let memo = Hashtbl.create 12 in
let rec do_x id =
if not (Hashtbl.mem memo id) then begin
Hashtbl.add memo id ();
List.iter do_x (ff id)
end
in
Hashtbl.iter (fun i loc2 -> if loc2.is_init && i <> loc.id then do_x i) e.loc;
if loc.is_init then List.iter (fun (ci, _) -> do_x (ci+1000000)) cases;
let disappear_count = (Hashtbl.length e.loc + List.length cases) - (Hashtbl.length memo) in
21 * disappear_count
in
(* calculate in/out count, weighted by changing guarantees *)
let fc =
1 * (2 * List.length loc.out_t + List.length loc.in_t)
in
(* calculate number of VOI (variables of interest) that are affected *)
let fd =
let vlist = refd_evars_of_f exprs in
3 * List.length
(List.filter (fun v -> List.mem v vlist) voi) in
(* give score to split *)
let score =
if fa = 0 then 0 else
fa + fb + fc + fd
in
Format.printf " %5d + %5d + %5d + %5d = %5d (q%d)@." fa fb fc fd score loc.id;
if score > 0 &&
match !qc with
| None -> true
| Some (s, _, _, _, _) -> score >= s
then
qc := Some(score, q, c, cases_t, cases_f)
end)
cs
)
e.loc;
match !qc with
| None ->
Format.printf "@.Found no more possible refinement.@.@."
| Some (score, q, c, cases_t, cases_f) ->
Format.printf "@.Refine q%d : @[<v 2>[ %a ]@]@." q
(print_list D0.print ", ") (cases_t@cases_f);
let loc = Hashtbl.find e.loc q in
Hashtbl.remove e.loc loc.id;
let handle_case cc case =
if not (D0.is_bot (D0.meet loc.v case)) then
let ff = simplify_k [cc] loc.f in
let ff = simplify_k (get_root_true ff) ff in
let loc2 =
{ loc with
id = (incr e.counter; !(e.counter));
depth = loc.depth + 1;
def = D0.meet loc.def case;
f = ff;
cl = conslist_of_f ff } in
Hashtbl.add e.loc loc2.id loc2
in
List.iter (handle_case c) cases_t;
List.iter (handle_case (BNot c)) cases_f;
iter (n+1)
end
in iter 0;
(* Check guarantees *)
let check_guarantee (id, f, _) =
Format.printf "@[<v 4>";
let cl = Formula.conslist_of_f f in
Format.printf "%s:@ %a ⇒ ⊥ @ "
id Formula_printer.print_conslist cl;
let violate = ref [] in
Hashtbl.iter
(fun lid loc ->
if List.mem id loc.violate_g then
violate := lid::!violate)
e.loc;
if !violate = [] then
Format.printf "OK"
else
Format.printf "VIOLATED in @[<hov 2>[ %a ]@]"
(print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") !violate;
Format.printf "@]@ ";
in
if e.guarantees <> [] then begin
Format.printf "Guarantee @[<v 0>";
List.iter check_guarantee e.guarantees;
Format.printf "@]@."
end;
(* Examine probes *)
if List.exists (fun (p, _, _) -> p) e.ve.all_vars then begin
let final =
Hashtbl.fold
(fun _ loc v -> D0.join v loc.v)
e.loc (D0.bottom e.ve) in
Format.printf "Probes: @[<v 0>";
List.iter (fun (p, id, ty) ->
if p then match ty with
| TInt | TReal ->
Format.printf "%a ∊ %a@ " Formula_printer.print_id id
D0.print_itv (D0.nproject final id)
| TEnum _ -> Format.printf "%a : enum variable@ "
Formula_printer.print_id id)
e.ve.all_vars;
Format.printf "@]@."
end
end