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

let report = Log.report ~plugin:"salsa" ~verbose_level:Salsa.Log.verbose_level

11


12

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

13

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

14


15

let fun_types node =

16

try

17

match node.LT.top_decl_desc with

18

 LT.Node nd >

19

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

20

Types.type_list_of_type tin, Types.type_list_of_type tout

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 =

30

let td, _ =

31

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

32

with Not_found > assert false

33

in

34

td

35

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

36


37

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

38

let rec get_expr_real_vars e =

39

let open MT in

40

match e.value_desc with

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

48

Vars.empty args

49

 Array _  Access _  Power _ >

50

assert false

51


52

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

53

let rec get_read_vars instrs =

54

let open MT in

55

match instrs with

56

 [] >

57

Vars.empty

58

 i :: tl > (

59

let vars_tl = get_read_vars tl in

60

match Corelang.get_instr_desc i with

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

68

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

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)

74


75

let rec get_written_vars instrs =

76

let open MT in

77

match instrs with

78

 [] >

79

Vars.empty

80

 i :: tl > (

81

let vars_tl = get_written_vars tl in

82

match Corelang.get_instr_desc i with

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)

93


94

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

95

(* let new_expr, new_range = *)

96

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

97

(* in *)

98

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

99

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

100


101

(* iterTransformExpr fresh_id new_expr abstractEnv new_range *)

102

(* else *)

103

(* new_expr, new_range *)

104


105

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

106

let opt_num_expr_sliced ranges e_salsa =

107

try

108

let fresh_id = "toto" in

109


110

(* TODO more meaningful name *)

111

let abstractEnv = RangesInt.to_abstract_env ranges in

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 =

116

Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv

117

in

118

report ~level:2 (fun fmt >

119

Format.fprintf fmt " Analysis done: %s@ "

120

(Salsa.Print.printExpression new_e_salsa));

121


122

(* (\* Debug *\) *)

123

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

124

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

125

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

126

(* (\* Debug *\) *)

127

report ~level:2 (fun fmt >

128

Format.fprintf fmt " Computing range progress@ ");

129


130

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

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

145

 true, false >

146

report ~level:2 (fun fmt >

147

Format.fprintf fmt

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

160

in

161

report ~level:2 (fun fmt > Format.fprintf fmt " Computing range done@ ");

162


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

174

expr, expr_range

175

with (* Not_found > *)

176

 Salsa.Epeg_types.EPEGError _ >

177

report ~level:2 (fun fmt >

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

182

e_salsa, None

183


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 =

188

let rec opt_expr m vars_env ranges formalEnv e =

189

let open MT in

190

match e.value_desc with

191

 Cst cst >

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

207

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

208

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

209

formalEnv e *)

210

(* else e, None *)

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

239

(* Convert expression *)

240

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

241

c) constEnv; *)

242

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

243


244

(* Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val

245

(salsa_expr2value_t vars_env [](\* constEnv *\) e_salsa) ; *)

246


247

(* Convert formalEnv *)

248

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

249

formalEnv; *)

250

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

251


252

(* Format.eprintf "Expression avant et apres substVars.@.Avant %a@."

253

MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ; *)

254


255

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

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

259

in

260


261

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

262

e_salsa) ; *)

263


264

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

265

let abstractEnv = RangesInt.to_abstract_env ranges in

266

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

267

(* The expression is partially evaluated by the available ranges

268

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

269

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

270

 on garde *)

271

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

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

279

in

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

284

let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in

285

if Vars.cardinal free_vars > 0 then (

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)

317

else (

318

if !debug then

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 subexpressions@ ");

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

449

in

450


451

opt_expr m vars_env ranges formalEnv e

452


453

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

454

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

455

let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv

456

vars_to_print =

457

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

458

let ordered_vars =

459

List.stable_sort

460

(FormalEnv.get_sort_fun formalEnv)

461

(Vars.elements vars_to_print)

462

in

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

474

try

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)

505


506

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

507

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

508

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

509

let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv

510

printed_vars vars_to_print =

511

let formal_env_def = FormalEnv.def constEnv vars_env in

512

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

513

let assign_vars = assign_vars nodename m constEnv vars_env in

514

(* if !debug then ( *)

515

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

516

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

517

(* Vars.pp printed_vars *)

518

(* Vars.pp vars_to_print *)

519

(* FormalEnv.pp formalEnv) *)

520

(* ); *)

521

match instrs with

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

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

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

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

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

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 )

839


840

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

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

846

in

847

let annots =

848

List.fold_left

849

(fun accu annl >

850

List.fold_left

851

(fun accu (key, range) >

852

match key with

853

 [ "salsa"; "ranges"; var ] >

854

(var, range) :: accu

855

 _ >

856

accu)

857

accu annl.LT.annots)

858

[] m.MT.mannot

859

in

860

let ranges =

861

List.fold_left

862

(fun ranges (v, value) >

863

match value.LT.eexpr_qfexpr.LT.expr_desc with

864

 LT.Expr_tuple [ minv; maxv ] >

865

let get_cst e =

866

match e.LT.expr_desc with

867

 LT.Expr_const (LT.Const_real r) >

868

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

869

Real.to_num r

870

 _ >

871

Format.eprintf

872

"Invalid salsa range: %a. It should be a pair of constant \

873

floats and %a is not a float.@."

874

Printers.pp_expr value.LT.eexpr_qfexpr Printers.pp_expr e;

875

assert false

876

in

877

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

878

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

879

(* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v

880

(Num.string_of_num minv) (Num.string_of_num maxv); *)

881

RangesInt.enlarge ranges v

882

(Salsa.Float.Domain.inject_nums (get_cst minv) (get_cst maxv))

883

 _ >

884

Format.eprintf

885

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

886

Printers.pp_expr value.LT.eexpr_qfexpr;

887

assert false)

888

ranges annots

889

in

890

let formal_env = FormalEnv.empty () in

891

let vars_to_print =

892

Vars.real_vars

893

(Vars.union (Vars.of_list m.MT.mmemory) (Vars.of_list s.MT.step_outputs))

894

in

895


896

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

897

let vars_env = compute_vars_env m in

898

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

899

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

900

rewrite_instrs m.MT.mname m constEnv vars_env m s.MT.step_instrs ranges

901

formal_env

902

(Vars.real_vars

903

(Vars.of_list

904

s.MT.step_inputs

905

(* printed_vars : real inputs are considered as already printed *)))

906

vars_to_print

907

in

908


909

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

910

let unused = Vars.diff all_local_vars printed_vars in

911

let locals =

912

if not (Vars.is_empty unused) then (

913

if !debug then

914

report ~level:2 (fun fmt >

915

Format.fprintf fmt "Unused local vars: [%a]. Removing them.@ "

916

Vars.pp unused);

917

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

918

else s.MT.step_locals

919

in

920

let locals = locals @ Vars.elements new_locals in

921

{ s with MT.step_instrs = new_instrs; MT.step_locals = locals }

922

(* we have also to modify local variables to declare new vars *)

923


924

let machine_t2machine_t_optimized_by_salsa constEnv mt =

925

try

926

if !debug then

927

report ~level:2 (fun fmt >

928

Format.fprintf fmt "@[<v 3>Optimizing machine %s@ "

929

mt.MT.mname.LT.node_id);

930

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

931

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

932

{ mt with MT.mstep = new_step }

933

with FormalEnv.NoDefinition v as exp >

934

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

935

raise exp

936


937

(* Local Variables: *)

938

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

939

(* End: *)
