1

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

2

(* *)

3

(* The LustreC compiler toolset / The LustreC Development Team *)

4

(* Copyright 2012   ONERA  CNRS  INPT *)

5

(* *)

6

(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)

7

(* under the terms of the GNU Lesser General Public License *)

8

(* version 2.1. *)

9

(* *)

10

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

11


12

open Utils

13

open Lustre_types

14

open Machine_code_types

15

open Corelang

16

open Causality

17

open Machine_code_common

18

open Dimension

19

module Mpfr = Lustrec_mpfr

20


21

let pp_elim m fmt elim =

22

pp_imap ~comment:"/* elim table: */" (pp_val m) fmt elim

23

(* Format.fprintf fmt "@[<hv 0>@[<hv 2>{ /* elim table: */";

24

* IMap.iter (fun v expr > Format.fprintf fmt "@ %s > %a," v (pp_val m) expr) elim;

25

* Format.fprintf fmt "@]@ }@]" *)

26


27

let rec eliminate m elim instr =

28

let e_expr = eliminate_expr m elim in

29

match get_instr_desc instr with

30

 MLocalAssign (i, v) >

31

update_instr_desc instr (MLocalAssign (i, e_expr v))

32

 MStateAssign (i, v) >

33

update_instr_desc instr (MStateAssign (i, e_expr v))

34

 MSetReset _

35

 MNoReset _

36

 MClearReset

37

 MResetAssign _

38

 MSpec _

39

 MComment _ >

40

instr

41

 MStep (il, i, vl) >

42

update_instr_desc instr (MStep (il, i, List.map e_expr vl))

43

 MBranch (g, hl) >

44

update_instr_desc instr

45

(MBranch

46

( e_expr g,

47

List.map (fun (l, il) > l, List.map (eliminate m elim) il) hl ))

48


49

and eliminate_expr m elim expr =

50

let eliminate_expr = eliminate_expr m in

51

match expr.value_desc with

52

 Var v > (

53

if is_memory m v then expr

54

else try IMap.find v.var_id elim with Not_found > expr)

55

 Fun (id, vl) >

56

{ expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl) }

57

 Array vl >

58

{ expr with value_desc = Array (List.map (eliminate_expr elim) vl) }

59

 Access (v1, v2) >

60

{

61

expr with

62

value_desc = Access (eliminate_expr elim v1, eliminate_expr elim v2);

63

}

64

 Power (v1, v2) >

65

{

66

expr with

67

value_desc = Power (eliminate_expr elim v1, eliminate_expr elim v2);

68

}

69

 Cst _  ResetFlag >

70

expr

71


72

let eliminate_dim elim dim =

73

Dimension.expr_replace_expr

74

(fun v >

75

try dimension_of_value (IMap.find v elim)

76

with Not_found > mkdim_ident dim.dim_loc v)

77

dim

78


79

(* 8th Jan 2016: issues when merging salsa with horn_encoding: The following

80

functions seem unsused. They have to be adapted to the new type for expr *)

81


82

let unfold_expr_offset m offset expr =

83

List.fold_left

84

(fun res > function

85

 Index i >

86

mk_val

87

(Access (res, value_of_dimension m i))

88

(Types.array_element_type res.value_type)

89

 Field _ >

90

Format.eprintf "internal error: not yet implemented !";

91

assert false)

92

expr offset

93


94

let rec simplify_cst_expr m offset typ cst =

95

match offset, cst with

96

 [], _ >

97

mk_val (Cst cst) typ

98

 Index i :: q, Const_array cl when Dimension.is_dimension_const i >

99

let elt_typ = Types.array_element_type typ in

100

simplify_cst_expr m q elt_typ

101

(List.nth cl (Dimension.size_const_dimension i))

102

 Index i :: q, Const_array cl >

103

let elt_typ = Types.array_element_type typ in

104

unfold_expr_offset m [ Index i ]

105

(mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)

106

 Field f :: q, Const_struct fl >

107

let fld_typ = Types.struct_field_type typ f in

108

simplify_cst_expr m q fld_typ (List.assoc f fl)

109

 _ >

110

Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@."

111

Printers.pp_const cst;

112

assert false

113


114

let simplify_expr_offset m expr =

115

let rec simplify offset expr =

116

match offset, expr.value_desc with

117

 Field _ :: _, _ >

118

failwith "not yet implemented"

119

 _, Fun (id, vl) when Basic_library.is_value_internal_fun expr >

120

mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type

121

 _, Fun _  _, Var _ >

122

unfold_expr_offset m offset expr

123

 _, Cst cst >

124

simplify_cst_expr m offset expr.value_type cst

125

 _, Access (expr, i) >

126

simplify (Index (dimension_of_value i) :: offset) expr

127

 _, ResetFlag >

128

expr

129

 [], _ >

130

expr

131

 Index _ :: q, Power (expr, _) >

132

simplify q expr

133

 Index i :: q, Array vl when Dimension.is_dimension_const i >

134

simplify q (List.nth vl (Dimension.size_const_dimension i))

135

 Index i :: q, Array vl >

136

unfold_expr_offset m [ Index i ]

137

(mk_val (Array (List.map (simplify q) vl)) expr.value_type)

138

(*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr

139

(Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)

140

with e > (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr

141

(Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)

142

in

143

simplify [] expr

144


145

let rec simplify_instr_offset m instr =

146

match get_instr_desc instr with

147

 MLocalAssign (v, expr) >

148

update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))

149

 MStateAssign (v, expr) >

150

update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))

151

 MSetReset _

152

 MNoReset _

153

 MClearReset

154

 MResetAssign _

155

 MSpec _

156

 MComment _ >

157

instr

158

 MStep (outputs, id, inputs) >

159

update_instr_desc instr

160

(MStep (outputs, id, List.map (simplify_expr_offset m) inputs))

161

 MBranch (cond, brl) >

162

update_instr_desc instr

163

(MBranch

164

( simplify_expr_offset m cond,

165

List.map (fun (l, il) > l, simplify_instrs_offset m il) brl ))

166


167

and simplify_instrs_offset m instrs = List.map (simplify_instr_offset m) instrs

168


169

let is_scalar_const c =

170

match c with Const_real _  Const_int _  Const_tag _ > true  _ > false

171


172

(* An instruction v = expr may (and will) be unfolded iff:  either expr is

173

atomic (no complex expressions, only const, vars and array/struct accesses) 

174

or v has a fanin <= 1 (used at most once) *)

175

let is_unfoldable_expr fanin expr =

176

let rec unfold_const offset cst =

177

match offset, cst with

178

 _, Const_int _  _, Const_real _  _, Const_tag _ >

179

true

180

 Field f :: q, Const_struct fl >

181

unfold_const q (List.assoc f fl)

182

 [], Const_struct _ >

183

false

184

 Index i :: q, Const_array cl when Dimension.is_dimension_const i >

185

unfold_const q (List.nth cl (Dimension.size_const_dimension i))

186

 _, Const_array _ >

187

false

188

 _ >

189

assert false

190

in

191

let rec unfold offset expr =

192

match offset, expr.value_desc with

193

 _, Cst cst >

194

unfold_const offset cst

195

 _, Var _ >

196

true

197

 [], Power _  [], Array _ >

198

false

199

 Index _ :: q, Power (v, _) >

200

unfold q v

201

 Index i :: q, Array vl when Dimension.is_dimension_const i >

202

unfold q (List.nth vl (Dimension.size_const_dimension i))

203

 _, Array _ >

204

false

205

 _, Access (v, i) >

206

unfold (Index (dimension_of_value i) :: offset) v

207

 _, Fun (_, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr

208

>

209

List.for_all (unfold offset) vl

210

 _, Fun _ >

211

false

212

 _ >

213

assert false

214

in

215

unfold [] expr

216


217

let basic_unfoldable_assign fanin v expr =

218

try

219

let d = Hashtbl.find fanin v.var_id in

220

is_unfoldable_expr d expr

221

with Not_found > false

222


223

let unfoldable_assign fanin v expr =

224

(if !Options.mpfr then Mpfr.unfoldable_value expr else true)

225

&& basic_unfoldable_assign fanin v expr

226


227

let merge_elim elim1 elim2 =

228

let merge _ e1 e2 =

229

match e1, e2 with

230

 Some e1, Some e2 >

231

if e1 = e2 then Some e1 else None

232

 _, Some e2 >

233

Some e2

234

 Some e1, _ >

235

Some e1

236

 _ >

237

None

238

in

239

IMap.merge merge elim1 elim2

240


241

(* see if elim has to take in account the provided instr: if so, update elim and

242

return the remove flag, otherwise, the expression should be kept and elim is

243

left untouched *)

244

let rec instrs_unfold m fanin elim instrs =

245

let elim, rev_instrs =

246

List.fold_left

247

(fun (elim, instrs) instr >

248

(* each subexpression in instr that could be rewritten by the elim set

249

is rewritten *)

250

let instr = eliminate m (IMap.map fst elim) instr in

251

(* if instr is a simple local assign, then (a) elim is simplified with

252

it (b) it is stored as the elim set *)

253

instr_unfold m fanin instrs elim instr)

254

(elim, []) instrs

255

in

256

elim, List.rev rev_instrs

257


258

and instr_unfold m fanin instrs (elim : (value_t * eq) IMap.t) instr =

259

(* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE

260

IT@." pp_instr instr;*)

261

match get_instr_desc instr with

262

(* Simple cases*)

263

 MStep ([ v ], id, vl)

264

when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)

265

>

266

instr_unfold m fanin instrs elim

267

(update_instr_desc instr

268

(MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))

269

 MLocalAssign (v, expr)

270

when (not (is_clock_dec_type v.var_dec_type.ty_dec_desc))

271

&& unfoldable_assign fanin v expr >

272

(* we don't eliminate clock definitions *)

273

let new_eq =

274

Corelang.mkeq (desome instr.lustre_eq).eq_loc

275

([ v.var_id ], (desome instr.lustre_eq).eq_rhs)

276

in

277

IMap.add v.var_id (expr, new_eq) elim, instrs

278

 MBranch (g, hl) when false >

279

let elim_branches =

280

List.map (fun (h, l) > h, instrs_unfold m fanin elim l) hl

281

in

282

let elim, branches =

283

List.fold_right

284

(fun (h, (e, l)) (elim, branches) >

285

merge_elim elim e, (h, l) :: branches)

286

elim_branches (elim, [])

287

in

288

elim, update_instr_desc instr (MBranch (g, branches)) :: instrs

289

 _ >

290

elim, instr :: instrs

291

(* default case, we keep the instruction and do not modify elim *)

292


293

(** We iterate in the order, recording simple local assigns in an accumulator 1.

294

each expression is rewritten according to the accumulator 2. local assigns

295

then rewrite occurrences of the lhs in the computed accumulator *)

296


297

let static_call_unfold elim (inst, (n, args)) =

298

let replace v =

299

try dimension_of_value (IMap.find v elim)

300

with Not_found > Dimension.mkdim_ident Location.dummy_loc v

301

in

302

inst, (n, List.map (Dimension.expr_replace_expr replace) args)

303


304

(** Perform optimization on machine code:  iterate through step instructions

305

and remove simple local assigns *)

306

let machine_unfold fanin elim machine =

307

Log.report ~level:3 (fun fmt >

308

Format.fprintf fmt "machine_unfold %s %a@ " machine.mname.node_id

309

(pp_elim machine) (IMap.map fst elim));

310

let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in

311

let elim_vars, instrs =

312

instrs_unfold machine fanin elim_consts machine.mstep.step_instrs

313

in

314

let instrs = simplify_instrs_offset machine instrs in

315

let checks =

316

List.map

317

(fun (loc, check) >

318

loc, eliminate_expr machine (IMap.map fst elim_vars) check)

319

machine.mstep.step_checks

320

in

321

let locals =

322

List.filter

323

(fun v > not (IMap.mem v.var_id elim_vars))

324

machine.mstep.step_locals

325

in

326

let elim_consts = IMap.map fst elim_consts in

327

let minstances =

328

List.map (static_call_unfold elim_consts) machine.minstances

329

in

330

let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls in

331

( {

332

machine with

333

mstep =

334

{

335

machine.mstep with

336

step_locals = locals;

337

step_instrs = instrs;

338

step_checks = checks;

339

};

340

mconst;

341

minstances;

342

mcalls;

343

},

344

elim_vars )

345


346

let instr_of_const top_const =

347

let const = const_of_top top_const in

348

let loc = const.const_loc in

349

let id = const.const_id in

350

let vdecl =

351

mkvar_decl loc

352

( id,

353

mktyp Location.dummy_loc Tydec_any,

354

mkclock loc Ckdec_any,

355

true,

356

None,

357

None )

358

in

359

let vdecl = { vdecl with var_type = const.const_type } in

360

let lustre_eq =

361

mkeq loc ([ const.const_id ], mkexpr loc (Expr_const const.const_value))

362

in

363

mkinstr ~lustre_eq

364

(MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))

365


366

(* We do not perform this optimization on contract nodes since there is not

367

explicit dependence btw variables and their use in contracts. *)

368

let machines_unfold consts node_schs machines =

369

List.fold_right

370

(fun m (machines, removed) >

371

let is_contract =

372

match m.mspec.mnode_spec with Some (Contract _) > true  _ > false

373

in

374

if is_contract then m :: machines, removed

375

else

376

let fanin =

377

(IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table

378

in

379

let elim_consts, _ =

380

instrs_unfold m fanin IMap.empty (List.map instr_of_const consts)

381

in

382

let m, removed_m = machine_unfold fanin elim_consts m in

383

m :: machines, IMap.add m.mname.node_id removed_m removed)

384

machines ([], IMap.empty)

385


386

let get_assign_lhs instr =

387

match get_instr_desc instr with

388

 MLocalAssign (v, e) >

389

mk_val (Var v) e.value_type

390

 MStateAssign (v, e) >

391

mk_val (Var v) e.value_type

392

 _ >

393

assert false

394


395

let get_assign_rhs instr =

396

match get_instr_desc instr with

397

 MLocalAssign (_, e)  MStateAssign (_, e) >

398

e

399

 _ >

400

assert false

401


402

let is_assign instr =

403

match get_instr_desc instr with

404

 MLocalAssign _  MStateAssign _ >

405

true

406

 _ >

407

false

408


409

let mk_assign m v e =

410

match v.value_desc with

411

 Var v >

412

if is_memory m v then MStateAssign (v, e) else MLocalAssign (v, e)

413

 _ >

414

assert false

415


416

let rec assigns_instr instr assign =

417

match get_instr_desc instr with

418

 MLocalAssign (i, _)  MStateAssign (i, _) >

419

VSet.add i assign

420

 MStep (ol, _, _) >

421

List.fold_right VSet.add ol assign

422

 MBranch (_, hl) >

423

List.fold_right (fun (_, il) > assigns_instrs il) hl assign

424

 _ >

425

assign

426


427

and assigns_instrs instrs assign =

428

List.fold_left (fun assign instr > assigns_instr instr assign) assign instrs

429


430

(* and substitute_expr subst expr = match expr with  Var v > (try IMap.find

431

expr subst with Not_found > expr)  Fun (id, vl) > Fun (id, List.map

432

(substitute_expr subst) vl)  Array(vl) > Array(List.map (substitute_expr

433

subst) vl)  Access(v1, v2) > Access(substitute_expr subst v1,

434

substitute_expr subst v2)  Power(v1, v2) > Power(substitute_expr subst v1,

435

substitute_expr subst v2)  Cst _ > expr *)

436


437

(** Finds a substitute for [instr] in [instrs], i.e. another instr' with the

438

same rhs expression. Then substitute this expression with the first assigned

439

var *)

440

let subst_instr m subst instrs instr =

441

(* Format.eprintf "subst instr: %a@." (pp_instr m) instr; *)

442

let instr = eliminate m subst instr in

443

let instr_v = get_assign_lhs instr in

444

let instr_e = get_assign_rhs instr in

445

try

446

(* Searching for equivalent asssign *)

447

let instr' =

448

List.find

449

(fun instr' > is_assign instr' && get_assign_rhs instr' = instr_e)

450

instrs

451

in

452

(* Registering the instr_v as instr'_v while replacing *)

453

match instr_v.value_desc with

454

 Var v > (

455

let instr'_v = get_assign_lhs instr' in

456

if not (is_memory m v) then

457

(* The current instruction defines a local variables, ie not memory, we

458

can just record the relationship and continue *)

459

IMap.add v.var_id instr'_v subst, instrs

460

else

461

(* The current instruction defines a memory. We need to keep the

462

definition, simplified *)

463

match instr'_v.value_desc with

464

 Var v' >

465

if not (is_memory m v') then

466

(* We define v' = v. Don't need to update the records. *)

467

let instr =

468

eliminate m subst

469

(update_instr_desc instr (mk_assign m instr_v instr'_v))

470

in

471

subst, instr :: instrs

472

else

473

(* Last case, v', the lhs of the previous similar definition is,

474

itself, a memory *)

475


476

(* TODO regarder avec X. Il me semble qu'on peut faire plus simple: *)

477

(* Filtering out the list of instructions:  we copy in the same

478

order the list of instr in instrs (fold_right)  if the current

479

instr is this instr' then apply the elimination with v' > v on

480

instr' before recording it as an instruction. *)

481

let subst_v' = IMap.add v'.var_id instr_v IMap.empty in

482

let instrs' =

483

snd

484

(List.fold_right

485

(fun instr (ok, instrs) >

486

( ok  instr = instr',

487

if ok then instr :: instrs

488

else if instr = instr' then instrs

489

else eliminate m subst_v' instr :: instrs ))

490

instrs (false, []))

491

in

492

IMap.add v'.var_id instr_v subst, instr :: instrs'

493

 _ >

494

assert false)

495

 _ >

496

assert false

497

with Not_found >

498

(* No such equivalent expr: keeping the definition *)

499

subst, instr :: instrs

500


501

(*  [subst] : hashtable from ident to (simple) definition it is an equivalence

502

table  [elim] : set of eliminated variables  [instrs] : previous

503

instructions, which [instr] is compared against  [instr] : current

504

instruction, normalized by [subst] *)

505


506

(** Common subexpression elimination for machine instructions *)

507

let rec instr_cse m (subst, instrs) instr =

508

match get_instr_desc instr with

509

(* Simple cases*)

510

 MStep ([ v ], id, vl)

511

when Basic_library.is_internal_fun id (List.map (fun v > v.value_type) vl)

512

>

513

instr_cse m (subst, instrs)

514

(update_instr_desc instr

515

(MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))

516

 MLocalAssign (v, expr) when is_unfoldable_expr 2 expr >

517

IMap.add v.var_id expr subst, instr :: instrs

518

 _ when is_assign instr >

519

subst_instr m subst instrs instr

520

 _ >

521

subst, instr :: instrs

522


523

(** Apply common subexpression elimination to a sequence of instrs *)

524

let instrs_cse m subst instrs =

525

let subst, rev_instrs = List.fold_left (instr_cse m) (subst, []) instrs in

526

subst, List.rev rev_instrs

527


528

(** Apply common subexpression elimination to a machine  iterate through step

529

instructions and remove simple local assigns *)

530

let machine_cse subst machine =

531

(*Log.report ~level:1 (fun fmt > Format.fprintf fmt "machine_cse %a@."

532

pp_elim subst);*)

533

let _, instrs = instrs_cse machine subst machine.mstep.step_instrs in

534

let assigned = assigns_instrs instrs VSet.empty in

535

{

536

machine with

537

mmemory = List.filter (fun vdecl > VSet.mem vdecl assigned) machine.mmemory;

538

mstep =

539

{

540

machine.mstep with

541

step_locals =

542

List.filter

543

(fun vdecl > VSet.mem vdecl assigned)

544

machine.mstep.step_locals;

545

step_instrs = instrs;

546

};

547

}

548


549

let machines_cse machines = List.map (machine_cse IMap.empty) machines

550


551

(* variable substitution for optimizing purposes *)

552


553

(* checks whether an [instr] is skip and can be removed from program *)

554

let rec instr_is_skip instr =

555

match get_instr_desc instr with

556

 MLocalAssign (i, { value_desc = Var v; _ }) when i = v >

557

true

558

 MStateAssign (i, { value_desc = Var v; _ }) when i = v >

559

true

560

 MBranch (_, hl) >

561

List.for_all (fun (_, il) > instrs_are_skip il) hl

562

 _ >

563

false

564


565

and instrs_are_skip instrs = List.for_all instr_is_skip instrs

566


567

let instr_cons instr cont = if instr_is_skip instr then cont else instr :: cont

568


569

let rec instr_remove_skip instr cont =

570

match get_instr_desc instr with

571

 MLocalAssign (i, { value_desc = Var v; _ }) when i = v >

572

cont

573

 MStateAssign (i, { value_desc = Var v; _ }) when i = v >

574

cont

575

 MBranch (g, hl) >

576

update_instr_desc instr

577

(MBranch (g, List.map (fun (h, il) > h, instrs_remove_skip il []) hl))

578

:: cont

579

 _ >

580

instr :: cont

581


582

and instrs_remove_skip instrs cont =

583

List.fold_right instr_remove_skip instrs cont

584


585

let rec value_replace_var fvar value =

586

match value.value_desc with

587

 Cst _  ResetFlag >

588

value

589

 Var v >

590

{ value with value_desc = Var (fvar v) }

591

 Fun (id, args) >

592

{ value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }

593

 Array vl >

594

{ value with value_desc = Array (List.map (value_replace_var fvar) vl) }

595

 Access (t, i) >

596

{ value with value_desc = Access (value_replace_var fvar t, i) }

597

 Power (v, n) >

598

{ value with value_desc = Power (value_replace_var fvar v, n) }

599


600

let rec instr_replace_var fvar instr cont =

601

match get_instr_desc instr with

602

 MLocalAssign (i, v) >

603

instr_cons

604

(update_instr_desc instr

605

(MLocalAssign (fvar i, value_replace_var fvar v)))

606

cont

607

 MStateAssign (i, v) >

608

instr_cons

609

(update_instr_desc instr (MStateAssign (i, value_replace_var fvar v)))

610

cont

611

 MSetReset _

612

 MNoReset _

613

 MClearReset

614

 MResetAssign _

615

 MSpec _

616

 MComment _ >

617

instr_cons instr cont

618

 MStep (il, i, vl) >

619

instr_cons

620

(update_instr_desc instr

621

(MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)))

622

cont

623

 MBranch (g, hl) >

624

instr_cons

625

(update_instr_desc instr

626

(MBranch

627

( value_replace_var fvar g,

628

List.map (fun (h, il) > h, instrs_replace_var fvar il []) hl )))

629

cont

630


631

and instrs_replace_var fvar instrs cont =

632

List.fold_right (instr_replace_var fvar) instrs cont

633


634

let step_replace_var fvar step =

635

(* Some outputs may have been replaced by locals. We then need to rename those

636

outputs without changing their clocks, etc *)

637

let outputs' =

638

List.map (fun o > { o with var_id = (fvar o).var_id }) step.step_outputs

639

in

640

let locals' =

641

List.fold_left

642

(fun res l >

643

let l' = fvar l in

644

if List.exists (fun o > o.var_id = l'.var_id) outputs' then res

645

else Utils.add_cons l' res)

646

[] step.step_locals

647

in

648

{

649

step with

650

step_checks =

651

List.map (fun (l, v) > l, value_replace_var fvar v) step.step_checks;

652

step_outputs = outputs';

653

step_locals = locals';

654

step_instrs = instrs_replace_var fvar step.step_instrs [];

655

}

656


657

let machine_replace_variables fvar m =

658

{ m with mstep = step_replace_var fvar m.mstep }

659


660

let machine_reuse_variables m reuse =

661

let fvar v = try Hashtbl.find reuse v.var_id with Not_found > v in

662

machine_replace_variables fvar m

663


664

let machines_reuse_variables prog reuse_tables =

665

List.map

666

(fun m >

667

machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables))

668

prog

669


670

let rec instr_assign res instr =

671

match get_instr_desc instr with

672

 MLocalAssign (i, _) >

673

Disjunction.CISet.add i res

674

 MStateAssign (i, _) >

675

Disjunction.CISet.add i res

676

 MBranch (_, hl) >

677

List.fold_left (fun res (_, b) > instrs_assign res b) res hl

678

 MStep (il, _, _) >

679

List.fold_right Disjunction.CISet.add il res

680

 _ >

681

res

682


683

and instrs_assign res instrs = List.fold_left instr_assign res instrs

684


685

let rec instr_constant_assign var instr =

686

match get_instr_desc instr with

687

 MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })

688

 MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) >

689

i = var

690

 MBranch (_, hl) >

691

List.for_all (fun (_, b) > instrs_constant_assign var b) hl

692

 _ >

693

false

694


695

and instrs_constant_assign var instrs =

696

List.fold_left

697

(fun res i >

698

if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then

699

instr_constant_assign var i

700

else res)

701

false instrs

702


703

let rec instr_reduce branches instr1 cont =

704

match get_instr_desc instr1 with

705

 MLocalAssign (_, { value_desc = Cst (Const_tag c); _ }) >

706

instr1 :: (List.assoc c branches @ cont)

707

 MStateAssign (_, { value_desc = Cst (Const_tag c); _ }) >

708

instr1 :: (List.assoc c branches @ cont)

709

 MBranch (g, hl) >

710

update_instr_desc instr1

711

(MBranch (g, List.map (fun (h, b) > h, instrs_reduce branches b []) hl))

712

:: cont

713

 _ >

714

instr1 :: cont

715


716

and instrs_reduce branches instrs cont =

717

match instrs with

718

 [] >

719

cont

720

 [ i ] >

721

instr_reduce branches i cont

722

 i1 :: i2 :: q >

723

i1 :: instrs_reduce branches (i2 :: q) cont

724


725

let rec instrs_fusion instrs =

726

match instrs, List.map get_instr_desc instrs with

727

 [], []  [ _ ], [ _ ] >

728

instrs

729

 i1 :: _ :: q, _ :: MBranch ({ value_desc = Var v; _ }, hl) :: _

730

when instr_constant_assign v i1 >

731

instr_reduce

732

(List.map (fun (h, b) > h, instrs_fusion b) hl)

733

i1 (instrs_fusion q)

734

 i1 :: i2 :: q, _ >

735

i1 :: instrs_fusion (i2 :: q)

736

 _ >

737

assert false

738

(* Other cases should not happen since both lists are of same size *)

739


740

let step_fusion step =

741

{ step with step_instrs = instrs_fusion step.step_instrs }

742


743

let machine_fusion m = { m with mstep = step_fusion m.mstep }

744


745

let machines_fusion prog = List.map machine_fusion prog

746


747

(* Additional function to modify the prog according to removed variables map *)

748


749

let elim_prog_variables prog removed_table =

750

List.map

751

(fun t >

752

match t.top_decl_desc with

753

 Node nd > (

754

match IMap.find_opt nd.node_id removed_table with

755

 Some nd_elim_map >

756

(* Iterating through the elim map to compute  the list of variables

757

to remove  the associated list of lustre definitions x = expr to

758

be used when removing these variables *)

759

let vars_to_replace, defs =

760

(* Recovering vid from node locals *)

761

IMap.fold

762

(fun v (_, eq) (accu_locals, accu_defs) >

763

let locals =

764

try

765

List.find (fun v' > v'.var_id = v) nd.node_locals

766

:: accu_locals

767

with Not_found > accu_locals

768

(* Variable v shall be a global constant, we do no need to

769

eliminate it from the locals *)

770

in

771

(* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc =

772

e.expr_loc } in *)

773

let defs = eq :: accu_defs in

774

locals, defs)

775

nd_elim_map ([], [])

776

in

777


778

let node_locals, node_stmts =

779

List.fold_right

780

(fun stmt (locals, res_stmts) >

781

match stmt with

782

 Aut _ >

783

assert false (* should be processed by now *)

784

 Eq eq > (

785

match eq.eq_lhs with

786

 [] >

787

assert false (* shall not happen *)

788

 _ :: _ :: _ >

789

(* When more than one lhs we just keep the equation and do

790

not delete it *)

791

let eq_rhs' =

792

substitute_expr vars_to_replace defs eq.eq_rhs

793

in

794

locals, Eq { eq with eq_rhs = eq_rhs' } :: res_stmts

795

 [ lhs ] >

796

if List.exists (fun v > v.var_id = lhs) vars_to_replace

797

then

798

(* We remove the def *)

799

List.filter (fun v > v.var_id <> lhs) locals, res_stmts

800

else

801

(* We keep it but modify any use of an eliminatend var *)

802

let eq_rhs' =

803

substitute_expr vars_to_replace defs eq.eq_rhs

804

in

805

locals, Eq { eq with eq_rhs = eq_rhs' } :: res_stmts))

806

nd.node_stmts (nd.node_locals, [])

807

in

808

let nd' = { nd with node_locals; node_stmts } in

809

{ t with top_decl_desc = Node nd' }

810

 None >

811

t)

812

 _ >

813

t)

814

prog

815


816

(*** Main function ***)

817


818

(* This functions produces an optimzed prog * machines It 1 eliminates common

819

subexpressions (TODO how is this different from normalization?) 2 inline

820

constants and eliminate duplicated variables 3 try to reuse variables

821

whenever possible

822


823

When item (2) identified eliminated variables, the initial prog is modified,

824

its normalized recomputed, as well as its scheduling, before regenerating the

825

machines.

826


827

The function returns both the (possibly updated) prog as well as the machines *)

828

let optimize params prog node_schs machine_code =

829

let machine_code =

830

if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then (

831

Log.report ~level:1 (fun fmt >

832

Format.fprintf fmt

833

"@ @[<v 2>.. machines optimization: subexpression elimination@ ");

834

let machine_code = machines_cse machine_code in

835

Log.report ~level:3 (fun fmt >

836

Format.fprintf fmt

837

"@[<v 2>.. generated machines (subexpr elim):@ %a@]@ " pp_machines

838

machine_code);

839

Log.report ~level:1 (fun fmt > Format.fprintf fmt "@]");

840

machine_code)

841

else machine_code

842

in

843

(* Optimize machine code *)

844

let prog, machine_code, removed_table =

845

if

846

!Options.optimization >= 2 && !Options.output <> "emf"

847

(*&& !Options.output <> "horn"*)

848

then (

849

Log.report ~level:1 (fun fmt >

850

Format.fprintf fmt

851

"@ @[<v 2>.. machines optimization: const. inlining (partial eval. \

852

with const)@ ");

853

let machine_code, removed_table =

854

machines_unfold (Corelang.get_consts prog) node_schs machine_code

855

in

856

Log.report ~level:3 (fun fmt >

857

Format.fprintf fmt "@ Eliminated flows: %a@ "

858

(pp_imap (fun fmt m > pp_elim empty_machine fmt (IMap.map fst m)))

859

removed_table);

860

Log.report ~level:3 (fun fmt >

861

Format.fprintf fmt

862

"@ @[<v 2>.. generated machines (const inlining):@ %a@]@ "

863

pp_machines machine_code);

864

(* If variables were eliminated, relaunch the normalization/machine

865

generation *)

866

let prog, machine_code, removed_table =

867

if IMap.is_empty removed_table then

868

(* stopping here, no need to reupdate the prog *)

869

prog, machine_code, removed_table

870

else

871

let prog = elim_prog_variables prog removed_table in

872

(* Mini stage1 *)

873

let prog = Normalization.normalize_prog params prog in

874

let prog = SortProg.sort_nodes_locals prog in

875

(* Mini stage2: note that we do not protect against alg. loop since

876

this should have been handled before *)

877

let prog, node_schs = Scheduling.schedule_prog prog in

878

let machine_code = Machine_code.translate_prog prog node_schs in

879

(* Mini stage2 machine optimiation *)

880

let machine_code, removed_table =

881

machines_unfold (Corelang.get_consts prog) node_schs machine_code

882

in

883

prog, machine_code, removed_table

884

in

885

Log.report ~level:1 (fun fmt > Format.fprintf fmt "@]");

886

prog, machine_code, removed_table)

887

else prog, machine_code, IMap.empty

888

in

889

(* Optimize machine code *)

890

let machine_code =

891

if !Options.optimization >= 3 && not (Backends.is_functional ()) then (

892

Log.report ~level:1 (fun fmt >

893

Format.fprintf fmt

894

".. machines optimization: minimize stack usage by reusing \

895

variables@,");

896

let node_schs =

897

Scheduling.remove_prog_inlined_locals removed_table node_schs

898

in

899

let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in

900

machines_fusion (machines_reuse_variables machine_code reuse_tables))

901

else machine_code

902

in

903


904

prog, machine_code

905


906

(* Local Variables: *)

907

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

908

(* End: *)
