lustrec / src / backends / EMF / EMF_backend.ml @ dd71e482
History  View  Annotate  Download (28.4 KB)
1 
(* EMF backend *) 

2 
(* This backup is initially motivated by the need to express Spacer computed 
3 
invariants as Matlab Simulink executable evidences. 
4  
5 
Therefore the input language is more restricted. We do not expect fancy 
6 
datastructure, complex function calls, etc. 
7  
8 
In case of error, use node foo inline to eliminate function calls that are 
9 
not seriously handled yet. 
10 

11  
12 
In terms of algorithm, the process was initially based on printing normalized 
13 
code. We now rely on machine code printing. The old code is preserved for 
14 
reference. 
15 
*) 
16  
17 
open LustreSpec 
18 
open Machine_code 
19 
open Format 
20 
open Utils 
21  
22 
exception Unhandled of string 
23 

24  
25 
(* Basic printing functions *) 
26 

27 
let pp_var_string fmt v = fprintf fmt "\"%s\"" v 
28 
(*let pp_var_name fmt v = fprintf fmt "\"%a\"" Printers.pp_var_name v*) 
29 
(*let pp_node_args = fprintf_list ~sep:", " pp_var_name*) 
30  
31 
let pp_emf_var_decl fmt v = 
32 
fprintf fmt "@[{\"name\": \"%a\", \"type\":\"%a\"}@]" 
33 
Printers.pp_var_name v 
34 
Printers.pp_var_type v 
35 

36 
let pp_emf_vars_decl fmt vl = 
37 
fprintf fmt "@["; 
38 
fprintf_list ~sep:",@ " pp_emf_var_decl fmt vl; 
39 
fprintf fmt "@]" 
40 

41 
let reset_name id = 
42 
"reset_" ^ id 
43 

44 

45 
(* Matlab starting counting from 1. 
46 
simple function to extract the element id in the list. Starts from 1. *) 
47 
let rec get_idx x l = 
48 
match l with 
49 
 hd::tl > if hd = x then 1 else 1+(get_idx x tl) 
50 
 [] > assert false 
51  
52 
(**********************************************) 
53 
(* Old stuff: printing normalized code as EMF *) 
54 
(**********************************************) 
55  
56 
(* 
57 
let pp_expr vars fmt expr = 
58 
let rec pp_expr fmt expr = 
59 
match expr.expr_desc with 
60 
 Expr_const c > Printers.pp_const fmt c 
61 
 Expr_ident id > 
62 
if List.mem id vars then 
63 
Format.fprintf fmt "u%i" (get_idx id vars) 
64 
else 
65 
assert false (* impossible to find element id in var list *) 
66 
 Expr_array a > fprintf fmt "[%a]" pp_tuple a 
67 
 Expr_access (a, d) > fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d 
68 
 Expr_power (a, d) > fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d 
69 
 Expr_tuple el > fprintf fmt "(%a)" pp_tuple el 
70 
 Expr_ite (c, t, e) > fprintf fmt "if %a; y=(%a); else y=(%a); end" pp_expr c pp_expr t pp_expr e 
71 
 Expr_arrow (e1, e2) >( 
72 
match e1.expr_desc, e2.expr_desc with 
73 
 Expr_const c1, Expr_const c2 > if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then fprintf fmt "STEP" else assert false (* only handle true > false *) 
74 
 _ > assert false (* only handle true > false *) 
75 
) 
76 
 Expr_fby (e1, e2) > assert false (* not covered yet *) 
77 
 Expr_pre e > fprintf fmt "UNITDELAY" 
78 
 Expr_when (e, id, l) > assert false (* clocked based expressions are not handled yet *) 
79 
 Expr_merge (id, hl) > assert false (* clocked based expressions are not handled yet *) 
80 
 Expr_appl (id, e, r) > pp_app fmt id e r 
81  
82 
and pp_tuple fmt el = 
83 
fprintf_list ~sep:"," pp_expr fmt el 
84  
85 
and pp_app fmt id e r = 
86 
match r with 
87 
 None > pp_call fmt id e 
88 
 Some c > assert false (* clocked based expressions are not handled yet *) 
89  
90 
and pp_call fmt id e = 
91 
match id, e.expr_desc with 
92 
 "+", Expr_tuple([e1;e2]) > fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2 
93 
 "uminus", _ > fprintf fmt "( %a)" pp_expr e 
94 
 "", Expr_tuple([e1;e2]) > fprintf fmt "(%a  %a)" pp_expr e1 pp_expr e2 
95 
 "*", Expr_tuple([e1;e2]) > fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2 
96 
 "/", Expr_tuple([e1;e2]) > fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2 
97 
 "mod", Expr_tuple([e1;e2]) > fprintf fmt "mod (%a, %a)" pp_expr e1 pp_expr e2 
98 
 "&&", Expr_tuple([e1;e2]) > fprintf fmt "(%a & %a)" pp_expr e1 pp_expr e2 
99 
 "", Expr_tuple([e1;e2]) > fprintf fmt "(%a  %a)" pp_expr e1 pp_expr e2 
100 
 "xor", Expr_tuple([e1;e2]) > fprintf fmt "xor (%a, %a)" pp_expr e1 pp_expr e2 
101 
 "impl", Expr_tuple([e1;e2]) > fprintf fmt "((~%a)  %a)" pp_expr e1 pp_expr e2 
102 
 "<", Expr_tuple([e1;e2]) > fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2 
103 
 "<=", Expr_tuple([e1;e2]) > fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2 
104 
 ">", Expr_tuple([e1;e2]) > fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2 
105 
 ">=", Expr_tuple([e1;e2]) > fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2 
106 
 "!=", Expr_tuple([e1;e2]) > fprintf fmt "(%a ~= %a)" pp_expr e1 pp_expr e2 
107 
 "=", Expr_tuple([e1;e2]) > fprintf fmt "(%a == %a)" pp_expr e1 pp_expr e2 
108 
 "not", _ > fprintf fmt "(~%a)" pp_expr e 
109 
 _, Expr_tuple _ > fprintf fmt "%s %a" id pp_expr e 
110 
 _ > fprintf fmt "%s (%a)" id pp_expr e 
111  
112 
in 
113 
pp_expr fmt expr 
114  
115 
let pp_stmt fmt stmt = 
116 
match stmt with 
117 
 Eq eq > ( 
118 
match eq.eq_lhs with 
119 
[var] > ( 
120 
(* first, we extract the expression and associated variables *) 
121 
let vars = Utils.ISet.elements (Corelang.get_expr_vars eq.eq_rhs) in 
122  
123 
fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @]}" 
124 
var 
125 
(pp_expr vars) eq.eq_rhs (* todo_pp_expr expr *) 
126 
(fprintf_list ~sep:", " pp_var_string) vars 
127 
) 
128 
 _ > assert false (* should not happen for input of EMF backend (cocospec generated nodes *) 
129 
) 
130 
 _ > assert false (* should not happen with EMF backend *) 
131  
132 
let pp_node fmt nd = 
133 
fprintf fmt "@[<v 2>\"%s\": {@ \"inputs\": [%a],@ \"outputs\": [%a],@ " 
134 
nd.node_id 
135 
pp_node_args nd.node_inputs 
136 
pp_node_args nd.node_outputs; 
137 
fprintf fmt "\"exprs\": {@[<v 1> %a@]@ }" 
138 
(fprintf_list ~sep:",@ " pp_stmt ) nd.node_stmts; 
139 
fprintf fmt "@]@ }" 
140  
141 
let pp_decl fmt decl = 
142 
match decl.top_decl_desc with 
143 
 Node nd > fprintf fmt "%a@ " pp_node nd 
144 
 ImportedNode _ 
145 
 Const _ 
146 
 Open _ 
147 
 TypeDef _ > eprintf "should not happen in EMF backend" 
148 
*) 
149  
150  
151 
(**********************************************) 
152 
(* Utility functions: arrow and lustre expr *) 
153 
(**********************************************) 
154  
155 
(* detect whether the instruction i represents an ARROW, ie an arrow with true 
156 
> false *) 
157 
let is_arrow_fun m i = 
158 
match Corelang.get_instr_desc i with 
159 
 MStep ([var], i, vl) > ( 
160 
let name = try (Machine_code.get_node_def i m).node_id with Not_found > Format.eprintf "Impossible to find node %s@.@?" i; raise Not_found in 
161 
match name, vl with 
162 
 "_arrow", [v1; v2] > ( 
163 
match v1.value_desc, v2.value_desc with 
164 
 Cst c1, Cst c2 > 
165 
if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then 
166 
true 
167 
else 
168 
assert false (* only handle true > false *) 
169 
 _ > assert false 
170 
) 
171 
 _ > false 
172 
) 
173 
 _ > false 
174  
175 
let pp_original_lustre_expression m fmt i = 
176 
match Corelang.get_instr_desc i with 
177 
 MLocalAssign _  MStateAssign _ 
178 
 MBranch _ 
179 
> ( match i.lustre_eq with None > ()  Some e > Printers.pp_node_eq fmt e) 
180 
 MStep _ when is_arrow_fun m i > () (* we print nothing, this is a STEP *) 
181 
 MStep _ > (match i.lustre_eq with None > ()  Some eq > Printers.pp_node_eq fmt eq) 
182 
 _ > () 
183  
184 
(* 
185 
let rec get_instr_lhs i = 
186 
match Corelang.get_instr_desc i with 
187 
 MLocalAssign (var,_) 
188 
 MStateAssign (var,_) > [var.var_id] 
189 
 MStep (vars, _, _) > List.map (fun v > v.var_id) vars 
190 
 MBranch (_,(_,case1)::_) > 
191 
get_instrs_lhs case1 (* assuming all cases define the same variables *) 
192 
 MBranch _ > assert false (* branch instruction should admit at least one case *) 
193 
 MReset ni 
194 
 MNoReset ni > [reset_name ni] 
195 
 MComment _ > assert false (* not available for EMF output *) 
196 
and get_instrs_lhs il = 
197 
List.fold_left (fun accu i > (get_instr_lhs i) @ accu ) [] il 
198 
*) 
199 
(**********************************************) 
200 
(* Printing machine code as EMF *) 
201 
(**********************************************) 
202  
203 
(******************* 
204 

205 
(* Print machine code values as matlab expressions. Variable identifiers are 
206 
replaced by uX where X is the index of the variables in the list vars of input 
207 
variables. *) 
208 
let rec pp_matlab_val vars fmt v = 
209 
match v.value_desc with 
210 
 Cst c > Printers.pp_const fmt c 
211 
 LocalVar v 
212 
 StateVar v > 
213 
let id = v.var_id in 
214 
if List.mem id vars then 
215 
Format.fprintf fmt "u%i" (get_idx id vars) 
216 
else 
217 
let _ = Format.eprintf "Error: looking for var %s in %a@.@?" id (Utils.fprintf_list ~sep:"," Format.pp_print_string) vars in assert false (* impossible to find element id in var list *) 
218 
 Fun (n, vl) > pp_fun vars n fmt vl 
219 
 _ > assert false (* not available in EMF backend *) 
220 
and pp_fun vars id fmt vl = 
221 
(* eprintf "print %s with %i args@.@?" id (List.length vl);*) 
222 
match id, vl with 
223 
 "+", [v1;v2] > fprintf fmt "(%a + %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
224 
 "uminus", [v] > fprintf fmt "( %a)" (pp_matlab_val vars) v 
225 
 "", [v1;v2] > fprintf fmt "(%a  %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
226 
 "*",[v1;v2] > fprintf fmt "(%a * %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
227 
 "/", [v1;v2] > fprintf fmt "(%a / %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
228 
 "mod", [v1;v2] > fprintf fmt "mod (%a, %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
229 
 "&&", [v1;v2] > fprintf fmt "(%a & %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
230 
 "", [v1; v2] > fprintf fmt "(%a  %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
231 
 "xor", [v1; v2] > fprintf fmt "xor (%a, %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
232 
 "impl", [v1; v2] > fprintf fmt "((~%a)  %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
233 
 "<", [v1; v2] > fprintf fmt "(%a < %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
234 
 "<=", [v1; v2] > fprintf fmt "(%a <= %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
235 
 ">", [v1; v2] > fprintf fmt "(%a > %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
236 
 ">=", [v1; v2] > fprintf fmt "(%a >= %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
237 
 "!=", [v1; v2] > fprintf fmt "(%a != %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
238 
 "=", [v1; v2] > fprintf fmt "(%a = %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2 
239 
 "not", [v] > fprintf fmt "(~%a)" (pp_matlab_val vars) v 
240 
 _ > fprintf fmt "%s (%a)" id (Utils.fprintf_list ~sep:", " (pp_matlab_val vars)) vl 
241  
242 

243  
244 
(* pp_basic_instr prints regular instruction. These do not contain MStep which 
245 
should have been already filtered out. Another restriction which is supposed 
246 
to be enforced is that branching statement contain a single instruction (in 
247 
practice it has to be an assign) *) 
248 
let pp_matlab_basic_instr m vars fmt i = 
249 
match Corelang.get_instr_desc i with 
250 
 MLocalAssign (var,v) 
251 
 MStateAssign (var,v) > fprintf fmt "y = %a" (pp_matlab_val vars) v 
252 
 MReset _ 
253 
> Format.eprintf "unhandled reset in EMF@.@?"; assert false 
254 
 MNoReset _ 
255 
> Format.eprintf "unhandled noreset in EMF@.@?"; assert false 
256 
 MBranch _ (* branching instructions already handled *) 
257 
> Format.eprintf "unhandled branch statement in EMF (should have been filtered out before)@.@?"; 
258 
assert false 
259 
 MStep _ (* function calls already handled, including STEP *) 
260 
> Format.eprintf "unhandled function call in EMF (should have been filtered out before)@.@?"; 
261 
assert false 
262 
 MComment _ 
263 
> Format.eprintf "unhandled comment in EMF@.@?"; assert false 
264 
(* not available for EMF output *) 
265  
266  
267  
268 
let rec get_instr_lhs_var i = 
269 
match Corelang.get_instr_desc i with 
270 
 MLocalAssign (var,_) 
271 
 MStateAssign (var,_) 
272 
 MStep ([var], _, _) > 
273 
(* The only MStep instructions that filtered here 
274 
should be arrows, ie. single var *) 
275 
var 
276 
 MBranch (_,(_,case1)::_) > 
277 
get_instrs_var case1 (* assuming all cases define the same variables *) 
278 
 MStep (f,name,a) > Format.eprintf "step %s@.@?" name; assert false (* no other MStep here *) 
279 
 MBranch _ > assert false (* branch instruction should admit at least one case *) 
280 
 MReset _ 
281 
 MNoReset _ 
282 
 MComment _ > assert false (* not available for EMF output *) 
283 
and get_instrs_var il = 
284 
match il with 
285 
 i::_ > get_instr_lhs_var i (* looking for the first instr *) 
286 
 _ > assert false 
287  
288 

289 
let rec get_val_vars v = 
290 
match v.value_desc with 
291 
 Cst c > Utils.ISet.empty 
292 
 LocalVar v 
293 
 StateVar v > Utils.ISet.singleton v.var_id 
294 
 Fun (n, vl) > List.fold_left (fun res v > Utils.ISet.union (get_val_vars v) res) Utils.ISet.empty vl 
295 
 _ > assert false (* not available in EMF backend *) 
296  
297 
let rec get_instr_rhs_vars i = 
298 
match Corelang.get_instr_desc i with 
299 
 MLocalAssign (_,v) 
300 
 MStateAssign (_,v) > get_val_vars v 
301 
 MStep (_, _, vl) > List.fold_left (fun res v > Utils.ISet.union res (get_val_vars v)) Utils.ISet.empty vl 
302 
 MBranch (c,[(_,[case1]);(_,[case2])]) > 
303 
Utils.ISet.union 
304 
(get_val_vars c) 
305 
( 
306 
Utils.ISet.union 
307 
(get_instr_rhs_vars case1) 
308 
(get_instr_rhs_vars case2) 
309 
) 
310 
 MBranch (g, branches) > 
311 
List.fold_left 
312 
(fun accu (_, il) > Utils.ISet.union accu (get_instrs_vars il)) 
313 
(get_val_vars g) 
314 
branches 
315 
 MReset id 
316 
 MNoReset id > Utils.ISet.singleton id 
317 
 MComment _ > Utils.ISet.empty 
318 
and get_instrs_vars il = 
319 
List.fold_left (fun res i > Utils.ISet.union res (get_instr_rhs_vars i)) 
320 
Utils.ISet.empty 
321 
il 
322  
323  
324 

325 
let rec pp_emf_instr m fmt i = 
326 
(* Either it is a Step function non arrow, then we have a dedicated treatment, 
327 
or it has to be a single variable assigment *) 
328 
let arguments_vars = Utils.ISet.elements (get_instr_rhs_vars i) in 
329 

330 
match Corelang.get_instr_desc i with 
331 
(* Regular node call either a statuful node or a functional one *) 
332 
 MStep (outputs, f, inputs) when not (is_arrow_fun m i) > ( 
333 
fprintf fmt "\"CALL\": @[<v 2>{ \"node\": \"%s\",@ \"inputs\": [%a],@ \"vars\": [%a]@ \"lhs\": [%a],@ \"original_lustre_expr\": [%a]@]}" 
334 
((Machine_code.get_node_def f m).node_id) (* Node name *) 
335 
(Utils.fprintf_list ~sep:", " (fun fmt _val > fprintf fmt "\"%a\"" (pp_matlab_val arguments_vars) _val)) inputs (* inputs *) 
336 
(fprintf_list ~sep:", " pp_var_string) arguments_vars 
337 
(fprintf_list ~sep:", " (fun fmt v > pp_var_string fmt v.var_id)) outputs (* outputs *) 
338 
(pp_original_lustre_expression m) i (* original lustre expr *) 
339 
) 
340 
 MStep _ > (* Arrow case *) ( 
341 
let var = get_instr_lhs_var i in 
342 
fprintf fmt "\"STEP\": @[<v 2>{ \"lhs\": \"%s\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%a]@]}" 
343 
var.var_id 
344 
(fprintf_list ~sep:", " pp_var_string) arguments_vars 
345 
(pp_original_lustre_expression m) i 
346 
) 
347 
 MBranch (g,[(tag1,[case1]);(tag2,[case2])]) when tag1 = Corelang.tag_true  tag2 = Corelang.tag_true > 
348 
(* Thanks to normalization with join_guards = false, branches shall contain 
349 
a single expression *) 
350 
let var = get_instr_lhs_var i in 
351 
let then_case, else_case = 
352 
if tag1 = Corelang.tag_true then 
353 
case1, case2 
354 
else 
355 
case2, case1 
356 
in 
357 
fprintf fmt "\"ITE\": @[<v 2>{ \"lhs\": \"%s\",@ \"guard\": \"%a\",@ \"then_expr\": \"%a\",@ \"else_expr\": \"%a\",@ \"vars\": [%a],@ \"original_lustre_expr\": [%a]@]}" 
358 
var.var_id 
359 
(pp_matlab_val arguments_vars) g 
360 
(pp_matlab_basic_instr m arguments_vars) then_case 
361 
(pp_matlab_basic_instr m arguments_vars) else_case 
362 
(fprintf_list ~sep:", " pp_var_string) arguments_vars 
363 
(pp_original_lustre_expression m) i 
364  
365 
 MBranch (g, [single_tag, single_branch]) > 
366 
(* First case: it corresponds to a clocked expression: a MBranch with a 
367 
single case. It shall become a subsystem with an enable port that depends on g = single_tag *) 
368 
(* Thanks to normalization with join_guards = false, branches shall contain 
369 
a single expression TODO REMOVE COMMENT THIS IS NOT TRUE *) 
370 
let var = get_instr_lhs_var i in 
371 
fprintf fmt "\"ENABLEDSUB\": @[<v 2>{ \"lhs\": \"%s\",@ \"enable_cond\": \"%a = %s\",@ \"subsystem\": {%a },@ \"vars\": [%a],@ \"original_lustre_expr\": [%a]@]}" 
372 
var.var_id 
373 
(pp_matlab_val arguments_vars) g 
374 
single_tag 
375 
(fprintf_list ~sep:",@ " (pp_emf_instr m)) single_branch 
376 
(fprintf_list ~sep:", " pp_var_string) arguments_vars 
377 
(pp_original_lustre_expression m) i 
378 

379 
 MBranch (g, hl) > 
380 
(* Thanks to normalization with join_guards = false, branches shall contain 
381 
a single expression *) 
382 
fprintf fmt "\"BRANCH\": @[<v 2>{ \"guard\": \"%a\",@ \"branches\": [@[<v 0>%a@]],@ \"vars\": [%a],@ \"original_lustre_expr\": [%a]@]}" 
383 
(pp_matlab_val arguments_vars) g 
384 
(fprintf_list ~sep:",@ " 
385 
(fun fmt (tag, (is_tag: instr_t list)) > 
386 
fprintf fmt "\"%s\": [%a]" 
387 
tag 
388 
(fprintf_list ~sep:",@ " (fun fmt i_tag > match Corelang.get_instr_desc i_tag with 
389 
 MLocalAssign (var,v) 
390 
 MStateAssign (var,v) > 
391 
fprintf fmt "{lhs= \"%s\", rhs= \"%a\"]" var.var_id (pp_matlab_val arguments_vars) v 
392 
 _ > Format.eprintf "unhandled instr: %a@." Machine_code.pp_instr i_tag; assert false 
393 
)) is_tag 
394 
)) hl 
395 
(fprintf_list ~sep:", " pp_var_string) arguments_vars 
396 
(pp_original_lustre_expression m) i 
397 

398 

399 

400 
 _ > 
401 
(* Other expressions, including "pre" *) 
402 
( 
403 
(* first, we extract the expression and associated variables *) 
404 
let var = get_instr_lhs_var i in 
405 
fprintf fmt "\"EXPR\": @[<v 2>{ \"lhs\": \"%s\",@ \"expr\": \"%a\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%a]@]}" 
406 
var.var_id 
407 
(fun fmt i > match Corelang.get_instr_desc i with 
408 
 MStep _ > fprintf fmt "STEP" 
409 
 _ > pp_matlab_basic_instr m arguments_vars fmt i) i 
410 
(fprintf_list ~sep:", " pp_var_string) arguments_vars 
411 
(pp_original_lustre_expression m) i 
412 
) 
413  
414 
*********************) 
415 

416 
let pp_emf_cst_or_var fmt v = 
417 
match v.value_desc with 
418 
 Cst c > 
419 
fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%a\"@ @]}" 
420 
Printers.pp_const c 
421 
 LocalVar v 
422 
 StateVar v > 
423 
fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\"@ @]}" 
424 
Printers.pp_var_name v 
425 
 _ > assert false (* Invalid argument *) 
426  
427 
let rec get_expr_vars v = 
428 
match v.value_desc with 
429 
 Cst c > VSet.empty 
430 
 LocalVar v  StateVar v > VSet.singleton v 
431 
 Fun (_, args) > List.fold_left (fun accu v > VSet.union accu (get_expr_vars v)) VSet.empty args 
432 
 _ > assert false (* Invalid argument *) 
433  
434 
let branch_cpt = ref 0 
435 
let get_instr_id fmt i = 
436 
match Corelang.get_instr_desc i with 
437 
 MLocalAssign(lhs,_)  MStateAssign (lhs, _) > Printers.pp_var_name fmt lhs 
438 
 MReset i  MNoReset i > fprintf fmt "%s" (reset_name i) 
439 
 MBranch (g, _) > incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt 
440 
 MStep (_, id, _) > fprintf fmt "%s" id 
441 
 _ > () (* No name *) 
442  
443 
let rec branch_block_vars il = 
444 
List.fold_left 
445 
(fun (accu_def, accu_read) i > 
446 
let defined_vars, read_vars = branch_instr_vars i in 
447 
ISet.union accu_def defined_vars, VSet.union accu_read read_vars) 
448 
(ISet.empty, VSet.empty) il 
449 
and branch_instr_vars i = 
450 
match Corelang.get_instr_desc i with 
451 
 MLocalAssign (var,expr) 
452 
 MStateAssign (var,expr) > ISet.singleton var.var_id, get_expr_vars expr 
453 
 MStep (vars, _, args) > 
454 
ISet.of_list (List.map (fun v > v.var_id) vars), 
455 
List.fold_left (fun accu v > VSet.union accu (get_expr_vars v)) VSet.empty args 
456 
 MBranch (g,(_,hd_il)::tl) > (* We focus on variables defined in all branches *) 
457 
let read_guard = get_expr_vars g in 
458 
let def_vars_hd, read_vars_hd = branch_block_vars hd_il in 
459 
let def_vars, read_vars = 
460 
List.fold_left 
461 
(fun (def_vars, read_vars) (_, il) > 
462 
(* We accumulate reads but intersect writes *) 
463 
let writes_il, reads_il = branch_block_vars il in 
464 
ISet.inter def_vars writes_il, 
465 
VSet.union read_vars reads_il 
466 
) 
467 
(def_vars_hd, read_vars_hd) 
468 
tl 
469 
in 
470 
def_vars, VSet.union read_guard read_vars 
471 
 MBranch _ > assert false (* branch instruction should admit at least one case *) 
472 
 MReset ni 
473 
 MNoReset ni > ISet.singleton (reset_name ni), VSet.empty 
474 
 MComment _ > assert false (* not available for EMF output *) 
475 

476 

477 
let pp_emf_cst_or_var_list = 
478 
fprintf_list ~sep:",@ " pp_emf_cst_or_var 
479 

480 
let rec pp_emf_instr2 m fmt i = 
481 
(* let arguments_vars = Utils.ISet.elements (get_instr_rhs_vars i) in *) 
482 
let pp_content fmt i = 
483 
match Corelang.get_instr_desc i with 
484 
 MLocalAssign(lhs, expr) 
485 
> ( 
486 
(match expr.value_desc with 
487 
 Fun (fun_id, vl) > ( 
488 
(* Thanks to normalization, vl shall only contain constant or 
489 
local/state vars but not calls to other functions *) 
490 
fprintf fmt "\"kind\": \"operator\",@ "; 
491 
fprintf fmt "\"lhs\": \"%a\",@ " Printers.pp_var_name lhs; 
492 
fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]" 
493 
fun_id 
494 
pp_emf_cst_or_var_list vl 
495 
) 
496 
 Array _  Access _  Power _ > assert false (* No array expression allowed yet *) 
497 
 Cst _ 
498 
 LocalVar _ 
499 
 StateVar _ > ( 
500 
fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a" 
501 
Printers.pp_var_name lhs 
502 
pp_emf_cst_or_var expr 
503 
)) ) 
504  
505 
 MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a 
506 
variable or a constant, no function anymore! *) 
507 
> ( 
508 
fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a" 
509 
Printers.pp_var_name lhs 
510 
pp_emf_cst_or_var expr 
511 
) 
512 

513 
 MReset id 
514 
> ( 
515 
fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\"" 
516 
(reset_name id) 
517 
) 
518 
 MNoReset id 
519 
> ( 
520 
fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\"" 
521 
(reset_name id) 
522 
) 
523 

524 
 MBranch (g, hl) > ( 
525 
let outputs, inputs = branch_instr_vars i in 
526 
fprintf fmt "\"kind\": \"branch\",@ "; 
527 
fprintf fmt "\"guard\": %a,@ " pp_emf_cst_or_var g; (* it has to be a variable or a constant *) 
528 
fprintf fmt "\"outputs\": [%a],@ " (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs); 
529 
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl 
530 
(* (let guard_inputs = get_expr_vars g in 
531 
VSet.elements (VSet.diff inputs guard_inputs))  previous version to 
532 
removed guard's variable from inputs *) 
533 
(VSet.elements inputs) 
534 
; 
535 
fprintf fmt "@[<v 2>\"branches\": {@ %a@]}@ " 
536 
(fprintf_list ~sep:",@ " 
537 
(fun fmt (tag, instrs_tag) > 
538 
let (*branch_outputs*) _, branch_inputs = branch_block_vars instrs_tag in 
539 

540 
fprintf fmt "@[<v 2>\"%s\": {@ " tag; 
541 
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl (VSet.elements branch_inputs); 
542 
fprintf fmt "@[<v 2>\"instrs\": {@ "; 
543 
fprintf_list ~sep:",@ " (pp_emf_instr2 m) fmt instrs_tag; 
544 
fprintf fmt "@]}@ "; 
545 
fprintf fmt "@]}" 
546  
547 
) 
548 
) 
549 
hl 
550 
) 
551  
552 
 MStep ([var], f, _) when is_arrow_fun m i > (* Arrow case *) ( 
553 
fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\"" 
554 
f 
555 
Printers.pp_var_name var 
556 
(reset_name f) 
557 
) 
558  
559 
 MStep (outputs, f, inputs) > ( 
560 
let node_f = Machine_code.get_node_def f m in 
561 
let is_stateful = List.mem_assoc f m.minstances in 
562 
fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%s\",@ \"id\": \"%s\",@ " 
563 
(if is_stateful then "statefulcall" else "statelesscall") 
564 
(node_f.node_id) 
565 
f; 
566 
fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]" 
567 
(fprintf_list ~sep:",@ " (fun fmt v > fprintf fmt "\"%a\"" Printers.pp_var_name v)) outputs 
568 
pp_emf_cst_or_var_list inputs; 
569 
if is_stateful then fprintf fmt ",@ \"reset\": \"%s\"" (reset_name f) else fprintf fmt "@ " 
570 
) 
571  
572 
 MComment _ 
573 
> Format.eprintf "unhandled comment in EMF@.@?"; assert false 
574 
(* not available for EMF output *) 
575  
576 
in 
577 
fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i; 
578 
fprintf fmt "%a@ " pp_content i; 
579 
(* fprintf fmt "@[<v 2>\"original_lustre_expr\": [@ \"%a\"@]]@]" (pp_original_lustre_expression m) i; *) 
580 
fprintf fmt "}@]" 
581  
582 

583 

584 
(* A (normalized) node becomes a JSON struct 
585 
node foo (in1, in2: int) returns (out1, out2: int); 
586 
var x : int; 
587 
let 
588 
x = bar(in1, in2);  a stateful node 
589 
out1 = x; 
590 
out2 = in2; 
591 
tel 
592  
593 
Since foo contains a stateful node, it is stateful itself. Its prototype is 
594 
extended with a reset input. When the node is reset, each of its "pre" expression 
595 
is reset as well as all calls to stateful node it contains. 
596  
597 
will produce the following JSON struct: 
598 
"foo": {"kind": "stateful", 
599 
inputs: [{name: "in1", type: "int"}, 
600 
{name: "in2", type: "int"}, 
601 
], 
602 
outputs: [{name: "out1", type: "int"}, {name: "out2", type: "int"}], 
603 
locals: [{name: "x", type: "int"}], 
604 
instrs: { 
605 
def_x: { lhs: ["x"], 
606 
rhs: {type: "statefulcall", name: "bar", 
607 
args: [in1, in2], reset: [ni4_reset] } 
608 
} 
609 

610 
def_out1: { lhs: "out1", rhs: "x" } , 
611 
def_out2: { lhs: "out2", rhs: "in2"} 
612 
} 
613 
} 
614  
615 
Basically we have the following different definitions 
616 
1. local assign of a variable to another one: 
617 
def_out1: { kind: "local_assign", lhs: "out1", rhs: "x" }, 
618  
619 
2. pre construct over a variable (this is a state assign): 
620 
def_pre_x: { kind: "pre", lhs: "pre_x", rhs: "x" }, 
621  
622 
3. arrow constructs, while there is not specific input, it could be reset 
623 
by a specific signal. We register it as a fresh rhs var: 
624 
def_arrow: { kind: "arrow", name: "ni4", lhs: "is_init", rhs: "reset_ni4"} 
625  
626 
2. call to a stateless function, typically an operator 
627 
def_x: { kind: "statelesscall", lhs: ["x"], 
628 
name: "bar", rhs: [in1, in2]} 
629 

630 
or in the operator version 
631 
def_x: { kind: "operator", lhs: ["x"], 
632 
name: "+", rhs: [in1, in2]} 
633 

634  
635 
In Simulink this should introduce a subsystem in the first case or a 
636 
regular block in the second with card(lhs) outputs and card{args} inputs. 
637  
638 
3. call to a stateful node. It is similar to the stateless above, 
639 
with the addition of the reset argument 
640 
{ def_x: { kind: "statefulcall", lhs: ["x"], 
641 
name: "bar", rhs: [in1, in2], reset: [ni4_reset] } 
642 
} 
643 

644 
In lustrec compilation phases, a unique id is associated to this specific 
645 
instance of stateful node "bar", here ni4. 
646 
Instruction such as reset(ni4) or noreset(ni4) may  or not  reset this 
647 
specific node. This corresponds to "every c" suffix of a node call in lustre. 
648  
649 
In Simulink this should introduce a subsystem that has this extra reset input. 
650 
The reset should be defined as an "OR" over (1) the input reset of the parent 
651 
node, __reset in the present example and (2) any occurence of reset(ni4) in 
652 
the instructions. 
653  
654 
4. branching construct: (guard expr, (tag, instr list) list) 
655 
"merge_XX": { type: "branch", guard: "var_guard", 
656 
inputs: ["varx", "vary"], 
657 
outputs: ["vark", "varz"], 
658 
branches: {"tag1": {liste_of_definitions (14)}, ...} 
659 
} 
660 

661  
662 
In Simulink, this should become one IF block to produce enable ports 
663 
"var_guard == tag1", "var_guard == tag2", .... as well as one action 
664 
block per branch: each of these action block shall 
665 
*) 
666 
let pp_machine fmt m = 
667 
try 
668 
fprintf fmt "@[<v 2>\"%s\": {@ " 
669 
m.mname.node_id; 
670 
fprintf fmt "\"kind\": %t,@ \"inputs\": [%a],@ \"outputs\": [%a],@ \"locals\": [%a],@ " 
671 
(fun fmt > if not ( snd (get_stateless_status m) ) 
672 
then fprintf fmt "\"stateful\"" 
673 
else fprintf fmt "\"stateless\"") 
674 
pp_emf_vars_decl m.mstep.step_inputs 
675 
pp_emf_vars_decl m.mstep.step_outputs 
676 
pp_emf_vars_decl m.mstep.step_locals 
677 
; 
678 
fprintf fmt "\"instrs\": {@[<v 0> %a@]@ }" 
679 
(fprintf_list ~sep:",@ " (pp_emf_instr2 m)) m.mstep.step_instrs; 
680 
fprintf fmt "@]@ }" 
681 
with Unhandled msg > ( 
682 
eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ " 
683 
m.mname.node_id; 
684 
eprintf "%s@ " msg; 
685 
eprintf "node skipped  no output generated@ @]@." 
686 
) 
687  
688 
(****************************************************) 
689 
(* Main function: iterates over node and print them *) 
690 
(****************************************************) 
691 
let pp_meta fmt basename = 
692 
fprintf fmt "\"meta\": @[<v 0>{@ "; 
693 
Utils.fprintf_list ~sep:",@ " 
694 
(fun fmt (k, v) > fprintf fmt "\"%s\": \"%s\"" k v) 
695 
fmt 
696 
["compilername", (Filename.basename Sys.executable_name); 
697 
"compilerversion", Version.number; 
698 
"command", (String.concat " " (Array.to_list Sys.argv)); 
699 
"source_file", basename 
700 
] 
701 
; 
702 
fprintf fmt "@ @]},@ " 
703 

704 
let translate fmt basename prog machines = 
705 
fprintf fmt "@[<v 0>{@ "; 
706 
pp_meta fmt basename; 
707 
fprintf fmt "\"nodes\": @[<v 0>{@ "; 
708 
(* Previous alternative: mapping normalized lustre to EMF: 
709 
fprintf_list ~sep:",@ " pp_decl fmt prog; *) 
710 
fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines); 
711 
fprintf fmt "@ @]}"; 
712 
fprintf fmt "@ @]}" 
713  
714 
(* Local Variables: *) 
715 
(* compilecommand: "make C ../.." *) 
716 
(* End: *) 