summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp_dynpart.ml277
1 files changed, 142 insertions, 135 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index bc0755b..65255ca 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -501,150 +501,156 @@ end = struct
let qc = ref None in
- (* put true or false conditions into location definition *)
- Hashtbl.iter
- (fun q (loc : location) ->
- let rec iter () =
- 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))))
- (ternary_conds loc.f)
- in
- let tr =
- if 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 (top e) (conslist_of_f c) in
- let cases_f = apply_cl_all_cases (top e) (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)))
- 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
- (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)))
- cases)
- loc.in_t
+ 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, _) ->
+ is_bot (apply_cl loc.v (conslist_of_f c))
+ || is_bot (apply_cl loc.v (conslist_of_f (BNot c))))
+ (ternary_conds loc.f)
in
- (* calculate which transitions q -> qo stay or are destroyed (approximation) *)
- let out_tc =
- List.flatten @@ List.map
- (fun (ci, case) ->
- let v = 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)
- loco.cl
- in qo, ci, not (is_bot w))
- loc.out_t)
- cases
+ let tr =
+ if is_bot (apply_cl loc.v (conslist_of_f cond))
+ then BNot cond
+ else cond
in
- (* calculate which cases have a good number of disappearing transitions *)
- let fa =
- let cs_sc =
- List.map
+ 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 (top e) (conslist_of_f c) in
+ let cases_f = apply_cl_all_cases (top e) (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)))
+ 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
+ (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)))
+ 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 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)
+ let v = 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)
+ loco.cl
+ in qo, ci, not (is_bot w))
+ loc.out_t)
cases
in
- 5 * List.fold_left max 0 cs_sc
- in
- (* calculate which states become inaccessible *)
- let fb =
- if fa = 0 || 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)
+ (* 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 + (if a + b > 0 then 1 else 0))
+ cases
+ in
+ let a = List.fold_left max 0 cs_sc in
+ let b = 5 * a in
+ if a > 0 && b = 0 then 1 else 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 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
+ 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
- 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
+ (* calculate in/out count, weighted by changing guarantees *)
+ let fc =
+ 0 * (2 * List.length loc.out_t + List.length loc.in_t)
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 number of VOI (variables of interest) that are affected *)
- let fc =
- let vlist = refd_evars_of_f exprs in
- 10 * List.length
- (List.filter (fun v -> List.mem v vlist) voi) in
- (* give score to split *)
- let fd = 2 * List.length loc.out_t + List.length loc.in_t in
- 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)
- )
- cs
- )
- e.loc;
+ (* 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;
- if Hashtbl.length e.loc < e.opt.max_dp_width then
match !qc with
| None ->
Format.printf "@.Found no more possible refinement.@.@."
@@ -673,6 +679,7 @@ end = struct
List.iter (handle_case (BNot c)) cases_f;
iter (n+1)
+ end
in iter 0;
(* Check guarantees *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 16:46:35 +0000