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

28  28 
let rec eliminate m elim instr = 
29  29 
let e_expr = eliminate_expr m elim in 
30  30 
match get_instr_desc instr with 
31 
 MSpec _  MComment _ > instr 

32  31 
 MLocalAssign (i,v) > update_instr_desc instr (MLocalAssign (i, e_expr v)) 
33  32 
 MStateAssign (i,v) > update_instr_desc instr (MStateAssign (i, e_expr v)) 
34 
 MReset _ > instr 

35 
 MNoReset _ > instr 

33 
 MSetReset _ 

34 
 MNoReset _ 

35 
 MClearReset 

36 
 MSpec _ 

37 
 MComment _ > instr 

36  38 
 MStep (il, i, vl) > update_instr_desc instr (MStep(il, i, List.map e_expr vl)) 
37  39 
 MBranch (g,hl) > 
38  40 
update_instr_desc instr ( 
...  ...  
115  117 
match get_instr_desc instr with 
116  118 
 MLocalAssign (v, expr) > update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr)) 
117  119 
 MStateAssign (v, expr) > update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr)) 
118 
 MReset _ > instr 

119 
 MNoReset _ > instr 

120 
 MSetReset _ 

121 
 MNoReset _ 

122 
 MClearReset 

123 
 MSpec _ 

124 
 MComment _ > instr 

120  125 
 MStep (outputs, id, inputs) > update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs)) 
121  126 
 MBranch (cond, brl) 
122  127 
> update_instr_desc instr ( 
123  128 
MBranch(simplify_expr_offset m cond, List.map (fun (l, il) > l, simplify_instrs_offset m il) brl) 
124  129 
) 
125 
 MSpec _  MComment _ > instr 

126  130  
127  131 
and simplify_instrs_offset m instrs = 
128  132 
List.map (simplify_instr_offset m) instrs 
...  ...  
284  288 
let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in 
285  289 
mkinstr 
286  290 
~lustre_eq 
287 
True 

288  291 
(MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type)) 
289  292  
290  293 
(* We do not perform this optimization on contract nodes since there 
...  ...  
499  502  
500  503 
let rec instr_replace_var fvar instr cont = 
501  504 
match get_instr_desc instr with 
502 
 MSpec _  MComment _ > instr_cons instr cont 

503  505 
 MLocalAssign (i, v) > instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont 
504  506 
 MStateAssign (i, v) > instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont 
505 
 MReset _ > instr_cons instr cont 

506 
 MNoReset _ > instr_cons instr cont 

507 
 MSetReset _ 

508 
 MNoReset _ 

509 
 MClearReset 

510 
 MSpec _ 

511 
 MComment _ > instr_cons instr cont 

507  512 
 MStep (il, i, vl) > instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont 
508  513 
 MBranch (g, hl) > instr_cons (update_instr_desc instr (MBranch (value_replace_var fvar g, List.map (fun (h, il) > (h, instrs_replace_var fvar il [])) hl))) cont 
509  514  
...  ...  
763  768 
in 
764  769  
765  770  
766 
prog, List.rev machine_code


771 
prog, machine_code


767  772  
768  773 

769  774 
(* Local Variables: *) 
Also available in: Unified diff
work on spec generation almost done