1

(* We try to avoid opening modules here *)

2

module ST = Salsa.SalsaTypes

3

module SDT = SalsaDatatypes

4

module LT = LustreSpec

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.MC.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

match e.LT.value_desc with

33

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

34

 LT.LocalVar _ LT.StateVar _

35

 LT.Cst _ > Vars.empty

36

 LT.Fun (_, args) >

37

List.fold_left

38

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

39

Vars.empty args

40

 LT.Array _

41

 LT.Access _

42

 LT.Power _ > assert false

43


44

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

45

let rec get_read_vars instrs =

46

match instrs with

47

[] > Vars.empty

48

 i::tl > (

49

let vars_tl = get_read_vars tl in

50

match i with

51

 LT.MLocalAssign(_,e)

52

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

53

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

54

 LT.MBranch(e, branches) > (

55

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

56

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

57

)

58

 LT.MReset _

59

 LT.MComment _ > Vars.empty

60

)

61


62

let rec get_written_vars instrs =

63

match instrs with

64

[] > Vars.empty

65

 i::tl > (

66

let vars_tl = get_written_vars tl in

67

match i with

68

 LT.MLocalAssign(v,_)

69

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

70

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

71

 LT.MBranch(_, branches) > (

72

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

73

)

74

 LT.MReset _

75

 LT.MComment _ > Vars.empty

76

)

77


78

let rec iterTransformExpr fresh_id e_salsa abstractEnv old_range =

79

let new_expr, new_range =

80

Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv

81

in

82

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

83

if Salsa.Float.errLt new_range old_range < 0 then

84


85

iterTransformExpr fresh_id new_expr abstractEnv new_range

86

else

87

new_expr, new_range

88


89


90

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

91

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

92

let rec opt_expr ranges formalEnv e =

93

match e.LT.value_desc with

94

 LT.Cst cst >

95

Format.eprintf "optmizing constant expr ? @ ";

96

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

97

constant *)

98

let typ = Typing.type_const Location.dummy_loc cst in

99

if Types.is_real_type typ then

100

opt_num_expr ranges formalEnv e

101

else e, None

102

 LT.LocalVar v

103

 LT.StateVar v >

104

if not (Vars.mem v printed_vars) &&

105

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

106

then

107

opt_num_expr ranges formalEnv e

108

else

109

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

110

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

111

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

112

(* else e, None *)

113

 LT.Fun (fun_id, args) > (

114

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

115

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

116

if Types.is_real_type e.LT.value_type then

117

opt_num_expr ranges formalEnv e

118

else (

119

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

120

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

121

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

122

)

123

)

124

 LT.Array _

125

 LT.Access _

126

 LT.Power _ > assert false

127

and opt_num_expr ranges formalEnv e =

128

if debug then Format.eprintf "Optimizing expression %a@ " MC.pp_val e;

129

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

130

(* Convert expression *)

131

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

132

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

133

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

134


135

(* Convert formalEnv *)

136

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

137

let formalEnv_salsa =

138

FormalEnv.fold (fun id expr accu >

139

(id, value_t2salsa_expr constEnv expr)::accu

140

) formalEnv [] in

141

if debug then Format.eprintf "Formal env converted to salsa@ ";

142

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

143

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

144

Salsa.Rewrite.substVars

145

e_salsa

146

formalEnv_salsa

147

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

148

in

149

if debug then Format.eprintf "Substituted def in expr@ ";

150

let abstractEnv = Hashtbl.fold

151

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

152

ranges

153

[]

154

in

155

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

156

(* The expression is partially evaluated by the available ranges

157

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

158

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

159

 on garde *)

160

if debug then Format.eprintf "avant avant eval part@ ";

161

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

162

let e_salsa =

163

Salsa.Float.evalPartExpr

164

e_salsa

165

(Salsa.Float.valEnv2ExprEnv abstractEnv)

166

([] (* no blacklisted variables *))

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


173

if Vars.cardinal free_vars > 0 then (

174

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

175

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)

176

MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);

177

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

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

try

183

if debug then

184

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

185

MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa)

186

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

187

;

188

let range_before = Float.evalExpr e_salsa abstractEnv in

189


190

let new_e_salsa, e_val =

191

iterTransformExpr fresh_id e_salsa abstractEnv range_before

192

in

193


194

let range_after = Float.evalExpr new_e_salsa abstractEnv in

195


196

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

197

if debug then Format.eprintf "@ @[<v>old: %a@ new: %a@ old range: %a@ new range: %a@ computed range: %a@]"

198

MC.pp_val e

199

MC.pp_val new_e

200

RangesInt.pp_val range_before

201

RangesInt.pp_val range_after

202

RangesInt.pp_val e_val;

203

new_e, Some e_val

204

with Not_found > assert false

205

 Salsa.Epeg_types.EPEGError _ > (

206

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

207

e, None

208

)

209

)

210


211


212


213

in

214

if debug then

215

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

216

MC.pp_val e

217

FormalEnv.pp formalEnv

218

RangesInt.pp ranges;

219

let res = opt_expr ranges formalEnv e in

220

Format.eprintf "@]@ ";

221

res

222


223


224


225

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

226

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

227

let assign_vars nodename constEnv vars_env printed_vars ranges formalEnv vars_to_print =

228

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

229


230

let ordered_vars =

231

List.stable_sort

232

(FormalEnv.get_sort_fun formalEnv)

233

(Vars.elements vars_to_print)

234

in

235

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

236

List.fold_right (

237

fun v (accu_instr, accu_ranges) >

238

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

239

try

240

(* Obtaining unfold expression of v in formalEnv *)

241

let v_def = FormalEnv.get_def formalEnv v in

242

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

243

let instr =

244

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

245

LT.MLocalAssign(v, e)

246

else

247

LT.MStateAssign(v, e)

248

in

249

instr::accu_instr,

250

(match r with

251

 None > ranges

252

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

253

with FormalEnv.NoDefinition _ > (

254

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

255

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

256

)

257

) ordered_vars ([], ranges)

258


259

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

260

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

261

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

262

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

263

let assign_vars = assign_vars nodename constEnv vars_env in

264

if debug then (

265

Format.eprintf "@ ";

266

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

267

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

268

);

269

match instrs with

270

 [] >

271

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

272

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

273

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

274

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

275

instrs,

276

ranges',

277

formalEnv,

278

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

279

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

280


281

 hd_instr::tl_instrs >

282

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

283

formalEnv, possibly ranges and vars_to_print *)

284

begin

285

let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print =

286

match hd_instr with

287

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

288

(* LocalAssign are injected into formalEnv *)

289

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

290

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

291

[], (* no instr generated *)

292

ranges, (* no new range computed *)

293

formalEnv',

294

printed_vars, (* no new printed vars *)

295

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

296


297

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

298


299

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

300

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

301

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

302

assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)

303

in

304

instrs',

305

ranges', (* no new range computed *)

306

formalEnv', (* formelEnv already updated *)

307

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

308

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

309


310

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

311


312

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

313

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

314

outputs. vd is removed from remaining vars_to_print *)

315

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

316

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

317

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

318

assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)

319

in

320

instrs',

321

ranges', (* no new range computed *)

322

formalEnv, (* formelEnv already updated *)

323

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

324

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

325


326

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

327

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

328

well its dependencies *)

329

let required_vars = get_expr_real_vars vt in

330

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

331

already

332

produced

333

variables *)

334

let prefix_instr, ranges =

335

assign_vars printed_vars ranges formalEnv required_vars in

336

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

337

let new_instr =

338

match hd_instr with

339

 LT.MLocalAssign _ > LT.MLocalAssign(vd,vt')

340

 _ > LT.MStateAssign(vd,vt')

341

in

342

let written_vars = Vars.add vd required_vars in

343

prefix_instr@[new_instr],

344

ranges, (* no new range computed *)

345

formalEnv, (* formelEnv untouched *)

346

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

347

new printed vars *)

348

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

349

variables to print *)

350


351

 LT.MStep(vdl,id,vtl) >

352

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

353

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

354

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

355

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

356

call are removed from vars to be printed *)

357

let node = called_node_id m id in

358

let node_id = Corelang.node_name node in

359

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

360

if node_id = "_arrow" then

361

match vdl with

362

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

363

[t; t], [t]

364

 _ > assert false (* should not happen *)

365

else

366

fun_types node

367

in

368

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

369

let vtl', vtl_ranges = List.fold_right2 (

370

fun e typ_e (exprl, range_l)>

371

if Types.is_real_type typ_e then

372

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

373

e'::exprl, r'::range_l

374

else

375

e::exprl, None::range_l

376

) vtl tin ([], [])

377

in

378

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

379

let required_vars =

380

List.fold_left2

381

(fun accu e typ_e >

382

if Types.is_real_type typ_e then

383

Vars.union accu (get_expr_real_vars e)

384

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

385

accu

386

)

387

Vars.empty

388

vtl' tin

389

in

390

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

391

Vars.pp required_vars

392

Vars.pp printed_vars

393

Vars.pp (Vars.diff required_vars printed_vars)

394

;

395

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

396

already

397

produced

398

variables *)

399

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

400

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

401

instrs' @ [LT.MStep(vdl,id,vtl')], (* New instrs *)

402

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

403

formalEnv,

404

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

405

Vars.diff vars_to_print written_vars

406


407

 LT.MBranch(vt, branches) >

408

(* Required variables to compute vt are introduced.

409

Then each branch is refactored specifically

410

*)

411

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

412

let required_vars = get_expr_real_vars vt in

413

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

414

already

415

produced

416

variables *)

417

let prefix_instr, ranges =

418

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

419


420

let printed_vars = Vars.union printed_vars required_vars in

421


422

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

423


424

let read_vars_tl = get_read_vars tl_instrs in

425

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

426

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

427

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

428

let b_write_vars = get_written_vars b_instrs in

429

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

430

let b_fe = formalEnv in (* because of side effect

431

data, we copy it for

432

each branch *)

433

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

434

rewrite_instrs nodename constEnv vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print

435

in

436

(* b_vars should be empty *)

437

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

438


439

(* Producing the refactored branch *)

440

(b_l, b_instrs') :: new_branches,

441

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

442

use union instead of

443

inter to ease the

444

bootstrap *)

445

RangesInt.merge merged_ranges b_ranges

446


447

) branches ([], required_vars, ranges) in

448

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

449

prefix_instr@[LT.MBranch(vt', branches')],

450

merged_ranges, (* Only step functions call within branches

451

may have produced new ranges. We merge this data by

452

computing the join per variable *)

453

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

454

branch, no new definition should have been computed

455

without being already printed *)

456

Vars.union written_vars printed_vars,

457

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

458

produced within branches *)

459


460


461

 LT.MReset(_)  LT.MComment _ >

462

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

463


464

(* Untouched instruction *)

465

[ hd_instr ], (* unmodified instr *)

466

ranges, (* no new range computed *)

467

formalEnv, (* no formelEnv update *)

468

printed_vars,

469

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

470


471

in

472

let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print =

473

rewrite_instrs

474

nodename

475

constEnv

476

vars_env

477

m

478

tl_instrs

479

ranges

480

formalEnv

481

printed_vars

482

vars_to_print

483

in

484

hd_instrs @ tl_instrs,

485

ranges,

486

formalEnv,

487

printed_vars,

488

vars_to_print

489

end

490


491


492


493


494


495


496

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

497

let salsaStep constEnv m s =

498

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

499

machine annotations or externally provided information *) in

500

let annots = List.fold_left (

501

fun accu annl >

502

List.fold_left (

503

fun accu (key, range) >

504

match key with

505

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

506

 _ > accu

507

) accu annl.LT.annots

508

) [] m.MC.mannot

509

in

510

let ranges =

511

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

512

match value.LT.eexpr_qfexpr.LT.expr_desc with

513

 LT.Expr_tuple [minv; maxv] > (

514

let get_cst e = match e.LT.expr_desc with

515

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

516

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

517

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

518

 _ >

519

Format.eprintf

520

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

521

Printers.pp_expr value.LT.eexpr_qfexpr;

522

assert false

523

in

524

let minv, maxv = get_cst minv, get_cst maxv in

525

if debug then Format.eprintf "%s in [%f, %f]@ " v minv maxv;

526

let irange = Salsa.SalsaTypes.I(minv, maxv) in

527

RangesInt.enlarge ranges v (irange, Salsa.Float.ulp irange)

528

)

529

 _ >

530

Format.eprintf

531

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

532

Printers.pp_expr value.LT.eexpr_qfexpr;

533

assert false

534

) ranges annots

535

in

536

let formal_env = FormalEnv.empty () in

537

let vars_to_print =

538

Vars.real_vars

539

(

540

Vars.union

541

(Vars.of_list m.MC.mmemory)

542

(Vars.of_list s.MC.step_outputs)

543

)

544

in

545

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

546

let vars_env = compute_vars_env m in

547

let new_instrs, _, _, printed_vars, _ =

548

rewrite_instrs

549

m.MC.mname.LT.node_id

550

constEnv

551

vars_env

552

m

553

s.MC.step_instrs

554

ranges

555

formal_env

556

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

557

inputs are considered as

558

already printed *)))

559

vars_to_print

560

in

561

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

562

let unused = (Vars.diff all_local_vars printed_vars) in

563

let locals =

564

if not (Vars.is_empty unused) then (

565

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

566

Vars.pp unused;

567

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

568

)

569

else

570

s.MC.step_locals

571

in

572

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

573


574


575

let machine_t2machine_t_optimized_by_salsa constEnv mt =

576

try

577

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

578

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

579

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

580

{ mt with MC.mstep = new_step }

581


582


583

with FormalEnv.NoDefinition v as exp >

584

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

585

raise exp

586


587


588

(* Local Variables: *)

589

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

590

(* End: *)

591

