Revision 3ca27bc7 src/optimize_machine.ml
src/optimize_machine.ml  

26  26  
27  27 
let rec eliminate elim instr = 
28  28 
let e_expr = eliminate_expr elim in 
29 
match instr with 

29 
match get_instr_desc instr with


30  30 
 MComment _ > instr 
31 
 MLocalAssign (i,v) > MLocalAssign (i, e_expr v)


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


31 
 MLocalAssign (i,v) > update_instr_desc instr (MLocalAssign (i, e_expr v))


32 
 MStateAssign (i,v) > update_instr_desc instr (MStateAssign (i, e_expr v))


33  33 
 MReset i > instr 
34  34 
 MNoReset i > instr 
35 
 MStep (il, i, vl) > MStep(il, i, List.map e_expr vl)


35 
 MStep (il, i, vl) > update_instr_desc instr (MStep(il, i, List.map e_expr vl))


36  36 
 MBranch (g,hl) > 
37 
MBranch 

38 
(e_expr g, 

39 
(List.map 

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

41 
hl 

42 
) 

43 
) 

37 
update_instr_desc instr ( 

38 
MBranch 

39 
(e_expr g, 

40 
(List.map 

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

42 
hl 

43 
) 

44 
) 

45 
) 

44  46 

45  47 
and eliminate_expr elim expr = 
46  48 
match expr.value_desc with 
...  ...  
106  108 
in simplify [] expr 
107  109  
108  110 
let rec simplify_instr_offset m instr = 
109 
match instr with 

110 
 MLocalAssign (v, expr) > MLocalAssign (v, simplify_expr_offset m expr)


111 
 MStateAssign (v, expr) > MStateAssign (v, simplify_expr_offset m expr)


111 
match get_instr_desc instr with


112 
 MLocalAssign (v, expr) > update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))


113 
 MStateAssign (v, expr) > update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))


112  114 
 MReset id > instr 
113  115 
 MNoReset id > instr 
114 
 MStep (outputs, id, inputs) > MStep (outputs, id, List.map (simplify_expr_offset m) inputs)


116 
 MStep (outputs, id, inputs) > update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))


115  117 
 MBranch (cond, brl) 
116 
> MBranch(simplify_expr_offset m cond, List.map (fun (l, il) > l, simplify_instrs_offset m il) brl) 

118 
> update_instr_desc instr ( 

119 
MBranch(simplify_expr_offset m cond, List.map (fun (l, il) > l, simplify_instrs_offset m il) brl) 

120 
) 

117  121 
 MComment _ > instr 
118  122  
119  123 
and simplify_instrs_offset m instrs = 
...  ...  
197  201  
198  202 
and instr_unfold fanin instrs elim instr = 
199  203 
(* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*) 
200 
match instr with 

204 
match get_instr_desc instr with


201  205 
(* Simple cases*) 
202  206 
 MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type) 
203 
> instr_unfold fanin instrs elim (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))


207 
> instr_unfold fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))


204  208 
 MLocalAssign(v, expr) when unfoldable_assign fanin v expr 
205  209 
> (IMap.add v.var_id expr elim, instrs) 
206  210 
 MBranch(g, hl) when false 
...  ...  
209  213 
List.fold_right 
210  214 
(fun (h, (e, l)) (elim, branches) > (merge_elim elim e, (h, l)::branches)) 
211  215 
elim_branches (elim, []) 
212 
in elim, (MBranch (g, branches) :: instrs)


216 
in elim, ((update_instr_desc instr (MBranch (g, branches))) :: instrs)


213  217 
 _ 
214  218 
> (elim, instr :: instrs) 
215  219 
(* default case, we keep the instruction and do not modify elim *) 
...  ...  
259  263 
let const = const_of_top top_const in 
260  264 
let vdecl = mkvar_decl Location.dummy_loc (const.const_id, mktyp Location.dummy_loc Tydec_any, mkclock Location.dummy_loc Ckdec_any, true, None) in 
261  265 
let vdecl = { vdecl with var_type = const.const_type } 
262 
in MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type)


266 
in mkinstr (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))


263  267  
264  268 
let machines_unfold consts node_schs machines = 
265  269 
List.fold_right (fun m (machines, removed) > 
...  ...  
272  276 
([], IMap.empty) 
273  277  
274  278 
let get_assign_lhs instr = 
275 
match instr with 

279 
match get_instr_desc instr with


276  280 
 MLocalAssign(v, e) > mk_val (LocalVar v) e.value_type 
277  281 
 MStateAssign(v, e) > mk_val (StateVar v) e.value_type 
278  282 
 _ > assert false 
279  283  
280  284 
let get_assign_rhs instr = 
281 
match instr with 

285 
match get_instr_desc instr with


282  286 
 MLocalAssign(_, e) 
283  287 
 MStateAssign(_, e) > e 
284  288 
 _ > assert false 
285  289  
286  290 
let is_assign instr = 
287 
match instr with 

291 
match get_instr_desc instr with


288  292 
 MLocalAssign _ 
289  293 
 MStateAssign _ > true 
290  294 
 _ > false 
...  ...  
296  300 
 _ > assert false 
297  301  
298  302 
let rec assigns_instr instr assign = 
299 
match instr with 

303 
match get_instr_desc instr with


300  304 
 MLocalAssign (i,_) 
301  305 
 MStateAssign (i,_) > ISet.add i assign 
302  306 
 MStep (ol, _, _) > List.fold_right ISet.add ol assign 
...  ...  
359  363 
let lhs = get_assign_lhs instr' in 
360  364 
(match lhs.value_desc with 
361  365 
 LocalVar v' > 
362 
let instr = eliminate subst (mk_assign v lhs) in


366 
let instr = eliminate subst (update_instr_desc instr (mk_assign v lhs)) in


363  367 
subst, instr :: instrs 
364  368 
 StateVar stv' > 
365  369 
let subst_v' = IMap.add stv'.var_id v IMap.empty in 
...  ...  
377  381 
 [instr] : current instruction, normalized by [subst] 
378  382 
*) 
379  383 
let rec instr_cse (subst, instrs) instr = 
380 
match instr with 

384 
match get_instr_desc instr with


381  385 
(* Simple cases*) 
382  386 
 MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v > v.value_type) vl) 
383 
> instr_cse (subst, instrs) (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))


387 
> instr_cse (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))


384  388 
 MLocalAssign(v, expr) when is_unfoldable_expr 2 expr 
385  389 
> (IMap.add v.var_id expr subst, instr :: instrs) 
386  390 
 _ when is_assign instr 
...  ...  
421  425  
422  426 
(* checks whether an [instr] is skip and can be removed from program *) 
423  427 
let rec instr_is_skip instr = 
424 
match instr with 

428 
match get_instr_desc instr with


425  429 
 MLocalAssign (i, { value_desc = (LocalVar v) ; _}) when i = v > true 
426  430 
 MStateAssign (i, { value_desc = StateVar v; _}) when i = v > true 
427  431 
 MBranch (g, hl) > List.for_all (fun (_, il) > instrs_are_skip il) hl 
...  ...  
433  437 
if instr_is_skip instr then cont else instr::cont 
434  438  
435  439 
let rec instr_remove_skip instr cont = 
436 
match instr with 

440 
match get_instr_desc instr with


437  441 
 MLocalAssign (i, { value_desc = LocalVar v; _ }) when i = v > cont 
438  442 
 MStateAssign (i, { value_desc = StateVar v; _ }) when i = v > cont 
439 
 MBranch (g, hl) > MBranch (g, List.map (fun (h, il) > (h, instrs_remove_skip il [])) hl) :: cont


443 
 MBranch (g, hl) > update_instr_desc instr (MBranch (g, List.map (fun (h, il) > (h, instrs_remove_skip il [])) hl)) :: cont


440  444 
 _ > instr::cont 
441  445  
442  446 
and instrs_remove_skip instrs cont = 
...  ...  
453  457 
 Power (v, n) > { value with value_desc = Power(value_replace_var fvar v, n)} 
454  458  
455  459 
let rec instr_replace_var fvar instr cont = 
456 
match instr with 

460 
match get_instr_desc instr with


457  461 
 MComment _ > instr_cons instr cont 
458 
 MLocalAssign (i, v) > instr_cons (MLocalAssign (fvar i, value_replace_var fvar v)) cont


459 
 MStateAssign (i, v) > instr_cons (MStateAssign (i, value_replace_var fvar v)) cont


462 
 MLocalAssign (i, v) > instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont


463 
 MStateAssign (i, v) > instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont


460  464 
 MReset i > instr_cons instr cont 
461  465 
 MNoReset i > instr_cons instr cont 
462 
 MStep (il, i, vl) > instr_cons (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)) cont


463 
 MBranch (g, hl) > instr_cons (MBranch (value_replace_var fvar g, List.map (fun (h, il) > (h, instrs_replace_var fvar il [])) hl)) cont


466 
 MStep (il, i, vl) > instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont


467 
 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


464  468  
465  469 
and instrs_replace_var fvar instrs cont = 
466  470 
List.fold_right (instr_replace_var fvar) instrs cont 
...  ...  
504  508 
) prog 
505  509  
506  510 
let rec instr_assign res instr = 
507 
match instr with 

511 
match get_instr_desc instr with


508  512 
 MLocalAssign (i, _) > Disjunction.CISet.add i res 
509  513 
 MStateAssign (i, _) > Disjunction.CISet.add i res 
510  514 
 MBranch (g, hl) > List.fold_left (fun res (h, b) > instrs_assign res b) res hl 
...  ...  
515  519 
List.fold_left instr_assign res instrs 
516  520  
517  521 
let rec instr_constant_assign var instr = 
518 
match instr with 

522 
match get_instr_desc instr with


519  523 
 MLocalAssign (i, { value_desc = Cst (Const_tag _); _ }) 
520  524 
 MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) > i = var 
521  525 
 MBranch (g, hl) > List.for_all (fun (h, b) > instrs_constant_assign var b) hl 
...  ...  
525  529 
List.fold_left (fun res i > if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then instr_constant_assign var i else res) false instrs 
526  530  
527  531 
let rec instr_reduce branches instr1 cont = 
528 
match instr1 with 

532 
match get_instr_desc instr1 with


529  533 
 MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) > instr1 :: (List.assoc c branches @ cont) 
530  534 
 MStateAssign (_, { value_desc = Cst (Const_tag c); _}) > instr1 :: (List.assoc c branches @ cont) 
531 
 MBranch (g, hl) > MBranch (g, List.map (fun (h, b) > (h, instrs_reduce branches b [])) hl) :: cont


535 
 MBranch (g, hl) > (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) > (h, instrs_reduce branches b [])) hl))) :: cont


532  536 
 _ > instr1 :: cont 
533  537  
534  538 
and instrs_reduce branches instrs cont = 
...  ...  
538  542 
 i1::i2::q > i1 :: instrs_reduce branches (i2::q) cont 
539  543  
540  544 
let rec instrs_fusion instrs = 
541 
match instrs with 

542 
 [] 

543 
 [_] > 

545 
match instrs, List.map get_instr_desc instrs with


546 
 [], []


547 
 [_], [_] >


544  548 
instrs 
545 
 i1::(MBranch ({ value_desc = LocalVar v; _}, hl))::q when instr_constant_assign v i1 >


549 
 i1::i2::q, i1_desc::(MBranch ({ value_desc = LocalVar v; _}, hl))::q_desc when instr_constant_assign v i1 >


546  550 
instr_reduce (List.map (fun (h, b) > h, instrs_fusion b) hl) i1 (instrs_fusion q) 
547 
 i1::(MBranch ({ value_desc = StateVar v; _}, hl))::q when instr_constant_assign v i1 >


551 
 i1::i2::q, i1_desc::(MBranch ({ value_desc = StateVar v; _}, hl))::q_desc when instr_constant_assign v i1 >


548  552 
instr_reduce (List.map (fun (h, b) > h, instrs_fusion b) hl) i1 (instrs_fusion q) 
549 
 i1::i2::q > 

553 
 i1::i2::q, _ >


550  554 
i1 :: instrs_fusion (i2::q) 
551  
555 
 _ > assert false (* Other cases should not happen since both lists are of same size *) 

556 


552  557 
let step_fusion step = 
553  558 
{ step with 
554  559 
step_instrs = instrs_fusion step.step_instrs; 
Also available in: Unified diff