Revision 3ca27bc7 src/plugins/salsa/machine_salsa_opt.ml
src/plugins/salsa/machine_salsa_opt.ml  

48  48 
[] > Vars.empty 
49  49 
 i::tl > ( 
50  50 
let vars_tl = get_read_vars tl in 
51 
match i with 

51 
match Corelang.get_instr_desc i with


52  52 
 LT.MLocalAssign(_,e) 
53  53 
 LT.MStateAssign(_,e) > Vars.union (get_expr_real_vars e) vars_tl 
54  54 
 LT.MStep(_, _, el) > List.fold_left (fun accu e > Vars.union (get_expr_real_vars e) accu) vars_tl el 
...  ...  
66  66 
[] > Vars.empty 
67  67 
 i::tl > ( 
68  68 
let vars_tl = get_written_vars tl in 
69 
match i with 

69 
match Corelang.get_instr_desc i with


70  70 
 LT.MLocalAssign(v,_) 
71  71 
 LT.MStateAssign(v,_) > Vars.add v vars_tl 
72  72 
 LT.MStep(vdl, _, _) > List.fold_left (fun accu v > Vars.add v accu) vars_tl vdl 
...  ...  
224  224 
(* Obtaining unfold expression of v in formalEnv *) 
225  225 
let v_def = FormalEnv.get_def formalEnv v in 
226  226 
let e, r = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv v_def in 
227 
let instr = 

227 
let instr_desc =


228  228 
if try (get_var vars_env v.LT.var_id).is_local with Not_found > assert false then 
229  229 
LT.MLocalAssign(v, e) 
230  230 
else 
231  231 
LT.MStateAssign(v, e) 
232  232 
in 
233 
instr::accu_instr,


233 
(Corelang.mkinstr instr_desc)::accu_instr,


234  234 
(match r with 
235  235 
 None > ranges 
236  236 
 Some v_r > RangesInt.add_def ranges v.LT.var_id v_r) 
...  ...  
267  267 
formalEnv, possibly ranges and vars_to_print *) 
268  268 
begin 
269  269 
let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print = 
270 
match hd_instr with 

270 
match Corelang.get_instr_desc hd_instr with


271  271 
 LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && not (Vars.mem vd vars_to_print) > 
272  272 
(* LocalAssign are injected into formalEnv *) 
273  273 
if debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; 
...  ...  
319  319 
assign_vars printed_vars ranges formalEnv required_vars in 
320  320 
let vt', _ = optimize_expr nodename constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in 
321  321 
let new_instr = 
322 
match hd_instr with 

323 
 LT.MLocalAssign _ > LT.MLocalAssign(vd,vt')


324 
 _ > LT.MStateAssign(vd,vt')


322 
match Corelang.get_instr_desc hd_instr with


323 
 LT.MLocalAssign _ > Corelang.update_instr_desc hd_instr (LT.MLocalAssign(vd,vt'))


324 
 _ > Corelang.update_instr_desc hd_instr (LT.MStateAssign(vd,vt'))


325  325 
in 
326  326 
let written_vars = Vars.add vd required_vars in 
327  327 
prefix_instr@[new_instr], 
...  ...  
382  382 
variables *) 
383  383 
let written_vars = Vars.union required_vars (Vars.of_list vdl) in 
384  384 
let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in 
385 
instrs' @ [LT.MStep(vdl,id,vtl')], (* New instrs *)


385 
instrs' @ [Corelang.update_instr_desc hd_instr (LT.MStep(vdl,id,vtl'))], (* New instrs *)


386  386 
RangesInt.add_call ranges' vdl id vtl_ranges, (* add information bounding each vdl var *) 
387  387 
formalEnv, 
388  388 
Vars.union written_vars printed_vars, (* adding vdl to new printed vars *) 
...  ...  
430  430 

431  431 
) branches ([], required_vars, ranges) in 
432  432 
if debug then Format.eprintf "dealing with branches done@ @]@ "; 
433 
prefix_instr@[LT.MBranch(vt', branches')],


433 
prefix_instr@[Corelang.update_instr_desc hd_instr (LT.MBranch(vt', branches'))],


434  434 
merged_ranges, (* Only step functions call within branches 
435  435 
may have produced new ranges. We merge this data by 
436  436 
computing the join per variable *) 
Also available in: Unified diff