Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/backends/EMF/EMF_backend.ml | ||
---|---|---|
101 | 101 |
open Lustre_types |
102 | 102 |
open Machine_code_types |
103 | 103 |
open Machine_code_common |
104 |
open Format
|
|
104 |
open Format |
|
105 | 105 |
open EMF_common |
106 |
|
|
106 | 107 |
exception Unhandled of string |
107 | 108 |
|
108 | 109 |
module ISet = Utils.ISet |
109 |
let fprintf_list = Utils.fprintf_list |
|
110 |
|
|
111 | 110 |
|
111 |
let fprintf_list = Utils.fprintf_list |
|
112 | 112 |
|
113 | 113 |
(**********************************************) |
114 | 114 |
(* Utility functions: arrow and lustre expr *) |
... | ... | |
118 | 118 |
-> false *) |
119 | 119 |
let is_arrow_fun m i = |
120 | 120 |
match Corelang.get_instr_desc i with |
121 |
| MStep ([_], i, vl) -> |
|
122 |
( |
|
123 |
try |
|
124 |
let name = (get_node_def i m).node_id in |
|
125 |
match name, vl with |
|
126 |
| "_arrow", [v1; v2] -> ( |
|
127 |
match v1.value_desc, v2.value_desc with |
|
128 |
| Cst c1, Cst c2 -> |
|
129 |
if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then |
|
130 |
true |
|
131 |
else |
|
132 |
assert false (* only handle true -> false *) |
|
133 |
| _ -> assert false |
|
134 |
) |
|
135 |
|
|
136 |
| _ -> false |
|
137 |
with |
|
138 |
| Not_found -> false (* Not declared (should have been detected now, or |
|
139 |
imported node) *) |
|
140 |
) |
|
121 |
| MStep ([ _ ], i, vl) -> ( |
|
122 |
try |
|
123 |
let name = (get_node_def i m).node_id in |
|
124 |
match name, vl with |
|
125 |
| "_arrow", [ v1; v2 ] -> ( |
|
126 |
match v1.value_desc, v2.value_desc with |
|
127 |
| Cst c1, Cst c2 -> |
|
128 |
if |
|
129 |
c1 = Corelang.const_of_bool true |
|
130 |
&& c2 = Corelang.const_of_bool false |
|
131 |
then true |
|
132 |
else assert false |
|
133 |
(* only handle true -> false *) |
|
134 |
| _ -> assert false) |
|
135 |
| _ -> false |
|
136 |
with Not_found -> |
|
137 |
false |
|
138 |
(* Not declared (should have been detected now, or |
|
139 |
imported node) *)) |
|
141 | 140 |
| _ -> false |
142 |
|
|
143 |
|
|
144 |
|
|
141 |
|
|
145 | 142 |
let is_resetable_fun lustre_eq = |
146 | 143 |
(* We extract the clock if it exist from the original lustre equation *) |
147 | 144 |
match lustre_eq with |
148 | 145 |
| Some eq -> ( |
149 |
match eq.eq_rhs.expr_desc with |
|
150 |
| Expr_appl(_,_,reset) -> ( |
|
151 |
match reset with None -> false | Some _ -> true |
|
152 |
) |
|
153 |
| Expr_arrow _ -> true |
|
154 |
| _ -> Format.eprintf "reseting expr %a@.@?" Printers.pp_expr eq.eq_rhs; assert false |
|
155 |
) |
|
156 |
| None -> assert false (* should have been assigned to an original lustre equation *) |
|
146 |
match eq.eq_rhs.expr_desc with |
|
147 |
| Expr_appl (_, _, reset) -> ( |
|
148 |
match reset with None -> false | Some _ -> true) |
|
149 |
| Expr_arrow _ -> true |
|
150 |
| _ -> |
|
151 |
Format.eprintf "reseting expr %a@.@?" Printers.pp_expr eq.eq_rhs; |
|
152 |
assert false) |
|
153 |
| None -> assert false |
|
154 |
(* should have been assigned to an original lustre equation *) |
|
157 | 155 |
|
158 | 156 |
(**********************************************) |
159 | 157 |
(* Printing machine code as EMF *) |
160 | 158 |
(**********************************************) |
161 | 159 |
|
162 |
|
|
163 |
|
|
164 | 160 |
let branch_cpt = ref 0 |
161 |
|
|
165 | 162 |
let get_instr_id fmt i = |
166 | 163 |
match Corelang.get_instr_desc i with |
167 |
| MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
|
|
164 |
| MLocalAssign (lhs, _) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
|
|
168 | 165 |
| MSetReset i | MNoReset i -> fprintf fmt "%s" (reset_name i) |
169 | 166 |
(* TODO: handle clear_reset *) |
170 | 167 |
| MClearReset -> () |
171 |
| MBranch _ -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt |
|
168 |
| MBranch _ -> |
|
169 |
incr branch_cpt; |
|
170 |
fprintf fmt "branch_%i" !branch_cpt |
|
172 | 171 |
| MStep (outs, id, _) -> |
173 |
print_protect fmt |
|
174 |
(fun fmt -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id) |
|
175 |
| _ -> () (* No name *) |
|
172 |
print_protect fmt (fun fmt -> |
|
173 |
fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id) |
|
174 |
| _ -> () |
|
175 |
(* No name *) |
|
176 | 176 |
|
177 | 177 |
let rec branch_block_vars m il = |
178 | 178 |
List.fold_left |
179 | 179 |
(fun (accu_all_def, accu_def, accu_read) i -> |
180 |
let all_defined_vars, common_def_vars, read_vars = branch_instr_vars m i in |
|
181 |
ISet.union accu_all_def all_defined_vars, |
|
182 |
ISet.union accu_def common_def_vars, |
|
183 |
VSet.union accu_read read_vars) |
|
184 |
(ISet.empty, ISet.empty, VSet.empty) il |
|
185 |
|
|
180 |
let all_defined_vars, common_def_vars, read_vars = |
|
181 |
branch_instr_vars m i |
|
182 |
in |
|
183 |
( ISet.union accu_all_def all_defined_vars, |
|
184 |
ISet.union accu_def common_def_vars, |
|
185 |
VSet.union accu_read read_vars )) |
|
186 |
(ISet.empty, ISet.empty, VSet.empty) |
|
187 |
il |
|
188 |
|
|
186 | 189 |
and branch_instr_vars m i = |
187 | 190 |
(* Returns all_outputs, outputs, inputs of the instruction. It is |
188 | 191 |
only called on MBranch instructions but evaluate recursively |
... | ... | |
193 | 196 |
|
194 | 197 |
The set "All outputs" is used to filter out input variables |
195 | 198 |
belong to that set. *) |
196 |
|
|
197 | 199 |
match Corelang.get_instr_desc i with |
198 |
| MLocalAssign (var,expr) |
|
199 |
| MStateAssign (var,expr) -> ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr |
|
200 |
| MStep (vars, f, args) -> |
|
201 |
let is_stateful = List.mem_assoc f m.minstances in |
|
202 |
let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in |
|
203 |
let args_vars = |
|
204 |
List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args in |
|
205 |
|
|
206 |
lhs, lhs, |
|
207 |
( |
|
208 |
if is_stateful && is_resetable_fun i.lustre_eq then |
|
209 |
let reset_var = |
|
210 |
let loc = Location.dummy_loc in |
|
211 |
Corelang.mkvar_decl loc |
|
212 |
(reset_name f, |
|
213 |
Corelang.mktyp loc Tydec_bool, Corelang.mkclock loc Ckdec_any, |
|
214 |
false, |
|
215 |
None, |
|
216 |
None) |
|
217 |
in |
|
218 |
VSet.add reset_var args_vars |
|
219 |
else |
|
220 |
args_vars |
|
221 |
) |
|
222 |
| MBranch (g,(_,hd_il)::tl) -> (* We focus on variables defined in all branches *) |
|
223 |
let read_guard = get_expr_vars g in |
|
224 |
(* Bootstrapping with first item *) |
|
225 |
let all_def_vars_hd, def_vars_hd, read_vars_hd = branch_block_vars m hd_il in |
|
226 |
let all_def_vars, def_vars, read_vars = |
|
227 |
List.fold_left |
|
228 |
(fun (all_def_vars, def_vars, read_vars) (_, il) -> |
|
229 |
(* We accumulate reads but intersect writes *) |
|
230 |
let all_writes_il, writes_il, reads_il = branch_block_vars m il in |
|
231 |
ISet.union all_def_vars all_writes_il, |
|
232 |
ISet.inter def_vars writes_il, |
|
233 |
VSet.union read_vars reads_il |
|
234 |
) |
|
235 |
(all_def_vars_hd, def_vars_hd, read_vars_hd) |
|
236 |
tl |
|
237 |
in |
|
238 |
(* all_def_vars correspond to variables written or defined in one |
|
239 |
of the branch. It may happen that a variable is defined in one |
|
240 |
but not in the other, because of reset for example. |
|
241 |
|
|
242 |
def_vars are variables defined in all branches. *) |
|
243 |
|
|
244 |
|
|
245 |
all_def_vars, def_vars, VSet.union read_guard read_vars |
|
246 |
| MBranch _ -> assert false (* branch instruction should admit at least one case *) |
|
247 |
| MSetReset ni |
|
248 |
| MNoReset ni -> |
|
249 |
let write = ISet.singleton (reset_name ni) in |
|
250 |
write, write, VSet.empty |
|
200 |
| MLocalAssign (var, expr) | MStateAssign (var, expr) -> |
|
201 |
ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr |
|
202 |
| MStep (vars, f, args) -> |
|
203 |
let is_stateful = List.mem_assoc f m.minstances in |
|
204 |
let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in |
|
205 |
let args_vars = |
|
206 |
List.fold_left |
|
207 |
(fun accu v -> VSet.union accu (get_expr_vars v)) |
|
208 |
VSet.empty args |
|
209 |
in |
|
210 |
|
|
211 |
( lhs, |
|
212 |
lhs, |
|
213 |
if is_stateful && is_resetable_fun i.lustre_eq then |
|
214 |
let reset_var = |
|
215 |
let loc = Location.dummy_loc in |
|
216 |
Corelang.mkvar_decl loc |
|
217 |
( reset_name f, |
|
218 |
Corelang.mktyp loc Tydec_bool, |
|
219 |
Corelang.mkclock loc Ckdec_any, |
|
220 |
false, |
|
221 |
None, |
|
222 |
None ) |
|
223 |
in |
|
224 |
VSet.add reset_var args_vars |
|
225 |
else args_vars ) |
|
226 |
| MBranch (g, (_, hd_il) :: tl) -> |
|
227 |
(* We focus on variables defined in all branches *) |
|
228 |
let read_guard = get_expr_vars g in |
|
229 |
(* Bootstrapping with first item *) |
|
230 |
let all_def_vars_hd, def_vars_hd, read_vars_hd = |
|
231 |
branch_block_vars m hd_il |
|
232 |
in |
|
233 |
let all_def_vars, def_vars, read_vars = |
|
234 |
List.fold_left |
|
235 |
(fun (all_def_vars, def_vars, read_vars) (_, il) -> |
|
236 |
(* We accumulate reads but intersect writes *) |
|
237 |
let all_writes_il, writes_il, reads_il = branch_block_vars m il in |
|
238 |
( ISet.union all_def_vars all_writes_il, |
|
239 |
ISet.inter def_vars writes_il, |
|
240 |
VSet.union read_vars reads_il )) |
|
241 |
(all_def_vars_hd, def_vars_hd, read_vars_hd) |
|
242 |
tl |
|
243 |
in |
|
244 |
|
|
245 |
(* all_def_vars correspond to variables written or defined in one |
|
246 |
of the branch. It may happen that a variable is defined in one |
|
247 |
but not in the other, because of reset for example. |
|
248 |
|
|
249 |
def_vars are variables defined in all branches. *) |
|
250 |
all_def_vars, def_vars, VSet.union read_guard read_vars |
|
251 |
| MBranch _ -> |
|
252 |
assert false (* branch instruction should admit at least one case *) |
|
253 |
| MSetReset ni | MNoReset ni -> |
|
254 |
let write = ISet.singleton (reset_name ni) in |
|
255 |
write, write, VSet.empty |
|
251 | 256 |
(* TODO: handle clear_reset and reset flag *) |
252 | 257 |
| MClearReset | MResetAssign _ -> ISet.empty, ISet.empty, VSet.empty |
253 |
| MSpec _ | MComment _ -> assert false (* not available for EMF output *) |
|
254 |
|
|
258 |
| MSpec _ | MComment _ -> assert false |
|
259 |
(* not available for EMF output *) |
|
260 |
|
|
255 | 261 |
(* A kind of super join_guards: all MBranch are postponed and sorted by |
256 | 262 |
guards so they can be easier merged *) |
257 | 263 |
let merge_branches instrs = |
258 | 264 |
let instrs, branches = |
259 |
List.fold_right (fun i (il, branches) -> |
|
260 |
match Corelang.get_instr_desc i with |
|
261 |
MBranch _ -> il, i::branches |
|
262 |
| _ -> i::il, branches |
|
263 |
) instrs ([],[]) |
|
265 |
List.fold_right |
|
266 |
(fun i (il, branches) -> |
|
267 |
match Corelang.get_instr_desc i with |
|
268 |
| MBranch _ -> il, i :: branches |
|
269 |
| _ -> i :: il, branches) |
|
270 |
instrs ([], []) |
|
264 | 271 |
in |
265 | 272 |
let sorting_branches b1 b2 = |
266 | 273 |
match Corelang.get_instr_desc b1, Corelang.get_instr_desc b2 with |
267 |
| MBranch(g1, _), MBranch(g2, _) -> |
|
268 |
compare g1 g2 |
|
274 |
| MBranch (g1, _), MBranch (g2, _) -> compare g1 g2 |
|
269 | 275 |
| _ -> assert false |
270 | 276 |
in |
271 | 277 |
let sorted_branches = List.sort sorting_branches branches in |
272 |
instrs @ (join_guards_list sorted_branches)
|
|
273 |
|
|
278 |
instrs @ join_guards_list sorted_branches
|
|
279 |
|
|
274 | 280 |
let rec pp_emf_instr m fmt i = |
275 | 281 |
let pp_content fmt i = |
276 | 282 |
match Corelang.get_instr_desc i with |
277 |
| MLocalAssign(lhs, expr) ->
|
|
278 |
begin match expr.value_desc with
|
|
283 |
| MLocalAssign (lhs, expr) -> (
|
|
284 |
match expr.value_desc with
|
|
279 | 285 |
| Fun (fun_id, vl) -> |
280 |
(* Thanks to normalization, vl shall only contain constant or |
|
281 |
local/state vars but not calls to other functions *) |
|
282 |
fprintf fmt "\"kind\": \"operator\",@ "; |
|
283 |
fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs; |
|
284 |
fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]" |
|
285 |
fun_id |
|
286 |
(pp_emf_cst_or_var_list m) vl |
|
287 |
| Array _ | Access _ | Power _ |
|
288 |
| Cst _ |
|
289 |
| Var _ -> |
|
290 |
fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a" |
|
291 |
pp_var_name lhs |
|
292 |
(pp_emf_cst_or_var m) expr |
|
286 |
(* |
|
287 |
Thanks to normalization, vl shall only contain constant or |
|
288 |
local/state vars but not calls to other functions *) |
|
289 |
fprintf fmt "\"kind\": \"operator\",@ "; |
|
290 |
fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs; |
|
291 |
fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]" fun_id |
|
292 |
(pp_emf_cst_or_var_list m) vl |
|
293 |
| Array _ | Access _ | Power _ | Cst _ | Var _ -> |
|
294 |
fprintf fmt |
|
295 |
"\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a" |
|
296 |
pp_var_name lhs (pp_emf_cst_or_var m) expr |
|
293 | 297 |
| ResetFlag -> |
294 |
(* TODO: handle reset flag *) |
|
295 |
assert false |
|
296 |
end |
|
297 |
|
|
298 |
| MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a |
|
299 |
variable or a constant, no function anymore! *) |
|
300 |
-> ( |
|
301 |
fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a" |
|
302 |
pp_var_name lhs |
|
303 |
(pp_emf_cst_or_var m) expr |
|
304 |
) |
|
305 |
|
|
306 |
| MSetReset id |
|
307 |
-> ( |
|
308 |
fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\"" |
|
309 |
(reset_name id) |
|
310 |
) |
|
311 |
| MNoReset id |
|
312 |
-> ( |
|
313 |
fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\"" |
|
314 |
(reset_name id) |
|
315 |
) |
|
298 |
(* TODO: handle reset flag *) |
|
299 |
assert false) |
|
300 |
| MStateAssign (lhs, expr) |
|
301 |
(* a Pre construct Shall only be defined by a |
|
302 |
variable or a constant, no function anymore! *) -> |
|
303 |
fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a" |
|
304 |
pp_var_name lhs (pp_emf_cst_or_var m) expr |
|
305 |
| MSetReset id -> |
|
306 |
fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\"" |
|
307 |
(reset_name id) |
|
308 |
| MNoReset id -> |
|
309 |
fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\"" |
|
310 |
(reset_name id) |
|
316 | 311 |
(* TODO: handle clear_reset and reset flag *) |
317 | 312 |
| MClearReset | MResetAssign _ -> () |
318 |
|
|
319 |
| MBranch (g, hl) -> ( |
|
313 |
| MBranch (g, hl) -> |
|
320 | 314 |
let all_outputs, outputs, inputs = branch_instr_vars m i in |
315 |
|
|
321 | 316 |
(* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *) |
322 | 317 |
(* Machine_code.pp_instr i *) |
323 | 318 |
(* (fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *) |
... | ... | |
326 | 321 |
(* (VSet.elements inputs) *) |
327 | 322 |
|
328 | 323 |
(* ; *) |
329 |
let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in |
|
330 |
(* Format.eprintf "Filtering in: %a@.@." *) |
|
331 |
(* pp_emf_vars_decl *) |
|
332 |
(* (VSet.elements inputs) *) |
|
333 |
|
|
334 |
(* ; *) |
|
335 |
fprintf fmt "\"kind\": \"branch\",@ "; |
|
336 |
fprintf fmt "\"guard\": %a,@ " (pp_emf_cst_or_var m) g; (* it has to be a variable or a constant *) |
|
337 |
fprintf fmt "\"outputs\": [%a],@ " (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs); |
|
338 |
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl |
|
339 |
(* (let guard_inputs = get_expr_vars g in |
|
340 |
VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to |
|
341 |
remove guard's variable from inputs *) |
|
342 |
(VSet.elements inputs) |
|
343 |
; |
|
344 |
fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }" |
|
345 |
(fprintf_list ~sep:",@ " |
|
346 |
(fun fmt (tag, instrs_tag) -> |
|
347 |
let branch_all_lhs, _, branch_inputs = branch_block_vars m instrs_tag in |
|
348 |
let branch_inputs = VSet.filter (fun v -> not (ISet.mem v.var_id branch_all_lhs)) branch_inputs in |
|
349 |
fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt -> Format.pp_print_string fmt tag); |
|
350 |
fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag; |
|
351 |
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl (VSet.elements branch_inputs); |
|
352 |
fprintf fmt "@[<v 2>\"instrs\": {@ "; |
|
353 |
(pp_emf_instrs m) fmt instrs_tag; |
|
354 |
fprintf fmt "@]@ }"; |
|
355 |
fprintf fmt "@]@ }" |
|
356 |
) |
|
357 |
) |
|
358 |
hl |
|
359 |
) |
|
360 |
|
|
361 |
| MStep ([var], f, _) when is_arrow_fun m i -> (* Arrow case *) ( |
|
362 |
fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\"" |
|
363 |
f |
|
364 |
pp_var_name var |
|
365 |
(reset_name f) |
|
366 |
) |
|
367 |
|
|
368 |
| MStep (outputs, f, inputs) when not (is_imported_node f m) -> ( |
|
369 |
let node_f = get_node_def f m in |
|
370 |
let is_stateful = List.mem_assoc f m.minstances in |
|
371 |
fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ " |
|
372 |
(if is_stateful then "statefulcall" else "statelesscall") |
|
373 |
print_protect (fun fmt -> pp_print_string fmt (node_f.node_id)) |
|
374 |
f; |
|
375 |
fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]" |
|
376 |
(fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" pp_var_name v)) outputs |
|
377 |
(pp_emf_cst_or_var_list m) inputs; |
|
378 |
if is_stateful then |
|
379 |
fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}" |
|
380 |
(reset_name f) |
|
381 |
(is_resetable_fun i.lustre_eq) |
|
382 |
else fprintf fmt "@ " |
|
383 |
) |
|
384 |
|
|
385 |
| MStep(outputs, f, inputs ) -> (* This is an imported node *) |
|
386 |
EMF_library_calls.pp_call fmt m f outputs inputs |
|
387 |
|
|
388 |
| MSpec _ | MComment _ |
|
389 |
-> Format.eprintf "unhandled comment in EMF@.@?"; assert false |
|
390 |
(* not available for EMF output *) |
|
324 |
let inputs = |
|
325 |
VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs |
|
326 |
in |
|
327 |
|
|
328 |
(* Format.eprintf "Filtering in: %a@.@." *) |
|
329 |
(* pp_emf_vars_decl *) |
|
330 |
(* (VSet.elements inputs) *) |
|
331 |
|
|
332 |
(* ; *) |
|
333 |
fprintf fmt "\"kind\": \"branch\",@ "; |
|
334 |
fprintf fmt "\"guard\": %a,@ " (pp_emf_cst_or_var m) g; |
|
335 |
(* it has to be a variable or a constant *) |
|
336 |
fprintf fmt "\"outputs\": [%a],@ " |
|
337 |
(fprintf_list ~sep:", " pp_var_string) |
|
338 |
(ISet.elements outputs); |
|
339 |
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl |
|
340 |
(* |
|
341 |
(let guard_inputs = get_expr_vars g in |
|
342 |
VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to |
|
343 |
remove guard's variable from inputs *) |
|
344 |
(VSet.elements inputs); |
|
345 |
fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }" |
|
346 |
(fprintf_list ~sep:",@ " (fun fmt (tag, instrs_tag) -> |
|
347 |
let branch_all_lhs, _, branch_inputs = |
|
348 |
branch_block_vars m instrs_tag |
|
349 |
in |
|
350 |
let branch_inputs = |
|
351 |
VSet.filter |
|
352 |
(fun v -> not (ISet.mem v.var_id branch_all_lhs)) |
|
353 |
branch_inputs |
|
354 |
in |
|
355 |
fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt -> |
|
356 |
Format.pp_print_string fmt tag); |
|
357 |
fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag; |
|
358 |
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl |
|
359 |
(VSet.elements branch_inputs); |
|
360 |
fprintf fmt "@[<v 2>\"instrs\": {@ "; |
|
361 |
(pp_emf_instrs m) fmt instrs_tag; |
|
362 |
fprintf fmt "@]@ }"; |
|
363 |
fprintf fmt "@]@ }")) |
|
364 |
hl |
|
365 |
| MStep ([ var ], f, _) when is_arrow_fun m i -> |
|
366 |
(* Arrow case *) |
|
367 |
fprintf fmt |
|
368 |
"\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \ |
|
369 |
\"%s\"" |
|
370 |
f pp_var_name var (reset_name f) |
|
371 |
| MStep (outputs, f, inputs) when not (is_imported_node f m) -> |
|
372 |
let node_f = get_node_def f m in |
|
373 |
let is_stateful = List.mem_assoc f m.minstances in |
|
374 |
fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ " |
|
375 |
(if is_stateful then "statefulcall" else "statelesscall") |
|
376 |
print_protect |
|
377 |
(fun fmt -> pp_print_string fmt node_f.node_id) |
|
378 |
f; |
|
379 |
fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]" |
|
380 |
(fprintf_list ~sep:",@ " (fun fmt v -> |
|
381 |
fprintf fmt "\"%a\"" pp_var_name v)) |
|
382 |
outputs (pp_emf_cst_or_var_list m) inputs; |
|
383 |
if is_stateful then |
|
384 |
fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}" |
|
385 |
(reset_name f) |
|
386 |
(is_resetable_fun i.lustre_eq) |
|
387 |
else fprintf fmt "@ " |
|
388 |
| MStep (outputs, f, inputs) -> |
|
389 |
(* This is an imported node *) |
|
390 |
EMF_library_calls.pp_call fmt m f outputs inputs |
|
391 |
| MSpec _ | MComment _ -> |
|
392 |
Format.eprintf "unhandled comment in EMF@.@?"; |
|
393 |
assert false |
|
394 |
(* not available for EMF output *) |
|
391 | 395 |
in |
392 |
fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i; |
|
393 |
fprintf fmt "%a" pp_content i; |
|
394 |
fprintf fmt "@]@]@ }" |
|
395 |
and pp_emf_instrs m fmt instrs = fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs |
|
396 |
fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i; |
|
397 |
fprintf fmt "%a" pp_content i; |
|
398 |
fprintf fmt "@]@]@ }" |
|
399 |
|
|
400 |
and pp_emf_instrs m fmt instrs = |
|
401 |
fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs |
|
396 | 402 |
|
397 | 403 |
let pp_emf_annot cpt fmt (key, ee) = |
398 | 404 |
let _ = |
399 |
fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }" |
|
400 |
!cpt |
|
401 |
(fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s)) key |
|
402 |
pp_emf_eexpr ee |
|
405 |
fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }" !cpt |
|
406 |
(fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s)) |
|
407 |
key pp_emf_eexpr ee |
|
403 | 408 |
in |
404 | 409 |
incr cpt |
405 | 410 |
|
406 | 411 |
let pp_emf_spec_mode fmt m = |
407 | 412 |
fprintf fmt "{@["; |
408 |
fprintf fmt "\"mode_id\": \"%s\",@ " |
|
409 |
m.mode_id; |
|
410 |
fprintf fmt "\"ensure\": [%a],@ " |
|
411 |
pp_emf_eexprs m.ensure; |
|
412 |
fprintf fmt "\"require\": [%a]@ " |
|
413 |
pp_emf_eexprs m.require; |
|
413 |
fprintf fmt "\"mode_id\": \"%s\",@ " m.mode_id; |
|
414 |
fprintf fmt "\"ensure\": [%a],@ " pp_emf_eexprs m.ensure; |
|
415 |
fprintf fmt "\"require\": [%a]@ " pp_emf_eexprs m.require; |
|
414 | 416 |
fprintf fmt "@]}" |
415 |
|
|
417 |
|
|
416 | 418 |
let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode |
417 | 419 |
|
418 | 420 |
let pp_emf_spec_import fmt i = |
419 | 421 |
fprintf fmt "{@["; |
420 |
fprintf fmt "\"contract\": \"%s\",@ " |
|
421 |
i.import_nodeid; |
|
422 |
fprintf fmt "\"inputs\": [%a],@ " |
|
423 |
pp_emf_expr i.inputs; |
|
424 |
fprintf fmt "\"outputs\": [%a],@ " |
|
425 |
pp_emf_expr i.outputs; |
|
422 |
fprintf fmt "\"contract\": \"%s\",@ " i.import_nodeid; |
|
423 |
fprintf fmt "\"inputs\": [%a],@ " pp_emf_expr i.inputs; |
|
424 |
fprintf fmt "\"outputs\": [%a],@ " pp_emf_expr i.outputs; |
|
426 | 425 |
fprintf fmt "@]}" |
427 |
|
|
426 |
|
|
428 | 427 |
let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import |
429 | 428 |
|
430 | 429 |
let pp_emf_spec fmt spec = |
... | ... | |
435 | 434 |
* pp_emf_vars_decl spec.locals; |
436 | 435 |
* fprintf fmt "\"stmts\": [%a],@ " |
437 | 436 |
* pp_emf_stmts spec.stmts; *) |
438 |
fprintf fmt "\"assume\": [%a],@ " |
|
439 |
pp_emf_eexprs spec.assume; |
|
440 |
fprintf fmt "\"guarantees\": [%a],@ " |
|
441 |
pp_emf_eexprs spec.guarantees; |
|
442 |
fprintf fmt "\"modes\": [%a]@ " |
|
443 |
pp_emf_spec_modes spec.modes; |
|
437 |
fprintf fmt "\"assume\": [%a],@ " pp_emf_eexprs spec.assume; |
|
438 |
fprintf fmt "\"guarantees\": [%a],@ " pp_emf_eexprs spec.guarantees; |
|
439 |
fprintf fmt "\"modes\": [%a]@ " pp_emf_spec_modes spec.modes; |
|
444 | 440 |
(* fprintf fmt "\"imports\": [%a]@ " |
445 |
* pp_emf_spec_imports spec.imports; *)
|
|
441 |
* pp_emf_spec_imports spec.imports; *) |
|
446 | 442 |
fprintf fmt "@] }" |
447 |
|
|
448 |
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots |
|
449 |
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list |
|
443 |
|
|
444 |
let pp_emf_annots cpt fmt annots = |
|
445 |
fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots |
|
446 |
|
|
447 |
let pp_emf_annots_list cpt fmt annots_list = |
|
448 |
fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list |
|
450 | 449 |
|
451 | 450 |
(* let pp_emf_contract fmt nd = |
452 | 451 |
* let c = Printers.node_as_contract nd in |
... | ... | |
455 | 454 |
* fprintf fmt "\"contract\": %a@ " |
456 | 455 |
* pp_emf_spec c; |
457 | 456 |
* fprintf fmt "@]@ }" *) |
458 |
|
|
457 |
|
|
459 | 458 |
let pp_machine fmt m = |
460 |
let instrs = (*merge_branches*) m.mstep.step_instrs in |
|
459 |
let instrs = |
|
460 |
(*merge_branches*) |
|
461 |
m.mstep.step_instrs |
|
462 |
in |
|
461 | 463 |
try |
462 |
fprintf fmt "@[<v 2>\"%a\": {@ " |
|
463 |
print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
|
|
464 |
fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt ->
|
|
465 |
pp_print_string fmt m.mname.node_id);
|
|
464 | 466 |
(match m.mspec.mnode_spec with |
465 |
| Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ "
|
|
466 |
| _ -> ());
|
|
467 |
| Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ " |
|
468 |
| _ -> ()); |
|
467 | 469 |
fprintf fmt "\"imported\": \"false\",@ "; |
468 |
fprintf fmt "\"kind\": %t,@ " |
|
469 |
(fun fmt -> if not ( snd (get_stateless_status m) ) |
|
470 |
then fprintf fmt "\"stateful\"" |
|
471 |
else fprintf fmt "\"stateless\""); |
|
472 |
fprintf fmt "\"inputs\": [%a],@ " |
|
473 |
pp_emf_vars_decl m.mstep.step_inputs; |
|
474 |
fprintf fmt "\"outputs\": [%a],@ " |
|
475 |
pp_emf_vars_decl m.mstep.step_outputs; |
|
476 |
fprintf fmt "\"locals\": [%a],@ " |
|
477 |
pp_emf_vars_decl m.mstep.step_locals; |
|
478 |
fprintf fmt "\"mems\": [%a],@ " |
|
479 |
pp_emf_vars_decl m.mmemory; |
|
470 |
fprintf fmt "\"kind\": %t,@ " (fun fmt -> |
|
471 |
if not (snd (get_stateless_status m)) then fprintf fmt "\"stateful\"" |
|
472 |
else fprintf fmt "\"stateless\""); |
|
473 |
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl m.mstep.step_inputs; |
|
474 |
fprintf fmt "\"outputs\": [%a],@ " pp_emf_vars_decl m.mstep.step_outputs; |
|
475 |
fprintf fmt "\"locals\": [%a],@ " pp_emf_vars_decl m.mstep.step_locals; |
|
476 |
fprintf fmt "\"mems\": [%a],@ " pp_emf_vars_decl m.mmemory; |
|
480 | 477 |
fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id; |
481 |
fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ " |
|
482 |
(pp_emf_instrs m) instrs; |
|
478 |
fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ " (pp_emf_instrs m) instrs; |
|
483 | 479 |
(match m.mspec.mnode_spec with |
484 |
| None -> ()
|
|
485 |
| Some (Contract c) -> (
|
|
486 |
assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);
|
|
487 |
fprintf fmt "\"spec\": %a,@ " pp_emf_spec c
|
|
488 |
)
|
|
489 |
| Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id
|
|
490 |
);
|
|
491 |
fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
|
|
480 |
| None -> () |
|
481 |
| Some (Contract c) ->
|
|
482 |
assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []); |
|
483 |
fprintf fmt "\"spec\": %a,@ " pp_emf_spec c |
|
484 |
| Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id);
|
|
485 |
fprintf fmt "\"annots\": {@[<v 0> %a@]@ }"
|
|
486 |
(pp_emf_annots_list (ref 0))
|
|
487 |
m.mannot;
|
|
492 | 488 |
fprintf fmt "@]@ }" |
493 |
with Unhandled msg -> (
|
|
489 |
with Unhandled msg -> |
|
494 | 490 |
eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ " |
495 | 491 |
m.mname.node_id; |
496 | 492 |
eprintf "%s@ " msg; |
497 | 493 |
eprintf "node skipped - no output generated@ @]@." |
498 |
) |
|
499 | 494 |
|
500 | 495 |
(*let pp_machine fmt m = |
501 | 496 |
match m.mspec with |
502 | 497 |
| None | Some (NodeSpec _) -> pp_machine fmt m |
503 | 498 |
| Some (Contract _) -> pp_emf_contract fmt m |
504 | 499 |
*) |
505 |
|
|
500 |
|
|
506 | 501 |
let pp_emf_imported_node fmt top = |
507 | 502 |
let ind = Corelang.imported_node_of_top top in |
508 | 503 |
try |
509 |
fprintf fmt "@[<v 2>\"%a\": {@ " |
|
510 |
print_protect (fun fmt -> pp_print_string fmt ind.nodei_id);
|
|
504 |
fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt ->
|
|
505 |
pp_print_string fmt ind.nodei_id);
|
|
511 | 506 |
fprintf fmt "\"imported\": \"true\",@ "; |
512 |
fprintf fmt "\"inputs\": [%a],@ " |
|
513 |
pp_emf_vars_decl ind.nodei_inputs; |
|
514 |
fprintf fmt "\"outputs\": [%a],@ " |
|
515 |
pp_emf_vars_decl ind.nodei_outputs; |
|
507 |
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl ind.nodei_inputs; |
|
508 |
fprintf fmt "\"outputs\": [%a],@ " pp_emf_vars_decl ind.nodei_outputs; |
|
516 | 509 |
fprintf fmt "\"original_name\": \"%s\"" ind.nodei_id; |
517 |
(match ind.nodei_spec with None -> fprintf fmt "@ "
|
|
518 |
| Some (Contract _) -> assert false (* should have been processed *)
|
|
519 |
| Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id
|
|
520 |
); |
|
510 |
(match ind.nodei_spec with |
|
511 |
| None -> fprintf fmt "@ "
|
|
512 |
| Some (Contract _) -> assert false (* should have been processed *)
|
|
513 |
| Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id);
|
|
521 | 514 |
fprintf fmt "@]@ }" |
522 |
with Unhandled msg -> (
|
|
515 |
with Unhandled msg -> |
|
523 | 516 |
eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ " |
524 | 517 |
ind.nodei_id; |
525 | 518 |
eprintf "%s@ " msg; |
526 | 519 |
eprintf "node skipped - no output generated@ @]@." |
527 |
) |
|
520 |
|
|
528 | 521 |
(****************************************************) |
529 | 522 |
(* Main function: iterates over node and print them *) |
530 | 523 |
(****************************************************) |
... | ... | |
533 | 526 |
Utils.fprintf_list ~sep:",@ " |
534 | 527 |
(fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v) |
535 | 528 |
fmt |
536 |
["compiler-name", (Filename.basename Sys.executable_name);
|
|
537 |
"compiler-version", Version.number;
|
|
538 |
"command", (String.concat " " (Array.to_list Sys.argv));
|
|
539 |
"source_file", basename
|
|
540 |
]
|
|
541 |
; |
|
529 |
[ |
|
530 |
"compiler-name", Filename.basename Sys.executable_name;
|
|
531 |
"compiler-version", Version.number;
|
|
532 |
"command", String.concat " " (Array.to_list Sys.argv);
|
|
533 |
"source_file", basename;
|
|
534 |
];
|
|
542 | 535 |
fprintf fmt "@ @]},@ " |
543 |
|
|
536 |
|
|
544 | 537 |
let translate fmt basename prog machines = |
545 | 538 |
(* record_types prog; *) |
546 | 539 |
fprintf fmt "@[<v 0>{@ "; |
547 | 540 |
pp_meta fmt basename; |
548 | 541 |
(* Typedef *) |
549 | 542 |
fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ " |
550 |
(pp_emf_list pp_emf_typedef) (Corelang.get_typedefs prog); |
|
543 |
(pp_emf_list pp_emf_typedef) |
|
544 |
(Corelang.get_typedefs prog); |
|
551 | 545 |
fprintf fmt "\"consts\": [@[<v 0>%a@]],@ " |
552 |
(pp_emf_list pp_emf_top_const) (Corelang.get_consts prog); |
|
546 |
(pp_emf_list pp_emf_top_const) |
|
547 |
(Corelang.get_consts prog); |
|
553 | 548 |
fprintf fmt "\"imported_nodes\": @[<v 0>{@ "; |
554 | 549 |
pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog); |
555 | 550 |
fprintf fmt "}@],@ "; |
556 | 551 |
fprintf fmt "\"nodes\": @[<v 0>{@ "; |
557 |
(* Previous alternative: mapping normalized lustre to EMF:
|
|
552 |
(* Previous alternative: mapping normalized lustre to EMF: |
|
558 | 553 |
fprintf_list ~sep:",@ " pp_decl fmt prog; *) |
559 | 554 |
pp_emf_list pp_machine fmt machines; |
560 | 555 |
fprintf fmt "}@]@ }"; |
Also available in: Unified diff
reformatting