Project

General

Profile

Download (15.4 KB) Statistics
| Branch: | Tag: | Revision:
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 Lustre_types
102
open Machine_code_types
103
open Machine_code_common
104
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

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

    
117
(* 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
  | MStep ([var], i, vl) ->
122
     (
123
       try
124
	 let name = (get_node_def i m).node_id in
125
	 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
  | _ -> false
142
     
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
    | _ ->  assert false
154
  )
155
  | None -> assert false (* should have been assigned to an original lustre equation *)
156

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

    
161
     
162

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

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

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

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

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

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

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

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

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

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

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