Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / EMF / EMF_backend.ml @ 3ca27bc7

History | View | Annotate | Download (12.3 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
   code. We now rely on machine code printing. The old code is preserved for
14
   reference.
15
*)
16
17 a6df3992 Ploc
open LustreSpec
18 f7caf067 ploc
open Machine_code
19 a6df3992 Ploc
open Format
20
open Utils
21
22 f7caf067 ploc
exception Unhandled of string
23 3ca27bc7 ploc
    
24
25
(* Basic printing functions *)
26
    
27 a6df3992 Ploc
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 3ca27bc7 ploc
    
32
(* Matlab starting counting from 1.
33
   simple function to extract the element id in the list. Starts from 1. *)
34 f7caf067 ploc
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 3ca27bc7 ploc
39
(**********************************************)
40
(* Old stuff: printing normalized code as EMF *)     
41
(**********************************************)
42
43
(*
44 a6df3992 Ploc
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 32539b6d ploc
	 Format.fprintf fmt "u%i" (get_idx id vars)
51 a6df3992 Ploc
       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 97be8db8 Teme
    | 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 a6df3992 Ploc
    | 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 30dee850 Teme
    | Expr_pre e -> fprintf fmt "UNITDELAY"
65 a6df3992 Ploc
    | 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 97be8db8 Teme
    | "!=", 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 a6df3992 Ploc
    | "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 97be8db8 Teme
110 d3e837ea Ploc
	fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @]}"
111 a6df3992 Ploc
	  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 d3e837ea Ploc
  fprintf fmt "@[<v 2>\"%s\": {@ \"inputs\": [%a],@ \"outputs\": [%a],@ "
121 a6df3992 Ploc
    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 d3e837ea Ploc
    (fprintf_list ~sep:",@ " pp_stmt ) nd.node_stmts;
126 a6df3992 Ploc
  fprintf fmt "@]@ }"
127 30dee850 Teme
128 a6df3992 Ploc
let pp_decl fmt decl =
129
  match decl.top_decl_desc with
130
  | Node nd -> fprintf fmt "%a@ " pp_node nd
131 30dee850 Teme
  | ImportedNode _
132 a6df3992 Ploc
  | Const _
133 30dee850 Teme
  | Open _
134 a6df3992 Ploc
  | TypeDef _ -> eprintf "should not happen in EMF backend"
135 3ca27bc7 ploc
*)
136
137
138
(**********************************************)
139
(*   Printing machine code as EMF             *)
140
(**********************************************)
141 a6df3992 Ploc
142 f7caf067 ploc
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 32539b6d ploc
       Format.fprintf fmt "u%i" (get_idx id vars)
150 f7caf067 ploc
     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 a6df3992 Ploc
176 3ca27bc7 ploc
     
177 f7caf067 ploc
178
     
179
let rec pp_instr m vars fmt i =
180 3ca27bc7 ploc
  match Corelang.get_instr_desc i with
181 f7caf067 ploc
  | MLocalAssign (var,v) 
182
  | MStateAssign (var,v) -> fprintf fmt "y = %a" (pp_val vars) v
183
  | MStep ([var], i, vl)  -> (
184
    let name = (Machine_code.get_node_def i m).node_id in
185
    match name, vl with
186
      "_arrow", [v1; v2] -> (
187
	match v1.value_desc, v2.value_desc with
188
	| Cst c1, Cst 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 *)
189
	| _ -> assert false
190
      )
191
    | _ -> raise (Unhandled ("call to node " ^ name))
192
  )
193
  | MBranch (g,[(tag1,case1);(tag2,case2)])     ->
194
     let then_case, else_case =
195
       if tag1 = Corelang.tag_true then
196
	 case1, case2
197
       else
198
	 case2, case1
199
     in
200
     fprintf fmt "if %a; %a; else %a; end"
201
       (pp_val vars) g
202
       (pp_instrs m vars) then_case
203
       (pp_instrs m vars) else_case
204
  | MStep _ (* only single output for function call *)
205
  | MBranch _ (* EMF backend only accept true/false ite *)
206
  | MReset _           
207
  | MNoReset _
208
  | MComment _ -> assert false (* not  available for EMF output *)
209
and pp_instrs m vars fmt il =
210
  fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," (pp_instr m vars)) il
211
212 3ca27bc7 ploc
213 f7caf067 ploc
let rec get_instr_var i =
214 3ca27bc7 ploc
  match Corelang.get_instr_desc i with
215 f7caf067 ploc
  | MLocalAssign (var,_) 
216
  | MStateAssign (var,_) 
217
  | MStep ([var], _, _)  -> var 
218
  | MBranch (_,[(tag1,case1);(tag2,case2)])     ->
219
     get_instrs_var case1 (* assuming case1 and case2 define the same variable *)
220
  | MStep _ (* only single output for function call *)
221
  | MBranch _ (* EMF backend only accept true/false ite *)
222
  | MReset _           
223
  | MNoReset _
224
  | MComment _ -> assert false (* not  available for EMF output *)
225
and get_instrs_var il =
226
  match il with
227
  | i::_ -> get_instr_var i (* looking for the first instr *)
228
  | _ -> assert false
229
230 3ca27bc7 ploc
  
231 f7caf067 ploc
let rec  get_val_vars v =
232
  match v.value_desc with
233
  | Cst c -> Utils.ISet.empty
234
  | LocalVar v
235
  | StateVar v -> Utils.ISet.singleton v.var_id
236
  | Fun (n, vl) -> List.fold_left (fun res v -> Utils.ISet.union (get_val_vars v) res) Utils.ISet.empty vl
237
  | _ -> assert false (* not available in EMF backend *)
238 3ca27bc7 ploc
239 f7caf067 ploc
let rec get_instr_vars i =
240 3ca27bc7 ploc
  match Corelang.get_instr_desc i with
241 f7caf067 ploc
  | MLocalAssign (_,v)  
242
  | MStateAssign (_,v) -> get_val_vars v
243
  | MStep ([_], _, vl)  -> List.fold_left (fun res v -> Utils.ISet.union res (get_val_vars v)) Utils.ISet.empty vl 
244
  | MBranch (c,[(_,case1);(_,case2)])     ->
245
     Utils.ISet.union
246
       (get_val_vars c)
247
       (
248
	 Utils.ISet.union
249
	   (get_instrs_vars case1)
250
	   (get_instrs_vars case2)
251
       )
252
  | MStep _ (* only single output for function call *)
253
  | MBranch _ (* EMF backend only accept true/false ite *)
254
  | MReset _           
255
  | MNoReset _
256 3ca27bc7 ploc
  | MComment _ -> failwith "Error in compiling some constructs into EMF. Have you considered -node foo -inline options ?" (* not  available for EMF output *)
257 f7caf067 ploc
and get_instrs_vars il =
258
  List.fold_left (fun res i -> Utils.ISet.union res (get_instr_vars i))
259
    Utils.ISet.empty
260
    il
261
    
262
let pp_instr_main m fmt i =
263
  (* first, we extract the expression and associated variables *)
264
  let var = get_instr_var i in
265
  let vars = Utils.ISet.elements (get_instr_vars i) in	
266 3ca27bc7 ploc
  fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%t]@]}"
267 f7caf067 ploc
    var.var_id
268
    (pp_instr m vars) i
269
    (fprintf_list ~sep:", " pp_var_string) vars
270 3ca27bc7 ploc
    (fun fmt -> ()
271
      (*xxxx
272
      if is expr than print associated lustre eq else empty string
273
	xxx todo
274
      *)
275
    ) 
276 f7caf067 ploc
     
277
let pp_machine fmt m =
278
  try
279
    fprintf fmt "@[<v 2>\"%s\": {@ \"inputs\": [%a],@ \"outputs\": [%a],@ "
280
      m.mname.node_id
281
      pp_node_args m.mstep.step_inputs
282
      pp_node_args m.mstep.step_outputs;
283
    fprintf fmt "\"exprs\": {@[<v 1> %a@]@ }"
284
      (fprintf_list ~sep:",@ " (pp_instr_main m)) m.mstep.step_instrs;
285
    fprintf fmt "@]@ }"
286
  with Unhandled msg -> (
287
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
288
      m.mname.node_id;
289
    eprintf "%s@ " msg;
290
    eprintf "node skipped - no output generated@ @]@."
291
  )
292 3ca27bc7 ploc
293
(****************************************************)
294
(* Main function: iterates over node and print them *)
295
(****************************************************)
296
let pp_meta fmt basename =
297
  fprintf fmt "\"meta\": @[<v 0>{@ ";
298
  Utils.fprintf_list ~sep:",@ "
299
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
300
    fmt
301
    ["compiler-name", (Filename.basename Sys.executable_name);
302
     "compiler-version", Version.number;
303
     "command", (String.concat " " (Array.to_list Sys.argv));
304
     "source_file", basename
305
    ]
306
  ;
307
  fprintf fmt "@ @]},@ "
308 f7caf067 ploc
    
309 3ca27bc7 ploc
let translate fmt basename prog machines =
310 a6df3992 Ploc
  fprintf fmt "@[<v 0>{@ ";
311 3ca27bc7 ploc
  pp_meta fmt basename;
312
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
313 f7caf067 ploc
  (* fprintf_list ~sep:",@ " pp_decl fmt prog; *)
314
  fprintf_list ~sep:",@ " pp_machine fmt machines;
315 3ca27bc7 ploc
  fprintf fmt "@ @]}";
316 a6df3992 Ploc
  fprintf fmt "@ @]}"
317 3ca27bc7 ploc
318
(* Local Variables: *)
319
(* compile-command: "make -C ../.." *)
320
(* End: *)