Project

General

Profile

Download (15.4 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 2475c9e8 ploc
open Machine_code
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 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 7eafa0e1 ploc
  | MStep ([var], i, vl) ->
122
     (
123
       try
124
	 let name = (Machine_code.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 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
    | _ ->  assert false
154
  )
155
  | None -> assert false (* should have been assigned to an original lustre equation *)
156 524060b3 ploc
157 9f0f88dd ploc
(**********************************************)
158
(*   Printing machine code as EMF             *)
159
(**********************************************)
160 524060b3 ploc
161 9f0f88dd ploc
     
162 dd71e482 ploc
163 9f0f88dd ploc
let branch_cpt = ref 0
164
let get_instr_id fmt i =
165
  match Corelang.get_instr_desc i with
166 785b64f9 ploc
  | MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
167 9f0f88dd ploc
  | MReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
168
  | MBranch (g, _) -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
169 785b64f9 ploc
  | MStep (outs, id, _) ->
170
     print_protect fmt 
171
       (fun fmt -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)
172 9f0f88dd ploc
  | _ -> () (* No name *)
173
174 7eafa0e1 ploc
let rec branch_block_vars m il =
175 27d18db9 ploc
  List.fold_left
176 1b721bfd ploc
    (fun (accu_all_def, accu_def, accu_read) i ->
177 7eafa0e1 ploc
      let all_defined_vars, common_def_vars, read_vars = branch_instr_vars m i in
178 1b721bfd ploc
      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 7eafa0e1 ploc
and branch_instr_vars m i =
183 27d18db9 ploc
  match Corelang.get_instr_desc i with
184 dd71e482 ploc
  | MLocalAssign (var,expr) 
185 1b721bfd ploc
  | MStateAssign (var,expr) -> ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
186 7eafa0e1 ploc
  | MStep (vars, f, args)  ->
187
     let is_stateful = List.mem_assoc f m.minstances in 
188 1b721bfd ploc
     let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in
189 7eafa0e1 ploc
     let args_vars =
190
       List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args in
191
     
192 1b721bfd ploc
     lhs, lhs,
193 7eafa0e1 ploc
     (
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 66359a5e ploc
	      None,
202 7eafa0e1 ploc
	      None) 
203
	 in
204
	 VSet.add reset_var args_vars
205
       else
206
	 args_vars
207
     )
208 dd71e482 ploc
  | MBranch (g,(_,hd_il)::tl)     -> (* We focus on variables defined in all branches *)
209
     let read_guard = get_expr_vars g in
210 7eafa0e1 ploc
     let all_def_vars_hd, def_vars_hd, read_vars_hd = branch_block_vars m hd_il in
211 1b721bfd ploc
     let all_def_vars, def_vars, read_vars =
212 dd71e482 ploc
       List.fold_left
213 1b721bfd ploc
	 (fun (all_def_vars, def_vars, read_vars) (_, il) ->
214 7eafa0e1 ploc
	   (* We accumulate reads but intersect writes *)
215
	   let all_writes_il, writes_il, reads_il = branch_block_vars m il in
216 1b721bfd ploc
	   ISet.union all_def_vars all_writes_il,
217 dd71e482 ploc
	   ISet.inter def_vars writes_il,
218 1b721bfd ploc
	   VSet.union read_vars reads_il
219 dd71e482 ploc
	 )
220 1b721bfd ploc
	 (all_def_vars_hd, def_vars_hd, read_vars_hd)
221 dd71e482 ploc
	 tl
222
     in
223 1b721bfd ploc
     all_def_vars, def_vars, VSet.union read_guard read_vars
224 27d18db9 ploc
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
225
  | MReset ni           
226 1b721bfd ploc
  | MNoReset ni ->
227
     let write = ISet.singleton (reset_name ni) in
228
     write, write, VSet.empty
229 27d18db9 ploc
  | MComment _ -> assert false (* not  available for EMF output *)
230
     
231 01b501ca ploc
(* 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 2475c9e8 ploc
let rec pp_emf_instr m fmt i =
251 9f0f88dd ploc
  let pp_content fmt i =
252
    match Corelang.get_instr_desc i with
253
    | MLocalAssign(lhs, expr)
254 8f0e9f74 ploc
      -> (
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 69c8d06c ploc
	  pp_var_name lhs
279 9f0f88dd ploc
	  pp_emf_cst_or_var expr
280 8f0e9f74 ploc
      )
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 7eafa0e1 ploc
      let all_outputs, outputs, inputs = branch_instr_vars m i in
295 2196948d ploc
      (* 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 1b721bfd ploc
302 2196948d ploc
      (* ; *)
303 8f0e9f74 ploc
      let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in
304 2196948d ploc
      (* Format.eprintf "Filtering in: %a@.@." *)
305
      (* 	pp_emf_vars_decl *)
306
      (* 	(VSet.elements inputs) *)
307 9f0f88dd ploc
308 2196948d ploc
      (* ; *)
309 8f0e9f74 ploc
      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 7eafa0e1 ploc
	     let branch_all_lhs, _, branch_inputs = branch_block_vars m instrs_tag in
322 8f0e9f74 ploc
	     let branch_inputs = VSet.filter (fun v -> not (ISet.mem v.var_id branch_all_lhs)) branch_inputs in
323 2196948d ploc
	     fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt -> Format.pp_print_string fmt tag);
324 8f0e9f74 ploc
	     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 9f0f88dd ploc
335 8f0e9f74 ploc
    | 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 = Machine_code.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 7eafa0e1 ploc
	  (is_resetable_fun i.lustre_eq)	  
356 8f0e9f74 ploc
      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 9f0f88dd ploc
  (* not  available for EMF output *)
365
  in
366 def94a59 ploc
    fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
367 568b5a26 ploc
    fprintf fmt "%a" pp_content i;
368
    fprintf fmt "@]@]@ }"
369 01b501ca ploc
and pp_emf_instrs m fmt instrs = fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
370 66359a5e ploc
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 f7caf067 ploc
let pp_machine fmt m =
383 9f231bff ploc
  let instrs = (*merge_branches*) m.mstep.step_instrs in
384 f7caf067 ploc
  try
385 fbad3c4b ploc
    fprintf fmt "@[<v 2>\"%a\": {@ "
386
       print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
387 66359a5e ploc
    fprintf fmt "\"kind\": %t,@ "
388 9f0f88dd ploc
      (fun fmt -> if not ( snd (get_stateless_status m) )
389
	then fprintf fmt "\"stateful\""
390 66359a5e ploc
	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 7c79dd93 ploc
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
401 66359a5e ploc
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
402 01b501ca ploc
      (pp_emf_instrs m) instrs;
403 66359a5e ploc
    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
404 f7caf067 ploc
    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 3ca27bc7 ploc
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 f7caf067 ploc
    
428 3ca27bc7 ploc
let translate fmt basename prog machines =
429 01b501ca ploc
   (* record_types prog; *)
430 a6df3992 Ploc
  fprintf fmt "@[<v 0>{@ ";
431 3ca27bc7 ploc
  pp_meta fmt basename;
432
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
433 145379a9 ploc
  (* Previous alternative: mapping normalized lustre to EMF: 
434
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
435 ab1c9ed2 Bourbouh
  fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
436 12c62417 ploc
  fprintf fmt "}@]@ }";
437 568b5a26 ploc
  fprintf fmt "@]@ }"
438 3ca27bc7 ploc
439
(* Local Variables: *)
440
(* compile-command: "make -C ../.." *)
441
(* End: *)