Project

General

Profile

Download (35.2 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 ~plugin:"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
    | MSpec _ | 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
      | MSpec _ | 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 expr, expr_range  =
123
      match RangesInt.Value.leq old_val e_val, RangesInt.Value.leq e_val old_val with
124
      | true, true -> (
125
	if !debug then report ~level:2 (fun fmt ->
126
	  Format.fprintf fmt "No improvement on abstract value %a@ " RangesInt.pp_val e_val;
127
	);
128
	e_salsa, Some old_val
129
      )
130
      | false, true -> (
131
	if !debug then report ~level:2 (fun fmt ->
132
	  Format.fprintf fmt "Improved!@ ";
133
	);
134
	new_e_salsa, Some e_val
135
      )
136
      | true, false ->
137
         report ~level:2 (fun fmt ->
138
             Format.fprintf fmt
139
               "CAREFUL --- new range is worse!. Restoring provided expression@ ");
140
 	     e_salsa, Some old_val
141

    
142
      | false, false -> (
143
        report ~level:2 (fun fmt ->
144
            Format.fprintf fmt
145
	      "Error; new range is not comparable with old end. It may need some investigation!@. ";
146
	    Format.fprintf fmt "old: %a@.new: %a@ "
147
	      RangesInt.pp_val old_val
148
	      RangesInt.pp_val e_val);
149
	
150
	new_e_salsa, Some e_val
151
       	(* assert false *)
152
      )
153
    in
154
    report ~level:2 (fun fmt -> Format.fprintf fmt " Computing range done@ ");
155

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

    
176

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

    
235
    (* Convert formalEnv *)
236
    (* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)
237
    (* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)
238

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

    
241
    (* Substitute all occurences of variables by their definition in env *)
242
    let (e_salsa: Salsa.Types.expression), _ = 
243
      Salsa.Rewrite.substVars 
244
	e_salsa
245
	(FormalEnv.to_salsa constEnv formalEnv)
246
	0 (* TODO: Nasrine, what is this integer value for ? *)
247
    in
248

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

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

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

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

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

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

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

    
391
        let expr_salsa, expr_range = opt_num_expr_sliced ranges e_salsa in
392
        let expr = try salsa_expr2value_t vars_env' constEnv expr_salsa   with Not_found -> assert false in
393

    
394
        expr, expr_range, List.rev rev_def_tmp_instrs, new_local_vars
395

    
396

    
397

    
398
    (* ???? Bout de code dans unstable lors du merge avec salsa ? 
399
      ====
400

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

    
428

    
429
    
430
  in
431
  opt_expr m vars_env ranges formalEnv e  
432
    
433
    
434
(* Returns a list of assign, for each var in vars_to_print, that produce the
435
   definition of it according to formalEnv, and driven by the ranges. *)
436
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print =
437
  (* We print thhe expression in the order of definition *)
438

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

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

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

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

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

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

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

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

    
623

    
624

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

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

    
650
	   let written_vars = Vars.of_list vdl in
651
	   
652

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

    
675
	    let new_locals = prefix_new_locals in
676
	    
677
	   (* let prefix_instr, ranges =  *)
678
	   (*   assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in *)
679

    
680
	   let printed_vars = Vars.union printed_vars required_vars in
681

    
682

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

    
722

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

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

    
757

    
758

    
759

    
760

    
761

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

    
847

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

    
860

    
861
(* Local Variables: *)
862
(* compile-command:"make -C ../../.." *)
863
(* End: *)
864

    
(2-2/4)