Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / EMF / EMF_backend.ml @ 953879f0

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