Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / EMF / EMF_backend.ml @ 1b721bfd

History | View | Annotate | Download (12.8 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
  | MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> Printers.pp_var_name fmt lhs
150
  | MReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
151
  | MBranch (g, _) -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
152 2475c9e8 ploc
  | MStep (outs, id, _) -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" Printers.pp_var_name) outs id
153 9f0f88dd ploc
  | _ -> () (* No name *)
154
155 dd71e482 ploc
let rec branch_block_vars il =
156 27d18db9 ploc
  List.fold_left
157 1b721bfd ploc
    (fun (accu_all_def, accu_def, accu_read) i ->
158
      let all_defined_vars, common_def_vars, read_vars = branch_instr_vars i in
159
      ISet.union accu_all_def all_defined_vars,
160
      ISet.union accu_def common_def_vars,
161
      VSet.union accu_read read_vars)
162
    (ISet.empty, ISet.empty, VSet.empty) il
163 dd71e482 ploc
and branch_instr_vars i =
164 27d18db9 ploc
  match Corelang.get_instr_desc i with
165 dd71e482 ploc
  | MLocalAssign (var,expr) 
166 1b721bfd ploc
  | MStateAssign (var,expr) -> ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
167 dd71e482 ploc
  | MStep (vars, _, args)  ->
168 1b721bfd ploc
     let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in
169
     lhs, lhs,
170
     List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args
171 dd71e482 ploc
  | MBranch (g,(_,hd_il)::tl)     -> (* We focus on variables defined in all branches *)
172
     let read_guard = get_expr_vars g in
173 1b721bfd ploc
     let all_def_vars_hd, def_vars_hd, read_vars_hd = branch_block_vars hd_il in
174
     let all_def_vars, def_vars, read_vars =
175 dd71e482 ploc
       List.fold_left
176 1b721bfd ploc
	 (fun (all_def_vars, def_vars, read_vars) (_, il) ->
177 dd71e482 ploc
	 (* We accumulate reads but intersect writes *)
178 1b721bfd ploc
	   let all_writes_il, writes_il, reads_il = branch_block_vars il in
179
	   ISet.union all_def_vars all_writes_il,
180 dd71e482 ploc
	   ISet.inter def_vars writes_il,
181 1b721bfd ploc
	   VSet.union read_vars reads_il
182 dd71e482 ploc
	 )
183 1b721bfd ploc
	 (all_def_vars_hd, def_vars_hd, read_vars_hd)
184 dd71e482 ploc
	 tl
185
     in
186 1b721bfd ploc
     all_def_vars, def_vars, VSet.union read_guard read_vars
187 27d18db9 ploc
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
188
  | MReset ni           
189 1b721bfd ploc
  | MNoReset ni ->
190
     let write = ISet.singleton (reset_name ni) in
191
     write, write, VSet.empty
192 27d18db9 ploc
  | MComment _ -> assert false (* not  available for EMF output *)
193
     
194
  
195 2475c9e8 ploc
      
196
let rec pp_emf_instr m fmt i =
197 9f0f88dd ploc
  let pp_content fmt i =
198
    match Corelang.get_instr_desc i with
199
    | MLocalAssign(lhs, expr)
200
    -> (
201
      (match expr.value_desc with
202
      | Fun (fun_id, vl) -> (
203
	(* Thanks to normalization, vl shall only contain constant or
204
	   local/state vars but not calls to other functions *)
205
	fprintf fmt "\"kind\": \"operator\",@ ";
206
	fprintf fmt "\"lhs\": \"%a\",@ " Printers.pp_var_name lhs;
207 ab1c9ed2 Bourbouh
	fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
208 9f0f88dd ploc
	  fun_id
209
	  pp_emf_cst_or_var_list vl
210
      )	 
211
      | Array _ | Access _ | Power _ -> assert false (* No array expression allowed yet *)
212
      | Cst _ 
213
      | LocalVar _
214
      | StateVar _ -> (
215
	fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
216
	  Printers.pp_var_name lhs
217
	  pp_emf_cst_or_var expr
218
      ))    )
219
220
  | MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a
221
			       variable or a constant, no function anymore! *)
222
    -> (
223
      fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
224
	Printers.pp_var_name lhs
225
	pp_emf_cst_or_var expr
226
    )
227
     
228
  | MReset id           
229
    -> (
230
      fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
231
	(reset_name id)
232
    )
233
  | MNoReset id           
234
    -> (
235
      fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
236
	(reset_name id)
237
    )
238 1bff14ac ploc
    
239 9f0f88dd ploc
  | MBranch (g, hl) -> (
240 1b721bfd ploc
    let all_outputs, outputs, inputs = branch_instr_vars i in
241
    Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@."
242
      Machine_code.pp_instr i
243
      (fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs)
244
      (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs)
245
      pp_emf_vars_decl
246
      (VSet.elements inputs)
247
248
    ;
249
    let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in
250
    Format.eprintf "Filtering in: %a@.@."
251
      pp_emf_vars_decl
252
      (VSet.elements inputs)
253
254
      ;
255 9f0f88dd ploc
    fprintf fmt "\"kind\": \"branch\",@ ";
256
    fprintf fmt "\"guard\": %a,@ " pp_emf_cst_or_var g; (* it has to be a variable or a constant *)
257 dd71e482 ploc
    fprintf fmt "\"outputs\": [%a],@ " (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs);
258
    fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
259
      (* (let guard_inputs = get_expr_vars g in
260
	  VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to
261 2475c9e8 ploc
	 remove guard's variable from inputs *)
262 dd71e482 ploc
      (VSet.elements inputs)
263
    ;
264
    fprintf fmt "@[<v 2>\"branches\": {@ %a@]}@ "
265 9f0f88dd ploc
      (fprintf_list ~sep:",@ "
266
	 (fun fmt (tag, instrs_tag) ->
267 1b721bfd ploc
	   let branch_all_lhs, _, branch_inputs = branch_block_vars instrs_tag in
268
	   let branch_inputs = VSet.filter (fun v -> not (ISet.mem v.var_id branch_all_lhs)) branch_inputs in
269 dd71e482 ploc
	   fprintf fmt "@[<v 2>\"%s\": {@ " tag;
270 2823bc51 ploc
	   fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag; 
271 dd71e482 ploc
	   fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl (VSet.elements branch_inputs); 
272
	   fprintf fmt "@[<v 2>\"instrs\": {@ ";
273 2475c9e8 ploc
	   fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs_tag;
274 dd71e482 ploc
	   fprintf fmt "@]}@ ";
275
	   fprintf fmt "@]}"
276 9f0f88dd ploc
277
	 )
278
      )
279
      hl
280 dd71e482 ploc
   )
281 9f0f88dd ploc
282
  | MStep ([var], f, _) when is_arrow_fun m i -> (* Arrow case *) (
283
    fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\""
284
      f
285
      Printers.pp_var_name var
286
      (reset_name f)
287
  )
288
289 2475c9e8 ploc
  | MStep (outputs, f, inputs) when not (is_imported_node f m) -> (
290 9f0f88dd ploc
    let node_f = Machine_code.get_node_def f m in
291
    let is_stateful = List.mem_assoc f m.minstances in 
292
    fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%s\",@ \"id\": \"%s\",@ "
293
      (if is_stateful then "statefulcall" else "statelesscall")
294
      (node_f.node_id) 
295
      f;
296 dd71e482 ploc
    fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
297 9f0f88dd ploc
      (fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" Printers.pp_var_name v)) outputs
298
      pp_emf_cst_or_var_list inputs;
299 dd71e482 ploc
    if is_stateful then fprintf fmt ",@ \"reset\": \"%s\"" (reset_name f) else fprintf fmt "@ "
300 9f0f88dd ploc
  )
301
302 2475c9e8 ploc
  | MStep(outputs, f, inputs ) -> (* This is an imported node *)
303
        EMF_library_calls.pp_call fmt m f outputs inputs
304
	  
305 9f0f88dd ploc
  | MComment _ 
306
    -> Format.eprintf "unhandled comment in EMF@.@?"; assert false
307
  (* not  available for EMF output *)
308
309
  in
310 dd71e482 ploc
  fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
311
  fprintf fmt "%a@ " pp_content i;
312 9f0f88dd ploc
  fprintf fmt "}@]"
313
314
       
315 f7caf067 ploc
let pp_machine fmt m =
316
  try
317 9f0f88dd ploc
    fprintf fmt "@[<v 2>\"%s\": {@ "
318
      m.mname.node_id;
319
    fprintf fmt "\"kind\": %t,@ \"inputs\": [%a],@ \"outputs\": [%a],@ \"locals\": [%a],@ "
320
      (fun fmt -> if not ( snd (get_stateless_status m) )
321
	then fprintf fmt "\"stateful\""
322
	else fprintf fmt "\"stateless\"")
323
      pp_emf_vars_decl m.mstep.step_inputs
324
      pp_emf_vars_decl m.mstep.step_outputs
325
      pp_emf_vars_decl m.mstep.step_locals
326
    ;
327 ab1c9ed2 Bourbouh
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ }"
328 2475c9e8 ploc
      (fprintf_list ~sep:",@ " (pp_emf_instr m)) m.mstep.step_instrs;
329 f7caf067 ploc
    fprintf fmt "@]@ }"
330
  with Unhandled msg -> (
331
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
332
      m.mname.node_id;
333
    eprintf "%s@ " msg;
334
    eprintf "node skipped - no output generated@ @]@."
335
  )
336 3ca27bc7 ploc
337
(****************************************************)
338
(* Main function: iterates over node and print them *)
339
(****************************************************)
340
let pp_meta fmt basename =
341
  fprintf fmt "\"meta\": @[<v 0>{@ ";
342
  Utils.fprintf_list ~sep:",@ "
343
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
344
    fmt
345
    ["compiler-name", (Filename.basename Sys.executable_name);
346
     "compiler-version", Version.number;
347
     "command", (String.concat " " (Array.to_list Sys.argv));
348
     "source_file", basename
349
    ]
350
  ;
351
  fprintf fmt "@ @]},@ "
352 f7caf067 ploc
    
353 3ca27bc7 ploc
let translate fmt basename prog machines =
354 c82ea2ca ploc
  (* record_types prog; *)
355 a6df3992 Ploc
  fprintf fmt "@[<v 0>{@ ";
356 3ca27bc7 ploc
  pp_meta fmt basename;
357
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
358 145379a9 ploc
  (* Previous alternative: mapping normalized lustre to EMF: 
359
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
360 ab1c9ed2 Bourbouh
  fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
361 3ca27bc7 ploc
  fprintf fmt "@ @]}";
362 a6df3992 Ploc
  fprintf fmt "@ @]}"
363 3ca27bc7 ploc
364
(* Local Variables: *)
365
(* compile-command: "make -C ../.." *)
366
(* End: *)