Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / EMF / EMF_backend.ml @ fbad3c4b

History | View | Annotate | Download (13.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
    try
122
      let name = (Machine_code.get_node_def i m).node_id in
123
      match name, vl with
124
      | "_arrow", [v1; v2] -> (
125
	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
      )
133
	 
134
      | _ -> false
135
    with
136
    | Not_found -> false (* Not declared (should have been detected now, or imported node *)
137
  )
138
  | _ -> false
139

    
140
(**********************************************)
141
(*   Printing machine code as EMF             *)
142
(**********************************************)
143

    
144
     
145

    
146
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, _) -> 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
  | MStep (outs, id, _) ->
153
     print_protect fmt 
154
       (fun fmt -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)
155
  | _ -> () (* No name *)
156

    
157
let rec branch_block_vars il =
158
  List.fold_left
159
    (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
and branch_instr_vars i =
166
  match Corelang.get_instr_desc i with
167
  | MLocalAssign (var,expr) 
168
  | MStateAssign (var,expr) -> ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
169
  | MStep (vars, _, args)  ->
170
     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
  | MBranch (g,(_,hd_il)::tl)     -> (* We focus on variables defined in all branches *)
174
     let read_guard = get_expr_vars g in
175
     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
       List.fold_left
178
	 (fun (all_def_vars, def_vars, read_vars) (_, il) ->
179
	 (* We accumulate reads but intersect writes *)
180
	   let all_writes_il, writes_il, reads_il = branch_block_vars il in
181
	   ISet.union all_def_vars all_writes_il,
182
	   ISet.inter def_vars writes_il,
183
	   VSet.union read_vars reads_il
184
	 )
185
	 (all_def_vars_hd, def_vars_hd, read_vars_hd)
186
	 tl
187
     in
188
     all_def_vars, def_vars, VSet.union read_guard read_vars
189
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
190
  | MReset ni           
191
  | MNoReset ni ->
192
     let write = ISet.singleton (reset_name ni) in
193
     write, write, VSet.empty
194
  | MComment _ -> assert false (* not  available for EMF output *)
195
     
196
(* 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
let rec pp_emf_instr m fmt i =
216
  let pp_content fmt i =
217
    match Corelang.get_instr_desc i with
218
    | MLocalAssign(lhs, expr)
219
    -> (
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
	pp_var_name lhs
244
	pp_emf_cst_or_var expr
245
    )
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

    
267
    ;
268
    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

    
273
      ;
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\": {@ %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
      )
298
      hl
299
   )
300

    
301
  | MStep ([var], f, _) when is_arrow_fun m i -> (* Arrow case *) (
302
    fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\""
303
      f
304
      pp_var_name var
305
      (reset_name f)
306
  )
307

    
308
  | MStep (outputs, f, inputs) when not (is_imported_node f m) -> (
309
    let node_f = Machine_code.get_node_def f m in
310
    let is_stateful = List.mem_assoc f m.minstances in 
311
    fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ "
312
      (if is_stateful then "statefulcall" else "statelesscall")
313
      print_protect (fun fmt -> pp_print_string fmt (node_f.node_id)) 
314
      f;
315
    fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
316
      (fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" pp_var_name v)) outputs
317
      pp_emf_cst_or_var_list inputs;
318
    if is_stateful then fprintf fmt ",@ \"reset\": \"%s\"" (reset_name f) else fprintf fmt "@ "
319
  )
320

    
321
  | MStep(outputs, f, inputs ) -> (* This is an imported node *)
322
        EMF_library_calls.pp_call fmt m f outputs inputs
323
	  
324
  | MComment _ 
325
    -> Format.eprintf "unhandled comment in EMF@.@?"; assert false
326
  (* not  available for EMF output *)
327

    
328
  in
329
  fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
330
  fprintf fmt "%a@ " pp_content i;
331
  fprintf fmt "}@]"
332
and pp_emf_instrs m fmt instrs = fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
333
       
334
let pp_machine fmt m =
335
  let instrs = merge_branches m.mstep.step_instrs in
336
  try
337
    fprintf fmt "@[<v 2>\"%a\": {@ "
338
       print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
339
    fprintf fmt "\"kind\": %t,@ \"inputs\": [%a],@ \"outputs\": [%a],@ \"locals\": [%a],@ "
340
      (fun fmt -> if not ( snd (get_stateless_status m) )
341
	then fprintf fmt "\"stateful\""
342
	else fprintf fmt "\"stateless\"")
343
      pp_emf_vars_decl m.mstep.step_inputs
344
      pp_emf_vars_decl m.mstep.step_outputs
345
      pp_emf_vars_decl m.mstep.step_locals
346
    ;
347
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ }"
348
      (pp_emf_instrs m) instrs;
349
    fprintf fmt "@]@ }"
350
  with Unhandled msg -> (
351
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
352
      m.mname.node_id;
353
    eprintf "%s@ " msg;
354
    eprintf "node skipped - no output generated@ @]@."
355
  )
356

    
357
(****************************************************)
358
(* Main function: iterates over node and print them *)
359
(****************************************************)
360
let pp_meta fmt basename =
361
  fprintf fmt "\"meta\": @[<v 0>{@ ";
362
  Utils.fprintf_list ~sep:",@ "
363
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
364
    fmt
365
    ["compiler-name", (Filename.basename Sys.executable_name);
366
     "compiler-version", Version.number;
367
     "command", (String.concat " " (Array.to_list Sys.argv));
368
     "source_file", basename
369
    ]
370
  ;
371
  fprintf fmt "@ @]},@ "
372
    
373
let translate fmt basename prog machines =
374
   (* record_types prog; *)
375
  fprintf fmt "@[<v 0>{@ ";
376
  pp_meta fmt basename;
377
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
378
  (* Previous alternative: mapping normalized lustre to EMF: 
379
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
380
  fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
381
  fprintf fmt "@ @]}";
382
  fprintf fmt "@ @]}"
383

    
384
(* Local Variables: *)
385
(* compile-command: "make -C ../.." *)
386
(* End: *)