Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (14.6 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
	 in
202
	 VSet.add reset_var args_vars
203
       else
204
	 args_vars
205
     )
206
  | MBranch (g,(_,hd_il)::tl)     -> (* We focus on variables defined in all branches *)
207
     let read_guard = get_expr_vars g in
208
     let all_def_vars_hd, def_vars_hd, read_vars_hd = branch_block_vars m hd_il in
209
     let all_def_vars, def_vars, read_vars =
210
       List.fold_left
211
	 (fun (all_def_vars, def_vars, read_vars) (_, il) ->
212
	   (* We accumulate reads but intersect writes *)
213
	   let all_writes_il, writes_il, reads_il = branch_block_vars m il in
214
	   ISet.union all_def_vars all_writes_il,
215
	   ISet.inter def_vars writes_il,
216
	   VSet.union read_vars reads_il
217
	 )
218
	 (all_def_vars_hd, def_vars_hd, read_vars_hd)
219
	 tl
220
     in
221
     all_def_vars, def_vars, VSet.union read_guard read_vars
222
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
223
  | MReset ni           
224
  | MNoReset ni ->
225
     let write = ISet.singleton (reset_name ni) in
226
     write, write, VSet.empty
227
  | MComment _ -> assert false (* not  available for EMF output *)
228
     
229
(* 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
let rec pp_emf_instr m fmt i =
249
  let pp_content fmt i =
250
    match Corelang.get_instr_desc i with
251
    | MLocalAssign(lhs, expr)
252
      -> (
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
	  pp_var_name lhs
277
	  pp_emf_cst_or_var expr
278
      )
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
      let all_outputs, outputs, inputs = branch_instr_vars m i in
293
      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

    
300
      ;
301
      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

    
306
      ;
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
	     let branch_all_lhs, _, branch_inputs = branch_block_vars m instrs_tag in
320
	     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

    
333
    | 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
	  (is_resetable_fun i.lustre_eq)	  
354
      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
  (* not  available for EMF output *)
363
  in
364
    fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
365
    fprintf fmt "%a" pp_content i;
366
    fprintf fmt "@]@]@ }"
367
and pp_emf_instrs m fmt instrs = fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
368
       
369
let pp_machine fmt m =
370
  let instrs = (*merge_branches*) m.mstep.step_instrs in
371
  try
372
    fprintf fmt "@[<v 2>\"%a\": {@ "
373
       print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
374
    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
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
383
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ }"
384
      (pp_emf_instrs m) instrs;
385
    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

    
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
    
409
let translate fmt basename prog machines =
410
   (* record_types prog; *)
411
  fprintf fmt "@[<v 0>{@ ";
412
  pp_meta fmt basename;
413
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
414
  (* Previous alternative: mapping normalized lustre to EMF: 
415
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
416
  fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
417
  fprintf fmt "}@]@ }";
418
  fprintf fmt "@]@ }"
419

    
420
(* Local Variables: *)
421
(* compile-command: "make -C ../.." *)
422
(* End: *)