1
|
(* We try to avoid opening modules here *)
|
2
|
module ST = Salsa.SalsaTypes
|
3
|
module SDT = SalsaDatatypes
|
4
|
module LT = LustreSpec
|
5
|
module MC = Machine_code
|
6
|
|
7
|
(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *)
|
8
|
open SalsaDatatypes
|
9
|
(******************************************************************)
|
10
|
(* TODO Xavier: should those functions be declared more globally? *)
|
11
|
|
12
|
let fun_types node =
|
13
|
try
|
14
|
match node.LT.top_decl_desc with
|
15
|
| LT.Node nd ->
|
16
|
let tin, tout = Types.split_arrow nd.LT.node_type in
|
17
|
Types.type_list_of_type tin, Types.type_list_of_type tout
|
18
|
| _ -> Format.eprintf "%a is not a node@.@?" Printers.pp_decl node; assert false
|
19
|
with Not_found -> Format.eprintf "Unable to find type def for function %s@.@?" (Corelang.node_name node); assert false
|
20
|
|
21
|
let called_node_id m id =
|
22
|
let td, _ =
|
23
|
try
|
24
|
List.assoc id m.MC.mcalls (* TODO Xavier: mcalls or minstances ? *)
|
25
|
with Not_found -> assert false
|
26
|
in
|
27
|
td
|
28
|
(******************************************************************)
|
29
|
|
30
|
(* Returns the set of vars that appear in the expression *)
|
31
|
let rec get_expr_real_vars e =
|
32
|
match e.LT.value_desc with
|
33
|
| LT.LocalVar v | LT.StateVar v when Types.is_real_type v.LT.var_type -> Vars.singleton v
|
34
|
| LT.LocalVar _| LT.StateVar _
|
35
|
| LT.Cst _ -> Vars.empty
|
36
|
| LT.Fun (_, args) ->
|
37
|
List.fold_left
|
38
|
(fun acc e -> Vars.union acc (get_expr_real_vars e))
|
39
|
Vars.empty args
|
40
|
| LT.Array _
|
41
|
| LT.Access _
|
42
|
| LT.Power _ -> assert false
|
43
|
|
44
|
(* Extract the variables to appear as free variables in expressions (lhs) *)
|
45
|
let rec get_read_vars instrs =
|
46
|
match instrs with
|
47
|
[] -> Vars.empty
|
48
|
| i::tl -> (
|
49
|
let vars_tl = get_read_vars tl in
|
50
|
match i with
|
51
|
| LT.MLocalAssign(_,e)
|
52
|
| LT.MStateAssign(_,e) -> Vars.union (get_expr_real_vars e) vars_tl
|
53
|
| LT.MStep(_, _, el) -> List.fold_left (fun accu e -> Vars.union (get_expr_real_vars e) accu) vars_tl el
|
54
|
| LT.MBranch(e, branches) -> (
|
55
|
let vars = Vars.union (get_expr_real_vars e) vars_tl in
|
56
|
List.fold_left (fun vars (_, b) -> Vars.union vars (get_read_vars b) ) vars branches
|
57
|
)
|
58
|
| LT.MReset _
|
59
|
| LT.MComment _ -> Vars.empty
|
60
|
)
|
61
|
|
62
|
let rec get_written_vars instrs =
|
63
|
match instrs with
|
64
|
[] -> Vars.empty
|
65
|
| i::tl -> (
|
66
|
let vars_tl = get_written_vars tl in
|
67
|
match i with
|
68
|
| LT.MLocalAssign(v,_)
|
69
|
| LT.MStateAssign(v,_) -> Vars.add v vars_tl
|
70
|
| LT.MStep(vdl, _, _) -> List.fold_left (fun accu v -> Vars.add v accu) vars_tl vdl
|
71
|
| LT.MBranch(_, branches) -> (
|
72
|
List.fold_left (fun vars (_, b) -> Vars.union vars (get_written_vars b) ) vars_tl branches
|
73
|
)
|
74
|
| LT.MReset _
|
75
|
| LT.MComment _ -> Vars.empty
|
76
|
)
|
77
|
|
78
|
let rec iterTransformExpr fresh_id e_salsa abstractEnv old_range =
|
79
|
let new_expr, new_range =
|
80
|
Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
|
81
|
in
|
82
|
Format.eprintf "New range: %a@." RangesInt.pp_val new_range;
|
83
|
if Salsa.Float.errLt new_range old_range < 0 then
|
84
|
|
85
|
iterTransformExpr fresh_id new_expr abstractEnv new_range
|
86
|
else
|
87
|
new_expr, new_range
|
88
|
|
89
|
|
90
|
(* Optimize a given expression. It returns another expression and a computed range. *)
|
91
|
let optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e : LT.value_t * RangesInt.t option =
|
92
|
let rec opt_expr ranges formalEnv e =
|
93
|
match e.LT.value_desc with
|
94
|
| LT.Cst cst ->
|
95
|
Format.eprintf "optmizing constant expr ? @ ";
|
96
|
(* the expression is a constant, we optimize it directly if it is a real
|
97
|
constant *)
|
98
|
let typ = Typing.type_const Location.dummy_loc cst in
|
99
|
if Types.is_real_type typ then
|
100
|
opt_num_expr ranges formalEnv e
|
101
|
else e, None
|
102
|
| LT.LocalVar v
|
103
|
| LT.StateVar v ->
|
104
|
if not (Vars.mem v printed_vars) &&
|
105
|
(Types.is_real_type e.LT.value_type || Types.is_real_type v.LT.var_type)
|
106
|
then
|
107
|
opt_num_expr ranges formalEnv e
|
108
|
else
|
109
|
e, None (* Nothing to optimize for expressions containing a single non real variable *)
|
110
|
(* (\* optimize only numerical vars *\) *)
|
111
|
(* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *)
|
112
|
(* else e, None *)
|
113
|
| LT.Fun (fun_id, args) -> (
|
114
|
(* necessarily, this is a basic function (ie. + - * / && || mod ... ) *)
|
115
|
(* if the return type is real then optimize it, otherwise call recusrsively on arguments *)
|
116
|
if Types.is_real_type e.LT.value_type then
|
117
|
opt_num_expr ranges formalEnv e
|
118
|
else (
|
119
|
(* We do not care for computed local ranges. *)
|
120
|
let args' = List.map (fun arg -> let arg', _ = opt_expr ranges formalEnv arg in arg') args in
|
121
|
{ e with LT.value_desc = LT.Fun(fun_id, args')}, None
|
122
|
)
|
123
|
)
|
124
|
| LT.Array _
|
125
|
| LT.Access _
|
126
|
| LT.Power _ -> assert false
|
127
|
and opt_num_expr ranges formalEnv e =
|
128
|
if debug then Format.eprintf "Optimizing expression %a@ " MC.pp_val e;
|
129
|
let fresh_id = "toto" in (* TODO more meaningful name *)
|
130
|
(* Convert expression *)
|
131
|
List.iter (fun (l,c) -> Format.eprintf "%s -> %a@ " l Printers.pp_const c) constEnv;
|
132
|
let e_salsa : Salsa.SalsaTypes.expression = value_t2salsa_expr constEnv e in
|
133
|
Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val (salsa_expr2value_t vars_env [](* constEnv *) e_salsa) ;
|
134
|
|
135
|
(* Convert formalEnv *)
|
136
|
if debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv;
|
137
|
let formalEnv_salsa =
|
138
|
FormalEnv.fold (fun id expr accu ->
|
139
|
(id, value_t2salsa_expr constEnv expr)::accu
|
140
|
) formalEnv [] in
|
141
|
if debug then Format.eprintf "Formal env converted to salsa@ ";
|
142
|
(* Substitute all occurences of variables by their definition in env *)
|
143
|
let (e_salsa: Salsa.SalsaTypes.expression), _ =
|
144
|
Salsa.Rewrite.substVars
|
145
|
e_salsa
|
146
|
formalEnv_salsa
|
147
|
0 (* TODO: Nasrine, what is this integer value for ? *)
|
148
|
in
|
149
|
if debug then Format.eprintf "Substituted def in expr@ ";
|
150
|
let abstractEnv = Hashtbl.fold
|
151
|
(fun id value accu -> (id,value)::accu)
|
152
|
ranges
|
153
|
[]
|
154
|
in
|
155
|
(* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id) abstractEnv; *)
|
156
|
(* The expression is partially evaluated by the available ranges
|
157
|
valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on
|
158
|
garde evalPartExpr remplace les variables e qui sont dans env par la cst
|
159
|
- on garde *)
|
160
|
if debug then Format.eprintf "avant avant eval part@ ";
|
161
|
Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);
|
162
|
let e_salsa =
|
163
|
Salsa.Float.evalPartExpr
|
164
|
e_salsa
|
165
|
(Salsa.Float.valEnv2ExprEnv abstractEnv)
|
166
|
([] (* no blacklisted variables *))
|
167
|
in
|
168
|
Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);
|
169
|
(* Checking if we have all necessary information *)
|
170
|
|
171
|
let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in
|
172
|
|
173
|
if Vars.cardinal free_vars > 0 then (
|
174
|
Format.eprintf "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ "
|
175
|
Vars.pp (Vars.fold (fun v accu -> let v' = {v with LT.var_id = nodename ^ "." ^ v.LT.var_id } in Vars.add v' accu) free_vars Vars.empty)
|
176
|
MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);
|
177
|
if debug then Format.eprintf "Some free vars, not optimizing@.";
|
178
|
let new_e = try salsa_expr2value_t vars_env constEnv e_salsa with Not_found -> assert false in
|
179
|
new_e, None
|
180
|
)
|
181
|
else (
|
182
|
try
|
183
|
if debug then
|
184
|
Format.eprintf "Analyzing expression %a with env: @[<v>%a@ @]@ "
|
185
|
MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa)
|
186
|
(Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv
|
187
|
;
|
188
|
let range_before = Float.evalExpr e_salsa abstractEnv in
|
189
|
|
190
|
let new_e_salsa, e_val =
|
191
|
iterTransformExpr fresh_id e_salsa abstractEnv range_before
|
192
|
in
|
193
|
|
194
|
let range_after = Float.evalExpr new_e_salsa abstractEnv in
|
195
|
|
196
|
let new_e = try salsa_expr2value_t vars_env constEnv new_e_salsa with Not_found -> assert false in
|
197
|
if debug then Format.eprintf "@ @[<v>old: %a@ new: %a@ old range: %a@ new range: %a@ computed range: %a@]"
|
198
|
MC.pp_val e
|
199
|
MC.pp_val new_e
|
200
|
RangesInt.pp_val range_before
|
201
|
RangesInt.pp_val range_after
|
202
|
RangesInt.pp_val e_val;
|
203
|
new_e, Some e_val
|
204
|
with Not_found -> assert false
|
205
|
| Salsa.Epeg_types.EPEGError _ -> (
|
206
|
Format.eprintf "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e;
|
207
|
e, None
|
208
|
)
|
209
|
)
|
210
|
|
211
|
|
212
|
|
213
|
in
|
214
|
if debug then
|
215
|
Format.eprintf "@[<v 2>Optimizing expression %a in environment %a and ranges %a@ "
|
216
|
MC.pp_val e
|
217
|
FormalEnv.pp formalEnv
|
218
|
RangesInt.pp ranges;
|
219
|
let res = opt_expr ranges formalEnv e in
|
220
|
Format.eprintf "@]@ ";
|
221
|
res
|
222
|
|
223
|
|
224
|
|
225
|
(* Returns a list of assign, for each var in vars_to_print, that produce the
|
226
|
definition of it according to formalEnv, and driven by the ranges. *)
|
227
|
let assign_vars nodename constEnv vars_env printed_vars ranges formalEnv vars_to_print =
|
228
|
(* We print thhe expression in the order of definition *)
|
229
|
|
230
|
let ordered_vars =
|
231
|
List.stable_sort
|
232
|
(FormalEnv.get_sort_fun formalEnv)
|
233
|
(Vars.elements vars_to_print)
|
234
|
in
|
235
|
Format.eprintf "Printing vars in the following order: [%a]@ " (Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars ;
|
236
|
List.fold_right (
|
237
|
fun v (accu_instr, accu_ranges) ->
|
238
|
if debug then Format.eprintf "Printing assign for variable %s@ " v.LT.var_id;
|
239
|
try
|
240
|
(* Obtaining unfold expression of v in formalEnv *)
|
241
|
let v_def = FormalEnv.get_def formalEnv v in
|
242
|
let e, r = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv v_def in
|
243
|
let instr =
|
244
|
if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then
|
245
|
LT.MLocalAssign(v, e)
|
246
|
else
|
247
|
LT.MStateAssign(v, e)
|
248
|
in
|
249
|
instr::accu_instr,
|
250
|
(match r with
|
251
|
| None -> ranges
|
252
|
| Some v_r -> RangesInt.add_def ranges v.LT.var_id v_r)
|
253
|
with FormalEnv.NoDefinition _ -> (
|
254
|
(* It should not happen with C backend, but may happen with Lustre backend *)
|
255
|
if !Options.output = "lustre" then accu_instr, ranges else (Format.eprintf "@?"; assert false)
|
256
|
)
|
257
|
) ordered_vars ([], ranges)
|
258
|
|
259
|
(* Main recursive function: modify the instructions list while preserving the
|
260
|
order of assigns for state variables. Returns a quintuple: (new_instrs,
|
261
|
ranges, formalEnv, printed_vars, and remaining vars to be printed) *)
|
262
|
let rec rewrite_instrs nodename constEnv vars_env m instrs ranges formalEnv printed_vars vars_to_print =
|
263
|
let assign_vars = assign_vars nodename constEnv vars_env in
|
264
|
if debug then (
|
265
|
Format.eprintf "------------@ ";
|
266
|
Format.eprintf "Current printed_vars: [%a]@ " Vars.pp printed_vars;
|
267
|
Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv;
|
268
|
);
|
269
|
match instrs with
|
270
|
| [] ->
|
271
|
(* End of instruction list: we produce the definition of each variable that
|
272
|
appears in vars_to_print. Each of them should be defined in formalEnv *)
|
273
|
if debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print;
|
274
|
let instrs, ranges' = assign_vars printed_vars ranges formalEnv vars_to_print in
|
275
|
instrs,
|
276
|
ranges',
|
277
|
formalEnv,
|
278
|
Vars.union printed_vars vars_to_print, (* We should have printed all required vars *)
|
279
|
[] (* No more vars to be printed *)
|
280
|
|
281
|
| hd_instr::tl_instrs ->
|
282
|
(* We reformulate hd_instr, producing or not a fresh instruction, updating
|
283
|
formalEnv, possibly ranges and vars_to_print *)
|
284
|
begin
|
285
|
let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print =
|
286
|
match hd_instr with
|
287
|
| LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && not (Vars.mem vd vars_to_print) ->
|
288
|
(* LocalAssign are injected into formalEnv *)
|
289
|
if debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr;
|
290
|
let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *)
|
291
|
[], (* no instr generated *)
|
292
|
ranges, (* no new range computed *)
|
293
|
formalEnv',
|
294
|
printed_vars, (* no new printed vars *)
|
295
|
vars_to_print (* no more or less variables to print *)
|
296
|
|
297
|
| LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
|
298
|
|
299
|
if debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr;
|
300
|
let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *)
|
301
|
let instrs', ranges' = (* printing vd = optimized vt *)
|
302
|
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)
|
303
|
in
|
304
|
instrs',
|
305
|
ranges', (* no new range computed *)
|
306
|
formalEnv', (* formelEnv already updated *)
|
307
|
Vars.add vd printed_vars, (* adding vd to new printed vars *)
|
308
|
Vars.remove vd vars_to_print (* removed vd from variables to print *)
|
309
|
|
310
|
| LT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
|
311
|
|
312
|
(* StateAssign are produced since they are required by the function. We still
|
313
|
keep their definition in the formalEnv in case it can optimize later
|
314
|
outputs. vd is removed from remaining vars_to_print *)
|
315
|
if debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr;
|
316
|
let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *)
|
317
|
let instrs', ranges' = (* printing vd = optimized vt *)
|
318
|
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)
|
319
|
in
|
320
|
instrs',
|
321
|
ranges', (* no new range computed *)
|
322
|
formalEnv, (* formelEnv already updated *)
|
323
|
Vars.add vd printed_vars, (* adding vd to new printed vars *)
|
324
|
Vars.remove vd vars_to_print (* removed vd from variables to print *)
|
325
|
|
326
|
| (LT.MLocalAssign(vd,vt) | LT.MStateAssign(vd,vt)) ->
|
327
|
(* We have to produce the instruction. But we may have to produce as
|
328
|
well its dependencies *)
|
329
|
let required_vars = get_expr_real_vars vt in
|
330
|
let required_vars = Vars.diff required_vars printed_vars in (* remove
|
331
|
already
|
332
|
produced
|
333
|
variables *)
|
334
|
let prefix_instr, ranges =
|
335
|
assign_vars printed_vars ranges formalEnv required_vars in
|
336
|
let vt', _ = optimize_expr nodename constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in
|
337
|
let new_instr =
|
338
|
match hd_instr with
|
339
|
| LT.MLocalAssign _ -> LT.MLocalAssign(vd,vt')
|
340
|
| _ -> LT.MStateAssign(vd,vt')
|
341
|
in
|
342
|
let written_vars = Vars.add vd required_vars in
|
343
|
prefix_instr@[new_instr],
|
344
|
ranges, (* no new range computed *)
|
345
|
formalEnv, (* formelEnv untouched *)
|
346
|
Vars.union written_vars printed_vars, (* adding vd + dependencies to
|
347
|
new printed vars *)
|
348
|
Vars.diff vars_to_print written_vars (* removed vd + dependencies from
|
349
|
variables to print *)
|
350
|
|
351
|
| LT.MStep(vdl,id,vtl) ->
|
352
|
if debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr;
|
353
|
(* Call of an external function. Input expressions have to be
|
354
|
optimized, their free variables produced. A fresh range has to be
|
355
|
computed for each output variable in vdl. Output of the function
|
356
|
call are removed from vars to be printed *)
|
357
|
let node = called_node_id m id in
|
358
|
let node_id = Corelang.node_name node in
|
359
|
let tin, tout = (* special care for arrow *)
|
360
|
if node_id = "_arrow" then
|
361
|
match vdl with
|
362
|
| [v] -> let t = v.LT.var_type in
|
363
|
[t; t], [t]
|
364
|
| _ -> assert false (* should not happen *)
|
365
|
else
|
366
|
fun_types node
|
367
|
in
|
368
|
if debug then Format.eprintf "@[<v 2>... optimizing arguments@ ";
|
369
|
let vtl', vtl_ranges = List.fold_right2 (
|
370
|
fun e typ_e (exprl, range_l)->
|
371
|
if Types.is_real_type typ_e then
|
372
|
let e', r' = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e in
|
373
|
e'::exprl, r'::range_l
|
374
|
else
|
375
|
e::exprl, None::range_l
|
376
|
) vtl tin ([], [])
|
377
|
in
|
378
|
if debug then Format.eprintf "... done@ @]@ ";
|
379
|
let required_vars =
|
380
|
List.fold_left2
|
381
|
(fun accu e typ_e ->
|
382
|
if Types.is_real_type typ_e then
|
383
|
Vars.union accu (get_expr_real_vars e)
|
384
|
else (* we do not consider non real expressions *)
|
385
|
accu
|
386
|
)
|
387
|
Vars.empty
|
388
|
vtl' tin
|
389
|
in
|
390
|
if debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ "
|
391
|
Vars.pp required_vars
|
392
|
Vars.pp printed_vars
|
393
|
Vars.pp (Vars.diff required_vars printed_vars)
|
394
|
;
|
395
|
let required_vars = Vars.diff required_vars printed_vars in (* remove
|
396
|
already
|
397
|
produced
|
398
|
variables *)
|
399
|
let written_vars = Vars.union required_vars (Vars.of_list vdl) in
|
400
|
let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in
|
401
|
instrs' @ [LT.MStep(vdl,id,vtl')], (* New instrs *)
|
402
|
RangesInt.add_call ranges' vdl id vtl_ranges, (* add information bounding each vdl var *)
|
403
|
formalEnv,
|
404
|
Vars.union written_vars printed_vars, (* adding vdl to new printed vars *)
|
405
|
Vars.diff vars_to_print written_vars
|
406
|
|
407
|
| LT.MBranch(vt, branches) ->
|
408
|
(* Required variables to compute vt are introduced.
|
409
|
Then each branch is refactored specifically
|
410
|
*)
|
411
|
if debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr;
|
412
|
let required_vars = get_expr_real_vars vt in
|
413
|
let required_vars = Vars.diff required_vars printed_vars in (* remove
|
414
|
already
|
415
|
produced
|
416
|
variables *)
|
417
|
let prefix_instr, ranges =
|
418
|
assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in
|
419
|
|
420
|
let printed_vars = Vars.union printed_vars required_vars in
|
421
|
|
422
|
let vt', _ = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv vt in
|
423
|
|
424
|
let read_vars_tl = get_read_vars tl_instrs in
|
425
|
if debug then Format.eprintf "@[<v 2>Dealing with branches@ ";
|
426
|
let branches', written_vars, merged_ranges = List.fold_right (
|
427
|
fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges) ->
|
428
|
let b_write_vars = get_written_vars b_instrs in
|
429
|
let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in
|
430
|
let b_fe = formalEnv in (* because of side effect
|
431
|
data, we copy it for
|
432
|
each branch *)
|
433
|
let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars =
|
434
|
rewrite_instrs nodename constEnv vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print
|
435
|
in
|
436
|
(* b_vars should be empty *)
|
437
|
let _ = if b_vars != [] then assert false in
|
438
|
|
439
|
(* Producing the refactored branch *)
|
440
|
(b_l, b_instrs') :: new_branches,
|
441
|
Vars.union b_printed written_vars, (* They should coincides. We
|
442
|
use union instead of
|
443
|
inter to ease the
|
444
|
bootstrap *)
|
445
|
RangesInt.merge merged_ranges b_ranges
|
446
|
|
447
|
) branches ([], required_vars, ranges) in
|
448
|
if debug then Format.eprintf "dealing with branches done@ @]@ ";
|
449
|
prefix_instr@[LT.MBranch(vt', branches')],
|
450
|
merged_ranges, (* Only step functions call within branches
|
451
|
may have produced new ranges. We merge this data by
|
452
|
computing the join per variable *)
|
453
|
formalEnv, (* Thanks to the computation of var_to_print in each
|
454
|
branch, no new definition should have been computed
|
455
|
without being already printed *)
|
456
|
Vars.union written_vars printed_vars,
|
457
|
Vars.diff vars_to_print written_vars (* We remove vars that have been
|
458
|
produced within branches *)
|
459
|
|
460
|
|
461
|
| LT.MReset(_) | LT.MComment _ ->
|
462
|
if debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr;
|
463
|
|
464
|
(* Untouched instruction *)
|
465
|
[ hd_instr ], (* unmodified instr *)
|
466
|
ranges, (* no new range computed *)
|
467
|
formalEnv, (* no formelEnv update *)
|
468
|
printed_vars,
|
469
|
vars_to_print (* no more or less variables to print *)
|
470
|
|
471
|
in
|
472
|
let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print =
|
473
|
rewrite_instrs
|
474
|
nodename
|
475
|
constEnv
|
476
|
vars_env
|
477
|
m
|
478
|
tl_instrs
|
479
|
ranges
|
480
|
formalEnv
|
481
|
printed_vars
|
482
|
vars_to_print
|
483
|
in
|
484
|
hd_instrs @ tl_instrs,
|
485
|
ranges,
|
486
|
formalEnv,
|
487
|
printed_vars,
|
488
|
vars_to_print
|
489
|
end
|
490
|
|
491
|
|
492
|
|
493
|
|
494
|
|
495
|
|
496
|
(* TODO: deal with new variables, ie. tmp *)
|
497
|
let salsaStep constEnv m s =
|
498
|
let ranges = RangesInt.empty (* empty for the moment, should be build from
|
499
|
machine annotations or externally provided information *) in
|
500
|
let annots = List.fold_left (
|
501
|
fun accu annl ->
|
502
|
List.fold_left (
|
503
|
fun accu (key, range) ->
|
504
|
match key with
|
505
|
| ["salsa"; "ranges"; var] -> (var, range)::accu
|
506
|
| _ -> accu
|
507
|
) accu annl.LT.annots
|
508
|
) [] m.MC.mannot
|
509
|
in
|
510
|
let ranges =
|
511
|
List.fold_left (fun ranges (v, value) ->
|
512
|
match value.LT.eexpr_qfexpr.LT.expr_desc with
|
513
|
| LT.Expr_tuple [minv; maxv] -> (
|
514
|
let get_cst e = match e.LT.expr_desc with
|
515
|
| LT.Expr_const (LT.Const_real (c,e,s)) ->
|
516
|
(* calculer la valeur c * 10^e *)
|
517
|
Num.float_of_num (Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e)))
|
518
|
| _ ->
|
519
|
Format.eprintf
|
520
|
"Invalid scala range: %a. It should be a pair of constant floats.@."
|
521
|
Printers.pp_expr value.LT.eexpr_qfexpr;
|
522
|
assert false
|
523
|
in
|
524
|
let minv, maxv = get_cst minv, get_cst maxv in
|
525
|
if debug then Format.eprintf "%s in [%f, %f]@ " v minv maxv;
|
526
|
let irange = Salsa.SalsaTypes.I(minv, maxv) in
|
527
|
RangesInt.enlarge ranges v (irange, Salsa.Float.ulp irange)
|
528
|
)
|
529
|
| _ ->
|
530
|
Format.eprintf
|
531
|
"Invalid scala range: %a. It should be a pair of floats.@."
|
532
|
Printers.pp_expr value.LT.eexpr_qfexpr;
|
533
|
assert false
|
534
|
) ranges annots
|
535
|
in
|
536
|
let formal_env = FormalEnv.empty () in
|
537
|
let vars_to_print =
|
538
|
Vars.real_vars
|
539
|
(
|
540
|
Vars.union
|
541
|
(Vars.of_list m.MC.mmemory)
|
542
|
(Vars.of_list s.MC.step_outputs)
|
543
|
)
|
544
|
in
|
545
|
(* TODO: should be at least step output + may be memories *)
|
546
|
let vars_env = compute_vars_env m in
|
547
|
let new_instrs, _, _, printed_vars, _ =
|
548
|
rewrite_instrs
|
549
|
m.MC.mname.LT.node_id
|
550
|
constEnv
|
551
|
vars_env
|
552
|
m
|
553
|
s.MC.step_instrs
|
554
|
ranges
|
555
|
formal_env
|
556
|
(Vars.real_vars (Vars.of_list s.MC.step_inputs (* printed_vars : real
|
557
|
inputs are considered as
|
558
|
already printed *)))
|
559
|
vars_to_print
|
560
|
in
|
561
|
let all_local_vars = Vars.real_vars (Vars.of_list s.MC.step_locals) in
|
562
|
let unused = (Vars.diff all_local_vars printed_vars) in
|
563
|
let locals =
|
564
|
if not (Vars.is_empty unused) then (
|
565
|
Format.eprintf "Unused local vars: [%a]. Removing them.@.@?"
|
566
|
Vars.pp unused;
|
567
|
List.filter (fun v -> not (Vars.mem v unused)) s.MC.step_locals
|
568
|
)
|
569
|
else
|
570
|
s.MC.step_locals
|
571
|
in
|
572
|
{ s with MC.step_instrs = new_instrs; MC.step_locals = locals } (* we have also to modify local variables to declare new vars *)
|
573
|
|
574
|
|
575
|
let machine_t2machine_t_optimized_by_salsa constEnv mt =
|
576
|
try
|
577
|
if debug then Format.eprintf "@[<v 2>------------------ Optimizing machine %s@ " mt.MC.mname.LT.node_id;
|
578
|
let new_step = salsaStep constEnv mt mt.MC.mstep in
|
579
|
if debug then Format.eprintf "@]@.";
|
580
|
{ mt with MC.mstep = new_step }
|
581
|
|
582
|
|
583
|
with FormalEnv.NoDefinition v as exp ->
|
584
|
Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v;
|
585
|
raise exp
|
586
|
|
587
|
|
588
|
(* Local Variables: *)
|
589
|
(* compile-command:"make -C ../../.." *)
|
590
|
(* End: *)
|
591
|
|