
1 
open LustreSpec


2 
open Corelang


3 
open Machine_code


4 


5 
let rec eliminate elim instr =


6 
let e_expr = eliminate_expr elim in


7 
match instr with


8 
 MLocalAssign (i,v) > MLocalAssign (i, e_expr v)


9 
 MStateAssign (i,v) > MStateAssign (i, e_expr v)


10 
 MReset i > instr


11 
 MStep (il, i, vl) > MStep(il, i, List.map e_expr vl)


12 
 MBranch (g,hl) >


13 
MBranch


14 
(e_expr g,


15 
(List.map


16 
(fun (l, il) > l, List.map (eliminate elim) il)


17 
hl


18 
)


19 
)


20 


21 
and eliminate_expr elim expr =


22 
match expr with


23 
 LocalVar v > if List.mem_assoc v elim then List.assoc v elim else expr


24 
 Fun (id, vl) > Fun (id, List.map (eliminate_expr elim) vl)


25 
 Array(vl) > Array(List.map (eliminate_expr elim) vl)


26 
 Access(v1, v2) > Access(eliminate_expr elim v1, eliminate_expr elim v2)


27 
 Power(v1, v2) > Access(eliminate_expr elim v1, eliminate_expr elim v2)


28 
 Cst _  StateVar _ > expr


29 


30 
(* see if elim has to take in account the provided instr:


31 
if so, upodate elim and return the remove flag,


32 
otherwise, the expression should be kept and elim is left untouched *)


33 
let update_elim elim instr =


34 
Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;


35 


36 
let apply elim v new_e =


37 
(v, new_e)::List.map (fun (v, e) > v, eliminate_expr [v, new_e] e) elim


38 
in


39 
match instr with


40 
(* Simple cases*)


41 
 MLocalAssign (v, (Cst _ as e))


42 
 MLocalAssign (v, (LocalVar _ as e))


43 
 MLocalAssign (v, (StateVar _ as e)) > true, apply elim v e


44 
(* When optimization >= 3, we also inline any basic operator call.


45 
All those are returning a single ouput *)


46 
 MStep([v], id, vl) when


47 
List.mem id Basic_library.internal_funs


48 
&& !Options.optimization >= 3


49 
> assert false


50 
(* true, apply elim v (Fun(id, vl))*)


51 


52 


53 
 MLocalAssign (v, ((Fun (id, il)) as e)) when


54 
List.mem id Basic_library.internal_funs (* this will avoid inlining ite *)


55 
&& !Options.optimization >= 3


56 
> (


57 
Format.eprintf "WE STORE THE EXPRESSION DEFINING %s TO ELIMINATE IT@." v.var_id;


58 
true, apply elim v e


59 
)


60 
 _ >


61 
(* default case, we keep the instruction and do not modify elim *)


62 
false, elim


63 


64 


65 
(** We iterate in the order, recording simple local assigns in an accumulator


66 
1. each expression is rewritten according to the accumulator


67 
2. local assigns then rewrite occurrences of the lhs in the computed accumulator


68 
*)


69 
let optimize_minstrs instrs =


70 
let rev_instrs, eliminate =


71 
List.fold_left (fun (rinstrs, elim) instr >


72 
(* each subexpression in instr that could be rewritten by the elim set is


73 
rewritten *)


74 
let instr = eliminate elim instr in


75 
(* if instr is a simple local assign, then (a) elim is simplified with it (b) it


76 
is stored as the elim set *)


77 
let remove, elim = update_elim elim instr in


78 
(if remove then rinstrs else instr::rinstrs), elim


79 
) ([],[]) instrs


80 
in


81 
let eliminated_vars = List.map fst eliminate in


82 
eliminated_vars, List.rev rev_instrs


83 


84 
(** Perform optimization on machine code:


85 
 iterate through step instructions and remove simple local assigns


86 


87 
*)


88 
let optimize_machine machine =


89 
let eliminated_vars, new_instrs = optimize_minstrs machine.mstep.step_instrs in


90 
let new_locals =


91 
List.filter (fun v > not (List.mem v eliminated_vars)) machine.mstep.step_locals


92 
in


93 
{


94 
machine with


95 
mstep = {


96 
machine.mstep with


97 
step_locals = new_locals;


98 
step_instrs = new_instrs


99 
}


100 
}


101 


102 


103 


104 
let optimize_machines machines =


105 
List.map optimize_machine machines


106 


107 


108 
(* Local Variables: *)


109 
(* compilecommand:"make C .." *)


110 
(* End: *)
