Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / plugins / salsa / machine_salsa_opt.ml @ 8e6cab20

History | View | Annotate | Download (29.2 KB)

1 53206908 xthirioux
(* We try to avoid opening modules here *)
2 94c457b7 ploc
module ST = Salsa.Types
3 53206908 xthirioux
module SDT = SalsaDatatypes
4 8446bf03 ploc
module LT = Lustre_types
5 53206908 xthirioux
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 089f94be ploc
      List.assoc id m.MT.mcalls (* TODO Xavier: mcalls or minstances ? *)
25 53206908 xthirioux
    with Not_found -> assert false
26
  in
27
  td
28
(******************************************************************)    
29
30
(* Returns the set of vars that appear in the expression *)
31 8446bf03 ploc
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 53206908 xthirioux
    List.fold_left 
39
      (fun acc e -> Vars.union acc (get_expr_real_vars e)) 
40
      Vars.empty args
41 8446bf03 ploc
  | Array _
42
  | Access _
43
  | Power _ -> assert false 
44 53206908 xthirioux
45
(* Extract the variables to appear as free variables in expressions (lhs) *)
46
let rec get_read_vars instrs =
47 8446bf03 ploc
  let open MT in
48 53206908 xthirioux
  match instrs with
49
    [] -> Vars.empty
50
  | i::tl -> (
51
    let vars_tl = get_read_vars tl in 
52 3ca27bc7 ploc
    match Corelang.get_instr_desc i with
53 8446bf03 ploc
    | 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 53206908 xthirioux
      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 8446bf03 ploc
    | MReset _ 
61
    | MNoReset _ 
62
    | MComment _ -> Vars.empty  
63 53206908 xthirioux
  )
64
65
let rec get_written_vars instrs =
66 8446bf03 ploc
  let open MT in
67 53206908 xthirioux
  match instrs with
68
    [] -> Vars.empty
69
  | i::tl -> (
70
    let vars_tl = get_written_vars tl in 
71 3ca27bc7 ploc
    match Corelang.get_instr_desc i with
72 8446bf03 ploc
    | 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 53206908 xthirioux
      List.fold_left (fun vars (_, b) -> Vars.union vars (get_written_vars b) ) vars_tl branches
77
    )
78 8446bf03 ploc
    | MReset _ 
79
    | MNoReset _ 
80
    | MComment _ -> Vars.empty    
81 53206908 xthirioux
  )
82
83 c0d116ec ploc
(* 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 8980b5cf Ploc
    
90 c0d116ec ploc
(*     iterTransformExpr fresh_id new_expr abstractEnv new_range *)
91
(*   else *)
92
(*     new_expr, new_range *)
93 8980b5cf Ploc
94 53206908 xthirioux
95
(* Optimize a given expression. It returns another expression and a computed range. *)
96 68322df3 ploc
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e : MT.value_t * RangesInt.t option * (MT.instr_t list) = 
97
  let rec opt_expr vars_env ranges formalEnv e =
98 8446bf03 ploc
    let open MT in
99
    match e.value_desc with
100
    | Cst cst ->
101 68322df3 ploc
       (* Format.eprintf "optmizing constant expr @ "; *)
102
       (* the expression is a constant, we optimize it directly if it is a real
103
  	  constant *)
104
       let typ = Typing.type_const Location.dummy_loc cst in
105
       if Types.is_real_type typ then 
106
	 opt_num_expr vars_env ranges formalEnv e 
107
       else e, None, []
108 8446bf03 ploc
    | LocalVar v
109
    | StateVar v -> 
110 68322df3 ploc
       if not (Vars.mem v printed_vars) && 
111
	 (* TODO xavier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *)
112
	 (Types.is_real_type e.value_type ||  Types.is_real_type v.LT.var_type) 
113
       then
114
	 opt_num_expr vars_env ranges formalEnv e 
115
       else 
116
	 e, None, []  (* Nothing to optimize for expressions containing a single non real variable *)
117 53206908 xthirioux
    (* (\* optimize only numerical vars *\) *)
118
    (* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *)
119
    (* else e, None *)
120 8446bf03 ploc
    | Fun (fun_id, args) -> (
121 53206908 xthirioux
      (* necessarily, this is a basic function (ie. + - * / && || mod ... ) *)
122
      (* if the return type is real then optimize it, otherwise call recusrsively on arguments *)
123 8446bf03 ploc
      if Types.is_real_type e.value_type then
124 68322df3 ploc
	opt_num_expr vars_env ranges formalEnv e 
125 53206908 xthirioux
      else (
126
	(* We do not care for computed local ranges. *)
127 68322df3 ploc
  	let args', il = List.fold_right (fun arg (al, il) -> let arg', _, arg_il = opt_expr vars_env ranges formalEnv arg in arg'::al, arg_il@il) args ([], [])  in
128
  	{ e with value_desc = Fun(fun_id, args')}, None, il	  
129 53206908 xthirioux
      )
130
    )
131 8446bf03 ploc
    | Array _
132
    | Access _
133
    | Power _ -> assert false  
134 68322df3 ploc
  and opt_num_expr vars_env ranges formalEnv e = 
135 8e6cab20 ploc
    if !debug then (
136
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Optimizing expression %a@ "
137
	MC.pp_val e);
138
    );
139 68322df3 ploc
    (* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ " MC.pp_val e;  *)
140 53206908 xthirioux
    let fresh_id = "toto"  in (* TODO more meaningful name *)
141
    (* Convert expression *)
142 9b8acef5 ploc
    (* List.iter (fun (l,c) -> Format.eprintf "%s -> %a@ " l Printers.pp_const c) constEnv; *)
143 94c457b7 ploc
    let e_salsa : Salsa.Types.expression = value_t2salsa_expr constEnv e in
144 9b8acef5 ploc
    (* Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val (salsa_expr2value_t vars_env [](\* constEnv *\) e_salsa) ;  *)
145 53206908 xthirioux
146
    (* Convert formalEnv *)
147 94c457b7 ploc
    (* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)
148
    (* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)
149 642e116d ploc
150 8e6cab20 ploc
    (* Format.eprintf "Expression avant et apres substVars.@.Avant %a@." MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ;   *)
151 642e116d ploc
152 53206908 xthirioux
    (* Substitute all occurences of variables by their definition in env *)
153 94c457b7 ploc
    let (e_salsa: Salsa.Types.expression), _ = 
154 53206908 xthirioux
      Salsa.Rewrite.substVars 
155
	e_salsa
156 642e116d ploc
	(FormalEnv.to_salsa constEnv formalEnv)
157 53206908 xthirioux
	0 (* TODO: Nasrine, what is this integer value for ? *)
158
    in
159 642e116d ploc
160 8e6cab20 ploc
    (* Format.eprintf "Apres %a@." MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ;   *)
161 642e116d ploc
162 94c457b7 ploc
    (* if !debug then Format.eprintf "Substituted def in expr@ "; *)
163 68322df3 ploc
    let abstractEnv = RangesInt.to_abstract_env ranges in
164 53206908 xthirioux
    (* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id) abstractEnv; *)
165
    (* The expression is partially evaluated by the available ranges
166
       valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on
167
       garde evalPartExpr remplace les variables e qui sont dans env par la cst
168
       - on garde *)
169 94c457b7 ploc
    (* if !debug then Format.eprintf "avant avant eval part@ "; *)
170 8e6cab20 ploc
    (* Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *)
171 53206908 xthirioux
    let e_salsa =  
172 94c457b7 ploc
      Salsa.Analyzer.evalPartExpr 
173 53206908 xthirioux
	e_salsa
174 94c457b7 ploc
	(Salsa.Analyzer.valEnv2ExprEnv abstractEnv) 
175
	([] (* no blacklisted variables *))
176
	([] (* no arrays *))
177 53206908 xthirioux
    in
178 8e6cab20 ploc
    (* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *)
179 53206908 xthirioux
    (* Checking if we have all necessary information *)
180
181 94c457b7 ploc
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
182 53206908 xthirioux
    if Vars.cardinal free_vars > 0 then (
183 94c457b7 ploc
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 
184 68322df3 ploc
	Vars.pp (Vars.fold (fun v accu -> let v' = {v with LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id } in Vars.add v' accu) free_vars Vars.empty)
185 94c457b7 ploc
	MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));
186 8e6cab20 ploc
      if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt  "Some free vars, not optimizing@ ");
187
      if !debug then Log.report ~level:3 (fun fmt -> Format.fprintf fmt "  ranges: %a@ "
188
	RangesInt.pp ranges);
189
190
      (* if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Formal env was @[<v 0>%a@]@ " FormalEnv.pp formalEnv); *)
191
	
192 642e116d ploc
      
193 53206908 xthirioux
      let new_e = try salsa_expr2value_t vars_env constEnv e_salsa   with Not_found -> assert false in
194 68322df3 ploc
      new_e, None, []
195 53206908 xthirioux
    )
196
    else (
197 94c457b7 ploc
      
198 642e116d ploc
      try 
199 94c457b7 ploc
	if !debug then
200 8e6cab20 ploc
	  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Analyzing expression %a with ranges: @[<v>%a@ @]@ "
201 642e116d ploc
	    (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)
202 8e6cab20 ploc
	    (Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv)
203 53206908 xthirioux
	;
204 94c457b7 ploc
205 8e6cab20 ploc
	(* Format.eprintf "going to slice@."; *)
206 68322df3 ploc
	(* Slicing it XXX C'est là !!! ploc *)
207 642e116d ploc
	let e_salsa, seq = Salsa.Rewrite.sliceExpr e_salsa 0 (Salsa.Types.Nop(Salsa.Types.Lab 0)) in
208 8e6cab20 ploc
	(* Format.eprintf "sliced@."; *)
209 68322df3 ploc
	let def_tmps = Salsa.Utils.flatten_seq seq [] in
210
	(* Registering tmp ids in vars_env *)
211
	let vars_env' = List.fold_left
212
	  (fun vs (id, _) ->
213
	    VarEnv.add
214
	      id
215
	      {
216
		vdecl = Corelang.mk_fresh_var
217
		  nodename
218
		  Location.dummy_loc
219
		  e.MT.value_type
220
		  (Clocks.new_var true) ;
221
		is_local = true;
222
	      }
223
	      vs
224
	  )
225
	  vars_env
226
	  def_tmps
227
	in 
228 8e6cab20 ploc
	(* Format.eprintf "List of tmp: @[<v 0>%a@]" *)
229
	(*   ( *)
230
	(*     Utils.fprintf_list *)
231
	(*       ~sep:"@ " *)
232
	(*       (fun fmt (id, e_id) -> *)
233
	(* 	Format.fprintf fmt "(%s,%a) -> %a" *)
234
	(* 	  id *)
235
	(* 	  Printers.pp_var (get_var vars_env' id).vdecl *)
236
	(* 	  (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_id) *)
237
	(*       ) *)
238
	(*   ) *)
239
	(*   def_tmps; *)
240
	(* Format.eprintf "Sliced expression %a@.@?" *)
241
	(*   (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_salsa) *)
242
	(* ; *)
243 68322df3 ploc
244
	(* Optimize def tmp, and build the associated instructions. Update the abstract Env with computed ranges *)
245
	let rev_def_tmp_instrs, ranges =
246
	  List.fold_left (fun (accu_instrs, ranges) (id, e_id) ->
247 8e6cab20 ploc
	    (* Format.eprintf "Cleaning/Optimizing %s@." id; *)
248 68322df3 ploc
	    let abstractEnv = RangesInt.to_abstract_env ranges in
249
	    let e_id', e_range = Salsa.MainEPEG.transformExpression id e_id abstractEnv in
250
251
	    let vdecl = (get_var vars_env' id).vdecl in
252
	    let new_e_id' = try salsa_expr2value_t vars_env' constEnv e_id'  with Not_found -> assert false in
253
	
254
	    let new_local_assign =
255
	      (* let expr = salsa_expr2value_t vars_env' constEnv e_id' in *)
256
	      MT.MLocalAssign(vdecl, new_e_id')
257
	    in
258
	    let new_local_assign = {
259
	      MT.instr_desc = new_local_assign;
260
	      MT.lustre_eq = None (* could be Corelang.mkeq Location.dummy_loc
261
				     ([vdecl.LT.var_id], e_id) provided it is
262
				     converted as Lustre expression rather than
263
				     a Machine code value *);
264
	    }
265
	    in
266
	    let new_ranges = RangesInt.add_def ranges id e_range in
267
	    new_local_assign::accu_instrs, new_ranges
268
	  ) ([], ranges) def_tmps
269
	in
270
271 8e6cab20 ploc
	(* Format.eprintf "Optimizing main expression %s@.AbstractEnv is %a" (Salsa.Print.printExpression e_salsa) RangesInt.pp ranges; *)
272 642e116d ploc
	
273 68322df3 ploc
	let abstractEnv = RangesInt.to_abstract_env ranges in
274 53206908 xthirioux
	let new_e_salsa, e_val = 
275 642e116d ploc
	  Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
276 53206908 xthirioux
	in
277 6b686ae9 Ploc
278 68322df3 ploc
	(* let range_after = Float.evalExpr new_e_salsa abstractEnv in *)
279 6b686ae9 Ploc
280 68322df3 ploc
    	let new_e = try salsa_expr2value_t vars_env' constEnv new_e_salsa   with Not_found -> assert false in
281 8e6cab20 ploc
	if !debug then Log.report ~level:2 (fun fmt ->
282
	  let old_range = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in
283
	  match RangesInt.Value.leq old_range e_val, RangesInt.Value.leq e_val old_range with
284
	  | true, true -> Format.fprintf fmt "No improvement on abstract value %a@ " RangesInt.pp_val e_val
285
	  | true, false -> (
286
	    Format.fprintf fmt "Improved!";
287
	    Format.fprintf fmt
288
	      "  @[<v>old_expr: @[<v 0>%a@ range: %a@]@ new_expr: @[<v 0>%a@ range: %a@]@ @]@ "
289
	      MC.pp_val e
290
	      RangesInt.pp_val (Salsa.Analyzer.evalExpr e_salsa abstractEnv [])
291
	      MC.pp_val new_e
292
	      RangesInt.pp_val e_val
293
	  )
294
	  | false, true -> Format.eprintf "Error; new range is worse!@.@?"; assert false
295
	  | false, false -> Format.eprintf "Error; new range is not comparabe with old end. This should not happen!@.@?"; assert false
296
	);
297 68322df3 ploc
	new_e, Some e_val, List.rev rev_def_tmp_instrs
298 642e116d ploc
      with (* Not_found ->  *)
299 53206908 xthirioux
      | Salsa.Epeg_types.EPEGError _ -> (
300 8e6cab20 ploc
	Log.report ~level:2 (fun fmt -> Format.fprintf fmt "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e);
301 68322df3 ploc
	e, None, []
302 53206908 xthirioux
      )
303
    )
304
305
306 8e6cab20 ploc
    
307 53206908 xthirioux
  in
308 8e6cab20 ploc
  opt_expr vars_env ranges formalEnv e  
309 53206908 xthirioux
    
310
    
311
(* Returns a list of assign, for each var in vars_to_print, that produce the
312
   definition of it according to formalEnv, and driven by the ranges. *)
313 642e116d ploc
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print =
314 53206908 xthirioux
  (* We print thhe expression in the order of definition *)
315
316
  let ordered_vars = 
317
    List.stable_sort
318
      (FormalEnv.get_sort_fun formalEnv) 
319
      (Vars.elements vars_to_print) 
320
  in
321 8e6cab20 ploc
  if !debug then Log.report ~level:4 (fun fmt -> Format.fprintf fmt
322
    "Printing vars in the following order: [%a]@ "
323
    (Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars);
324
  
325 53206908 xthirioux
  List.fold_right (
326
    fun v (accu_instr, accu_ranges) -> 
327 8e6cab20 ploc
      if !debug then  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Printing assign for variable %s@ " v.LT.var_id);
328 53206908 xthirioux
      try
329
	(* Obtaining unfold expression of v in formalEnv *)
330
	let v_def = FormalEnv.get_def formalEnv v  in
331 68322df3 ploc
	let e, r, il = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv v_def in
332 3ca27bc7 ploc
	let instr_desc = 
333 53206908 xthirioux
	  if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then
334 8446bf03 ploc
	    MT.MLocalAssign(v, e)
335 53206908 xthirioux
	  else
336 8446bf03 ploc
	    MT.MStateAssign(v, e)
337 53206908 xthirioux
	in
338 68322df3 ploc
	il@((Corelang.mkinstr instr_desc)::accu_instr), 
339 53206908 xthirioux
	(match r with 
340
	| None -> ranges 
341
	| Some v_r -> RangesInt.add_def ranges v.LT.var_id v_r)
342
      with FormalEnv.NoDefinition _ -> (
343
	(* It should not happen with C backend, but may happen with Lustre backend *)
344
	if !Options.output = "lustre" then accu_instr, ranges else (Format.eprintf "@?"; assert false)
345
      )
346
  ) ordered_vars ([], ranges)
347
348
(* Main recursive function: modify the instructions list while preserving the
349
   order of assigns for state variables. Returns a quintuple: (new_instrs,
350
   ranges, formalEnv, printed_vars, and remaining vars to be printed) *)
351 642e116d ploc
let rec rewrite_instrs nodename m constEnv  vars_env m instrs ranges formalEnv printed_vars vars_to_print =
352
  let formal_env_def = FormalEnv.def constEnv vars_env in
353 8e6cab20 ploc
  (* Format.eprintf "Rewrite intrs : [%a]@." MC.pp_instrs instrs; *)
354 642e116d ploc
  let assign_vars = assign_vars nodename m constEnv vars_env in
355 8e6cab20 ploc
  (* if !debug then ( *)
356
  (*   Log.report ~level:3 (fun fmt -> Format.fprintf fmt    *)
357
  (*     "Current printed_vars: [%a]@ Vars to print: [%a]@ Formal env is [%a]@ " *)
358
  (*     Vars.pp printed_vars *)
359
  (*     Vars.pp vars_to_print *)
360
  (*     FormalEnv.pp formalEnv) *)
361
  (* ); *)
362 53206908 xthirioux
  match instrs with
363
  | [] -> 
364
     (* End of instruction list: we produce the definition of each variable that
365 68322df3 ploc
	appears in vars_to_print. Each of them should be defined in formalEnv *)
366 8e6cab20 ploc
     (* if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print; *)
367 68322df3 ploc
    let instrs, ranges' = assign_vars printed_vars ranges formalEnv vars_to_print in
368
    instrs,
369
    ranges',     
370
    formalEnv,
371
    Vars.union printed_vars vars_to_print, (* We should have printed all required vars *)
372
    []          (* No more vars to be printed *)
373 53206908 xthirioux
374
  | hd_instr::tl_instrs -> 
375
     (* We reformulate hd_instr, producing or not a fresh instruction, updating
376 68322df3 ploc
	formalEnv, possibly ranges and vars_to_print *)
377 53206908 xthirioux
     begin
378
       let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print =
379 3ca27bc7 ploc
	 match Corelang.get_instr_desc hd_instr with 
380 8446bf03 ploc
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type  && not (Vars.mem vd vars_to_print) -> 
381 68322df3 ploc
	   (* LocalAssign are injected into formalEnv *)
382
	   (* if !debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; *)
383 8e6cab20 ploc
	   (* if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
384 68322df3 ploc
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
385
	   [],                        (* no instr generated *)
386
	   ranges,                    (* no new range computed *)
387
	   formalEnv',
388
	   printed_vars,              (* no new printed vars *)
389
	   vars_to_print              (* no more or less variables to print *)
390
	     
391 8446bf03 ploc
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
392 53206908 xthirioux
393 68322df3 ploc
           (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
394
           (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
395 8e6cab20 ploc
           (* if !debug then ( *)
396
	   (*   Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
397
	   (*   Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd; *)
398
	   (* ); *)
399 642e116d ploc
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)
400 68322df3 ploc
	   let instrs', ranges' = (* printing vd = optimized vt *)
401
	     assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
402
	   in
403
	   instrs',
404
	   ranges',                          (* no new range computed *)
405
	   formalEnv',                       (* formelEnv already updated *)
406
	   Vars.add vd printed_vars,        (* adding vd to new printed vars *)
407
	   Vars.remove vd vars_to_print     (* removed vd from variables to print *)
408 53206908 xthirioux
409 8446bf03 ploc
	 | MT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print  *)-> 
410 53206908 xthirioux
411 68322df3 ploc
	   (* StateAssign are produced since they are required by the function. We still
412
	      keep their definition in the formalEnv in case it can optimize later
413
	      outputs. vd is removed from remaining vars_to_print *)
414
	   (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
415 8e6cab20 ploc
           (* if !debug then ( *)
416
	   (*   Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
417
	   (*   Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd; *)
418
	   (* ); *)
419 68322df3 ploc
	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
420
	   let instrs', ranges' = (* printing vd = optimized vt *)
421
	     assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  
422
	   in
423
	   instrs',
424
	   ranges',                          (* no new range computed *)
425
	   formalEnv,                       (* formelEnv already updated *)
426
	   Vars.add vd printed_vars,        (* adding vd to new printed vars *)
427
	   Vars.remove vd vars_to_print     (* removed vd from variables to print *)
428 53206908 xthirioux
429 8446bf03 ploc
	 | (MT.MLocalAssign(vd,vt) | MT.MStateAssign(vd,vt))  ->
430 8e6cab20 ploc
	    (* Format.eprintf "other assign %a@." MC.pp_instr hd_instr; *)
431 94c457b7 ploc
432 68322df3 ploc
	   (* We have to produce the instruction. But we may have to produce as
433
	      well its dependencies *)
434
	   let required_vars = get_expr_real_vars vt in
435
	   let required_vars = Vars.diff required_vars printed_vars in (* remove
436
									  already
437
									  produced
438
									  variables *)
439 8e6cab20 ploc
	   (* Format.eprintf "Required vars: %a@." Vars.pp required_vars; *)
440 68322df3 ploc
	   let required_vars = Vars.diff required_vars (Vars.of_list m.MT.mmemory) in
441
	   let prefix_instr, ranges = 
442
	     assign_vars printed_vars ranges formalEnv required_vars in
443
444
	   let vt', _, il = optimize_expr nodename m constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in
445
	   let new_instr = 
446
	     match Corelang.get_instr_desc hd_instr with
447
	     | MT.MLocalAssign _ -> Corelang.update_instr_desc hd_instr (MT.MLocalAssign(vd,vt'))
448
	     | _ -> Corelang.update_instr_desc hd_instr (MT.MStateAssign(vd,vt'))
449
	   in
450
	   let written_vars = Vars.add vd required_vars in
451
	   prefix_instr@il@[new_instr],
452
	   ranges,                          (* no new range computed *)
453
	   formalEnv,                       (* formelEnv untouched *)
454
	   Vars.union written_vars printed_vars,  (* adding vd + dependencies to
455
						     new printed vars *)
456
	   Vars.diff vars_to_print written_vars (* removed vd + dependencies from
457
						   variables to print *)
458 53206908 xthirioux
459 8446bf03 ploc
	 | MT.MStep(vdl,id,vtl) ->
460 8e6cab20 ploc
	    (* Format.eprintf "step@."; *)
461 94c457b7 ploc
462 8e6cab20 ploc
	   (* if !debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr; *)
463 68322df3 ploc
	   (* Call of an external function. Input expressions have to be
464
	      optimized, their free variables produced. A fresh range has to be
465
	      computed for each output variable in vdl. Output of the function
466
	      call are removed from vars to be printed *)
467
	   let node =  called_node_id m id in
468
	   let node_id = Corelang.node_name node in
469
	   let tin, tout =  (* special care for arrow *)
470
	     if node_id = "_arrow" then
471
	       match vdl with 
472
	       | [v] -> let t = v.LT.var_type in
473
			[t; t], [t]
474
	       | _ -> assert false (* should not happen *)
475
	     else
476
	       fun_types node
477
	   in
478 8e6cab20 ploc
	   (* if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; *)
479 68322df3 ploc
	   let vtl', vtl_ranges, il = List.fold_right2 (
480
	     fun e typ_e (exprl, range_l, il_l)-> 
481
	       if Types.is_real_type typ_e then
482
		 let e', r', il = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e in
483
		 e'::exprl, r'::range_l, il@il_l
484
	       else 
485
		 e::exprl, None::range_l, il_l
486
	   ) vtl tin ([], [], []) 
487
	   in 
488 8e6cab20 ploc
	   (* if !debug then Format.eprintf "... done@ @]@ "; *)
489 68322df3 ploc
490
491
492
	   (* let required_vars =  *)
493
	   (*   List.fold_left2  *)
494
	   (*     (fun accu e typ_e ->  *)
495
	   (* 	 if Types.is_real_type typ_e then *)
496
	   (* 	   Vars.union accu (get_expr_real_vars e)  *)
497
	   (* 	 else (\* we do not consider non real expressions *\) *)
498
	   (* 	   accu *)
499
	   (*     ) *)
500
 	   (*     Vars.empty  *)
501
	   (*     vtl' tin *)
502
	   (* in *)
503
	   (* if !debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ " *)
504
	   (*   Vars.pp required_vars  *)
505
	   (*   Vars.pp printed_vars *)
506
	   (*   Vars.pp (Vars.diff required_vars printed_vars) *)
507
	   (* ; *)
508
	   (* let required_vars = Vars.diff required_vars printed_vars in (\* remove *)
509
	   (* 								  already *)
510
	   (* 								  produced *)
511
	   (* 								  variables *\) *)
512
	   (* let written_vars = Vars.union required_vars (Vars.of_list vdl) in *)
513
	   (* let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in *)
514
515
	   (* instrs' @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *) *)
516
517
	   let written_vars = Vars.of_list vdl in
518
	   
519
520
	   
521
	   il @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *)
522
	   RangesInt.add_call ranges vdl id vtl_ranges,   (* add information bounding each vdl var *) 
523
	   formalEnv,
524
	   Vars.union written_vars printed_vars,        (* adding vdl to new printed vars *)
525
	   Vars.diff vars_to_print written_vars
526
	     
527 8446bf03 ploc
	 | MT.MBranch(vt, branches) ->
528 94c457b7 ploc
	    
529 53206908 xthirioux
	    (* Required variables to compute vt are introduced. 
530 68322df3 ploc
	       Then each branch is refactored specifically 
531
	    *)
532 8e6cab20 ploc
	    (* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; *)
533 68322df3 ploc
	   let required_vars = get_expr_real_vars vt in
534
	   let required_vars = Vars.diff required_vars printed_vars in (* remove
535
									  already
536
									  produced
537
									  variables *)
538
	   let vt', _, prefix_instr = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv vt in
539
540
	   (* let prefix_instr, ranges =  *)
541
	   (*   assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in *)
542
543
	   let printed_vars = Vars.union printed_vars required_vars in
544
545
546
	   let read_vars_tl = get_read_vars tl_instrs in
547 8e6cab20 ploc
	   (* if !debug then Format.eprintf "@[<v 2>Dealing with branches@ "; *)
548 68322df3 ploc
	   let branches', written_vars, merged_ranges = List.fold_right (
549
	     fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges) -> 
550
	       let b_write_vars = get_written_vars b_instrs in
551
	       let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in 
552
	       let b_fe = formalEnv in               (* because of side effect
553
							data, we copy it for
554
							each branch *)
555
	       let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars = 
556
		 rewrite_instrs nodename m constEnv  vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
557
	       in
558
	       (* b_vars should be empty *)
559
	       let _ = if b_vars != [] then assert false in
560
	       
561
	       (* Producing the refactored branch *)
562
	       (b_l, b_instrs') :: new_branches,
563
	       Vars.union b_printed written_vars, (* They should coincides. We
564
						     use union instead of
565
						     inter to ease the
566
						     bootstrap *)
567
	       RangesInt.merge merged_ranges b_ranges      
568
		 
569
	   ) branches ([], required_vars, ranges) in
570 8e6cab20 ploc
	   (* if !debug then Format.eprintf "dealing with branches done@ @]@ ";	   *)
571 68322df3 ploc
	   prefix_instr@[Corelang.update_instr_desc hd_instr (MT.MBranch(vt', branches'))],
572
	     merged_ranges, (* Only step functions call within branches
573
			       may have produced new ranges. We merge this data by
574
			       computing the join per variable *)
575
	     formalEnv,    (* Thanks to the computation of var_to_print in each
576
			      branch, no new definition should have been computed
577
			      without being already printed *)
578
	     Vars.union written_vars printed_vars,
579
	     Vars.diff vars_to_print written_vars (* We remove vars that have been
580
						     produced within branches *)
581 53206908 xthirioux
582
583 8446bf03 ploc
	 | MT.MReset(_) | MT.MNoReset _ | MT.MComment _ ->
584 8e6cab20 ploc
	    (* if !debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr; *)
585 68322df3 ploc
586
	   (* Untouched instruction *)
587
	   [ hd_instr ],                    (* unmodified instr *)
588
	      ranges,                          (* no new range computed *)
589
	      formalEnv,                       (* no formelEnv update *)
590
	      printed_vars,
591
	      vars_to_print                    (* no more or less variables to print *)
592
		
593 53206908 xthirioux
       in
594
       let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print = 
595
	 rewrite_instrs 
596
	   nodename
597 642e116d ploc
	   m
598 53206908 xthirioux
	   constEnv 	  
599
	   vars_env
600
	   m 
601
	   tl_instrs
602
	   ranges
603
	   formalEnv
604
	   printed_vars
605
	   vars_to_print
606
       in
607
       hd_instrs @ tl_instrs,
608
       ranges,
609
       formalEnv, 
610
       printed_vars,
611
       vars_to_print 
612
     end
613
614
615
616
617
618
619
(* TODO: deal with new variables, ie. tmp *)
620
let salsaStep constEnv  m s = 
621
  let ranges = RangesInt.empty (* empty for the moment, should be build from
622
				  machine annotations or externally provided information *) in
623
  let annots = List.fold_left (
624
    fun accu annl -> 
625
      List.fold_left (
626
	fun accu (key, range) ->
627
	  match key with 
628
	  | ["salsa"; "ranges"; var] -> (var, range)::accu
629
	  | _ -> accu
630
      ) accu annl.LT.annots
631 089f94be ploc
  ) [] m.MT.mannot
632 53206908 xthirioux
  in
633
  let ranges = 
634
    List.fold_left (fun ranges (v, value) ->
635
      match value.LT.eexpr_qfexpr.LT.expr_desc with 
636
      | LT.Expr_tuple [minv; maxv] -> (
637
	let get_cst e = match e.LT.expr_desc with 
638
	  | LT.Expr_const (LT.Const_real (c,e,s)) -> 
639
	    (* calculer la valeur c * 10^e *) 
640 94c457b7 ploc
	    Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))
641 53206908 xthirioux
	  | _ -> 
642
	    Format.eprintf 
643 8e6cab20 ploc
	      "Invalid salsa range: %a. It should be a pair of constant floats and %a is not a float.@." 
644
	      Printers.pp_expr value.LT.eexpr_qfexpr
645
	      Printers.pp_expr e
646
	    ; 
647 53206908 xthirioux
	    assert false 
648
	in
649 151117f7 ploc
	(* let minv = Salsa.Float.Domain.of_num (get_cst minv) and *)
650
	(*     maxv = Salsa.Float.Domain.of_num (get_cst maxv) in *)
651 642e116d ploc
	(* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv); *)
652 151117f7 ploc
	RangesInt.enlarge ranges v (Salsa.Float.Domain.inject_nums (get_cst minv) (get_cst maxv))
653 53206908 xthirioux
      )
654
      | _ -> 
655
	Format.eprintf 
656 8e6cab20 ploc
	  "Invalid salsa range: %a. It should be a pair of floats.@." 
657 53206908 xthirioux
	  Printers.pp_expr value.LT.eexpr_qfexpr; 
658
	assert false
659
    ) ranges annots
660
  in
661
  let formal_env = FormalEnv.empty () in
662
  let vars_to_print =
663
    Vars.real_vars  
664
      (
665
	Vars.union 
666 089f94be ploc
	  (Vars.of_list m.MT.mmemory) 
667
	  (Vars.of_list s.MT.step_outputs) 
668 53206908 xthirioux
      )
669
  in 
670
  (* TODO: should be at least step output + may be memories *)
671 9b8acef5 ploc
  
672 94c457b7 ploc
  let vars_env = compute_vars_env m in  
673 8e6cab20 ploc
  (* if !debug then Format.eprintf "@[<v 2>Registering node equations@ ";  *)
674 53206908 xthirioux
  let new_instrs, _, _, printed_vars, _ = 
675
    rewrite_instrs
676 68322df3 ploc
      m.MT.mname
677 642e116d ploc
      m
678 53206908 xthirioux
      constEnv 
679
      vars_env
680
      m
681 089f94be ploc
      s.MT.step_instrs
682 53206908 xthirioux
      ranges
683
      formal_env
684 089f94be ploc
      (Vars.real_vars (Vars.of_list s.MT.step_inputs (* printed_vars : real
685 53206908 xthirioux
							inputs are considered as
686
							already printed *)))
687
      vars_to_print 
688
  in
689 089f94be ploc
  let all_local_vars = Vars.real_vars (Vars.of_list s.MT.step_locals) in
690 53206908 xthirioux
  let unused = (Vars.diff all_local_vars printed_vars) in
691
  let locals =
692
    if not (Vars.is_empty unused) then (
693 8e6cab20 ploc
      if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt  "Unused local vars: [%a]. Removing them.@ "
694
	Vars.pp unused);
695 089f94be ploc
      List.filter (fun v -> not (Vars.mem v unused)) s.MT.step_locals
696 53206908 xthirioux
    )
697
    else
698 089f94be ploc
      s.MT.step_locals
699 53206908 xthirioux
  in
700 089f94be ploc
  { s with MT.step_instrs = new_instrs; MT.step_locals = locals } (* we have also to modify local variables to declare new vars *)
701 53206908 xthirioux
702
703 94c457b7 ploc
let machine_t2machine_t_optimized_by_salsa constEnv  mt =
704 53206908 xthirioux
  try
705 8e6cab20 ploc
    if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@[<v 3>[salsa] Optimizing machine %s@ " mt.MT.mname.LT.node_id);
706 089f94be ploc
    let new_step = salsaStep constEnv  mt mt.MT.mstep in
707 8e6cab20 ploc
    if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@]@ ");
708 089f94be ploc
    { mt with MT.mstep = new_step } 
709 53206908 xthirioux
    
710
      
711
  with FormalEnv.NoDefinition v as exp -> 
712
    Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v; 
713
    raise exp
714
715
716
(* Local Variables: *)
717
(* compile-command:"make -C ../../.." *)
718
(* End: *)