Revision d0f26f04
Added by LĂ©lio Brun 7 months ago
src/machine_code.ml  

236  236 
 None > 
237  237 
None, [] 
238  238  
239 
let translate_eq env ctx id inputs locals outputs i eq = 

239 
let translate_eq env ctx nd inputs locals outputs i eq = 

240 
let id = nd.node_id in 

240  241 
let translate_expr = translate_expr env in 
241  242 
let translate_act = translate_act env in 
242  243 
let locals_pi = Lustre_live.inter_live_i_with id (i  1) locals in 
...  ...  
268  269 
{ 
269  270 
inst with 
270  271 
instr_spec = 
271 
[ 

272 
mk_memory_pack ~i id; 

273 
mk_transition ~i id (vdecls_to_vals inputs) 

274 
(vdecls_to_vals locals_i) (vdecls_to_vals outputs_i); 

275 
]; 

272 
(if fst (get_stateless_status_node nd) then [] 

273 
else [ mk_memory_pack ~i id ]) 

274 
@ [ 

275 
mk_transition ~i id (vdecls_to_vals inputs) 

276 
(vdecls_to_vals locals_i) (vdecls_to_vals outputs_i); 

277 
]; 

276  278 
} 
277  279 
:: ctx.s; 
278  280 
mp = pred_mp ctx spec_mp; 
...  ...  
388  390 
else eqs) 
389  391 
[] locals 
390  392  
391 
let translate_eqs env ctx id inputs locals outputs eqs =


393 
let translate_eqs env ctx nd inputs locals outputs eqs =


392  394 
List.fold_left 
393  395 
(fun (ctx, i) eq > 
394 
let ctx = translate_eq env ctx id inputs locals outputs i eq in


396 
let ctx = translate_eq env ctx nd inputs locals outputs i eq in


395  397 
ctx, i + 1) 
396  398 
(ctx, 1) eqs 
397  399 
> fst 
...  ...  
434  436 
in 
435  437 
vars, eql, assertl 
436  438  
437 
let translate_core env nid sorted_eqs inputs locals outputs =


439 
let translate_core env nd sorted_eqs inputs locals outputs = 

438  440 
let constant_eqs = constant_equations locals in 
439  441  
440  442 
(* Compute constants' instructions *) 
441 
let ctx0 = 

442 
translate_eqs env ctx_init nid inputs locals outputs constant_eqs 

443 
in 

443 
let ctx0 = translate_eqs env ctx_init nd inputs locals outputs constant_eqs in 

444  444 
assert (ctx0.si = []); 
445  445 
assert (IMap.is_empty ctx0.j); 
446  446  
447  447 
(* Compute ctx for all eqs *) 
448 
let ctx = translate_eqs env ctx_init nid inputs locals outputs sorted_eqs in


448 
let ctx = translate_eqs env ctx_init nd inputs locals outputs sorted_eqs in 

449  449  
450  450 
ctx, ctx0.s 
451  451  
...  ...  
480  480 
} 
481  481  
482  482 
let transition_toplevel nd i = 
483 
let tr = 

484 
mk_transition nd.node_id ~i 

485 
(vdecls_to_vals nd.node_inputs) 

486 
[] 

487 
(vdecls_to_vals nd.node_outputs) 

488 
in 

483  489 
{ 
484  490 
tname = nd; 
485  491 
tindex = None; 
...  ...  
487  493 
tlocals = []; 
488  494 
toutputs = nd.node_outputs; 
489  495 
tformula = 
490 
ExistsMem 

491 
( nd.node_id, 

492 
Predicate (ResetCleared nd.node_id), 

493 
mk_transition nd.node_id ~i 

494 
(vdecls_to_vals nd.node_inputs) 

495 
[] 

496 
(vdecls_to_vals nd.node_outputs) ); 

496 
(if fst (get_stateless_status_node nd) then tr 

497 
else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr)); 

497  498 
tfootprint = ISet.empty; 
498  499 
} 
499  500  
...  ...  
542  543  
543  544 
(* Translate equations *) 
544  545 
let ctx, ctx0_s = 
545 
translate_core env nd.node_id equations nd.node_inputs locals 

546 
nd.node_outputs 

546 
translate_core env nd equations nd.node_inputs locals nd.node_outputs 

547  547 
in 
548  548  
549  549 
(* Format.eprintf "ok4@.@?"; *) 
...  ...  
578  578 
let clear_reset = 
579  579 
mkinstr 
580  580 
~instr_spec: 
581 
[ 

582 
mk_memory_pack ~i:0 nd.node_id; 

583 
mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] []; 

584 
] 

581 
((if fst (get_stateless_status_node nd) then [] 

582 
else [ mk_memory_pack ~i:0 nd.node_id ]) 

583 
@ [ 

584 
mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] []; 

585 
]) 

585  586 
MClearReset 
586  587 
in 
587  588 
{ 
Also available in: Unified diff
corrections for stateless nodes