Project

General

Profile

Download (20 KB) Statistics
| Branch: | Tag: | Revision:
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 2475c9e8 ploc
   code. We now rely on machine code printing. The old code is available in old
14
   commits (eg in dd71e482a9d0).
15 3ca27bc7 ploc
16 2475c9e8 ploc
   
17
   A (normalized) node becomes a JSON struct
18
   node foo (in1, in2: int) returns (out1, out2: int);
19
   var x : int;
20
   let
21
   x = bar(in1, in2); -- a stateful node
22
   out1 = x;
23
   out2 = in2;
24
   tel
25 a6df3992 Ploc
26 2475c9e8 ploc
   Since foo contains a stateful node, it is stateful itself. Its prototype is 
27
   extended with a reset input. When the node is reset, each of its "pre" expression
28
   is reset as well as all calls to stateful node it contains. 
29 3ca27bc7 ploc
30 2475c9e8 ploc
   will produce the following JSON struct:
31
   "foo": {"kind":  "stateful",
32
   inputs:  [{name: "in1", type: "int"}, 
33
   {name: "in2", type: "int"}, 
34
   ],
35
   outputs: [{name: "out1", type: "int"}, {name: "out2", type: "int"}],
36
   locals:  [{name: "x", type: "int"}],
37
   instrs:  {
38
   def_x: { lhs: ["x"], 
39
   rhs: {type: "statefulcall", name: "bar", 
40
   args: [in1, in2], reset: [ni4_reset] } 
41
   }
42
   
43
   def_out1: { lhs: "out1", rhs: "x" } ,
44
   def_out2: { lhs: "out2", rhs: "in2"}
45
   }
46
   }
47 3ca27bc7 ploc
48 2475c9e8 ploc
   Basically we have the following different definitions
49
   1. local assign of a variable to another one:
50
   def_out1: { kind: "local_assign", lhs: "out1", rhs: "x" },
51 3ca27bc7 ploc
52 2475c9e8 ploc
   2. pre construct over a variable (this is a state assign):
53
   def_pre_x: { kind: "pre", lhs: "pre_x", rhs: "x" },
54
55
   3. arrow constructs, while there is not specific input, it could be reset 
56
   by a specific signal. We register it as a fresh rhs var:
57
   def_arrow: { kind: "arrow", name: "ni4", lhs: "is_init", rhs: "reset_ni4"}
58
59
   2. call to a stateless function, typically an operator
60
   def_x: { kind: "statelesscall", lhs: ["x"], 
61
   name: "bar", rhs: [in1, in2]} 
62
   
63
   or in the operator version 
64
   def_x: { kind: "operator", lhs: ["x"], 
65
   name: "+", rhs: [in1, in2]} 
66
   
67
68
   In Simulink this should introduce a subsystem in the first case or a 
69
   regular block in the second with card(lhs) outputs and card{args} inputs.
70
71
   3. call to a stateful node. It is similar to the stateless above, 
72
   with the addition of the reset argument
73
   { def_x: { kind: "statefulcall", lhs: ["x"], 
74
   name: "bar", rhs: [in1, in2], reset: [ni4_reset] } 
75
   }
76
   
77
   In lustrec compilation phases, a unique id is associated to this specific
78
   instance of stateful node "bar", here ni4. 
79
   Instruction such as reset(ni4) or noreset(ni4) may -- or not -- reset this 
80
   specific node. This corresponds to "every c" suffix of a node call in lustre.
81
82
   In Simulink this should introduce a subsystem that has this extra reset input.  
83
   The reset should be defined as an "OR" over (1) the input reset of the parent 
84
   node, __reset in the present example and (2) any occurence of reset(ni4) in 
85
   the instructions.
86
87
   4. branching construct: (guard expr, (tag, instr list) list)
88
   "merge_XX": { type: "branch", guard: "var_guard", 
89
   inputs:   ["varx", "vary"],
90
   outputs:  ["vark", "varz"],
91
   branches: {"tag1": {liste_of_definitions (1-4)}, ...}
92
   }
93
   
94
95
   In Simulink, this should become one IF block to produce enable ports 
96
   "var_guard == tag1", "var_guard == tag2", .... as well as one action 
97
   block per branch: each of these action block shall  
98 a6df3992 Ploc
99 3ca27bc7 ploc
*)
100
101 8446bf03 ploc
open Lustre_types
102
open Machine_code_types
103 2863281f ploc
open Machine_code_common
104 2475c9e8 ploc
open Format 
105
open EMF_common
106
exception Unhandled of string
107
108
module ISet = Utils.ISet
109
let fprintf_list = Utils.fprintf_list
110
  
111
112 3ca27bc7 ploc
113
(**********************************************)
114 9f0f88dd ploc
(*   Utility functions: arrow and lustre expr *)
115 3ca27bc7 ploc
(**********************************************)
116 a6df3992 Ploc
117 524060b3 ploc
(* detect whether the instruction i represents an ARROW, ie an arrow with true
118
   -> false *)
119
let is_arrow_fun m i =
120
  match Corelang.get_instr_desc i with
121 ca7e8027 Lélio Brun
  | MStep ([_], i, vl) ->
122 7eafa0e1 ploc
     (
123
       try
124 2863281f ploc
	 let name = (get_node_def i m).node_id in
125 7eafa0e1 ploc
	 match name, vl with
126
	 | "_arrow", [v1; v2] -> (
127
	   match v1.value_desc, v2.value_desc with
128
	   | Cst c1, Cst c2 ->
129
	      if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then
130
		true
131
	      else
132
		assert false (* only handle true -> false *)
133
	   | _ -> assert false
134
	 )
135
	    
136
	 | _ -> false
137
       with
138
       | Not_found -> false (* Not declared (should have been detected now, or
139
			       imported node) *)
140
     )
141 524060b3 ploc
  | _ -> false
142 7eafa0e1 ploc
     
143
     
144
     
145
let is_resetable_fun lustre_eq =
146
  (* We extract the clock if it exist from the original lustre equation *)
147
  match lustre_eq with
148
  | Some eq -> (
149
    match eq.eq_rhs.expr_desc with
150
    | Expr_appl(_,_,reset) -> (
151
      match reset with None -> false | Some _ -> true
152
    )
153 42f91c0b ploc
    | Expr_arrow _ -> true
154
    | _ -> Format.eprintf "reseting expr %a@.@?" Printers.pp_expr eq.eq_rhs; assert false
155 7eafa0e1 ploc
  )
156
  | None -> assert false (* should have been assigned to an original lustre equation *)
157 524060b3 ploc
158 9f0f88dd ploc
(**********************************************)
159
(*   Printing machine code as EMF             *)
160
(**********************************************)
161 524060b3 ploc
162 9f0f88dd ploc
     
163 dd71e482 ploc
164 9f0f88dd ploc
let branch_cpt = ref 0
165
let get_instr_id fmt i =
166
  match Corelang.get_instr_desc i with
167 785b64f9 ploc
  | MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
168 6d1693b9 Lélio Brun
  | MSetReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
169
  (* TODO: handle clear_reset *)
170
  | MClearReset -> ()
171 ca7e8027 Lélio Brun
  | MBranch _ -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
172 785b64f9 ploc
  | MStep (outs, id, _) ->
173
     print_protect fmt 
174
       (fun fmt -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)
175 9f0f88dd ploc
  | _ -> () (* No name *)
176
177 7eafa0e1 ploc
let rec branch_block_vars m il =
178 27d18db9 ploc
  List.fold_left
179 1b721bfd ploc
    (fun (accu_all_def, accu_def, accu_read) i ->
180 7eafa0e1 ploc
      let all_defined_vars, common_def_vars, read_vars = branch_instr_vars m i in
181 1b721bfd ploc
      ISet.union accu_all_def all_defined_vars,
182
      ISet.union accu_def common_def_vars,
183
      VSet.union accu_read read_vars)
184
    (ISet.empty, ISet.empty, VSet.empty) il
185 42f91c0b ploc
  
186 7eafa0e1 ploc
and branch_instr_vars m i =
187 42f91c0b ploc
  (* Returns all_outputs, outputs, inputs of the instruction. It is
188
     only called on MBranch instructions but evaluate recursively
189
     instructions appearing in branches.
190
191
     It is used to gather the global input/output of a switch and
192
     print it at the begin of the JSON subtree.
193
194
     The set "All outputs" is used to filter out input variables
195
     belong to that set. *)
196
197 27d18db9 ploc
  match Corelang.get_instr_desc i with
198 dd71e482 ploc
  | MLocalAssign (var,expr) 
199 42f91c0b ploc
    | MStateAssign (var,expr) -> ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
200 7eafa0e1 ploc
  | MStep (vars, f, args)  ->
201
     let is_stateful = List.mem_assoc f m.minstances in 
202 1b721bfd ploc
     let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in
203 7eafa0e1 ploc
     let args_vars =
204
       List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args in
205
     
206 1b721bfd ploc
     lhs, lhs,
207 7eafa0e1 ploc
     (
208
       if is_stateful && is_resetable_fun i.lustre_eq then
209
	 let reset_var =
210
	   let loc = Location.dummy_loc in
211
	   Corelang.mkvar_decl loc
212
	     (reset_name f,
213
	      Corelang.mktyp loc Tydec_bool, Corelang.mkclock loc Ckdec_any,
214
	      false,
215 66359a5e ploc
	      None,
216 7eafa0e1 ploc
	      None) 
217
	 in
218
	 VSet.add reset_var args_vars
219
       else
220
	 args_vars
221
     )
222 dd71e482 ploc
  | MBranch (g,(_,hd_il)::tl)     -> (* We focus on variables defined in all branches *)
223
     let read_guard = get_expr_vars g in
224 42f91c0b ploc
     (* Bootstrapping with first item *) 
225 7eafa0e1 ploc
     let all_def_vars_hd, def_vars_hd, read_vars_hd = branch_block_vars m hd_il in
226 1b721bfd ploc
     let all_def_vars, def_vars, read_vars =
227 dd71e482 ploc
       List.fold_left
228 1b721bfd ploc
	 (fun (all_def_vars, def_vars, read_vars) (_, il) ->
229 7eafa0e1 ploc
	   (* We accumulate reads but intersect writes *)
230
	   let all_writes_il, writes_il, reads_il = branch_block_vars m il in
231 1b721bfd ploc
	   ISet.union all_def_vars all_writes_il,
232 dd71e482 ploc
	   ISet.inter def_vars writes_il,
233 1b721bfd ploc
	   VSet.union read_vars reads_il
234 dd71e482 ploc
	 )
235 1b721bfd ploc
	 (all_def_vars_hd, def_vars_hd, read_vars_hd)
236 dd71e482 ploc
	 tl
237
     in
238 42f91c0b ploc
     (* all_def_vars correspond to variables written or defined in one
239
        of the branch. It may happen that a variable is defined in one
240
        but not in the other, because of reset for example.  
241
242
        def_vars are variables defined in all branches. *)
243
244
245 1b721bfd ploc
     all_def_vars, def_vars, VSet.union read_guard read_vars
246 27d18db9 ploc
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
247 6d1693b9 Lélio Brun
  | MSetReset ni
248
  | MNoReset ni ->
249
    let write = ISet.singleton (reset_name ni) in
250
    write, write, VSet.empty
251 aaa8e454 Lélio Brun
  (* TODO: handle clear_reset and reset flag *)
252
  | MClearReset | MResetAssign _ -> ISet.empty, ISet.empty, VSet.empty
253 42f91c0b ploc
  | MSpec _ | MComment _ -> assert false (* not  available for EMF output *)
254 27d18db9 ploc
     
255 01b501ca ploc
(* A kind of super join_guards: all MBranch are postponed and sorted by
256
   guards so they can be easier merged *)
257
let merge_branches instrs =
258
  let instrs, branches =
259
    List.fold_right (fun i (il, branches) ->
260
      match Corelang.get_instr_desc i with
261
	MBranch _ -> il, i::branches
262
      | _ -> i::il, branches
263
    ) instrs ([],[])
264
  in
265
  let sorting_branches b1 b2 =
266
    match Corelang.get_instr_desc b1, Corelang.get_instr_desc b2 with
267 ca7e8027 Lélio Brun
    | MBranch(g1, _), MBranch(g2, _) ->
268 01b501ca ploc
       compare g1 g2
269
    | _ -> assert false
270
  in
271
  let sorted_branches = List.sort sorting_branches branches in
272 2863281f ploc
  instrs @ (join_guards_list sorted_branches)
273 01b501ca ploc
    
274 2475c9e8 ploc
let rec pp_emf_instr m fmt i =
275 9f0f88dd ploc
  let pp_content fmt i =
276
    match Corelang.get_instr_desc i with
277 aaa8e454 Lélio Brun
    | MLocalAssign(lhs, expr) ->
278
      begin match expr.value_desc with
279
        | Fun (fun_id, vl) ->
280
          (* Thanks to normalization, vl shall only contain constant or
281
             local/state vars but not calls to other functions *)
282
          fprintf fmt "\"kind\": \"operator\",@ ";
283
          fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;
284
          fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
285
            fun_id
286
            (pp_emf_cst_or_var_list m) vl
287
        | Array _ | Access _ | Power _
288
        | Cst _
289
        | Var _ ->
290
          fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
291
            pp_var_name lhs
292
            (pp_emf_cst_or_var m) expr
293
        | ResetFlag ->
294
          (* TODO: handle reset flag *)
295
          assert false
296
      end
297 8f0e9f74 ploc
298
    | MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a
299 aaa8e454 Lélio Brun
                                 variable or a constant, no function anymore! *)
300 8f0e9f74 ploc
      -> (
301 aaa8e454 Lélio Brun
          fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
302
            pp_var_name lhs
303
            (pp_emf_cst_or_var m) expr
304
        )
305
306 6d1693b9 Lélio Brun
    | MSetReset id
307 8f0e9f74 ploc
      -> (
308 aaa8e454 Lélio Brun
          fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
309
            (reset_name id)
310
        )
311 8f0e9f74 ploc
    | MNoReset id           
312
      -> (
313 aaa8e454 Lélio Brun
          fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
314
            (reset_name id)
315
        )
316
    (* TODO: handle clear_reset and reset flag *)
317
    | MClearReset | MResetAssign _ -> ()
318 1b721bfd ploc
319 aaa8e454 Lélio Brun
    | MBranch (g, hl) -> (
320
        let all_outputs, outputs, inputs = branch_instr_vars m i in
321
        (* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)
322
        (* 	Machine_code.pp_instr i *)
323
        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *)
324
        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs) *)
325
        (* 	pp_emf_vars_decl *)
326
        (* 	(VSet.elements inputs) *)
327
328
        (* ; *)
329
        let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in
330 2196948d ploc
      (* Format.eprintf "Filtering in: %a@.@." *)
331
      (* 	pp_emf_vars_decl *)
332
      (* 	(VSet.elements inputs) *)
333 9f0f88dd ploc
334 2196948d ploc
      (* ; *)
335 8f0e9f74 ploc
      fprintf fmt "\"kind\": \"branch\",@ ";
336 c35de73b ploc
      fprintf fmt "\"guard\": %a,@ " (pp_emf_cst_or_var m) g; (* it has to be a variable or a constant *)
337 8f0e9f74 ploc
      fprintf fmt "\"outputs\": [%a],@ " (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs);
338
      fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
339
	(* (let guard_inputs = get_expr_vars g in
340
	   VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to
341
	   remove guard's variable from inputs *)
342
	(VSet.elements inputs)
343
      ;
344
      fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }"
345
	(fprintf_list ~sep:",@ "
346
	   (fun fmt (tag, instrs_tag) ->
347 7eafa0e1 ploc
	     let branch_all_lhs, _, branch_inputs = branch_block_vars m instrs_tag in
348 8f0e9f74 ploc
	     let branch_inputs = VSet.filter (fun v -> not (ISet.mem v.var_id branch_all_lhs)) branch_inputs in
349 2196948d ploc
	     fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt -> Format.pp_print_string fmt tag);
350 8f0e9f74 ploc
	     fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag; 
351
	     fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl (VSet.elements branch_inputs); 
352
	     fprintf fmt "@[<v 2>\"instrs\": {@ ";
353
	     (pp_emf_instrs m) fmt instrs_tag;
354
	     fprintf fmt "@]@ }";
355
	     fprintf fmt "@]@ }"
356
	   )
357
	)
358
	hl
359
    )
360 9f0f88dd ploc
361 8f0e9f74 ploc
    | MStep ([var], f, _) when is_arrow_fun m i -> (* Arrow case *) (
362
      fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\""
363
	f
364
	pp_var_name var
365
	(reset_name f)
366
    )
367
368
    | MStep (outputs, f, inputs) when not (is_imported_node f m) -> (
369 2863281f ploc
      let node_f = get_node_def f m in
370 8f0e9f74 ploc
      let is_stateful = List.mem_assoc f m.minstances in 
371
      fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ "
372
	(if is_stateful then "statefulcall" else "statelesscall")
373
	print_protect (fun fmt -> pp_print_string fmt (node_f.node_id)) 
374
	f;
375
      fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
376
	(fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" pp_var_name v)) outputs
377 c35de73b ploc
	(pp_emf_cst_or_var_list m) inputs;
378 8f0e9f74 ploc
      if is_stateful then
379
	fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}"
380
	  (reset_name f)
381 7eafa0e1 ploc
	  (is_resetable_fun i.lustre_eq)	  
382 8f0e9f74 ploc
      else fprintf fmt "@ "
383
    )
384
385
    | MStep(outputs, f, inputs ) -> (* This is an imported node *)
386
       EMF_library_calls.pp_call fmt m f outputs inputs
387
	 
388 42f91c0b ploc
    | MSpec _ | MComment _ 
389 8f0e9f74 ploc
      -> Format.eprintf "unhandled comment in EMF@.@?"; assert false
390 9f0f88dd ploc
  (* not  available for EMF output *)
391
  in
392 def94a59 ploc
    fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
393 568b5a26 ploc
    fprintf fmt "%a" pp_content i;
394
    fprintf fmt "@]@]@ }"
395 01b501ca ploc
and pp_emf_instrs m fmt instrs = fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
396 66359a5e ploc
397
let pp_emf_annot cpt fmt (key, ee) =
398
  let _ =
399
    fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }"
400
      !cpt
401
      (fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s)) key
402
      pp_emf_eexpr ee
403
  in
404
  incr cpt
405 59020713 ploc
406
let pp_emf_spec_mode fmt m =
407
  fprintf fmt "{@[";
408
  fprintf fmt "\"mode_id\": \"%s\",@ "
409
    m.mode_id;
410 42f91c0b ploc
  fprintf fmt "\"ensure\": [%a],@ "
411 59020713 ploc
    pp_emf_eexprs m.ensure;
412 42f91c0b ploc
  fprintf fmt "\"require\": [%a]@ "
413 59020713 ploc
    pp_emf_eexprs m.require;
414
  fprintf fmt "@]}"
415
  
416
let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode
417
418
let pp_emf_spec_import fmt i =
419
  fprintf fmt "{@[";
420
  fprintf fmt "\"contract\": \"%s\",@ "
421
    i.import_nodeid;
422
  fprintf fmt "\"inputs\": [%a],@ "
423 f4cba4b8 ploc
    pp_emf_expr i.inputs;
424 59020713 ploc
  fprintf fmt "\"outputs\": [%a],@ "
425 f4cba4b8 ploc
    pp_emf_expr i.outputs;
426 59020713 ploc
  fprintf fmt "@]}"
427
  
428
let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import
429
430
let pp_emf_spec fmt spec =
431
  fprintf fmt "{ @[<hov 0>";
432 42f91c0b ploc
  (* fprintf fmt "\"consts\": [%a],@ "
433
   *   pp_emf_consts spec.consts;
434
   * fprintf fmt "\"locals\": [%a],@ "
435
   *   pp_emf_vars_decl spec.locals;
436
   * fprintf fmt "\"stmts\": [%a],@ "
437
   *   pp_emf_stmts spec.stmts; *)
438 59020713 ploc
  fprintf fmt "\"assume\": [%a],@ "
439
    pp_emf_eexprs spec.assume;
440
  fprintf fmt "\"guarantees\": [%a],@ "
441
    pp_emf_eexprs spec.guarantees;
442 42f91c0b ploc
  fprintf fmt "\"modes\": [%a]@ "
443 59020713 ploc
    pp_emf_spec_modes spec.modes;
444 42f91c0b ploc
  (* fprintf fmt "\"imports\": [%a]@ "
445
   *   pp_emf_spec_imports spec.imports;   *)
446 59020713 ploc
  fprintf fmt "@] }"
447 66359a5e ploc
  
448
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
449
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
450 59020713 ploc
451 42f91c0b ploc
(* let pp_emf_contract fmt nd =
452
 *   let c = Printers.node_as_contract nd in
453
 *   fprintf fmt "@[<v 2>\"%a\": {@ "
454
 *     print_protect (fun fmt -> pp_print_string fmt nd.node_id);
455
 *   fprintf fmt "\"contract\": %a@ "
456
 *     pp_emf_spec c;
457
 *   fprintf fmt "@]@ }" *)
458 59020713 ploc
  
459 f7caf067 ploc
let pp_machine fmt m =
460 9f231bff ploc
  let instrs = (*merge_branches*) m.mstep.step_instrs in
461 f7caf067 ploc
  try
462 fbad3c4b ploc
    fprintf fmt "@[<v 2>\"%a\": {@ "
463 59020713 ploc
      print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
464 7ee5f69e Lélio Brun
    (match m.mspec.mnode_spec with
465
     | Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ "
466
     | _ -> ());
467 59020713 ploc
    fprintf fmt "\"imported\": \"false\",@ ";
468 66359a5e ploc
    fprintf fmt "\"kind\": %t,@ "
469 9f0f88dd ploc
      (fun fmt -> if not ( snd (get_stateless_status m) )
470
	then fprintf fmt "\"stateful\""
471 66359a5e ploc
	else fprintf fmt "\"stateless\"");
472
    fprintf fmt "\"inputs\": [%a],@ "
473
      pp_emf_vars_decl m.mstep.step_inputs;
474
    fprintf fmt "\"outputs\": [%a],@ "
475
      pp_emf_vars_decl m.mstep.step_outputs;
476
    fprintf fmt "\"locals\": [%a],@ "
477
      pp_emf_vars_decl m.mstep.step_locals;
478
    fprintf fmt "\"mems\": [%a],@ "
479
      pp_emf_vars_decl m.mmemory;
480 7c79dd93 ploc
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
481 66359a5e ploc
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
482 01b501ca ploc
      (pp_emf_instrs m) instrs;
483 7ee5f69e Lélio Brun
    (match m.mspec.mnode_spec with
484
     | None -> ()
485
     | Some (Contract c) -> (
486
         assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);
487
         fprintf fmt "\"spec\": %a,@ " pp_emf_spec c
488
       )
489
     | Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id
490 f4cba4b8 ploc
    );
491 66359a5e ploc
    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
492 f7caf067 ploc
    fprintf fmt "@]@ }"
493
  with Unhandled msg -> (
494
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
495
      m.mname.node_id;
496
    eprintf "%s@ " msg;
497
    eprintf "node skipped - no output generated@ @]@."
498
  )
499 3ca27bc7 ploc
500 42f91c0b ploc
(*let pp_machine fmt m =                      
501 f4cba4b8 ploc
  match m.mspec with
502
  | None | Some (NodeSpec _) -> pp_machine fmt m
503 42f91c0b ploc
  | Some (Contract _) -> pp_emf_contract fmt m
504
 *)
505
                      
506 59020713 ploc
let pp_emf_imported_node fmt top =
507
  let ind = Corelang.imported_node_of_top top in
508 f4cba4b8 ploc
  try
509 59020713 ploc
    fprintf fmt "@[<v 2>\"%a\": {@ "
510
      print_protect (fun fmt -> pp_print_string fmt ind.nodei_id);
511
    fprintf fmt "\"imported\": \"true\",@ ";
512
    fprintf fmt "\"inputs\": [%a],@ "
513
      pp_emf_vars_decl ind.nodei_inputs;
514
    fprintf fmt "\"outputs\": [%a],@ "
515
      pp_emf_vars_decl ind.nodei_outputs;
516 3b007718 ploc
    fprintf fmt "\"original_name\": \"%s\"" ind.nodei_id;
517
    (match ind.nodei_spec with None -> fprintf fmt "@ "
518 f4cba4b8 ploc
                             | Some (Contract _) -> assert false (* should have been processed *)
519 3b007718 ploc
                             | Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id
520 f4cba4b8 ploc
    );
521 59020713 ploc
    fprintf fmt "@]@ }"
522
  with Unhandled msg -> (
523
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
524
      ind.nodei_id;
525
    eprintf "%s@ " msg;
526
    eprintf "node skipped - no output generated@ @]@."
527
  )
528 3ca27bc7 ploc
(****************************************************)
529
(* Main function: iterates over node and print them *)
530
(****************************************************)
531
let pp_meta fmt basename =
532
  fprintf fmt "\"meta\": @[<v 0>{@ ";
533
  Utils.fprintf_list ~sep:",@ "
534
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
535
    fmt
536
    ["compiler-name", (Filename.basename Sys.executable_name);
537
     "compiler-version", Version.number;
538
     "command", (String.concat " " (Array.to_list Sys.argv));
539
     "source_file", basename
540
    ]
541
  ;
542
  fprintf fmt "@ @]},@ "
543 f7caf067 ploc
    
544 3ca27bc7 ploc
let translate fmt basename prog machines =
545 59020713 ploc
  (* record_types prog; *)
546 a6df3992 Ploc
  fprintf fmt "@[<v 0>{@ ";
547 3ca27bc7 ploc
  pp_meta fmt basename;
548 59020713 ploc
  (* Typedef *)
549
  fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ "
550
    (pp_emf_list pp_emf_typedef) (Corelang.get_typedefs prog);
551
  fprintf fmt "\"consts\": [@[<v 0>%a@]],@ "
552
    (pp_emf_list pp_emf_top_const) (Corelang.get_consts prog);
553
  fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";
554
  pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog);
555
  fprintf fmt "}@],@ ";
556 3ca27bc7 ploc
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
557 145379a9 ploc
  (* Previous alternative: mapping normalized lustre to EMF: 
558
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
559 a4c3d888 ploc
  pp_emf_list pp_machine fmt machines;
560 12c62417 ploc
  fprintf fmt "}@]@ }";
561 568b5a26 ploc
  fprintf fmt "@]@ }"
562 3ca27bc7 ploc
563
(* Local Variables: *)
564
(* compile-command: "make -C ../.." *)
565
(* End: *)