Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / plugins / salsa / machine_salsa_opt.ml @ 642e116d

History | View | Annotate | Download (25 KB)

1

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

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

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

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

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

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

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

    
81

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

    
128
    (* Convert formalEnv *)
129
    (* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)
130
    (* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)
131

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

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

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

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

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

    
186
	(* Slicing it *)
187
	let e_salsa, seq = Salsa.Rewrite.sliceExpr e_salsa 0 (Salsa.Types.Nop(Salsa.Types.Lab 0)) in
188

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

    
206

    
207

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

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

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

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

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

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

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

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

    
338
	 | (LT.MLocalAssign(vd,vt) | LT.MStateAssign(vd,vt))  ->
339
	    Format.eprintf "other assign %a@." MC.pp_instr hd_instr;
340

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

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

    
368
	 | LT.MStep(vdl,id,vtl) ->
369
	    Format.eprintf "step@.";
370

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

    
440
	    let printed_vars = Vars.union printed_vars required_vars in
441

    
442
	    let vt', _ = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv vt in
443

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

    
480

    
481
	 | LT.MReset(_) | LT.MNoReset _ | LT.MComment _ ->
482
			   if !debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr;
483

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

    
514

    
515

    
516

    
517

    
518

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

    
600

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

    
613

    
614
(* Local Variables: *)
615
(* compile-command:"make -C ../../.." *)
616
(* End: *)
617