Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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 (1-4)}, ...}
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
    ["compiler-name", (Filename.basename Sys.executable_name);
697
     "compiler-version", 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
(* compile-command: "make -C ../.." *)
716
(* End: *)