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