Revision 0406ab94
Added by LĂ©lio Brun 7 months ago
src/optimize_machine.ml  

11  11  
12  12 
open Utils 
13  13 
open Lustre_types 
14 
open Spec_types 

14  15 
open Machine_code_types 
15  16 
open Corelang 
16  17 
open Causality 
...  ...  
597  598 
 Power (v, n) > 
598  599 
{ value with value_desc = Power (value_replace_var fvar v, n) } 
599  600  
600 
let rec instr_replace_var fvar instr cont = 

601 
match get_instr_desc instr with 

602 
 MLocalAssign (i, v) > 

603 
instr_cons 

604 
(update_instr_desc instr 

605 
(MLocalAssign (fvar i, value_replace_var fvar v))) 

606 
cont 

607 
 MStateAssign (i, v) > 

608 
instr_cons 

609 
(update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) 

610 
cont 

611 
 MSetReset _ 

612 
 MNoReset _ 

613 
 MClearReset 

614 
 MResetAssign _ 

615 
 MSpec _ 

616 
 MComment _ > 

617 
instr_cons instr cont 

618 
 MStep (il, i, vl) > 

619 
instr_cons 

620 
(update_instr_desc instr 

621 
(MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) 

622 
cont 

623 
 MBranch (g, hl) > 

624 
instr_cons 

625 
(update_instr_desc instr 

626 
(MBranch 

627 
( value_replace_var fvar g, 

628 
List.map (fun (h, il) > h, instrs_replace_var fvar il []) hl ))) 

629 
cont 

601 
let expr_spec_replace : 

602 
type a. 

603 
(var_decl > var_decl) > 

604 
(value_t, a) expression_t > 

605 
(value_t, a) expression_t = 

606 
fun fvar > function 

607 
 Val v > 

608 
Val (value_replace_var fvar v) 

609 
 Var v > 

610 
Var (fvar v) 

611 
 e > 

612 
e 

613  
614 
let predicate_spec_replace fvar = function 

615 
 Transition (f, inst, i, vars, r, mems, insts) > 

616 
Transition 

617 
(f, inst, i, List.map (expr_spec_replace fvar) vars, r, mems, insts) 

618 
 p > 

619 
p 

620  
621 
let rec instr_spec_replace fvar = 

622 
let aux instr = instr_spec_replace fvar instr in 

623 
function 

624 
 Equal (e1, e2) > 

625 
Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2) 

626 
 And f > 

627 
And (List.map aux f) 

628 
 Or f > 

629 
Or (List.map aux f) 

630 
 Imply (a, b) > 

631 
Imply (aux a, aux b) 

632 
 Exists (xs, a) > 

633 
let fvar v = if List.mem v xs then v else fvar v in 

634 
Exists (xs, instr_spec_replace fvar a) 

635 
 Forall (xs, a) > 

636 
let fvar v = if List.mem v xs then v else fvar v in 

637 
Forall (xs, instr_spec_replace fvar a) 

638 
 Ternary (e, a, b) > 

639 
Ternary (expr_spec_replace fvar e, aux a, aux b) 

640 
 Predicate p > 

641 
Predicate (predicate_spec_replace fvar p) 

642 
 ExistsMem (f, a, b) > 

643 
ExistsMem (f, aux a, aux b) 

644 
 f > 

645 
f 

646  
647 
let rec instr_replace_var fvar instr = 

648 
let instr_desc = 

649 
match instr.instr_desc with 

650 
 MLocalAssign (i, v) > 

651 
MLocalAssign (fvar i, value_replace_var fvar v) 

652 
 MStateAssign (i, v) > 

653 
MStateAssign (i, value_replace_var fvar v) 

654 
 MStep (il, i, vl) > 

655 
MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl) 

656 
 MBranch (g, hl) > 

657 
MBranch 

658 
( value_replace_var fvar g, 

659 
List.map (fun (h, il) > h, instrs_replace_var fvar il []) hl ) 

660 
 MSetReset _ 

661 
 MNoReset _ 

662 
 MClearReset 

663 
 MResetAssign _ 

664 
 MSpec _ 

665 
 MComment _ > 

666 
instr.instr_desc 

667 
in 

668 
let instr_spec = List.map (instr_spec_replace fvar) instr.instr_spec in 

669 
instr_cons { instr with instr_desc; instr_spec } 

630  670  
631  671 
and instrs_replace_var fvar instrs cont = 
632  672 
List.fold_right (instr_replace_var fvar) instrs cont 
...  ...  
657  697 
let machine_replace_variables fvar m = 
658  698 
{ m with mstep = step_replace_var fvar m.mstep } 
659  699  
660 
let machine_reuse_variables m reuse =


700 
let machine_reuse_variables reuse m =


661  701 
let fvar v = try Hashtbl.find reuse v.var_id with Not_found > v in 
662  702 
machine_replace_variables fvar m 
663  703  
664 
let machines_reuse_variables prog reuse_tables = 

665 
List.map 

666 
(fun m > 

667 
machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables)) 

668 
prog 

704 
let machines_reuse_variables reuse_tables = 

705 
List.map (fun m > 

706 
machine_reuse_variables (Utils.IMap.find m.mname.node_id reuse_tables) m) 

669  707  
670  708 
let rec instr_assign res instr = 
671  709 
match get_instr_desc instr with 
...  ...  
723  761 
i1 :: instrs_reduce branches (i2 :: q) cont 
724  762  
725  763 
let rec instrs_fusion instrs = 
726 
match instrs, List.map get_instr_desc instrs with


727 
 [], []  [ _ ], [ _ ] >


764 
match instrs with 

765 
 []  [ _ ] >


728  766 
instrs 
729 
 i1 :: _ :: q, _ :: MBranch ({ value_desc = Var v; _ }, hl) :: _ 

730 
when instr_constant_assign v i1 > 

731 
instr_reduce 

732 
(List.map (fun (h, b) > h, instrs_fusion b) hl) 

733 
i1 (instrs_fusion q) 

734 
 i1 :: i2 :: q, _ > 

735 
i1 :: instrs_fusion (i2 :: q) 

736 
 _ > 

737 
assert false 

738 
(* Other cases should not happen since both lists are of same size *) 

767 
 i1 :: i2 :: q > ( 

768 
match i2.instr_desc with 

769 
 MBranch ({ value_desc = Var v; _ }, hl) when instr_constant_assign v i1 > 

770 
instr_reduce 

771 
(List.map (fun (h, b) > h, instrs_fusion b) hl) 

772 
{ i1 with instr_spec = i1.instr_spec @ i2.instr_spec } 

773 
(instrs_fusion q) 

774 
 _ > 

775 
i1 :: instrs_fusion (i2 :: q)) 

739  776  
740  777 
let step_fusion step = 
741  778 
{ step with step_instrs = instrs_fusion step.step_instrs } 
...  ...  
897  934 
Scheduling.remove_prog_inlined_locals removed_table node_schs 
898  935 
in 
899  936 
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in 
900 
machines_fusion (machines_reuse_variables machine_code reuse_tables))


937 
machines_fusion (machines_reuse_variables reuse_tables machine_code))


901  938 
else machine_code 
902  939 
in 
903  940 
Also available in: Unified diff
implement optimization on spec: IT WORKS