Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / EMF / EMF_backend.ml @ 2823bc51

History | View | Annotate | Download (11.9 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, _) -> 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
  | MStep (outs, id, _) -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" Printers.pp_var_name) outs id
153
  | _ -> () (* No name *)
154

    
155
let rec branch_block_vars il =
156
  List.fold_left
157
    (fun (accu_def, accu_read) i ->
158
      let defined_vars, read_vars = branch_instr_vars i in
159
      ISet.union accu_def defined_vars, VSet.union accu_read read_vars)
160
    (ISet.empty, VSet.empty) il
161
and branch_instr_vars i =
162
  match Corelang.get_instr_desc i with
163
  | MLocalAssign (var,expr) 
164
  | MStateAssign (var,expr) -> ISet.singleton var.var_id, get_expr_vars expr
165
  | MStep (vars, _, args)  ->
166
     ISet.of_list (List.map (fun v -> v.var_id) vars),
167
    List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args
168
  | MBranch (g,(_,hd_il)::tl)     -> (* We focus on variables defined in all branches *)
169
     let read_guard = get_expr_vars g in
170
     let def_vars_hd, read_vars_hd = branch_block_vars hd_il in
171
     let def_vars, read_vars =
172
       List.fold_left
173
	 (fun (def_vars, read_vars) (_, il) ->
174
	 (* We accumulate reads but intersect writes *)
175
	   let writes_il, reads_il = branch_block_vars il in
176
	   ISet.inter def_vars writes_il,
177
	 VSet.union read_vars reads_il
178
	 )
179
	 (def_vars_hd, read_vars_hd)
180
	 tl
181
     in
182
     def_vars, VSet.union read_guard read_vars
183
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
184
  | MReset ni           
185
  | MNoReset ni -> ISet.singleton (reset_name ni), VSet.empty
186
  | MComment _ -> assert false (* not  available for EMF output *)
187
     
188
  
189
      
190
let rec pp_emf_instr m fmt i =
191
  let pp_content fmt i =
192
    match Corelang.get_instr_desc i with
193
    | MLocalAssign(lhs, expr)
194
    -> (
195
      (match expr.value_desc with
196
      | Fun (fun_id, vl) -> (
197
	(* Thanks to normalization, vl shall only contain constant or
198
	   local/state vars but not calls to other functions *)
199
	fprintf fmt "\"kind\": \"operator\",@ ";
200
	fprintf fmt "\"lhs\": \"%a\",@ " Printers.pp_var_name lhs;
201
	fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
202
	  fun_id
203
	  pp_emf_cst_or_var_list vl
204
      )	 
205
      | Array _ | Access _ | Power _ -> assert false (* No array expression allowed yet *)
206
      | Cst _ 
207
      | LocalVar _
208
      | StateVar _ -> (
209
	fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
210
	  Printers.pp_var_name lhs
211
	  pp_emf_cst_or_var expr
212
      ))    )
213

    
214
  | MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a
215
			       variable or a constant, no function anymore! *)
216
    -> (
217
      fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
218
	Printers.pp_var_name lhs
219
	pp_emf_cst_or_var expr
220
    )
221
     
222
  | MReset id           
223
    -> (
224
      fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
225
	(reset_name id)
226
    )
227
  | MNoReset id           
228
    -> (
229
      fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
230
	(reset_name id)
231
    )
232
    
233
  | MBranch (g, hl) -> (
234
    let outputs, inputs = branch_instr_vars i in
235
    fprintf fmt "\"kind\": \"branch\",@ ";
236
    fprintf fmt "\"guard\": %a,@ " pp_emf_cst_or_var g; (* it has to be a variable or a constant *)
237
    fprintf fmt "\"outputs\": [%a],@ " (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs);
238
    fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
239
      (* (let guard_inputs = get_expr_vars g in
240
	  VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to
241
	 remove guard's variable from inputs *)
242
      (VSet.elements inputs)
243
    ;
244
    fprintf fmt "@[<v 2>\"branches\": {@ %a@]}@ "
245
      (fprintf_list ~sep:",@ "
246
	 (fun fmt (tag, instrs_tag) ->
247
	   let (*branch_outputs*) _, branch_inputs = branch_block_vars instrs_tag in    	   
248
	   fprintf fmt "@[<v 2>\"%s\": {@ " tag;
249
	   fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag; 
250
	   fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl (VSet.elements branch_inputs); 
251
	   fprintf fmt "@[<v 2>\"instrs\": {@ ";
252
	   fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs_tag;
253
	   fprintf fmt "@]}@ ";
254
	   fprintf fmt "@]}"
255

    
256
	 )
257
      )
258
      hl
259
   )
260

    
261
  | MStep ([var], f, _) when is_arrow_fun m i -> (* Arrow case *) (
262
    fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\""
263
      f
264
      Printers.pp_var_name var
265
      (reset_name f)
266
  )
267

    
268
  | MStep (outputs, f, inputs) when not (is_imported_node f m) -> (
269
    let node_f = Machine_code.get_node_def f m in
270
    let is_stateful = List.mem_assoc f m.minstances in 
271
    fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%s\",@ \"id\": \"%s\",@ "
272
      (if is_stateful then "statefulcall" else "statelesscall")
273
      (node_f.node_id) 
274
      f;
275
    fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
276
      (fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" Printers.pp_var_name v)) outputs
277
      pp_emf_cst_or_var_list inputs;
278
    if is_stateful then fprintf fmt ",@ \"reset\": \"%s\"" (reset_name f) else fprintf fmt "@ "
279
  )
280

    
281
  | MStep(outputs, f, inputs ) -> (* This is an imported node *)
282
        EMF_library_calls.pp_call fmt m f outputs inputs
283
	  
284
  | MComment _ 
285
    -> Format.eprintf "unhandled comment in EMF@.@?"; assert false
286
  (* not  available for EMF output *)
287

    
288
  in
289
  fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
290
  fprintf fmt "%a@ " pp_content i;
291
  fprintf fmt "}@]"
292

    
293
       
294
let pp_machine fmt m =
295
  try
296
    fprintf fmt "@[<v 2>\"%s\": {@ "
297
      m.mname.node_id;
298
    fprintf fmt "\"kind\": %t,@ \"inputs\": [%a],@ \"outputs\": [%a],@ \"locals\": [%a],@ "
299
      (fun fmt -> if not ( snd (get_stateless_status m) )
300
	then fprintf fmt "\"stateful\""
301
	else fprintf fmt "\"stateless\"")
302
      pp_emf_vars_decl m.mstep.step_inputs
303
      pp_emf_vars_decl m.mstep.step_outputs
304
      pp_emf_vars_decl m.mstep.step_locals
305
    ;
306
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ }"
307
      (fprintf_list ~sep:",@ " (pp_emf_instr m)) m.mstep.step_instrs;
308
    fprintf fmt "@]@ }"
309
  with Unhandled msg -> (
310
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
311
      m.mname.node_id;
312
    eprintf "%s@ " msg;
313
    eprintf "node skipped - no output generated@ @]@."
314
  )
315

    
316
(****************************************************)
317
(* Main function: iterates over node and print them *)
318
(****************************************************)
319
let pp_meta fmt basename =
320
  fprintf fmt "\"meta\": @[<v 0>{@ ";
321
  Utils.fprintf_list ~sep:",@ "
322
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
323
    fmt
324
    ["compiler-name", (Filename.basename Sys.executable_name);
325
     "compiler-version", Version.number;
326
     "command", (String.concat " " (Array.to_list Sys.argv));
327
     "source_file", basename
328
    ]
329
  ;
330
  fprintf fmt "@ @]},@ "
331
    
332
let translate fmt basename prog machines =
333
  (* record_types prog; *)
334
  fprintf fmt "@[<v 0>{@ ";
335
  pp_meta fmt basename;
336
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
337
  (* Previous alternative: mapping normalized lustre to EMF: 
338
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
339
  fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
340
  fprintf fmt "@ @]}";
341
  fprintf fmt "@ @]}"
342

    
343
(* Local Variables: *)
344
(* compile-command: "make -C ../.." *)
345
(* End: *)