Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / plugins / salsa / machine_salsa_opt.ml @ 8446bf03

History | View | Annotate | Download (24.9 KB)

1

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

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

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

    
84

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

    
132
    (* Convert formalEnv *)
133
    (* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)
134
    (* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)
135

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

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

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

    
148
    (* if !debug then Format.eprintf "Substituted def in expr@ "; *)
149
    let abstractEnv = Hashtbl.fold 
150
      (fun id value accu -> (id,value)::accu) 
151
      ranges
152
      [] 
153
    in
154
    (* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id) abstractEnv; *)
155
    (* The expression is partially evaluated by the available ranges
156
       valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on
157
       garde evalPartExpr remplace les variables e qui sont dans env par la cst
158
       - on garde *)
159
    (* if !debug then Format.eprintf "avant avant eval part@ "; *)
160
     Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);
161
    let e_salsa =  
162
      Salsa.Analyzer.evalPartExpr 
163
	e_salsa
164
	(Salsa.Analyzer.valEnv2ExprEnv abstractEnv) 
165
	([] (* no blacklisted variables *))
166
	([] (* no arrays *))
167
    in
168
     Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);
169
    (* Checking if we have all necessary information *)
170

    
171
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
172
    if Vars.cardinal free_vars > 0 then (
173
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 
174
	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)
175
	MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));
176
      if !debug then Format.eprintf "Some free vars, not optimizing@.";
177
      
178
      let new_e = try salsa_expr2value_t vars_env constEnv e_salsa   with Not_found -> assert false in
179
      new_e, None
180
    )
181
    else (
182
      
183
      try 
184
	if !debug then
185
	  Format.eprintf "Analyzing expression %a with env: @[<v>%a@ @]@ @?"
186
	    (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)
187
	    (Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv
188
	;
189

    
190
	(* Slicing it *)
191
	let e_salsa, seq = Salsa.Rewrite.sliceExpr e_salsa 0 (Salsa.Types.Nop(Salsa.Types.Lab 0)) in
192

    
193
	Format.eprintf "Sliced expression %a@.@?"
194
	  (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)
195
	;
196
	
197
	let new_e_salsa, e_val = 
198
	  Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
199
	in
200
    	let new_e = try salsa_expr2value_t vars_env constEnv new_e_salsa   with Not_found -> assert false in
201
	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;
202
	new_e, Some e_val
203
      with (* Not_found ->  *)
204
      | Salsa.Epeg_types.EPEGError _ -> (
205
	Format.eprintf "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e;
206
	e, None
207
      )
208
    )
209

    
210

    
211

    
212
  in
213
  if !debug then 
214
    Format.eprintf "@[<v 2>Optimizing expression %a in environment %a and ranges %a@ "
215
      MC.pp_val e
216
      FormalEnv.pp formalEnv
217
      RangesInt.pp ranges;
218
  let res = opt_expr ranges formalEnv e in
219
  Format.eprintf "@]@ ";
220
  res
221

    
222
    
223
    
224
(* Returns a list of assign, for each var in vars_to_print, that produce the
225
   definition of it according to formalEnv, and driven by the ranges. *)
226
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print =
227
  (* We print thhe expression in the order of definition *)
228

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

    
258
(* Main recursive function: modify the instructions list while preserving the
259
   order of assigns for state variables. Returns a quintuple: (new_instrs,
260
   ranges, formalEnv, printed_vars, and remaining vars to be printed) *)
261
let rec rewrite_instrs nodename m constEnv  vars_env m instrs ranges formalEnv printed_vars vars_to_print =
262
  let formal_env_def = FormalEnv.def constEnv vars_env in
263
  Format.eprintf "Rewrite intrs :%a@." Machine_code.pp_instrs instrs;
264
  let assign_vars = assign_vars nodename m constEnv vars_env in
265
  if !debug then (
266
    Format.eprintf "@.------------@ ";
267
    Format.eprintf "Current printed_vars: [%a]@ " Vars.pp printed_vars;
268
    Format.eprintf "Vars to print: [%a]@ " Vars.pp vars_to_print;
269
    Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv;
270
  );
271
  match instrs with
272
  | [] -> 
273
     (* End of instruction list: we produce the definition of each variable that
274
       appears in vars_to_print. Each of them should be defined in formalEnv *)
275
     if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print;
276
     let instrs, ranges' = assign_vars printed_vars ranges formalEnv vars_to_print in
277
     instrs,
278
     ranges',     
279
     formalEnv,
280
     Vars.union printed_vars vars_to_print, (* We should have printed all required vars *)
281
     []          (* No more vars to be printed *)
282

    
283
  | hd_instr::tl_instrs -> 
284
     (* We reformulate hd_instr, producing or not a fresh instruction, updating
285
       formalEnv, possibly ranges and vars_to_print *)
286
     begin
287
       Format.eprintf "Hdlist@.";
288
       let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print =
289
	 match Corelang.get_instr_desc hd_instr with 
290
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type  && not (Vars.mem vd vars_to_print) -> 
291
       Format.eprintf "local assign@.";
292
	    (* LocalAssign are injected into formalEnv *)
293
	    (* if !debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; *)
294
	    if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr;
295
	    let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
296
	    [],                        (* no instr generated *)
297
	    ranges,                    (* no new range computed *)
298
	    formalEnv',
299
	    printed_vars,              (* no new printed vars *)
300
	    vars_to_print              (* no more or less variables to print *)
301
	      
302
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
303
       Format.eprintf "local assign 2@.";
304

    
305
            (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
306
            (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
307
           if !debug then (
308
	     Format.eprintf "%a@]@ " MC.pp_instr hd_instr;
309
	     Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd;
310
	   );
311
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
312
	    let instrs', ranges' = (* printing vd = optimized vt *)
313
	      assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
314
	    in
315
	    instrs',
316
	    ranges',                          (* no new range computed *)
317
	    formalEnv',                       (* formelEnv already updated *)
318
	    Vars.add vd printed_vars,        (* adding vd to new printed vars *)
319
	    Vars.remove vd vars_to_print     (* removed vd from variables to print *)
320

    
321
	 | MT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print  *)-> 
322
	    Format.eprintf "state assign of real type@.";
323

    
324
	    (* StateAssign are produced since they are required by the function. We still
325
	     keep their definition in the formalEnv in case it can optimize later
326
	     outputs. vd is removed from remaining vars_to_print *)
327
	    (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
328
           if !debug then (
329
	     Format.eprintf "%a@]@ " MC.pp_instr hd_instr;
330
	     Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd;
331
	   );
332
	    let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
333
	    let instrs', ranges' = (* printing vd = optimized vt *)
334
	      assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
335
	    in
336
	    instrs',
337
	    ranges',                          (* no new range computed *)
338
	    formalEnv,                       (* formelEnv already updated *)
339
	    Vars.add vd printed_vars,        (* adding vd to new printed vars *)
340
	    Vars.remove vd vars_to_print     (* removed vd from variables to print *)
341

    
342
	 | (MT.MLocalAssign(vd,vt) | MT.MStateAssign(vd,vt))  ->
343
	    Format.eprintf "other assign %a@." MC.pp_instr hd_instr;
344

    
345
	    (* We have to produce the instruction. But we may have to produce as
346
	     well its dependencies *)
347
	    let required_vars = get_expr_real_vars vt in
348
	    let required_vars = Vars.diff required_vars printed_vars in (* remove
349
									 already
350
									 produced
351
									   variables *)
352
	    Format.eprintf "Requited vars: %a@." Vars.pp required_vars;
353
	    let required_vars = Vars.diff required_vars (Vars.of_list m.MC.mmemory) in
354
	    let prefix_instr, ranges = 
355
	      assign_vars printed_vars ranges formalEnv required_vars in
356

    
357
	    let vt', _ = optimize_expr nodename m constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in
358
	    let new_instr = 
359
	      match Corelang.get_instr_desc hd_instr with
360
	      | MT.MLocalAssign _ -> Corelang.update_instr_desc hd_instr (MT.MLocalAssign(vd,vt'))
361
	      | _ -> Corelang.update_instr_desc hd_instr (MT.MStateAssign(vd,vt'))
362
	    in
363
	    let written_vars = Vars.add vd required_vars in
364
	    prefix_instr@[new_instr],
365
	    ranges,                          (* no new range computed *)
366
	    formalEnv,                       (* formelEnv untouched *)
367
	    Vars.union written_vars printed_vars,  (* adding vd + dependencies to
368
						    new printed vars *)
369
	    Vars.diff vars_to_print written_vars (* removed vd + dependencies from
370
						  variables to print *)
371

    
372
	 | MT.MStep(vdl,id,vtl) ->
373
	    Format.eprintf "step@.";
374

    
375
	    if !debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr;
376
	    (* Call of an external function. Input expressions have to be
377
	     optimized, their free variables produced. A fresh range has to be
378
	     computed for each output variable in vdl. Output of the function
379
	     call are removed from vars to be printed *)
380
	    let node =  called_node_id m id in
381
	    let node_id = Corelang.node_name node in
382
	    let tin, tout =  (* special care for arrow *)
383
	      if node_id = "_arrow" then
384
		match vdl with 
385
		| [v] -> let t = v.LT.var_type in
386
			 [t; t], [t]
387
		| _ -> assert false (* should not happen *)
388
	      else
389
		fun_types node
390
	    in
391
	    if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ ";
392
	    let vtl', vtl_ranges = List.fold_right2 (
393
				       fun e typ_e (exprl, range_l)-> 
394
				       if Types.is_real_type typ_e then
395
					 let e', r' = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e in
396
					 e'::exprl, r'::range_l
397
				       else 
398
					 e::exprl, None::range_l
399
				     ) vtl tin ([], []) 
400
	    in 
401
	    if !debug then Format.eprintf "... done@ @]@ ";
402
	    let required_vars = 
403
	      List.fold_left2 
404
		(fun accu e typ_e -> 
405
		 if Types.is_real_type typ_e then
406
		   Vars.union accu (get_expr_real_vars e) 
407
		 else (* we do not consider non real expressions *)
408
		   accu
409
		)
410
 		Vars.empty 
411
		vtl' tin
412
	    in
413
	    if !debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ "
414
					 Vars.pp required_vars 
415
					 Vars.pp printed_vars
416
					 Vars.pp (Vars.diff required_vars printed_vars)
417
	    ;
418
	      let required_vars = Vars.diff required_vars printed_vars in (* remove
419
									 already
420
									 produced
421
									 variables *)
422
	      let written_vars = Vars.union required_vars (Vars.of_list vdl) in
423
	      let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in
424
	      instrs' @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *)
425
	      RangesInt.add_call ranges' vdl id vtl_ranges,   (* add information bounding each vdl var *) 
426
	      formalEnv,
427
	      Vars.union written_vars printed_vars,        (* adding vdl to new printed vars *)
428
	      Vars.diff vars_to_print written_vars
429
			
430
	 | MT.MBranch(vt, branches) ->
431
	    
432
	    (* Required variables to compute vt are introduced. 
433
	     Then each branch is refactored specifically 
434
	     *)
435
	    if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr;
436
	    let required_vars = get_expr_real_vars vt in
437
	    let required_vars = Vars.diff required_vars printed_vars in (* remove
438
									 already
439
									 produced
440
									 variables *)
441
	    let prefix_instr, ranges = 
442
	      assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in
443

    
444
	    let printed_vars = Vars.union printed_vars required_vars in
445

    
446
	    let vt', _ = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv vt in
447

    
448
	    let read_vars_tl = get_read_vars tl_instrs in
449
	    if !debug then Format.eprintf "@[<v 2>Dealing with branches@ ";
450
	    let branches', written_vars, merged_ranges = List.fold_right (
451
							     fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges) -> 
452
							     let b_write_vars = get_written_vars b_instrs in
453
							     let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in 
454
							     let b_fe = formalEnv in               (* because of side effect
455
						       data, we copy it for
456
						       each branch *)
457
							     let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars = 
458
							       rewrite_instrs nodename m constEnv  vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
459
							     in
460
							     (* b_vars should be empty *)
461
							     let _ = if b_vars != [] then assert false in
462
							     
463
							     (* Producing the refactored branch *)
464
							     (b_l, b_instrs') :: new_branches,
465
							     Vars.union b_printed written_vars, (* They should coincides. We
466
						       use union instead of
467
						       inter to ease the
468
						       bootstrap *)
469
							     RangesInt.merge merged_ranges b_ranges      
470
									     
471
							   ) branches ([], required_vars, ranges) in
472
	    if !debug then Format.eprintf "dealing with branches done@ @]@ ";	  
473
	    prefix_instr@[Corelang.update_instr_desc hd_instr (MT.MBranch(vt', branches'))],
474
	    merged_ranges, (* Only step functions call within branches
475
			    may have produced new ranges. We merge this data by
476
			    computing the join per variable *)
477
	    formalEnv,    (* Thanks to the computation of var_to_print in each
478
			   branch, no new definition should have been computed
479
			   without being already printed *)
480
	    Vars.union written_vars printed_vars,
481
	    Vars.diff vars_to_print written_vars (* We remove vars that have been
482
						  produced within branches *)
483

    
484

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

    
488
			   (* Untouched instruction *)
489
			   [ hd_instr ],                    (* unmodified instr *)
490
			   ranges,                          (* no new range computed *)
491
			   formalEnv,                       (* no formelEnv update *)
492
			   printed_vars,
493
			   vars_to_print                    (* no more or less variables to print *)
494
			     
495
       in
496
       Format.eprintf "cic@.";
497
       let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print = 
498
	 rewrite_instrs 
499
	   nodename
500
	   m
501
	   constEnv 	  
502
	   vars_env
503
	   m 
504
	   tl_instrs
505
	   ranges
506
	   formalEnv
507
	   printed_vars
508
	   vars_to_print
509
       in
510
       Format.eprintf "la@.";
511
       hd_instrs @ tl_instrs,
512
       ranges,
513
       formalEnv, 
514
       printed_vars,
515
       vars_to_print 
516
     end
517

    
518

    
519

    
520

    
521

    
522

    
523
(* TODO: deal with new variables, ie. tmp *)
524
let salsaStep constEnv  m s = 
525
  let ranges = RangesInt.empty (* empty for the moment, should be build from
526
				  machine annotations or externally provided information *) in
527
  let annots = List.fold_left (
528
    fun accu annl -> 
529
      List.fold_left (
530
	fun accu (key, range) ->
531
	  match key with 
532
	  | ["salsa"; "ranges"; var] -> (var, range)::accu
533
	  | _ -> accu
534
      ) accu annl.LT.annots
535
  ) [] m.MC.mannot
536
  in
537
  let ranges = 
538
    List.fold_left (fun ranges (v, value) ->
539
      match value.LT.eexpr_qfexpr.LT.expr_desc with 
540
      | LT.Expr_tuple [minv; maxv] -> (
541
	let get_cst e = match e.LT.expr_desc with 
542
	  | LT.Expr_const (LT.Const_real (c,e,s)) -> 
543
	    (* calculer la valeur c * 10^e *) 
544
	    Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))
545
	  | _ -> 
546
	    Format.eprintf 
547
	      "Invalid scala range: %a. It should be a pair of constant floats.@." 
548
	      Printers.pp_expr value.LT.eexpr_qfexpr; 
549
	    assert false 
550
	in
551
	let minv, maxv = get_cst minv, get_cst maxv in
552
	let minv, maxv = Num.float_of_num minv, Num.float_of_num  maxv in
553
	(* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv); *)
554
	RangesInt.enlarge ranges v (Salsa.Float.Domain.nnew minv maxv)
555
      )
556
      | _ -> 
557
	Format.eprintf 
558
	  "Invalid scala range: %a. It should be a pair of floats.@." 
559
	  Printers.pp_expr value.LT.eexpr_qfexpr; 
560
	assert false
561
    ) ranges annots
562
  in
563
  let formal_env = FormalEnv.empty () in
564
  let vars_to_print =
565
    Vars.real_vars  
566
      (
567
	Vars.union 
568
	  (Vars.of_list m.MC.mmemory) 
569
	  (Vars.of_list s.MC.step_outputs) 
570
      )
571
  in 
572
  (* TODO: should be at least step output + may be memories *)
573
  
574
  let vars_env = compute_vars_env m in  
575
  if !debug then Format.eprintf "@[<v 2>Registering node equations@ "; 
576
  let new_instrs, _, _, printed_vars, _ = 
577
    rewrite_instrs
578
      m.MC.mname.LT.node_id
579
      m
580
      constEnv 
581
      vars_env
582
      m
583
      s.MC.step_instrs
584
      ranges
585
      formal_env
586
      (Vars.real_vars (Vars.of_list s.MC.step_inputs (* printed_vars : real
587
							inputs are considered as
588
							already printed *)))
589
      vars_to_print 
590
  in
591
  let all_local_vars = Vars.real_vars (Vars.of_list s.MC.step_locals) in
592
  let unused = (Vars.diff all_local_vars printed_vars) in
593
  let locals =
594
    if not (Vars.is_empty unused) then (
595
      Format.eprintf "Unused local vars: [%a]. Removing them.@.@?"
596
	Vars.pp unused;
597
      List.filter (fun v -> not (Vars.mem v unused)) s.MC.step_locals
598
    )
599
    else
600
      s.MC.step_locals
601
  in
602
  { s with MC.step_instrs = new_instrs; MC.step_locals = locals } (* we have also to modify local variables to declare new vars *)
603

    
604

    
605
let machine_t2machine_t_optimized_by_salsa constEnv  mt =
606
  try
607
    if !debug then Format.eprintf "@[<v 8>[salsa] Optimizing machine %s@ " mt.MC.mname.LT.node_id;
608
    let new_step = salsaStep constEnv  mt mt.MC.mstep in
609
    if !debug then Format.eprintf "@]@ ";
610
    { mt with MC.mstep = new_step } 
611
    
612
      
613
  with FormalEnv.NoDefinition v as exp -> 
614
    Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v; 
615
    raise exp
616

    
617

    
618
(* Local Variables: *)
619
(* compile-command:"make -C ../../.." *)
620
(* End: *)
621