summaryrefslogtreecommitdiff
path: root/abstract/abs_interp_dynpart.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/abs_interp_dynpart.ml')
-rw-r--r--abstract/abs_interp_dynpart.ml207
1 files changed, 69 insertions, 138 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index bbd8d19..0f6bbbf 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -5,20 +5,17 @@ open Typing
open Cmdline
open Util
-open Num_domain
-open Enum_domain
+open Abs_domain
open Varenv
-module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN)
+module I (D0 : ENVIRONMENT_DOMAIN)
: sig
val do_prog : cmdline_opt -> rooted_prog -> unit
end = struct
- type abs_v = ED.t * ND.t
-
(*
Abstract analysis based on dynamic partitionning of the state space.
Idea : use somme conditions appearing in the text of the program as
@@ -32,7 +29,7 @@ end = struct
id : int;
depth : int;
- mutable def : abs_v;
+ mutable def : D0.t;
is_init : bool;
mutable f : bool_expr;
@@ -40,7 +37,7 @@ end = struct
(* For chaotic iteration fixpoint *)
mutable in_c : int;
- mutable v : abs_v;
+ mutable v : D0.t;
mutable out_t : int list;
mutable in_t : int list;
@@ -69,86 +66,32 @@ end = struct
************************** *)
(*
- 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) = ED.is_bot e || ND.is_bot n
-
- let print_v fmt (enum, num) =
- if is_bot (enum, num) then
- Format.fprintf fmt "⊥"
- else
- Format.fprintf fmt "@[<hov 1>(%a,@ %a)@]" ED.print enum ND.print num
-
- (*
- join : abs_v -> abs_v -> abs_v
- widen : abs_v -> abs_v -> abs_v
- meet : abs_v -> abs_v -> abs_v
- *)
- let join a b =
- if is_bot a then b
- else if is_bot b then a
- else (ED.join (fst a) (fst b), ND.join (snd a) (snd b))
-
- let widen a b =
- if is_bot a then b
- else if is_bot b then a
- else (ED.join (fst a) (fst b), ND.widen (snd a) (snd b))
-
- 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 -> ED.vtop e1, ND.vbottom n1
-
- (*
- eq_v : abs_v -> abs_v -> bool
- subset_v : abs_v -> abs_v -> bool
+ apply_cl : D0.t -> conslist -> D0.t
*)
- let eq_v (a, b) (c, d) =
- (is_bot (a, b) && is_bot (c, d))
- || (ED.eq a c && ND.eq b d)
-
- let subset_v (a, b) (c, d) =
- (is_bot (a, b)) ||
- (not (is_bot (c, d)) && ED.subset a c && ND.subset b d)
-
- (*
- apply_cl : abs_v -> conslist -> abs_v
- *)
- let rec apply_cl (enum, num) (ec, nc, r) =
+ let rec apply_cl v (ec, nc, r) =
begin match r with
| CLTrue ->
- begin
- try (ED.apply_cl enum ec, ND.apply_cl num nc)
- with Bot -> ED.vtop enum, ND.vbottom num
- end
+ D0.apply_ncl (D0.apply_ecl v ec) nc
| CLFalse ->
- (ED.vtop enum, ND.vbottom num)
+ D0.bottom (D0.varenv v)
| 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
+ 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 (enum, num) (ec@eca, nc@nca, ra) in
- let b = apply_cl (enum, num) (ec@ecb, nc@ncb, rb) in
- join a b
+ 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 : abs_v -> conslist -> abs_v list
+ 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 =
- try ED.apply_cl (fst v) ec, ND.apply_cl (snd v) nc
- with Bot -> ED.vtop (fst v), ND.vbottom (snd v)
- in
- if is_bot v then [] else [v]
+ let v = D0.apply_ncl (D0.apply_ecl v ec) nc in
+ if D0.is_bot v then [] else [v]
| CLFalse ->
[]
| CLAnd(a, b) ->
@@ -158,7 +101,7 @@ end = struct
| 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 -> eq_v a b) lb)) la)
+ lb@(List.filter (fun a -> not (List.exists (fun b -> D0.eq a b) lb)) la)
(* ***************************
@@ -237,14 +180,14 @@ end = struct
{
id;
depth = 0;
- def = apply_cl (top env) (conslist_of_f cf);
+ def = apply_cl (D0.top env.ve) (conslist_of_f cf);
is_init;
f = cf;
cl = conslist_of_f cf;
in_c = 0;
- v = bottom env;
+ v = D0.bottom env.ve;
out_t = [];
in_t = [];
@@ -281,41 +224,29 @@ end = struct
set_target_case : env -> edd_v -> bool_expr -> edd_v
cycle : env -> edd_v -> conslist -> edd_v
*)
- let pass_cycle env (enum, num) =
+ 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 enum = ED.assign enum assign_e in
- let num = ND.assign num assign_n in
+ let v = D0.eassign v assign_e in
+ let v = D0.nassign v 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
+ D0.forgetvars v (List.map fst env.forget)
- (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
-
- let unpass_cycle env (enum, num) =
+ 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 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
+ let v = D0.eassign v assign_e in
+ let v = D0.nassign v assign_n in
- (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
+ D0.forgetvars v (List.map fst env.ve.forget_inv)
(*
print_locs : env -> unit
@@ -324,7 +255,7 @@ end = struct
let print_locs_defs e =
Hashtbl.iter
(fun id loc ->
- Format.printf "q%d: @[<v 2>%a@]@." id print_v loc.def;
+ Format.printf "q%d: @[<v 2>%a@]@." id D0.print loc.def;
)
e.loc
@@ -332,9 +263,9 @@ end = struct
Hashtbl.iter
(fun id loc ->
Format.printf "@.";
- Format.printf "q%d (depth = %d):@. D: @[<v 2>%a@]@." id loc.depth print_v loc.def;
+ 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@." print_v loc.v;
+ 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;
)
@@ -385,10 +316,10 @@ end = struct
loc.in_t <- [];
loc.in_c <- 0;
if loc.is_init then begin
- loc.v <- apply_cl (top e) loc.cl;
+ loc.v <- apply_cl (D0.top e.ve) loc.cl;
delta := q::!delta
end else
- loc.v <- bottom e)
+ loc.v <- D0.bottom e.ve)
e.loc;
(*print_locs_defs e;*)
@@ -404,14 +335,14 @@ end = struct
let start = loc.v in
let f i =
- (*Format.printf "I: %a@." print_v i;*)
- let i' = meet i (unpass_cycle e loc.def) in
- (*Format.printf "I': %a@." print_v i';*)
- let j = join start
+ (*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
- (meet (pass_cycle e.ve i') loc.def)
+ (D0.meet (pass_cycle e.ve i') loc.def)
loc.cl) in
- (*Format.printf "J: %a@." print_v j;*)
+ (*Format.printf "J: %a@." D0.print j;*)
j
in
@@ -419,11 +350,11 @@ end = struct
let fi = f i in
let j =
if n < e.opt.widen_delay then
- join i fi
+ D0.join i fi
else
- widen i fi
+ D0.widen i fi
in
- if eq_v i j
+ if D0.eq i j
then i
else iter (n+1) j
in
@@ -432,27 +363,27 @@ end = struct
let u = pass_cycle e.ve z in
if e.opt.verbose_ci then
- Format.printf "Fixpoint: %a@. mem fp: %a@." print_v z print_v u;
+ Format.printf "Fixpoint: %a@. mem fp: %a@." D0.print z D0.print u;
loc.v <- z;
Hashtbl.iter
(fun t loc2 ->
- let v = meet u loc2.def in
+ let v = D0.meet u loc2.def 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;*)
- if not (is_bot w) then begin
+ (*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 print_v w;
+ 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 (subset_v w loc2.v) then begin
+ if not (D0.subset w loc2.v) then begin
if loc2.in_c < e.opt.widen_delay then
- loc2.v <- join loc2.v w
+ loc2.v <- D0.join loc2.v w
else
- loc2.v <- widen loc2.v w;
+ loc2.v <- D0.widen loc2.v w;
loc2.in_c <- loc2.in_c + 1;
if not (List.mem t !delta)
then delta := t::!delta
@@ -467,7 +398,7 @@ end = struct
let useless = ref [] in
Hashtbl.iter
(fun i loc ->
- if is_bot loc.v then begin
+ if D0.is_bot loc.v then begin
Format.printf "Useless location detected: q%d@." i;
useless := i::!useless
end)
@@ -479,7 +410,7 @@ end = struct
(fun _ loc ->
let verif, violate = List.partition
(fun (_, f, _) ->
- is_bot (apply_cl loc.v (conslist_of_f 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;
@@ -511,12 +442,12 @@ end = struct
try
let cond, _ = List.find
(fun (c, _) ->
- is_bot (apply_cl loc.v (conslist_of_f c))
- || is_bot (apply_cl loc.v (conslist_of_f (BNot 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 is_bot (apply_cl loc.v (conslist_of_f cond))
+ if D0.is_bot (apply_cl loc.v (conslist_of_f cond))
then BNot cond
else cond
in
@@ -538,13 +469,13 @@ end = struct
let cs = ternary_conds loc.f in
List.iter
(fun (c, exprs) ->
- let cases_t = apply_cl_all_cases (top e) (conslist_of_f c) in
- let cases_f = apply_cl_all_cases (top e) (conslist_of_f (BNot c)) in
+ 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 (is_bot (meet loc.v case)))
+ (fun (_, case) -> not (D0.is_bot (D0.meet loc.v case)))
cases)
>= 2
then
@@ -554,10 +485,10 @@ end = struct
(fun qi ->
let loci = Hashtbl.find e.loc qi in
let v = apply_cl
- (meet (pass_cycle e.ve loci.v) loc.def)
+ (D0.meet (pass_cycle e.ve loci.v) loc.def)
loc.cl in
List.map
- (fun (ci, case) -> qi, ci, not (is_bot (meet v case)))
+ (fun (ci, case) -> qi, ci, not (D0.is_bot (D0.meet v case)))
cases)
loc.in_t
in
@@ -565,14 +496,14 @@ end = struct
let out_tc =
List.flatten @@ List.map
(fun (ci, case) ->
- let v = meet loc.v case in
+ let v = D0.meet loc.v case in
List.map
(fun qo ->
let loco = Hashtbl.find e.loc qo in
let w = apply_cl
- (meet (pass_cycle e.ve v) loco.def)
+ (D0.meet (pass_cycle e.ve v) loco.def)
loco.cl
- in qo, ci, not (is_bot w))
+ in qo, ci, not (D0.is_bot w))
loc.out_t)
cases
in
@@ -672,13 +603,13 @@ end = struct
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 print_v ", ") (cases_t@cases_f);
+ (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 (is_bot (meet loc.v case)) then
+ 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
@@ -686,7 +617,7 @@ end = struct
{ loc with
id = (incr e.counter; !(e.counter));
depth = loc.depth + 1;
- def = meet loc.def case;
+ def = D0.meet loc.def case;
f = ff;
cl = conslist_of_f ff } in
Hashtbl.add e.loc loc2.id loc2
@@ -727,15 +658,15 @@ end = struct
if List.exists (fun (p, _, _) -> p) e.ve.all_vars then begin
let final =
Hashtbl.fold
- (fun _ loc v -> join v loc.v)
- e.loc (bottom e) in
+ (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
- ND.print_itv (ND.project (snd final) id)
+ D0.print_itv (D0.nproject final id)
| TEnum _ -> Format.printf "%a : enum variable@ "
Formula_printer.print_id id)
e.ve.all_vars;
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-16 19:52:29 +0000