Revision a0c92fa8 src/tools/seal/seal_extract.ml
src/tools/seal/seal_extract.ml | ||
---|---|---|
91 | 91 |
* let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *) |
92 | 92 |
|
93 | 93 |
let rec e2ze e = |
94 |
(* Format.eprintf "e2ze %a: %a@." Printers.pp_expr e Types.print_ty e.expr_type; *) |
|
94 | 95 |
if mem_expr e then ( |
95 | 96 |
get_zexpr e |
96 | 97 |
) |
... | ... | |
121 | 122 |
) |
122 | 123 |
) |
123 | 124 |
| Expr_appl (id,args, None) (* no reset *) -> |
124 |
let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in |
|
125 |
let el = Corelang.expr_list_of_expr args in |
|
126 |
|
|
127 |
let eltyp = List.map (fun e -> e.expr_type) el in |
|
128 |
let elv = List.map e2ze el in |
|
129 |
let z3e = Zustre_common.horn_basic_app id elv (eltyp, e.expr_type) in |
|
125 | 130 |
add_expr e z3e; |
126 | 131 |
z3e |
127 | 132 |
| Expr_tuple [e] -> |
... | ... | |
597 | 602 |
expr.expr_loc |
598 | 603 |
(Expr_appl(id, deelem e, None)) |
599 | 604 |
in |
605 |
let new_e = { new_e with expr_type = expr.expr_type; expr_clock = expr.expr_clock } in |
|
600 | 606 |
guards, |
601 | 607 |
Expr (Corelang.partial_eval new_e) |
602 | 608 |
) args |
... | ... | |
905 | 911 |
"@[<v 2>===> @[%t@ @]@]@ @]@ " |
906 | 912 |
(fun fmt -> List.iter (fun (gl,up) -> |
907 | 913 |
Format.fprintf fmt "[@[%a@]] -> (%a)@ " |
908 |
(pp_guard_list Printers.pp_expr) gl pp_up up) res);
|
|
914 |
(pp_guard_list Printers.pp_expr) gl (pp_up Printers.pp_expr) up) res);
|
|
909 | 915 |
|
910 | 916 |
)); |
911 | 917 |
res |
912 | 918 |
|
913 | 919 |
|
914 |
|
|
915 |
(* Take a normalized node and extract a list of switches: (cond, |
|
916 |
update) meaning "if cond then update" where update shall define all |
|
917 |
node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *) |
|
918 |
let node_as_switched_sys consts (mems:var_decl list) nd = |
|
919 |
Z3.Params.update_param_value !ctx "timeout" "10000"; |
|
920 |
let build_environement consts (mems:var_decl list) nd = |
|
921 |
|
|
922 |
Z3.Params.update_param_value !ctx "timeout" "10000"; |
|
920 | 923 |
|
921 | 924 |
|
922 | 925 |
(* rescheduling node: has been scheduled already, no need to protect |
... | ... | |
1018 | 1021 |
(pp_guard_expr pp_elem)) mdefs |
1019 | 1022 |
)) |
1020 | 1023 |
mem_defs); |
1021 |
(* Format.eprintf "Split init@."; *) |
|
1022 |
let init_defs, update_defs = |
|
1023 |
split_init mem_defs |
|
1024 |
mem_defs, output_defs |
|
1025 |
|
|
1026 |
|
|
1027 |
(* Iter through the elements and gather them by updates *) |
|
1028 |
let merge_updates sys = |
|
1029 |
(* The map will associate to each update up the pair (set, set |
|
1030 |
list) where set is the share guards and set list a list of |
|
1031 |
disjunctive guards. Each set represents a conjunction of |
|
1032 |
expressions. *) |
|
1033 |
|
|
1034 |
(* We perform multiple pass to avoid errors *) |
|
1035 |
let map = |
|
1036 |
List.fold_left (fun map (gl,up) -> |
|
1037 |
(* creating a new set to describe gl *) |
|
1038 |
let new_set = |
|
1039 |
List.fold_left |
|
1040 |
(fun set g -> Guards.add g set) |
|
1041 |
Guards.empty |
|
1042 |
gl |
|
1043 |
in |
|
1044 |
(* updating the map with up -> new_set *) |
|
1045 |
if UpMap.mem up map then |
|
1046 |
let guard_set = UpMap.find up map in |
|
1047 |
UpMap.add up (new_set::guard_set) map |
|
1048 |
else |
|
1049 |
UpMap.add up [new_set] map |
|
1050 |
) UpMap.empty sys |
|
1024 | 1051 |
in |
1025 |
let init_out, update_out = |
|
1026 |
split_init output_defs |
|
1052 |
|
|
1053 |
(* Processing the set of guards leading to the same update: return |
|
1054 |
conj, disj with conf is a set of guards, and disj a DNF, ie a |
|
1055 |
list of set of guards *) |
|
1056 |
let map = |
|
1057 |
UpMap.map ( |
|
1058 |
fun guards -> |
|
1059 |
match guards with |
|
1060 |
| [] -> Guards.empty, [] (* Nothing *) |
|
1061 |
| [s]-> s, [] (* basic case *) |
|
1062 |
| hd::tl -> |
|
1063 |
let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in |
|
1064 |
let remaining = List.map (fun s -> Guards.diff s shared) guards in |
|
1065 |
(* If one of them is empty, we can remove the others, otherwise keep them *) |
|
1066 |
if List.exists Guards.is_empty remaining then |
|
1067 |
shared, [] |
|
1068 |
else |
|
1069 |
shared, remaining |
|
1070 |
) map |
|
1027 | 1071 |
in |
1028 |
report ~level:3 |
|
1029 |
(fun fmt -> |
|
1030 |
Format.fprintf fmt |
|
1031 |
"@[<v 0>Init:@ %a@]@." |
|
1032 |
(Utils.fprintf_list ~sep:"@ " |
|
1033 |
(fun fmt (m,mdefs) -> |
|
1034 |
Format.fprintf fmt |
|
1035 |
"%s -> @[<v 0>[%a@] ]@ " |
|
1036 |
m |
|
1037 |
(Utils.fprintf_list ~sep:"@ " |
|
1038 |
(pp_guard_expr pp_elem)) mdefs |
|
1039 |
)) |
|
1040 |
init_defs); |
|
1041 |
report ~level:3 |
|
1042 |
(fun fmt -> |
|
1043 |
Format.fprintf fmt |
|
1044 |
"@[<v 0>Step:@ %a@]@." |
|
1045 |
(Utils.fprintf_list ~sep:"@ " |
|
1046 |
(fun fmt (m,mdefs) -> |
|
1047 |
Format.fprintf fmt |
|
1048 |
"%s -> @[<v 0>[%a@] ]@ " |
|
1049 |
m |
|
1050 |
(Utils.fprintf_list ~sep:"@ " |
|
1051 |
(pp_guard_expr pp_elem)) mdefs |
|
1052 |
)) |
|
1053 |
update_defs); |
|
1054 |
(* Format.eprintf "Build init@."; *) |
|
1055 |
|
|
1056 |
report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ...@."); |
|
1057 |
let sw_init= |
|
1058 |
build_switch_sys init_defs [] |
|
1072 |
let rec mk_binop op l = match l with |
|
1073 |
[] -> assert false |
|
1074 |
| [e] -> e |
|
1075 |
| hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl] |
|
1059 | 1076 |
in |
1060 |
(* Format.eprintf "Build step@."; *) |
|
1061 |
let sw_sys = |
|
1062 |
build_switch_sys update_defs [] |
|
1077 |
let gl_as_expr gl = |
|
1078 |
let gl = Guards.elements gl in |
|
1079 |
let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in |
|
1080 |
match gl with |
|
1081 |
[] -> [] |
|
1082 |
| [e] -> [export e] |
|
1083 |
| _ -> |
|
1084 |
[mk_binop "&&" |
|
1085 |
(List.map export gl)] |
|
1063 | 1086 |
in |
1064 |
report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ... done@."); |
|
1087 |
let rec clean_disj disj = |
|
1088 |
match disj with |
|
1089 |
| [] -> [] |
|
1090 |
| [_] -> assert false (* A disjunction with a single case can be ignored *) |
|
1091 |
| _::_::_ -> ( |
|
1092 |
(* First basic version: producing a DNF One can later, (1) |
|
1093 |
simplify it with z3, or (2) build the compact tree with |
|
1094 |
maximum shared subexpression (and simplify it with z3) *) |
|
1095 |
let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in |
|
1096 |
let or_expr = mk_binop "||" elems in |
|
1097 |
[or_expr] |
|
1065 | 1098 |
|
1066 |
report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ...@."); |
|
1067 |
let init_out = |
|
1068 |
build_switch_sys init_out [] |
|
1069 |
in |
|
1070 |
(* report ~level:1 (fun fmt -> Format.fprintf fmt "Build step out@."); *) |
|
1071 | 1099 |
|
1072 |
let update_out = |
|
1073 |
build_switch_sys update_out [] |
|
1100 |
(* TODO disj*) |
|
1101 |
(* get the item that occurs in most case *) |
|
1102 |
(* List.fold_left (fun accu s -> |
|
1103 |
* List.fold_left (fun accu (e,b) -> |
|
1104 |
* if List.mem_assoc (e.expr_tag, b) |
|
1105 |
* ) accu (Guards.elements s) |
|
1106 |
* ) [] disj *) |
|
1107 |
|
|
1108 |
) |
|
1074 | 1109 |
in |
1075 |
report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ... done@."); |
|
1110 |
if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map); |
|
1111 |
UpMap.fold (fun up (common, disj) accu -> |
|
1112 |
if !seal_debug then |
|
1113 |
report ~level:6 (fun fmt -> Format.fprintf fmt |
|
1114 |
"Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@." |
|
1115 |
Guards.pp_short common |
|
1116 |
(fprintf_list ~sep:";@ " Guards.pp_long) disj |
|
1117 |
UpMap.pp up); |
|
1118 |
let disj = clean_disj disj in |
|
1119 |
let guard_expr = (gl_as_expr common)@disj in |
|
1120 |
|
|
1121 |
((match guard_expr with |
|
1122 |
| [] -> None |
|
1123 |
| _ -> Some (mk_binop "&&" guard_expr)), up)::accu |
|
1124 |
) map [] |
|
1125 |
|
|
1126 |
|
|
1127 |
|
|
1076 | 1128 |
|
1077 |
report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ...@."); |
|
1129 |
(* Take a normalized node and extract a list of switches: (cond, |
|
1130 |
update) meaning "if cond then update" where update shall define all |
|
1131 |
node memories. Everything as to be expressed over inputs or |
|
1132 |
memories, intermediate variables are removed through inlining *) |
|
1133 |
let node_as_switched_sys consts (mems:var_decl list) nd = |
|
1134 |
let mem_defs, output_defs = build_environement consts mems nd in |
|
1135 |
|
|
1136 |
let init_defs, update_defs = split_init mem_defs in |
|
1137 |
let init_out, update_out = split_init output_defs in |
|
1138 |
|
|
1139 |
report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 0>Init:@ %a@ Step:@ %a@]@." |
|
1140 |
(pp_assign_map pp_elem) init_defs |
|
1141 |
(pp_assign_map pp_elem) update_defs); |
|
1142 |
|
|
1143 |
|
|
1144 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1145 |
"init/step as a switched system ...@."); |
|
1146 |
let sw_init= build_switch_sys init_defs [] in |
|
1147 |
let sw_sys = build_switch_sys update_defs [] in |
|
1148 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1149 |
"init/step as a switched system ... done@."); |
|
1150 |
|
|
1151 |
|
|
1152 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1153 |
"output function as a switched system ...@."); |
|
1154 |
let init_out = build_switch_sys init_out [] in |
|
1155 |
let update_out = build_switch_sys update_out [] in |
|
1156 |
|
|
1157 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1158 |
"output function as a switched system ... done@."); |
|
1159 |
|
|
1160 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1161 |
"removing dead branches and merging remaining ...@."); |
|
1078 | 1162 |
|
1079 | 1163 |
let sw_init = clean_sys sw_init in |
1080 | 1164 |
let sw_sys = clean_sys sw_sys in |
1081 | 1165 |
let init_out = clean_sys init_out in |
1082 | 1166 |
let update_out = clean_sys update_out in |
1083 |
report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ... done@."); |
|
1167 |
|
|
1168 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@."); |
|
1169 |
let sw_init = merge_updates sw_init in |
|
1170 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@."); |
|
1171 |
let sw_sys = merge_updates sw_sys in |
|
1172 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@."); |
|
1173 |
let init_out = merge_updates init_out in |
|
1174 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@."); |
|
1175 |
let update_out = merge_updates update_out in |
|
1176 |
report ~level:1 (fun fmt -> |
|
1177 |
Format.fprintf fmt "removing dead branches and merging remaining ... done@."); |
|
1178 |
|
|
1179 |
sw_init , sw_sys, init_out, update_out |
|
1180 |
|
|
1181 |
|
|
1182 |
let fun_as_switched_sys consts nd = |
|
1183 |
let _, update_out = build_environement consts [] nd in |
|
1184 |
|
|
1185 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1186 |
"output function as a switched system ...@."); |
|
1187 |
let update_out = build_switch_sys update_out [] in |
|
1188 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1189 |
"output function as a switched system ... done@."); |
|
1190 |
|
|
1191 |
report ~level:1 (fun fmt -> Format.fprintf fmt |
|
1192 |
"removing dead branches and merging remaining ...@."); |
|
1193 |
let update_out = clean_sys update_out in |
|
1194 |
let update_out = merge_updates update_out in |
|
1195 |
report ~level:1 (fun fmt -> |
|
1196 |
Format.fprintf fmt "removing dead branches and merging remaining ... done@."); |
|
1197 |
|
|
1198 |
update_out |
|
1199 |
|
|
1200 |
|
|
1201 |
|
|
1202 |
|
|
1203 |
|
|
1204 |
(* Some code that was used to check for duplicate entries in guards. |
|
1205 |
|
|
1084 | 1206 |
|
1085 | 1207 |
(* Some additional checks *) |
1086 | 1208 |
|
... | ... | |
1156 | 1278 |
end; |
1157 | 1279 |
|
1158 | 1280 |
|
1159 |
(* Iter through the elements and gather them by updates *) |
|
1160 |
let process sys = |
|
1161 |
(* The map will associate to each update up the pair (set, set |
|
1162 |
list) where set is the share guards and set list a list of |
|
1163 |
disjunctive guards. Each set represents a conjunction of |
|
1164 |
expressions. *) |
|
1165 |
report ~level:3 (fun fmt -> Format.fprintf fmt "%t@." |
|
1166 |
(fun fmt -> List.iter (fun (gl,up) -> |
|
1167 |
Format.fprintf fmt "[@[%a@]] -> (%a)@ " |
|
1168 |
(pp_guard_list Printers.pp_expr) gl pp_up up) sw_init)); |
|
1169 |
|
|
1170 |
(* We perform multiple pass to avoid errors *) |
|
1171 |
let map = |
|
1172 |
List.fold_left (fun map (gl,up) -> |
|
1173 |
(* creating a new set to describe gl *) |
|
1174 |
let new_set = |
|
1175 |
List.fold_left |
|
1176 |
(fun set g -> Guards.add g set) |
|
1177 |
Guards.empty |
|
1178 |
gl |
|
1179 |
in |
|
1180 |
(* updating the map with up -> new_set *) |
|
1181 |
if UpMap.mem up map then |
|
1182 |
let guard_set = UpMap.find up map in |
|
1183 |
UpMap.add up (new_set::guard_set) map |
|
1184 |
else |
|
1185 |
UpMap.add up [new_set] map |
|
1186 |
) UpMap.empty sys |
|
1187 |
in |
|
1188 |
(* Processing the set of guards leading to the same update: return |
|
1189 |
conj, disj with conf is a set of guards, and disj a DNF, ie a |
|
1190 |
list of set of guards *) |
|
1191 |
let map = |
|
1192 |
UpMap.map ( |
|
1193 |
fun guards -> |
|
1194 |
match guards with |
|
1195 |
| [] -> Guards.empty, [] (* Nothing *) |
|
1196 |
| [s]-> s, [] (* basic case *) |
|
1197 |
| hd::tl -> |
|
1198 |
let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in |
|
1199 |
let remaining = List.map (fun s -> Guards.diff s shared) guards in |
|
1200 |
(* If one of them is empty, we can remove the others, otherwise keep them *) |
|
1201 |
if List.exists Guards.is_empty remaining then |
|
1202 |
shared, [] |
|
1203 |
else |
|
1204 |
shared, remaining |
|
1205 |
) map |
|
1206 |
in |
|
1207 |
let rec mk_binop op l = match l with |
|
1208 |
[] -> assert false |
|
1209 |
| [e] -> e |
|
1210 |
| hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl] |
|
1211 |
in |
|
1212 |
let gl_as_expr gl = |
|
1213 |
let gl = Guards.elements gl in |
|
1214 |
let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in |
|
1215 |
match gl with |
|
1216 |
[] -> [] |
|
1217 |
| [e] -> [export e] |
|
1218 |
| _ -> |
|
1219 |
[mk_binop "&&" |
|
1220 |
(List.map export gl)] |
|
1221 |
in |
|
1222 |
let rec clean_disj disj = |
|
1223 |
match disj with |
|
1224 |
| [] -> [] |
|
1225 |
| [_] -> assert false (* A disjunction was a single case can be ignored *) |
|
1226 |
| _::_::_ -> ( |
|
1227 |
(* First basic version: producing a DNF One can later, (1) |
|
1228 |
simplify it with z3, or (2) build the compact tree with |
|
1229 |
maximum shared subexpression (and simplify it with z3) *) |
|
1230 |
let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in |
|
1231 |
let or_expr = mk_binop "||" elems in |
|
1232 |
[or_expr] |
|
1233 |
|
|
1234 |
|
|
1235 |
(* TODO disj*) |
|
1236 |
(* get the item that occurs in most case *) |
|
1237 |
(* List.fold_left (fun accu s -> |
|
1238 |
* List.fold_left (fun accu (e,b) -> |
|
1239 |
* if List.mem_assoc (e.expr_tag, b) |
|
1240 |
* ) accu (Guards.elements s) |
|
1241 |
* ) [] disj *) |
|
1242 |
|
|
1243 |
) |
|
1244 |
in |
|
1245 |
if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map); |
|
1246 |
UpMap.fold (fun up (common, disj) accu -> |
|
1247 |
if !seal_debug then |
|
1248 |
report ~level:6 (fun fmt -> Format.fprintf fmt |
|
1249 |
"Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@." |
|
1250 |
Guards.pp_short common |
|
1251 |
(fprintf_list ~sep:";@ " Guards.pp_long) disj |
|
1252 |
UpMap.pp up); |
|
1253 |
let disj = clean_disj disj in |
|
1254 |
let guard_expr = (gl_as_expr common)@disj in |
|
1255 |
|
|
1256 |
((match guard_expr with |
|
1257 |
| [] -> None |
|
1258 |
| _ -> Some (mk_binop "&&" guard_expr)), up)::accu |
|
1259 |
) map [] |
|
1260 |
|
|
1261 |
in |
|
1262 |
|
|
1263 |
|
|
1264 |
|
|
1265 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@."); |
|
1266 |
let sw_init = process sw_init in |
|
1267 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@."); |
|
1268 |
let sw_sys = process sw_sys in |
|
1269 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@."); |
|
1270 |
let init_out = process init_out in |
|
1271 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@."); |
|
1272 |
let update_out = process update_out in |
|
1273 |
sw_init , sw_sys, init_out, update_out |
|
1281 |
*) |
Also available in: Unified diff