80 
80 

81 
81 

82 
82 
(* Optimize a given expression. It returns another expression and a computed range. *)

83 

let optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e : LT.value_t * RangesInt.t option =


83 
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e : LT.value_t * RangesInt.t option =

84 
84 
let rec opt_expr ranges formalEnv e =

85 
85 
match e.LT.value_desc with

86 
86 
 LT.Cst cst >

...  ...  
127 
127 

128 
128 
(* Convert formalEnv *)

129 
129 
(* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)

130 

let formalEnv_salsa =

131 

FormalEnv.fold (fun id expr accu >

132 

(id, value_t2salsa_expr constEnv expr)::accu

133 

) formalEnv [] in

134 
130 
(* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)


131 


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


133 

135 
134 
(* Substitute all occurences of variables by their definition in env *)

136 
135 
let (e_salsa: Salsa.Types.expression), _ =

137 
136 
Salsa.Rewrite.substVars

138 
137 
e_salsa

139 

formalEnv_salsa


138 
(FormalEnv.to_salsa constEnv formalEnv)

140 
139 
0 (* TODO: Nasrine, what is this integer value for ? *)

141 
140 
in


141 


142 
Format.eprintf "Apres %a@." MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ;


143 

142 
144 
(* if !debug then Format.eprintf "Substituted def in expr@ "; *)

143 
145 
let abstractEnv = Hashtbl.fold

144 
146 
(fun id value accu > (id,value)::accu)

...  ...  
151 
153 
garde evalPartExpr remplace les variables e qui sont dans env par la cst

152 
154 
 on garde *)

153 
155 
(* if !debug then Format.eprintf "avant avant eval part@ "; *)

154 

(* Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *)


156 
Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);

155 
157 
let e_salsa =

156 
158 
Salsa.Analyzer.evalPartExpr

157 
159 
e_salsa

...  ...  
159 
161 
([] (* no blacklisted variables *))

160 
162 
([] (* no arrays *))

161 
163 
in

162 

(* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *)


164 
Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);

163 
165 
(* Checking if we have all necessary information *)

164 
166 

165 
167 
let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in

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

169 
171 
MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));

170 
172 
if !debug then Format.eprintf "Some free vars, not optimizing@.";


173 

171 
174 
let new_e = try salsa_expr2value_t vars_env constEnv e_salsa with Not_found > assert false in

172 
175 
new_e, None

173 
176 
)

174 
177 
else (

175 
178 

176 

try


179 
try

177 
180 
if !debug then

178 

Format.eprintf "Analyzing expression %a with env: @[<v>%a@ @]@ "

179 

MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa)


181 
Format.eprintf "Analyzing expression %a with env: @[<v>%a@ @]@ @?"


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

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

181 
184 
;

182 
185 


186 
(* Slicing it *)


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


188 


189 
Format.eprintf "Sliced expression %a@.@?"


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


191 
;


192 

183 
193 
let new_e_salsa, e_val =

184 

Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv


194 
Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv

185 
195 
in

186 
196 
let new_e = try salsa_expr2value_t vars_env constEnv new_e_salsa with Not_found > assert false in

187 
197 
if !debug then Format.eprintf "@ @[<v>old: %a@ new: %a@ range: %a@]" MC.pp_val e MC.pp_val new_e RangesInt.pp_val e_val;

188 
198 
new_e, Some e_val

189 

with Not_found > assert false


199 
with (* Not_found > *)

190 
200 
 Salsa.Epeg_types.EPEGError _ > (

191 
201 
Format.eprintf "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e;

192 
202 
e, None

...  ...  
209 
219 

210 
220 
(* Returns a list of assign, for each var in vars_to_print, that produce the

211 
221 
definition of it according to formalEnv, and driven by the ranges. *)

212 

let assign_vars nodename constEnv vars_env printed_vars ranges formalEnv vars_to_print =


222 
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print =

213 
223 
(* We print thhe expression in the order of definition *)

214 
224 

215 
225 
let ordered_vars =

...  ...  
224 
234 
try

225 
235 
(* Obtaining unfold expression of v in formalEnv *)

226 
236 
let v_def = FormalEnv.get_def formalEnv v in

227 

let e, r = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv v_def in


237 
let e, r = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv v_def in

228 
238 
let instr_desc =

229 
239 
if try (get_var vars_env v.LT.var_id).is_local with Not_found > assert false then

230 
240 
LT.MLocalAssign(v, e)

...  ...  
244 
254 
(* Main recursive function: modify the instructions list while preserving the

245 
255 
order of assigns for state variables. Returns a quintuple: (new_instrs,

246 
256 
ranges, formalEnv, printed_vars, and remaining vars to be printed) *)

247 

let rec rewrite_instrs nodename constEnv vars_env m instrs ranges formalEnv printed_vars vars_to_print =


257 
let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv printed_vars vars_to_print =


258 
let formal_env_def = FormalEnv.def constEnv vars_env in

248 
259 
Format.eprintf "Rewrite intrs :%a@." Machine_code.pp_instrs instrs;

249 

let assign_vars = assign_vars nodename constEnv vars_env in

250 

(* if !debug then ( *)

251 

(* Format.eprintf "@ "; *)

252 

(* Format.eprintf "Current printed_vars: [%a]@ " Vars.pp printed_vars; *)

253 

(* Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)

254 

(* ); *)


260 
let assign_vars = assign_vars nodename m constEnv vars_env in


261 
if !debug then (


262 
Format.eprintf "@.@ ";


263 
Format.eprintf "Current printed_vars: [%a]@ " Vars.pp printed_vars;


264 
Format.eprintf "Vars to print: [%a]@ " Vars.pp vars_to_print;


265 
Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv;


266 
);

255 
267 
match instrs with

256 
268 
 [] >

257 
269 
(* End of instruction list: we produce the definition of each variable that

...  ...  
276 
288 
(* LocalAssign are injected into formalEnv *)

277 
289 
(* if !debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; *)

278 
290 
if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr;

279 

let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *)


291 
let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)

280 
292 
[], (* no instr generated *)

281 
293 
ranges, (* no new range computed *)

282 
294 
formalEnv',

...  ...  
292 
304 
Format.eprintf "%a@]@ " MC.pp_instr hd_instr;

293 
305 
Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd;

294 
306 
);

295 

let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *)


307 
let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)

296 
308 
let instrs', ranges' = (* printing vd = optimized vt *)

297 
309 
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)

298 
310 
in

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

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

304 
316 

305 

 LT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print >

306 

Format.eprintf "state assign@.";


317 
 LT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print *)>


318 
Format.eprintf "state assign of real type@.";

307 
319 

308 
320 
(* StateAssign are produced since they are required by the function. We still

309 
321 
keep their definition in the formalEnv in case it can optimize later

...  ...  
313 
325 
Format.eprintf "%a@]@ " MC.pp_instr hd_instr;

314 
326 
Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd;

315 
327 
);

316 

let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *)


328 
let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)

317 
329 
let instrs', ranges' = (* printing vd = optimized vt *)

318 
330 
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)

319 
331 
in

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

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

325 
337 

326 

 (LT.MLocalAssign(vd,vt)  LT.MStateAssign(vd,vt)) >

327 

Format.eprintf "other assign@.";


338 
 (LT.MLocalAssign(vd,vt)  LT.MStateAssign(vd,vt)) >


339 
Format.eprintf "other assign %a@." MC.pp_instr hd_instr;

328 
340 

329 
341 
(* We have to produce the instruction. But we may have to produce as

330 
342 
well its dependencies *)

...  ...  
332 
344 
let required_vars = Vars.diff required_vars printed_vars in (* remove

333 
345 
already

334 
346 
produced

335 

variables *)


347 
variables *)


348 
Format.eprintf "Requited vars: %a@." Vars.pp required_vars;


349 
let required_vars = Vars.diff required_vars (Vars.of_list m.MC.mmemory) in

336 
350 
let prefix_instr, ranges =

337 
351 
assign_vars printed_vars ranges formalEnv required_vars in

338 
352 

339 

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


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

340 
354 
let new_instr =

341 
355 
match Corelang.get_instr_desc hd_instr with

342 
356 
 LT.MLocalAssign _ > Corelang.update_instr_desc hd_instr (LT.MLocalAssign(vd,vt'))

...  ...  
374 
388 
let vtl', vtl_ranges = List.fold_right2 (

375 
389 
fun e typ_e (exprl, range_l)>

376 
390 
if Types.is_real_type typ_e then

377 

let e', r' = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e in


391 
let e', r' = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e in

378 
392 
e'::exprl, r'::range_l

379 
393 
else

380 
394 
e::exprl, None::range_l

...  ...  
425 
439 

426 
440 
let printed_vars = Vars.union printed_vars required_vars in

427 
441 

428 

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


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

429 
443 

430 
444 
let read_vars_tl = get_read_vars tl_instrs in

431 
445 
if !debug then Format.eprintf "@[<v 2>Dealing with branches@ ";

...  ...  
437 
451 
data, we copy it for

438 
452 
each branch *)

439 
453 
let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars =

440 

rewrite_instrs nodename constEnv vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print


454 
rewrite_instrs nodename m constEnv vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print

441 
455 
in

442 
456 
(* b_vars should be empty *)

443 
457 
let _ = if b_vars != [] then assert false in

...  ...  
479 
493 
let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print =

480 
494 
rewrite_instrs

481 
495 
nodename


496 
m

482 
497 
constEnv

483 
498 
vars_env

484 
499 
m

...  ...  
530 
545 
assert false

531 
546 
in

532 
547 
let minv, maxv = get_cst minv, get_cst maxv in

533 

if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv);


548 
let minv, maxv = Num.float_of_num minv, Num.float_of_num maxv in


549 
(* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv); *)

534 
550 
RangesInt.enlarge ranges v (Salsa.Float.Domain.nnew minv maxv)

535 
551 
)

536 
552 
 _ >

...  ...  
556 
572 
let new_instrs, _, _, printed_vars, _ =

557 
573 
rewrite_instrs

558 
574 
m.MC.mname.LT.node_id


575 
m

559 
576 
constEnv

560 
577 
vars_env

561 
578 
m
