Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / plugins / salsa / machine_salsa_opt.ml @ 53206908

History | View | Annotate | Download (22.7 KB)

1

    
2
(* We try to avoid opening modules here *)
3
module ST = Salsa.SalsaTypes
4
module SDT = SalsaDatatypes
5
module LT = LustreSpec
6
module MC = Machine_code
7

    
8
(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *)
9
open SalsaDatatypes
10
(******************************************************************)
11
(* TODO Xavier: should those functions be declared more globally? *)
12

    
13
let fun_types node = 
14
  try
15
    match node.LT.top_decl_desc with 
16
    | LT.Node nd -> 
17
      let tin, tout = Types.split_arrow nd.LT.node_type in
18
      Types.type_list_of_type tin, Types.type_list_of_type tout
19
    | _ -> Format.eprintf "%a is not a node@.@?" Printers.pp_decl node; assert false
20
  with Not_found -> Format.eprintf "Unable to find type def for function %s@.@?" (Corelang.node_name node); assert false
21

    
22
let called_node_id m id = 
23
  let td, _ =
24
    try
25
      List.assoc id m.MC.mcalls (* TODO Xavier: mcalls or minstances ? *)
26
    with Not_found -> assert false
27
  in
28
  td
29
(******************************************************************)    
30

    
31
(* Returns the set of vars that appear in the expression *)
32
let rec get_expr_real_vars e = 
33
  match e.LT.value_desc with
34
  | LT.LocalVar v | LT.StateVar v when Types.is_real_type v.LT.var_type -> Vars.singleton v
35
  | LT.LocalVar _| LT.StateVar _
36
  | LT.Cst _ -> Vars.empty 
37
  | LT.Fun (_, args) -> 
38
    List.fold_left 
39
      (fun acc e -> Vars.union acc (get_expr_real_vars e)) 
40
      Vars.empty args
41
  | LT.Array _
42
  | LT.Access _
43
  | LT.Power _ -> assert false 
44

    
45
(* Extract the variables to appear as free variables in expressions (lhs) *)
46
let rec get_read_vars instrs =
47
  match instrs with
48
    [] -> Vars.empty
49
  | i::tl -> (
50
    let vars_tl = get_read_vars tl in 
51
    match i with
52
    | LT.MLocalAssign(_,e) 
53
    | LT.MStateAssign(_,e) -> Vars.union (get_expr_real_vars e) vars_tl
54
    | LT.MStep(_, _, el) -> List.fold_left (fun accu e -> Vars.union (get_expr_real_vars e) accu) vars_tl el
55
    | LT.MBranch(e, branches) -> (
56
      let vars = Vars.union (get_expr_real_vars e) vars_tl in
57
      List.fold_left (fun vars (_, b) -> Vars.union vars (get_read_vars b) ) vars branches
58
    )
59
    | LT.MReset _ 
60
    | LT.MComment _ -> Vars.empty  
61
  )
62

    
63
let rec get_written_vars instrs =
64
  match instrs with
65
    [] -> Vars.empty
66
  | i::tl -> (
67
    let vars_tl = get_written_vars tl in 
68
    match i with
69
    | LT.MLocalAssign(v,_) 
70
    | LT.MStateAssign(v,_) -> Vars.add v vars_tl 
71
    | LT.MStep(vdl, _, _) -> List.fold_left (fun accu v -> Vars.add v accu) vars_tl vdl
72
    | LT.MBranch(_, branches) -> (
73
      List.fold_left (fun vars (_, b) -> Vars.union vars (get_written_vars b) ) vars_tl branches
74
    )
75
    | LT.MReset _ 
76
    | LT.MComment _ -> Vars.empty    
77
  )
78

    
79

    
80
(* Optimize a given expression. It returns another expression and a computed range. *)
81
let optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e : LT.value_t * RangesInt.t option = 
82
  let rec opt_expr ranges formalEnv e =
83
    match e.LT.value_desc with
84
    | LT.Cst cst ->
85
      Format.eprintf "optmizing constant expr ? @ ";
86
      (* the expression is a constant, we optimize it directly if it is a real
87
  	 constant *)
88
      let typ = Typing.type_const Location.dummy_loc cst in
89
      if Types.is_real_type typ then 
90
	opt_num_expr ranges formalEnv e 
91
      else e, None
92
    | LT.LocalVar v
93
    | LT.StateVar v -> 
94
      if not (Vars.mem v printed_vars) && 
95
	(* TODO xAvier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *)
96
	(Types.is_real_type e.LT.value_type ||  Types.is_real_type v.LT.var_type) 
97
      then
98
	opt_num_expr ranges formalEnv e 
99
      else 
100
	e, None  (* Nothing to optimize for expressions containing a single non real variable *)
101
    (* (\* optimize only numerical vars *\) *)
102
    (* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *)
103
    (* else e, None *)
104
    | LT.Fun (fun_id, args) -> (
105
      (* necessarily, this is a basic function (ie. + - * / && || mod ... ) *)
106
      (* if the return type is real then optimize it, otherwise call recusrsively on arguments *)
107
      if Types.is_real_type e.LT.value_type then
108
	opt_num_expr ranges formalEnv e 
109
      else (
110
	(* We do not care for computed local ranges. *)
111
  	let args' = List.map (fun arg -> let arg', _ = opt_expr ranges formalEnv arg in arg') args in
112
  	{ e with LT.value_desc = LT.Fun(fun_id, args')}, None	  
113
      )
114
    )
115
    | LT.Array _
116
    | LT.Access _
117
    | LT.Power _ -> assert false  
118
  and opt_num_expr ranges formalEnv e = 
119
    if debug then Format.eprintf "Optimizing expression %a@ " MC.pp_val e; 
120
    let fresh_id = "toto"  in (* TODO more meaningful name *)
121
    (* Convert expression *)
122
    List.iter (fun (l,c) -> Format.eprintf "%s -> %a@ " l Printers.pp_const c) constEnv;
123
    let e_salsa : Salsa.SalsaTypes.expression = value_t2salsa_expr constEnv e in
124
    Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val (salsa_expr2value_t vars_env [](* constEnv *) e_salsa) ; 
125

    
126
    (* Convert formalEnv *)
127
    if debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv;
128
    let formalEnv_salsa = 
129
      FormalEnv.fold (fun id expr accu ->
130
	(id, value_t2salsa_expr constEnv expr)::accu
131
		     ) formalEnv []  in
132
    if debug then Format.eprintf "Formal env converted to salsa@ ";
133
    (* Substitute all occurences of variables by their definition in env *)
134
    let (e_salsa: Salsa.SalsaTypes.expression), _ = 
135
      Salsa.Rewrite.substVars 
136
	e_salsa
137
	formalEnv_salsa
138
	0 (* TODO: Nasrine, what is this integer value for ? *)
139
    in
140
    if debug then Format.eprintf "Substituted def in expr@ ";
141
    let abstractEnv = Hashtbl.fold 
142
      (fun id value accu -> (id,value)::accu) 
143
      ranges
144
      [] 
145
    in
146
    (* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id) abstractEnv; *)
147
    (* The expression is partially evaluated by the available ranges
148
       valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on
149
       garde evalPartExpr remplace les variables e qui sont dans env par la cst
150
       - on garde *)
151
    if debug then Format.eprintf "avant avant eval part@ ";
152
     Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); 
153
    let e_salsa =  
154
      Salsa.Float.evalPartExpr 
155
	e_salsa
156
	(Salsa.Float.valEnv2ExprEnv abstractEnv) 
157
	([] (* no blacklisted variables *))  
158
    in
159
     Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); 
160
    (* Checking if we have all necessary information *)
161

    
162
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv  e_salsa in
163

    
164
    if Vars.cardinal free_vars > 0 then (
165
      Format.eprintf "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 
166
	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)
167
	MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);
168
      if debug then Format.eprintf "Some free vars, not optimizing@.";
169
      let new_e = try salsa_expr2value_t vars_env constEnv e_salsa   with Not_found -> assert false in
170
      new_e, None
171
    )
172
    else (
173
      try
174
	if debug then
175
	  Format.eprintf "Analyzing expression %a with env: @[<v>%a@ @]@ "
176
	    MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa)
177
	    (Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv
178
	;
179
	  
180
	let new_e_salsa, e_val = 
181
	  Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv 
182
	in
183
    	let new_e = try salsa_expr2value_t vars_env constEnv new_e_salsa   with Not_found -> assert false in
184
	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;
185
	new_e, Some e_val
186
      with Not_found -> assert false
187
      | Salsa.Epeg_types.EPEGError _ -> (
188
	Format.eprintf "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e;
189
	e, None
190
      )
191
    )
192

    
193

    
194

    
195
  in
196
  if debug then 
197
    Format.eprintf "@[<v 2>Optimizing expression %a in environment %a and ranges %a@ "
198
      MC.pp_val e
199
      FormalEnv.pp formalEnv
200
      RangesInt.pp ranges;
201
  let res = opt_expr ranges formalEnv e in
202
  Format.eprintf "@]@ ";
203
  res
204

    
205
    
206
    
207
(* Returns a list of assign, for each var in vars_to_print, that produce the
208
   definition of it according to formalEnv, and driven by the ranges. *)
209
let assign_vars nodename constEnv vars_env printed_vars ranges formalEnv vars_to_print =
210
  (* We print thhe expression in the order of definition *)
211

    
212
  let ordered_vars = 
213
    List.stable_sort
214
      (FormalEnv.get_sort_fun formalEnv) 
215
      (Vars.elements vars_to_print) 
216
  in
217
  Format.eprintf "Printing vars in the following order: [%a]@ " (Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars ;
218
  List.fold_right (
219
    fun v (accu_instr, accu_ranges) -> 
220
      if debug then Format.eprintf "Printing assign for variable %s@ " v.LT.var_id;
221
      try
222
	(* Obtaining unfold expression of v in formalEnv *)
223
	let v_def = FormalEnv.get_def formalEnv v  in
224
	let e, r = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv v_def in
225
	let instr = 
226
	  if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then
227
	    LT.MLocalAssign(v, e)
228
	  else
229
	    LT.MStateAssign(v, e)
230
	in
231
	instr::accu_instr, 
232
	(match r with 
233
	| None -> ranges 
234
	| Some v_r -> RangesInt.add_def ranges v.LT.var_id v_r)
235
      with FormalEnv.NoDefinition _ -> (
236
	(* It should not happen with C backend, but may happen with Lustre backend *)
237
	if !Options.output = "lustre" then accu_instr, ranges else (Format.eprintf "@?"; assert false)
238
      )
239
  ) ordered_vars ([], ranges)
240

    
241
(* Main recursive function: modify the instructions list while preserving the
242
   order of assigns for state variables. Returns a quintuple: (new_instrs,
243
   ranges, formalEnv, printed_vars, and remaining vars to be printed) *)
244
let rec rewrite_instrs nodename constEnv  vars_env m instrs ranges formalEnv printed_vars vars_to_print = 
245
  let assign_vars = assign_vars nodename constEnv vars_env in
246
  if debug then (
247
    Format.eprintf "------------@ ";
248
    Format.eprintf "Current printed_vars: [%a]@ " Vars.pp printed_vars;
249
    Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv;
250
  );
251
  match instrs with
252
  | [] -> 
253
     (* End of instruction list: we produce the definition of each variable that
254
       appears in vars_to_print. Each of them should be defined in formalEnv *)
255
     if debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print;
256
     let instrs, ranges' = assign_vars printed_vars ranges formalEnv vars_to_print in
257
     instrs,
258
     ranges',     
259
     formalEnv,
260
     Vars.union printed_vars vars_to_print, (* We should have printed all required vars *)
261
     []          (* No more vars to be printed *)
262

    
263
  | hd_instr::tl_instrs -> 
264
     (* We reformulate hd_instr, producing or not a fresh instruction, updating
265
       formalEnv, possibly ranges and vars_to_print *)
266
     begin
267
       let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print =
268
	 match hd_instr with 
269
	 | LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type  && not (Vars.mem vd vars_to_print) -> 
270
	    (* LocalAssign are injected into formalEnv *)
271
	    if debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr;
272
	    let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *)
273
	    [],                        (* no instr generated *)
274
	    ranges,                    (* no new range computed *)
275
	    formalEnv',
276
	    printed_vars,              (* no new printed vars *)
277
	    vars_to_print              (* no more or less variables to print *)
278
	      
279
	 | LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
280

    
281
            if debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr;
282
	    let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
283
	    let instrs', ranges' = (* printing vd = optimized vt *)
284
	      assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
285
	    in
286
	    instrs',
287
	    ranges',                          (* no new range computed *)
288
	    formalEnv',                       (* formelEnv already updated *)
289
	    Vars.add vd printed_vars,        (* adding vd to new printed vars *)
290
	    Vars.remove vd vars_to_print     (* removed vd from variables to print *)
291

    
292
	 | LT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print -> 
293

    
294
	    (* StateAssign are produced since they are required by the function. We still
295
	     keep their definition in the formalEnv in case it can optimize later
296
	     outputs. vd is removed from remaining vars_to_print *)
297
	    if debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr;
298
	    let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
299
	    let instrs', ranges' = (* printing vd = optimized vt *)
300
	      assign_vars printed_vars ranges formalEnv (Vars.singleton vd)  
301
	    in
302
	    instrs',
303
	    ranges',                          (* no new range computed *)
304
	    formalEnv,                       (* formelEnv already updated *)
305
	    Vars.add vd printed_vars,        (* adding vd to new printed vars *)
306
	    Vars.remove vd vars_to_print     (* removed vd from variables to print *)
307

    
308
	 | (LT.MLocalAssign(vd,vt) | LT.MStateAssign(vd,vt)) -> 
309
	    (* We have to produce the instruction. But we may have to produce as
310
	     well its dependencies *)
311
	    let required_vars = get_expr_real_vars vt in
312
	    let required_vars = Vars.diff required_vars printed_vars in (* remove
313
									 already
314
									 produced
315
									 variables *)
316
	    let prefix_instr, ranges = 
317
	      assign_vars printed_vars ranges formalEnv required_vars in
318
	    let vt', _ = optimize_expr nodename constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in
319
	    let new_instr = 
320
	      match hd_instr with
321
	      | LT.MLocalAssign _ -> LT.MLocalAssign(vd,vt')
322
	      | _ -> LT.MStateAssign(vd,vt')
323
	    in
324
	    let written_vars = Vars.add vd required_vars in
325
	    prefix_instr@[new_instr],
326
	    ranges,                          (* no new range computed *)
327
	    formalEnv,                       (* formelEnv untouched *)
328
	    Vars.union written_vars printed_vars,  (* adding vd + dependencies to
329
						    new printed vars *)
330
	    Vars.diff vars_to_print written_vars (* removed vd + dependencies from
331
						  variables to print *)
332

    
333
	 | LT.MStep(vdl,id,vtl) -> 
334
	    if debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr;
335
	    (* Call of an external function. Input expressions have to be
336
	     optimized, their free variables produced. A fresh range has to be
337
	     computed for each output variable in vdl. Output of the function
338
	     call are removed from vars to be printed *)
339
	    let node =  called_node_id m id in
340
	    let node_id = Corelang.node_name node in
341
	    let tin, tout =  (* special care for arrow *)
342
	      if node_id = "_arrow" then
343
		match vdl with 
344
		| [v] -> let t = v.LT.var_type in
345
			 [t; t], [t]
346
		| _ -> assert false (* should not happen *)
347
	      else
348
		fun_types node
349
	    in
350
	    if debug then Format.eprintf "@[<v 2>... optimizing arguments@ ";
351
	    let vtl', vtl_ranges = List.fold_right2 (
352
				       fun e typ_e (exprl, range_l)-> 
353
				       if Types.is_real_type typ_e then
354
					 let e', r' = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e in
355
					 e'::exprl, r'::range_l
356
				       else 
357
					 e::exprl, None::range_l
358
				     ) vtl tin ([], []) 
359
	    in 
360
	    if debug then Format.eprintf "... done@ @]@ ";
361
	    let required_vars = 
362
	      List.fold_left2 
363
		(fun accu e typ_e -> 
364
		 if Types.is_real_type typ_e then
365
		   Vars.union accu (get_expr_real_vars e) 
366
		 else (* we do not consider non real expressions *)
367
		   accu
368
		)
369
 		Vars.empty 
370
		vtl' tin
371
	    in
372
	    if debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ "
373
					 Vars.pp required_vars 
374
					 Vars.pp printed_vars
375
					 Vars.pp (Vars.diff required_vars printed_vars)
376
	    ;
377
	      let required_vars = Vars.diff required_vars printed_vars in (* remove
378
									 already
379
									 produced
380
									 variables *)
381
	      let written_vars = Vars.union required_vars (Vars.of_list vdl) in
382
	      let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in
383
	      instrs' @ [LT.MStep(vdl,id,vtl')], (* New instrs *)
384
	      RangesInt.add_call ranges' vdl id vtl_ranges,   (* add information bounding each vdl var *) 
385
	      formalEnv,
386
	      Vars.union written_vars printed_vars,        (* adding vdl to new printed vars *)
387
	      Vars.diff vars_to_print written_vars
388
			
389
	 | LT.MBranch(vt, branches) -> 
390
	    (* Required variables to compute vt are introduced. 
391
	     Then each branch is refactored specifically 
392
	     *)
393
	    if debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr;
394
	    let required_vars = get_expr_real_vars vt in
395
	    let required_vars = Vars.diff required_vars printed_vars in (* remove
396
									 already
397
									 produced
398
									 variables *)
399
	    let prefix_instr, ranges = 
400
	      assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in
401

    
402
	    let printed_vars = Vars.union printed_vars required_vars in
403

    
404
	    let vt', _ = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv vt in
405

    
406
	    let read_vars_tl = get_read_vars tl_instrs in
407
	    if debug then Format.eprintf "@[<v 2>Dealing with branches@ ";
408
	    let branches', written_vars, merged_ranges = List.fold_right (
409
							     fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges) -> 
410
							     let b_write_vars = get_written_vars b_instrs in
411
							     let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in 
412
							     let b_fe = formalEnv in               (* because of side effect
413
						       data, we copy it for
414
						       each branch *)
415
							     let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars = 
416
							       rewrite_instrs nodename constEnv  vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
417
							     in
418
							     (* b_vars should be empty *)
419
							     let _ = if b_vars != [] then assert false in
420
							     
421
							     (* Producing the refactored branch *)
422
							     (b_l, b_instrs') :: new_branches,
423
							     Vars.union b_printed written_vars, (* They should coincides. We
424
						       use union instead of
425
						       inter to ease the
426
						       bootstrap *)
427
							     RangesInt.merge merged_ranges b_ranges      
428
									     
429
							   ) branches ([], required_vars, ranges) in
430
	    if debug then Format.eprintf "dealing with branches done@ @]@ ";	  
431
	    prefix_instr@[LT.MBranch(vt', branches')],
432
	    merged_ranges, (* Only step functions call within branches
433
			    may have produced new ranges. We merge this data by
434
			    computing the join per variable *)
435
	    formalEnv,    (* Thanks to the computation of var_to_print in each
436
			   branch, no new definition should have been computed
437
			   without being already printed *)
438
	    Vars.union written_vars printed_vars,
439
	    Vars.diff vars_to_print written_vars (* We remove vars that have been
440
						  produced within branches *)
441

    
442

    
443
	 | LT.MReset(_) | LT.MComment _ ->
444
			   if debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr;
445

    
446
			   (* Untouched instruction *)
447
			   [ hd_instr ],                    (* unmodified instr *)
448
			   ranges,                          (* no new range computed *)
449
			   formalEnv,                       (* no formelEnv update *)
450
			   printed_vars,
451
			   vars_to_print                    (* no more or less variables to print *)
452
			     
453
       in
454
       let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print = 
455
	 rewrite_instrs 
456
	   nodename
457
	   constEnv 	  
458
	   vars_env
459
	   m 
460
	   tl_instrs
461
	   ranges
462
	   formalEnv
463
	   printed_vars
464
	   vars_to_print
465
       in
466
       hd_instrs @ tl_instrs,
467
       ranges,
468
       formalEnv, 
469
       printed_vars,
470
       vars_to_print 
471
     end
472

    
473

    
474

    
475

    
476

    
477

    
478
(* TODO: deal with new variables, ie. tmp *)
479
let salsaStep constEnv  m s = 
480
  let ranges = RangesInt.empty (* empty for the moment, should be build from
481
				  machine annotations or externally provided information *) in
482
  let annots = List.fold_left (
483
    fun accu annl -> 
484
      List.fold_left (
485
	fun accu (key, range) ->
486
	  match key with 
487
	  | ["salsa"; "ranges"; var] -> (var, range)::accu
488
	  | _ -> accu
489
      ) accu annl.LT.annots
490
  ) [] m.MC.mannot
491
  in
492
  let ranges = 
493
    List.fold_left (fun ranges (v, value) ->
494
      match value.LT.eexpr_qfexpr.LT.expr_desc with 
495
      | LT.Expr_tuple [minv; maxv] -> (
496
	let get_cst e = match e.LT.expr_desc with 
497
	  | LT.Expr_const (LT.Const_real (c,e,s)) -> 
498
	    (* calculer la valeur c * 10^e *) 
499
	    Num.float_of_num (Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))) 
500
	  | _ -> 
501
	    Format.eprintf 
502
	      "Invalid scala range: %a. It should be a pair of constant floats.@." 
503
	      Printers.pp_expr value.LT.eexpr_qfexpr; 
504
	    assert false 
505
	in
506
	let minv, maxv = get_cst minv, get_cst maxv in
507
	if debug then Format.eprintf "%s in [%f, %f]@ " v minv maxv;
508
	RangesInt.enlarge ranges v (Salsa.SalsaTypes.I(minv, maxv),Salsa.SalsaTypes.J(0.,0.))
509
      )
510
      | _ -> 
511
	Format.eprintf 
512
	  "Invalid scala range: %a. It should be a pair of floats.@." 
513
	  Printers.pp_expr value.LT.eexpr_qfexpr; 
514
	assert false
515
    ) ranges annots
516
  in
517
  let formal_env = FormalEnv.empty () in
518
  let vars_to_print =
519
    Vars.real_vars  
520
      (
521
	Vars.union 
522
	  (Vars.of_list m.MC.mmemory) 
523
	  (Vars.of_list s.MC.step_outputs) 
524
      )
525
  in 
526
  (* TODO: should be at least step output + may be memories *)
527
  let vars_env = compute_vars_env m in
528
  let new_instrs, _, _, printed_vars, _ = 
529
    rewrite_instrs
530
      m.MC.mname.LT.node_id
531
      constEnv 
532
      vars_env
533
      m
534
      s.MC.step_instrs
535
      ranges
536
      formal_env
537
      (Vars.real_vars (Vars.of_list s.MC.step_inputs (* printed_vars : real
538
							inputs are considered as
539
							already printed *)))
540
      vars_to_print 
541
  in
542
  let all_local_vars = Vars.real_vars (Vars.of_list s.MC.step_locals) in
543
  let unused = (Vars.diff all_local_vars printed_vars) in
544
  let locals =
545
    if not (Vars.is_empty unused) then (
546
      Format.eprintf "Unused local vars: [%a]. Removing them.@.@?"
547
	Vars.pp unused;
548
      List.filter (fun v -> not (Vars.mem v unused)) s.MC.step_locals
549
    )
550
    else
551
      s.MC.step_locals
552
  in
553
  { s with MC.step_instrs = new_instrs; MC.step_locals = locals } (* we have also to modify local variables to declare new vars *)
554

    
555

    
556
let machine_t2machine_t_optimized_by_salsa constEnv  mt = 
557
  try
558
    if debug then Format.eprintf "@[<v 2>------------------ Optimizing machine %s@ " mt.MC.mname.LT.node_id;
559
    let new_step = salsaStep constEnv  mt mt.MC.mstep in
560
    if debug then Format.eprintf "@]@.";
561
    { mt with MC.mstep = new_step } 
562
    
563
      
564
  with FormalEnv.NoDefinition v as exp -> 
565
    Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v; 
566
    raise exp
567

    
568

    
569
(* Local Variables: *)
570
(* compile-command:"make -C ../../.." *)
571
(* End: *)
572