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