Revision d4807c3d src/machine_code.ml
src/machine_code.ml | ||
---|---|---|
215 | 215 |
o |
216 | 216 |
end |
217 | 217 |
|
218 |
let const_of_carrier cr = |
|
219 |
match (carrier_repr cr).carrier_desc with |
|
220 |
| Carry_const id -> id |
|
221 |
| Carry_name |
|
222 |
| Carry_var |
|
223 |
| Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *) |
|
224 |
|
|
225 | 218 |
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *) |
226 | 219 |
(* the context contains m : state aka memory variables *) |
227 | 220 |
(* si : initialization instructions *) |
... | ... | |
240 | 233 |
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst = |
241 | 234 |
match (Clocks.repr ck).cdesc with |
242 | 235 |
| Con (ck1, cr, l) -> |
243 |
let id = const_of_carrier cr in |
|
236 |
let id = Clocks.const_of_carrier cr in
|
|
244 | 237 |
control_on_clock node args ck1 (MBranch (translate_ident node args id, |
245 | 238 |
[l, [inst]] )) |
246 | 239 |
| _ -> inst |
... | ... | |
313 | 306 |
let translate_guard node args expr = |
314 | 307 |
match expr.expr_desc with |
315 | 308 |
| Expr_ident x -> translate_ident node args x |
316 |
| _ -> assert false
|
|
309 |
| _ -> (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false)
|
|
317 | 310 |
|
318 | 311 |
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = |
319 | 312 |
match expr.expr_desc with |
... | ... | |
367 | 360 |
node_f, |
368 | 361 |
NodeDep.filter_static_inputs (node_inputs node_f) el in |
369 | 362 |
let o = new_instance node node_f eq.eq_rhs.expr_tag in |
363 |
let call_ck = Clocks.new_var true in |
|
364 |
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock; |
|
370 | 365 |
(m, |
371 | 366 |
(if Stateless.check_node node_f then si else MReset o :: si), |
372 | 367 |
(if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j), |
373 | 368 |
d, |
374 | 369 |
reset_instance node args o r eq.eq_rhs.expr_clock @ |
375 |
(control_on_clock node args eq.eq_rhs.expr_clock (MStep (var_p, o, vl))) :: s)
|
|
370 |
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
|
|
376 | 371 |
|
377 | 372 |
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) |
378 | 373 |
are preserved. While they are replaced as if g then x = t else x = e in C or Java |
Also available in: Unified diff