Project

General

Profile

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

View differences:

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