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 Spec_types

15

open Machine_code_types

16

open Corelang

17

open Causality

18

open Machine_code_common

19

module Mpfr = Lustrec_mpfr

20


21

let pp_elim m fmt elim =

22

IMap.pp ~comment:"/* elim table: */" (pp_val m) fmt elim

23


24

let eliminate_var_decl elim m v f a =

25

if is_memory m v then a

26

else try

27

f (IMap.find v.var_id elim)

28

with Not_found > a

29


30

let rec eliminate_val m elim expr =

31

let eliminate_val = eliminate_val m in

32

match expr.value_desc with

33

 Var v >

34

eliminate_var_decl elim m v (fun x > x) expr

35

 Fun (id, vl) >

36

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

37

 Array vl >

38

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

39

 Access (v1, v2) >

40

{

41

expr with

42

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

43

}

44

 Power (v1, v2) >

45

{

46

expr with

47

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

48

}

49

 Cst _  ResetFlag >

50

expr

51


52

let eliminate_expr m elim e =

53

let e_val = eliminate_val m elim in

54

match e with

55

 Val v > Val (e_val v)

56

 Var v > eliminate_var_decl elim m v (fun x > Val x) e

57

 _ > e

58


59

let eliminate_pred m elim = function

60

 Transition (s, f, inst, i, vars, r, mems, insts) >

61

let vars = List.filter_map (function

62

 Spec_types.Val v >

63

begin match v.value_desc with

64

 Var vd when IMap.mem vd.var_id elim > None

65

 _ > Some (Val v)

66

end

67

 Spec_types.Var vd when IMap.mem vd.var_id elim > None

68

 e > Some (eliminate_expr m elim e)) vars

69

in

70

Transition (s, f, inst, i, vars, r, mems, insts)

71

 p >

72

p

73


74

let rec eliminate_formula m elim =

75

let e_expr = eliminate_expr m elim in

76

let e_instr i = eliminate_formula m elim i in

77

let e_pred = eliminate_pred m elim in

78

function

79

 Equal (e1, e2) >

80

Equal (e_expr e1, e_expr e2)

81

 And f >

82

And (List.map e_instr f)

83

 Or f >

84

Or (List.map e_instr f)

85

 Imply (a, b) >

86

Imply (e_instr a, e_instr b)

87

 Exists (xs, a) >

88

let xs = List.filter (fun vd > not (IMap.mem vd.var_id elim)) xs in

89

Exists (xs, eliminate_formula m elim a)

90

 Forall (xs, a) >

91

let xs = List.filter (fun vd > not (IMap.mem vd.var_id elim)) xs in

92

Forall (xs, eliminate_formula m elim a)

93

 Ternary (e, a, b) >

94

Ternary (e_expr e, e_instr a, e_instr b)

95

 Predicate p >

96

Predicate (e_pred p)

97

 ExistsMem (f, a, b) >

98

ExistsMem (f, e_instr a, e_instr b)

99

 f >

100

f

101


102

let rec eliminate m elim instr =

103

let e_val = eliminate_val m elim in

104

let instr = { instr with instr_spec = List.map (eliminate_formula m elim) instr.instr_spec } in

105

match get_instr_desc instr with

106

 MLocalAssign (i, v) >

107

update_instr_desc instr (MLocalAssign (i, e_val v))

108

 MStateAssign (i, v) >

109

update_instr_desc instr (MStateAssign (i, e_val v))

110

 MSetReset _

111

 MNoReset _

112

 MClearReset

113

 MResetAssign _

114

 MSpec _

115

 MComment _ >

116

instr

117

 MStep (il, i, vl) >

118

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

119

 MBranch (g, hl) >

120

update_instr_desc

121

instr

122

(MBranch

123

( e_val g,

124

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

125


126

let eliminate_transition m elim t =

127

{ t with

128

tvars = List.filter (fun vd > not (IMap.mem vd.var_id elim)) t.tvars;

129

tformula = eliminate_formula m elim t.tformula }

130


131

(* XXX: UNUSED *)

132

(* let eliminate_dim elim dim =

133

* Dimension.expr_replace_expr

134

* (fun v >

135

* try dimension_of_value (IMap.find v elim)

136

* with Not_found > mkdim_ident dim.dim_loc v)

137

* dim *)

138


139

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

140

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

141


142

let unfold_expr_offset m offset expr =

143

List.fold_left

144

(fun res > function

145

 Index i >

146

mk_val

147

(Access (res, value_of_dimension m i))

148

(Types.array_element_type res.value_type)

149

 Field _ >

150

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

151

assert false)

152

expr

153

offset

154


155

let rec simplify_cst_expr m offset typ cst =

156

match offset, cst with

157

 [], _ >

158

mk_val (Cst cst) typ

159

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

160

let elt_typ = Types.array_element_type typ in

161

simplify_cst_expr m q elt_typ (List.nth cl (Dimension.size_const i))

162

 Index i :: q, Const_array cl >

163

let elt_typ = Types.array_element_type typ in

164

unfold_expr_offset

165

m

166

[ Index i ]

167

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

168

 Field f :: q, Const_struct fl >

169

let fld_typ = Types.struct_field_type typ f in

170

simplify_cst_expr m q fld_typ (List.assoc f fl)

171

 _ >

172

Format.eprintf

173

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

174

Printers.pp_const

175

cst;

176

assert false

177


178

let simplify_expr_offset m expr =

179

let rec simplify offset expr =

180

match offset, expr.value_desc with

181

 Field _ :: _, _ >

182

failwith "not yet implemented"

183

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

184

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

185

 _, Fun _  _, Var _ >

186

unfold_expr_offset m offset expr

187

 _, Cst cst >

188

simplify_cst_expr m offset expr.value_type cst

189

 _, Access (expr, i) >

190

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

191

 _, ResetFlag >

192

expr

193

 [], _ >

194

expr

195

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

196

simplify q expr

197

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

198

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

199

 Index i :: q, Array vl >

200

unfold_expr_offset

201

m

202

[ Index i ]

203

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

204

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

205

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

206

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

207

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

208

in

209

simplify [] expr

210


211

let rec simplify_instr_offset m instr =

212

match get_instr_desc instr with

213

 MLocalAssign (v, expr) >

214

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

215

 MStateAssign (v, expr) >

216

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

217

 MSetReset _

218

 MNoReset _

219

 MClearReset

220

 MResetAssign _

221

 MSpec _

222

 MComment _ >

223

instr

224

 MStep (outputs, id, inputs) >

225

update_instr_desc

226

instr

227

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

228

 MBranch (cond, brl) >

229

update_instr_desc

230

instr

231

(MBranch

232

( simplify_expr_offset m cond,

233

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

234


235

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

236


237

(* XXX: UNUSED *)

238

(* let is_scalar_const c =

239

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

240


241

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

242

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

243

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

244

let is_unfoldable_expr fanin expr =

245

let rec unfold_const offset cst =

246

match offset, cst with

247

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

248

true

249

 Field f :: q, Const_struct fl >

250

unfold_const q (List.assoc f fl)

251

 [], Const_struct _ >

252

false

253

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

254

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

255

 _, Const_array _ >

256

false

257

 _ >

258

assert false

259

in

260

let rec unfold offset expr =

261

match offset, expr.value_desc with

262

 _, Cst cst >

263

unfold_const offset cst

264

 _, Var _ >

265

true

266

 [], Power _  [], Array _ >

267

false

268

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

269

unfold q v

270

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

271

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

272

 _, Array _ >

273

false

274

 _, Access (v, i) >

275

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

276

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

277

>

278

List.for_all (unfold offset) vl

279

 _, Fun _ >

280

false

281

 _ >

282

assert false

283

in

284

unfold [] expr

285


286

let basic_unfoldable_assign fanin v expr =

287

try

288

let d = Hashtbl.find fanin v.var_id in

289

is_unfoldable_expr d expr

290

with Not_found > false

291


292

let unfoldable_assign fanin v expr =

293

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

294

&& basic_unfoldable_assign fanin v expr

295


296

let merge_elim elim1 elim2 =

297

let merge _ e1 e2 =

298

match e1, e2 with

299

 Some e1, Some e2 >

300

if e1 = e2 then Some e1 else None

301

 _, Some e2 >

302

Some e2

303

 Some e1, _ >

304

Some e1

305

 _ >

306

None

307

in

308

IMap.merge merge elim1 elim2

309


310

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

311

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

312

left untouched *)

313

let rec instrs_unfold m fanin elim instrs =

314

let elim, rev_instrs =

315

List.fold_left

316

(fun (elim, instrs) instr >

317

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

318

is rewritten *)

319

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

320

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

321

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

322

instr_unfold m fanin instrs elim instr)

323

(elim, [])

324

instrs

325

in

326

elim, List.rev rev_instrs

327


328

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

329

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

330

IT@." pp_instr instr;*)

331

match get_instr_desc instr with

332

(* Simple cases*)

333

 MStep ([ v ], id, vl)

334

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

335

>

336

instr_unfold

337

m

338

fanin

339

instrs

340

elim

341

(update_instr_desc

342

instr

343

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

344

 MLocalAssign (v, expr)

345

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

346

&& unfoldable_assign fanin v expr >

347

(* we don't eliminate clock definitions *)

348

let new_eq =

349

Corelang.mkeq

350

(desome instr.lustre_eq).eq_loc

351

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

352

in

353

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

354

 MBranch (g, hl) when false >

355

let elim_branches =

356

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

357

in

358

let elim, branches =

359

List.fold_right

360

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

361

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

362

elim_branches

363

(elim, [])

364

in

365

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

366

 _ >

367

elim, instr :: instrs

368

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

369


370

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

371

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

372

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

373


374

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

375

let replace v =

376

try dimension_of_value (IMap.find v elim)

377

with Not_found > Dimension.mkdim_ident Location.dummy v

378

in

379

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

380


381

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

382

and remove simple local assigns *)

383

let machine_unfold fanin elim machine =

384

Log.report ~level:3 (fun fmt >

385

Format.fprintf

386

fmt

387

"machine_unfold %s %a@ "

388

machine.mname.node_id

389

(pp_elim machine)

390

(IMap.map fst elim));

391

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

392

let elim_vars, instrs =

393

instrs_unfold machine fanin elim_consts machine.mstep.step_instrs

394

in

395

let step_instrs = simplify_instrs_offset machine instrs in

396

let step_checks =

397

List.map

398

(fun (loc, check) >

399

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

400

machine.mstep.step_checks

401

in

402

let step_locals =

403

List.filter

404

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

405

machine.mstep.step_locals

406

in

407

let mtransitions = List.map (eliminate_transition machine (IMap.map fst elim_vars)) machine.mspec.mtransitions in

408

let elim_consts = IMap.map fst elim_consts in

409

let minstances =

410

List.map (static_call_unfold elim_consts) machine.minstances

411

in

412

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

413

( {

414

machine with

415

mstep =

416

{

417

machine.mstep with

418

step_locals;

419

step_instrs;

420

step_checks;

421

};

422

mspec =

423

{

424

machine.mspec with

425

mtransitions

426

};

427

mconst;

428

minstances;

429

mcalls;

430

},

431

elim_vars )

432


433

let instr_of_const top_const =

434

let const = const_of_top top_const in

435

let loc = const.const_loc in

436

let id = const.const_id in

437

let vdecl =

438

mkvar_decl

439

loc

440

( id,

441

mktyp Location.dummy Tydec_any,

442

mkclock loc Ckdec_any,

443

true,

444

None,

445

None )

446

in

447

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

448

let lustre_eq =

449

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

450

in

451

mkinstr

452

~lustre_eq

453

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

454


455

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

456

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

457

let machines_unfold consts node_schs machines =

458

List.fold_right

459

(fun m (machines, removed) >

460

let is_contract =

461

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

462

in

463

if is_contract then m :: machines, removed

464

else

465

let fanin =

466

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

467

in

468

let elim_consts, _ =

469

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

470

in

471

let m, removed_m = machine_unfold fanin elim_consts m in

472

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

473

machines

474

([], IMap.empty)

475


476

let get_assign_lhs instr =

477

match get_instr_desc instr with

478

 MLocalAssign (v, e) >

479

mk_val (Var v) e.value_type

480

 MStateAssign (v, e) >

481

mk_val (Var v) e.value_type

482

 _ >

483

assert false

484


485

let get_assign_rhs instr =

486

match get_instr_desc instr with

487

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

488

e

489

 _ >

490

assert false

491


492

let is_assign instr =

493

match get_instr_desc instr with

494

 MLocalAssign _  MStateAssign _ >

495

true

496

 _ >

497

false

498


499

let mk_assign m v e =

500

match v.value_desc with

501

 Var v >

502

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

503

 _ >

504

assert false

505


506

let rec assigns_instr instr assign =

507

match get_instr_desc instr with

508

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

509

VSet.add i assign

510

 MStep (ol, _, _) >

511

List.fold_right VSet.add ol assign

512

 MBranch (_, hl) >

513

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

514

 _ >

515

assign

516


517

and assigns_instrs instrs assign =

518

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

519


520

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

521

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

522

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

523

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

524

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

525

substitute_expr subst v2)  Cst _ > expr *)

526


527

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

528

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

529

var *)

530

let subst_instr m subst instrs instr =

531

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

532

let instr = eliminate m subst instr in

533

let instr_v = get_assign_lhs instr in

534

let instr_e = get_assign_rhs instr in

535

try

536

(* Searching for equivalent asssign *)

537

let instr' =

538

List.find

539

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

540

instrs

541

in

542

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

543

match instr_v.value_desc with

544

 Var v > (

545

let instr'_v = get_assign_lhs instr' in

546

if not (is_memory m v) then

547

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

548

can just record the relationship and continue *)

549

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

550

else

551

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

552

definition, simplified *)

553

match instr'_v.value_desc with

554

 Var v' >

555

if not (is_memory m v') then

556

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

557

let instr =

558

eliminate

559

m

560

subst

561

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

562

in

563

subst, instr :: instrs

564

else

565

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

566

itself, a memory *)

567


568

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

569

simple: *)

570

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

571

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

572

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

573

instr' before recording it as an instruction. *)

574

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

575

let instrs' =

576

snd

577

(List.fold_right

578

(fun instr (ok, instrs) >

579

( ok  instr = instr',

580

if ok then instr :: instrs

581

else if instr = instr' then instrs

582

else eliminate m subst_v' instr :: instrs ))

583

instrs

584

(false, []))

585

in

586

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

587

 _ >

588

assert false)

589

 _ >

590

assert false

591

with Not_found >

592

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

593

subst, instr :: instrs

594


595

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

596

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

597

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

598

instruction, normalized by [subst] *)

599


600

(** Common subexpression elimination for machine instructions *)

601

let rec instr_cse m (subst, instrs) instr =

602

match get_instr_desc instr with

603

(* Simple cases*)

604

 MStep ([ v ], id, vl)

605

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

606

>

607

instr_cse

608

m

609

(subst, instrs)

610

(update_instr_desc

611

instr

612

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

613

 MLocalAssign (v, expr) when is_unfoldable_expr 2 expr >

614

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

615

 _ when is_assign instr >

616

subst_instr m subst instrs instr

617

 _ >

618

subst, instr :: instrs

619


620

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

621

let instrs_cse m subst instrs =

622

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

623

subst, List.rev rev_instrs

624


625

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

626

instructions and remove simple local assigns *)

627

let machine_cse subst machine =

628

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

629

pp_elim subst);*)

630

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

631

let assigned = assigns_instrs instrs VSet.empty in

632

{

633

machine with

634

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

635

mstep =

636

{

637

machine.mstep with

638

step_locals =

639

List.filter

640

(fun vdecl > VSet.mem vdecl assigned)

641

machine.mstep.step_locals;

642

step_instrs = instrs;

643

};

644

}

645


646

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

647


648

(* variable substitution for optimizing purposes *)

649


650

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

651

let rec instr_is_skip instr =

652

match get_instr_desc instr with

653

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

654

true

655

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

656

true

657

 MBranch (_, hl) >

658

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

659

 _ >

660

false

661


662

and instrs_are_skip instrs = List.for_all instr_is_skip instrs

663


664

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

665


666

(* XXX: UNUSED *)

667

(* let rec instr_remove_skip instr cont =

668

* match get_instr_desc instr with

669

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

670

* cont

671

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

672

* cont

673

*  MBranch (g, hl) >

674

* update_instr_desc instr

675

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

676

* :: cont

677

*  _ >

678

* instr :: cont

679

*

680

* and instrs_remove_skip instrs cont =

681

* List.fold_right instr_remove_skip instrs cont *)

682


683

let rec value_replace_var fvar value =

684

match value.value_desc with

685

 Cst _  ResetFlag >

686

value

687

 Var v >

688

{ value with value_desc = Var (fvar v) }

689

 Fun (id, args) >

690

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

691

 Array vl >

692

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

693

 Access (t, i) >

694

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

695

 Power (v, n) >

696

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

697


698

let expr_spec_replace fvar = function

699

 Val v >

700

Val (value_replace_var fvar v)

701

 Var v >

702

Var (fvar v)

703

 e >

704

e

705


706

let predicate_spec_replace fvar = function

707

 Transition (s, f, inst, i, vars, r, mems, insts) >

708

Transition

709

(s, f, inst, i, List.map (expr_spec_replace fvar) vars, r, mems, insts)

710

 p >

711

p

712


713

let rec instr_spec_replace fvar =

714

let aux instr = instr_spec_replace fvar instr in

715

function

716

 Equal (e1, e2) >

717

Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2)

718

 And f >

719

And (List.map aux f)

720

 Or f >

721

Or (List.map aux f)

722

 Imply (a, b) >

723

Imply (aux a, aux b)

724

 Exists (xs, a) >

725

let fvar v = if List.mem v xs then v else fvar v in

726

Exists (xs, instr_spec_replace fvar a)

727

 Forall (xs, a) >

728

let fvar v = if List.mem v xs then v else fvar v in

729

Forall (xs, instr_spec_replace fvar a)

730

 Ternary (e, a, b) >

731

Ternary (expr_spec_replace fvar e, aux a, aux b)

732

 Predicate p >

733

Predicate (predicate_spec_replace fvar p)

734

 ExistsMem (f, a, b) >

735

ExistsMem (f, aux a, aux b)

736

 f >

737

f

738


739

let rec instr_replace_var fvar instr =

740

let instr_desc =

741

match instr.instr_desc with

742

 MLocalAssign (i, v) >

743

MLocalAssign (fvar i, value_replace_var fvar v)

744

 MStateAssign (i, v) >

745

MStateAssign (i, value_replace_var fvar v)

746

 MStep (il, i, vl) >

747

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

748

 MBranch (g, hl) >

749

MBranch

750

( value_replace_var fvar g,

751

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

752

 MSetReset _

753

 MNoReset _

754

 MClearReset

755

 MResetAssign _

756

 MSpec _

757

 MComment _ >

758

instr.instr_desc

759

in

760

let instr_spec = List.map (instr_spec_replace fvar) instr.instr_spec in

761

instr_cons { instr with instr_desc; instr_spec }

762


763

and instrs_replace_var fvar instrs cont =

764

List.fold_right (instr_replace_var fvar) instrs cont

765


766

let step_replace_var fvar step =

767

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

768

outputs without changing their clocks, etc *)

769

let outputs' =

770

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

771

in

772

let locals' =

773

List.fold_left

774

(fun res l >

775

let l' = fvar l in

776

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

777

else Utils.add_cons l' res)

778

[]

779

step.step_locals

780

in

781

{

782

step with

783

step_checks =

784

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

785

step_outputs = outputs';

786

step_locals = locals';

787

step_instrs = instrs_replace_var fvar step.step_instrs [];

788

}

789


790

let machine_replace_variables fvar m =

791

{ m with mstep = step_replace_var fvar m.mstep }

792


793

let machine_reuse_variables reuse m =

794

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

795

machine_replace_variables fvar m

796


797

let machines_reuse_variables reuse_tables =

798

List.map (fun m >

799

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

800


801

let rec instr_assign res instr =

802

match get_instr_desc instr with

803

 MLocalAssign (i, _) >

804

Disjunction.CISet.add i res

805

 MStateAssign (i, _) >

806

Disjunction.CISet.add i res

807

 MBranch (_, hl) >

808

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

809

 MStep (il, _, _) >

810

List.fold_right Disjunction.CISet.add il res

811

 _ >

812

res

813


814

and instrs_assign res instrs = List.fold_left instr_assign res instrs

815


816

let rec instr_constant_assign var instr =

817

match get_instr_desc instr with

818

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

819

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

820

i = var

821

 MBranch (_, hl) >

822

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

823

 _ >

824

false

825


826

and instrs_constant_assign var instrs =

827

List.fold_left

828

(fun res i >

829

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

830

instr_constant_assign var i

831

else res)

832

false

833

instrs

834


835

let rec instr_reduce branches instr1 cont =

836

match get_instr_desc instr1 with

837

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

838

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

839

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

840

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

841

 MBranch (g, hl) >

842

update_instr_desc

843

instr1

844

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

845

:: cont

846

 _ >

847

instr1 :: cont

848


849

and instrs_reduce branches instrs cont =

850

match instrs with

851

 [] >

852

cont

853

 [ i ] >

854

instr_reduce branches i cont

855

 i1 :: i2 :: q >

856

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

857


858

let rec instrs_fusion instrs =

859

match instrs with

860

 []  [ _ ] >

861

instrs

862

 i1 :: i2 :: q > (

863

match i2.instr_desc with

864

 MBranch ({ value_desc = Var v; _ }, hl) when instr_constant_assign v i1 >

865

instr_reduce

866

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

867

{ i1 with instr_spec = i1.instr_spec @ i2.instr_spec }

868

(instrs_fusion q)

869

 _ >

870

i1 :: instrs_fusion (i2 :: q))

871


872

let step_fusion step =

873

{ step with step_instrs = instrs_fusion step.step_instrs }

874


875

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

876


877

let machines_fusion prog = List.map machine_fusion prog

878


879

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

880


881

let elim_prog_variables prog removed_table =

882

List.map

883

(fun t >

884

match t.top_decl_desc with

885

 Node nd > (

886

match IMap.find_opt nd.node_id removed_table with

887

 Some nd_elim_map >

888

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

889

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

890

be used when removing these variables *)

891

let vars_to_replace, defs =

892

(* Recovering vid from node locals *)

893

IMap.fold

894

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

895

let locals =

896

try

897

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

898

:: accu_locals

899

with Not_found > accu_locals

900

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

901

eliminate it from the locals *)

902

in

903

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

904

e.expr_loc } in *)

905

let defs = eq :: accu_defs in

906

locals, defs)

907

nd_elim_map

908

([], [])

909

in

910

let node_locals, node_stmts =

911

List.fold_right

912

(fun stmt (locals, res_stmts) >

913

match stmt with

914

 Aut _ >

915

assert false (* should be processed by now *)

916

 Eq eq > (

917

match eq.eq_lhs with

918

 [] >

919

assert false (* shall not happen *)

920

 [lhs] when List.exists (fun v > v.var_id = lhs) vars_to_replace >

921

(* We remove the def *)

922

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

923

 _ >

924

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

925

not delete it *)

926

let eq_rhs =

927

substitute_expr vars_to_replace defs eq.eq_rhs

928

in

929

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

930

nd.node_stmts

931

(nd.node_locals, [])

932

in

933

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

934

{ t with top_decl_desc = Node nd' }

935

 None >

936

t)

937

 _ >

938

t)

939

prog

940


941

(*** Main function ***)

942


943

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

944

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

945

constants and eliminate duplicated variables 3 try to reuse variables

946

whenever possible

947


948

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

949

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

950

machines.

951


952

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

953

machines *)

954

let optimize params prog node_schs machine_code =

955

let machine_code =

956

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

957

Log.report ~level:1 (fun fmt >

958

Format.fprintf

959

fmt

960

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

961

let machine_code = machines_cse machine_code in

962

Log.report ~level:3 (fun fmt >

963

Format.fprintf

964

fmt

965

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

966

pp_machines

967

machine_code);

968

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

969

machine_code)

970

else machine_code

971

in

972

(* Optimize machine code *)

973

let prog, machine_code, removed_table =

974

if

975

!Options.optimization >= 2 && !Options.output <> Options.OutEMF

976

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

977

then (

978

Log.report ~level:1 (fun fmt >

979

Format.fprintf

980

fmt

981

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

982

with const)@ ");

983

let machine_code, removed_table =

984

machines_unfold (Corelang.get_consts prog) node_schs machine_code

985

in

986

Log.report ~level:3 (fun fmt >

987

Format.fprintf

988

fmt

989

"@ Eliminated flows: %a@ "

990

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

991

removed_table);

992

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

993

generation *)

994

let prog, machine_code, removed_table =

995

if IMap.is_empty removed_table then

996

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

997

prog, machine_code, removed_table

998

else

999

let prog = elim_prog_variables prog removed_table in

1000

(* Mini stage1 *)

1001

let prog = Normalization.normalize_prog ~first:false params prog in

1002

let prog = SortProg.sort_nodes_locals prog in

1003

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

1004

this should have been handled before *)

1005

let prog, node_schs = Scheduling.schedule_prog prog in

1006

let machine_code = Machine_code.translate_prog prog node_schs in

1007

(* Mini stage2 machine optimiation *)

1008

let machine_code, removed_table =

1009

machines_unfold (Corelang.get_consts prog) node_schs machine_code

1010

in

1011

prog, machine_code, removed_table

1012

in

1013

Log.report ~level:3 (fun fmt >

1014

Format.fprintf

1015

fmt

1016

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

1017

pp_machines

1018

machine_code);

1019

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

1020

prog, machine_code, removed_table)

1021

else prog, machine_code, IMap.empty

1022

in

1023

(* Optimize machine code *)

1024

let machine_code =

1025

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

1026

Log.report ~level:1 (fun fmt >

1027

Format.fprintf

1028

fmt

1029

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

1030

variables@,");

1031

let node_schs =

1032

Scheduling.remove_prog_inlined_locals removed_table node_schs

1033

in

1034

let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in

1035

machines_fusion (machines_reuse_variables reuse_tables machine_code))

1036

else machine_code

1037

in

1038


1039

prog, machine_code

1040


1041

(* Local Variables: *)

1042

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

1043

(* End: *)
