Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/plugins/salsa/machine_salsa_opt.ml
6 6

  
7 7
(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *)
8 8
open SalsaDatatypes
9
   
10
let report = Log.report ~plugin:"salsa" ~verbose_level:Salsa.Log.verbose_level 
9

  
10
let report = Log.report ~plugin:"salsa" ~verbose_level:Salsa.Log.verbose_level
11

  
11 12
(******************************************************************)
12 13
(* TODO Xavier: should those functions be declared more globally? *)
13 14

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

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

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

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

  
67 75
let rec get_written_vars instrs =
68 76
  let open MT in
69 77
  match instrs with
70
    [] -> Vars.empty
71
  | i::tl -> (
72
    let vars_tl = get_written_vars tl in 
78
  | [] ->
79
    Vars.empty
80
  | i :: tl -> (
81
    let vars_tl = get_written_vars tl in
73 82
    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
  )
83
    | MLocalAssign (v, _) | MStateAssign (v, _) ->
84
      Vars.add v vars_tl
85
    | MStep (vdl, _, _) ->
86
      List.fold_left (fun accu v -> Vars.add v accu) vars_tl vdl
87
    | MBranch (_, branches) ->
88
      List.fold_left
89
        (fun vars (_, b) -> Vars.union vars (get_written_vars b))
90
        vars_tl branches
91
    | MReset _ | MNoReset _ | MSpec _ | MComment _ ->
92
      Vars.empty)
84 93

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

  
92 101
(*     iterTransformExpr fresh_id new_expr abstractEnv new_range *)
93 102
(*   else *)
94 103
(*     new_expr, new_range *)
95 104

  
96

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

  
110
    (* TODO more meaningful name *)
102 111
    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 = 
112
    report ~level:2 (fun fmt ->
113
        Format.fprintf fmt "Launching analysis: %s@ "
114
          (Salsa.Print.printExpression e_salsa));
115
    let new_e_salsa, e_val =
107 116
      Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
108 117
    in
109
    report ~level:2 (fun fmt -> Format.fprintf fmt " Analysis done: %s@ "
110
      (Salsa.Print.printExpression new_e_salsa));
111

  
118
    report ~level:2 (fun fmt ->
119
        Format.fprintf fmt " Analysis done: %s@ "
120
          (Salsa.Print.printExpression new_e_salsa));
112 121

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

  
121 130
    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
      )
131
    let expr, expr_range =
132
      match
133
        RangesInt.Value.leq old_val e_val, RangesInt.Value.leq e_val old_val
134
      with
135
      | true, true ->
136
        if !debug then
137
          report ~level:2 (fun fmt ->
138
              Format.fprintf fmt "No improvement on abstract value %a@ "
139
                RangesInt.pp_val e_val);
140
        e_salsa, Some old_val
141
      | false, true ->
142
        if !debug then
143
          report ~level:2 (fun fmt -> Format.fprintf fmt "Improved!@ ");
144
        new_e_salsa, Some e_val
136 145
      | 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 146
        report ~level:2 (fun fmt ->
144 147
            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
      )
148
              "CAREFUL --- new range is worse!. Restoring provided expression@ ");
149
        e_salsa, Some old_val
150
      | false, false ->
151
        report ~level:2 (fun fmt ->
152
            Format.fprintf fmt
153
              "Error; new range is not comparable with old end. It may need \
154
               some investigation!@. ";
155
            Format.fprintf fmt "old: %a@.new: %a@ " RangesInt.pp_val old_val
156
              RangesInt.pp_val e_val);
157

  
158
        new_e_salsa, Some e_val
159
      (* assert false *)
153 160
    in
154 161
    report ~level:2 (fun fmt -> Format.fprintf fmt " Computing range done@ ");
155 162

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

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

  
244
    (* Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val
245
       (salsa_expr2value_t vars_env [](\* constEnv *\) e_salsa) ; *)
234 246

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

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

  
241 255
    (* 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 ? *)
256
    let (e_salsa : Salsa.Types.expression), _ =
257
      Salsa.Rewrite.substVars e_salsa (FormalEnv.to_salsa constEnv formalEnv) 0
258
      (* TODO: Nasrine, what is this integer value for ? *)
247 259
    in
248 260

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

  
251 264
    (* if !debug then Format.eprintf "Substituted def in expr@ "; *)
252 265
    let abstractEnv = RangesInt.to_abstract_env ranges in
......
256 269
       garde evalPartExpr remplace les variables e qui sont dans env par la cst
257 270
       - on garde *)
258 271
    (* 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 *))
272
    (* Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t
273
       vars_env constEnv e_salsa); *)
274
    let e_salsa =
275
      Salsa.Analyzer.evalPartExpr e_salsa
276
        (Salsa.Analyzer.valEnv2ExprEnv abstractEnv)
277
        [] (* no blacklisted variables *) []
278
      (* no arrays *)
266 279
    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 280

  
281
    (* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t
282
       vars_env constEnv e_salsa); *)
283
    (* Checking if we have all necessary information *)
270 284
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
271 285
    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
    )
286
      report ~level:2 (fun fmt ->
287
          Format.fprintf fmt
288
            "Warning: unbounded free vars (%a) in expression %a. We do not \
289
             optimize it.@ "
290
            Vars.pp
291
            (Vars.fold
292
               (fun v accu ->
293
                 let v' =
294
                   {
295
                     v with
296
                     LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id;
297
                   }
298
                 in
299
                 Vars.add v' accu)
300
               free_vars Vars.empty)
301
            (MC.pp_val m)
302
            (salsa_expr2value_t vars_env constEnv e_salsa));
303
      if !debug then
304
        report ~level:2 (fun fmt ->
305
            Format.fprintf fmt "Some free vars, not optimizing@ ");
306
      if !debug then
307
        report ~level:3 (fun fmt ->
308
            Format.fprintf fmt "  ranges: %a@ " RangesInt.pp ranges);
309

  
310
      (* if !debug then Log.report ~level:2 (fun fmt -> Format.fprintf fmt
311
         "Formal env was @[<v 0>%a@]@ " FormalEnv.pp formalEnv); *)
312
      let new_e =
313
        try salsa_expr2value_t vars_env constEnv e_salsa
314
        with Not_found -> assert false
315
      in
316
      new_e, None, [], Vars.empty)
289 317
    else (
290
      
291 318
      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
    
319
        report ~level:3 (fun fmt ->
320
            Format.fprintf fmt
321
              "@[<v 2>Analyzing expression %a@  with ranges: @[<v>%a@ @]@ @]@ "
322
              (C_backend_common.pp_c_val m ""
323
                 (C_backend_common.pp_c_var_read m))
324
              (salsa_expr2value_t vars_env constEnv e_salsa)
325
              (Utils.fprintf_list ~sep:",@ " (fun fmt (l, r) ->
326
                   Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r))
327
              abstractEnv);
328

  
329
      (* Slicing expression *)
330
      let e_salsa, seq =
331
        try
332
          Salsa.Rewrite.sliceExpr e_salsa 0
333
            (Salsa.Types.Nop (Salsa.Types.Lab 0))
334
        with _ ->
335
          Format.eprintf "Issues rewriting express %s@.@?"
336
            (Salsa.Print.printExpression e_salsa);
337
          assert false
338
      in
339
      let def_tmps = Salsa.Utils.flatten_seq seq [] in
340
      (* Registering tmp ids in vars_env *)
341
      let vars_env', new_local_vars =
342
        List.fold_left
343
          (fun (vs, vars) (id, _) ->
344
            let vdecl =
345
              Corelang.mk_fresh_var (nodename.node_id, [])
346
                (* TODO check that the empty env is ok. One may need to build or
347
                   access to the current env *)
348
                Location.dummy_loc e.MT.value_type (Clocks.new_var true)
349
            in
350

  
351
            let vs' = VarEnv.add id { vdecl; is_local = true } vs in
352
            let vars' = Vars.add vdecl vars in
353
            vs', vars')
354
          (vars_env, Vars.empty) def_tmps
355
      in
356
      (* Debug *)
357
      if !debug then
358
        report ~level:3 (fun fmt ->
359
            Format.fprintf fmt "List of slices: @[<v 0>%a@]@ "
360
              (Utils.fprintf_list ~sep:"@ " (fun fmt (id, e_id) ->
361
                   Format.fprintf fmt "(%s,%a) -> %a" id Printers.pp_var
362
                     (get_var vars_env' id).vdecl
363
                     (C_backend_common.pp_c_val m ""
364
                        (C_backend_common.pp_c_var_read m))
365
                     (salsa_expr2value_t vars_env' constEnv e_id)))
366
              def_tmps;
367
            Format.fprintf fmt "Sliced expression: %a@ "
368
              (C_backend_common.pp_c_val m ""
369
                 (C_backend_common.pp_c_var_read m))
370
              (salsa_expr2value_t vars_env' constEnv e_salsa));
371

  
372
      (* Debug *)
373

  
374
      (* Optimize def tmp, and build the associated instructions. Update the
375
         abstract Env with computed ranges *)
376
      if !debug && List.length def_tmps >= 1 then
377
        report ~level:3 (fun fmt ->
378
            Format.fprintf fmt "@[<v 3>Optimizing sliced sub-expressions@ ");
379
      let rev_def_tmp_instrs, ranges =
380
        List.fold_left
381
          (fun (accu_instrs, ranges) (id, e_id) ->
382
            (* Format.eprintf "Cleaning/Optimizing %s@." id; *)
383
            let e_id', e_range =
384
              (*Salsa.MainEPEG.transformExpression id e_id abstractEnv*)
385
              opt_num_expr_sliced ranges e_id
386
            in
387
            let new_e_id' =
388
              try salsa_expr2value_t vars_env' constEnv e_id'
389
              with Not_found -> assert false
390
            in
391

  
392
            let vdecl = (get_var vars_env' id).vdecl in
393

  
394
            let new_local_assign =
395
              (* let expr = salsa_expr2value_t vars_env' constEnv e_id' in *)
396
              MT.MLocalAssign (vdecl, new_e_id')
397
            in
398
            let new_local_assign =
399
              {
400
                MT.instr_desc = new_local_assign;
401
                MT.lustre_eq =
402
                  None
403
                  (* could be Corelang.mkeq Location.dummy_loc
404
                     ([vdecl.LT.var_id], e_id) provided it is converted as
405
                     Lustre expression rather than a Machine code value *);
406
              }
407
            in
408
            let new_ranges =
409
              match e_range with
410
              | None ->
411
                ranges
412
              | Some e_range ->
413
                RangesInt.add_def ranges id e_range
414
            in
415
            new_local_assign :: accu_instrs, new_ranges)
416
          ([], ranges) def_tmps
417
      in
418
      if !debug && List.length def_tmps >= 1 then
419
        report ~level:3 (fun fmt -> Format.fprintf fmt "@]@ ");
420

  
421
      (* Format.eprintf "Optimizing main expression %s@.AbstractEnv is %a"
422
         (Salsa.Print.printExpression e_salsa) RangesInt.pp ranges; *)
423
      let expr_salsa, expr_range = opt_num_expr_sliced ranges e_salsa in
424
      let expr =
425
        try salsa_expr2value_t vars_env' constEnv expr_salsa
426
        with Not_found -> assert false
427
      in
428

  
429
      expr, expr_range, List.rev rev_def_tmp_instrs, new_local_vars
430
      (* ???? Bout de code dans unstable lors du merge avec salsa ? ====
431

  
432
         let new_e = try salsa_expr2value_t vars_env' constEnv new_e_salsa with
433
         Not_found -> assert false in if !debug then Log.report ~level:2 (fun
434
         fmt -> let old_range = Salsa.Analyzer.evalExpr e_salsa abstractEnv []
435
         in match RangesInt.Value.leq old_range e_val, RangesInt.Value.leq e_val
436
         old_range with | true, true -> Format.fprintf fmt "No improvement on
437
         abstract value %a@ " RangesInt.pp_val e_val | true, false -> (
438
         Format.fprintf fmt "Improved!"; Format.fprintf fmt " @[<v>old_expr:
439
         @[<v 0>%a@ range: %a@]@ new_expr: @[<v 0>%a@ range: %a@]@ @]@ "
440
         (MC.pp_val m) e RangesInt.pp_val (Salsa.Analyzer.evalExpr e_salsa
441
         abstractEnv []) (MC.pp_val m) new_e RangesInt.pp_val e_val ) | false,
442
         true -> Format.eprintf "Error; new range is worse!@.@?"; assert false |
443
         false, false -> Format.eprintf "Error; new range is not comparabe with
444
         old end. This should not happen!@.@?"; assert false ); new_e, Some
445
         e_val, List.rev rev_def_tmp_instrs with (* Not_found -> *) |
446
         Salsa.Epeg_types.EPEGError _ -> ( Log.report ~level:2 (fun fmt ->
447
         Format.fprintf fmt "BECAUSE OF AN ERROR, Expression %a was not
448
         optimized@ " (MC.pp_val m) e); e, None, [] ) >>>>>>> unstable *))
430 449
  in
431
  opt_expr m vars_env ranges formalEnv e  
432
    
433
    
450

  
451
  opt_expr m vars_env ranges formalEnv e
452

  
434 453
(* Returns a list of assign, for each var in vars_to_print, that produce the
435 454
   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 =
455
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv
456
    vars_to_print =
437 457
  (* We print thhe expression in the order of definition *)
438

  
439
  let ordered_vars = 
458
  let ordered_vars =
440 459
    List.stable_sort
441
      (FormalEnv.get_sort_fun formalEnv) 
442
      (Vars.elements vars_to_print) 
460
      (FormalEnv.get_sort_fun formalEnv)
461
      (Vars.elements vars_to_print)
443 462
  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);
463
  if !debug then
464
    report ~level:4 (fun fmt ->
465
        Format.fprintf fmt "Printing vars in the following order: [%a]@ "
466
          (Utils.fprintf_list ~sep:", " Printers.pp_var)
467
          ordered_vars);
468

  
469
  List.fold_right
470
    (fun v (accu_instr, accu_ranges, accu_new_locals) ->
471
      if !debug then
472
        report ~level:4 (fun fmt ->
473
            Format.fprintf fmt "Printing assign for variable %s@ " v.LT.var_id);
451 474
      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)
475
        (* Obtaining unfold expression of v in formalEnv *)
476
        let v_def = FormalEnv.get_def formalEnv v in
477
        let e, r, il, new_v_locals =
478
          optimize_expr nodename m constEnv printed_vars vars_env ranges
479
            formalEnv v_def
480
        in
481
        let instr_desc =
482
          if
483
            try (get_var vars_env v.LT.var_id).is_local
484
            with Not_found -> assert false
485
          then MT.MLocalAssign (v, e)
486
          else MT.MStateAssign (v, e)
487
        in
488
        ( il @ Corelang.mkinstr instr_desc :: accu_instr,
489
          (match r with
490
          | None ->
491
            ranges
492
          | Some v_r ->
493
            RangesInt.add_def ranges v.LT.var_id v_r),
494
          Vars.union accu_new_locals new_v_locals )
495
      with FormalEnv.NoDefinition _ ->
496
        if
497
          (* It should not happen with C backend, but may happen with Lustre
498
             backend *)
499
          !Options.output = "lustre"
500
        then accu_instr, ranges, Vars.empty
501
        else (
502
          Format.eprintf "@?";
503
          assert false))
504
    ordered_vars ([], ranges, Vars.empty)
474 505

  
475 506
(* Main recursive function: modify the instructions list while preserving the
476 507
   order of assigns for state variables. Returns a quintuple: (new_instrs,
477 508
   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 =
509
let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv
510
    printed_vars vars_to_print =
479 511
  let formal_env_def = FormalEnv.def constEnv vars_env in
480 512
  (* Format.eprintf "Rewrite intrs : [%a]@." MC.pp_instrs instrs; *)
481 513
  let assign_vars = assign_vars nodename m constEnv vars_env in
......
487 519
  (*     FormalEnv.pp formalEnv) *)
488 520
  (* ); *)
489 521
  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
522
  | [] ->
523
    (* End of instruction list: we produce the definition of each variable that
524
       appears in vars_to_print. Each of them should be defined in formalEnv *)
525
    (* if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp
526
       vars_to_print; *)
527
    let instrs, ranges', new_expr_locals =
528
      assign_vars printed_vars ranges formalEnv vars_to_print
529
    in
530
    ( instrs,
531
      ranges',
532
      formalEnv,
533
      Vars.union printed_vars vars_to_print,
534
      (* We should have printed all required vars *)
535
      [],
536
      (* No more vars to be printed *)
537
      Vars.empty )
538
  | hd_instr :: tl_instrs ->
539
    (* We reformulate hd_instr, producing or not a fresh instruction, updating
540
       formalEnv, possibly ranges and vars_to_print *)
541
    let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print, hd_new_locals
542
        =
543
      match Corelang.get_instr_desc hd_instr with
544
      | MT.MLocalAssign (vd, vt)
545
        when Types.is_real_type vd.LT.var_type
546
             && not (Vars.mem vd vars_to_print) ->
547
        (* LocalAssign are injected into formalEnv *)
548
        (* if !debug then Format.eprintf "Registering local assign %a@ "
549
           MC.pp_instr hd_instr; *)
550
        (* if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
551
        let formalEnv' = formal_env_def formalEnv vd vt in
552
        (* formelEnv updated with vd = vt *)
553
        ( [],
554
          (* no instr generated *)
555
          ranges,
556
          (* no new range computed *)
557
          formalEnv',
558
          printed_vars,
559
          (* no new printed vars *)
560
          vars_to_print,
561
          (* no more or less variables to print *)
562
          Vars.empty )
563
      (* no new locals *)
564
      | MT.MLocalAssign (vd, vt)
565
        when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
566
        (* if !debug then Format.eprintf "Registering and producing state assign
567
           %a@ " MC.pp_instr hd_instr; *)
568
        (* if !debug then Format.eprintf "Registering and producing state assign
569
           %a@ " MC.pp_instr hd_instr; *)
570
        (* if !debug then ( *)
571
        (*   Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
572
        (* Format.eprintf "Selected var %a: producing expression@ "
573
           Printers.pp_var vd; *)
574
        (* ); *)
575
        let formalEnv' = formal_env_def formalEnv vd vt in
576
        (* formelEnv updated with vd = vt *)
577
        let instrs', ranges', expr_new_locals =
578
          (* printing vd = optimized vt *)
579
          assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)
580
        in
581
        ( instrs',
582
          ranges',
583
          (* no new range computed *)
584
          formalEnv',
585
          (* formelEnv already updated *)
586
          Vars.add vd printed_vars,
587
          (* adding vd to new printed vars *)
588
          Vars.remove vd vars_to_print,
589
          (* removed vd from variables to print *)
590
          expr_new_locals )
591
      (* adding sliced vardecl to the list *)
592
      | MT.MStateAssign (vd, vt)
593
        when Types.is_real_type vd.LT.var_type
594
             (* && Vars.mem vd vars_to_print *) ->
595
        (* StateAssign are produced since they are required by the function. We
596
           still keep their definition in the formalEnv in case it can optimize
597
           later outputs. vd is removed from remaining vars_to_print *)
598
        (* if !debug then Format.eprintf "Registering and producing state assign
599
           %a@ " MC.pp_instr hd_instr; *)
600
        (* if !debug then ( *)
601
        (*   Format.eprintf "%a@ " MC.pp_instr hd_instr; *)
602
        (* Format.eprintf "State assign %a: producing expression@ "
603
           Printers.pp_var vd; *)
604
        (* ); *)
605
        let formalEnv' = formal_env_def formalEnv vd vt in
606
        (* formelEnv updated with vd = vt *)
607
        let instrs', ranges', expr_new_locals =
608
          (* printing vd = optimized vt *)
609
          assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)
610
        in
611
        ( instrs',
612
          ranges',
613
          (* no new range computed *)
614
          formalEnv,
615
          (* formelEnv already updated *)
616
          Vars.add vd printed_vars,
617
          (* adding vd to new printed vars *)
618
          Vars.remove vd vars_to_print,
619
          (* removed vd from variables to print *)
620
          expr_new_locals )
621
      (* adding sliced vardecl to the list *)
622
      | MT.MLocalAssign (vd, vt) | MT.MStateAssign (vd, vt) ->
623
        (* Format.eprintf "other assign %a@." MC.pp_instr hd_instr; *)
624

  
625
        (* We have to produce the instruction. But we may have to produce as
626
           well its dependencies *)
627
        let required_vars = get_expr_real_vars vt in
628
        let required_vars = Vars.diff required_vars printed_vars in
629
        (* remove already produced variables *)
630
        (* Format.eprintf "Required vars: %a@." Vars.pp required_vars; *)
631
        let required_vars =
632
          Vars.diff required_vars (Vars.of_list m.MT.mmemory)
633
        in
634
        let prefix_instr, ranges, new_expr_dep_locals =
635
          assign_vars printed_vars ranges formalEnv required_vars
636
        in
756 637

  
638
        let vt', _, il, expr_new_locals =
639
          optimize_expr nodename m constEnv
640
            (Vars.union required_vars printed_vars)
641
            vars_env ranges formalEnv vt
642
        in
643
        let new_instr =
644
          match Corelang.get_instr_desc hd_instr with
645
          | MT.MLocalAssign _ ->
646
            Corelang.update_instr_desc hd_instr (MT.MLocalAssign (vd, vt'))
647
          | _ ->
648
            Corelang.update_instr_desc hd_instr (MT.MStateAssign (vd, vt'))
649
        in
650
        let written_vars = Vars.add vd required_vars in
651
        ( prefix_instr @ il @ [ new_instr ],
652
          ranges,
653
          (* no new range computed *)
654
          formalEnv,
655
          (* formelEnv untouched *)
656
          Vars.union written_vars printed_vars,
657
          (* adding vd + dependencies to new printed vars *)
658
          Vars.diff vars_to_print written_vars,
659
          (* removed vd + dependencies from variables to print *)
660
          Vars.union new_expr_dep_locals expr_new_locals )
661
      | MT.MStep (vdl, id, vtl) ->
662
        (* Format.eprintf "step@."; *)
663

  
664
        (* if !debug then Format.eprintf "Call to a node %a@ " MC.pp_instr
665
           hd_instr; *)
666
        (* Call of an external function. Input expressions have to be optimized,
667
           their free variables produced. A fresh range has to be computed for
668
           each output variable in vdl. Output of the function call are removed
669
           from vars to be printed *)
670
        let node = called_node_id m id in
671
        let node_id = Corelang.node_name node in
672
        let tin, tout =
673
          (* special care for arrow *)
674
          if node_id = "_arrow" then
675
            match vdl with
676
            | [ v ] ->
677
              let t = v.LT.var_type in
678
              [ t; t ], [ t ]
679
            | _ ->
680
              assert false (* should not happen *)
681
          else fun_types node
682
        in
683
        (* if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; *)
684
        let vtl', vtl_ranges, il, args_new_locals =
685
          List.fold_right2
686
            (fun e typ_e (exprl, range_l, il_l, new_locals) ->
687
              if Types.is_real_type typ_e then
688
                let e', r', il, new_expr_locals =
689
                  optimize_expr nodename m constEnv printed_vars vars_env ranges
690
                    formalEnv e
691
                in
692
                ( e' :: exprl,
693
                  r' :: range_l,
694
                  il @ il_l,
695
                  Vars.union new_locals new_expr_locals )
696
              else e :: exprl, None :: range_l, il_l, new_locals)
697
            vtl tin ([], [], [], Vars.empty)
698
        in
757 699

  
700
        (* if !debug then Format.eprintf "... done@ @]@ "; *)
701

  
702
        (* let required_vars =  *)
703
        (*   List.fold_left2  *)
704
        (*     (fun accu e typ_e ->  *)
705
        (* 	 if Types.is_real_type typ_e then *)
706
        (* 	   Vars.union accu (get_expr_real_vars e)  *)
707
        (* 	 else (\* we do not consider non real expressions *\) *)
708
        (* 	   accu *)
709
        (*     ) *)
710
        (*     Vars.empty  *)
711
        (*     vtl' tin *)
712
        (* in *)
713
        (* if !debug then Format.eprintf "Required vars: [%a]@ Printed vars:
714
           [%a]@ Remaining required vars: [%a]@ " *)
715
        (*   Vars.pp required_vars  *)
716
        (*   Vars.pp printed_vars *)
717
        (*   Vars.pp (Vars.diff required_vars printed_vars) *)
718
        (* ; *)
719
        (* let required_vars = Vars.diff required_vars printed_vars in (\* remove *)
720
        (* 								  already *)
721
        (* 								  produced *)
722
        (* 								  variables *\) *)
723
        (* let written_vars = Vars.union required_vars (Vars.of_list vdl) in *)
724
        (* let instrs', ranges' = assign_vars (Vars.union written_vars
725
           printed_vars) ranges formalEnv required_vars in *)
726

  
727
        (* instrs' @ [Corelang.update_instr_desc hd_instr
728
           (MT.MStep(vdl,id,vtl'))], (* New instrs *) *)
729
        let written_vars = Vars.of_list vdl in
730

  
731
        ( il @ [ Corelang.update_instr_desc hd_instr (MT.MStep (vdl, id, vtl')) ],
732
          (* New instrs *)
733
          RangesInt.add_call ranges vdl id vtl_ranges,
734
          (* add information bounding each vdl var *)
735
          formalEnv,
736
          Vars.union written_vars printed_vars,
737
          (* adding vdl to new printed vars *)
738
          Vars.diff vars_to_print written_vars,
739
          args_new_locals )
740
      | MT.MBranch (vt, branches) ->
741
        (* Required variables to compute vt are introduced. Then each branch is
742
           refactored specifically *)
743

  
744
        (* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; *)
745
        let required_vars = get_expr_real_vars vt in
746
        let required_vars = Vars.diff required_vars printed_vars in
747
        (* remove already produced variables *)
748
        let vt', _, prefix_instr, prefix_new_locals =
749
          optimize_expr nodename m constEnv printed_vars vars_env ranges
750
            formalEnv vt
751
        in
758 752

  
753
        let new_locals = prefix_new_locals in
754

  
755
        (* let prefix_instr, ranges = *)
756
        (* assign_vars (Vars.union required_vars printed_vars) ranges formalEnv
757
           required_vars in *)
758
        let printed_vars = Vars.union printed_vars required_vars in
759

  
760
        let read_vars_tl = get_read_vars tl_instrs in
761
        (* if !debug then Format.eprintf "@[<v 2>Dealing with branches@ "; *)
762
        let branches', written_vars, merged_ranges, new_locals =
763
          List.fold_right
764
            (fun (b_l, b_instrs)
765
                 (new_branches, written_vars, merged_ranges, new_locals) ->
766
              let b_write_vars = get_written_vars b_instrs in
767
              let b_vars_to_print =
768
                Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print)
769
              in
770
              let b_fe = formalEnv in
771
              (* because of side effect data, we copy it for each branch *)
772
              let ( b_instrs',
773
                    b_ranges,
774
                    b_formalEnv,
775
                    b_printed,
776
                    b_vars,
777
                    b_new_locals ) =
778
                rewrite_instrs nodename m constEnv vars_env m b_instrs ranges
779
                  b_fe printed_vars b_vars_to_print
780
              in
781
              (* b_vars should be empty *)
782
              let _ = if b_vars != [] then assert false in
783

  
784
              (* Producing the refactored branch *)
785
              ( (b_l, b_instrs') :: new_branches,
786
                Vars.union b_printed written_vars,
787
                (* They should coincides. We use union instead of inter to ease
788
                   the bootstrap *)
789
                RangesInt.merge merged_ranges b_ranges,
790
                Vars.union new_locals b_new_locals ))
791
            branches
792
            ([], required_vars, ranges, new_locals)
793
        in
794
        (* if !debug then Format.eprintf "dealing with branches done@ @]@ "; *)
795
        ( prefix_instr
796
          @ [
797
              Corelang.update_instr_desc hd_instr (MT.MBranch (vt', branches'));
798
            ],
799
          merged_ranges,
800
          (* Only step functions call within branches may have produced new
801
             ranges. We merge this data by computing the join per variable *)
802
          formalEnv,
803
          (* Thanks to the computation of var_to_print in each branch, no new
804
             definition should have been computed without being already printed *)
805
          Vars.union written_vars printed_vars,
806
          Vars.diff vars_to_print written_vars
807
          (* We remove vars that have been produced within branches *),
808
          new_locals )
809
      | MT.MReset _ | MT.MNoReset _ | MT.MSpec _ | MT.MComment _ ->
810
        (* if !debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr
811
           hd_instr; *)
812

  
813
        (* Untouched instruction *)
814
        ( [ hd_instr ],
815
          (* unmodified instr *)
816
          ranges,
817
          (* no new range computed *)
818
          formalEnv,
819
          (* no formelEnv update *)
820
          printed_vars,
821
          vars_to_print,
822
          (* no more or less variables to print *)
823
          Vars.empty )
824
      (* no new slides vars *)
825
    in
759 826

  
827
    let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print, tl_new_locals
828
        =
829
      rewrite_instrs nodename m constEnv vars_env m tl_instrs ranges formalEnv
830
        printed_vars vars_to_print
831
    in
760 832

  
833
    ( hd_instrs @ tl_instrs,
834
      ranges,
835
      formalEnv,
836
      printed_vars,
837
      vars_to_print,
838
      Vars.union hd_new_locals tl_new_locals )
761 839

  
762 840
(* 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
841
let salsaStep constEnv m s =
842
  let ranges =
843
    RangesInt.empty
844
    (* empty for the moment, should be build from machine annotations or
845
       externally provided information *)
775 846
  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 r) -> 
782
	     (* calculer la valeur c * 10^e *)
783
             Real.to_num r 
784
	  | _ -> 
785
	    Format.eprintf 
786
	      "Invalid salsa range: %a. It should be a pair of constant floats and %a is not a float.@." 
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff