Project

General

Profile

Revision 642e116d src/plugins/salsa/machine_salsa_opt.ml

View differences:

src/plugins/salsa/machine_salsa_opt.ml
80 80

  
81 81

  
82 82
(* Optimize a given expression. It returns another expression and a computed range. *)
83
let optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e : LT.value_t * RangesInt.t option = 
83
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e : LT.value_t * RangesInt.t option = 
84 84
  let rec opt_expr ranges formalEnv e =
85 85
    match e.LT.value_desc with
86 86
    | LT.Cst cst ->
......
127 127

  
128 128
    (* Convert formalEnv *)
129 129
    (* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)
130
    let formalEnv_salsa = 
131
      FormalEnv.fold (fun id expr accu ->
132
	(id, value_t2salsa_expr constEnv expr)::accu
133
		     ) formalEnv []  in
134 130
    (* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)
131

  
132
    Format.eprintf "Expression avant et apres substVars.@.Avant %a@." MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ;  
133

  
135 134
    (* Substitute all occurences of variables by their definition in env *)
136 135
    let (e_salsa: Salsa.Types.expression), _ = 
137 136
      Salsa.Rewrite.substVars 
138 137
	e_salsa
139
	formalEnv_salsa
138
	(FormalEnv.to_salsa constEnv formalEnv)
140 139
	0 (* TODO: Nasrine, what is this integer value for ? *)
141 140
    in
141

  
142
    Format.eprintf "Apres %a@." MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ;  
143

  
142 144
    (* if !debug then Format.eprintf "Substituted def in expr@ "; *)
143 145
    let abstractEnv = Hashtbl.fold 
144 146
      (fun id value accu -> (id,value)::accu) 
......
151 153
       garde evalPartExpr remplace les variables e qui sont dans env par la cst
152 154
       - on garde *)
153 155
    (* if !debug then Format.eprintf "avant avant eval part@ "; *)
154
    (*  Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);  *)
156
     Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);
155 157
    let e_salsa =  
156 158
      Salsa.Analyzer.evalPartExpr 
157 159
	e_salsa
......
159 161
	([] (* no blacklisted variables *))
160 162
	([] (* no arrays *))
161 163
    in
162
     (* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);  *)
164
     Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);
163 165
    (* Checking if we have all necessary information *)
164 166

  
165 167
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
......
168 170
	Vars.pp (Vars.fold (fun v accu -> let v' = {v with LT.var_id = nodename ^ "." ^ v.LT.var_id } in Vars.add v' accu) free_vars Vars.empty)
169 171
	MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));
170 172
      if !debug then Format.eprintf "Some free vars, not optimizing@.";
173
      
171 174
      let new_e = try salsa_expr2value_t vars_env constEnv e_salsa   with Not_found -> assert false in
172 175
      new_e, None
173 176
    )
174 177
    else (
175 178
      
176
      try
179
      try 
177 180
	if !debug then
178
	  Format.eprintf "Analyzing expression %a with env: @[<v>%a@ @]@ "
179
	    MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa)
181
	  Format.eprintf "Analyzing expression %a with env: @[<v>%a@ @]@ @?"
182
	    (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)
180 183
	    (Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv
181 184
	;
182 185

  
186
	(* Slicing it *)
187
	let e_salsa, seq = Salsa.Rewrite.sliceExpr e_salsa 0 (Salsa.Types.Nop(Salsa.Types.Lab 0)) in
188

  
189
	Format.eprintf "Sliced expression %a@.@?"
190
	  (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)
191
	;
192
	
183 193
	let new_e_salsa, e_val = 
184
	  Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv 
194
	  Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
185 195
	in
186 196
    	let new_e = try salsa_expr2value_t vars_env constEnv new_e_salsa   with Not_found -> assert false in
187 197
	if !debug then Format.eprintf "@  @[<v>old: %a@ new: %a@ range: %a@]" MC.pp_val e MC.pp_val new_e RangesInt.pp_val e_val;
188 198
	new_e, Some e_val
189
      with Not_found -> assert false
199
      with (* Not_found ->  *)
190 200
      | Salsa.Epeg_types.EPEGError _ -> (
191 201
	Format.eprintf "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e;
192 202
	e, None
......
209 219
    
210 220
(* Returns a list of assign, for each var in vars_to_print, that produce the
211 221
   definition of it according to formalEnv, and driven by the ranges. *)
212
let assign_vars nodename constEnv vars_env printed_vars ranges formalEnv vars_to_print =
222
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print =
213 223
  (* We print thhe expression in the order of definition *)
214 224

  
215 225
  let ordered_vars = 
......
224 234
      try
225 235
	(* Obtaining unfold expression of v in formalEnv *)
226 236
	let v_def = FormalEnv.get_def formalEnv v  in
227
	let e, r = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv v_def in
237
	let e, r = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv v_def in
228 238
	let instr_desc = 
229 239
	  if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then
230 240
	    LT.MLocalAssign(v, e)
......
244 254
(* Main recursive function: modify the instructions list while preserving the
245 255
   order of assigns for state variables. Returns a quintuple: (new_instrs,
246 256
   ranges, formalEnv, printed_vars, and remaining vars to be printed) *)
247
let rec rewrite_instrs nodename constEnv  vars_env m instrs ranges formalEnv printed_vars vars_to_print =
257
let rec rewrite_instrs nodename m constEnv  vars_env m instrs ranges formalEnv printed_vars vars_to_print =
258
  let formal_env_def = FormalEnv.def constEnv vars_env in
248 259
  Format.eprintf "Rewrite intrs :%a@." Machine_code.pp_instrs instrs;
249
  let assign_vars = assign_vars nodename constEnv vars_env in
250
  (* if !debug then ( *)
251
  (*   Format.eprintf "------------@ "; *)
252
  (*   Format.eprintf "Current printed_vars: [%a]@ " Vars.pp printed_vars; *)
253
  (*   Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)
254
  (* ); *)
260
  let assign_vars = assign_vars nodename m constEnv vars_env in
261
  if !debug then (
262
    Format.eprintf "@.------------@ ";
263
    Format.eprintf "Current printed_vars: [%a]@ " Vars.pp printed_vars;
264
    Format.eprintf "Vars to print: [%a]@ " Vars.pp vars_to_print;
265
    Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv;
266
  );
255 267
  match instrs with
256 268
  | [] -> 
257 269
     (* End of instruction list: we produce the definition of each variable that
......
276 288
	    (* LocalAssign are injected into formalEnv *)
277 289
	    (* if !debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; *)
278 290
	    if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr;
279
	    let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *)
291
	    let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
280 292
	    [],                        (* no instr generated *)
281 293
	    ranges,                    (* no new range computed *)
282 294
	    formalEnv',
......
292 304
	     Format.eprintf "%a@]@ " MC.pp_instr hd_instr;
293 305
	     Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd;
294 306
	   );
295
	   let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *)
307
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
296 308
	    let instrs', ranges' = (* printing vd = optimized vt *)
297 309
	      assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
298 310
	    in
......
302 314
	    Vars.add vd printed_vars,        (* adding vd to new printed vars *)
303 315
	    Vars.remove vd vars_to_print     (* removed vd from variables to print *)
304 316

  
305
	 | LT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print -> 
306
       Format.eprintf "state assign@.";
317
	 | LT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print  *)-> 
318
	    Format.eprintf "state assign of real type@.";
307 319

  
308 320
	    (* StateAssign are produced since they are required by the function. We still
309 321
	     keep their definition in the formalEnv in case it can optimize later
......
313 325
	     Format.eprintf "%a@]@ " MC.pp_instr hd_instr;
314 326
	     Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd;
315 327
	   );
316
	    let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
328
	    let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
317 329
	    let instrs', ranges' = (* printing vd = optimized vt *)
318 330
	      assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
319 331
	    in
......
323 335
	    Vars.add vd printed_vars,        (* adding vd to new printed vars *)
324 336
	    Vars.remove vd vars_to_print     (* removed vd from variables to print *)
325 337

  
326
	 | (LT.MLocalAssign(vd,vt) | LT.MStateAssign(vd,vt)) ->
327
	    Format.eprintf "other assign@.";
338
	 | (LT.MLocalAssign(vd,vt) | LT.MStateAssign(vd,vt))  ->
339
	    Format.eprintf "other assign %a@." MC.pp_instr hd_instr;
328 340

  
329 341
	    (* We have to produce the instruction. But we may have to produce as
330 342
	     well its dependencies *)
......
332 344
	    let required_vars = Vars.diff required_vars printed_vars in (* remove
333 345
									 already
334 346
									 produced
335
									 variables *)
347
									   variables *)
348
	    Format.eprintf "Requited vars: %a@." Vars.pp required_vars;
349
	    let required_vars = Vars.diff required_vars (Vars.of_list m.MC.mmemory) in
336 350
	    let prefix_instr, ranges = 
337 351
	      assign_vars printed_vars ranges formalEnv required_vars in
338 352

  
339
	    let vt', _ = optimize_expr nodename constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in
353
	    let vt', _ = optimize_expr nodename m constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in
340 354
	    let new_instr = 
341 355
	      match Corelang.get_instr_desc hd_instr with
342 356
	      | LT.MLocalAssign _ -> Corelang.update_instr_desc hd_instr (LT.MLocalAssign(vd,vt'))
......
374 388
	    let vtl', vtl_ranges = List.fold_right2 (
375 389
				       fun e typ_e (exprl, range_l)-> 
376 390
				       if Types.is_real_type typ_e then
377
					 let e', r' = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e in
391
					 let e', r' = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e in
378 392
					 e'::exprl, r'::range_l
379 393
				       else 
380 394
					 e::exprl, None::range_l
......
425 439

  
426 440
	    let printed_vars = Vars.union printed_vars required_vars in
427 441

  
428
	    let vt', _ = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv vt in
442
	    let vt', _ = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv vt in
429 443

  
430 444
	    let read_vars_tl = get_read_vars tl_instrs in
431 445
	    if !debug then Format.eprintf "@[<v 2>Dealing with branches@ ";
......
437 451
						       data, we copy it for
438 452
						       each branch *)
439 453
							     let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars = 
440
							       rewrite_instrs nodename constEnv  vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
454
							       rewrite_instrs nodename m constEnv  vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
441 455
							     in
442 456
							     (* b_vars should be empty *)
443 457
							     let _ = if b_vars != [] then assert false in
......
479 493
       let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print = 
480 494
	 rewrite_instrs 
481 495
	   nodename
496
	   m
482 497
	   constEnv 	  
483 498
	   vars_env
484 499
	   m 
......
530 545
	    assert false 
531 546
	in
532 547
	let minv, maxv = get_cst minv, get_cst maxv in
533
	if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv);
548
	let minv, maxv = Num.float_of_num minv, Num.float_of_num  maxv in
549
	(* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv); *)
534 550
	RangesInt.enlarge ranges v (Salsa.Float.Domain.nnew minv maxv)
535 551
      )
536 552
      | _ -> 
......
556 572
  let new_instrs, _, _, printed_vars, _ = 
557 573
    rewrite_instrs
558 574
      m.MC.mname.LT.node_id
575
      m
559 576
      constEnv 
560 577
      vars_env
561 578
      m

Also available in: Unified diff