1


2

(* We try to avoid opening modules here *)

3

module ST = Salsa.Types

4

module SDT = SalsaDatatypes

5

module LT = Lustre_types

6

module MC = Machine_code

7


8

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

9

open SalsaDatatypes

10

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

11

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

12


13

let fun_types node =

14

try

15

match node.LT.top_decl_desc with

16

 LT.Node nd >

17

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

18

Types.type_list_of_type tin, Types.type_list_of_type tout

19

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

20

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

21


22

let called_node_id m id =

23

let td, _ =

24

try

25

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

26

with Not_found > assert false

27

in

28

td

29

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

30


31

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

32

let rec get_expr_real_vars e =

33

let open MT in

34

match e.value_desc with

35

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

36

 LocalVar _ StateVar _

37

 Cst _ > Vars.empty

38

 Fun (_, args) >

39

List.fold_left

40

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

41

Vars.empty args

42

 Array _

43

 Access _

44

 Power _ > assert false

45


46

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

47

let rec get_read_vars instrs =

48

let open MT in

49

match instrs with

50

[] > Vars.empty

51

 i::tl > (

52

let vars_tl = get_read_vars tl in

53

match Corelang.get_instr_desc i with

54

 MLocalAssign(_,e)

55

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

56

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

57

 MBranch(e, branches) > (

58

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

59

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

60

)

61

 MReset _

62

 MNoReset _

63

 MComment _ > Vars.empty

64

)

65


66

let rec get_written_vars instrs =

67

let open MT in

68

match instrs with

69

[] > Vars.empty

70

 i::tl > (

71

let vars_tl = get_written_vars tl in

72

match Corelang.get_instr_desc i with

73

 MLocalAssign(v,_)

74

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

75

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

76

 MBranch(_, branches) > (

77

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

78

)

79

 MReset _

80

 MNoReset _

81

 MComment _ > Vars.empty

82

)

83


84


85

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

86

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

87

let rec opt_expr ranges formalEnv e =

88

let open MT in

89

match e.value_desc with

90

 Cst cst >

91

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

92

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

93

constant *)

94

let typ = Typing.type_const Location.dummy_loc cst in

95

if Types.is_real_type typ then

96

opt_num_expr ranges formalEnv e

97

else e, None

98

 LocalVar v

99

 StateVar v >

100

if not (Vars.mem v printed_vars) &&

101

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

102

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

103

then

104

opt_num_expr ranges formalEnv e

105

else

106

e, None (* Nothing to optimize for expressions containing a single non real variable *)

107

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

108

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

109

(* else e, None *)

110

 Fun (fun_id, args) > (

111

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

112

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

113

if Types.is_real_type e.value_type then

114

opt_num_expr ranges formalEnv e

115

else (

116

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

117

let args' = List.map (fun arg > let arg', _ = opt_expr ranges formalEnv arg in arg') args in

118

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

119

)

120

)

121

 Array _

122

 Access _

123

 Power _ > assert false

124

and opt_num_expr ranges formalEnv e =

125

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

126

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

127

(* Convert expression *)

128

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

129

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

130

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

131


132

(* Convert formalEnv *)

133

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

134

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

135


136

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

137


138

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

139

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

140

Salsa.Rewrite.substVars

141

e_salsa

142

(FormalEnv.to_salsa constEnv formalEnv)

143

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

144

in

145


146

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

147


148

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

149

let abstractEnv = Hashtbl.fold

150

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

151

ranges

152

[]

153

in

154

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

155

(* The expression is partially evaluated by the available ranges

156

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

157

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

158

 on garde *)

159

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

160

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

161

let e_salsa =

162

Salsa.Analyzer.evalPartExpr

163

e_salsa

164

(Salsa.Analyzer.valEnv2ExprEnv abstractEnv)

165

([] (* no blacklisted variables *))

166

([] (* no arrays *))

167

in

168

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

169

(* Checking if we have all necessary information *)

170


171

let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in

172

if Vars.cardinal free_vars > 0 then (

173

Log.report ~level:2 (fun fmt > Format.fprintf fmt "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ "

174

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)

175

MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));

176

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

177


178

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

179

new_e, None

180

)

181

else (

182


183

try

184

if !debug then

185

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

186

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

187

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

188

;

189


190

(* Slicing it *)

191

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

192


193

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

194

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

195

;

196


197

let new_e_salsa, e_val =

198

Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv

199

in

200

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

201

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;

202

new_e, Some e_val

203

with (* Not_found > *)

204

 Salsa.Epeg_types.EPEGError _ > (

205

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

206

e, None

207

)

208

)

209


210


211


212

in

213

if !debug then

214

Format.eprintf "@[<v 2>Optimizing expression %a in environment %a and ranges %a@ "

215

MC.pp_val e

216

FormalEnv.pp formalEnv

217

RangesInt.pp ranges;

218

let res = opt_expr ranges formalEnv e in

219

Format.eprintf "@]@ ";

220

res

221


222


223


224

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

225

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

226

let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print =

227

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

228


229

let ordered_vars =

230

List.stable_sort

231

(FormalEnv.get_sort_fun formalEnv)

232

(Vars.elements vars_to_print)

233

in

234

if !debug then Format.eprintf "Printing vars in the following order: [%a]@ " (Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars ;

235

List.fold_right (

236

fun v (accu_instr, accu_ranges) >

237

if !debug then Format.eprintf "Printing assign for variable %s@ " v.LT.var_id;

238

try

239

(* Obtaining unfold expression of v in formalEnv *)

240

let v_def = FormalEnv.get_def formalEnv v in

241

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

242

let instr_desc =

243

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

244

MT.MLocalAssign(v, e)

245

else

246

MT.MStateAssign(v, e)

247

in

248

(Corelang.mkinstr instr_desc)::accu_instr,

249

(match r with

250

 None > ranges

251

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

252

with FormalEnv.NoDefinition _ > (

253

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

254

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

255

)

256

) ordered_vars ([], ranges)

257


258

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

259

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

260

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

261

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

262

let formal_env_def = FormalEnv.def constEnv vars_env in

263

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

264

let assign_vars = assign_vars nodename m constEnv vars_env in

265

if !debug then (

266

Format.eprintf "@.@ ";

267

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

268

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

269

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

270

);

271

match instrs with

272

 [] >

273

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

274

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

275

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

276

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

277

instrs,

278

ranges',

279

formalEnv,

280

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

281

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

282


283

 hd_instr::tl_instrs >

284

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

285

formalEnv, possibly ranges and vars_to_print *)

286

begin

287

Format.eprintf "Hdlist@.";

288

let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print =

289

match Corelang.get_instr_desc hd_instr with

290

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

291

Format.eprintf "local assign@.";

292

(* LocalAssign are injected into formalEnv *)

293

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

294

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

295

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

296

[], (* no instr generated *)

297

ranges, (* no new range computed *)

298

formalEnv',

299

printed_vars, (* no new printed vars *)

300

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

301


302

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

303

Format.eprintf "local assign 2@.";

304


305

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

306

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

307

if !debug then (

308

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

309

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

310

);

311

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

312

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

313

assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)

314

in

315

instrs',

316

ranges', (* no new range computed *)

317

formalEnv', (* formelEnv already updated *)

318

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

319

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

320


321

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

322

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

323


324

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

325

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

326

outputs. vd is removed from remaining vars_to_print *)

327

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

328

if !debug then (

329

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

330

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

331

);

332

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

333

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

334

assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)

335

in

336

instrs',

337

ranges', (* no new range computed *)

338

formalEnv, (* formelEnv already updated *)

339

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

340

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

341


342

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

343

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

344


345

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

346

well its dependencies *)

347

let required_vars = get_expr_real_vars vt in

348

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

349

already

350

produced

351

variables *)

352

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

353

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

354

let prefix_instr, ranges =

355

assign_vars printed_vars ranges formalEnv required_vars in

356


357

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

358

let new_instr =

359

match Corelang.get_instr_desc hd_instr with

360

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

361

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

362

in

363

let written_vars = Vars.add vd required_vars in

364

prefix_instr@[new_instr],

365

ranges, (* no new range computed *)

366

formalEnv, (* formelEnv untouched *)

367

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

368

new printed vars *)

369

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

370

variables to print *)

371


372

 MT.MStep(vdl,id,vtl) >

373

Format.eprintf "step@.";

374


375

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

376

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

377

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

378

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

379

call are removed from vars to be printed *)

380

let node = called_node_id m id in

381

let node_id = Corelang.node_name node in

382

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

383

if node_id = "_arrow" then

384

match vdl with

385

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

386

[t; t], [t]

387

 _ > assert false (* should not happen *)

388

else

389

fun_types node

390

in

391

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

392

let vtl', vtl_ranges = List.fold_right2 (

393

fun e typ_e (exprl, range_l)>

394

if Types.is_real_type typ_e then

395

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

396

e'::exprl, r'::range_l

397

else

398

e::exprl, None::range_l

399

) vtl tin ([], [])

400

in

401

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

402

let required_vars =

403

List.fold_left2

404

(fun accu e typ_e >

405

if Types.is_real_type typ_e then

406

Vars.union accu (get_expr_real_vars e)

407

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

408

accu

409

)

410

Vars.empty

411

vtl' tin

412

in

413

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

414

Vars.pp required_vars

415

Vars.pp printed_vars

416

Vars.pp (Vars.diff required_vars printed_vars)

417

;

418

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

419

already

420

produced

421

variables *)

422

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

423

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

424

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

425

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

426

formalEnv,

427

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

428

Vars.diff vars_to_print written_vars

429


430

 MT.MBranch(vt, branches) >

431


432

(* Required variables to compute vt are introduced.

433

Then each branch is refactored specifically

434

*)

435

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

436

let required_vars = get_expr_real_vars vt in

437

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

438

already

439

produced

440

variables *)

441

let prefix_instr, ranges =

442

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

443


444

let printed_vars = Vars.union printed_vars required_vars in

445


446

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

447


448

let read_vars_tl = get_read_vars tl_instrs in

449

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

450

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

451

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

452

let b_write_vars = get_written_vars b_instrs in

453

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

454

let b_fe = formalEnv in (* because of side effect

455

data, we copy it for

456

each branch *)

457

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

458

rewrite_instrs nodename m constEnv vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print

459

in

460

(* b_vars should be empty *)

461

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

462


463

(* Producing the refactored branch *)

464

(b_l, b_instrs') :: new_branches,

465

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

466

use union instead of

467

inter to ease the

468

bootstrap *)

469

RangesInt.merge merged_ranges b_ranges

470


471

) branches ([], required_vars, ranges) in

472

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

473

prefix_instr@[Corelang.update_instr_desc hd_instr (MT.MBranch(vt', branches'))],

474

merged_ranges, (* Only step functions call within branches

475

may have produced new ranges. We merge this data by

476

computing the join per variable *)

477

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

478

branch, no new definition should have been computed

479

without being already printed *)

480

Vars.union written_vars printed_vars,

481

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

482

produced within branches *)

483


484


485

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

486

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

487


488

(* Untouched instruction *)

489

[ hd_instr ], (* unmodified instr *)

490

ranges, (* no new range computed *)

491

formalEnv, (* no formelEnv update *)

492

printed_vars,

493

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

494


495

in

496

Format.eprintf "cic@.";

497

let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print =

498

rewrite_instrs

499

nodename

500

m

501

constEnv

502

vars_env

503

m

504

tl_instrs

505

ranges

506

formalEnv

507

printed_vars

508

vars_to_print

509

in

510

Format.eprintf "la@.";

511

hd_instrs @ tl_instrs,

512

ranges,

513

formalEnv,

514

printed_vars,

515

vars_to_print

516

end

517


518


519


520


521


522


523

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

524

let salsaStep constEnv m s =

525

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

526

machine annotations or externally provided information *) in

527

let annots = List.fold_left (

528

fun accu annl >

529

List.fold_left (

530

fun accu (key, range) >

531

match key with

532

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

533

 _ > accu

534

) accu annl.LT.annots

535

) [] m.MC.mannot

536

in

537

let ranges =

538

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

539

match value.LT.eexpr_qfexpr.LT.expr_desc with

540

 LT.Expr_tuple [minv; maxv] > (

541

let get_cst e = match e.LT.expr_desc with

542

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

543

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

544

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

545

 _ >

546

Format.eprintf

547

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

548

Printers.pp_expr value.LT.eexpr_qfexpr;

549

assert false

550

in

551

let minv, maxv = get_cst minv, get_cst maxv in

552

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

553

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

554

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

555

)

556

 _ >

557

Format.eprintf

558

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

559

Printers.pp_expr value.LT.eexpr_qfexpr;

560

assert false

561

) ranges annots

562

in

563

let formal_env = FormalEnv.empty () in

564

let vars_to_print =

565

Vars.real_vars

566

(

567

Vars.union

568

(Vars.of_list m.MC.mmemory)

569

(Vars.of_list s.MC.step_outputs)

570

)

571

in

572

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

573


574

let vars_env = compute_vars_env m in

575

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

576

let new_instrs, _, _, printed_vars, _ =

577

rewrite_instrs

578

m.MC.mname.LT.node_id

579

m

580

constEnv

581

vars_env

582

m

583

s.MC.step_instrs

584

ranges

585

formal_env

586

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

587

inputs are considered as

588

already printed *)))

589

vars_to_print

590

in

591

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

592

let unused = (Vars.diff all_local_vars printed_vars) in

593

let locals =

594

if not (Vars.is_empty unused) then (

595

Format.eprintf "Unused local vars: [%a]. Removing them.@.@?"

596

Vars.pp unused;

597

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

598

)

599

else

600

s.MC.step_locals

601

in

602

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

603


604


605

let machine_t2machine_t_optimized_by_salsa constEnv mt =

606

try

607

if !debug then Format.eprintf "@[<v 8>[salsa] Optimizing machine %s@ " mt.MC.mname.LT.node_id;

608

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

609

if !debug then Format.eprintf "@]@ ";

610

{ mt with MC.mstep = new_step }

611


612


613

with FormalEnv.NoDefinition v as exp >

614

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

615

raise exp

616


617


618

(* Local Variables: *)

619

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

620

(* End: *)

621

