Project

General

Profile

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

    
7
(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *)
8
open SalsaDatatypes
9

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

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

    
15
let fun_types node =
16
  try
17
    match node.LT.top_decl_desc with
18
    | LT.Node nd ->
19
      let tin, tout = Types.split_arrow nd.LT.node_type in
20
      Types.type_list_of_type tin, Types.type_list_of_type tout
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 =
30
  let td, _ =
31
    try List.assoc id m.MT.mcalls (* TODO Xavier: mcalls or minstances ? *)
32
    with Not_found -> assert false
33
  in
34
  td
35
(******************************************************************)
36

    
37
(* Returns the set of vars that appear in the expression *)
38
let rec get_expr_real_vars e =
39
  let open MT in
40
  match e.value_desc with
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))
48
      Vars.empty args
49
  | Array _ | Access _ | Power _ ->
50
    assert false
51

    
52
(* Extract the variables to appear as free variables in expressions (lhs) *)
53
let rec get_read_vars instrs =
54
  let open MT in
55
  match instrs with
56
  | [] ->
57
    Vars.empty
58
  | i :: tl -> (
59
    let vars_tl = get_read_vars tl in
60
    match Corelang.get_instr_desc i with
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) ->
68
      let vars = Vars.union (get_expr_real_vars e) vars_tl in
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)
74

    
75
let rec get_written_vars instrs =
76
  let open MT in
77
  match instrs with
78
  | [] ->
79
    Vars.empty
80
  | i :: tl -> (
81
    let vars_tl = get_written_vars tl in
82
    match Corelang.get_instr_desc i with
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)
93

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

    
101
(*     iterTransformExpr fresh_id new_expr abstractEnv new_range *)
102
(*   else *)
103
(*     new_expr, new_range *)
104

    
105
(* Takes as input a salsa expression and return an optimized one *)
106
let opt_num_expr_sliced ranges e_salsa =
107
  try
108
    let fresh_id = "toto" in
109

    
110
    (* TODO more meaningful name *)
111
    let abstractEnv = RangesInt.to_abstract_env ranges in
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 =
116
      Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
117
    in
118
    report ~level:2 (fun fmt ->
119
        Format.fprintf fmt " Analysis done: %s@ "
120
          (Salsa.Print.printExpression new_e_salsa));
121

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

    
130
    let old_val = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in
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
145
      | true, false ->
146
        report ~level:2 (fun fmt ->
147
            Format.fprintf fmt
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 *)
160
    in
161
    report ~level:2 (fun fmt -> Format.fprintf fmt " Computing range done@ ");
162

    
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);
174
    expr, expr_range
175
  with (* Not_found -> *)
176
  | Salsa.Epeg_types.EPEGError _ ->
177
    report ~level:2 (fun fmt ->
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 *));
182
    e_salsa, None
183

    
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 =
188
  let rec opt_expr m vars_env ranges formalEnv e =
189
    let open MT in
190
    match e.value_desc with
191
    | Cst cst ->
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 *)
207
    (* (\* optimize only numerical vars *\) *)
208
    (* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges
209
       formalEnv e *)
210
    (* else e, None *)
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; *)
239
    (* Convert expression *)
240
    (* List.iter (fun (l,c) -> Format.eprintf "%s -> %a@ " l Printers.pp_const
241
       c) constEnv; *)
242
    let e_salsa : Salsa.Types.expression = value_t2salsa_expr constEnv e in
243

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

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

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

    
255
    (* Substitute all occurences of variables by their definition in env *)
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 ? *)
259
    in
260

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

    
264
    (* if !debug then Format.eprintf "Substituted def in expr@ "; *)
265
    let abstractEnv = RangesInt.to_abstract_env ranges in
266
    (* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id) abstractEnv; *)
267
    (* The expression is partially evaluated by the available ranges
268
       valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on
269
       garde evalPartExpr remplace les variables e qui sont dans env par la cst
270
       - on garde *)
271
    (* if !debug then Format.eprintf "avant avant eval part@ "; *)
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 *)
279
    in
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 *)
284
    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
285
    if Vars.cardinal free_vars > 0 then (
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)
317
    else (
318
      if !debug then
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 *))
449
  in
450

    
451
  opt_expr m vars_env ranges formalEnv e
452

    
453
(* Returns a list of assign, for each var in vars_to_print, that produce the
454
   definition of it according to formalEnv, and driven by the ranges. *)
455
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv
456
    vars_to_print =
457
  (* We print thhe expression in the order of definition *)
458
  let ordered_vars =
459
    List.stable_sort
460
      (FormalEnv.get_sort_fun formalEnv)
461
      (Vars.elements vars_to_print)
462
  in
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);
474
      try
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)
505

    
506
(* Main recursive function: modify the instructions list while preserving the
507
   order of assigns for state variables. Returns a quintuple: (new_instrs,
508
   ranges, formalEnv, printed_vars, and remaining vars to be printed) *)
509
let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv
510
    printed_vars vars_to_print =
511
  let formal_env_def = FormalEnv.def constEnv vars_env in
512
  (* Format.eprintf "Rewrite intrs : [%a]@." MC.pp_instrs instrs; *)
513
  let assign_vars = assign_vars nodename m constEnv vars_env in
514
  (* if !debug then ( *)
515
  (*   Log.report ~level:3 (fun fmt -> Format.fprintf fmt    *)
516
  (*     "Current printed_vars: [%a]@ Vars to print: [%a]@ Formal env is [%a]@ " *)
517
  (*     Vars.pp printed_vars *)
518
  (*     Vars.pp vars_to_print *)
519
  (*     FormalEnv.pp formalEnv) *)
520
  (* ); *)
521
  match instrs with
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
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
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
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
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
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 )
839

    
840
(* TODO: deal with new variables, ie. tmp *)
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 *)
846
  in
847
  let annots =
848
    List.fold_left
849
      (fun accu annl ->
850
        List.fold_left
851
          (fun accu (key, range) ->
852
            match key with
853
            | [ "salsa"; "ranges"; var ] ->
854
              (var, range) :: accu
855
            | _ ->
856
              accu)
857
          accu annl.LT.annots)
858
      [] m.MT.mannot
859
  in
860
  let ranges =
861
    List.fold_left
862
      (fun ranges (v, value) ->
863
        match value.LT.eexpr_qfexpr.LT.expr_desc with
864
        | LT.Expr_tuple [ minv; maxv ] ->
865
          let get_cst e =
866
            match e.LT.expr_desc with
867
            | LT.Expr_const (LT.Const_real r) ->
868
              (* calculer la valeur c * 10^e *)
869
              Real.to_num r
870
            | _ ->
871
              Format.eprintf
872
                "Invalid salsa range: %a. It should be a pair of constant \
873
                 floats and %a is not a float.@."
874
                Printers.pp_expr value.LT.eexpr_qfexpr Printers.pp_expr e;
875
              assert false
876
          in
877
          (* let minv = Salsa.Float.Domain.of_num (get_cst minv) and *)
878
          (*     maxv = Salsa.Float.Domain.of_num (get_cst maxv) in *)
879
          (* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v
880
             (Num.string_of_num minv) (Num.string_of_num maxv); *)
881
          RangesInt.enlarge ranges v
882
            (Salsa.Float.Domain.inject_nums (get_cst minv) (get_cst maxv))
883
        | _ ->
884
          Format.eprintf
885
            "Invalid salsa range: %a. It should be a pair of floats.@."
886
            Printers.pp_expr value.LT.eexpr_qfexpr;
887
          assert false)
888
      ranges annots
889
  in
890
  let formal_env = FormalEnv.empty () in
891
  let vars_to_print =
892
    Vars.real_vars
893
      (Vars.union (Vars.of_list m.MT.mmemory) (Vars.of_list s.MT.step_outputs))
894
  in
895

    
896
  (* TODO: should be at least step output + may be memories *)
897
  let vars_env = compute_vars_env m in
898
  (* if !debug then Format.eprintf "@[<v 2>Registering node equations@ "; *)
899
  let new_instrs, _, _, printed_vars, _, new_locals =
900
    rewrite_instrs m.MT.mname m constEnv vars_env m s.MT.step_instrs ranges
901
      formal_env
902
      (Vars.real_vars
903
         (Vars.of_list
904
            s.MT.step_inputs
905
            (* printed_vars : real inputs are considered as already printed *)))
906
      vars_to_print
907
  in
908

    
909
  let all_local_vars = Vars.real_vars (Vars.of_list s.MT.step_locals) in
910
  let unused = Vars.diff all_local_vars printed_vars in
911
  let locals =
912
    if not (Vars.is_empty unused) then (
913
      if !debug then
914
        report ~level:2 (fun fmt ->
915
            Format.fprintf fmt "Unused local vars: [%a]. Removing them.@ "
916
              Vars.pp unused);
917
      List.filter (fun v -> not (Vars.mem v unused)) s.MT.step_locals)
918
    else s.MT.step_locals
919
  in
920
  let locals = locals @ Vars.elements new_locals in
921
  { s with MT.step_instrs = new_instrs; MT.step_locals = locals }
922
(* we have also to modify local variables to declare new vars *)
923

    
924
let machine_t2machine_t_optimized_by_salsa constEnv mt =
925
  try
926
    if !debug then
927
      report ~level:2 (fun fmt ->
928
          Format.fprintf fmt "@[<v 3>Optimizing machine %s@ "
929
            mt.MT.mname.LT.node_id);
930
    let new_step = salsaStep constEnv mt mt.MT.mstep in
931
    if !debug then report ~level:2 (fun fmt -> Format.fprintf fmt "@]@ ");
932
    { mt with MT.mstep = new_step }
933
  with FormalEnv.NoDefinition v as exp ->
934
    Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v;
935
    raise exp
936

    
937
(* Local Variables: *)
938
(* compile-command:"make -C ../../.." *)
939
(* End: *)
(2-2/4)