lustrec / src / optimize_machine.ml @ a77bd1e3
History  View  Annotate  Download (3.72 KB)
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 outputs 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)) > 
44 
if not (List.mem v outputs) then true, apply elim v e else false, elim 
45 
(* When optimization >= 3, we also inline any basic operator call. 
46 
All those are returning a single ouput *) 
47 
 MStep([v], id, vl) when 
48 
List.mem id Basic_library.internal_funs 
49 
&& !Options.optimization >= 3 
50 
> assert false 
51 
(* true, apply elim v (Fun(id, vl))*) 
52  
53 

54 
 MLocalAssign (v, ((Fun (id, il)) as e)) when 
55 
not (List.mem v outputs) 
56 
&& List.mem id Basic_library.internal_funs (* this will avoid inlining ite *) 
57 
&& !Options.optimization >= 3 
58 
> ( 
59 
(* Format.eprintf "WE STORE THE EXPRESSION DEFINING %s TO ELIMINATE IT@." v.var_id; *) 
60 
true, apply elim v e 
61 
) 
62 
 _ > 
63 
(* default case, we keep the instruction and do not modify elim *) 
64 
false, elim 
65 

66  
67 
(** We iterate in the order, recording simple local assigns in an accumulator 
68 
1. each expression is rewritten according to the accumulator 
69 
2. local assigns then rewrite occurrences of the lhs in the computed accumulator 
70 
*) 
71 
let optimize_minstrs outputs instrs = 
72 
let rev_instrs, eliminate = 
73 
List.fold_left (fun (rinstrs, elim) instr > 
74 
(* each subexpression in instr that could be rewritten by the elim set is 
75 
rewritten *) 
76 
let instr = eliminate elim instr in 
77 
(* if instr is a simple local assign, then (a) elim is simplified with it (b) it 
78 
is stored as the elim set *) 
79 
let remove, elim = update_elim outputs elim instr in 
80 
(if remove then rinstrs else instr::rinstrs), elim 
81 
) ([],[]) instrs 
82 
in 
83 
let eliminated_vars = List.map fst eliminate in 
84 
eliminated_vars, List.rev rev_instrs 
85  
86 
(** Perform optimization on machine code: 
87 
 iterate through step instructions and remove simple local assigns 
88 

89 
*) 
90 
let optimize_machine machine = 
91 
let eliminated_vars, new_instrs = optimize_minstrs machine.mstep.step_outputs machine.mstep.step_instrs in 
92 
let new_locals = 
93 
List.filter (fun v > not (List.mem v eliminated_vars)) machine.mstep.step_locals 
94 
in 
95 
{ 
96 
machine with 
97 
mstep = { 
98 
machine.mstep with 
99 
step_locals = new_locals; 
100 
step_instrs = new_instrs 
101 
} 
102 
} 
103 

104  
105  
106 
let optimize_machines machines = 
107 
List.map optimize_machine machines 
108  
109  
110 
(* Local Variables: *) 
111 
(* compilecommand:"make C .." *) 
112 
(* End: *) 