Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / plugins / salsa / machine_salsa_opt.ml @ 9a9058f4

History | View | Annotate | Download (32 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
(* Takes as input a salsa expression and return an optimized one *)
96
let opt_num_expr_sliced ranges e_salsa =
97
  try 
98
    let fresh_id = "toto"  in (* TODO more meaningful name *)
99

    
100
    let abstractEnv = RangesInt.to_abstract_env ranges in
101
    Format.eprintf "Launching analysis@.@?";
102
    let new_e_salsa, e_val = 
103
      Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
104
    in
105
    Format.eprintf " Analysis done@.@?";
106

    
107

    
108
    (* (\* Debug *\) *)
109
    (* Format.eprintf "Salsa:@.input expr: %s@.outputexpr: %s@." *)
110
    (*   (Salsa.Print.printExpression e_salsa) *)
111
    (*   (Salsa.Print.printExpression new_e_salsa); *)
112
    (* (\* Debug *\) *)
113
    
114
    Format.eprintf " Computing range progress@.@?";
115

    
116
    let old_val = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in
117
    let expr, expr_range  =
118
      match RangesInt.Value.leq old_val e_val, RangesInt.Value.leq e_val old_val with
119
      | true, true -> (
120
	if !debug then Log.report ~level:2 (fun fmt ->
121
	  Format.fprintf fmt "No improvement on abstract value %a@ " RangesInt.pp_val e_val;
122
	);
123
	e_salsa, Some old_val
124
      )
125
      | false, true -> (
126
	if !debug then Log.report ~level:2 (fun fmt ->
127
	  Format.fprintf fmt "Improved!@ ";
128
	);
129
	new_e_salsa, Some e_val
130
      )
131
      | true, false -> Format.eprintf "CAREFUL --- new range is worse!. Restoring provided expression@ "; 	e_salsa, Some old_val
132

    
133
      | false, false -> (
134
	Format.eprintf
135
	  "Error; new range is not comparabe with old end. It may need some investigation!@.@?";
136
	Format.eprintf "old: %a@.new: %a@.@?"
137
	  RangesInt.pp_val old_val
138
	  RangesInt.pp_val e_val;
139
	
140
	new_e_salsa, Some e_val
141
       	(* assert false *)
142
      )
143
    in
144
    Format.eprintf " Computing range done@.@?";
145

    
146
    if !debug then Log.report ~level:2 (fun fmt ->
147
      Format.fprintf fmt
148
	"  @[<v>old_expr: @[<v 0>%s@ range: %a@]@ new_expr: @[<v 0>%s@ range: %a@]@ @]@ "
149
	(Salsa.Print.printExpression e_salsa)
150
	(* MC.pp_val e *)
151
	RangesInt.pp_val old_val
152
	(Salsa.Print.printExpression new_e_salsa)
153
	(* MC.pp_val new_e *)
154
	RangesInt.pp_val e_val;
155
    );
156
    expr, expr_range
157
  with (* Not_found ->  *)
158
  | Salsa.Epeg_types.EPEGError _ -> (
159
    Log.report ~level:2 (fun fmt ->
160
      Format.fprintf fmt
161
	"BECAUSE OF AN ERROR, Expression %s was not optimized@ " 	(Salsa.Print.printExpression e_salsa)
162
(* MC.pp_val e *));
163
    e_salsa, None
164
  )
165

    
166

    
167
     
168
(* Optimize a given expression. It returns the modified expression, a computed range and freshly defined variables. *)
169
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e : MT.value_t * RangesInt.t option * MT.instr_t list * Vars.VarSet.t = 
170
  let rec opt_expr vars_env ranges formalEnv e =
171
    let open MT in
172
    match e.value_desc with
173
    | Cst cst ->
174
       (* Format.eprintf "optmizing constant expr @ "; *)
175
       (* the expression is a constant, we optimize it directly if it is a real
176
  	  constant *)
177
       let typ = Typing.type_const Location.dummy_loc cst in
178
       if Types.is_real_type typ then 
179
	 opt_num_expr vars_env ranges formalEnv e 
180
       else e, None, [], Vars.empty
181
    | LocalVar v
182
    | StateVar v -> 
183
       if not (Vars.mem v printed_vars) && 
184
	 (* TODO xavier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *)
185
	 (Types.is_real_type e.value_type ||  Types.is_real_type v.LT.var_type) 
186
       then
187
	 opt_num_expr vars_env ranges formalEnv e 
188
       else 
189
	 e, None, [],  Vars.empty  (* Nothing to optimize for expressions containing a single non real variable *)
190
    (* (\* optimize only numerical vars *\) *)
191
    (* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *)
192
    (* else e, None *)
193
    | Fun (fun_id, args) -> (
194
      (* necessarily, this is a basic function (ie. + - * / && || mod ... ) *)
195
      (* if the return type is real then optimize it, otherwise call recusrsively on arguments *)
196
      if Types.is_real_type e.value_type then
197
	opt_num_expr vars_env ranges formalEnv e 
198
      else (
199
	(* We do not care for computed local ranges. *)
200
  	let args', il, new_locals =
201
	  List.fold_right (
202
	    fun arg (al, il, nl) ->
203
	      let arg', _, arg_il, arg_nl =
204
		opt_expr vars_env ranges formalEnv arg in
205
	      arg'::al, arg_il@il, Vars.union arg_nl nl)
206
	    args
207
	    ([], [], Vars.empty)
208
	in
209
  	{ e with value_desc = Fun(fun_id, args')}, None, il, new_locals	  
210
      )
211
    )
212
    | Array _
213
    | Access _
214
    | Power _ -> assert false  
215
  and opt_num_expr vars_env ranges formalEnv e = 
216
    if !debug then (
217
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Optimizing expression @[<hov>%a@]@ "
218
	MC.pp_val e);
219
    );
220
    (* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ " MC.pp_val e;  *)
221
    (* Convert expression *)
222
    (* List.iter (fun (l,c) -> Format.eprintf "%s -> %a@ " l Printers.pp_const c) constEnv; *)
223
    let e_salsa : Salsa.Types.expression = value_t2salsa_expr constEnv e in
224
    (* Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val (salsa_expr2value_t vars_env [](\* constEnv *\) e_salsa) ;  *)
225

    
226
    (* Convert formalEnv *)
227
    (* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)
228
    (* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)
229

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

    
232
    (* Substitute all occurences of variables by their definition in env *)
233
    let (e_salsa: Salsa.Types.expression), _ = 
234
      Salsa.Rewrite.substVars 
235
	e_salsa
236
	(FormalEnv.to_salsa constEnv formalEnv)
237
	0 (* TODO: Nasrine, what is this integer value for ? *)
238
    in
239

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

    
242
    (* if !debug then Format.eprintf "Substituted def in expr@ "; *)
243
    let abstractEnv = RangesInt.to_abstract_env ranges in
244
    (* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id) abstractEnv; *)
245
    (* The expression is partially evaluated by the available ranges
246
       valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on
247
       garde evalPartExpr remplace les variables e qui sont dans env par la cst
248
       - on garde *)
249
    (* if !debug then Format.eprintf "avant avant eval part@ "; *)
250
    (* Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *)
251
    let e_salsa =  
252
      Salsa.Analyzer.evalPartExpr 
253
	e_salsa
254
	(Salsa.Analyzer.valEnv2ExprEnv abstractEnv) 
255
	([] (* no blacklisted variables *))
256
	([] (* no arrays *))
257
    in
258
    (* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *)
259
    (* Checking if we have all necessary information *)
260

    
261
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
262
    if Vars.cardinal free_vars > 0 then (
263
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt
264
	"Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 
265
	Vars.pp (Vars.fold (fun v accu ->
266
	  let v' = {v with LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id } in
267
	  Vars.add v' accu)
268
		   free_vars Vars.empty)
269
	MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));
270
      if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt  "Some free vars, not optimizing@ ");
271
      if !debug then Log.report ~level:3 (fun fmt -> Format.fprintf fmt "  ranges: %a@ "
272
	RangesInt.pp ranges);
273

    
274
      (* if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Formal env was @[<v 0>%a@]@ " FormalEnv.pp formalEnv); *)
275
      
276
      
277
      let new_e = try salsa_expr2value_t vars_env constEnv e_salsa   with Not_found -> assert false in
278
      new_e, None, [] , Vars.empty
279
    )
280
    else (
281
      
282
      if !debug then
283
	  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 2>Analyzing expression %a@  with ranges: @[<v>%a@ @]@ @]@ "
284
	    (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)
285
	    (Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv)
286
	
287
      ;
288

    
289
      (* Slicing expression *)
290
      let e_salsa, seq =
291
	try
292
	  Salsa.Rewrite.sliceExpr e_salsa 0 (Salsa.Types.Nop(Salsa.Types.Lab 0))
293
	    with _ -> Format.eprintf "Issues rewriting express %s@.@?" (Salsa.Print.printExpression e_salsa); assert false
294
      in
295
      let def_tmps = Salsa.Utils.flatten_seq seq [] in
296
      (* Registering tmp ids in vars_env *)
297
      let vars_env', new_local_vars = List.fold_left
298
	(fun (vs,vars) (id, _) ->
299
	  let vdecl = Corelang.mk_fresh_var
300
	    nodename
301
	    Location.dummy_loc
302
	    e.MT.value_type
303
	    (Clocks.new_var true)
304
	    
305
	  in
306
	  let vs' =
307
	    VarEnv.add
308
	      id
309
	      {
310
		vdecl = vdecl ;
311
		is_local = true;
312
	      }
313
	      vs
314
	  in
315
	  let vars' = Vars.add vdecl vars in
316
	  vs', vars'
317
	)
318
	(vars_env,Vars.empty)
319
	def_tmps
320
      in 
321
      (* Debug *)
322
      if !debug then (
323
	Log.report ~level:3 (fun fmt ->
324
	  Format.fprintf  fmt "List of slices: @[<v 0>%a@]@ "
325
	    (Utils.fprintf_list
326
	       ~sep:"@ "
327
	       (fun fmt (id, e_id) ->
328
		 Format.fprintf fmt "(%s,%a) -> %a"
329
		   id
330
		   Printers.pp_var (get_var vars_env' id).vdecl
331
		   (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_id)
332
	       )
333
	    )
334
	    def_tmps;
335
	  Format.eprintf "Sliced expression: %a@ "
336
	    (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_salsa)
337
	  ;
338
	));
339
      (* Debug *)
340
      
341
      (* Optimize def tmp, and build the associated instructions.  Update the
342
	 abstract Env with computed ranges *)
343
      if !debug && List.length def_tmps >= 1 then (
344
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 3>Optimizing sliced sub-expressions@ ")
345
      );
346
      let rev_def_tmp_instrs, ranges =
347
	List.fold_left (fun (accu_instrs, ranges) (id, e_id) ->
348
	  (* Format.eprintf "Cleaning/Optimizing %s@." id; *)
349
	  let e_id', e_range = (*Salsa.MainEPEG.transformExpression id e_id abstractEnv*)
350
	    opt_num_expr_sliced ranges e_id
351
	  in
352
	  let new_e_id' = try salsa_expr2value_t vars_env' constEnv e_id'  with Not_found -> assert false in
353

    
354
	  let vdecl = (get_var vars_env' id).vdecl in
355
	  
356
	  let new_local_assign =
357
	    (* let expr = salsa_expr2value_t vars_env' constEnv e_id' in *)
358
	    MT.MLocalAssign(vdecl, new_e_id')
359
	  in
360
	  let new_local_assign = {
361
	    MT.instr_desc = new_local_assign;
362
	    MT.lustre_eq = None (* could be Corelang.mkeq Location.dummy_loc
363
				   ([vdecl.LT.var_id], e_id) provided it is
364
				   converted as Lustre expression rather than
365
				   a Machine code value *);
366
	  }
367
	  in
368
	  let new_ranges =
369
	    match e_range with
370
	      None -> ranges
371
	    | Some e_range -> RangesInt.add_def ranges id e_range in
372
	  new_local_assign::accu_instrs, new_ranges
373
	) ([], ranges) def_tmps
374
      in
375
      if !debug && List.length def_tmps >= 1 then (
376
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt "@]@ ")
377
      );
378

    
379
      (* Format.eprintf "Optimizing main expression %s@.AbstractEnv is %a" (Salsa.Print.printExpression e_salsa) RangesInt.pp ranges; *)
380
      
381

    
382
      let expr_salsa, expr_range = opt_num_expr_sliced ranges e_salsa in
383
      let expr = try salsa_expr2value_t vars_env' constEnv expr_salsa   with Not_found -> assert false in
384

    
385
      expr, expr_range, List.rev rev_def_tmp_instrs, new_local_vars
386

    
387

    
388

    
389
    )
390

    
391

    
392
      
393
  in
394
  opt_expr vars_env ranges formalEnv e  
395
    
396
    
397
(* Returns a list of assign, for each var in vars_to_print, that produce the
398
   definition of it according to formalEnv, and driven by the ranges. *)
399
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print =
400
  (* We print thhe expression in the order of definition *)
401

    
402
  let ordered_vars = 
403
    List.stable_sort
404
      (FormalEnv.get_sort_fun formalEnv) 
405
      (Vars.elements vars_to_print) 
406
  in
407
  if !debug then Log.report ~level:4 (fun fmt -> Format.fprintf fmt
408
    "Printing vars in the following order: [%a]@ "
409
    (Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars);
410
  
411
  List.fold_right (
412
    fun v (accu_instr, accu_ranges, accu_new_locals) -> 
413
      if !debug then  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Printing assign for variable %s@ " v.LT.var_id);
414
      try
415
	(* Obtaining unfold expression of v in formalEnv *)
416
	let v_def = FormalEnv.get_def formalEnv v  in
417
	let e, r, il, new_v_locals =
418
	  optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv v_def
419
	in
420
	let instr_desc = 
421
	  if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then
422
	    MT.MLocalAssign(v, e)
423
	  else
424
	    MT.MStateAssign(v, e)
425
	in
426
	  (il@((Corelang.mkinstr instr_desc)::accu_instr)), 
427
	    (
428
	      match r with 
429
	      | None -> ranges 
430
	      | Some v_r -> RangesInt.add_def ranges v.LT.var_id v_r),
431
	    (Vars.union accu_new_locals new_v_locals)
432
      with FormalEnv.NoDefinition _ -> (
433
	(* It should not happen with C backend, but may happen with Lustre backend *)
434
	if !Options.output = "lustre" then accu_instr, ranges, Vars.empty else (Format.eprintf "@?"; assert false)
435
      )
436
  ) ordered_vars ([], ranges, Vars.empty)
437

    
438
(* Main recursive function: modify the instructions list while preserving the
439
   order of assigns for state variables. Returns a quintuple: (new_instrs,
440
   ranges, formalEnv, printed_vars, and remaining vars to be printed) *)
441
let rec rewrite_instrs nodename m constEnv  vars_env m instrs ranges formalEnv printed_vars vars_to_print =
442
  let formal_env_def = FormalEnv.def constEnv vars_env in
443
  (* Format.eprintf "Rewrite intrs : [%a]@." MC.pp_instrs instrs; *)
444
  let assign_vars = assign_vars nodename m constEnv vars_env in
445
  (* if !debug then ( *)
446
  (*   Log.report ~level:3 (fun fmt -> Format.fprintf fmt    *)
447
  (*     "Current printed_vars: [%a]@ Vars to print: [%a]@ Formal env is [%a]@ " *)
448
  (*     Vars.pp printed_vars *)
449
  (*     Vars.pp vars_to_print *)
450
  (*     FormalEnv.pp formalEnv) *)
451
  (* ); *)
452
  match instrs with
453
  | [] -> 
454
     (* End of instruction list: we produce the definition of each variable that
455
	appears in vars_to_print. Each of them should be defined in formalEnv *)
456
     (* if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print; *)
457
    let instrs, ranges', new_expr_locals = assign_vars printed_vars ranges formalEnv vars_to_print in
458
    instrs,
459
    ranges',     
460
    formalEnv,
461
    Vars.union printed_vars vars_to_print, (* We should have printed all required vars *)
462
    [], (* No more vars to be printed *)
463
    Vars.empty
464
      
465
  | hd_instr::tl_instrs -> 
466
     (* We reformulate hd_instr, producing or not a fresh instruction, updating
467
	formalEnv, possibly ranges and vars_to_print *)
468
     begin
469
       let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print, hd_new_locals =
470
	 match Corelang.get_instr_desc hd_instr with 
471
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type  && not (Vars.mem vd vars_to_print) -> 
472
	   (* LocalAssign are injected into formalEnv *)
473
	   (* if !debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; *)
474
	   (* if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
475
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
476
	   [],                        (* no instr generated *)
477
	   ranges,                    (* no new range computed *)
478
	   formalEnv',
479
	   printed_vars,              (* no new printed vars *)
480
	   vars_to_print,              (* no more or less variables to print *)
481
	   Vars.empty              (* no new locals *)
482
	   
483
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
484

    
485
           (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
486
           (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
487
           (* if !debug then ( *)
488
	   (*   Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
489
	   (*   Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd; *)
490
	   (* ); *)
491
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
492
	   let instrs', ranges', expr_new_locals = (* printing vd = optimized vt *)
493
	     assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
494
	   in
495
	   instrs',
496
	   ranges',                          (* no new range computed *)
497
	   formalEnv',                       (* formelEnv already updated *)
498
	   Vars.add vd printed_vars,         (* adding vd to new printed vars *)
499
	   Vars.remove vd vars_to_print,     (* removed vd from variables to print *)
500
	   expr_new_locals                   (* adding sliced vardecl to the list *)
501
	     
502
	 | MT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print  *)-> 
503

    
504
	   (* StateAssign are produced since they are required by the function. We still
505
	      keep their definition in the formalEnv in case it can optimize later
506
	      outputs. vd is removed from remaining vars_to_print *)
507
	   (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
508
           (* if !debug then ( *)
509
	   (*   Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
510
	   (*   Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd; *)
511
	   (* ); *)
512
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
513
	   let instrs', ranges', expr_new_locals = (* printing vd = optimized vt *)
514
	     assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
515
	   in
516
	   instrs',
517
	   ranges',                          (* no new range computed *)
518
	   formalEnv,                        (* formelEnv already updated *)
519
	   Vars.add vd printed_vars,         (* adding vd to new printed vars *)
520
	   Vars.remove vd vars_to_print,     (* removed vd from variables to print *)
521
	   expr_new_locals                   (* adding sliced vardecl to the list *)
522

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

    
526
	   (* We have to produce the instruction. But we may have to produce as
527
	      well its dependencies *)
528
	   let required_vars = get_expr_real_vars vt in
529
	   let required_vars = Vars.diff required_vars printed_vars in (* remove
530
									  already
531
									  produced
532
									  variables *)
533
	   (* Format.eprintf "Required vars: %a@." Vars.pp required_vars; *)
534
	   let required_vars = Vars.diff required_vars (Vars.of_list m.MT.mmemory) in
535
	   let prefix_instr, ranges, new_expr_dep_locals  = 
536
	     assign_vars printed_vars ranges formalEnv required_vars in
537

    
538
	   let vt', _, il, expr_new_locals = optimize_expr nodename m constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in
539
	   let new_instr = 
540
	     match Corelang.get_instr_desc hd_instr with
541
	     | MT.MLocalAssign _ -> Corelang.update_instr_desc hd_instr (MT.MLocalAssign(vd,vt'))
542
	     | _ -> Corelang.update_instr_desc hd_instr (MT.MStateAssign(vd,vt'))
543
	   in
544
	   let written_vars = Vars.add vd required_vars in
545
	   prefix_instr@il@[new_instr],
546
	   ranges,                          (* no new range computed *)
547
	   formalEnv,                       (* formelEnv untouched *)
548
	   Vars.union written_vars printed_vars,  (* adding vd + dependencies to
549
						     new printed vars *)
550
	   Vars.diff vars_to_print written_vars, (* removed vd + dependencies from
551
						   variables to print *)
552
	   (Vars.union new_expr_dep_locals expr_new_locals)
553
	 | MT.MStep(vdl,id,vtl) ->
554
	    (* Format.eprintf "step@."; *)
555

    
556
	   (* if !debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr; *)
557
	   (* Call of an external function. Input expressions have to be
558
	      optimized, their free variables produced. A fresh range has to be
559
	      computed for each output variable in vdl. Output of the function
560
	      call are removed from vars to be printed *)
561
	   let node =  called_node_id m id in
562
	   let node_id = Corelang.node_name node in
563
	   let tin, tout =  (* special care for arrow *)
564
	     if node_id = "_arrow" then
565
	       match vdl with 
566
	       | [v] -> let t = v.LT.var_type in
567
			[t; t], [t]
568
	       | _ -> assert false (* should not happen *)
569
	     else
570
	       fun_types node
571
	   in
572
	   (* if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; *)
573
	   let vtl', vtl_ranges, il, args_new_locals = List.fold_right2 (
574
	     fun e typ_e (exprl, range_l, il_l, new_locals)-> 
575
	       if Types.is_real_type typ_e then
576
		 let e', r', il, new_expr_locals =
577
		   optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e
578
		 in
579
		 e'::exprl, r'::range_l, il@il_l, Vars.union new_locals new_expr_locals
580
	       else 
581
		 e::exprl, None::range_l, il_l, new_locals
582
	   ) vtl tin ([], [], [], Vars.empty) 
583
	   in 
584
	   (* if !debug then Format.eprintf "... done@ @]@ "; *)
585

    
586

    
587

    
588
	   (* let required_vars =  *)
589
	   (*   List.fold_left2  *)
590
	   (*     (fun accu e typ_e ->  *)
591
	   (* 	 if Types.is_real_type typ_e then *)
592
	   (* 	   Vars.union accu (get_expr_real_vars e)  *)
593
	   (* 	 else (\* we do not consider non real expressions *\) *)
594
	   (* 	   accu *)
595
	   (*     ) *)
596
 	   (*     Vars.empty  *)
597
	   (*     vtl' tin *)
598
	   (* in *)
599
	   (* if !debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ " *)
600
	   (*   Vars.pp required_vars  *)
601
	   (*   Vars.pp printed_vars *)
602
	   (*   Vars.pp (Vars.diff required_vars printed_vars) *)
603
	   (* ; *)
604
	   (* let required_vars = Vars.diff required_vars printed_vars in (\* remove *)
605
	   (* 								  already *)
606
	   (* 								  produced *)
607
	   (* 								  variables *\) *)
608
	   (* let written_vars = Vars.union required_vars (Vars.of_list vdl) in *)
609
	   (* let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in *)
610

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

    
613
	   let written_vars = Vars.of_list vdl in
614
	   
615

    
616
	   
617
	   il @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *)
618
	   RangesInt.add_call ranges vdl id vtl_ranges,   (* add information bounding each vdl var *) 
619
	   formalEnv,
620
	   Vars.union written_vars printed_vars,        (* adding vdl to new printed vars *)
621
	   Vars.diff vars_to_print written_vars,
622
	   args_new_locals
623
	     
624
	 | MT.MBranch(vt, branches) ->
625
	    
626
	    (* Required variables to compute vt are introduced. 
627
	       Then each branch is refactored specifically 
628
	    *)
629
	    
630
	    (* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; *)
631
	    let required_vars = get_expr_real_vars vt in
632
	    let required_vars = Vars.diff required_vars printed_vars in (* remove
633
									   already
634
									   produced
635
									   variables *)
636
	    let vt', _, prefix_instr, prefix_new_locals = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv vt in
637

    
638
	    let new_locals = prefix_new_locals in
639
	    
640
	   (* let prefix_instr, ranges =  *)
641
	   (*   assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in *)
642

    
643
	   let printed_vars = Vars.union printed_vars required_vars in
644

    
645

    
646
	   let read_vars_tl = get_read_vars tl_instrs in
647
	   (* if !debug then Format.eprintf "@[<v 2>Dealing with branches@ "; *)
648
	   let branches', written_vars, merged_ranges, new_locals = List.fold_right (
649
	     fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges, new_locals) -> 
650
	       let b_write_vars = get_written_vars b_instrs in
651
	       let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in 
652
	       let b_fe = formalEnv in               (* because of side effect
653
							data, we copy it for
654
							each branch *)
655
	       let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars, b_new_locals = 
656
		 rewrite_instrs nodename m constEnv  vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
657
	       in
658
	       (* b_vars should be empty *)
659
	       let _ = if b_vars != [] then assert false in
660
	       
661
	       (* Producing the refactored branch *)
662
	       (b_l, b_instrs') :: new_branches,
663
	       Vars.union b_printed written_vars, (* They should coincides. We
664
						     use union instead of
665
						     inter to ease the
666
						     bootstrap *)
667
	       RangesInt.merge merged_ranges b_ranges,
668
	       Vars.union new_locals b_new_locals
669
		 
670
	   ) branches ([], required_vars, ranges, new_locals)
671
	   in
672
	   (* if !debug then Format.eprintf "dealing with branches done@ @]@ ";	   *)
673
	   prefix_instr@[Corelang.update_instr_desc hd_instr (MT.MBranch(vt', branches'))],
674
	   merged_ranges, (* Only step functions call within branches may have
675
			     produced new ranges. We merge this data by
676
			     computing the join per variable *)
677
	   formalEnv,    (* Thanks to the computation of var_to_print in each
678
			    branch, no new definition should have been computed
679
			    without being already printed *)
680
	   Vars.union written_vars printed_vars,
681
	   Vars.diff vars_to_print written_vars (* We remove vars that have been
682
						   produced within branches *),
683
	   new_locals
684

    
685

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

    
689
	   (* Untouched instruction *)
690
	   [ hd_instr ],                    (* unmodified instr *)
691
	   ranges,                          (* no new range computed *)
692
	   formalEnv,                       (* no formelEnv update *)
693
	   printed_vars,
694
	   vars_to_print,                   (* no more or less variables to print *)
695
	   Vars.empty                       (* no new slides vars *)
696
		
697
       in
698
       let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print, tl_new_locals = 
699
	 rewrite_instrs 
700
	   nodename
701
	   m
702
	   constEnv 	  
703
	   vars_env
704
	   m 
705
	   tl_instrs
706
	   ranges
707
	   formalEnv
708
	   printed_vars
709
	   vars_to_print
710
	   
711
       in
712
       hd_instrs @ tl_instrs,
713
       ranges,
714
       formalEnv, 
715
       printed_vars,
716
       vars_to_print,
717
       (Vars.union hd_new_locals tl_new_locals)
718
     end
719

    
720

    
721

    
722

    
723

    
724

    
725
(* TODO: deal with new variables, ie. tmp *)
726
let salsaStep constEnv  m s = 
727
  let ranges = RangesInt.empty (* empty for the moment, should be build from
728
				  machine annotations or externally provided information *) in
729
  let annots = List.fold_left (
730
    fun accu annl -> 
731
      List.fold_left (
732
	fun accu (key, range) ->
733
	  match key with 
734
	  | ["salsa"; "ranges"; var] -> (var, range)::accu
735
	  | _ -> accu
736
      ) accu annl.LT.annots
737
  ) [] m.MT.mannot
738
  in
739
  let ranges = 
740
    List.fold_left (fun ranges (v, value) ->
741
      match value.LT.eexpr_qfexpr.LT.expr_desc with 
742
      | LT.Expr_tuple [minv; maxv] -> (
743
	let get_cst e = match e.LT.expr_desc with 
744
	  | LT.Expr_const (LT.Const_real (c,e,s)) -> 
745
	    (* calculer la valeur c * 10^e *) 
746
	    Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))
747
	  | _ -> 
748
	    Format.eprintf 
749
	      "Invalid salsa range: %a. It should be a pair of constant floats and %a is not a float.@." 
750
	      Printers.pp_expr value.LT.eexpr_qfexpr
751
	      Printers.pp_expr e
752
	    ; 
753
	    assert false 
754
	in
755
	(* let minv = Salsa.Float.Domain.of_num (get_cst minv) and *)
756
	(*     maxv = Salsa.Float.Domain.of_num (get_cst maxv) in *)
757
	(* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv); *)
758
	RangesInt.enlarge ranges v (Salsa.Float.Domain.inject_nums (get_cst minv) (get_cst maxv))
759
      )
760
      | _ -> 
761
	Format.eprintf 
762
	  "Invalid salsa range: %a. It should be a pair of floats.@." 
763
	  Printers.pp_expr value.LT.eexpr_qfexpr; 
764
	assert false
765
    ) ranges annots
766
  in
767
  let formal_env = FormalEnv.empty () in
768
  let vars_to_print =
769
    Vars.real_vars  
770
      (
771
	Vars.union 
772
	  (Vars.of_list m.MT.mmemory) 
773
	  (Vars.of_list s.MT.step_outputs) 
774
      )
775
  in 
776
  (* TODO: should be at least step output + may be memories *)
777
  
778
  let vars_env = compute_vars_env m in  
779
  (* if !debug then Format.eprintf "@[<v 2>Registering node equations@ ";  *)
780
  let new_instrs, _, _, printed_vars, _, new_locals = 
781
    rewrite_instrs
782
      m.MT.mname
783
      m
784
      constEnv 
785
      vars_env
786
      m
787
      s.MT.step_instrs
788
      ranges
789
      formal_env
790
      (Vars.real_vars (Vars.of_list s.MT.step_inputs (* printed_vars : real
791
							inputs are considered as
792
							already printed *)))
793
      vars_to_print
794
      
795
  in
796
  let all_local_vars = Vars.real_vars (Vars.of_list s.MT.step_locals) in
797
  let unused = (Vars.diff all_local_vars printed_vars) in
798
  let locals =
799
    if not (Vars.is_empty unused) then (
800
      if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt  "Unused local vars: [%a]. Removing them.@ "
801
	Vars.pp unused);
802
      List.filter (fun v -> not (Vars.mem v unused)) s.MT.step_locals
803
    )
804
    else
805
      s.MT.step_locals
806
  in
807
  let locals = locals @ Vars.elements  new_locals in
808
  { s with MT.step_instrs = new_instrs; MT.step_locals = locals } (* we have also to modify local variables to declare new vars *)
809

    
810

    
811
let machine_t2machine_t_optimized_by_salsa constEnv  mt =
812
  try
813
    if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@[<v 3>[salsa] Optimizing machine %s@ " mt.MT.mname.LT.node_id);
814
    let new_step = salsaStep constEnv  mt mt.MT.mstep in
815
    if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@]@ ");
816
    { mt with MT.mstep = new_step } 
817
    
818
      
819
  with FormalEnv.NoDefinition v as exp -> 
820
    Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v; 
821
    raise exp
822

    
823

    
824
(* Local Variables: *)
825
(* compile-command:"make -C ../../.." *)
826
(* End: *)
827