Project

General

Profile

Download (22.8 KB) Statistics
| Branch: | Tag: | Revision:
1
(* We try to avoid opening modules here *)
2
module ST = Salsa.SalsaTypes
3
module SDT = SalsaDatatypes
4
module LT = LustreSpec
5
module MC = Machine_code
6

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

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

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

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

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

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

    
78

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

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

    
160
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv  e_salsa in
161

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

    
182
	  let range_before = Float.evalExpr e_salsa abstractEnv in
183
	  let range_after = Float.evalExpr new_e_salsa abstractEnv in
184

    
185
    	let new_e = try salsa_expr2value_t vars_env constEnv new_e_salsa   with Not_found -> assert false in
186
	if debug then Format.eprintf "@  @[<v>old: %a@ new: %a@ old range: %a@ new range: %a@]" 
187
	  MC.pp_val e 
188
	  MC.pp_val new_e 
189
	  RangesInt.pp_val range_before
190
	  RangesInt.pp_val range_after (* was e_val *);
191
	new_e, Some e_val
192
      with Not_found -> assert false
193
      | Salsa.Epeg_types.EPEGError _ -> (
194
	Format.eprintf "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e;
195
	e, None
196
      )
197
    )
198

    
199

    
200

    
201
  in
202
  if debug then 
203
    Format.eprintf "@[<v 2>Optimizing expression %a in environment %a and ranges %a@ "
204
      MC.pp_val e
205
      FormalEnv.pp formalEnv
206
      RangesInt.pp ranges;
207
  let res = opt_expr ranges formalEnv e in
208
  Format.eprintf "@]@ ";
209
  res
210

    
211
    
212
    
213
(* Returns a list of assign, for each var in vars_to_print, that produce the
214
   definition of it according to formalEnv, and driven by the ranges. *)
215
let assign_vars nodename constEnv vars_env printed_vars ranges formalEnv vars_to_print =
216
  (* We print thhe expression in the order of definition *)
217

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

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

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

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

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

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

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

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

    
408
	    let printed_vars = Vars.union printed_vars required_vars in
409

    
410
	    let vt', _ = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv vt in
411

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

    
448

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

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

    
479

    
480

    
481

    
482

    
483

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

    
561

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

    
574

    
575
(* Local Variables: *)
576
(* compile-command:"make -C ../../.." *)
577
(* End: *)
578

    
(1-1/3)