Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
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.@." |
Also available in: Unified diff
reformatting