Revision 03c767b1
Added by Pierre-Loïc Garoche almost 4 years ago
| src/tools/seal/seal_extract.ml | ||
|---|---|---|
| 6 | 6 |
|
| 7 | 7 |
(* Switched system extraction: expression are memoized *) |
| 8 | 8 |
(*let expr_mem = Hashtbl.create 13*) |
| 9 |
|
|
| 10 |
type element = IsInit | Expr of expr |
|
| 11 |
|
|
| 12 |
type guard = (element * bool) list |
|
| 13 |
type guarded_expr = guard * element |
|
| 14 |
type mdef_t = guarded_expr list |
|
| 15 |
|
|
| 16 |
let pp_elem fmt e = |
|
| 17 |
match e with |
|
| 18 |
| IsInit -> Format.fprintf fmt "init" |
|
| 19 |
| Expr e -> Format.fprintf fmt "%a" Printers.pp_expr e |
|
| 20 |
|
|
| 21 |
let pp_guard_list fmt gl = |
|
| 22 |
(fprintf_list ~sep:"; " |
|
| 23 |
(fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl |
|
| 24 |
|
|
| 25 |
let pp_guard_expr fmt (gl,e) = |
|
| 26 |
Format.fprintf fmt "%a -> %a" |
|
| 27 |
pp_guard_list gl |
|
| 28 |
pp_elem e |
|
| 29 |
|
|
| 30 |
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel |
|
| 31 |
|
|
| 32 |
|
|
| 9 |
|
|
| 33 | 10 |
let add_init defs vid = |
| 34 | 11 |
Hashtbl.add defs vid [[], IsInit] |
| 35 | 12 |
|
| 36 |
let deelem e = match e with |
|
| 37 |
Expr e -> e |
|
| 38 |
| IsInit -> assert false (* Wasn't expecting isinit here: we are building values! *) |
|
| 39 |
|
|
| 40 |
let is_eq_elem elem elem' = |
|
| 41 |
match elem, elem' with |
|
| 42 |
| IsInit, IsInit -> true |
|
| 43 |
| Expr e, Expr e' -> e = e' (* |
|
| 44 |
Corelang.is_eq_expr e e' *) |
|
| 45 |
| _ -> false |
|
| 46 |
|
|
| 47 |
let select_elem elem (gelem, _) = |
|
| 48 |
is_eq_elem elem gelem |
|
| 49 |
|
|
| 50 | 13 |
|
| 51 | 14 |
(**************************************************************) |
| 52 | 15 |
(* Convert from Lustre expressions to Z3 expressions and back *) |
| ... | ... | |
| 325 | 288 |
Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid) |
| 326 | 289 |
else |
| 327 | 290 |
begin |
| 328 |
if !debug then ( |
|
| 329 |
Format.eprintf "Checking implication: %s => %s? "
|
|
| 291 |
if !seal_debug then (
|
|
| 292 |
report ~level:6 (fun fmt -> Format.fprintf fmt "Checking implication: %s => %s?@ "
|
|
| 330 | 293 |
(Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2) |
| 331 |
); |
|
| 294 |
));
|
|
| 332 | 295 |
let solver = Z3.Solver.mk_simple_solver !ctx in |
| 333 | 296 |
let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in |
| 334 | 297 |
let res = |
| 335 | 298 |
try |
| 336 | 299 |
let status_res = Z3.Solver.check solver [tgt] in |
| 337 | 300 |
match status_res with |
| 338 |
| Z3.Solver.UNSATISFIABLE -> if !debug then Format.eprintf "Valid!@."; |
|
| 301 |
| Z3.Solver.UNSATISFIABLE -> if !seal_debug then |
|
| 302 |
report ~level:6 (fun fmt -> Format.fprintf fmt "Valid!@ "); |
|
| 339 | 303 |
true |
| 340 |
| _ -> if !debug then Format.eprintf "not proved valid@.";
|
|
| 304 |
| _ -> if !seal_debug then report ~level:6 (fun fmt -> Format.fprintf fmt "not proved valid@ ");
|
|
| 341 | 305 |
false |
| 342 | 306 |
with Zustre_common.UnknownFunction(id, msg) -> ( |
| 343 | 307 |
report ~level:1 msg; |
| ... | ... | |
| 376 | 340 |
tl |
| 377 | 341 |
) |
| 378 | 342 |
|
| 379 |
let check_sat ?(just_check=false) (l:guard) : bool * guard =
|
|
| 343 |
let check_sat ?(just_check=false) (l: elem_boolexpr guard) : bool * (elem_boolexpr guard) =
|
|
| 380 | 344 |
(* Syntactic simplification *) |
| 381 | 345 |
if false then |
| 382 |
Format.eprintf "Before simplify: %a@." pp_guard_list l;
|
|
| 346 |
Format.eprintf "Before simplify: %a@." (pp_guard_list pp_elem) l;
|
|
| 383 | 347 |
let l = simplify_neg_guard l in |
| 384 | 348 |
if false then ( |
| 385 |
Format.eprintf "After simplify: %a@." pp_guard_list l;
|
|
| 386 |
Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l;
|
|
| 349 |
Format.eprintf "After simplify: %a@." (pp_guard_list pp_elem) l;
|
|
| 350 |
Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " (pp_guard_list pp_elem)l;
|
|
| 387 | 351 |
); |
| 388 | 352 |
let solver = Z3.Solver.mk_simple_solver !ctx in |
| 389 | 353 |
try ( |
| ... | ... | |
| 589 | 553 |
(* Rewrite the expression expr, replacing any occurence of a variable |
| 590 | 554 |
by its definition. |
| 591 | 555 |
*) |
| 592 |
let rec rewrite defs expr : guarded_expr list = |
|
| 556 |
let rec rewrite defs expr : elem_guarded_expr list =
|
|
| 593 | 557 |
let rewrite = rewrite defs in |
| 594 | 558 |
let res = |
| 595 | 559 |
match expr.expr_desc with |
| ... | ... | |
| 623 | 587 |
(* Each expr is associated to its flatten guarded expr list *) |
| 624 | 588 |
let gell = List.map rewrite el in |
| 625 | 589 |
(* Computing all combinations: we obtain a list of guarded tuple *) |
| 626 |
let rec aux gell : (guard * expr list) list = |
|
| 590 |
let rec aux gell : (elem_boolexpr guard * expr list) list =
|
|
| 627 | 591 |
match gell with |
| 628 | 592 |
| [] -> assert false (* Not happening *) |
| 629 | 593 |
| [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel |
| ... | ... | |
| 635 | 599 |
fun accu (gl, minituple) -> |
| 636 | 600 |
let is_compat, guard_comb = combine_guards g gl in |
| 637 | 601 |
if is_compat then |
| 638 |
let new_gt : guard * expr list = (guard_comb, (deelem e)::minituple) in |
|
| 602 |
let new_gt : elem_boolexpr guard * expr list = (guard_comb, (deelem e)::minituple) in
|
|
| 639 | 603 |
new_gt::accu |
| 640 | 604 |
else |
| 641 | 605 |
accu |
| ... | ... | |
| 677 | 641 |
returns the same list of ge splited into the ones where the guard is true and the ones where it is false. In both lists the associated ge do not mention that guard anymore. |
| 678 | 642 |
|
| 679 | 643 |
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *) |
| 680 |
let split_mdefs elem (mdefs: guarded_expr list) = |
|
| 644 |
let split_mdefs elem (mdefs: elem_guarded_expr list) =
|
|
| 681 | 645 |
List.fold_left ( |
| 682 | 646 |
fun (selected, left_out) |
| 683 | 647 |
((guards, expr) as ge) -> |
| ... | ... | |
| 696 | 660 |
| _ -> ( |
| 697 | 661 |
Format.eprintf "@.Spliting list on elem %a.@.List:%a@." |
| 698 | 662 |
pp_elem elem |
| 699 |
pp_mdefs mdefs;
|
|
| 663 |
(pp_mdefs pp_elem) mdefs;
|
|
| 700 | 664 |
assert false (* more then one element selected. Should |
| 701 | 665 |
not happen , or trival dead code like if |
| 702 | 666 |
x then if not x then dead code *) |
| ... | ... | |
| 705 | 669 |
|
| 706 | 670 |
let split_mem_defs |
| 707 | 671 |
(elem: element) |
| 708 |
(mem_defs: (ident * guarded_expr list) list) |
|
| 672 |
(mem_defs: (ident * elem_guarded_expr list) list)
|
|
| 709 | 673 |
: |
| 710 |
((ident * mdef_t) list) * ((ident * mdef_t) list)
|
|
| 674 |
((ident * elem_guarded_expr mdef_t) list) * ((ident * elem_guarded_expr mdef_t) list)
|
|
| 711 | 675 |
|
| 712 | 676 |
= |
| 713 | 677 |
List.fold_right (fun (m,mdefs) |
| ... | ... | |
| 770 | 734 |
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions) |
| 771 | 735 |
*) |
| 772 | 736 |
let rec build_switch_sys |
| 773 |
(mem_defs : (Utils.ident * guarded_expr list) list ) |
|
| 737 |
(mem_defs : (Utils.ident * elem_guarded_expr list) list )
|
|
| 774 | 738 |
prefix |
| 775 | 739 |
: |
| 776 | 740 |
((expr * bool) list * (ident * expr) list ) list = |
| 777 |
if !debug then |
|
| 778 |
Format.eprintf "Build_switch with %a@."
|
|
| 741 |
if !seal_debug then
|
|
| 742 |
report ~level:4 (fun fmt -> Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@."
|
|
| 779 | 743 |
(Utils.fprintf_list ~sep:",@ " |
| 780 |
(fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a@ ]@]"
|
|
| 744 |
(fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]" |
|
| 781 | 745 |
id |
| 782 |
pp_mdefs gel))
|
|
| 783 |
mem_defs; |
|
| 746 |
(pp_mdefs pp_elem) gel))
|
|
| 747 |
mem_defs);
|
|
| 784 | 748 |
(* if all mem_defs have empty guards, we are done, return prefix, |
| 785 | 749 |
mem_defs expr. |
| 786 | 750 |
|
| 787 | 751 |
otherwise pick a guard in one of the mem, eg (g, b) then for each |
| 788 | 752 |
other mem, one need to select the same guard g with the same |
| 789 | 753 |
status b, *) |
| 754 |
let res = |
|
| 790 | 755 |
if List.for_all (fun (m,mdefs) -> |
| 791 | 756 |
(* All defs are unguarded *) |
| 792 | 757 |
match mdefs with |
| ... | ... | |
| 810 | 775 |
(* Picking a guard *) |
| 811 | 776 |
let elem_opt : expr option = pick_guard mem_defs in |
| 812 | 777 |
match elem_opt with |
| 813 |
None -> []
|
|
| 778 |
None -> assert false (* Otherwise the first case should have matched *)
|
|
| 814 | 779 |
| Some elem -> ( |
| 780 |
report ~level:4 (fun fmt -> Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem); |
|
| 815 | 781 |
let pos, neg = |
| 816 | 782 |
split_mem_defs |
| 817 | 783 |
(Expr elem) |
| ... | ... | |
| 844 | 810 |
let pos_prefix = (elem, true)::prefix in |
| 845 | 811 |
let neg_prefix = (elem, false)::prefix in |
| 846 | 812 |
let ok_pos, pos_prefix = clean pos_prefix in |
| 847 |
let ok_neg, neg_prefix = clean neg_prefix in |
|
| 848 |
(if ok_pos then build_switch_sys pos pos_prefix else []) |
|
| 849 |
@ |
|
| 850 |
(if ok_neg then build_switch_sys neg neg_prefix else []) |
|
| 813 |
let ok_neg, neg_prefix = clean neg_prefix in |
|
| 814 |
report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing %a@." Printers.pp_expr elem); |
|
| 815 |
let ok_l = if ok_pos then build_switch_sys pos pos_prefix else [] in |
|
| 816 |
report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing not(%a)@." Printers.pp_expr elem); |
|
| 817 |
let nok_l = if ok_neg then build_switch_sys neg neg_prefix else [] in |
|
| 818 |
ok_l @ nok_l |
|
| 851 | 819 |
) |
| 852 |
|
|
| 820 |
in |
|
| 821 |
if !seal_debug then ( |
|
| 822 |
report ~level:4 (fun fmt -> |
|
| 823 |
Format.fprintf fmt |
|
| 824 |
"@[<v 2>===> @[%t@ @]@]@ @]@ " |
|
| 825 |
(fun fmt -> List.iter (fun (gl,up) -> |
|
| 826 |
Format.fprintf fmt "[@[%a@]] -> (%a)@ " |
|
| 827 |
(pp_guard_list Printers.pp_expr) gl pp_up up) res); |
|
| 828 |
|
|
| 829 |
)); |
|
| 830 |
res |
|
| 831 |
|
|
| 853 | 832 |
|
| 854 | 833 |
|
| 855 | 834 |
(* Take a normalized node and extract a list of switches: (cond, |
| ... | ... | |
| 863 | 842 |
let eqs, auts = Corelang.get_node_eqs nd in |
| 864 | 843 |
assert (auts = []); (* Automata should be expanded by now *) |
| 865 | 844 |
let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in |
| 866 |
let defs : (ident, guarded_expr list) Hashtbl.t = Hashtbl.create 13 in |
|
| 845 |
let defs : (ident, elem_guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
|
|
| 867 | 846 |
let add_def = add_def defs in |
| 868 | 847 |
|
| 869 | 848 |
let vars = Corelang.get_node_vars nd in |
| ... | ... | |
| 910 | 889 |
Format.fprintf fmt "Output variable %s@." vid); |
| 911 | 890 |
add_def vid eq.eq_rhs; |
| 912 | 891 |
accu_mems, (vid, rewrite defs eq.eq_rhs)::accu_outputs |
| 913 |
|
|
| 892 |
|
|
| 914 | 893 |
) |
| 915 | 894 |
else |
| 916 | 895 |
( |
| 917 |
report ~level:3 (fun fmt -> |
|
| 918 |
Format.fprintf fmt "Registering variable %s@." vid); |
|
| 919 |
add_def vid eq.eq_rhs; |
|
| 920 |
accu_mems, accu_outputs |
|
| 921 |
) |
|
| 896 |
report ~level:3 (fun fmt ->
|
|
| 897 |
Format.fprintf fmt "Registering variable %s@." vid);
|
|
| 898 |
add_def vid eq.eq_rhs;
|
|
| 899 |
accu_mems, accu_outputs
|
|
| 900 |
)
|
|
| 922 | 901 |
| _ -> assert false (* should have been removed by normalization *) |
| 923 | 902 |
) ([], []) sorted_eqs |
| 924 | 903 |
in |
| ... | ... | |
| 929 | 908 |
report ~level:3 |
| 930 | 909 |
(fun fmt -> |
| 931 | 910 |
Format.fprintf fmt |
| 932 |
"@[<v 0>%a@]@ "
|
|
| 911 |
"@[<v 0>%a@]@."
|
|
| 933 | 912 |
(Utils.fprintf_list ~sep:"@ " |
| 934 | 913 |
(fun fmt (m,mdefs) -> |
| 935 | 914 |
Format.fprintf fmt |
| 936 | 915 |
"%s -> [@[<v 0>%a@] ]@ " |
| 937 | 916 |
m |
| 938 | 917 |
(Utils.fprintf_list ~sep:"@ " |
| 939 |
pp_guard_expr) mdefs
|
|
| 918 |
(pp_guard_expr pp_elem)) mdefs
|
|
| 940 | 919 |
)) |
| 941 | 920 |
mem_defs); |
| 942 | 921 |
(* Format.eprintf "Split init@."; *) |
| ... | ... | |
| 949 | 928 |
report ~level:3 |
| 950 | 929 |
(fun fmt -> |
| 951 | 930 |
Format.fprintf fmt |
| 952 |
"@[<v 0>Init:@ %a@ Step@ %a@]@ "
|
|
| 931 |
"@[<v 0>Init:@ %a@]@."
|
|
| 953 | 932 |
(Utils.fprintf_list ~sep:"@ " |
| 954 | 933 |
(fun fmt (m,mdefs) -> |
| 955 | 934 |
Format.fprintf fmt |
| 956 | 935 |
"%s -> @[<v 0>[%a@] ]@ " |
| 957 | 936 |
m |
| 958 | 937 |
(Utils.fprintf_list ~sep:"@ " |
| 959 |
pp_guard_expr) mdefs
|
|
| 938 |
(pp_guard_expr pp_elem)) mdefs
|
|
| 960 | 939 |
)) |
| 961 |
init_defs |
|
| 940 |
init_defs); |
|
| 941 |
report ~level:3 |
|
| 942 |
(fun fmt -> |
|
| 943 |
Format.fprintf fmt |
|
| 944 |
"@[<v 0>Step:@ %a@]@." |
|
| 962 | 945 |
(Utils.fprintf_list ~sep:"@ " |
| 963 | 946 |
(fun fmt (m,mdefs) -> |
| 964 | 947 |
Format.fprintf fmt |
| 965 | 948 |
"%s -> @[<v 0>[%a@] ]@ " |
| 966 | 949 |
m |
| 967 | 950 |
(Utils.fprintf_list ~sep:"@ " |
| 968 |
pp_guard_expr) mdefs
|
|
| 951 |
(pp_guard_expr pp_elem)) mdefs
|
|
| 969 | 952 |
)) |
| 970 | 953 |
update_defs); |
| 971 | 954 |
(* Format.eprintf "Build init@."; *) |
| 972 |
|
|
| 955 |
report ~level:4 (fun fmt -> Format.fprintf fmt "Build init@."); |
|
| 973 | 956 |
let sw_init= |
| 974 | 957 |
build_switch_sys init_defs [] |
| 975 | 958 |
in |
| 976 | 959 |
(* Format.eprintf "Build step@."; *) |
| 960 |
report ~level:4 (fun fmt -> Format.fprintf fmt "Build step@."); |
|
| 977 | 961 |
let sw_sys = |
| 978 | 962 |
build_switch_sys update_defs [] |
| 979 | 963 |
in |
| 980 | 964 |
|
| 965 |
report ~level:4 (fun fmt -> Format.fprintf fmt "Build init out@."); |
|
| 981 | 966 |
let init_out = |
| 982 | 967 |
build_switch_sys init_out [] |
| 983 | 968 |
in |
| 969 |
report ~level:4 (fun fmt -> Format.fprintf fmt "Build step out@."); |
|
| 970 |
|
|
| 984 | 971 |
let update_out = |
| 985 | 972 |
build_switch_sys update_out [] |
| 986 | 973 |
in |
| ... | ... | |
| 991 | 978 |
let update_out = clean_sys update_out in |
| 992 | 979 |
|
| 993 | 980 |
(* Some additional checks *) |
| 994 |
let pp_gl pp_expr = |
|
| 995 |
fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e) |
|
| 996 |
in |
|
| 997 |
let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in |
|
| 998 |
let pp_up fmt up = List.iter (fun (id,e) -> Format.fprintf fmt "%s->%i; " id e.expr_tag) up in |
|
| 999 | 981 |
|
| 1000 | 982 |
if false then |
| 1001 | 983 |
begin |
| ... | ... | |
| 1070 | 1052 |
|
| 1071 | 1053 |
|
| 1072 | 1054 |
(* Iter through the elements and gather them by updates *) |
| 1073 |
let module UpMap = |
|
| 1074 |
struct |
|
| 1075 |
include Map.Make ( |
|
| 1076 |
struct |
|
| 1077 |
type t = (ident * expr) list |
|
| 1078 |
let compare l1 l2 = |
|
| 1079 |
let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in |
|
| 1080 |
compare (proj l1) (proj l2) |
|
| 1081 |
end) |
|
| 1082 |
let pp = pp_up |
|
| 1083 |
end |
|
| 1084 |
in |
|
| 1085 |
let module Guards = struct |
|
| 1086 |
include Set.Make ( |
|
| 1087 |
struct |
|
| 1088 |
type t = (expr * bool) |
|
| 1089 |
let compare l1 l2 = |
|
| 1090 |
let proj (e,b) = e.expr_tag, b in |
|
| 1091 |
compare (proj l1) (proj l2) |
|
| 1092 |
end) |
|
| 1093 |
let pp_short fmt s = pp_gl_short fmt (elements s) |
|
| 1094 |
let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s) |
|
| 1095 |
end |
|
| 1096 |
in |
|
| 1097 | 1055 |
let process sys = |
| 1098 | 1056 |
(* The map will associate to each update up the pair (set, set |
| 1099 | 1057 |
list) where set is the share guards and set list a list of |
| 1100 | 1058 |
disjunctive guards. Each set represents a conjunction of |
| 1101 | 1059 |
expressions. *) |
| 1102 |
let map = |
|
| 1060 |
report ~level:3 (fun fmt -> Format.fprintf fmt "%t@." |
|
| 1061 |
(fun fmt -> List.iter (fun (gl,up) -> |
|
| 1062 |
Format.fprintf fmt "[@[%a@]] -> (%a)@ " |
|
| 1063 |
(pp_guard_list Printers.pp_expr) gl pp_up up) sw_init)); |
|
| 1064 |
|
|
| 1065 |
(* We perform multiple pass to avoid errors *) |
|
| 1066 |
let map = |
|
| 1103 | 1067 |
List.fold_left (fun map (gl,up) -> |
| 1104 | 1068 |
(* creating a new set to describe gl *) |
| 1105 | 1069 |
let new_set = |
| ... | ... | |
| 1110 | 1074 |
in |
| 1111 | 1075 |
(* updating the map with up -> new_set *) |
| 1112 | 1076 |
if UpMap.mem up map then |
| 1113 |
let (shared, disj) = UpMap.find up map in |
|
| 1114 |
let new_shared = Guards.inter shared new_set in |
|
| 1115 |
let remaining_shared = Guards.diff shared new_shared in |
|
| 1116 |
let remaining_new_set = Guards.diff new_set new_shared in |
|
| 1117 |
(* Adding remaining_shared to all elements of disj *) |
|
| 1118 |
let disj' = List.map (fun gs -> Guards.union remaining_shared gs) disj in |
|
| 1119 |
UpMap.add up (new_shared, remaining_new_set::disj') map |
|
| 1077 |
let guard_set = UpMap.find up map in |
|
| 1078 |
UpMap.add up (new_set::guard_set) map |
|
| 1120 | 1079 |
else |
| 1121 |
UpMap.add up (new_set, []) map
|
|
| 1080 |
UpMap.add up [new_set] map
|
|
| 1122 | 1081 |
) UpMap.empty sys |
| 1123 | 1082 |
in |
| 1124 |
let rec mk_binop op l = match l with |
|
| 1125 |
[] -> assert false |
|
| 1126 |
| [e] -> e |
|
| 1127 |
| hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl] |
|
| 1128 |
in |
|
| 1129 |
let gl_as_expr gl = |
|
| 1130 |
let gl = Guards.elements gl in |
|
| 1131 |
let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in |
|
| 1132 |
match gl with |
|
| 1133 |
[] -> [] |
|
| 1134 |
| [e] -> [export e] |
|
| 1135 |
| _ -> |
|
| 1136 |
[mk_binop "&&" |
|
| 1137 |
(List.map export gl)] |
|
| 1083 |
(* Processing the set of guards leading to the same update: return |
|
| 1084 |
conj, disj with conf is a set of guards, and disj a DNF, ie a |
|
| 1085 |
list of set of guards *) |
|
| 1086 |
let map = |
|
| 1087 |
UpMap.map ( |
|
| 1088 |
fun guards -> |
|
| 1089 |
match guards with |
|
| 1090 |
| [] -> Guards.empty, [] (* Nothing *) |
|
| 1091 |
| [s]-> s, [] (* basic case *) |
|
| 1092 |
| hd::tl -> |
|
| 1093 |
let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in |
|
| 1094 |
let remaining = List.map (fun s -> Guards.diff s shared) guards in |
|
| 1095 |
(* If one of them is empty, we can remove the others, otherwise keep them *) |
|
| 1096 |
if List.exists Guards.is_empty remaining then |
|
| 1097 |
shared, [] |
|
| 1098 |
else |
|
| 1099 |
shared, remaining |
|
| 1100 |
) map |
|
| 1138 | 1101 |
in |
| 1139 |
let rec clean_disj disj = |
|
| 1140 |
match disj with |
|
| 1141 |
| [] | [_] -> [] |
|
| 1142 |
| _::_::_ -> ( |
|
| 1143 |
(* First basic version: producing a DNF One can later, (1) |
|
| 1102 |
let rec mk_binop op l = match l with |
|
| 1103 |
[] -> assert false |
|
| 1104 |
| [e] -> e |
|
| 1105 |
| hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl] |
|
| 1106 |
in |
|
| 1107 |
let gl_as_expr gl = |
|
| 1108 |
let gl = Guards.elements gl in |
|
| 1109 |
let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in |
|
| 1110 |
match gl with |
|
| 1111 |
[] -> [] |
|
| 1112 |
| [e] -> [export e] |
|
| 1113 |
| _ -> |
|
| 1114 |
[mk_binop "&&" |
|
| 1115 |
(List.map export gl)] |
|
| 1116 |
in |
|
| 1117 |
let rec clean_disj disj = |
|
| 1118 |
match disj with |
|
| 1119 |
| [] -> [] |
|
| 1120 |
| [_] -> assert false (* A disjunction was a single case can be ignored *) |
|
| 1121 |
| _::_::_ -> ( |
|
| 1122 |
(* First basic version: producing a DNF One can later, (1) |
|
| 1144 | 1123 |
simplify it with z3, or (2) build the compact tree with |
| 1145 | 1124 |
maximum shared subexpression (and simplify it with z3) *) |
| 1146 |
let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in
|
|
| 1147 |
let or_expr = mk_binop "||" elems in
|
|
| 1148 |
[or_expr]
|
|
| 1125 |
let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in |
|
| 1126 |
let or_expr = mk_binop "||" elems in |
|
| 1127 |
[or_expr] |
|
| 1149 | 1128 |
|
| 1150 | 1129 |
|
| 1151 |
(* TODO disj*)
|
|
| 1152 |
(* get the item that occurs in most case *)
|
|
| 1153 |
(* List.fold_left (fun accu s ->
|
|
| 1154 |
* List.fold_left (fun accu (e,b) ->
|
|
| 1155 |
* if List.mem_assoc (e.expr_tag, b)
|
|
| 1156 |
* ) accu (Guards.elements s)
|
|
| 1157 |
* ) [] disj *)
|
|
| 1130 |
(* TODO disj*) |
|
| 1131 |
(* get the item that occurs in most case *) |
|
| 1132 |
(* List.fold_left (fun accu s -> |
|
| 1133 |
* List.fold_left (fun accu (e,b) -> |
|
| 1134 |
* if List.mem_assoc (e.expr_tag, b) |
|
| 1135 |
* ) accu (Guards.elements s) |
|
| 1136 |
* ) [] disj *) |
|
| 1158 | 1137 |
|
| 1159 |
) |
|
| 1138 |
) |
|
| 1139 |
in |
|
| 1140 |
if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map); |
|
| 1141 |
UpMap.fold (fun up (common, disj) accu -> |
|
| 1142 |
if !seal_debug then |
|
| 1143 |
Format.eprintf |
|
| 1144 |
"Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@." |
|
| 1145 |
Guards.pp_short common |
|
| 1146 |
(fprintf_list ~sep:";@ " Guards.pp_long) disj |
|
| 1147 |
UpMap.pp up; |
|
| 1148 |
let disj = clean_disj disj in |
|
| 1149 |
let guard_expr = (gl_as_expr common)@disj in |
|
| 1150 |
|
|
| 1151 |
((match guard_expr with |
|
| 1152 |
| [] -> None |
|
| 1153 |
| _ -> Some (mk_binop "&&" guard_expr)), up)::accu |
|
| 1154 |
) map [] |
|
| 1155 |
|
|
| 1160 | 1156 |
in |
| 1161 |
if !debug then Format.eprintf "Map: %i elements@." (UpMap.cardinal map); |
|
| 1162 |
UpMap.fold (fun up (common, disj) accu -> |
|
| 1163 |
if !debug then |
|
| 1164 |
Format.eprintf |
|
| 1165 |
"Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@." |
|
| 1166 |
Guards.pp_short common |
|
| 1167 |
(fprintf_list ~sep:";@ " Guards.pp_long) disj |
|
| 1168 |
UpMap.pp up; |
|
| 1169 |
let disj = clean_disj disj in |
|
| 1170 |
let guard_expr = (gl_as_expr common)@disj in |
|
| 1171 |
|
|
| 1172 |
((match guard_expr with |
|
| 1173 |
| [] -> None |
|
| 1174 |
| _ -> Some (mk_binop "&&" guard_expr)), up)::accu |
|
| 1175 |
) map [] |
|
| 1176 | 1157 |
|
| 1177 |
in |
|
| 1178 |
process sw_init, process sw_sys, process init_out, process update_out |
|
| 1158 |
|
|
| 1159 |
|
|
| 1160 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@."); |
|
| 1161 |
let sw_init = process sw_init in |
|
| 1162 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@."); |
|
| 1163 |
let sw_sys = process sw_sys in |
|
| 1164 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@."); |
|
| 1165 |
let init_out = process init_out in |
|
| 1166 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@."); |
|
| 1167 |
let update_out = process update_out in |
|
| 1168 |
sw_init , sw_sys, init_out, update_out |
|
Also available in: Unified diff
Seal: solved issue with guards merging