Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / EMF / EMF_backend.ml @ 7c79dd93

History | View | Annotate | Download (14.6 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 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 2475c9e8 ploc
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 3ca27bc7 ploc
112
(**********************************************)
113 9f0f88dd ploc
(*   Utility functions: arrow and lustre expr *)
114 3ca27bc7 ploc
(**********************************************)
115 a6df3992 Ploc
116 524060b3 ploc
(* 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 7eafa0e1 ploc
  | 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 524060b3 ploc
  | _ -> false
141 7eafa0e1 ploc
     
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 524060b3 ploc
156 9f0f88dd ploc
(**********************************************)
157
(*   Printing machine code as EMF             *)
158
(**********************************************)
159 524060b3 ploc
160 9f0f88dd ploc
     
161 dd71e482 ploc
162 9f0f88dd ploc
let branch_cpt = ref 0
163
let get_instr_id fmt i =
164
  match Corelang.get_instr_desc i with
165 785b64f9 ploc
  | MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
166 9f0f88dd ploc
  | MReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
167
  | MBranch (g, _) -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
168 785b64f9 ploc
  | MStep (outs, id, _) ->
169
     print_protect fmt 
170
       (fun fmt -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)
171 9f0f88dd ploc
  | _ -> () (* No name *)
172
173 7eafa0e1 ploc
let rec branch_block_vars m il =
174 27d18db9 ploc
  List.fold_left
175 1b721bfd ploc
    (fun (accu_all_def, accu_def, accu_read) i ->
176 7eafa0e1 ploc
      let all_defined_vars, common_def_vars, read_vars = branch_instr_vars m i in
177 1b721bfd ploc
      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 7eafa0e1 ploc
and branch_instr_vars m i =
182 27d18db9 ploc
  match Corelang.get_instr_desc i with
183 dd71e482 ploc
  | MLocalAssign (var,expr) 
184 1b721bfd ploc
  | MStateAssign (var,expr) -> ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
185 7eafa0e1 ploc
  | MStep (vars, f, args)  ->
186
     let is_stateful = List.mem_assoc f m.minstances in 
187 1b721bfd ploc
     let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in
188 7eafa0e1 ploc
     let args_vars =
189
       List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args in
190
     
191 1b721bfd ploc
     lhs, lhs,
192 7eafa0e1 ploc
     (
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
	 in
202
	 VSet.add reset_var args_vars
203
       else
204
	 args_vars
205
     )
206 dd71e482 ploc
  | MBranch (g,(_,hd_il)::tl)     -> (* We focus on variables defined in all branches *)
207
     let read_guard = get_expr_vars g in
208 7eafa0e1 ploc
     let all_def_vars_hd, def_vars_hd, read_vars_hd = branch_block_vars m hd_il in
209 1b721bfd ploc
     let all_def_vars, def_vars, read_vars =
210 dd71e482 ploc
       List.fold_left
211 1b721bfd ploc
	 (fun (all_def_vars, def_vars, read_vars) (_, il) ->
212 7eafa0e1 ploc
	   (* We accumulate reads but intersect writes *)
213
	   let all_writes_il, writes_il, reads_il = branch_block_vars m il in
214 1b721bfd ploc
	   ISet.union all_def_vars all_writes_il,
215 dd71e482 ploc
	   ISet.inter def_vars writes_il,
216 1b721bfd ploc
	   VSet.union read_vars reads_il
217 dd71e482 ploc
	 )
218 1b721bfd ploc
	 (all_def_vars_hd, def_vars_hd, read_vars_hd)
219 dd71e482 ploc
	 tl
220
     in
221 1b721bfd ploc
     all_def_vars, def_vars, VSet.union read_guard read_vars
222 27d18db9 ploc
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
223
  | MReset ni           
224 1b721bfd ploc
  | MNoReset ni ->
225
     let write = ISet.singleton (reset_name ni) in
226
     write, write, VSet.empty
227 27d18db9 ploc
  | MComment _ -> assert false (* not  available for EMF output *)
228
     
229 01b501ca ploc
(* A kind of super join_guards: all MBranch are postponed and sorted by
230
   guards so they can be easier merged *)
231
let merge_branches instrs =
232
  let instrs, branches =
233
    List.fold_right (fun i (il, branches) ->
234
      match Corelang.get_instr_desc i with
235
	MBranch _ -> il, i::branches
236
      | _ -> i::il, branches
237
    ) instrs ([],[])
238
  in
239
  let sorting_branches b1 b2 =
240
    match Corelang.get_instr_desc b1, Corelang.get_instr_desc b2 with
241
    | MBranch(g1, hl1), MBranch(g2, hl) ->
242
       compare g1 g2
243
    | _ -> assert false
244
  in
245
  let sorted_branches = List.sort sorting_branches branches in
246
  instrs @ (join_guards_list sorted_branches)
247
    
248 2475c9e8 ploc
let rec pp_emf_instr m fmt i =
249 9f0f88dd ploc
  let pp_content fmt i =
250
    match Corelang.get_instr_desc i with
251
    | MLocalAssign(lhs, expr)
252 8f0e9f74 ploc
      -> (
253
	(match expr.value_desc with
254
	| Fun (fun_id, vl) -> (
255
	  (* Thanks to normalization, vl shall only contain constant or
256
	     local/state vars but not calls to other functions *)
257
	  fprintf fmt "\"kind\": \"operator\",@ ";
258
	  fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;
259
	  fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
260
	    fun_id
261
	    pp_emf_cst_or_var_list vl
262
	)	 
263
	| Array _ | Access _ | Power _ -> assert false (* No array expression allowed yet *)
264
	| Cst _ 
265
	| LocalVar _
266
	| StateVar _ -> (
267
	  fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
268
	    pp_var_name lhs
269
	    pp_emf_cst_or_var expr
270
	))    )
271
272
    | MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a
273
				 variable or a constant, no function anymore! *)
274
      -> (
275
	fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
276 69c8d06c ploc
	  pp_var_name lhs
277 9f0f88dd ploc
	  pp_emf_cst_or_var expr
278 8f0e9f74 ploc
      )
279
       
280
    | MReset id           
281
      -> (
282
	fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
283
	  (reset_name id)
284
      )
285
    | MNoReset id           
286
      -> (
287
	fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
288
	  (reset_name id)
289
      )
290
       
291
    | MBranch (g, hl) -> (
292 7eafa0e1 ploc
      let all_outputs, outputs, inputs = branch_instr_vars m i in
293 8f0e9f74 ploc
      Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@."
294
	Machine_code.pp_instr i
295
	(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs)
296
	(fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs)
297
	pp_emf_vars_decl
298
	(VSet.elements inputs)
299 1b721bfd ploc
300
      ;
301 8f0e9f74 ploc
      let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in
302
      Format.eprintf "Filtering in: %a@.@."
303
	pp_emf_vars_decl
304
	(VSet.elements inputs)
305 9f0f88dd ploc
306 8f0e9f74 ploc
      ;
307
      fprintf fmt "\"kind\": \"branch\",@ ";
308
      fprintf fmt "\"guard\": %a,@ " pp_emf_cst_or_var g; (* it has to be a variable or a constant *)
309
      fprintf fmt "\"outputs\": [%a],@ " (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs);
310
      fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
311
	(* (let guard_inputs = get_expr_vars g in
312
	   VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to
313
	   remove guard's variable from inputs *)
314
	(VSet.elements inputs)
315
      ;
316
      fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }"
317
	(fprintf_list ~sep:",@ "
318
	   (fun fmt (tag, instrs_tag) ->
319 7eafa0e1 ploc
	     let branch_all_lhs, _, branch_inputs = branch_block_vars m instrs_tag in
320 8f0e9f74 ploc
	     let branch_inputs = VSet.filter (fun v -> not (ISet.mem v.var_id branch_all_lhs)) branch_inputs in
321
	     fprintf fmt "@[<v 2>\"%s\": {@ " tag;
322
	     fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag; 
323
	     fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl (VSet.elements branch_inputs); 
324
	     fprintf fmt "@[<v 2>\"instrs\": {@ ";
325
	     (pp_emf_instrs m) fmt instrs_tag;
326
	     fprintf fmt "@]@ }";
327
	     fprintf fmt "@]@ }"
328
	   )
329
	)
330
	hl
331
    )
332 9f0f88dd ploc
333 8f0e9f74 ploc
    | MStep ([var], f, _) when is_arrow_fun m i -> (* Arrow case *) (
334
      fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\""
335
	f
336
	pp_var_name var
337
	(reset_name f)
338
    )
339
340
    | MStep (outputs, f, inputs) when not (is_imported_node f m) -> (
341
      let node_f = Machine_code.get_node_def f m in
342
      let is_stateful = List.mem_assoc f m.minstances in 
343
      fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ "
344
	(if is_stateful then "statefulcall" else "statelesscall")
345
	print_protect (fun fmt -> pp_print_string fmt (node_f.node_id)) 
346
	f;
347
      fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
348
	(fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" pp_var_name v)) outputs
349
	pp_emf_cst_or_var_list inputs;
350
      if is_stateful then
351
	fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}"
352
	  (reset_name f)
353 7eafa0e1 ploc
	  (is_resetable_fun i.lustre_eq)	  
354 8f0e9f74 ploc
      else fprintf fmt "@ "
355
    )
356
357
    | MStep(outputs, f, inputs ) -> (* This is an imported node *)
358
       EMF_library_calls.pp_call fmt m f outputs inputs
359
	 
360
    | MComment _ 
361
      -> Format.eprintf "unhandled comment in EMF@.@?"; assert false
362 9f0f88dd ploc
  (* not  available for EMF output *)
363
  in
364 def94a59 ploc
    fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
365 568b5a26 ploc
    fprintf fmt "%a" pp_content i;
366
    fprintf fmt "@]@]@ }"
367 01b501ca ploc
and pp_emf_instrs m fmt instrs = fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
368 9f0f88dd ploc
       
369 f7caf067 ploc
let pp_machine fmt m =
370 9f231bff ploc
  let instrs = (*merge_branches*) m.mstep.step_instrs in
371 f7caf067 ploc
  try
372 fbad3c4b ploc
    fprintf fmt "@[<v 2>\"%a\": {@ "
373
       print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
374 9f0f88dd ploc
    fprintf fmt "\"kind\": %t,@ \"inputs\": [%a],@ \"outputs\": [%a],@ \"locals\": [%a],@ "
375
      (fun fmt -> if not ( snd (get_stateless_status m) )
376
	then fprintf fmt "\"stateful\""
377
	else fprintf fmt "\"stateless\"")
378
      pp_emf_vars_decl m.mstep.step_inputs
379
      pp_emf_vars_decl m.mstep.step_outputs
380
      pp_emf_vars_decl m.mstep.step_locals
381
    ;
382 7c79dd93 ploc
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
383 ab1c9ed2 Bourbouh
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ }"
384 01b501ca ploc
      (pp_emf_instrs m) instrs;
385 f7caf067 ploc
    fprintf fmt "@]@ }"
386
  with Unhandled msg -> (
387
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
388
      m.mname.node_id;
389
    eprintf "%s@ " msg;
390
    eprintf "node skipped - no output generated@ @]@."
391
  )
392 3ca27bc7 ploc
393
(****************************************************)
394
(* Main function: iterates over node and print them *)
395
(****************************************************)
396
let pp_meta fmt basename =
397
  fprintf fmt "\"meta\": @[<v 0>{@ ";
398
  Utils.fprintf_list ~sep:",@ "
399
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
400
    fmt
401
    ["compiler-name", (Filename.basename Sys.executable_name);
402
     "compiler-version", Version.number;
403
     "command", (String.concat " " (Array.to_list Sys.argv));
404
     "source_file", basename
405
    ]
406
  ;
407
  fprintf fmt "@ @]},@ "
408 f7caf067 ploc
    
409 3ca27bc7 ploc
let translate fmt basename prog machines =
410 01b501ca ploc
   (* record_types prog; *)
411 a6df3992 Ploc
  fprintf fmt "@[<v 0>{@ ";
412 3ca27bc7 ploc
  pp_meta fmt basename;
413
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
414 145379a9 ploc
  (* Previous alternative: mapping normalized lustre to EMF: 
415
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
416 ab1c9ed2 Bourbouh
  fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
417 12c62417 ploc
  fprintf fmt "}@]@ }";
418 568b5a26 ploc
  fprintf fmt "@]@ }"
419 3ca27bc7 ploc
420
(* Local Variables: *)
421
(* compile-command: "make -C ../.." *)
422
(* End: *)