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


22

let pp_elim m fmt elim =

23

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

24

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

25

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

26

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

27


28

let rec eliminate m elim instr =

29

let e_expr = eliminate_expr m elim in

30

match get_instr_desc instr with

31

 MSpec _  MComment _ > instr

32

 MLocalAssign (i,v) > update_instr_desc instr (MLocalAssign (i, e_expr v))

33

 MStateAssign (i,v) > update_instr_desc instr (MStateAssign (i, e_expr v))

34

 MReset _ > instr

35

 MNoReset _ > instr

36

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

37

 MBranch (g,hl) >

38

update_instr_desc instr (

39

MBranch

40

(e_expr g,

41

(List.map

42

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

43

hl

44

)

45

)

46

)

47


48

and eliminate_expr m elim expr =

49

let eliminate_expr = eliminate_expr m in

50

match expr.value_desc with

51

 Var v > if is_memory m v then

52

expr

53

else

54

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

55

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

56

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

57

 Access(v1, v2) > { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}

58

 Power(v1, v2) > { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}

59

 Cst _ > expr

60


61

let eliminate_dim elim dim =

62

Dimension.expr_replace_expr

63

(fun v > try

64

dimension_of_value (IMap.find v elim)

65

with Not_found > mkdim_ident dim.dim_loc v)

66

dim

67


68


69

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

70

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

71

*)

72


73

let unfold_expr_offset m offset expr =

74

List.fold_left

75

(fun res > (function  Index i > mk_val (Access (res, value_of_dimension m i))

76

(Types.array_element_type res.value_type)

77

 Field _ > Format.eprintf "internal error: not yet implemented !"; assert false))

78

expr offset

79


80

let rec simplify_cst_expr m offset typ cst =

81

match offset, cst with

82

 [] , _

83

> mk_val (Cst cst) typ

84

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

85

> let elt_typ = Types.array_element_type typ in

86

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

87

 Index i :: q, Const_array cl

88

> let elt_typ = Types.array_element_type typ in

89

unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)

90

 Field f :: q, Const_struct fl

91

> let fld_typ = Types.struct_field_type typ f in

92

simplify_cst_expr m q fld_typ (List.assoc f fl)

93

 _ > (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Printers.pp_const cst; assert false)

94


95

let simplify_expr_offset m expr =

96

let rec simplify offset expr =

97

match offset, expr.value_desc with

98

 Field _ ::_ , _ > failwith "not yet implemented"

99

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

100

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

101

 _ , Fun _

102

 _ , Var _ > unfold_expr_offset m offset expr

103

 _ , Cst cst > simplify_cst_expr m offset expr.value_type cst

104

 _ , Access (expr, i) > simplify (Index (dimension_of_value i) :: offset) expr

105

 [] , _ > expr

106

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

107

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

108

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

109

 Index i :: q, Array vl > unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify q) vl)) expr.value_type)

110

(*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)

111

with e > (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)

112

in simplify [] expr

113


114

let rec simplify_instr_offset m instr =

115

match get_instr_desc instr with

116

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

117

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

118

 MReset _ > instr

119

 MNoReset _ > instr

120

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

121

 MBranch (cond, brl)

122

> update_instr_desc instr (

123

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

124

)

125

 MSpec _  MComment _ > instr

126


127

and simplify_instrs_offset m instrs =

128

List.map (simplify_instr_offset m) instrs

129


130

let is_scalar_const c =

131

match c with

132

 Const_real _

133

 Const_int _

134

 Const_tag _ > true

135

 _ > false

136


137

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

138

 either expr is atomic

139

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

140

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

141

*)

142

let is_unfoldable_expr fanin expr =

143

let rec unfold_const offset cst =

144

match offset, cst with

145

 _ , Const_int _

146

 _ , Const_real _

147

 _ , Const_tag _ > true

148

 Field f :: q, Const_struct fl > unfold_const q (List.assoc f fl)

149

 [] , Const_struct _ > false

150

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

151

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

152

 _ , Const_array _ > false

153

 _ > assert false in

154

let rec unfold offset expr =

155

match offset, expr.value_desc with

156

 _ , Cst cst > unfold_const offset cst

157

 _ , Var _ > true

158

 [] , Power _

159

 [] , Array _ > false

160

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

161

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

162

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

163

 _ , Array _ > false

164

 _ , Access (v, i) > unfold (Index (dimension_of_value i) :: offset) v

165

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

166

> List.for_all (unfold offset) vl

167

 _ , Fun _ > false

168

 _ > assert false

169

in unfold [] expr

170


171

let basic_unfoldable_assign fanin v expr =

172

try

173

let d = Hashtbl.find fanin v.var_id

174

in is_unfoldable_expr d expr

175

with Not_found > false

176


177

let unfoldable_assign fanin v expr =

178

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

179

&& basic_unfoldable_assign fanin v expr

180


181

let merge_elim elim1 elim2 =

182

let merge _ e1 e2 =

183

match e1, e2 with

184

 Some e1, Some e2 > if e1 = e2 then Some e1 else None

185

 _ , Some e2 > Some e2

186

 Some e1, _ > Some e1

187

 _ > None

188

in IMap.merge merge elim1 elim2

189


190

(* see if elim has to take in account the provided instr:

191

if so, update elim and return the remove flag,

192

otherwise, the expression should be kept and elim is left untouched *)

193

let rec instrs_unfold m fanin elim instrs =

194

let elim, rev_instrs =

195

List.fold_left (fun (elim, instrs) instr >

196

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

197

rewritten *)

198

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

199

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

200

is stored as the elim set *)

201

instr_unfold m fanin instrs elim instr

202

) (elim, []) instrs

203

in elim, List.rev rev_instrs

204


205

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

206

(* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*)

207

match get_instr_desc instr with

208

(* Simple cases*)

209

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

210

> instr_unfold m fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))

211

 MLocalAssign(v, expr) when not (is_clock_dec_type v.var_dec_type.ty_dec_desc) && unfoldable_assign fanin v expr

212

> (* we don't eliminate clock definitions *)

213

let new_eq =

214

Corelang.mkeq

215

(desome instr.lustre_eq).eq_loc

216

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

217

in

218

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

219

 MBranch(g, hl) when false

220

> let elim_branches = List.map (fun (h, l) > (h, instrs_unfold m fanin elim l)) hl in

221

let (elim, branches) =

222

List.fold_right

223

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

224

elim_branches (elim, [])

225

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

226

 _

227

> (elim, instr :: instrs)

228

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

229


230


231

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

232

1. each expression is rewritten according to the accumulator

233

2. local assigns then rewrite occurrences of the lhs in the computed accumulator

234

*)

235


236

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

237

let replace v =

238

try

239

dimension_of_value (IMap.find v elim)

240

with Not_found > Dimension.mkdim_ident Location.dummy_loc v

241

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

242


243

(** Perform optimization on machine code:

244

 iterate through step instructions and remove simple local assigns

245


246

*)

247

let machine_unfold fanin elim machine =

248

Log.report ~level:3 (fun fmt > Format.fprintf fmt "machine_unfold %s %a@ "

249

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

250

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

251

let elim_vars, instrs = instrs_unfold machine fanin elim_consts machine.mstep.step_instrs in

252

let instrs = simplify_instrs_offset machine instrs in

253

let checks = List.map

254

(fun (loc, check) >

255

loc,

256

eliminate_expr machine (IMap.map fst elim_vars) check

257

) machine.mstep.step_checks

258

in

259

let locals = List.filter (fun v > not (IMap.mem v.var_id elim_vars)) machine.mstep.step_locals in

260

let elim_consts = IMap.map fst elim_consts in

261

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

262

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

263

in

264

{

265

machine with

266

mstep = {

267

machine.mstep with

268

step_locals = locals;

269

step_instrs = instrs;

270

step_checks = checks

271

};

272

mconst = mconst;

273

minstances = minstances;

274

mcalls = mcalls;

275

},

276

elim_vars

277


278

let instr_of_const top_const =

279

let const = const_of_top top_const in

280

let loc = const.const_loc in

281

let id = const.const_id in

282

let vdecl = mkvar_decl loc (id, mktyp Location.dummy_loc Tydec_any, mkclock loc Ckdec_any, true, None, None) in

283

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

284

let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in

285

mkinstr

286

~lustre_eq

287

True

288

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

289


290

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

291

is not explicit dependence btw variables and their use in

292

contracts. *)

293

let machines_unfold consts node_schs machines =

294

List.fold_right (fun m (machines, removed) >

295

let is_contract = match m.mspec.mnode_spec with

296

 Some (Contract _) > true

297

 _ > false in

298

if is_contract then

299

m :: machines, removed

300

else

301

let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in

302

let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in

303

let (m, removed_m) = machine_unfold fanin elim_consts m in

304

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

305

)

306

machines

307

([], IMap.empty)

308


309

let get_assign_lhs instr =

310

match get_instr_desc instr with

311

 MLocalAssign(v, e) > mk_val (Var v) e.value_type

312

 MStateAssign(v, e) > mk_val (Var v) e.value_type

313

 _ > assert false

314


315

let get_assign_rhs instr =

316

match get_instr_desc instr with

317

 MLocalAssign(_, e)

318

 MStateAssign(_, e) > e

319

 _ > assert false

320


321

let is_assign instr =

322

match get_instr_desc instr with

323

 MLocalAssign _

324

 MStateAssign _ > true

325

 _ > false

326


327

let mk_assign m v e =

328

match v.value_desc with

329

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

330

 _ > assert false

331


332

let rec assigns_instr instr assign =

333

match get_instr_desc instr with

334

 MLocalAssign (i,_)

335

 MStateAssign (i,_) > VSet.add i assign

336

 MStep (ol, _, _) > List.fold_right VSet.add ol assign

337

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

338

 _ > assign

339


340

and assigns_instrs instrs assign =

341

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

342


343

(*

344

and substitute_expr subst expr =

345

match expr with

346

 Var v > (try IMap.find expr subst with Not_found > expr)

347

 Fun (id, vl) > Fun (id, List.map (substitute_expr subst) vl)

348

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

349

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

350

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

351

 Cst _ > expr

352

*)

353

(** Finds a substitute for [instr] in [instrs],

354

i.e. another instr' with the same rhs expression.

355

Then substitute this expression with the first assigned var

356

*)

357

let subst_instr m subst instrs instr =

358

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

359

let instr = eliminate m subst instr in

360

let instr_v = get_assign_lhs instr in

361

let instr_e = get_assign_rhs instr in

362

try

363

(* Searching for equivalent asssign *)

364

let instr' = List.find (fun instr' > is_assign instr' &&

365

get_assign_rhs instr' = instr_e) instrs in

366

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

367

match instr_v.value_desc with

368

 Var v >

369

let instr'_v = get_assign_lhs instr' in

370

if not (is_memory m v) then

371

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

372

memory, we can just record the relationship and continue

373

*)

374

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

375

else (

376

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

377

the definition, simplified *)

378

(match instr'_v.value_desc with

379

 Var v' >

380

if not (is_memory m v') then

381

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

382

let instr = eliminate m subst (update_instr_desc instr (mk_assign m instr_v instr'_v)) in

383

subst, instr :: instrs

384

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

385

definition is, itself, a memory *)

386


387

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

388

(* Filtering out the list of instructions:

389

 we copy in the same order the list of instr in instrs (fold_right)

390

 if the current instr is this instr' then apply

391

the elimination with v' > v on instr' before recording it as an instruction.

392

*)

393

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

394

let instrs' =

395

snd

396

(List.fold_right

397

(fun instr (ok, instrs) >

398

(ok  instr = instr',

399

if ok then

400

instr :: instrs

401

else

402

if instr = instr' then

403

instrs

404

else

405

eliminate m subst_v' instr :: instrs))

406

instrs (false, []))

407

in

408

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

409

)

410

 _ > assert false)

411

)

412

 _ > assert false

413


414

with Not_found >

415

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

416

subst, instr :: instrs

417


418

(** Common subexpression elimination for machine instructions *)

419

(*  [subst] : hashtable from ident to (simple) definition

420

it is an equivalence table

421

 [elim] : set of eliminated variables

422

 [instrs] : previous instructions, which [instr] is compared against

423

 [instr] : current instruction, normalized by [subst]

424

*)

425

let rec instr_cse m (subst, instrs) instr =

426

match get_instr_desc instr with

427

(* Simple cases*)

428

 MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v > v.value_type) vl)

429

> instr_cse m (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))

430

 MLocalAssign(v, expr) when is_unfoldable_expr 2 expr

431

> (IMap.add v.var_id expr subst, instr :: instrs)

432

 _ when is_assign instr

433

> subst_instr m subst instrs instr

434

 _ > (subst, instr :: instrs)

435


436

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

437

*)

438

let instrs_cse m subst instrs =

439

let subst, rev_instrs =

440

List.fold_left (instr_cse m) (subst, []) instrs

441

in subst, List.rev rev_instrs

442


443

(** Apply common subexpression elimination to a machine

444

 iterate through step instructions and remove simple local assigns

445

*)

446

let machine_cse subst machine =

447

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

448

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

449

let assigned = assigns_instrs instrs VSet.empty

450

in

451

{

452

machine with

453

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

454

mstep = {

455

machine.mstep with

456

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

457

step_instrs = instrs

458

}

459

}

460


461

let machines_cse machines =

462

List.map

463

(machine_cse IMap.empty)

464

machines

465


466

(* variable substitution for optimizing purposes *)

467


468

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

469

let rec instr_is_skip instr =

470

match get_instr_desc instr with

471

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

472

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

473

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

474

 _ > false

475

and instrs_are_skip instrs =

476

List.for_all instr_is_skip instrs

477


478

let instr_cons instr cont =

479

if instr_is_skip instr then cont else instr::cont

480


481

let rec instr_remove_skip instr cont =

482

match get_instr_desc instr with

483

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

484

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

485

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

486

 _ > instr::cont

487


488

and instrs_remove_skip instrs cont =

489

List.fold_right instr_remove_skip instrs cont

490


491

let rec value_replace_var fvar value =

492

match value.value_desc with

493

 Cst _ > value

494

 Var v > { value with value_desc = Var (fvar v) }

495

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

496

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

497

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

498

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

499


500

let rec instr_replace_var fvar instr cont =

501

match get_instr_desc instr with

502

 MSpec _  MComment _ > instr_cons instr cont

503

 MLocalAssign (i, v) > instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont

504

 MStateAssign (i, v) > instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont

505

 MReset _ > instr_cons instr cont

506

 MNoReset _ > instr_cons instr cont

507

 MStep (il, i, vl) > instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont

508

 MBranch (g, hl) > instr_cons (update_instr_desc instr (MBranch (value_replace_var fvar g, List.map (fun (h, il) > (h, instrs_replace_var fvar il [])) hl))) cont

509


510

and instrs_replace_var fvar instrs cont =

511

List.fold_right (instr_replace_var fvar) instrs cont

512


513

let step_replace_var fvar step =

514

(* Some outputs may have been replaced by locals.

515

We then need to rename those outputs

516

without changing their clocks, etc *)

517

let outputs' =

518

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

519

let locals' =

520

List.fold_left (fun res l >

521

let l' = fvar l in

522

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

523

then res

524

else Utils.add_cons l' res)

525

[] step.step_locals in

526

{ step with

527

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

528

step_outputs = outputs';

529

step_locals = locals';

530

step_instrs = instrs_replace_var fvar step.step_instrs [];

531

}

532


533

let machine_replace_variables fvar m =

534

{ m with

535

mstep = step_replace_var fvar m.mstep

536

}

537


538

let machine_reuse_variables m reuse =

539

let fvar v =

540

try

541

Hashtbl.find reuse v.var_id

542

with Not_found > v in

543

machine_replace_variables fvar m

544


545

let machines_reuse_variables prog reuse_tables =

546

List.map

547

(fun m >

548

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

549

) prog

550


551

let rec instr_assign res instr =

552

match get_instr_desc instr with

553

 MLocalAssign (i, _) > Disjunction.CISet.add i res

554

 MStateAssign (i, _) > Disjunction.CISet.add i res

555

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

556

 MStep (il, _, _) > List.fold_right Disjunction.CISet.add il res

557

 _ > res

558


559

and instrs_assign res instrs =

560

List.fold_left instr_assign res instrs

561


562

let rec instr_constant_assign var instr =

563

match get_instr_desc instr with

564

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

565

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

566

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

567

 _ > false

568


569

and instrs_constant_assign var instrs =

570

List.fold_left (fun res i > if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then instr_constant_assign var i else res) false instrs

571


572

let rec instr_reduce branches instr1 cont =

573

match get_instr_desc instr1 with

574

 MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) > instr1 :: (List.assoc c branches @ cont)

575

 MStateAssign (_, { value_desc = Cst (Const_tag c); _}) > instr1 :: (List.assoc c branches @ cont)

576

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

577

 _ > instr1 :: cont

578


579

and instrs_reduce branches instrs cont =

580

match instrs with

581

 [] > cont

582

 [i] > instr_reduce branches i cont

583

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

584


585

let rec instrs_fusion instrs =

586

match instrs, List.map get_instr_desc instrs with

587

 [], []

588

 [_], [_] >

589

instrs

590

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

591

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

592

 i1::i2::q, _ >

593

i1 :: instrs_fusion (i2::q)

594

 _ > assert false (* Other cases should not happen since both lists are of same size *)

595


596

let step_fusion step =

597

{ step with

598

step_instrs = instrs_fusion step.step_instrs;

599

}

600


601

let machine_fusion m =

602

{ m with

603

mstep = step_fusion m.mstep

604

}

605


606

let machines_fusion prog =

607

List.map machine_fusion prog

608


609


610

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

611


612

let elim_prog_variables prog removed_table =

613

List.map (

614

fun t >

615

match t.top_decl_desc with

616

Node nd >

617

if IMap.mem nd.node_id removed_table then

618

let nd_elim_map = IMap.find nd.node_id removed_table in

619

(* Iterating through the elim map to compute

620

 the list of variables to remove

621

 the associated list of lustre definitions x = expr to

622

be used when removing these variables *)

623

let vars_to_replace, defs = (* Recovering vid from node locals *)

624

IMap.fold (fun v (_,eq) (accu_locals, accu_defs) >

625

let locals =

626

try

627

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

628

with Not_found > accu_locals (* Variable v shall

629

be a global

630

constant, we do no

631

need to eliminate

632

it from the locals

633

*)

634

in

635

(* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc = e.expr_loc } in *)

636

let defs = eq::accu_defs in

637

locals, defs

638

) nd_elim_map ([], [])

639

in

640


641

let new_locals, new_stmts =

642

List.fold_right (fun stmt (locals, res_stmts) >

643

match stmt with

644

Aut _ > assert false (* should be processed by now *)

645

 Eq eq > (

646

match eq.eq_lhs with

647

 [] > assert false (* shall not happen *)

648

 _::_::_ >

649

(* When more than one lhs we just keep the

650

equation and do not delete it *)

651

let eq_rhs' = substitute_expr vars_to_replace defs eq.eq_rhs in

652

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

653

 [lhs] >

654

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

655

(* We remove the def *)

656

List.filter (fun l > l.var_id != lhs) locals,

657

res_stmts

658

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

659

let eq_rhs' = substitute_expr vars_to_replace defs eq.eq_rhs in

660

locals,

661

(Eq { eq with eq_rhs = eq_rhs' })::res_stmts

662


663

)

664

) nd.node_stmts (nd.node_locals,[])

665

in

666

let nd' = { nd with

667

node_locals = new_locals;

668

node_stmts = new_stmts;

669

}

670

in

671

{ t with top_decl_desc = Node nd' }

672

else

673

t

674

 _ > t

675

) prog

676


677

(*** Main function ***)

678


679

(*

680

This functions produces an optimzed prog * machines

681

It

682

1 eliminates common subexpressions (TODO how is this different from normalization?)

683

2 inline constants and eliminate duplicated variables

684

3 try to reuse variables whenever possible

685


686

When item (2) identified eliminated variables, the initial prog is modified, its normalized recomputed, as well as its scheduling, before regenerating the machines.

687


688

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

689


690


691

*)

692

let optimize params prog node_schs machine_code =

693

let machine_code =

694

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

695

Log.report ~level:1

696

(fun fmt > Format.fprintf fmt "@ @[<v 2>.. machines optimization: subexpression elimination@ ");

697

let machine_code = machines_cse machine_code in

698

Log.report ~level:3 (fun fmt > Format.fprintf fmt "@[<v 2>.. generated machines (subexpr elim):@ %a@]@ "

699

pp_machines machine_code);

700

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

701

machine_code

702

end else

703

machine_code

704

in

705

(* Optimize machine code *)

706

let prog, machine_code, removed_table =

707

if !Options.optimization >= 2

708

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

709

then begin

710

Log.report ~level:1

711

(fun fmt >

712

Format.fprintf fmt

713

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

714

let machine_code, removed_table =

715

machines_unfold (Corelang.get_consts prog) node_schs machine_code in

716

Log.report ~level:3

717

(fun fmt >

718

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

719

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

720

Log.report ~level:3

721

(fun fmt >

722

Format.fprintf fmt

723

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

724

pp_machines machine_code);

725

(* If variables were eliminated, relaunch the

726

normalization/machine generation *)

727

let prog, machine_code, removed_table =

728

if IMap.is_empty removed_table then

729

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

730

prog, machine_code, removed_table

731

else (

732

let prog = elim_prog_variables prog removed_table in

733

(* Mini stage1 *)

734

let prog = Normalization.normalize_prog params prog in

735

let prog = SortProg.sort_nodes_locals prog in

736

(* Mini stage2: note that we do not protect against

737

alg. loop since this should have been handled before *)

738

let prog, node_schs = Scheduling.schedule_prog prog in

739

let machine_code = Machine_code.translate_prog prog node_schs in

740

(* Mini stage2 machine optimiation *)

741

let machine_code, removed_table =

742

machines_unfold (Corelang.get_consts prog) node_schs machine_code in

743

prog, machine_code, removed_table

744

)

745

in

746

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

747

prog, machine_code, removed_table

748


749

end else

750

prog, machine_code, IMap.empty

751

in

752

(* Optimize machine code *)

753

let machine_code =

754

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

755

begin

756

Log.report ~level:1 (fun fmt > Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");

757

let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in

758

let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in

759

machines_fusion (machines_reuse_variables machine_code reuse_tables)

760

end

761

else

762

machine_code

763

in

764


765


766

prog, List.rev machine_code

767


768


769

(* Local Variables: *)

770

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

771

(* End: *)
