Project

General

Profile

Download (29.1 KB) Statistics
| Branch: | Tag: | Revision:
1
(* We try to avoid opening modules here *)
2
module ST = Salsa.Types
3
module SDT = SalsaDatatypes
4
module LT = Lustre_types
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.MT.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
  let open MT in 
33
  match e.value_desc with
34
  | Var v  when Types.is_real_type v.LT.var_type -> Vars.singleton v
35
  | Var _
36
  | Cst _ -> Vars.empty 
37
  | Fun (_, args) -> 
38
    List.fold_left 
39
      (fun acc e -> Vars.union acc (get_expr_real_vars e)) 
40
      Vars.empty args
41
  | Array _
42
  | Access _
43
  | Power _ -> assert false 
44

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

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

    
83
(* let rec iterTransformExpr fresh_id e_salsa abstractEnv old_range = *)
84
(*   let new_expr, new_range =  *)
85
(*     Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv  *)
86
(*   in *)
87
(*   Format.eprintf "New range: %a@." 	  RangesInt.pp_val new_range; *)
88
(*   if Salsa.Float.errLt new_range old_range < 0 then  *)
89
    
90
(*     iterTransformExpr fresh_id new_expr abstractEnv new_range *)
91
(*   else *)
92
(*     new_expr, new_range *)
93

    
94

    
95
(* Optimize a given expression. It returns another expression and a computed range. *)
96
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e : MT.value_t * RangesInt.t option * (MT.instr_t list) = 
97
  let rec opt_expr m vars_env ranges formalEnv e =
98
    let open MT in
99
    match e.value_desc with
100
    | Cst cst ->
101
       (* Format.eprintf "optmizing constant expr @ "; *)
102
       (* the expression is a constant, we optimize it directly if it is a real
103
  	  constant *)
104
       let typ = Typing.type_const Location.dummy_loc cst in
105
       if Types.is_real_type typ then 
106
	 opt_num_expr m vars_env ranges formalEnv e 
107
       else e, None, []
108
    | Var v -> 
109
       if not (Vars.mem v printed_vars) && 
110
	 (* TODO xavier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *)
111
	 (Types.is_real_type e.value_type ||  Types.is_real_type v.LT.var_type) 
112
       then
113
	 opt_num_expr m vars_env ranges formalEnv e 
114
       else 
115
	 e, None, []  (* Nothing to optimize for expressions containing a single non real variable *)
116
    (* (\* optimize only numerical vars *\) *)
117
    (* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *)
118
    (* else e, None *)
119
    | Fun (fun_id, args) -> (
120
      (* necessarily, this is a basic function (ie. + - * / && || mod ... ) *)
121
      (* if the return type is real then optimize it, otherwise call recusrsively on arguments *)
122
      if Types.is_real_type e.value_type then
123
	opt_num_expr m vars_env ranges formalEnv e 
124
      else (
125
	(* We do not care for computed local ranges. *)
126
  	let args', il = List.fold_right (fun arg (al, il) -> let arg', _, arg_il = opt_expr m vars_env ranges formalEnv arg in arg'::al, arg_il@il) args ([], [])  in
127
  	{ e with value_desc = Fun(fun_id, args')}, None, il	  
128
      )
129
    )
130
    | Array _
131
    | Access _
132
    | Power _ -> assert false  
133
  and opt_num_expr m vars_env ranges formalEnv e = 
134
    if !debug then (
135
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Optimizing expression %a@ "
136
	(MC.pp_val m) e);
137
    );
138
    (* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ " MC.pp_val e;  *)
139
    let fresh_id = "toto"  in (* TODO more meaningful name *)
140
    (* Convert expression *)
141
    (* List.iter (fun (l,c) -> Format.eprintf "%s -> %a@ " l Printers.pp_const c) constEnv; *)
142
    let e_salsa : Salsa.Types.expression = value_t2salsa_expr constEnv e in
143
    (* Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val (salsa_expr2value_t vars_env [](\* constEnv *\) e_salsa) ;  *)
144

    
145
    (* Convert formalEnv *)
146
    (* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)
147
    (* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)
148

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

    
151
    (* Substitute all occurences of variables by their definition in env *)
152
    let (e_salsa: Salsa.Types.expression), _ = 
153
      Salsa.Rewrite.substVars 
154
	e_salsa
155
	(FormalEnv.to_salsa constEnv formalEnv)
156
	0 (* TODO: Nasrine, what is this integer value for ? *)
157
    in
158

    
159
    (* Format.eprintf "Apres %a@." MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ;   *)
160

    
161
    (* if !debug then Format.eprintf "Substituted def in expr@ "; *)
162
    let abstractEnv = RangesInt.to_abstract_env ranges in
163
    (* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id) abstractEnv; *)
164
    (* The expression is partially evaluated by the available ranges
165
       valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on
166
       garde evalPartExpr remplace les variables e qui sont dans env par la cst
167
       - on garde *)
168
    (* if !debug then Format.eprintf "avant avant eval part@ "; *)
169
    (* Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *)
170
    let e_salsa =  
171
      Salsa.Analyzer.evalPartExpr 
172
	e_salsa
173
	(Salsa.Analyzer.valEnv2ExprEnv abstractEnv) 
174
	([] (* no blacklisted variables *))
175
	([] (* no arrays *))
176
    in
177
    (* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *)
178
    (* Checking if we have all necessary information *)
179

    
180
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
181
    if Vars.cardinal free_vars > 0 then (
182
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 
183
	Vars.pp (Vars.fold (fun v accu -> let v' = {v with LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id } in Vars.add v' accu) free_vars Vars.empty)
184
	(MC.pp_val m) (salsa_expr2value_t vars_env constEnv e_salsa));
185
      if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt  "Some free vars, not optimizing@ ");
186
      if !debug then Log.report ~level:3 (fun fmt -> Format.fprintf fmt "  ranges: %a@ "
187
	RangesInt.pp ranges);
188

    
189
      (* if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Formal env was @[<v 0>%a@]@ " FormalEnv.pp formalEnv); *)
190
	
191
      
192
      let new_e = try salsa_expr2value_t vars_env constEnv e_salsa   with Not_found -> assert false in
193
      new_e, None, []
194
    )
195
    else (
196
      
197
      try 
198
	if !debug then
199
	  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Analyzing expression %a with ranges: @[<v>%a@ @]@ "
200
	    (C_backend_common.pp_c_val m "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)
201
	    (Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv)
202
	;
203

    
204
	(* Format.eprintf "going to slice@."; *)
205
	(* Slicing it XXX C'est là !!! ploc *)
206
	let e_salsa, seq = Salsa.Rewrite.sliceExpr e_salsa 0 (Salsa.Types.Nop(Salsa.Types.Lab 0)) in
207
	(* Format.eprintf "sliced@."; *)
208
	let def_tmps = Salsa.Utils.flatten_seq seq [] in
209
	(* Registering tmp ids in vars_env *)
210
	let vars_env' = List.fold_left
211
	  (fun vs (id, _) ->
212
	    VarEnv.add
213
	      id
214
	      {
215
		vdecl = Corelang.mk_fresh_var
216
		  nodename
217
		  Location.dummy_loc
218
		  e.MT.value_type
219
		  (Clocks.new_var true) ;
220
		is_local = true;
221
	      }
222
	      vs
223
	  )
224
	  vars_env
225
	  def_tmps
226
	in 
227
	(* Format.eprintf "List of tmp: @[<v 0>%a@]" *)
228
	(*   ( *)
229
	(*     Utils.fprintf_list *)
230
	(*       ~sep:"@ " *)
231
	(*       (fun fmt (id, e_id) -> *)
232
	(* 	Format.fprintf fmt "(%s,%a) -> %a" *)
233
	(* 	  id *)
234
	(* 	  Printers.pp_var (get_var vars_env' id).vdecl *)
235
	(* 	  (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_id) *)
236
	(*       ) *)
237
	(*   ) *)
238
	(*   def_tmps; *)
239
	(* Format.eprintf "Sliced expression %a@.@?" *)
240
	(*   (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_salsa) *)
241
	(* ; *)
242

    
243
	(* Optimize def tmp, and build the associated instructions. Update the abstract Env with computed ranges *)
244
	let rev_def_tmp_instrs, ranges =
245
	  List.fold_left (fun (accu_instrs, ranges) (id, e_id) ->
246
	    (* Format.eprintf "Cleaning/Optimizing %s@." id; *)
247
	    let abstractEnv = RangesInt.to_abstract_env ranges in
248
	    let e_id', e_range = Salsa.MainEPEG.transformExpression id e_id abstractEnv in
249

    
250
	    let vdecl = (get_var vars_env' id).vdecl in
251
	    let new_e_id' = try salsa_expr2value_t vars_env' constEnv e_id'  with Not_found -> assert false in
252
	
253
	    let new_local_assign =
254
	      (* let expr = salsa_expr2value_t vars_env' constEnv e_id' in *)
255
	      MT.MLocalAssign(vdecl, new_e_id')
256
	    in
257
	    let new_local_assign = {
258
	      MT.instr_desc = new_local_assign;
259
	      MT.lustre_eq = None (* could be Corelang.mkeq Location.dummy_loc
260
				     ([vdecl.LT.var_id], e_id) provided it is
261
				     converted as Lustre expression rather than
262
				     a Machine code value *);
263
	    }
264
	    in
265
	    let new_ranges = RangesInt.add_def ranges id e_range in
266
	    new_local_assign::accu_instrs, new_ranges
267
	  ) ([], ranges) def_tmps
268
	in
269

    
270
	(* Format.eprintf "Optimizing main expression %s@.AbstractEnv is %a" (Salsa.Print.printExpression e_salsa) RangesInt.pp ranges; *)
271
	
272
	let abstractEnv = RangesInt.to_abstract_env ranges in
273
	let new_e_salsa, e_val = 
274
	  Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
275
	in
276

    
277
	(* let range_after = Float.evalExpr new_e_salsa abstractEnv in *)
278

    
279
    	let new_e = try salsa_expr2value_t vars_env' constEnv new_e_salsa   with Not_found -> assert false in
280
	if !debug then Log.report ~level:2 (fun fmt ->
281
	  let old_range = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in
282
	  match RangesInt.Value.leq old_range e_val, RangesInt.Value.leq e_val old_range with
283
	  | true, true -> Format.fprintf fmt "No improvement on abstract value %a@ " RangesInt.pp_val e_val
284
	  | true, false -> (
285
	    Format.fprintf fmt "Improved!";
286
	    Format.fprintf fmt
287
	      "  @[<v>old_expr: @[<v 0>%a@ range: %a@]@ new_expr: @[<v 0>%a@ range: %a@]@ @]@ "
288
	      (MC.pp_val m) e
289
	      RangesInt.pp_val (Salsa.Analyzer.evalExpr e_salsa abstractEnv [])
290
	      (MC.pp_val m) new_e
291
	      RangesInt.pp_val e_val
292
	  )
293
	  | false, true -> Format.eprintf "Error; new range is worse!@.@?"; assert false
294
	  | false, false -> Format.eprintf "Error; new range is not comparabe with old end. This should not happen!@.@?"; assert false
295
	);
296
	new_e, Some e_val, List.rev rev_def_tmp_instrs
297
      with (* Not_found ->  *)
298
      | Salsa.Epeg_types.EPEGError _ -> (
299
	Log.report ~level:2 (fun fmt -> Format.fprintf fmt "BECAUSE OF AN ERROR, Expression %a was not optimized@ " (MC.pp_val m) e);
300
	e, None, []
301
      )
302
    )
303

    
304

    
305
    
306
  in
307
  opt_expr m vars_env ranges formalEnv e  
308
    
309
    
310
(* Returns a list of assign, for each var in vars_to_print, that produce the
311
   definition of it according to formalEnv, and driven by the ranges. *)
312
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print =
313
  (* We print thhe expression in the order of definition *)
314

    
315
  let ordered_vars = 
316
    List.stable_sort
317
      (FormalEnv.get_sort_fun formalEnv) 
318
      (Vars.elements vars_to_print) 
319
  in
320
  if !debug then Log.report ~level:4 (fun fmt -> Format.fprintf fmt
321
    "Printing vars in the following order: [%a]@ "
322
    (Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars);
323
  
324
  List.fold_right (
325
    fun v (accu_instr, accu_ranges) -> 
326
      if !debug then  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Printing assign for variable %s@ " v.LT.var_id);
327
      try
328
	(* Obtaining unfold expression of v in formalEnv *)
329
	let v_def = FormalEnv.get_def formalEnv v  in
330
	let e, r, il = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv v_def in
331
	let instr_desc = 
332
	  if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then
333
	    MT.MLocalAssign(v, e)
334
	  else
335
	    MT.MStateAssign(v, e)
336
	in
337
	il@((Corelang.mkinstr instr_desc)::accu_instr), 
338
	(match r with 
339
	| None -> ranges 
340
	| Some v_r -> RangesInt.add_def ranges v.LT.var_id v_r)
341
      with FormalEnv.NoDefinition _ -> (
342
	(* It should not happen with C backend, but may happen with Lustre backend *)
343
	if !Options.output = "lustre" then accu_instr, ranges else (Format.eprintf "@?"; assert false)
344
      )
345
  ) ordered_vars ([], ranges)
346

    
347
(* Main recursive function: modify the instructions list while preserving the
348
   order of assigns for state variables. Returns a quintuple: (new_instrs,
349
   ranges, formalEnv, printed_vars, and remaining vars to be printed) *)
350
let rec rewrite_instrs nodename m constEnv  vars_env m instrs ranges formalEnv printed_vars vars_to_print =
351
  let formal_env_def = FormalEnv.def constEnv vars_env in
352
  (* Format.eprintf "Rewrite intrs : [%a]@." MC.pp_instrs instrs; *)
353
  let assign_vars = assign_vars nodename m constEnv vars_env in
354
  (* if !debug then ( *)
355
  (*   Log.report ~level:3 (fun fmt -> Format.fprintf fmt    *)
356
  (*     "Current printed_vars: [%a]@ Vars to print: [%a]@ Formal env is [%a]@ " *)
357
  (*     Vars.pp printed_vars *)
358
  (*     Vars.pp vars_to_print *)
359
  (*     FormalEnv.pp formalEnv) *)
360
  (* ); *)
361
  match instrs with
362
  | [] -> 
363
     (* End of instruction list: we produce the definition of each variable that
364
	appears in vars_to_print. Each of them should be defined in formalEnv *)
365
     (* if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print; *)
366
    let instrs, ranges' = assign_vars printed_vars ranges formalEnv vars_to_print in
367
    instrs,
368
    ranges',     
369
    formalEnv,
370
    Vars.union printed_vars vars_to_print, (* We should have printed all required vars *)
371
    []          (* No more vars to be printed *)
372

    
373
  | hd_instr::tl_instrs -> 
374
     (* We reformulate hd_instr, producing or not a fresh instruction, updating
375
	formalEnv, possibly ranges and vars_to_print *)
376
     begin
377
       let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print =
378
	 match Corelang.get_instr_desc hd_instr with 
379
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type  && not (Vars.mem vd vars_to_print) -> 
380
	   (* LocalAssign are injected into formalEnv *)
381
	   (* if !debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; *)
382
	   (* if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
383
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
384
	   [],                        (* no instr generated *)
385
	   ranges,                    (* no new range computed *)
386
	   formalEnv',
387
	   printed_vars,              (* no new printed vars *)
388
	   vars_to_print              (* no more or less variables to print *)
389
	     
390
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
391

    
392
           (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
393
           (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
394
           (* if !debug then ( *)
395
	   (*   Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
396
	   (*   Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd; *)
397
	   (* ); *)
398
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
399
	   let instrs', ranges' = (* printing vd = optimized vt *)
400
	     assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
401
	   in
402
	   instrs',
403
	   ranges',                          (* no new range computed *)
404
	   formalEnv',                       (* formelEnv already updated *)
405
	   Vars.add vd printed_vars,        (* adding vd to new printed vars *)
406
	   Vars.remove vd vars_to_print     (* removed vd from variables to print *)
407

    
408
	 | MT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print  *)-> 
409

    
410
	   (* StateAssign are produced since they are required by the function. We still
411
	      keep their definition in the formalEnv in case it can optimize later
412
	      outputs. vd is removed from remaining vars_to_print *)
413
	   (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
414
           (* if !debug then ( *)
415
	   (*   Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
416
	   (*   Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd; *)
417
	   (* ); *)
418
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
419
	   let instrs', ranges' = (* printing vd = optimized vt *)
420
	     assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
421
	   in
422
	   instrs',
423
	   ranges',                          (* no new range computed *)
424
	   formalEnv,                       (* formelEnv already updated *)
425
	   Vars.add vd printed_vars,        (* adding vd to new printed vars *)
426
	   Vars.remove vd vars_to_print     (* removed vd from variables to print *)
427

    
428
	 | (MT.MLocalAssign(vd,vt) | MT.MStateAssign(vd,vt))  ->
429
	    (* Format.eprintf "other assign %a@." MC.pp_instr hd_instr; *)
430

    
431
	   (* We have to produce the instruction. But we may have to produce as
432
	      well its dependencies *)
433
	   let required_vars = get_expr_real_vars vt in
434
	   let required_vars = Vars.diff required_vars printed_vars in (* remove
435
									  already
436
									  produced
437
									  variables *)
438
	   (* Format.eprintf "Required vars: %a@." Vars.pp required_vars; *)
439
	   let required_vars = Vars.diff required_vars (Vars.of_list m.MT.mmemory) in
440
	   let prefix_instr, ranges = 
441
	     assign_vars printed_vars ranges formalEnv required_vars in
442

    
443
	   let vt', _, il = optimize_expr nodename m constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in
444
	   let new_instr = 
445
	     match Corelang.get_instr_desc hd_instr with
446
	     | MT.MLocalAssign _ -> Corelang.update_instr_desc hd_instr (MT.MLocalAssign(vd,vt'))
447
	     | _ -> Corelang.update_instr_desc hd_instr (MT.MStateAssign(vd,vt'))
448
	   in
449
	   let written_vars = Vars.add vd required_vars in
450
	   prefix_instr@il@[new_instr],
451
	   ranges,                          (* no new range computed *)
452
	   formalEnv,                       (* formelEnv untouched *)
453
	   Vars.union written_vars printed_vars,  (* adding vd + dependencies to
454
						     new printed vars *)
455
	   Vars.diff vars_to_print written_vars (* removed vd + dependencies from
456
						   variables to print *)
457

    
458
	 | MT.MStep(vdl,id,vtl) ->
459
	    (* Format.eprintf "step@."; *)
460

    
461
	   (* if !debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr; *)
462
	   (* Call of an external function. Input expressions have to be
463
	      optimized, their free variables produced. A fresh range has to be
464
	      computed for each output variable in vdl. Output of the function
465
	      call are removed from vars to be printed *)
466
	   let node =  called_node_id m id in
467
	   let node_id = Corelang.node_name node in
468
	   let tin, tout =  (* special care for arrow *)
469
	     if node_id = "_arrow" then
470
	       match vdl with 
471
	       | [v] -> let t = v.LT.var_type in
472
			[t; t], [t]
473
	       | _ -> assert false (* should not happen *)
474
	     else
475
	       fun_types node
476
	   in
477
	   (* if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; *)
478
	   let vtl', vtl_ranges, il = List.fold_right2 (
479
	     fun e typ_e (exprl, range_l, il_l)-> 
480
	       if Types.is_real_type typ_e then
481
		 let e', r', il = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e in
482
		 e'::exprl, r'::range_l, il@il_l
483
	       else 
484
		 e::exprl, None::range_l, il_l
485
	   ) vtl tin ([], [], []) 
486
	   in 
487
	   (* if !debug then Format.eprintf "... done@ @]@ "; *)
488

    
489

    
490

    
491
	   (* let required_vars =  *)
492
	   (*   List.fold_left2  *)
493
	   (*     (fun accu e typ_e ->  *)
494
	   (* 	 if Types.is_real_type typ_e then *)
495
	   (* 	   Vars.union accu (get_expr_real_vars e)  *)
496
	   (* 	 else (\* we do not consider non real expressions *\) *)
497
	   (* 	   accu *)
498
	   (*     ) *)
499
 	   (*     Vars.empty  *)
500
	   (*     vtl' tin *)
501
	   (* in *)
502
	   (* if !debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ " *)
503
	   (*   Vars.pp required_vars  *)
504
	   (*   Vars.pp printed_vars *)
505
	   (*   Vars.pp (Vars.diff required_vars printed_vars) *)
506
	   (* ; *)
507
	   (* let required_vars = Vars.diff required_vars printed_vars in (\* remove *)
508
	   (* 								  already *)
509
	   (* 								  produced *)
510
	   (* 								  variables *\) *)
511
	   (* let written_vars = Vars.union required_vars (Vars.of_list vdl) in *)
512
	   (* let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in *)
513

    
514
	   (* instrs' @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *) *)
515

    
516
	   let written_vars = Vars.of_list vdl in
517
	   
518

    
519
	   
520
	   il @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *)
521
	   RangesInt.add_call ranges vdl id vtl_ranges,   (* add information bounding each vdl var *) 
522
	   formalEnv,
523
	   Vars.union written_vars printed_vars,        (* adding vdl to new printed vars *)
524
	   Vars.diff vars_to_print written_vars
525
	     
526
	 | MT.MBranch(vt, branches) ->
527
	    
528
	    (* Required variables to compute vt are introduced. 
529
	       Then each branch is refactored specifically 
530
	    *)
531
	    (* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; *)
532
	   let required_vars = get_expr_real_vars vt in
533
	   let required_vars = Vars.diff required_vars printed_vars in (* remove
534
									  already
535
									  produced
536
									  variables *)
537
	   let vt', _, prefix_instr = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv vt in
538

    
539
	   (* let prefix_instr, ranges =  *)
540
	   (*   assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in *)
541

    
542
	   let printed_vars = Vars.union printed_vars required_vars in
543

    
544

    
545
	   let read_vars_tl = get_read_vars tl_instrs in
546
	   (* if !debug then Format.eprintf "@[<v 2>Dealing with branches@ "; *)
547
	   let branches', written_vars, merged_ranges = List.fold_right (
548
	     fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges) -> 
549
	       let b_write_vars = get_written_vars b_instrs in
550
	       let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in 
551
	       let b_fe = formalEnv in               (* because of side effect
552
							data, we copy it for
553
							each branch *)
554
	       let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars = 
555
		 rewrite_instrs nodename m constEnv  vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
556
	       in
557
	       (* b_vars should be empty *)
558
	       let _ = if b_vars != [] then assert false in
559
	       
560
	       (* Producing the refactored branch *)
561
	       (b_l, b_instrs') :: new_branches,
562
	       Vars.union b_printed written_vars, (* They should coincides. We
563
						     use union instead of
564
						     inter to ease the
565
						     bootstrap *)
566
	       RangesInt.merge merged_ranges b_ranges      
567
		 
568
	   ) branches ([], required_vars, ranges) in
569
	   (* if !debug then Format.eprintf "dealing with branches done@ @]@ ";	   *)
570
	   prefix_instr@[Corelang.update_instr_desc hd_instr (MT.MBranch(vt', branches'))],
571
	     merged_ranges, (* Only step functions call within branches
572
			       may have produced new ranges. We merge this data by
573
			       computing the join per variable *)
574
	     formalEnv,    (* Thanks to the computation of var_to_print in each
575
			      branch, no new definition should have been computed
576
			      without being already printed *)
577
	     Vars.union written_vars printed_vars,
578
	     Vars.diff vars_to_print written_vars (* We remove vars that have been
579
						     produced within branches *)
580

    
581

    
582
	 | MT.MReset(_) | MT.MNoReset _ | MT.MComment _ ->
583
	    (* if !debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr; *)
584

    
585
	   (* Untouched instruction *)
586
	   [ hd_instr ],                    (* unmodified instr *)
587
	      ranges,                          (* no new range computed *)
588
	      formalEnv,                       (* no formelEnv update *)
589
	      printed_vars,
590
	      vars_to_print                    (* no more or less variables to print *)
591
		
592
       in
593
       let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print = 
594
	 rewrite_instrs 
595
	   nodename
596
	   m
597
	   constEnv 	  
598
	   vars_env
599
	   m 
600
	   tl_instrs
601
	   ranges
602
	   formalEnv
603
	   printed_vars
604
	   vars_to_print
605
       in
606
       hd_instrs @ tl_instrs,
607
       ranges,
608
       formalEnv, 
609
       printed_vars,
610
       vars_to_print 
611
     end
612

    
613

    
614

    
615

    
616

    
617

    
618
(* TODO: deal with new variables, ie. tmp *)
619
let salsaStep constEnv  m s = 
620
  let ranges = RangesInt.empty (* empty for the moment, should be build from
621
				  machine annotations or externally provided information *) in
622
  let annots = List.fold_left (
623
    fun accu annl -> 
624
      List.fold_left (
625
	fun accu (key, range) ->
626
	  match key with 
627
	  | ["salsa"; "ranges"; var] -> (var, range)::accu
628
	  | _ -> accu
629
      ) accu annl.LT.annots
630
  ) [] m.MT.mannot
631
  in
632
  let ranges = 
633
    List.fold_left (fun ranges (v, value) ->
634
      match value.LT.eexpr_qfexpr.LT.expr_desc with 
635
      | LT.Expr_tuple [minv; maxv] -> (
636
	let get_cst e = match e.LT.expr_desc with 
637
	  | LT.Expr_const (LT.Const_real (c,e,s)) -> 
638
	    (* calculer la valeur c * 10^e *) 
639
	    Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))
640
	  | _ -> 
641
	    Format.eprintf 
642
	      "Invalid salsa range: %a. It should be a pair of constant floats and %a is not a float.@." 
643
	      Printers.pp_expr value.LT.eexpr_qfexpr
644
	      Printers.pp_expr e
645
	    ; 
646
	    assert false 
647
	in
648
	(* let minv = Salsa.Float.Domain.of_num (get_cst minv) and *)
649
	(*     maxv = Salsa.Float.Domain.of_num (get_cst maxv) in *)
650
	(* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv); *)
651
	RangesInt.enlarge ranges v (Salsa.Float.Domain.inject_nums (get_cst minv) (get_cst maxv))
652
      )
653
      | _ -> 
654
	Format.eprintf 
655
	  "Invalid salsa range: %a. It should be a pair of floats.@." 
656
	  Printers.pp_expr value.LT.eexpr_qfexpr; 
657
	assert false
658
    ) ranges annots
659
  in
660
  let formal_env = FormalEnv.empty () in
661
  let vars_to_print =
662
    Vars.real_vars  
663
      (
664
	Vars.union 
665
	  (Vars.of_list m.MT.mmemory) 
666
	  (Vars.of_list s.MT.step_outputs) 
667
      )
668
  in 
669
  (* TODO: should be at least step output + may be memories *)
670
  
671
  let vars_env = compute_vars_env m in  
672
  (* if !debug then Format.eprintf "@[<v 2>Registering node equations@ ";  *)
673
  let new_instrs, _, _, printed_vars, _ = 
674
    rewrite_instrs
675
      m.MT.mname
676
      m
677
      constEnv 
678
      vars_env
679
      m
680
      s.MT.step_instrs
681
      ranges
682
      formal_env
683
      (Vars.real_vars (Vars.of_list s.MT.step_inputs (* printed_vars : real
684
							inputs are considered as
685
							already printed *)))
686
      vars_to_print 
687
  in
688
  let all_local_vars = Vars.real_vars (Vars.of_list s.MT.step_locals) in
689
  let unused = (Vars.diff all_local_vars printed_vars) in
690
  let locals =
691
    if not (Vars.is_empty unused) then (
692
      if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt  "Unused local vars: [%a]. Removing them.@ "
693
	Vars.pp unused);
694
      List.filter (fun v -> not (Vars.mem v unused)) s.MT.step_locals
695
    )
696
    else
697
      s.MT.step_locals
698
  in
699
  { s with MT.step_instrs = new_instrs; MT.step_locals = locals } (* we have also to modify local variables to declare new vars *)
700

    
701

    
702
let machine_t2machine_t_optimized_by_salsa constEnv  mt =
703
  try
704
    if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@[<v 3>[salsa] Optimizing machine %s@ " mt.MT.mname.LT.node_id);
705
    let new_step = salsaStep constEnv  mt mt.MT.mstep in
706
    if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@]@ ");
707
    { mt with MT.mstep = new_step } 
708
    
709
      
710
  with FormalEnv.NoDefinition v as exp -> 
711
    Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v; 
712
    raise exp
713

    
714

    
715
(* Local Variables: *)
716
(* compile-command:"make -C ../../.." *)
717
(* End: *)
718

    
(2-2/4)