Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / EMF / EMF_backend.ml @ 66359a5e

History | View | Annotate | Download (15.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 available in old
14
   commits (eg in dd71e482a9d0).
15

    
16
   
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

    
26
   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

    
30
   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

    
48
   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

    
52
   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

    
99
*)
100

    
101
open LustreSpec
102
open Machine_code
103
open Format 
104
open EMF_common
105
exception Unhandled of string
106

    
107
module ISet = Utils.ISet
108
let fprintf_list = Utils.fprintf_list
109
  
110

    
111

    
112
(**********************************************)
113
(*   Utility functions: arrow and lustre expr *)
114
(**********************************************)
115

    
116
(* detect whether the instruction i represents an ARROW, ie an arrow with true
117
   -> false *)
118
let is_arrow_fun m i =
119
  match Corelang.get_instr_desc i with
120
  | MStep ([var], i, vl) ->
121
     (
122
       try
123
	 let name = (Machine_code.get_node_def i m).node_id in
124
	 match name, vl with
125
	 | "_arrow", [v1; v2] -> (
126
	   match v1.value_desc, v2.value_desc with
127
	   | Cst c1, Cst c2 ->
128
	      if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then
129
		true
130
	      else
131
		assert false (* only handle true -> false *)
132
	   | _ -> assert false
133
	 )
134
	    
135
	 | _ -> false
136
       with
137
       | Not_found -> false (* Not declared (should have been detected now, or
138
			       imported node) *)
139
     )
140
  | _ -> false
141
     
142
     
143
     
144
let is_resetable_fun lustre_eq =
145
  (* We extract the clock if it exist from the original lustre equation *)
146
  match lustre_eq with
147
  | Some eq -> (
148
    match eq.eq_rhs.expr_desc with
149
    | Expr_appl(_,_,reset) -> (
150
      match reset with None -> false | Some _ -> true
151
    )
152
    | _ ->  assert false
153
  )
154
  | None -> assert false (* should have been assigned to an original lustre equation *)
155

    
156
(**********************************************)
157
(*   Printing machine code as EMF             *)
158
(**********************************************)
159

    
160
     
161

    
162
let branch_cpt = ref 0
163
let get_instr_id fmt i =
164
  match Corelang.get_instr_desc i with
165
  | MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
166
  | MReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
167
  | MBranch (g, _) -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
168
  | MStep (outs, id, _) ->
169
     print_protect fmt 
170
       (fun fmt -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)
171
  | _ -> () (* No name *)
172

    
173
let rec branch_block_vars m il =
174
  List.fold_left
175
    (fun (accu_all_def, accu_def, accu_read) i ->
176
      let all_defined_vars, common_def_vars, read_vars = branch_instr_vars m i in
177
      ISet.union accu_all_def all_defined_vars,
178
      ISet.union accu_def common_def_vars,
179
      VSet.union accu_read read_vars)
180
    (ISet.empty, ISet.empty, VSet.empty) il
181
and branch_instr_vars m i =
182
  match Corelang.get_instr_desc i with
183
  | MLocalAssign (var,expr) 
184
  | MStateAssign (var,expr) -> ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
185
  | MStep (vars, f, args)  ->
186
     let is_stateful = List.mem_assoc f m.minstances in 
187
     let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in
188
     let args_vars =
189
       List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args in
190
     
191
     lhs, lhs,
192
     (
193
       if is_stateful && is_resetable_fun i.lustre_eq then
194
	 let reset_var =
195
	   let loc = Location.dummy_loc in
196
	   Corelang.mkvar_decl loc
197
	     (reset_name f,
198
	      Corelang.mktyp loc Tydec_bool, Corelang.mkclock loc Ckdec_any,
199
	      false,
200
	      None,
201
	      None) 
202
	 in
203
	 VSet.add reset_var args_vars
204
       else
205
	 args_vars
206
     )
207
  | MBranch (g,(_,hd_il)::tl)     -> (* We focus on variables defined in all branches *)
208
     let read_guard = get_expr_vars g in
209
     let all_def_vars_hd, def_vars_hd, read_vars_hd = branch_block_vars m hd_il in
210
     let all_def_vars, def_vars, read_vars =
211
       List.fold_left
212
	 (fun (all_def_vars, def_vars, read_vars) (_, il) ->
213
	   (* We accumulate reads but intersect writes *)
214
	   let all_writes_il, writes_il, reads_il = branch_block_vars m il in
215
	   ISet.union all_def_vars all_writes_il,
216
	   ISet.inter def_vars writes_il,
217
	   VSet.union read_vars reads_il
218
	 )
219
	 (all_def_vars_hd, def_vars_hd, read_vars_hd)
220
	 tl
221
     in
222
     all_def_vars, def_vars, VSet.union read_guard read_vars
223
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
224
  | MReset ni           
225
  | MNoReset ni ->
226
     let write = ISet.singleton (reset_name ni) in
227
     write, write, VSet.empty
228
  | MComment _ -> assert false (* not  available for EMF output *)
229
     
230
(* A kind of super join_guards: all MBranch are postponed and sorted by
231
   guards so they can be easier merged *)
232
let merge_branches instrs =
233
  let instrs, branches =
234
    List.fold_right (fun i (il, branches) ->
235
      match Corelang.get_instr_desc i with
236
	MBranch _ -> il, i::branches
237
      | _ -> i::il, branches
238
    ) instrs ([],[])
239
  in
240
  let sorting_branches b1 b2 =
241
    match Corelang.get_instr_desc b1, Corelang.get_instr_desc b2 with
242
    | MBranch(g1, hl1), MBranch(g2, hl) ->
243
       compare g1 g2
244
    | _ -> assert false
245
  in
246
  let sorted_branches = List.sort sorting_branches branches in
247
  instrs @ (join_guards_list sorted_branches)
248
    
249
let rec pp_emf_instr m fmt i =
250
  let pp_content fmt i =
251
    match Corelang.get_instr_desc i with
252
    | MLocalAssign(lhs, expr)
253
      -> (
254
	(match expr.value_desc with
255
	| Fun (fun_id, vl) -> (
256
	  (* Thanks to normalization, vl shall only contain constant or
257
	     local/state vars but not calls to other functions *)
258
	  fprintf fmt "\"kind\": \"operator\",@ ";
259
	  fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;
260
	  fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
261
	    fun_id
262
	    pp_emf_cst_or_var_list vl
263
	)	 
264
	| Array _ | Access _ | Power _ -> assert false (* No array expression allowed yet *)
265
	| Cst _ 
266
	| LocalVar _
267
	| StateVar _ -> (
268
	  fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
269
	    pp_var_name lhs
270
	    pp_emf_cst_or_var expr
271
	))    )
272

    
273
    | MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a
274
				 variable or a constant, no function anymore! *)
275
      -> (
276
	fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
277
	  pp_var_name lhs
278
	  pp_emf_cst_or_var expr
279
      )
280
       
281
    | MReset id           
282
      -> (
283
	fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
284
	  (reset_name id)
285
      )
286
    | MNoReset id           
287
      -> (
288
	fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
289
	  (reset_name id)
290
      )
291
       
292
    | MBranch (g, hl) -> (
293
      let all_outputs, outputs, inputs = branch_instr_vars m i in
294
      (* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)
295
      (* 	Machine_code.pp_instr i *)
296
      (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *)
297
      (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs) *)
298
      (* 	pp_emf_vars_decl *)
299
      (* 	(VSet.elements inputs) *)
300

    
301
      (* ; *)
302
      let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in
303
      (* Format.eprintf "Filtering in: %a@.@." *)
304
      (* 	pp_emf_vars_decl *)
305
      (* 	(VSet.elements inputs) *)
306

    
307
      (* ; *)
308
      fprintf fmt "\"kind\": \"branch\",@ ";
309
      fprintf fmt "\"guard\": %a,@ " pp_emf_cst_or_var g; (* it has to be a variable or a constant *)
310
      fprintf fmt "\"outputs\": [%a],@ " (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs);
311
      fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
312
	(* (let guard_inputs = get_expr_vars g in
313
	   VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to
314
	   remove guard's variable from inputs *)
315
	(VSet.elements inputs)
316
      ;
317
      fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }"
318
	(fprintf_list ~sep:",@ "
319
	   (fun fmt (tag, instrs_tag) ->
320
	     let branch_all_lhs, _, branch_inputs = branch_block_vars m instrs_tag in
321
	     let branch_inputs = VSet.filter (fun v -> not (ISet.mem v.var_id branch_all_lhs)) branch_inputs in
322
	     fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt -> Format.pp_print_string fmt tag);
323
	     fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag; 
324
	     fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl (VSet.elements branch_inputs); 
325
	     fprintf fmt "@[<v 2>\"instrs\": {@ ";
326
	     (pp_emf_instrs m) fmt instrs_tag;
327
	     fprintf fmt "@]@ }";
328
	     fprintf fmt "@]@ }"
329
	   )
330
	)
331
	hl
332
    )
333

    
334
    | MStep ([var], f, _) when is_arrow_fun m i -> (* Arrow case *) (
335
      fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\""
336
	f
337
	pp_var_name var
338
	(reset_name f)
339
    )
340

    
341
    | MStep (outputs, f, inputs) when not (is_imported_node f m) -> (
342
      let node_f = Machine_code.get_node_def f m in
343
      let is_stateful = List.mem_assoc f m.minstances in 
344
      fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ "
345
	(if is_stateful then "statefulcall" else "statelesscall")
346
	print_protect (fun fmt -> pp_print_string fmt (node_f.node_id)) 
347
	f;
348
      fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
349
	(fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" pp_var_name v)) outputs
350
	pp_emf_cst_or_var_list inputs;
351
      if is_stateful then
352
	fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}"
353
	  (reset_name f)
354
	  (is_resetable_fun i.lustre_eq)	  
355
      else fprintf fmt "@ "
356
    )
357

    
358
    | MStep(outputs, f, inputs ) -> (* This is an imported node *)
359
       EMF_library_calls.pp_call fmt m f outputs inputs
360
	 
361
    | MComment _ 
362
      -> Format.eprintf "unhandled comment in EMF@.@?"; assert false
363
  (* not  available for EMF output *)
364
  in
365
    fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
366
    fprintf fmt "%a" pp_content i;
367
    fprintf fmt "@]@]@ }"
368
and pp_emf_instrs m fmt instrs = fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
369

    
370
let pp_emf_annot cpt fmt (key, ee) =
371
  let _ =
372
    fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }"
373
      !cpt
374
      (fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s)) key
375
      pp_emf_eexpr ee
376
  in
377
  incr cpt
378
  
379
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
380
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
381
let pp_machine fmt m =
382
  let instrs = (*merge_branches*) m.mstep.step_instrs in
383
  try
384
    fprintf fmt "@[<v 2>\"%a\": {@ "
385
       print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
386
    fprintf fmt "\"kind\": %t,@ "
387
      (fun fmt -> if not ( snd (get_stateless_status m) )
388
	then fprintf fmt "\"stateful\""
389
	else fprintf fmt "\"stateless\"");
390
    fprintf fmt "\"inputs\": [%a],@ "
391
      pp_emf_vars_decl m.mstep.step_inputs;
392
    fprintf fmt "\"outputs\": [%a],@ "
393
      pp_emf_vars_decl m.mstep.step_outputs;
394
    fprintf fmt "\"locals\": [%a],@ "
395
      pp_emf_vars_decl m.mstep.step_locals;
396
    fprintf fmt "\"mems\": [%a],@ "
397
      pp_emf_vars_decl m.mmemory;
398
    
399
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
400
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
401
      (pp_emf_instrs m) instrs;
402
    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
403
    fprintf fmt "@]@ }"
404
  with Unhandled msg -> (
405
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
406
      m.mname.node_id;
407
    eprintf "%s@ " msg;
408
    eprintf "node skipped - no output generated@ @]@."
409
  )
410

    
411
(****************************************************)
412
(* Main function: iterates over node and print them *)
413
(****************************************************)
414
let pp_meta fmt basename =
415
  fprintf fmt "\"meta\": @[<v 0>{@ ";
416
  Utils.fprintf_list ~sep:",@ "
417
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
418
    fmt
419
    ["compiler-name", (Filename.basename Sys.executable_name);
420
     "compiler-version", Version.number;
421
     "command", (String.concat " " (Array.to_list Sys.argv));
422
     "source_file", basename
423
    ]
424
  ;
425
  fprintf fmt "@ @]},@ "
426
    
427
let translate fmt basename prog machines =
428
   (* record_types prog; *)
429
  fprintf fmt "@[<v 0>{@ ";
430
  pp_meta fmt basename;
431
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
432
  (* Previous alternative: mapping normalized lustre to EMF: 
433
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
434
  fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
435
  fprintf fmt "}@]@ }";
436
  fprintf fmt "@]@ }"
437

    
438
(* Local Variables: *)
439
(* compile-command: "make -C ../.." *)
440
(* End: *)