Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (12.8 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 preserved for
14
   reference.
15
*)
16

    
17
open LustreSpec
18
open Machine_code
19
open Format
20
open Utils
21

    
22
exception Unhandled of string
23
    
24

    
25
(* Basic printing functions *)
26
    
27
let pp_var_string fmt v = fprintf fmt "\"%s\"" v
28
let pp_var_name fmt v = fprintf fmt "\"%a\"" Printers.pp_var_name v
29
let pp_node_args = fprintf_list ~sep:", " pp_var_name
30

    
31
    
32
(* Matlab starting counting from 1.
33
   simple function to extract the element id in the list. Starts from 1. *)
34
let rec get_idx x l =
35
  match l with
36
  | hd::tl -> if hd = x then 1 else 1+(get_idx x tl)
37
  | [] -> assert false
38

    
39
(**********************************************)
40
(* Old stuff: printing normalized code as EMF *)     
41
(**********************************************)
42

    
43
(*
44
let pp_expr vars fmt expr =
45
  let rec pp_expr fmt expr =
46
    match expr.expr_desc with
47
    | Expr_const c -> Printers.pp_const fmt c
48
    | Expr_ident id ->
49
       if List.mem id vars then
50
	 Format.fprintf fmt "u%i" (get_idx id vars)
51
       else
52
	 assert false (* impossible to find element id in var list *)
53
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
54
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
55
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
56
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
57
    | Expr_ite (c, t, e) -> fprintf fmt "if %a; y=(%a); else y=(%a); end" pp_expr c pp_expr t pp_expr e
58
    | Expr_arrow (e1, e2) ->(
59
      match e1.expr_desc, e2.expr_desc with
60
      | Expr_const c1, Expr_const c2 -> if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then fprintf fmt "STEP" else assert false (* only handle true -> false *)
61
      | _ -> assert false (* only handle true -> false *)
62
    )
63
    | Expr_fby (e1, e2) -> assert false (* not covered yet *)
64
    | Expr_pre e -> fprintf fmt "UNITDELAY"
65
    | Expr_when (e, id, l) -> assert false (* clocked based expressions are not handled yet *)
66
    | Expr_merge (id, hl) -> assert false (* clocked based expressions are not handled yet *)
67
    | Expr_appl (id, e, r) -> pp_app fmt id e r
68

    
69
  and pp_tuple fmt el =
70
    fprintf_list ~sep:"," pp_expr fmt el
71

    
72
  and pp_app fmt id e r =
73
    match r with
74
    | None -> pp_call fmt id e
75
    | Some c -> assert false (* clocked based expressions are not handled yet *)
76

    
77
  and pp_call fmt id e =
78
    match id, e.expr_desc with
79
    | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
80
    | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
81
    | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
82
    | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
83
    | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
84
    | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "mod (%a, %a)" pp_expr e1 pp_expr e2
85
    | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a & %a)" pp_expr e1 pp_expr e2
86
    | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a | %a)" pp_expr e1 pp_expr e2
87
    | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "xor (%a, %a)" pp_expr e1 pp_expr e2
88
    | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "((~%a) | %a)" pp_expr e1 pp_expr e2
89
    | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
90
    | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
91
    | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
92
    | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
93
    | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a ~= %a)" pp_expr e1 pp_expr e2
94
    | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_expr e1 pp_expr e2
95
    | "not", _ -> fprintf fmt "(~%a)" pp_expr e
96
    | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
97
    | _ -> fprintf fmt "%s (%a)" id pp_expr e
98

    
99
  in
100
  pp_expr fmt expr
101

    
102
let pp_stmt fmt stmt =
103
  match stmt with
104
  | Eq eq -> (
105
    match eq.eq_lhs with
106
      [var] -> (
107
     (* first, we extract the expression and associated variables *)
108
	let vars = Utils.ISet.elements (Corelang.get_expr_vars eq.eq_rhs) in
109

    
110
	fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @]}"
111
	  var
112
	  (pp_expr vars) eq.eq_rhs (* todo_pp_expr expr *)
113
	  (fprintf_list ~sep:", " pp_var_string) vars
114
      )
115
    | _ -> assert false (* should not happen for input of EMF backend (cocospec generated nodes *)
116
  )
117
  | _ -> assert false (* should not happen with EMF backend *)
118

    
119
let pp_node fmt nd =
120
  fprintf fmt "@[<v 2>\"%s\": {@ \"inputs\": [%a],@ \"outputs\": [%a],@ "
121
    nd.node_id
122
    pp_node_args nd.node_inputs
123
    pp_node_args nd.node_outputs;
124
  fprintf fmt "\"exprs\": {@[<v 1> %a@]@ }"
125
    (fprintf_list ~sep:",@ " pp_stmt ) nd.node_stmts;
126
  fprintf fmt "@]@ }"
127

    
128
let pp_decl fmt decl =
129
  match decl.top_decl_desc with
130
  | Node nd -> fprintf fmt "%a@ " pp_node nd
131
  | ImportedNode _
132
  | Const _
133
  | Open _
134
  | TypeDef _ -> eprintf "should not happen in EMF backend"
135
*)
136

    
137

    
138
(**********************************************)
139
(*   Printing machine code as EMF             *)
140
(**********************************************)
141

    
142
let rec pp_val vars fmt v =
143
  match v.value_desc with
144
  | Cst c -> Printers.pp_const fmt c
145
  | LocalVar v
146
  | StateVar v ->
147
     let id = v.var_id in
148
     if List.mem id vars then
149
       Format.fprintf fmt "u%i" (get_idx id vars)
150
     else
151
       assert false (* impossible to find element id in var list *)
152
  | Fun (n, vl) -> pp_fun vars n fmt vl
153
  | _ -> assert false (* not available in EMF backend *)
154
and pp_fun vars id fmt vl =
155
  eprintf "print %s with %i args@.@?" id (List.length vl);
156
  match id, vl with
157
    | "+", [v1;v2] -> fprintf fmt "(%a + %a)" (pp_val vars) v1 (pp_val vars) v2
158
    | "uminus", [v] -> fprintf fmt "(- %a)" (pp_val vars) v
159
    | "-", [v1;v2] -> fprintf fmt "(%a - %a)" (pp_val vars) v1 (pp_val vars) v2
160
    | "*",[v1;v2] -> fprintf fmt "(%a * %a)" (pp_val vars) v1 (pp_val vars) v2
161
    | "/", [v1;v2] -> fprintf fmt "(%a / %a)" (pp_val vars) v1 (pp_val vars) v2
162
    | "mod", [v1;v2] -> fprintf fmt "mod (%a, %a)" (pp_val vars) v1 (pp_val vars) v2
163
    | "&&", [v1;v2] -> fprintf fmt "(%a & %a)" (pp_val vars) v1 (pp_val vars) v2
164
    | "||", [v1; v2] -> fprintf fmt "(%a | %a)" (pp_val vars) v1 (pp_val vars) v2
165
    | "xor", [v1; v2] -> fprintf fmt "xor (%a, %a)" (pp_val vars) v1 (pp_val vars) v2
166
    | "impl", [v1; v2] -> fprintf fmt "((~%a) | %a)" (pp_val vars) v1 (pp_val vars) v2
167
    | "<", [v1; v2] -> fprintf fmt "(%a < %a)" (pp_val vars) v1 (pp_val vars) v2
168
    | "<=", [v1; v2] -> fprintf fmt "(%a <= %a)" (pp_val vars) v1 (pp_val vars) v2
169
    | ">", [v1; v2] -> fprintf fmt "(%a > %a)" (pp_val vars) v1 (pp_val vars) v2
170
    | ">=", [v1; v2] -> fprintf fmt "(%a >= %a)" (pp_val vars) v1 (pp_val vars) v2
171
    | "!=", [v1; v2] -> fprintf fmt "(%a != %a)" (pp_val vars) v1 (pp_val vars) v2
172
    | "=", [v1; v2] -> fprintf fmt "(%a = %a)" (pp_val vars) v1 (pp_val vars) v2
173
    | "not", [v] -> fprintf fmt "(~%a)" (pp_val vars) v
174
    | _ -> fprintf fmt "%s (%a)" id  (Utils.fprintf_list ~sep:", " (pp_val vars)) vl 
175

    
176
     
177
(* detect whether the instruction i represents a STEP, ie an arrow with true -> false *)
178
let is_step_fun m i =
179
  match Corelang.get_instr_desc i with
180
  | MStep ([var], i, vl)  -> (
181
    let name = (Machine_code.get_node_def i m).node_id in
182
    match name, vl with
183
    | "_arrow", [v1; v2] -> (
184
	match v1.value_desc, v2.value_desc with
185
	| Cst c1, Cst c2 ->
186
	   if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then
187
	     true
188
	   else
189
	     assert false (* only handle true -> false *)
190
	| _ -> assert false
191
    )
192
    | _ -> false
193
  )
194
  | _ -> false
195

    
196
     
197
let rec pp_instr m vars fmt i =
198
  match Corelang.get_instr_desc i with
199
  | MLocalAssign (var,v) 
200
  | MStateAssign (var,v) -> fprintf fmt "y = %a" (pp_val vars) v
201
  | MStep _ when is_step_fun m i  -> fprintf fmt "STEP" 
202
  | MBranch (g,[(tag1,case1);(tag2,case2)])     ->
203
     let then_case, else_case =
204
       if tag1 = Corelang.tag_true then
205
	 case1, case2
206
       else
207
	 case2, case1
208
     in
209
     fprintf fmt "if %a; %a; else %a; end"
210
       (pp_val vars) g
211
       (pp_instrs m vars) then_case
212
       (pp_instrs m vars) else_case
213
  | MStep _ (* no function calls handled yet *)
214
  | MBranch _ (* EMF backend only accept true/false ite *)
215
  | MReset _           
216
  | MNoReset _
217
  | MComment _ -> assert false (* not  available for EMF output *)
218
and pp_instrs m vars fmt il =
219
  fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," (pp_instr m vars)) il
220

    
221

    
222
let rec get_instr_var i =
223
  match Corelang.get_instr_desc i with
224
  | MLocalAssign (var,_) 
225
  | MStateAssign (var,_) 
226
  | MStep ([var], _, _)  -> var 
227
  | MBranch (_,[(tag1,case1);(tag2,case2)])     ->
228
     get_instrs_var case1 (* assuming case1 and case2 define the same variable *)
229
  | MStep _ (* only single output for function call *)
230
  | MBranch _ (* EMF backend only accept true/false ite *)
231
  | MReset _           
232
  | MNoReset _
233
  | MComment _ -> assert false (* not  available for EMF output *)
234
and get_instrs_var il =
235
  match il with
236
  | i::_ -> get_instr_var i (* looking for the first instr *)
237
  | _ -> assert false
238

    
239
  
240
let rec  get_val_vars v =
241
  match v.value_desc with
242
  | Cst c -> Utils.ISet.empty
243
  | LocalVar v
244
  | StateVar v -> Utils.ISet.singleton v.var_id
245
  | Fun (n, vl) -> List.fold_left (fun res v -> Utils.ISet.union (get_val_vars v) res) Utils.ISet.empty vl
246
  | _ -> assert false (* not available in EMF backend *)
247

    
248
let rec get_instr_vars i =
249
  match Corelang.get_instr_desc i with
250
  | MLocalAssign (_,v)  
251
  | MStateAssign (_,v) -> get_val_vars v
252
  | MStep ([_], _, vl)  -> List.fold_left (fun res v -> Utils.ISet.union res (get_val_vars v)) Utils.ISet.empty vl 
253
  | MBranch (c,[(_,case1);(_,case2)])     ->
254
     Utils.ISet.union
255
       (get_val_vars c)
256
       (
257
	 Utils.ISet.union
258
	   (get_instrs_vars case1)
259
	   (get_instrs_vars case2)
260
       )
261
  | MStep _ (* only single output for function call *)
262
  | MBranch _ (* EMF backend only accept true/false ite *)
263
  | MReset _           
264
  | MNoReset _
265
  | MComment _ -> failwith "Error in compiling some constructs into EMF. Have you considered -node foo -inline options ?" (* not  available for EMF output *)
266
and get_instrs_vars il =
267
  List.fold_left (fun res i -> Utils.ISet.union res (get_instr_vars i))
268
    Utils.ISet.empty
269
    il
270

    
271

    
272
let pp_original_lustre_expression m fmt i =
273
  match Corelang.get_instr_desc i with
274
  | MLocalAssign _ | MStateAssign _ 
275
  | MBranch _
276
    -> ( match i.lustre_eq with None -> () | Some e -> Printers.pp_node_eq fmt e) 
277
  | MStep _ when is_step_fun m i -> () (* we print nothing, this is a STEP *)
278
  | MStep _ -> (match i.lustre_eq with None -> () | Some eq -> Printers.pp_node_eq fmt eq)
279
  | _ -> ()
280
    
281
let pp_instr_main m fmt i =
282
  (* first, we extract the expression and associated variables *)
283
  let var = get_instr_var i in
284
  let vars = Utils.ISet.elements (get_instr_vars i) in	
285
  fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%a]@]}"
286
    var.var_id
287
    (pp_instr m vars) i
288
    (fprintf_list ~sep:", " pp_var_string) vars
289
    (pp_original_lustre_expression m) i
290

    
291
    
292
     
293
let pp_machine fmt m =
294
  try
295
    fprintf fmt "@[<v 2>\"%s\": {@ \"inputs\": [%a],@ \"outputs\": [%a],@ "
296
      m.mname.node_id
297
      pp_node_args m.mstep.step_inputs
298
      pp_node_args m.mstep.step_outputs;
299
    fprintf fmt "\"exprs\": {@[<v 1> %a@]@ }"
300
      (fprintf_list ~sep:",@ " (pp_instr_main m)) m.mstep.step_instrs;
301
    fprintf fmt "@]@ }"
302
  with Unhandled msg -> (
303
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
304
      m.mname.node_id;
305
    eprintf "%s@ " msg;
306
    eprintf "node skipped - no output generated@ @]@."
307
  )
308

    
309
(****************************************************)
310
(* Main function: iterates over node and print them *)
311
(****************************************************)
312
let pp_meta fmt basename =
313
  fprintf fmt "\"meta\": @[<v 0>{@ ";
314
  Utils.fprintf_list ~sep:",@ "
315
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
316
    fmt
317
    ["compiler-name", (Filename.basename Sys.executable_name);
318
     "compiler-version", Version.number;
319
     "command", (String.concat " " (Array.to_list Sys.argv));
320
     "source_file", basename
321
    ]
322
  ;
323
  fprintf fmt "@ @]},@ "
324
    
325
let translate fmt basename prog machines =
326
  fprintf fmt "@[<v 0>{@ ";
327
  pp_meta fmt basename;
328
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
329
  (* fprintf_list ~sep:",@ " pp_decl fmt prog; *)
330
  fprintf_list ~sep:",@ " pp_machine fmt machines;
331
  fprintf fmt "@ @]}";
332
  fprintf fmt "@ @]}"
333

    
334
(* Local Variables: *)
335
(* compile-command: "make -C ../.." *)
336
(* End: *)