1

(* We try to avoid opening modules here *)

2

module ST = Salsa.Types

3

module SDT = SalsaDatatypes

4

module LT = Lustre_types

5

module MC = Machine_code

6


7

(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *)

8

open SalsaDatatypes

9

(******************************************************************)

10

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

11


12

let fun_types node =

13

try

14

match node.LT.top_decl_desc with

15

 LT.Node nd >

16

let tin, tout = Types.split_arrow nd.LT.node_type in

17

Types.type_list_of_type tin, Types.type_list_of_type tout

18

 _ > Format.eprintf "%a is not a node@.@?" Printers.pp_decl node; assert false

19

with Not_found > Format.eprintf "Unable to find type def for function %s@.@?" (Corelang.node_name node); assert false

20


21

let called_node_id m id =

22

let td, _ =

23

try

24

List.assoc id m.MT.mcalls (* TODO Xavier: mcalls or minstances ? *)

25

with Not_found > assert false

26

in

27

td

28

(******************************************************************)

29


30

(* Returns the set of vars that appear in the expression *)

31

let rec get_expr_real_vars e =

32

let open MT in

33

match e.value_desc with

34

 LocalVar v  StateVar v when Types.is_real_type v.LT.var_type > Vars.singleton v

35

 LocalVar _ StateVar _

36

 Cst _ > Vars.empty

37

 Fun (_, args) >

38

List.fold_left

39

(fun acc e > Vars.union acc (get_expr_real_vars e))

40

Vars.empty args

41

 Array _

42

 Access _

43

 Power _ > assert false

44


45

(* Extract the variables to appear as free variables in expressions (lhs) *)

46

let rec get_read_vars instrs =

47

let open MT in

48

match instrs with

49

[] > Vars.empty

50

 i::tl > (

51

let vars_tl = get_read_vars tl in

52

match Corelang.get_instr_desc i with

53

 MLocalAssign(_,e)

54

 MStateAssign(_,e) > Vars.union (get_expr_real_vars e) vars_tl

55

 MStep(_, _, el) > List.fold_left (fun accu e > Vars.union (get_expr_real_vars e) accu) vars_tl el

56

 MBranch(e, branches) > (

57

let vars = Vars.union (get_expr_real_vars e) vars_tl in

58

List.fold_left (fun vars (_, b) > Vars.union vars (get_read_vars b) ) vars branches

59

)

60

 MReset _

61

 MNoReset _

62

 MComment _ > Vars.empty

63

)

64


65

let rec get_written_vars instrs =

66

let open MT in

67

match instrs with

68

[] > Vars.empty

69

 i::tl > (

70

let vars_tl = get_written_vars tl in

71

match Corelang.get_instr_desc i with

72

 MLocalAssign(v,_)

73

 MStateAssign(v,_) > Vars.add v vars_tl

74

 MStep(vdl, _, _) > List.fold_left (fun accu v > Vars.add v accu) vars_tl vdl

75

 MBranch(_, branches) > (

76

List.fold_left (fun vars (_, b) > Vars.union vars (get_written_vars b) ) vars_tl branches

77

)

78

 MReset _

79

 MNoReset _

80

 MComment _ > Vars.empty

81

)

82


83

(* let rec iterTransformExpr fresh_id e_salsa abstractEnv old_range = *)

84

(* let new_expr, new_range = *)

85

(* Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv *)

86

(* in *)

87

(* Format.eprintf "New range: %a@." RangesInt.pp_val new_range; *)

88

(* if Salsa.Float.errLt new_range old_range < 0 then *)

89


90

(* iterTransformExpr fresh_id new_expr abstractEnv new_range *)

91

(* else *)

92

(* new_expr, new_range *)

93


94


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 =

159

let rec opt_expr vars_env ranges formalEnv e =

160

let open MT in

161

match e.value_desc with

162

 Cst cst >

163

(* Format.eprintf "optmizing constant expr @ "; *)

164

(* the expression is a constant, we optimize it directly if it is a real

165

constant *)

166

let typ = Typing.type_const Location.dummy_loc cst in

167

if Types.is_real_type typ then

168

opt_num_expr vars_env ranges formalEnv e

169

else e, None, [], Vars.empty

170

 LocalVar v

171

 StateVar v >

172

if not (Vars.mem v printed_vars) &&

173

(* TODO xavier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *)

174

(Types.is_real_type e.value_type  Types.is_real_type v.LT.var_type)

175

then

176

opt_num_expr vars_env ranges formalEnv e

177

else

178

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

179

(* (\* optimize only numerical vars *\) *)

180

(* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *)

181

(* else e, None *)

182

 Fun (fun_id, args) > (

183

(* necessarily, this is a basic function (ie. +  * / &&  mod ... ) *)

184

(* if the return type is real then optimize it, otherwise call recusrsively on arguments *)

185

if Types.is_real_type e.value_type then

186

opt_num_expr vars_env ranges formalEnv e

187

else (

188

(* We do not care for computed local ranges. *)

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

199

)

200

)

201

 Array _

202

 Access _

203

 Power _ > assert false

204

and opt_num_expr vars_env ranges formalEnv e =

205

if !debug then (

206

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

207

MC.pp_val e);

208

);

209

(* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ " MC.pp_val e; *)

210

(* Convert expression *)

211

(* List.iter (fun (l,c) > Format.eprintf "%s > %a@ " l Printers.pp_const c) constEnv; *)

212

let e_salsa : Salsa.Types.expression = value_t2salsa_expr constEnv e in

213

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

214


215

(* Convert formalEnv *)

216

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

217

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

218


219

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

220


221

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

222

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

223

Salsa.Rewrite.substVars

224

e_salsa

225

(FormalEnv.to_salsa constEnv formalEnv)

226

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

227

in

228


229

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

230


231

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

232

let abstractEnv = RangesInt.to_abstract_env ranges in

233

(* List.iter (fun (id, _) > Format.eprintf "absenv: %s@." id) abstractEnv; *)

234

(* The expression is partially evaluated by the available ranges

235

valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv  on

236

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

237

 on garde *)

238

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

239

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

240

let e_salsa =

241

Salsa.Analyzer.evalPartExpr

242

e_salsa

243

(Salsa.Analyzer.valEnv2ExprEnv abstractEnv)

244

([] (* no blacklisted variables *))

245

([] (* no arrays *))

246

in

247

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

248

(* Checking if we have all necessary information *)

249


250

let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in

251

if Vars.cardinal free_vars > 0 then (

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)

258

MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));

259

if !debug then Log.report ~level:2 (fun fmt > Format.fprintf fmt "Some free vars, not optimizing@ ");

260

if !debug then Log.report ~level:3 (fun fmt > Format.fprintf fmt " ranges: %a@ "

261

RangesInt.pp ranges);

262


263

(* if !debug then Log.report ~level:2 (fun fmt > Format.fprintf fmt "Formal env was @[<v 0>%a@]@ " FormalEnv.pp formalEnv); *)

264


265


266

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

267

new_e, None, [] , Vars.empty

268

)

269

else (

270


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

293

VarEnv.add

294

id

295

{

296

vdecl = vdecl ;

297

is_local = true;

298

}

299

vs

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

372


373


374


375

)

376


377


378


379

in

380

opt_expr vars_env ranges formalEnv e

381


382


383

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

384

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

385

let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print =

386

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

387


388

let ordered_vars =

389

List.stable_sort

390

(FormalEnv.get_sort_fun formalEnv)

391

(Vars.elements vars_to_print)

392

in

393

if !debug then Log.report ~level:4 (fun fmt > Format.fprintf fmt

394

"Printing vars in the following order: [%a]@ "

395

(Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars);

396


397

List.fold_right (

398

fun v (accu_instr, accu_ranges, accu_new_locals) >

399

if !debug then Log.report ~level:4 (fun fmt > Format.fprintf fmt "Printing assign for variable %s@ " v.LT.var_id);

400

try

401

(* Obtaining unfold expression of v in formalEnv *)

402

let v_def = FormalEnv.get_def formalEnv v 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

406

let instr_desc =

407

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

408

MT.MLocalAssign(v, e)

409

else

410

MT.MStateAssign(v, e)

411

in

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)

418

with FormalEnv.NoDefinition _ > (

419

(* It should not happen with C backend, but may happen with Lustre backend *)

420

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

421

)

422

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

423


424

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

425

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

426

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

427

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

428

let formal_env_def = FormalEnv.def constEnv vars_env in

429

(* Format.eprintf "Rewrite intrs : [%a]@." MC.pp_instrs instrs; *)

430

let assign_vars = assign_vars nodename m constEnv vars_env in

431

(* if !debug then ( *)

432

(* Log.report ~level:3 (fun fmt > Format.fprintf fmt *)

433

(* "Current printed_vars: [%a]@ Vars to print: [%a]@ Formal env is [%a]@ " *)

434

(* Vars.pp printed_vars *)

435

(* Vars.pp vars_to_print *)

436

(* FormalEnv.pp formalEnv) *)

437

(* ); *)

438

match instrs with

439

 [] >

440

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

441

appears in vars_to_print. Each of them should be defined in formalEnv *)

442

(* if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print; *)

443

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

444

instrs,

445

ranges',

446

formalEnv,

447

Vars.union printed_vars vars_to_print, (* We should have printed all required vars *)

448

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

449

Vars.empty

450


451

 hd_instr::tl_instrs >

452

(* We reformulate hd_instr, producing or not a fresh instruction, updating

453

formalEnv, possibly ranges and vars_to_print *)

454

begin

455

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

456

match Corelang.get_instr_desc hd_instr with

457

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

458

(* LocalAssign are injected into formalEnv *)

459

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

460

(* if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr; *)

461

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

462

[], (* no instr generated *)

463

ranges, (* no new range computed *)

464

formalEnv',

465

printed_vars, (* no new printed vars *)

466

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

467

Vars.empty (* no new locals *)

468


469

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

470


471

(* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)

472

(* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)

473

(* if !debug then ( *)

474

(* Format.eprintf "%a@ " MC.pp_instr hd_instr; *)

475

(* Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd; *)

476

(* ); *)

477

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

478

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

479

assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)

480

in

481

instrs',

482

ranges', (* no new range computed *)

483

formalEnv', (* formelEnv already updated *)

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


488

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

489


490

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

491

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

492

outputs. vd is removed from remaining vars_to_print *)

493

(* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)

494

(* if !debug then ( *)

495

(* Format.eprintf "%a@ " MC.pp_instr hd_instr; *)

496

(* Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd; *)

497

(* ); *)

498

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

499

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

500

assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)

501

in

502

instrs',

503

ranges', (* no new range computed *)

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 *)

508


509

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

510

(* Format.eprintf "other assign %a@." MC.pp_instr hd_instr; *)

511


512

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

513

well its dependencies *)

514

let required_vars = get_expr_real_vars vt in

515

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

516

already

517

produced

518

variables *)

519

(* Format.eprintf "Required vars: %a@." Vars.pp required_vars; *)

520

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

521

let prefix_instr, ranges, new_expr_dep_locals =

522

assign_vars printed_vars ranges formalEnv required_vars in

523


524

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

525

let new_instr =

526

match Corelang.get_instr_desc hd_instr with

527

 MT.MLocalAssign _ > Corelang.update_instr_desc hd_instr (MT.MLocalAssign(vd,vt'))

528

 _ > Corelang.update_instr_desc hd_instr (MT.MStateAssign(vd,vt'))

529

in

530

let written_vars = Vars.add vd required_vars in

531

prefix_instr@il@[new_instr],

532

ranges, (* no new range computed *)

533

formalEnv, (* formelEnv untouched *)

534

Vars.union written_vars printed_vars, (* adding vd + dependencies to

535

new printed vars *)

536

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

537

variables to print *)

538

(Vars.union new_expr_dep_locals expr_new_locals)

539

 MT.MStep(vdl,id,vtl) >

540

(* Format.eprintf "step@."; *)

541


542

(* if !debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr; *)

543

(* Call of an external function. Input expressions have to be

544

optimized, their free variables produced. A fresh range has to be

545

computed for each output variable in vdl. Output of the function

546

call are removed from vars to be printed *)

547

let node = called_node_id m id in

548

let node_id = Corelang.node_name node in

549

let tin, tout = (* special care for arrow *)

550

if node_id = "_arrow" then

551

match vdl with

552

 [v] > let t = v.LT.var_type in

553

[t; t], [t]

554

 _ > assert false (* should not happen *)

555

else

556

fun_types node

557

in

558

(* if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; *)

559

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

560

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

561

if Types.is_real_type typ_e then

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

566

else

567

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

568

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

569

in

570

(* if !debug then Format.eprintf "... done@ @]@ "; *)

571


572


573


574

(* let required_vars = *)

575

(* List.fold_left2 *)

576

(* (fun accu e typ_e > *)

577

(* if Types.is_real_type typ_e then *)

578

(* Vars.union accu (get_expr_real_vars e) *)

579

(* else (\* we do not consider non real expressions *\) *)

580

(* accu *)

581

(* ) *)

582

(* Vars.empty *)

583

(* vtl' tin *)

584

(* in *)

585

(* if !debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ " *)

586

(* Vars.pp required_vars *)

587

(* Vars.pp printed_vars *)

588

(* Vars.pp (Vars.diff required_vars printed_vars) *)

589

(* ; *)

590

(* let required_vars = Vars.diff required_vars printed_vars in (\* remove *)

591

(* already *)

592

(* produced *)

593

(* variables *\) *)

594

(* let written_vars = Vars.union required_vars (Vars.of_list vdl) in *)

595

(* let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in *)

596


597

(* instrs' @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *) *)

598


599

let written_vars = Vars.of_list vdl in

600


601


602


603

il @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *)

604

RangesInt.add_call ranges vdl id vtl_ranges, (* add information bounding each vdl var *)

605

formalEnv,

606

Vars.union written_vars printed_vars, (* adding vdl to new printed vars *)

607

Vars.diff vars_to_print written_vars,

608

args_new_locals

609


610

 MT.MBranch(vt, branches) >

611


612

(* Required variables to compute vt are introduced.

613

Then each branch is refactored specifically

614

*)

615


616

(* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; *)

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


626

(* let prefix_instr, ranges = *)

627

(* assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in *)

628


629

let printed_vars = Vars.union printed_vars required_vars in

630


631


632

let read_vars_tl = get_read_vars tl_instrs in

633

(* if !debug then Format.eprintf "@[<v 2>Dealing with branches@ "; *)

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) >

636

let b_write_vars = get_written_vars b_instrs in

637

let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in

638

let b_fe = formalEnv in (* because of side effect

639

data, we copy it for

640

each branch *)

641

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

642

rewrite_instrs nodename m constEnv vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print

643

in

644

(* b_vars should be empty *)

645

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

646


647

(* Producing the refactored branch *)

648

(b_l, b_instrs') :: new_branches,

649

Vars.union b_printed written_vars, (* They should coincides. We

650

use union instead of

651

inter to ease the

652

bootstrap *)

653

RangesInt.merge merged_ranges b_ranges,

654

Vars.union new_locals b_new_locals

655


656

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

657

in

658

(* if !debug then Format.eprintf "dealing with branches done@ @]@ "; *)

659

prefix_instr@[Corelang.update_instr_desc hd_instr (MT.MBranch(vt', 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

670


671


672

 MT.MReset(_)  MT.MNoReset _  MT.MComment _ >

673

(* if !debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr; *)

674


675

(* Untouched instruction *)

676

[ hd_instr ], (* unmodified instr *)

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 *)

682


683

in

684

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

685

rewrite_instrs

686

nodename

687

m

688

constEnv

689

vars_env

690

m

691

tl_instrs

692

ranges

693

formalEnv

694

printed_vars

695

vars_to_print

696


697

in

698

hd_instrs @ tl_instrs,

699

ranges,

700

formalEnv,

701

printed_vars,

702

vars_to_print,

703

(Vars.union hd_new_locals tl_new_locals)

704

end

705


706


707


708


709


710


711

(* TODO: deal with new variables, ie. tmp *)

712

let salsaStep constEnv m s =

713

let ranges = RangesInt.empty (* empty for the moment, should be build from

714

machine annotations or externally provided information *) in

715

let annots = List.fold_left (

716

fun accu annl >

717

List.fold_left (

718

fun accu (key, range) >

719

match key with

720

 ["salsa"; "ranges"; var] > (var, range)::accu

721

 _ > accu

722

) accu annl.LT.annots

723

) [] m.MT.mannot

724

in

725

let ranges =

726

List.fold_left (fun ranges (v, value) >

727

match value.LT.eexpr_qfexpr.LT.expr_desc with

728

 LT.Expr_tuple [minv; maxv] > (

729

let get_cst e = match e.LT.expr_desc with

730

 LT.Expr_const (LT.Const_real (c,e,s)) >

731

(* calculer la valeur c * 10^e *)

732

Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))

733

 _ >

734

Format.eprintf

735

"Invalid salsa range: %a. It should be a pair of constant floats and %a is not a float.@."

736

Printers.pp_expr value.LT.eexpr_qfexpr

737

Printers.pp_expr e

738

;

739

assert false

740

in

741

(* let minv = Salsa.Float.Domain.of_num (get_cst minv) and *)

742

(* maxv = Salsa.Float.Domain.of_num (get_cst maxv) in *)

743

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

744

RangesInt.enlarge ranges v (Salsa.Float.Domain.inject_nums (get_cst minv) (get_cst maxv))

745

)

746

 _ >

747

Format.eprintf

748

"Invalid salsa range: %a. It should be a pair of floats.@."

749

Printers.pp_expr value.LT.eexpr_qfexpr;

750

assert false

751

) ranges annots

752

in

753

let formal_env = FormalEnv.empty () in

754

let vars_to_print =

755

Vars.real_vars

756

(

757

Vars.union

758

(Vars.of_list m.MT.mmemory)

759

(Vars.of_list s.MT.step_outputs)

760

)

761

in

762

(* TODO: should be at least step output + may be memories *)

763


764

let vars_env = compute_vars_env m in

765

(* if !debug then Format.eprintf "@[<v 2>Registering node equations@ "; *)

766

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

767

rewrite_instrs

768

m.MT.mname

769

m

770

constEnv

771

vars_env

772

m

773

s.MT.step_instrs

774

ranges

775

formal_env

776

(Vars.real_vars (Vars.of_list s.MT.step_inputs (* printed_vars : real

777

inputs are considered as

778

already printed *)))

779

vars_to_print

780


781

in

782

let all_local_vars = Vars.real_vars (Vars.of_list s.MT.step_locals) in

783

let unused = (Vars.diff all_local_vars printed_vars) in

784

let locals =

785

if not (Vars.is_empty unused) then (

786

if !debug then Log.report ~level:2 (fun fmt > Format.fprintf fmt "Unused local vars: [%a]. Removing them.@ "

787

Vars.pp unused);

788

List.filter (fun v > not (Vars.mem v unused)) s.MT.step_locals

789

)

790

else

791

s.MT.step_locals

792

in

793

let locals = locals @ Vars.elements new_locals in

794

{ s with MT.step_instrs = new_instrs; MT.step_locals = locals } (* we have also to modify local variables to declare new vars *)

795


796


797

let machine_t2machine_t_optimized_by_salsa constEnv mt =

798

try

799

if !debug then Log.report ~level:2 (fun fmt > Format.fprintf fmt "@[<v 3>[salsa] Optimizing machine %s@ " mt.MT.mname.LT.node_id);

800

let new_step = salsaStep constEnv mt mt.MT.mstep in

801

if !debug then Log.report ~level:2 (fun fmt > Format.fprintf fmt "@]@ ");

802

{ mt with MT.mstep = new_step }

803


804


805

with FormalEnv.NoDefinition v as exp >

806

Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v;

807

raise exp

808


809


810

(* Local Variables: *)

811

(* compilecommand:"make C ../../.." *)

812

(* End: *)

813

