Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / plugins / salsa / machine_salsa_opt.ml @ 8e6cab20

History | View | Annotate | Download (29.2 KB)

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
  | LocalVar v | StateVar v when Types.is_real_type v.LT.var_type -> Vars.singleton v
35
  | LocalVar _| StateVar _
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 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 vars_env ranges formalEnv e 
107
       else e, None, []
108
    | LocalVar v
109
    | StateVar v -> 
110
       if not (Vars.mem v printed_vars) && 
111
	 (* TODO xavier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *)
112
	 (Types.is_real_type e.value_type ||  Types.is_real_type v.LT.var_type) 
113
       then
114
	 opt_num_expr vars_env ranges formalEnv e 
115
       else 
116
	 e, None, []  (* Nothing to optimize for expressions containing a single non real variable *)
117
    (* (\* optimize only numerical vars *\) *)
118
    (* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *)
119
    (* else e, None *)
120
    | Fun (fun_id, args) -> (
121
      (* necessarily, this is a basic function (ie. + - * / && || mod ... ) *)
122
      (* if the return type is real then optimize it, otherwise call recusrsively on arguments *)
123
      if Types.is_real_type e.value_type then
124
	opt_num_expr vars_env ranges formalEnv e 
125
      else (
126
	(* We do not care for computed local ranges. *)
127
  	let args', il = List.fold_right (fun arg (al, il) -> let arg', _, arg_il = opt_expr vars_env ranges formalEnv arg in arg'::al, arg_il@il) args ([], [])  in
128
  	{ e with value_desc = Fun(fun_id, args')}, None, il	  
129
      )
130
    )
131
    | Array _
132
    | Access _
133
    | Power _ -> assert false  
134
  and opt_num_expr vars_env ranges formalEnv e = 
135
    if !debug then (
136
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Optimizing expression %a@ "
137
	MC.pp_val e);
138
    );
139
    (* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ " MC.pp_val e;  *)
140
    let fresh_id = "toto"  in (* TODO more meaningful name *)
141
    (* Convert expression *)
142
    (* List.iter (fun (l,c) -> Format.eprintf "%s -> %a@ " l Printers.pp_const c) constEnv; *)
143
    let e_salsa : Salsa.Types.expression = value_t2salsa_expr constEnv e in
144
    (* Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val (salsa_expr2value_t vars_env [](\* constEnv *\) e_salsa) ;  *)
145

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

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

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

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

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

    
181
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
182
    if Vars.cardinal free_vars > 0 then (
183
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 
184
	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)
185
	MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));
186
      if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt  "Some free vars, not optimizing@ ");
187
      if !debug then Log.report ~level:3 (fun fmt -> Format.fprintf fmt "  ranges: %a@ "
188
	RangesInt.pp ranges);
189

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

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

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

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

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

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

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

    
305

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

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

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

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

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

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

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

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

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

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

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

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

    
490

    
491

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

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

    
517
	   let written_vars = Vars.of_list vdl in
518
	   
519

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

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

    
543
	   let printed_vars = Vars.union printed_vars required_vars in
544

    
545

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

    
582

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

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

    
614

    
615

    
616

    
617

    
618

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

    
702

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

    
715

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