Revision 9b348db1
Added by PierreLoïc Garoche over 5 years ago
src/plugins/salsa/machine_salsa_opt.ml  

92  92 
(* new_expr, new_range *) 
93  93  
94  94  
95 
(* Optimize a given expression. It returns another expression and a computed range. *) 

96 
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e : MT.value_t * RangesInt.t option * (MT.instr_t list) = 

95 
(* Takes as input a salsa expression and return an optimized one *) 

96 
let opt_num_expr_sliced ranges e_salsa = 

97 
try 

98 
let fresh_id = "toto" in (* TODO more meaningful name *) 

99  
100 
let abstractEnv = RangesInt.to_abstract_env ranges in 

101 
let new_e_salsa, e_val = 

102 
Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv 

103 
in 

104  
105  
106 
(* (\* Debug *\) *) 

107 
(* Format.eprintf "Salsa:@.input expr: %s@.outputexpr: %s@." *) 

108 
(* (Salsa.Print.printExpression e_salsa) *) 

109 
(* (Salsa.Print.printExpression new_e_salsa); *) 

110 
(* (\* Debug *\) *) 

111 


112  
113 
let old_val = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in 

114 
let expr, expr_range = 

115 
match RangesInt.Value.leq old_val e_val, RangesInt.Value.leq e_val old_val with 

116 
 true, true > ( 

117 
if !debug then Log.report ~level:2 (fun fmt > 

118 
Format.fprintf fmt "No improvement on abstract value %a@ " RangesInt.pp_val e_val; 

119 
); 

120 
e_salsa, Some old_val 

121 
) 

122 
 true, false > ( 

123 
if !debug then Log.report ~level:2 (fun fmt > 

124 
Format.fprintf fmt "Improved!@ "; 

125 
); 

126 
new_e_salsa, Some e_val 

127 
) 

128 
 false, true > Format.eprintf "CAREFUL  new range is worse!. Restoring provided expression@ "; e_salsa, Some old_val 

129  
130 
 false, false > 

131 
Format.eprintf 

132 
"Error; new range is not comparabe with old end. This should not happen!@.@?"; 

133 
assert false 

134 
in 

135 
if !debug then Log.report ~level:2 (fun fmt > 

136 
Format.fprintf fmt 

137 
" @[<v>old_expr: @[<v 0>%s@ range: %a@]@ new_expr: @[<v 0>%s@ range: %a@]@ @]@ " 

138 
(Salsa.Print.printExpression e_salsa) 

139 
(* MC.pp_val e *) 

140 
RangesInt.pp_val old_val 

141 
(Salsa.Print.printExpression new_e_salsa) 

142 
(* MC.pp_val new_e *) 

143 
RangesInt.pp_val e_val; 

144 
); 

145 
expr, expr_range 

146 
with (* Not_found > *) 

147 
 Salsa.Epeg_types.EPEGError _ > ( 

148 
Log.report ~level:2 (fun fmt > 

149 
Format.fprintf fmt 

150 
"BECAUSE OF AN ERROR, Expression %s was not optimized@ " (Salsa.Print.printExpression e_salsa) 

151 
(* MC.pp_val e *)); 

152 
e_salsa, None 

153 
) 

154  
155  
156 


157 
(* Optimize a given expression. It returns the modified expression, a computed range and freshly defined variables. *) 

158 
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 = 

97  159 
let rec opt_expr vars_env ranges formalEnv e = 
98  160 
let open MT in 
99  161 
match e.value_desc with 
...  ...  
104  166 
let typ = Typing.type_const Location.dummy_loc cst in 
105  167 
if Types.is_real_type typ then 
106  168 
opt_num_expr vars_env ranges formalEnv e 
107 
else e, None, [] 

169 
else e, None, [], Vars.empty


108  170 
 LocalVar v 
109  171 
 StateVar v > 
110  172 
if not (Vars.mem v printed_vars) && 
...  ...  
113  175 
then 
114  176 
opt_num_expr vars_env ranges formalEnv e 
115  177 
else 
116 
e, None, [] (* Nothing to optimize for expressions containing a single non real variable *) 

178 
e, None, [], Vars.empty (* Nothing to optimize for expressions containing a single non real variable *)


117  179 
(* (\* optimize only numerical vars *\) *) 
118  180 
(* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *) 
119  181 
(* else e, None *) 
...  ...  
124  186 
opt_num_expr vars_env ranges formalEnv e 
125  187 
else ( 
126  188 
(* We do not care for computed local ranges. *) 
127 
let args', il = List.fold_right (fun arg (al, il) > let arg', _, arg_il = opt_expr vars_env ranges formalEnv arg in arg'::al, arg_il@il) args ([], []) in 

128 
{ e with value_desc = Fun(fun_id, args')}, None, il 

189 
let args', il, new_locals = 

190 
List.fold_right ( 

191 
fun arg (al, il, nl) > 

192 
let arg', _, arg_il, arg_nl = 

193 
opt_expr vars_env ranges formalEnv arg in 

194 
arg'::al, arg_il@il, Vars.union arg_nl nl) 

195 
args 

196 
([], [], Vars.empty) 

197 
in 

198 
{ e with value_desc = Fun(fun_id, args')}, None, il, new_locals 

129  199 
) 
130  200 
) 
131  201 
 Array _ 
...  ...  
133  203 
 Power _ > assert false 
134  204 
and opt_num_expr vars_env ranges formalEnv e = 
135  205 
if !debug then ( 
136 
Log.report ~level:2 (fun fmt > Format.fprintf fmt "Optimizing expression %a@ "


206 
Log.report ~level:2 (fun fmt > Format.fprintf fmt "Optimizing expression @[<hov>%a@]@ "


137  207 
MC.pp_val e); 
138  208 
); 
139  209 
(* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ " MC.pp_val e; *) 
140 
let fresh_id = "toto" in (* TODO more meaningful name *) 

141  210 
(* Convert expression *) 
142  211 
(* List.iter (fun (l,c) > Format.eprintf "%s > %a@ " l Printers.pp_const c) constEnv; *) 
143  212 
let e_salsa : Salsa.Types.expression = value_t2salsa_expr constEnv e in 
...  ...  
180  249  
181  250 
let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in 
182  251 
if Vars.cardinal free_vars > 0 then ( 
183 
Log.report ~level:2 (fun fmt > Format.fprintf fmt "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 

184 
Vars.pp (Vars.fold (fun v accu > let v' = {v with LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id } in Vars.add v' accu) free_vars Vars.empty) 

252 
Log.report ~level:2 (fun fmt > Format.fprintf fmt 

253 
"Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 

254 
Vars.pp (Vars.fold (fun v accu > 

255 
let v' = {v with LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id } in 

256 
Vars.add v' accu) 

257 
free_vars Vars.empty) 

185  258 
MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa)); 
186  259 
if !debug then Log.report ~level:2 (fun fmt > Format.fprintf fmt "Some free vars, not optimizing@ "); 
187  260 
if !debug then Log.report ~level:3 (fun fmt > Format.fprintf fmt " ranges: %a@ " 
188  261 
RangesInt.pp ranges); 
189  262  
190  263 
(* if !debug then Log.report ~level:2 (fun fmt > Format.fprintf fmt "Formal env was @[<v 0>%a@]@ " FormalEnv.pp formalEnv); *) 
191 


264 


192  265 

193  266 
let new_e = try salsa_expr2value_t vars_env constEnv e_salsa with Not_found > assert false in 
194 
new_e, None, [] 

267 
new_e, None, [] , Vars.empty


195  268 
) 
196  269 
else ( 
197  270 

198 
try 

199 
if !debug then 

200 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "Analyzing expression %a with ranges: @[<v>%a@ @]@ " 

201 
(C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa) 

202 
(Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) > Format.fprintf fmt "%s > %a" l FloatIntSalsa.pp r)) abstractEnv) 

203 
; 

204  
205 
(* Format.eprintf "going to slice@."; *) 

206 
(* Slicing it XXX C'est là !!! ploc *) 

207 
let e_salsa, seq = Salsa.Rewrite.sliceExpr e_salsa 0 (Salsa.Types.Nop(Salsa.Types.Lab 0)) in 

208 
(* Format.eprintf "sliced@."; *) 

209 
let def_tmps = Salsa.Utils.flatten_seq seq [] in 

210 
(* Registering tmp ids in vars_env *) 

211 
let vars_env' = List.fold_left 

212 
(fun vs (id, _) > 

271 
if !debug then 

272 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "@[<v 2>Analyzing expression %a@ with ranges: @[<v>%a@ @]@ @]@ " 

273 
(C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa) 

274 
(Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) > Format.fprintf fmt "%s > %a" l FloatIntSalsa.pp r)) abstractEnv) 

275 
; 

276  
277 
(* Slicing expression *) 

278 
let e_salsa, seq = 

279 
Salsa.Rewrite.sliceExpr e_salsa 0 (Salsa.Types.Nop(Salsa.Types.Lab 0)) 

280 
in 

281 
let def_tmps = Salsa.Utils.flatten_seq seq [] in 

282 
(* Registering tmp ids in vars_env *) 

283 
let vars_env', new_local_vars = List.fold_left 

284 
(fun (vs,vars) (id, _) > 

285 
let vdecl = Corelang.mk_fresh_var 

286 
nodename 

287 
Location.dummy_loc 

288 
e.MT.value_type 

289 
(Clocks.new_var true) 

290 


291 
in 

292 
let vs' = 

213  293 
VarEnv.add 
214  294 
id 
215  295 
{ 
216 
vdecl = Corelang.mk_fresh_var 

217 
nodename 

218 
Location.dummy_loc 

219 
e.MT.value_type 

220 
(Clocks.new_var true) ; 

296 
vdecl = vdecl ; 

221  297 
is_local = true; 
222  298 
} 
223  299 
vs 
224 
) 

225 
vars_env 

226 
def_tmps 

227 
in 

228 
(* Format.eprintf "List of tmp: @[<v 0>%a@]" *) 

229 
(* ( *) 

230 
(* Utils.fprintf_list *) 

231 
(* ~sep:"@ " *) 

232 
(* (fun fmt (id, e_id) > *) 

233 
(* Format.fprintf fmt "(%s,%a) > %a" *) 

234 
(* id *) 

235 
(* Printers.pp_var (get_var vars_env' id).vdecl *) 

236 
(* (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_id) *) 

237 
(* ) *) 

238 
(* ) *) 

239 
(* def_tmps; *) 

240 
(* Format.eprintf "Sliced expression %a@.@?" *) 

241 
(* (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_salsa) *) 

242 
(* ; *) 

243  
244 
(* Optimize def tmp, and build the associated instructions. Update the abstract Env with computed ranges *) 

245 
let rev_def_tmp_instrs, ranges = 

246 
List.fold_left (fun (accu_instrs, ranges) (id, e_id) > 

247 
(* Format.eprintf "Cleaning/Optimizing %s@." id; *) 

248 
let abstractEnv = RangesInt.to_abstract_env ranges in 

249 
let e_id', e_range = Salsa.MainEPEG.transformExpression id e_id abstractEnv in 

250  
251 
let vdecl = (get_var vars_env' id).vdecl in 

252 
let new_e_id' = try salsa_expr2value_t vars_env' constEnv e_id' with Not_found > assert false in 

253 


254 
let new_local_assign = 

255 
(* let expr = salsa_expr2value_t vars_env' constEnv e_id' in *) 

256 
MT.MLocalAssign(vdecl, new_e_id') 

257 
in 

258 
let new_local_assign = { 

259 
MT.instr_desc = new_local_assign; 

260 
MT.lustre_eq = None (* could be Corelang.mkeq Location.dummy_loc 

261 
([vdecl.LT.var_id], e_id) provided it is 

262 
converted as Lustre expression rather than 

263 
a Machine code value *); 

264 
} 

265 
in 

266 
let new_ranges = RangesInt.add_def ranges id e_range in 

267 
new_local_assign::accu_instrs, new_ranges 

268 
) ([], ranges) def_tmps 

269 
in 

300 
in 

301 
let vars' = Vars.add vdecl vars in 

302 
vs', vars' 

303 
) 

304 
(vars_env,Vars.empty) 

305 
def_tmps 

306 
in 

307 
(* Debug *) 

308 
if !debug then ( 

309 
Log.report ~level:3 (fun fmt > 

310 
Format.fprintf fmt "List of slices: @[<v 0>%a@]@ " 

311 
(Utils.fprintf_list 

312 
~sep:"@ " 

313 
(fun fmt (id, e_id) > 

314 
Format.fprintf fmt "(%s,%a) > %a" 

315 
id 

316 
Printers.pp_var (get_var vars_env' id).vdecl 

317 
(C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_id) 

318 
) 

319 
) 

320 
def_tmps; 

321 
Format.eprintf "Sliced expression: %a@ " 

322 
(C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_salsa) 

323 
; 

324 
)); 

325 
(* Debug *) 

326 


327 
(* Optimize def tmp, and build the associated instructions. Update the 

328 
abstract Env with computed ranges *) 

329 
if !debug && List.length def_tmps >= 1 then ( 

330 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "@[<v 3>Optimizing sliced subexpressions@ ") 

331 
); 

332 
let rev_def_tmp_instrs, ranges = 

333 
List.fold_left (fun (accu_instrs, ranges) (id, e_id) > 

334 
(* Format.eprintf "Cleaning/Optimizing %s@." id; *) 

335 
let e_id', e_range = (*Salsa.MainEPEG.transformExpression id e_id abstractEnv*) 

336 
opt_num_expr_sliced ranges e_id 

337 
in 

338 
let new_e_id' = try salsa_expr2value_t vars_env' constEnv e_id' with Not_found > assert false in 

339  
340 
let vdecl = (get_var vars_env' id).vdecl in 

341 


342 
let new_local_assign = 

343 
(* let expr = salsa_expr2value_t vars_env' constEnv e_id' in *) 

344 
MT.MLocalAssign(vdecl, new_e_id') 

345 
in 

346 
let new_local_assign = { 

347 
MT.instr_desc = new_local_assign; 

348 
MT.lustre_eq = None (* could be Corelang.mkeq Location.dummy_loc 

349 
([vdecl.LT.var_id], e_id) provided it is 

350 
converted as Lustre expression rather than 

351 
a Machine code value *); 

352 
} 

353 
in 

354 
let new_ranges = 

355 
match e_range with 

356 
None > ranges 

357 
 Some e_range > RangesInt.add_def ranges id e_range in 

358 
new_local_assign::accu_instrs, new_ranges 

359 
) ([], ranges) def_tmps 

360 
in 

361 
if !debug && List.length def_tmps >= 1 then ( 

362 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "@]@ ") 

363 
); 

364  
365 
(* Format.eprintf "Optimizing main expression %s@.AbstractEnv is %a" (Salsa.Print.printExpression e_salsa) RangesInt.pp ranges; *) 

366 


367  
368 
let expr_salsa, expr_range = opt_num_expr_sliced ranges e_salsa in 

369 
let expr = try salsa_expr2value_t vars_env' constEnv expr_salsa with Not_found > assert false in 

370  
371 
expr, expr_range, List.rev rev_def_tmp_instrs, new_local_vars 

270  372  
271 
(* Format.eprintf "Optimizing main expression %s@.AbstractEnv is %a" (Salsa.Print.printExpression e_salsa) RangesInt.pp ranges; *) 

272 


273 
let abstractEnv = RangesInt.to_abstract_env ranges in 

274 
let new_e_salsa, e_val = 

275 
Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv 

276 
in 

277  373  
278 
(* let range_after = Float.evalExpr new_e_salsa abstractEnv in *) 

279  374  
280 
let new_e = try salsa_expr2value_t vars_env' constEnv new_e_salsa with Not_found > assert false in 

281 
if !debug then Log.report ~level:2 (fun fmt > 

282 
let old_range = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in 

283 
match RangesInt.Value.leq old_range e_val, RangesInt.Value.leq e_val old_range with 

284 
 true, true > Format.fprintf fmt "No improvement on abstract value %a@ " RangesInt.pp_val e_val 

285 
 true, false > ( 

286 
Format.fprintf fmt "Improved!"; 

287 
Format.fprintf fmt 

288 
" @[<v>old_expr: @[<v 0>%a@ range: %a@]@ new_expr: @[<v 0>%a@ range: %a@]@ @]@ " 

289 
MC.pp_val e 

290 
RangesInt.pp_val (Salsa.Analyzer.evalExpr e_salsa abstractEnv []) 

291 
MC.pp_val new_e 

292 
RangesInt.pp_val e_val 

293 
) 

294 
 false, true > Format.eprintf "Error; new range is worse!@.@?"; assert false 

295 
 false, false > Format.eprintf "Error; new range is not comparabe with old end. This should not happen!@.@?"; assert false 

296 
); 

297 
new_e, Some e_val, List.rev rev_def_tmp_instrs 

298 
with (* Not_found > *) 

299 
 Salsa.Epeg_types.EPEGError _ > ( 

300 
Log.report ~level:2 (fun fmt > Format.fprintf fmt "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e); 

301 
e, None, [] 

302 
) 

303  375 
) 
304  376  
305  377  
306 


378 


307  379 
in 
308  380 
opt_expr vars_env ranges formalEnv e 
309  381 

...  ...  
323  395 
(Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars); 
324  396 

325  397 
List.fold_right ( 
326 
fun v (accu_instr, accu_ranges) > 

398 
fun v (accu_instr, accu_ranges, accu_new_locals) >


327  399 
if !debug then Log.report ~level:4 (fun fmt > Format.fprintf fmt "Printing assign for variable %s@ " v.LT.var_id); 
328  400 
try 
329  401 
(* Obtaining unfold expression of v in formalEnv *) 
330  402 
let v_def = FormalEnv.get_def formalEnv v in 
331 
let e, r, il = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv v_def in 

403 
let e, r, il, new_v_locals = 

404 
optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv v_def 

405 
in 

332  406 
let instr_desc = 
333  407 
if try (get_var vars_env v.LT.var_id).is_local with Not_found > assert false then 
334  408 
MT.MLocalAssign(v, e) 
335  409 
else 
336  410 
MT.MStateAssign(v, e) 
337  411 
in 
338 
il@((Corelang.mkinstr instr_desc)::accu_instr), 

339 
(match r with 

340 
 None > ranges 

341 
 Some v_r > RangesInt.add_def ranges v.LT.var_id v_r) 

412 
(il@((Corelang.mkinstr instr_desc)::accu_instr)), 

413 
( 

414 
match r with 

415 
 None > ranges 

416 
 Some v_r > RangesInt.add_def ranges v.LT.var_id v_r), 

417 
(Vars.union accu_new_locals new_v_locals) 

342  418 
with FormalEnv.NoDefinition _ > ( 
343  419 
(* It should not happen with C backend, but may happen with Lustre backend *) 
344 
if !Options.output = "lustre" then accu_instr, ranges else (Format.eprintf "@?"; assert false) 

420 
if !Options.output = "lustre" then accu_instr, ranges, Vars.empty else (Format.eprintf "@?"; assert false)


345  421 
) 
346 
) ordered_vars ([], ranges) 

422 
) ordered_vars ([], ranges, Vars.empty)


347  423  
348  424 
(* Main recursive function: modify the instructions list while preserving the 
349  425 
order of assigns for state variables. Returns a quintuple: (new_instrs, 
...  ...  
364  440 
(* End of instruction list: we produce the definition of each variable that 
365  441 
appears in vars_to_print. Each of them should be defined in formalEnv *) 
366  442 
(* if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print; *) 
367 
let instrs, ranges' = assign_vars printed_vars ranges formalEnv vars_to_print in 

443 
let instrs, ranges', new_expr_locals = assign_vars printed_vars ranges formalEnv vars_to_print in


368  444 
instrs, 
369  445 
ranges', 
370  446 
formalEnv, 
371  447 
Vars.union printed_vars vars_to_print, (* We should have printed all required vars *) 
372 
[] (* No more vars to be printed *) 

373  
448 
[], (* No more vars to be printed *) 

449 
Vars.empty 

450 


374  451 
 hd_instr::tl_instrs > 
375  452 
(* We reformulate hd_instr, producing or not a fresh instruction, updating 
376  453 
formalEnv, possibly ranges and vars_to_print *) 
377  454 
begin 
378 
let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print = 

455 
let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print, hd_new_locals =


379  456 
match Corelang.get_instr_desc hd_instr with 
380  457 
 MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && not (Vars.mem vd vars_to_print) > 
381  458 
(* LocalAssign are injected into formalEnv *) 
...  ...  
386  463 
ranges, (* no new range computed *) 
387  464 
formalEnv', 
388  465 
printed_vars, (* no new printed vars *) 
389 
vars_to_print (* no more or less variables to print *) 

390 


466 
vars_to_print, (* no more or less variables to print *) 

467 
Vars.empty (* no new locals *) 

468 


391  469 
 MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print > 
392  470  
393  471 
(* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *) 
...  ...  
397  475 
(* Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd; *) 
398  476 
(* ); *) 
399  477 
let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
400 
let instrs', ranges' = (* printing vd = optimized vt *) 

478 
let instrs', ranges', expr_new_locals = (* printing vd = optimized vt *)


401  479 
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd) 
402  480 
in 
403  481 
instrs', 
404  482 
ranges', (* no new range computed *) 
405  483 
formalEnv', (* formelEnv already updated *) 
406 
Vars.add vd printed_vars, (* adding vd to new printed vars *) 

407 
Vars.remove vd vars_to_print (* removed vd from variables to print *) 

408  
484 
Vars.add vd printed_vars, (* adding vd to new printed vars *) 

485 
Vars.remove vd vars_to_print, (* removed vd from variables to print *) 

486 
expr_new_locals (* adding sliced vardecl to the list *) 

487 


409  488 
 MT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print *)> 
410  489  
411  490 
(* StateAssign are produced since they are required by the function. We still 
...  ...  
417  496 
(* Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd; *) 
418  497 
(* ); *) 
419  498 
let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
420 
let instrs', ranges' = (* printing vd = optimized vt *) 

499 
let instrs', ranges', expr_new_locals = (* printing vd = optimized vt *)


421  500 
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd) 
422  501 
in 
423  502 
instrs', 
424  503 
ranges', (* no new range computed *) 
425 
formalEnv, (* formelEnv already updated *) 

426 
Vars.add vd printed_vars, (* adding vd to new printed vars *) 

427 
Vars.remove vd vars_to_print (* removed vd from variables to print *) 

504 
formalEnv, (* formelEnv already updated *) 

505 
Vars.add vd printed_vars, (* adding vd to new printed vars *) 

506 
Vars.remove vd vars_to_print, (* removed vd from variables to print *) 

507 
expr_new_locals (* adding sliced vardecl to the list *) 

428  508  
429  509 
 (MT.MLocalAssign(vd,vt)  MT.MStateAssign(vd,vt)) > 
430  510 
(* Format.eprintf "other assign %a@." MC.pp_instr hd_instr; *) 
...  ...  
438  518 
variables *) 
439  519 
(* Format.eprintf "Required vars: %a@." Vars.pp required_vars; *) 
440  520 
let required_vars = Vars.diff required_vars (Vars.of_list m.MT.mmemory) in 
441 
let prefix_instr, ranges = 

521 
let prefix_instr, ranges, new_expr_dep_locals =


442  522 
assign_vars printed_vars ranges formalEnv required_vars in 
443  523  
444 
let vt', _, il = optimize_expr nodename m constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in 

524 
let vt', _, il, expr_new_locals = optimize_expr nodename m constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in


445  525 
let new_instr = 
446  526 
match Corelang.get_instr_desc hd_instr with 
447  527 
 MT.MLocalAssign _ > Corelang.update_instr_desc hd_instr (MT.MLocalAssign(vd,vt')) 
...  ...  
453  533 
formalEnv, (* formelEnv untouched *) 
454  534 
Vars.union written_vars printed_vars, (* adding vd + dependencies to 
455  535 
new printed vars *) 
456 
Vars.diff vars_to_print written_vars (* removed vd + dependencies from 

536 
Vars.diff vars_to_print written_vars, (* removed vd + dependencies from


457  537 
variables to print *) 
458  
538 
(Vars.union new_expr_dep_locals expr_new_locals) 

459  539 
 MT.MStep(vdl,id,vtl) > 
460  540 
(* Format.eprintf "step@."; *) 
461  541  
...  ...  
476  556 
fun_types node 
477  557 
in 
478  558 
(* if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; *) 
479 
let vtl', vtl_ranges, il = List.fold_right2 ( 

480 
fun e typ_e (exprl, range_l, il_l)> 

559 
let vtl', vtl_ranges, il, args_new_locals = List.fold_right2 (


560 
fun e typ_e (exprl, range_l, il_l, new_locals)>


481  561 
if Types.is_real_type typ_e then 
482 
let e', r', il = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e in 

483 
e'::exprl, r'::range_l, il@il_l 

562 
let e', r', il, new_expr_locals = 

563 
optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e 

564 
in 

565 
e'::exprl, r'::range_l, il@il_l, Vars.union new_locals new_expr_locals 

484  566 
else 
485 
e::exprl, None::range_l, il_l 

486 
) vtl tin ([], [], []) 

567 
e::exprl, None::range_l, il_l, new_locals


568 
) vtl tin ([], [], [], Vars.empty)


487  569 
in 
488  570 
(* if !debug then Format.eprintf "... done@ @]@ "; *) 
489  571  
...  ...  
522  604 
RangesInt.add_call ranges vdl id vtl_ranges, (* add information bounding each vdl var *) 
523  605 
formalEnv, 
524  606 
Vars.union written_vars printed_vars, (* adding vdl to new printed vars *) 
525 
Vars.diff vars_to_print written_vars 

607 
Vars.diff vars_to_print written_vars, 

608 
args_new_locals 

526  609 

527  610 
 MT.MBranch(vt, branches) > 
528  611 

529  612 
(* Required variables to compute vt are introduced. 
530  613 
Then each branch is refactored specifically 
531  614 
*) 
615 


532  616 
(* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; *) 
533 
let required_vars = get_expr_real_vars vt in 

534 
let required_vars = Vars.diff required_vars printed_vars in (* remove 

535 
already 

536 
produced 

537 
variables *) 

538 
let vt', _, prefix_instr = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv vt in 

539  
617 
let required_vars = get_expr_real_vars vt in 

618 
let required_vars = Vars.diff required_vars printed_vars in (* remove 

619 
already 

620 
produced 

621 
variables *) 

622 
let vt', _, prefix_instr, prefix_new_locals = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv vt in 

623  
624 
let new_locals = prefix_new_locals in 

625 


540  626 
(* let prefix_instr, ranges = *) 
541  627 
(* assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in *) 
542  628  
...  ...  
545  631  
546  632 
let read_vars_tl = get_read_vars tl_instrs in 
547  633 
(* if !debug then Format.eprintf "@[<v 2>Dealing with branches@ "; *) 
548 
let branches', written_vars, merged_ranges = List.fold_right ( 

549 
fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges) > 

634 
let branches', written_vars, merged_ranges, new_locals = List.fold_right (


635 
fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges, new_locals) >


550  636 
let b_write_vars = get_written_vars b_instrs in 
551  637 
let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in 
552  638 
let b_fe = formalEnv in (* because of side effect 
553  639 
data, we copy it for 
554  640 
each branch *) 
555 
let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars = 

641 
let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars, b_new_locals =


556  642 
rewrite_instrs nodename m constEnv vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
557  643 
in 
558  644 
(* b_vars should be empty *) 
...  ...  
564  650 
use union instead of 
565  651 
inter to ease the 
566  652 
bootstrap *) 
567 
RangesInt.merge merged_ranges b_ranges 

653 
RangesInt.merge merged_ranges b_ranges, 

654 
Vars.union new_locals b_new_locals 

568  655 

569 
) branches ([], required_vars, ranges) in 

656 
) branches ([], required_vars, ranges, new_locals) 

657 
in 

570  658 
(* if !debug then Format.eprintf "dealing with branches done@ @]@ "; *) 
571  659 
prefix_instr@[Corelang.update_instr_desc hd_instr (MT.MBranch(vt', branches'))], 
572 
merged_ranges, (* Only step functions call within branches 

573 
may have produced new ranges. We merge this data by 

574 
computing the join per variable *) 

575 
formalEnv, (* Thanks to the computation of var_to_print in each 

576 
branch, no new definition should have been computed 

577 
without being already printed *) 

578 
Vars.union written_vars printed_vars, 

579 
Vars.diff vars_to_print written_vars (* We remove vars that have been 

580 
produced within branches *) 

660 
merged_ranges, (* Only step functions call within branches may have 

661 
produced new ranges. We merge this data by 

662 
computing the join per variable *) 

663 
formalEnv, (* Thanks to the computation of var_to_print in each 

664 
branch, no new definition should have been computed 

665 
without being already printed *) 

666 
Vars.union written_vars printed_vars, 

667 
Vars.diff vars_to_print written_vars (* We remove vars that have been 

668 
produced within branches *), 

669 
new_locals 

581  670  
582  671  
583  672 
 MT.MReset(_)  MT.MNoReset _  MT.MComment _ > 
...  ...  
585  674  
586  675 
(* Untouched instruction *) 
587  676 
[ hd_instr ], (* unmodified instr *) 
588 
ranges, (* no new range computed *) 

589 
formalEnv, (* no formelEnv update *) 

590 
printed_vars, 

591 
vars_to_print (* no more or less variables to print *) 

677 
ranges, (* no new range computed *) 

678 
formalEnv, (* no formelEnv update *) 

679 
printed_vars, 

680 
vars_to_print, (* no more or less variables to print *) 

681 
Vars.empty (* no new slides vars *) 

592  682 

593  683 
in 
594 
let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print = 

684 
let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print, tl_new_locals =


595  685 
rewrite_instrs 
596  686 
nodename 
597  687 
m 
...  ...  
603  693 
formalEnv 
604  694 
printed_vars 
605  695 
vars_to_print 
696 


606  697 
in 
607  698 
hd_instrs @ tl_instrs, 
608  699 
ranges, 
609  700 
formalEnv, 
610  701 
printed_vars, 
611 
vars_to_print 

702 
vars_to_print, 

703 
(Vars.union hd_new_locals tl_new_locals) 

612  704 
end 
613  705  
614  706  
...  ...  
671  763 

672  764 
let vars_env = compute_vars_env m in 
673  765 
(* if !debug then Format.eprintf "@[<v 2>Registering node equations@ "; *) 
674 
let new_instrs, _, _, printed_vars, _ = 

766 
let new_instrs, _, _, printed_vars, _, new_locals =


675  767 
rewrite_instrs 
676  768 
m.MT.mname 
677  769 
m 
...  ...  
684  776 
(Vars.real_vars (Vars.of_list s.MT.step_inputs (* printed_vars : real 
685  777 
inputs are considered as 
686  778 
already printed *))) 
687 
vars_to_print 

779 
vars_to_print 

780 


688  781 
in 
689  782 
let all_local_vars = Vars.real_vars (Vars.of_list s.MT.step_locals) in 
690  783 
let unused = (Vars.diff all_local_vars printed_vars) in 
...  ...  
697  790 
else 
698  791 
s.MT.step_locals 
699  792 
in 
793 
let locals = locals @ Vars.elements new_locals in 

700  794 
{ s with MT.step_instrs = new_instrs; MT.step_locals = locals } (* we have also to modify local variables to declare new vars *) 
701  795  
702  796 
Also available in: Unified diff
[salsa] introducing sliced temporal variables