Project

General

Profile

Download (35.3 KB) Statistics
| Branch: | Tag: | Revision:
1
(* We try to avoid opening modules here *)
2
module ST = Salsa.Types
3
module SDT = SalsaDatatypes
4
module LT = Lustre_types
5
module MC = Machine_code
6

    
7
(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *)
8
open SalsaDatatypes
9
   
10
let report = Log.report ~plugins:"[salsa]" ~verbose_level:Salsa.Log.verbose_level 
11
(******************************************************************)
12
(* TODO Xavier: should those functions be declared more globally? *)
13

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

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

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

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

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

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

    
96

    
97
(* Takes as input a salsa expression and return an optimized one *)
98
let opt_num_expr_sliced ranges e_salsa =
99
  try 
100
    let fresh_id = "toto"  in (* TODO more meaningful name *)
101

    
102
    let abstractEnv = RangesInt.to_abstract_env ranges in
103
    report ~level:2 (fun fmt -> Format.fprintf fmt
104
                                  "Launching analysis: %s@ "
105
                                  (Salsa.Print.printExpression e_salsa));
106
    let new_e_salsa, e_val = 
107
      Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
108
    in
109
    report ~level:2 (fun fmt -> Format.fprintf fmt " Analysis done: %s@ "
110
      (Salsa.Print.printExpression new_e_salsa));
111

    
112

    
113
    (* (\* Debug *\) *)
114
    (* Format.eprintf "Salsa:@.input expr: %s@.outputexpr: %s@." *)
115
    (*   (Salsa.Print.printExpression e_salsa) *)
116
    (*   (Salsa.Print.printExpression new_e_salsa); *)
117
    (* (\* Debug *\) *)
118
    
119
    report ~level:2 (fun fmt -> Format.fprintf fmt " Computing range progress@ ");
120

    
121
    let old_val = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in
122
    let new_val = Salsa.Analyzer.evalExpr new_e_salsa abstractEnv [] in
123

    
124
    Format.eprintf "Valeurs@.old : %a@.new : %a@.new2: %a@."
125
      RangesInt.pp_val old_val
126
      RangesInt.pp_val new_val
127
      RangesInt.pp_val e_val
128
   ;
129
    let expr, expr_range  =
130
      match RangesInt.Value.leq old_val e_val, RangesInt.Value.leq e_val old_val with
131
      | true, true -> (
132
	if !debug then report ~level:2 (fun fmt ->
133
	  Format.fprintf fmt "No improvement on abstract value %a@ " RangesInt.pp_val e_val;
134
	);
135
	e_salsa, Some old_val
136
      )
137
      | false, true -> (
138
	if !debug then report ~level:2 (fun fmt ->
139
	  Format.fprintf fmt "Improved!@ ";
140
	);
141
	new_e_salsa, Some e_val
142
      )
143
      | true, false ->
144
         report ~level:2 (fun fmt ->
145
             Format.fprintf fmt
146
               "CAREFUL --- new range is worse!. Restoring provided expression@ ");
147
 	     e_salsa, Some old_val
148

    
149
      | false, false -> (
150
        report ~level:2 (fun fmt ->
151
            Format.fprintf fmt
152
	      "Error; new range is not comparable with old end. It may need some investigation!@. ";
153
	    Format.fprintf fmt "old: %a@.new: %a@ "
154
	      RangesInt.pp_val old_val
155
	      RangesInt.pp_val e_val);
156
	
157
	new_e_salsa, Some e_val
158
       	(* assert false *)
159
      )
160
    in
161
    report ~level:2 (fun fmt -> Format.fprintf fmt " Computing range done@ ");
162

    
163
    if !debug then report ~level:2 (fun fmt ->
164
      Format.fprintf fmt
165
	"  @[<v>old_expr: @[<v 0>%s@ range: %a@]@ new_expr: @[<v 0>%s@ range: %a@]@ @]@ "
166
	(Salsa.Print.printExpression e_salsa)
167
	(* MC.pp_val e *)
168
	RangesInt.pp_val old_val
169
	(Salsa.Print.printExpression new_e_salsa)
170
	(* MC.pp_val new_e *)
171
	RangesInt.pp_val e_val;
172
    );
173
    expr, expr_range
174
  with (* Not_found ->  *)
175
  | Salsa.Epeg_types.EPEGError _ -> (
176
    report ~level:2 (fun fmt ->
177
      Format.fprintf fmt
178
	"BECAUSE OF AN ERROR, Expression %s was not optimized@ " 	(Salsa.Print.printExpression e_salsa)
179
(* MC.pp_val e *));
180
    e_salsa, None
181
  )
182

    
183

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

    
242
    (* Convert formalEnv *)
243
    (* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)
244
    (* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)
245

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

    
248
    (* Substitute all occurences of variables by their definition in env *)
249
    let (e_salsa: Salsa.Types.expression), _ = 
250
      Salsa.Rewrite.substVars 
251
	e_salsa
252
	(FormalEnv.to_salsa constEnv formalEnv)
253
	0 (* TODO: Nasrine, what is this integer value for ? *)
254
    in
255

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

    
258
    (* if !debug then Format.eprintf "Substituted def in expr@ "; *)
259
    let abstractEnv = RangesInt.to_abstract_env ranges in
260
    (* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id) abstractEnv; *)
261
    (* The expression is partially evaluated by the available ranges
262
       valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on
263
       garde evalPartExpr remplace les variables e qui sont dans env par la cst
264
       - on garde *)
265
    (* if !debug then Format.eprintf "avant avant eval part@ "; *)
266
    (* Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *)
267
    let e_salsa =  
268
      Salsa.Analyzer.evalPartExpr 
269
	e_salsa
270
	(Salsa.Analyzer.valEnv2ExprEnv abstractEnv) 
271
	([] (* no blacklisted variables *))
272
	([] (* no arrays *))
273
    in
274
    (* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *)
275
    (* Checking if we have all necessary information *)
276

    
277
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
278
    if Vars.cardinal free_vars > 0 then (
279
      report ~level:2 (fun fmt -> Format.fprintf fmt
280
	                                "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 
281
	                                Vars.pp (Vars.fold (fun v accu ->
282
	                                             let v' = {v with LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id } in
283
	                                             Vars.add v' accu)
284
		                                   free_vars Vars.empty)
285
	                                (MC.pp_val m) (salsa_expr2value_t vars_env constEnv e_salsa));
286
      if !debug then report ~level:2 (fun fmt -> Format.fprintf fmt  "Some free vars, not optimizing@ ");
287
      if !debug then report ~level:3 (fun fmt -> Format.fprintf fmt "  ranges: %a@ "
288
	                                               RangesInt.pp ranges);
289

    
290
      (* if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Formal env was @[<v 0>%a@]@ " FormalEnv.pp formalEnv); *)
291
      
292
      
293
      let new_e = try salsa_expr2value_t vars_env constEnv e_salsa   with Not_found -> assert false in
294
      new_e, None, [] , Vars.empty
295
    )
296
    else (
297
      
298
      if !debug then
299
	report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 2>Analyzing expression %a@  with ranges: @[<v>%a@ @]@ @]@ "
300
	                                  (C_backend_common.pp_c_val m "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)
301
	                                  (Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv)
302
      
303
      ;
304

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

    
370
	      let vdecl = (get_var vars_env' id).vdecl in
371
	      
372
	      let new_local_assign =
373
	        (* let expr = salsa_expr2value_t vars_env' constEnv e_id' in *)
374
	        MT.MLocalAssign(vdecl, new_e_id')
375
	      in
376
	      let new_local_assign = {
377
	          MT.instr_desc = new_local_assign;
378
	          MT.lustre_eq = None (* could be Corelang.mkeq Location.dummy_loc
379
				   ([vdecl.LT.var_id], e_id) provided it is
380
				   converted as Lustre expression rather than
381
				   a Machine code value *);
382
	        }
383
	      in
384
	      let new_ranges =
385
	        match e_range with
386
	          None -> ranges
387
	        | Some e_range -> RangesInt.add_def ranges id e_range in
388
	      new_local_assign::accu_instrs, new_ranges
389
	    ) ([], ranges) def_tmps
390
        in
391
        if !debug && List.length def_tmps >= 1 then (
392
	  report ~level:3 (fun fmt -> Format.fprintf fmt "@]@ ")
393
        );
394

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

    
398
        let expr_salsa, expr_range = opt_num_expr_sliced ranges e_salsa in
399
        let expr = try salsa_expr2value_t vars_env' constEnv expr_salsa   with Not_found -> assert false in
400

    
401
        expr, expr_range, List.rev rev_def_tmp_instrs, new_local_vars
402

    
403

    
404

    
405
    (* ???? Bout de code dans unstable lors du merge avec salsa ? 
406
      ====
407

    
408
      let new_e = try salsa_expr2value_t vars_env' constEnv new_e_salsa   with Not_found -> assert false in
409
	if !debug then Log.report ~level:2 (fun fmt ->
410
	  let old_range = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in
411
	  match RangesInt.Value.leq old_range e_val, RangesInt.Value.leq e_val old_range with
412
	  | true, true -> Format.fprintf fmt "No improvement on abstract value %a@ " RangesInt.pp_val e_val
413
	  | true, false -> (
414
	    Format.fprintf fmt "Improved!";
415
	    Format.fprintf fmt
416
	      "  @[<v>old_expr: @[<v 0>%a@ range: %a@]@ new_expr: @[<v 0>%a@ range: %a@]@ @]@ "
417
	      (MC.pp_val m) e
418
	      RangesInt.pp_val (Salsa.Analyzer.evalExpr e_salsa abstractEnv [])
419
	      (MC.pp_val m) new_e
420
	      RangesInt.pp_val e_val
421
	  )
422
	  | false, true -> Format.eprintf "Error; new range is worse!@.@?"; assert false
423
	  | false, false -> Format.eprintf "Error; new range is not comparabe with old end. This should not happen!@.@?"; assert false
424
	);
425
	new_e, Some e_val, List.rev rev_def_tmp_instrs
426
      with (* Not_found ->  *)
427
      | Salsa.Epeg_types.EPEGError _ -> (
428
	Log.report ~level:2 (fun fmt -> Format.fprintf fmt "BECAUSE OF AN ERROR, Expression %a was not optimized@ " (MC.pp_val m) e);
429
	e, None, []
430
      )
431
>>>>>>> unstable
432
     *)
433
    )
434

    
435

    
436
    
437
  in
438
  opt_expr m vars_env ranges formalEnv e  
439
    
440
    
441
(* Returns a list of assign, for each var in vars_to_print, that produce the
442
   definition of it according to formalEnv, and driven by the ranges. *)
443
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print =
444
  (* We print thhe expression in the order of definition *)
445

    
446
  let ordered_vars = 
447
    List.stable_sort
448
      (FormalEnv.get_sort_fun formalEnv) 
449
      (Vars.elements vars_to_print) 
450
  in
451
  if !debug then report ~level:4 (fun fmt -> Format.fprintf fmt
452
    "Printing vars in the following order: [%a]@ "
453
    (Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars);
454
  
455
  List.fold_right (
456
    fun v (accu_instr, accu_ranges, accu_new_locals) -> 
457
      if !debug then report ~level:4 (fun fmt -> Format.fprintf fmt "Printing assign for variable %s@ " v.LT.var_id);
458
      try
459
	(* Obtaining unfold expression of v in formalEnv *)
460
	let v_def = FormalEnv.get_def formalEnv v  in
461
	let e, r, il, new_v_locals =
462
	  optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv v_def
463
	in
464
	let instr_desc = 
465
	  if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then
466
	    MT.MLocalAssign(v, e)
467
	  else
468
	    MT.MStateAssign(v, e)
469
	in
470
	  (il@((Corelang.mkinstr instr_desc)::accu_instr)), 
471
	    (
472
	      match r with 
473
	      | None -> ranges 
474
	      | Some v_r -> RangesInt.add_def ranges v.LT.var_id v_r),
475
	    (Vars.union accu_new_locals new_v_locals)
476
      with FormalEnv.NoDefinition _ -> (
477
	(* It should not happen with C backend, but may happen with Lustre backend *)
478
	if !Options.output = "lustre" then accu_instr, ranges, Vars.empty else (Format.eprintf "@?"; assert false)
479
      )
480
  ) ordered_vars ([], ranges, Vars.empty)
481

    
482
(* Main recursive function: modify the instructions list while preserving the
483
   order of assigns for state variables. Returns a quintuple: (new_instrs,
484
   ranges, formalEnv, printed_vars, and remaining vars to be printed) *)
485
let rec rewrite_instrs nodename m constEnv  vars_env m instrs ranges formalEnv printed_vars vars_to_print =
486
  let formal_env_def = FormalEnv.def constEnv vars_env in
487
  (* Format.eprintf "Rewrite intrs : [%a]@." MC.pp_instrs instrs; *)
488
  let assign_vars = assign_vars nodename m constEnv vars_env in
489
  (* if !debug then ( *)
490
  (*   Log.report ~level:3 (fun fmt -> Format.fprintf fmt    *)
491
  (*     "Current printed_vars: [%a]@ Vars to print: [%a]@ Formal env is [%a]@ " *)
492
  (*     Vars.pp printed_vars *)
493
  (*     Vars.pp vars_to_print *)
494
  (*     FormalEnv.pp formalEnv) *)
495
  (* ); *)
496
  match instrs with
497
  | [] -> 
498
     (* End of instruction list: we produce the definition of each variable that
499
	appears in vars_to_print. Each of them should be defined in formalEnv *)
500
     (* if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print; *)
501
    let instrs, ranges', new_expr_locals = assign_vars printed_vars ranges formalEnv vars_to_print in
502
    instrs,
503
    ranges',     
504
    formalEnv,
505
    Vars.union printed_vars vars_to_print, (* We should have printed all required vars *)
506
    [], (* No more vars to be printed *)
507
    Vars.empty
508
      
509
  | hd_instr::tl_instrs -> 
510
     (* We reformulate hd_instr, producing or not a fresh instruction, updating
511
	formalEnv, possibly ranges and vars_to_print *)
512
     begin
513
       let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print, hd_new_locals =
514
	 match Corelang.get_instr_desc hd_instr with 
515
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type  && not (Vars.mem vd vars_to_print) -> 
516
	   (* LocalAssign are injected into formalEnv *)
517
	   (* if !debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; *)
518
	   (* if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
519
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
520
	   [],                        (* no instr generated *)
521
	   ranges,                    (* no new range computed *)
522
	   formalEnv',
523
	   printed_vars,              (* no new printed vars *)
524
	   vars_to_print,              (* no more or less variables to print *)
525
	   Vars.empty              (* no new locals *)
526
	   
527
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
528

    
529
           (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
530
           (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
531
           (* if !debug then ( *)
532
	   (*   Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
533
	   (*   Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd; *)
534
	   (* ); *)
535
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
536
	   let instrs', ranges', expr_new_locals = (* printing vd = optimized vt *)
537
	     assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
538
	   in
539
	   instrs',
540
	   ranges',                          (* no new range computed *)
541
	   formalEnv',                       (* formelEnv already updated *)
542
	   Vars.add vd printed_vars,         (* adding vd to new printed vars *)
543
	   Vars.remove vd vars_to_print,     (* removed vd from variables to print *)
544
	   expr_new_locals                   (* adding sliced vardecl to the list *)
545
	     
546
	 | MT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print  *)-> 
547

    
548
	   (* StateAssign are produced since they are required by the function. We still
549
	      keep their definition in the formalEnv in case it can optimize later
550
	      outputs. vd is removed from remaining vars_to_print *)
551
	   (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
552
           (* if !debug then ( *)
553
	   (*   Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
554
	   (*   Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd; *)
555
	   (* ); *)
556
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
557
	   let instrs', ranges', expr_new_locals = (* printing vd = optimized vt *)
558
	     assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
559
	   in
560
	   instrs',
561
	   ranges',                          (* no new range computed *)
562
	   formalEnv,                        (* formelEnv already updated *)
563
	   Vars.add vd printed_vars,         (* adding vd to new printed vars *)
564
	   Vars.remove vd vars_to_print,     (* removed vd from variables to print *)
565
	   expr_new_locals                   (* adding sliced vardecl to the list *)
566

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

    
570
	   (* We have to produce the instruction. But we may have to produce as
571
	      well its dependencies *)
572
	   let required_vars = get_expr_real_vars vt in
573
	   let required_vars = Vars.diff required_vars printed_vars in (* remove
574
									  already
575
									  produced
576
									  variables *)
577
	   (* Format.eprintf "Required vars: %a@." Vars.pp required_vars; *)
578
	   let required_vars = Vars.diff required_vars (Vars.of_list m.MT.mmemory) in
579
	   let prefix_instr, ranges, new_expr_dep_locals  = 
580
	     assign_vars printed_vars ranges formalEnv required_vars in
581

    
582
	   let vt', _, il, expr_new_locals = optimize_expr nodename m constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in
583
	   let new_instr = 
584
	     match Corelang.get_instr_desc hd_instr with
585
	     | MT.MLocalAssign _ -> Corelang.update_instr_desc hd_instr (MT.MLocalAssign(vd,vt'))
586
	     | _ -> Corelang.update_instr_desc hd_instr (MT.MStateAssign(vd,vt'))
587
	   in
588
	   let written_vars = Vars.add vd required_vars in
589
	   prefix_instr@il@[new_instr],
590
	   ranges,                          (* no new range computed *)
591
	   formalEnv,                       (* formelEnv untouched *)
592
	   Vars.union written_vars printed_vars,  (* adding vd + dependencies to
593
						     new printed vars *)
594
	   Vars.diff vars_to_print written_vars, (* removed vd + dependencies from
595
						   variables to print *)
596
	   (Vars.union new_expr_dep_locals expr_new_locals)
597
	 | MT.MStep(vdl,id,vtl) ->
598
	    (* Format.eprintf "step@."; *)
599

    
600
	   (* if !debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr; *)
601
	   (* Call of an external function. Input expressions have to be
602
	      optimized, their free variables produced. A fresh range has to be
603
	      computed for each output variable in vdl. Output of the function
604
	      call are removed from vars to be printed *)
605
	   let node =  called_node_id m id in
606
	   let node_id = Corelang.node_name node in
607
	   let tin, tout =  (* special care for arrow *)
608
	     if node_id = "_arrow" then
609
	       match vdl with 
610
	       | [v] -> let t = v.LT.var_type in
611
			[t; t], [t]
612
	       | _ -> assert false (* should not happen *)
613
	     else
614
	       fun_types node
615
	   in
616
	   (* if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; *)
617
	   let vtl', vtl_ranges, il, args_new_locals = List.fold_right2 (
618
	     fun e typ_e (exprl, range_l, il_l, new_locals)-> 
619
	       if Types.is_real_type typ_e then
620
		 let e', r', il, new_expr_locals =
621
		   optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e
622
		 in
623
		 e'::exprl, r'::range_l, il@il_l, Vars.union new_locals new_expr_locals
624
	       else 
625
		 e::exprl, None::range_l, il_l, new_locals
626
	   ) vtl tin ([], [], [], Vars.empty) 
627
	   in 
628
	   (* if !debug then Format.eprintf "... done@ @]@ "; *)
629

    
630

    
631

    
632
	   (* let required_vars =  *)
633
	   (*   List.fold_left2  *)
634
	   (*     (fun accu e typ_e ->  *)
635
	   (* 	 if Types.is_real_type typ_e then *)
636
	   (* 	   Vars.union accu (get_expr_real_vars e)  *)
637
	   (* 	 else (\* we do not consider non real expressions *\) *)
638
	   (* 	   accu *)
639
	   (*     ) *)
640
 	   (*     Vars.empty  *)
641
	   (*     vtl' tin *)
642
	   (* in *)
643
	   (* if !debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ " *)
644
	   (*   Vars.pp required_vars  *)
645
	   (*   Vars.pp printed_vars *)
646
	   (*   Vars.pp (Vars.diff required_vars printed_vars) *)
647
	   (* ; *)
648
	   (* let required_vars = Vars.diff required_vars printed_vars in (\* remove *)
649
	   (* 								  already *)
650
	   (* 								  produced *)
651
	   (* 								  variables *\) *)
652
	   (* let written_vars = Vars.union required_vars (Vars.of_list vdl) in *)
653
	   (* let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in *)
654

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

    
657
	   let written_vars = Vars.of_list vdl in
658
	   
659

    
660
	   
661
	   il @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *)
662
	   RangesInt.add_call ranges vdl id vtl_ranges,   (* add information bounding each vdl var *) 
663
	   formalEnv,
664
	   Vars.union written_vars printed_vars,        (* adding vdl to new printed vars *)
665
	   Vars.diff vars_to_print written_vars,
666
	   args_new_locals
667
	     
668
	 | MT.MBranch(vt, branches) ->
669
	    
670
	    (* Required variables to compute vt are introduced. 
671
	       Then each branch is refactored specifically 
672
	    *)
673
	    
674
	    (* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; *)
675
	    let required_vars = get_expr_real_vars vt in
676
	    let required_vars = Vars.diff required_vars printed_vars in (* remove
677
									   already
678
									   produced
679
									   variables *)
680
	    let vt', _, prefix_instr, prefix_new_locals = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv vt in
681

    
682
	    let new_locals = prefix_new_locals in
683
	    
684
	   (* let prefix_instr, ranges =  *)
685
	   (*   assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in *)
686

    
687
	   let printed_vars = Vars.union printed_vars required_vars in
688

    
689

    
690
	   let read_vars_tl = get_read_vars tl_instrs in
691
	   (* if !debug then Format.eprintf "@[<v 2>Dealing with branches@ "; *)
692
	   let branches', written_vars, merged_ranges, new_locals = List.fold_right (
693
	     fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges, new_locals) -> 
694
	       let b_write_vars = get_written_vars b_instrs in
695
	       let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in 
696
	       let b_fe = formalEnv in               (* because of side effect
697
							data, we copy it for
698
							each branch *)
699
	       let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars, b_new_locals = 
700
		 rewrite_instrs nodename m constEnv  vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
701
	       in
702
	       (* b_vars should be empty *)
703
	       let _ = if b_vars != [] then assert false in
704
	       
705
	       (* Producing the refactored branch *)
706
	       (b_l, b_instrs') :: new_branches,
707
	       Vars.union b_printed written_vars, (* They should coincides. We
708
						     use union instead of
709
						     inter to ease the
710
						     bootstrap *)
711
	       RangesInt.merge merged_ranges b_ranges,
712
	       Vars.union new_locals b_new_locals
713
		 
714
	   ) branches ([], required_vars, ranges, new_locals)
715
	   in
716
	   (* if !debug then Format.eprintf "dealing with branches done@ @]@ ";	   *)
717
	   prefix_instr@[Corelang.update_instr_desc hd_instr (MT.MBranch(vt', branches'))],
718
	   merged_ranges, (* Only step functions call within branches may have
719
			     produced new ranges. We merge this data by
720
			     computing the join per variable *)
721
	   formalEnv,    (* Thanks to the computation of var_to_print in each
722
			    branch, no new definition should have been computed
723
			    without being already printed *)
724
	   Vars.union written_vars printed_vars,
725
	   Vars.diff vars_to_print written_vars (* We remove vars that have been
726
						   produced within branches *),
727
	   new_locals
728

    
729

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

    
733
	   (* Untouched instruction *)
734
	   [ hd_instr ],                    (* unmodified instr *)
735
	   ranges,                          (* no new range computed *)
736
	   formalEnv,                       (* no formelEnv update *)
737
	   printed_vars,
738
	   vars_to_print,                   (* no more or less variables to print *)
739
	   Vars.empty                       (* no new slides vars *)
740
		
741
       in
742
       let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print, tl_new_locals = 
743
	 rewrite_instrs 
744
	   nodename
745
	   m
746
	   constEnv 	  
747
	   vars_env
748
	   m 
749
	   tl_instrs
750
	   ranges
751
	   formalEnv
752
	   printed_vars
753
	   vars_to_print
754
	   
755
       in
756
       hd_instrs @ tl_instrs,
757
       ranges,
758
       formalEnv, 
759
       printed_vars,
760
       vars_to_print,
761
       (Vars.union hd_new_locals tl_new_locals)
762
     end
763

    
764

    
765

    
766

    
767

    
768

    
769
(* TODO: deal with new variables, ie. tmp *)
770
let salsaStep constEnv  m s = 
771
  let ranges = RangesInt.empty (* empty for the moment, should be build from
772
				  machine annotations or externally provided information *) in
773
  let annots = List.fold_left (
774
    fun accu annl -> 
775
      List.fold_left (
776
	fun accu (key, range) ->
777
	  match key with 
778
	  | ["salsa"; "ranges"; var] -> (var, range)::accu
779
	  | _ -> accu
780
      ) accu annl.LT.annots
781
  ) [] m.MT.mannot
782
  in
783
  let ranges = 
784
    List.fold_left (fun ranges (v, value) ->
785
      match value.LT.eexpr_qfexpr.LT.expr_desc with 
786
      | LT.Expr_tuple [minv; maxv] -> (
787
	let get_cst e = match e.LT.expr_desc with 
788
	  | LT.Expr_const (LT.Const_real (c,e,s)) -> 
789
	    (* calculer la valeur c * 10^e *) 
790
	    Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))
791
	  | _ -> 
792
	    Format.eprintf 
793
	      "Invalid salsa range: %a. It should be a pair of constant floats and %a is not a float.@." 
794
	      Printers.pp_expr value.LT.eexpr_qfexpr
795
	      Printers.pp_expr e
796
	    ; 
797
	    assert false 
798
	in
799
	(* let minv = Salsa.Float.Domain.of_num (get_cst minv) and *)
800
	(*     maxv = Salsa.Float.Domain.of_num (get_cst maxv) in *)
801
	(* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv); *)
802
	RangesInt.enlarge ranges v (Salsa.Float.Domain.inject_nums (get_cst minv) (get_cst maxv))
803
      )
804
      | _ -> 
805
	Format.eprintf 
806
	  "Invalid salsa range: %a. It should be a pair of floats.@." 
807
	  Printers.pp_expr value.LT.eexpr_qfexpr; 
808
	assert false
809
    ) ranges annots
810
  in
811
  let formal_env = FormalEnv.empty () in
812
  let vars_to_print =
813
    Vars.real_vars  
814
      (
815
	Vars.union 
816
	  (Vars.of_list m.MT.mmemory) 
817
	  (Vars.of_list s.MT.step_outputs) 
818
      )
819
  in 
820
  (* TODO: should be at least step output + may be memories *)
821
  
822
  let vars_env = compute_vars_env m in  
823
  (* if !debug then Format.eprintf "@[<v 2>Registering node equations@ ";  *)
824
  let new_instrs, _, _, printed_vars, _, new_locals = 
825
    rewrite_instrs
826
      m.MT.mname
827
      m
828
      constEnv 
829
      vars_env
830
      m
831
      s.MT.step_instrs
832
      ranges
833
      formal_env
834
      (Vars.real_vars (Vars.of_list s.MT.step_inputs (* printed_vars : real
835
							inputs are considered as
836
							already printed *)))
837
      vars_to_print
838
      
839
  in
840
  let all_local_vars = Vars.real_vars (Vars.of_list s.MT.step_locals) in
841
  let unused = (Vars.diff all_local_vars printed_vars) in
842
  let locals =
843
    if not (Vars.is_empty unused) then (
844
      if !debug then report ~level:2 (fun fmt -> Format.fprintf fmt  "Unused local vars: [%a]. Removing them.@ "
845
	Vars.pp unused);
846
      List.filter (fun v -> not (Vars.mem v unused)) s.MT.step_locals
847
    )
848
    else
849
      s.MT.step_locals
850
  in
851
  let locals = locals @ Vars.elements  new_locals in
852
  { s with MT.step_instrs = new_instrs; MT.step_locals = locals } (* we have also to modify local variables to declare new vars *)
853

    
854

    
855
let machine_t2machine_t_optimized_by_salsa constEnv  mt =
856
  try
857
    if !debug then report ~level:2 (fun fmt -> Format.fprintf fmt "@[<v 3>Optimizing machine %s@ " mt.MT.mname.LT.node_id);
858
    let new_step = salsaStep constEnv  mt mt.MT.mstep in
859
    if !debug then report ~level:2 (fun fmt -> Format.fprintf fmt "@]@ ");
860
    { mt with MT.mstep = new_step } 
861
    
862
      
863
  with FormalEnv.NoDefinition v as exp -> 
864
    Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v; 
865
    raise exp
866

    
867

    
868
(* Local Variables: *)
869
(* compile-command:"make -C ../../.." *)
870
(* End: *)
871

    
(2-2/4)