139 |
139 |
(* Printing machine code as EMF *)
|
140 |
140 |
(**********************************************)
|
141 |
141 |
|
|
142 |
(* Print machine code values as matlab expressions. Variable identifiers are
|
|
143 |
replaced by uX where X is the index of the variables in the list vars of input
|
|
144 |
variables. *)
|
142 |
145 |
let rec pp_val vars fmt v =
|
143 |
146 |
match v.value_desc with
|
144 |
147 |
| Cst c -> Printers.pp_const fmt c
|
... | ... | |
152 |
155 |
| Fun (n, vl) -> pp_fun vars n fmt vl
|
153 |
156 |
| _ -> assert false (* not available in EMF backend *)
|
154 |
157 |
and pp_fun vars id fmt vl =
|
155 |
|
eprintf "print %s with %i args@.@?" id (List.length vl);
|
|
158 |
(* eprintf "print %s with %i args@.@?" id (List.length vl);*)
|
156 |
159 |
match id, vl with
|
157 |
160 |
| "+", [v1;v2] -> fprintf fmt "(%a + %a)" (pp_val vars) v1 (pp_val vars) v2
|
158 |
161 |
| "uminus", [v] -> fprintf fmt "(- %a)" (pp_val vars) v
|
... | ... | |
174 |
177 |
| _ -> fprintf fmt "%s (%a)" id (Utils.fprintf_list ~sep:", " (pp_val vars)) vl
|
175 |
178 |
|
176 |
179 |
|
177 |
|
(* detect whether the instruction i represents a STEP, ie an arrow with true -> false *)
|
178 |
|
let is_step_fun m i =
|
|
180 |
(* detect whether the instruction i represents an ARROW, ie an arrow with true -> false *)
|
|
181 |
let is_arrow_fun m i =
|
179 |
182 |
match Corelang.get_instr_desc i with
|
180 |
183 |
| MStep ([var], i, vl) -> (
|
181 |
|
let name = (Machine_code.get_node_def i m).node_id in
|
|
184 |
let name = try (Machine_code.get_node_def i m).node_id with Not_found -> Format.eprintf "Impossible to find node %s@.@?" i; raise Not_found in
|
182 |
185 |
match name, vl with
|
183 |
186 |
| "_arrow", [v1; v2] -> (
|
184 |
187 |
match v1.value_desc, v2.value_desc with
|
... | ... | |
193 |
196 |
)
|
194 |
197 |
| _ -> false
|
195 |
198 |
|
196 |
|
|
197 |
|
let rec pp_instr m vars fmt i =
|
|
199 |
(* pp_basic_instr prints regular instruction. These do not contain MStep which
|
|
200 |
should have been already filtered out. Another restriction which is supposed
|
|
201 |
to be enforced is that branching statement contain a single instruction (in
|
|
202 |
practice it has to be an assign) *)
|
|
203 |
let rec pp_basic_instr m vars fmt i =
|
198 |
204 |
match Corelang.get_instr_desc i with
|
199 |
205 |
| MLocalAssign (var,v)
|
200 |
206 |
| 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)]) ->
|
|
207 |
| MBranch (g,[(tag1,[case1]);(tag2,[case2])]) ->
|
|
208 |
(* Thanks to normalization with join_guards = false, branches shall contain
|
|
209 |
a single expression *)
|
203 |
210 |
let then_case, else_case =
|
204 |
211 |
if tag1 = Corelang.tag_true then
|
205 |
212 |
case1, case2
|
... | ... | |
208 |
215 |
in
|
209 |
216 |
fprintf fmt "if %a; %a; else %a; end"
|
210 |
217 |
(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 *)
|
|
218 |
(pp_basic_instr m vars) then_case
|
|
219 |
(pp_basic_instr m vars) else_case
|
214 |
220 |
| MBranch _ (* EMF backend only accept true/false ite *)
|
|
221 |
-> Format.eprintf "unhandled branch in EMF@.@?"; assert false
|
215 |
222 |
| MReset _
|
|
223 |
-> Format.eprintf "unhandled reset in EMF@.@?"; assert false
|
216 |
224 |
| 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
|
|
225 |
-> Format.eprintf "unhandled noreset in EMF@.@?"; assert false
|
|
226 |
| MStep _ (* function calls already handled, including STEP *)
|
|
227 |
-> Format.eprintf "unhandled function call in EMF (should have been filtered out before)@.@?";
|
|
228 |
assert false
|
|
229 |
| MComment _
|
|
230 |
-> Format.eprintf "unhandled comment in EMF@.@?"; assert false
|
|
231 |
(* not available for EMF output *)
|
|
232 |
|
220 |
233 |
|
221 |
234 |
|
222 |
235 |
let rec get_instr_var i =
|
... | ... | |
249 |
262 |
match Corelang.get_instr_desc i with
|
250 |
263 |
| MLocalAssign (_,v)
|
251 |
264 |
| 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)]) ->
|
|
265 |
| MStep (_, _, vl) -> List.fold_left (fun res v -> Utils.ISet.union res (get_val_vars v)) Utils.ISet.empty vl
|
|
266 |
| MBranch (c,[(_,[case1]);(_,[case2])]) ->
|
254 |
267 |
Utils.ISet.union
|
255 |
268 |
(get_val_vars c)
|
256 |
269 |
(
|
257 |
270 |
Utils.ISet.union
|
258 |
|
(get_instrs_vars case1)
|
259 |
|
(get_instrs_vars case2)
|
|
271 |
(get_instr_vars case1)
|
|
272 |
(get_instr_vars case2)
|
260 |
273 |
)
|
261 |
|
| MStep _ (* only single output for function call *)
|
262 |
274 |
| MBranch _ (* EMF backend only accept true/false ite *)
|
263 |
275 |
| MReset _
|
264 |
276 |
| MNoReset _
|
265 |
277 |
| 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
|
|
278 |
(* and get_instrs_vars il = *)
|
|
279 |
(* List.fold_left (fun res i -> Utils.ISet.union res (get_instr_vars i)) *)
|
|
280 |
(* Utils.ISet.empty *)
|
|
281 |
(* il *)
|
270 |
282 |
|
271 |
283 |
|
272 |
284 |
let pp_original_lustre_expression m fmt i =
|
... | ... | |
274 |
286 |
| MLocalAssign _ | MStateAssign _
|
275 |
287 |
| MBranch _
|
276 |
288 |
-> ( 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 *)
|
|
289 |
| MStep _ when is_arrow_fun m i -> () (* we print nothing, this is a STEP *)
|
278 |
290 |
| MStep _ -> (match i.lustre_eq with None -> () | Some eq -> Printers.pp_node_eq fmt eq)
|
279 |
291 |
| _ -> ()
|
280 |
292 |
|
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 |
|
|
|
293 |
let pp_emf_instrs m fmt i =
|
|
294 |
(* Either it is a Step function non arrow, then we have a dedicated treatment,
|
|
295 |
or it has to be a single variable assigment *)
|
|
296 |
let arguments_vars = Utils.ISet.elements (get_instr_vars i) in
|
|
297 |
|
|
298 |
match Corelang.get_instr_desc i with
|
|
299 |
(* Regular node call either a statuful node or a functional one *)
|
|
300 |
MStep (outputs, f, inputs) when not (is_arrow_fun m i) -> (
|
|
301 |
fprintf fmt "\"__functioncall\": @[<v 2>{ \"node\": \"%s\",@ \"inputs\": [%a],@ \"vars\": [%a]@ \"outputs\": [%a],@ \"original_lustre_expr\": [%a]@]}"
|
|
302 |
((Machine_code.get_node_def f m).node_id) (* Node name *)
|
|
303 |
(Utils.fprintf_list ~sep:", " (fun fmt _val -> fprintf fmt "\"%a\"" (pp_val arguments_vars) _val)) inputs (* inputs *)
|
|
304 |
(fprintf_list ~sep:", " pp_var_string) arguments_vars
|
|
305 |
(fprintf_list ~sep:", " (fun fmt v -> pp_var_string fmt v.var_id)) outputs (* outputs *)
|
|
306 |
(pp_original_lustre_expression m) i (* original lustre expr *)
|
|
307 |
)
|
|
308 |
| _ ->
|
|
309 |
(* Other expressions, including "pre" *)
|
|
310 |
(
|
|
311 |
(* first, we extract the expression and associated variables *)
|
|
312 |
let var = get_instr_var i in
|
|
313 |
fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%a]@]}"
|
|
314 |
var.var_id
|
|
315 |
(fun fmt i -> match Corelang.get_instr_desc i with
|
|
316 |
| MStep _ -> fprintf fmt "STEP"
|
|
317 |
| _ -> pp_basic_instr m arguments_vars fmt i) i
|
|
318 |
(fprintf_list ~sep:", " pp_var_string) arguments_vars
|
|
319 |
(pp_original_lustre_expression m) i
|
|
320 |
)
|
291 |
321 |
|
292 |
322 |
|
293 |
323 |
let pp_machine fmt m =
|
... | ... | |
297 |
327 |
pp_node_args m.mstep.step_inputs
|
298 |
328 |
pp_node_args m.mstep.step_outputs;
|
299 |
329 |
fprintf fmt "\"exprs\": {@[<v 1> %a@]@ }"
|
300 |
|
(fprintf_list ~sep:",@ " (pp_instr_main m)) m.mstep.step_instrs;
|
|
330 |
(fprintf_list ~sep:",@ " (pp_emf_instrs m)) m.mstep.step_instrs;
|
301 |
331 |
fprintf fmt "@]@ }"
|
302 |
332 |
with Unhandled msg -> (
|
303 |
333 |
eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
|
... | ... | |
326 |
356 |
fprintf fmt "@[<v 0>{@ ";
|
327 |
357 |
pp_meta fmt basename;
|
328 |
358 |
fprintf fmt "\"nodes\": @[<v 0>{@ ";
|
329 |
|
(* fprintf_list ~sep:",@ " pp_decl fmt prog; *)
|
|
359 |
(* Previous alternative: mapping normalized lustre to EMF:
|
|
360 |
fprintf_list ~sep:",@ " pp_decl fmt prog; *)
|
330 |
361 |
fprintf_list ~sep:",@ " pp_machine fmt machines;
|
331 |
362 |
fprintf fmt "@ @]}";
|
332 |
363 |
fprintf fmt "@ @]}"
|
Improved EMF backend. Working on the whole fmcad suite