Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / EMF / EMF_backend.ml @ dd71e482

History | View | Annotate | Download (28.4 KB)

1 3ca27bc7 ploc
(* 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 a6df3992 Ploc
open LustreSpec
18 f7caf067 ploc
open Machine_code
19 a6df3992 Ploc
open Format
20
open Utils
21
22 f7caf067 ploc
exception Unhandled of string
23 3ca27bc7 ploc
    
24
25
(* Basic printing functions *)
26
    
27 a6df3992 Ploc
let pp_var_string fmt v = fprintf fmt "\"%s\"" v
28 9f0f88dd ploc
(*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 a6df3992 Ploc
31 9f0f88dd ploc
let pp_emf_var_decl fmt v =
32 ab1c9ed2 Bourbouh
  fprintf fmt "@[{\"name\": \"%a\", \"type\":\"%a\"}@]"
33 9f0f88dd ploc
    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 3ca27bc7 ploc
    
45
(* Matlab starting counting from 1.
46
   simple function to extract the element id in the list. Starts from 1. *)
47 f7caf067 ploc
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 3ca27bc7 ploc
52
(**********************************************)
53
(* Old stuff: printing normalized code as EMF *)     
54
(**********************************************)
55
56
(*
57 a6df3992 Ploc
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 32539b6d ploc
	 Format.fprintf fmt "u%i" (get_idx id vars)
64 a6df3992 Ploc
       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 97be8db8 Teme
    | 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 a6df3992 Ploc
    | 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 30dee850 Teme
    | Expr_pre e -> fprintf fmt "UNITDELAY"
78 a6df3992 Ploc
    | 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 97be8db8 Teme
    | "!=", 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 a6df3992 Ploc
    | "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 97be8db8 Teme
123 d3e837ea Ploc
	fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @]}"
124 a6df3992 Ploc
	  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 d3e837ea Ploc
  fprintf fmt "@[<v 2>\"%s\": {@ \"inputs\": [%a],@ \"outputs\": [%a],@ "
134 a6df3992 Ploc
    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 d3e837ea Ploc
    (fprintf_list ~sep:",@ " pp_stmt ) nd.node_stmts;
139 a6df3992 Ploc
  fprintf fmt "@]@ }"
140 30dee850 Teme
141 a6df3992 Ploc
let pp_decl fmt decl =
142
  match decl.top_decl_desc with
143
  | Node nd -> fprintf fmt "%a@ " pp_node nd
144 30dee850 Teme
  | ImportedNode _
145 a6df3992 Ploc
  | Const _
146 30dee850 Teme
  | Open _
147 a6df3992 Ploc
  | TypeDef _ -> eprintf "should not happen in EMF backend"
148 3ca27bc7 ploc
*)
149
150
151
(**********************************************)
152 9f0f88dd ploc
(*   Utility functions: arrow and lustre expr *)
153 3ca27bc7 ploc
(**********************************************)
154 a6df3992 Ploc
155 524060b3 ploc
(* 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 27d18db9 ploc
     (*
185 9f0f88dd ploc
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 27d18db9 ploc
  *)     
199 9f0f88dd ploc
(**********************************************)
200
(*   Printing machine code as EMF             *)
201
(**********************************************)
202 524060b3 ploc
203 9f0f88dd ploc
(*******************
204
     
205 145379a9 ploc
(* 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 524060b3 ploc
let rec pp_matlab_val vars fmt v =
209 f7caf067 ploc
  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 32539b6d ploc
       Format.fprintf fmt "u%i" (get_idx id vars)
216 f7caf067 ploc
     else
217 524060b3 ploc
       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 f7caf067 ploc
  | 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 145379a9 ploc
  (* eprintf "print %s with %i args@.@?" id (List.length vl);*)
222 f7caf067 ploc
  match id, vl with
223 524060b3 ploc
    | "+", [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 a6df3992 Ploc
242 3ca27bc7 ploc
     
243 1bff14ac ploc
244 145379a9 ploc
(* 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 524060b3 ploc
let pp_matlab_basic_instr m vars fmt i =
249 1bff14ac ploc
  match Corelang.get_instr_desc i with
250
  | MLocalAssign (var,v) 
251 524060b3 ploc
  | MStateAssign (var,v) -> fprintf fmt "y = %a" (pp_matlab_val vars) v
252 f7caf067 ploc
  | MReset _           
253 145379a9 ploc
    -> Format.eprintf "unhandled reset in EMF@.@?"; assert false
254 f7caf067 ploc
  | MNoReset _
255 145379a9 ploc
    -> Format.eprintf "unhandled noreset in EMF@.@?"; assert false
256 524060b3 ploc
  | MBranch _ (* branching instructions already handled *)
257
    -> Format.eprintf "unhandled branch statement in EMF (should have been filtered out before)@.@?";
258
      assert false
259 145379a9 ploc
  | 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 f7caf067 ploc
267 3ca27bc7 ploc
268 524060b3 ploc
let rec get_instr_lhs_var i =
269 3ca27bc7 ploc
  match Corelang.get_instr_desc i with
270 f7caf067 ploc
  | MLocalAssign (var,_) 
271
  | MStateAssign (var,_) 
272 524060b3 ploc
  | 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 f7caf067 ploc
  | MReset _           
281
  | MNoReset _
282
  | MComment _ -> assert false (* not  available for EMF output *)
283
and get_instrs_var il =
284
  match il with
285 524060b3 ploc
  | i::_ -> get_instr_lhs_var i (* looking for the first instr *)
286 f7caf067 ploc
  | _ -> assert false
287
288 3ca27bc7 ploc
  
289 f7caf067 ploc
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 3ca27bc7 ploc
297 524060b3 ploc
let rec get_instr_rhs_vars i =
298 3ca27bc7 ploc
  match Corelang.get_instr_desc i with
299 f7caf067 ploc
  | MLocalAssign (_,v)  
300
  | MStateAssign (_,v) -> get_val_vars v
301 145379a9 ploc
  | 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 f7caf067 ploc
     Utils.ISet.union
304
       (get_val_vars c)
305
       (
306
	 Utils.ISet.union
307 524060b3 ploc
	   (get_instr_rhs_vars case1)
308
	   (get_instr_rhs_vars case2)
309 f7caf067 ploc
       )
310 524060b3 ploc
  | 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 1bff14ac ploc
323
324 524060b3 ploc
     
325
let rec pp_emf_instr m fmt i =
326 145379a9 ploc
  (* 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 524060b3 ploc
  let arguments_vars = Utils.ISet.elements (get_instr_rhs_vars i) in	
329 145379a9 ploc
  
330
  match Corelang.get_instr_desc i with
331 524060b3 ploc
  (* 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 145379a9 ploc
      var.var_id
344
      (fprintf_list ~sep:", " pp_var_string) arguments_vars
345
      (pp_original_lustre_expression m) i
346
  )
347 524060b3 ploc
  | 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 9f0f88dd ploc
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 dd71e482 ploc
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 9f0f88dd ploc
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 dd71e482 ploc
let rec branch_block_vars il =
444 27d18db9 ploc
  List.fold_left
445 dd71e482 ploc
    (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 27d18db9 ploc
  match Corelang.get_instr_desc i with
451 dd71e482 ploc
  | 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 27d18db9 ploc
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
472
  | MReset ni           
473 dd71e482 ploc
  | MNoReset ni -> ISet.singleton (reset_name ni), VSet.empty
474 27d18db9 ploc
  | MComment _ -> assert false (* not  available for EMF output *)
475
     
476
  
477 9f0f88dd ploc
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 ab1c9ed2 Bourbouh
	fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
493 9f0f88dd ploc
	  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 1bff14ac ploc
    
524 9f0f88dd ploc
  | MBranch (g, hl) -> (
525 dd71e482 ploc
    let outputs, inputs = branch_instr_vars i in
526 9f0f88dd ploc
    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 dd71e482 ploc
    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 9f0f88dd ploc
      (fprintf_list ~sep:",@ "
537
	 (fun fmt (tag, instrs_tag) ->
538 dd71e482 ploc
	   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 9f0f88dd ploc
	   fprintf_list ~sep:",@ " (pp_emf_instr2 m) fmt instrs_tag;
544 dd71e482 ploc
	   fprintf fmt "@]}@ ";
545
	   fprintf fmt "@]}"
546 9f0f88dd ploc
547
	 )
548
      )
549
      hl
550 dd71e482 ploc
   )
551 9f0f88dd ploc
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 dd71e482 ploc
    fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
567 9f0f88dd ploc
      (fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" Printers.pp_var_name v)) outputs
568
      pp_emf_cst_or_var_list inputs;
569 dd71e482 ploc
    if is_stateful then fprintf fmt ",@ \"reset\": \"%s\"" (reset_name f) else fprintf fmt "@ "
570 9f0f88dd ploc
  )
571
572
  | MComment _ 
573
    -> Format.eprintf "unhandled comment in EMF@.@?"; assert false
574
  (* not  available for EMF output *)
575
576
  in
577 dd71e482 ploc
  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 9f0f88dd ploc
  fprintf fmt "}@]"
581
582
       
583
       
584 524060b3 ploc
(* 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 9f0f88dd ploc
   "foo": {"kind":  "stateful",
599
           inputs:  [{name: "in1", type: "int"}, 
600 524060b3 ploc
                     {name: "in2", type: "int"}, 
601
                    ],
602
           outputs: [{name: "out1", type: "int"}, {name: "out2", type: "int"}],
603
           locals:  [{name: "x", type: "int"}],
604 ab1c9ed2 Bourbouh
           instrs:  {
605
                    def_x: { lhs: ["x"], 
606 524060b3 ploc
                               rhs: {type: "statefulcall", name: "bar", 
607
                                     args: [in1, in2], reset: [ni4_reset] } 
608
                             }
609 ab1c9ed2 Bourbouh
                    
610
                    def_out1: { lhs: "out1", rhs: "x" } ,
611
                    def_out2: { lhs: "out2", rhs: "in2"}
612 524060b3 ploc
                    }
613
           }
614
615 9f0f88dd ploc
Basically we have the following different definitions
616
1. local assign of a variable to another one:
617 ab1c9ed2 Bourbouh
   def_out1: { kind: "local_assign", lhs: "out1", rhs: "x" },
618 9f0f88dd ploc
619
2. pre construct over a variable (this is a state assign):
620 ab1c9ed2 Bourbouh
   def_pre_x: { kind: "pre", lhs: "pre_x", rhs: "x" },
621 9f0f88dd ploc
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 ab1c9ed2 Bourbouh
   def_arrow: { kind: "arrow", name: "ni4", lhs: "is_init", rhs: "reset_ni4"}
625 9f0f88dd ploc
626 524060b3 ploc
2. call to a stateless function, typically an operator
627 ab1c9ed2 Bourbouh
    def_x: { kind: "statelesscall", lhs: ["x"], 
628 9f0f88dd ploc
              name: "bar", rhs: [in1, in2]} 
629 ab1c9ed2 Bourbouh
   
630 524060b3 ploc
  or in the operator version 
631 ab1c9ed2 Bourbouh
   def_x: { kind: "operator", lhs: ["x"], 
632 9f0f88dd ploc
              name: "+", rhs: [in1, in2]} 
633 ab1c9ed2 Bourbouh
   
634 524060b3 ploc
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 9f0f88dd ploc
    { def_x: { kind: "statefulcall", lhs: ["x"], 
641
               name: "bar", rhs: [in1, in2], reset: [ni4_reset] } 
642
      }
643 524060b3 ploc
  
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 ab1c9ed2 Bourbouh
    "merge_XX": { type: "branch", guard: "var_guard", 
656 524060b3 ploc
                   inputs:   ["varx", "vary"],
657
                   outputs:  ["vark", "varz"],
658 ab1c9ed2 Bourbouh
                   branches: {"tag1": {liste_of_definitions (1-4)}, ...}
659 524060b3 ploc
                 }
660 ab1c9ed2 Bourbouh
   
661 524060b3 ploc
662 9f0f88dd ploc
  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 524060b3 ploc
*)     
666 f7caf067 ploc
let pp_machine fmt m =
667
  try
668 9f0f88dd ploc
    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 ab1c9ed2 Bourbouh
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ }"
679 9f0f88dd ploc
      (fprintf_list ~sep:",@ " (pp_emf_instr2 m)) m.mstep.step_instrs;
680 f7caf067 ploc
    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 3ca27bc7 ploc
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 f7caf067 ploc
    
704 3ca27bc7 ploc
let translate fmt basename prog machines =
705 a6df3992 Ploc
  fprintf fmt "@[<v 0>{@ ";
706 3ca27bc7 ploc
  pp_meta fmt basename;
707
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
708 145379a9 ploc
  (* Previous alternative: mapping normalized lustre to EMF: 
709
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
710 ab1c9ed2 Bourbouh
  fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
711 3ca27bc7 ploc
  fprintf fmt "@ @]}";
712 a6df3992 Ploc
  fprintf fmt "@ @]}"
713 3ca27bc7 ploc
714
(* Local Variables: *)
715
(* compile-command: "make -C ../.." *)
716
(* End: *)