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


20


21

let pp_elim m fmt elim =

22

begin

23

Format.fprintf fmt "@[{ /* elim table: */@ ";

24

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

25

Format.fprintf fmt "}@ @]";

26

end

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 i > instr

35

 MNoReset i > 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 f > 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 f ::q , _ > 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 id > instr

119

 MNoReset id > 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 i :: 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 (id, 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 k 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@." machine.mname.node_id (pp_elim machine) (IMap.map fst elim));

249

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

250

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

251

let instrs = simplify_instrs_offset machine instrs in

252

let checks = List.map

253

(fun (loc, check) >

254

loc,

255

eliminate_expr machine (IMap.map fst elim_vars) check

256

) machine.mstep.step_checks

257

in

258

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

259

let elim_consts = IMap.map fst elim_consts in

260

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

261

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

262

in

263

{

264

machine with

265

mstep = {

266

machine.mstep with

267

step_locals = locals;

268

step_instrs = instrs;

269

step_checks = checks

270

};

271

mconst = mconst;

272

minstances = minstances;

273

mcalls = mcalls;

274

},

275

elim_vars

276


277

let instr_of_const top_const =

278

let const = const_of_top top_const in

279

let loc = const.const_loc in

280

let id = const.const_id in

281

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

282

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

283

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

284

mkinstr

285

~lustre_eq:lustre_eq

286

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

287


288

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

289

is not explicit dependence btw variables and their use in

290

contracts. *)

291

let machines_unfold consts node_schs machines =

292

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

293

let is_contract = match m.mspec with Some (Contract _) > true  _ > false in

294

if is_contract then

295

m::machines, removed

296

else

297

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

298

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

299

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

300

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

301

)

302

machines

303

([], IMap.empty)

304


305

let get_assign_lhs instr =

306

match get_instr_desc instr with

307

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

308

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

309

 _ > assert false

310


311

let get_assign_rhs instr =

312

match get_instr_desc instr with

313

 MLocalAssign(_, e)

314

 MStateAssign(_, e) > e

315

 _ > assert false

316


317

let is_assign instr =

318

match get_instr_desc instr with

319

 MLocalAssign _

320

 MStateAssign _ > true

321

 _ > false

322


323

let mk_assign m v e =

324

match v.value_desc with

325

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

326

 _ > assert false

327


328

let rec assigns_instr instr assign =

329

match get_instr_desc instr with

330

 MLocalAssign (i,_)

331

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

332

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

333

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

334

 _ > assign

335


336

and assigns_instrs instrs assign =

337

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

338


339

(*

340

and substitute_expr subst expr =

341

match expr with

342

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

343

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

344

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

345

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

346

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

347

 Cst _ > expr

348

*)

349

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

350

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

351

Then substitute this expression with the first assigned var

352

*)

353

let subst_instr m subst instrs instr =

354

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

355

let instr = eliminate m subst instr in

356

let instr_v = get_assign_lhs instr in

357

let instr_e = get_assign_rhs instr in

358

try

359

(* Searching for equivalent asssign *)

360

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

361

get_assign_rhs instr' = instr_e) instrs in

362

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

363

match instr_v.value_desc with

364

 Var v >

365

let instr'_v = get_assign_lhs instr' in

366

if not (is_memory m v) then

367

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

368

memory, we can just record the relationship and continue

369

*)

370

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

371

else (

372

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

373

the definition, simplified *)

374

(match instr'_v.value_desc with

375

 Var v' >

376

if not (is_memory m v') then

377

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

378

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

379

subst, instr :: instrs

380

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

381

definition is, itself, a memory *)

382


383

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

384

(* Filtering out the list of instructions:

385

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

386

 if the current instr is this instr' then apply

387

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

388

*)

389

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

390

let instrs' =

391

snd

392

(List.fold_right

393

(fun instr (ok, instrs) >

394

(ok  instr = instr',

395

if ok then

396

instr :: instrs

397

else

398

if instr = instr' then

399

instrs

400

else

401

eliminate m subst_v' instr :: instrs))

402

instrs (false, []))

403

in

404

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

405

)

406

 _ > assert false)

407

)

408

 _ > assert false

409


410

with Not_found >

411

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

412

subst, instr :: instrs

413


414

(** Common subexpression elimination for machine instructions *)

415

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

416

it is an equivalence table

417

 [elim] : set of eliminated variables

418

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

419

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

420

*)

421

let rec instr_cse m (subst, instrs) instr =

422

match get_instr_desc instr with

423

(* Simple cases*)

424

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

425

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

426

 MLocalAssign(v, expr) when is_unfoldable_expr 2 expr

427

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

428

 _ when is_assign instr

429

> subst_instr m subst instrs instr

430

 _ > (subst, instr :: instrs)

431


432

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

433

*)

434

let instrs_cse m subst instrs =

435

let subst, rev_instrs =

436

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

437

in subst, List.rev rev_instrs

438


439

(** Apply common subexpression elimination to a machine

440

 iterate through step instructions and remove simple local assigns

441

*)

442

let machine_cse subst machine =

443

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

444

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

445

let assigned = assigns_instrs instrs VSet.empty

446

in

447

{

448

machine with

449

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

450

mstep = {

451

machine.mstep with

452

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

453

step_instrs = instrs

454

}

455

}

456


457

let machines_cse machines =

458

List.map

459

(machine_cse IMap.empty)

460

machines

461


462

(* variable substitution for optimizing purposes *)

463


464

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

465

let rec instr_is_skip instr =

466

match get_instr_desc instr with

467

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

468

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

469

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

470

 _ > false

471

and instrs_are_skip instrs =

472

List.for_all instr_is_skip instrs

473


474

let instr_cons instr cont =

475

if instr_is_skip instr then cont else instr::cont

476


477

let rec instr_remove_skip instr cont =

478

match get_instr_desc instr with

479

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

480

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

481

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

482

 _ > instr::cont

483


484

and instrs_remove_skip instrs cont =

485

List.fold_right instr_remove_skip instrs cont

486


487

let rec value_replace_var fvar value =

488

match value.value_desc with

489

 Cst c > value

490

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

491

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

492

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

493

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

494

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

495


496

let rec instr_replace_var fvar instr cont =

497

match get_instr_desc instr with

498

 MSpec _  MComment _ > instr_cons instr cont

499

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

500

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

501

 MReset i > instr_cons instr cont

502

 MNoReset i > instr_cons instr cont

503

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

504

 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

505


506

and instrs_replace_var fvar instrs cont =

507

List.fold_right (instr_replace_var fvar) instrs cont

508


509

let step_replace_var fvar step =

510

(* Some outputs may have been replaced by locals.

511

We then need to rename those outputs

512

without changing their clocks, etc *)

513

let outputs' =

514

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

515

let locals' =

516

List.fold_left (fun res l >

517

let l' = fvar l in

518

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

519

then res

520

else Utils.add_cons l' res)

521

[] step.step_locals in

522

{ step with

523

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

524

step_outputs = outputs';

525

step_locals = locals';

526

step_instrs = instrs_replace_var fvar step.step_instrs [];

527

}

528


529

let rec machine_replace_variables fvar m =

530

{ m with

531

mstep = step_replace_var fvar m.mstep

532

}

533


534

let machine_reuse_variables m reuse =

535

let fvar v =

536

try

537

Hashtbl.find reuse v.var_id

538

with Not_found > v in

539

machine_replace_variables fvar m

540


541

let machines_reuse_variables prog reuse_tables =

542

List.map

543

(fun m >

544

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

545

) prog

546


547

let rec instr_assign res instr =

548

match get_instr_desc instr with

549

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

550

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

551

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

552

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

553

 _ > res

554


555

and instrs_assign res instrs =

556

List.fold_left instr_assign res instrs

557


558

let rec instr_constant_assign var instr =

559

match get_instr_desc instr with

560

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

561

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

562

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

563

 _ > false

564


565

and instrs_constant_assign var instrs =

566

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

567


568

let rec instr_reduce branches instr1 cont =

569

match get_instr_desc instr1 with

570

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

571

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

572

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

573

 _ > instr1 :: cont

574


575

and instrs_reduce branches instrs cont =

576

match instrs with

577

 [] > cont

578

 [i] > instr_reduce branches i cont

579

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

580


581

let rec instrs_fusion instrs =

582

match instrs, List.map get_instr_desc instrs with

583

 [], []

584

 [_], [_] >

585

instrs

586

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

587

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

588

 i1::i2::q, _ >

589

i1 :: instrs_fusion (i2::q)

590

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

591


592

let step_fusion step =

593

{ step with

594

step_instrs = instrs_fusion step.step_instrs;

595

}

596


597

let rec machine_fusion m =

598

{ m with

599

mstep = step_fusion m.mstep

600

}

601


602

let machines_fusion prog =

603

List.map machine_fusion prog

604


605


606

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

607


608

let elim_prog_variables prog removed_table =

609

List.map (

610

fun t >

611

match t.top_decl_desc with

612

Node nd >

613

if IMap.mem nd.node_id removed_table then

614

let nd_elim_map = IMap.find nd.node_id removed_table in

615

(* Iterating through the elim map to compute

616

 the list of variables to remove

617

 the associated list of lustre definitions x = expr to

618

be used when removing these variables *)

619

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

620

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

621

let locals =

622

try

623

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

624

with Not_found > accu_locals (* Variable v shall

625

be a global

626

constant, we do no

627

need to eliminate

628

it from the locals

629

*)

630

in

631

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

632

let defs = eq::accu_defs in

633

locals, defs

634

) nd_elim_map ([], [])

635

in

636


637

let new_locals, new_stmts =

638

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

639

match stmt with

640

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

641

 Eq eq > (

642

match eq.eq_lhs with

643

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

644

 _::_::_ >

645

(* When more than one lhs we just keep the

646

equation and do not delete it *)

647

let eq_rhs' = substitute_expr vars_to_replace defs eq.eq_rhs in

648

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

649

 [lhs] >

650

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

651

(* We remove the def *)

652

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

653

res_stmts

654

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

655

let eq_rhs' = substitute_expr vars_to_replace defs eq.eq_rhs in

656

locals,

657

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

658


659

)

660

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

661

in

662

let nd' = { nd with

663

node_locals = new_locals;

664

node_stmts = new_stmts;

665

}

666

in

667

{ t with top_decl_desc = Node nd' }

668

else

669

t

670

 _ > t

671

) prog

672


673

(*** Main function ***)

674


675

(*

676

This functions produces an optimzed prog * machines

677

It

678

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

679

2 inline constants and eliminate duplicated variables

680

3 try to reuse variables whenever possible

681


682

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

683


684

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

685


686


687

*)

688

let optimize params prog node_schs machine_code =

689

let machine_code =

690

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

691

begin

692

Log.report ~level:1

693

(fun fmt > Format.fprintf fmt ".. machines optimization: subexpression elimination@,");

694

let machine_code = machines_cse machine_code in

695

Log.report ~level:3 (fun fmt > Format.fprintf fmt ".. generated machines (subexpr elim):@ %a@ "pp_machines machine_code);

696

machine_code

697

end

698

else

699

machine_code

700

in

701

(* Optimize machine code *)

702

let prog, machine_code, removed_table =

703

if !Options.optimization >= 2

704

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

705

then

706

begin

707

Log.report ~level:1

708

(fun fmt >

709

Format.fprintf fmt

710

".. machines optimization: const. inlining (partial eval. with const)@,");

711

let machine_code, removed_table =

712

machines_unfold (Corelang.get_consts prog) node_schs machine_code in

713

Log.report ~level:3

714

(fun fmt >

715

Format.fprintf fmt "\t@[Eliminated flows: @[%a@]@]@ "

716

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

717

Log.report ~level:3

718

(fun fmt >

719

Format.fprintf fmt

720

".. generated machines (const inlining):@ %a@ "

721

pp_machines machine_code);

722

(* If variables were eliminated, relaunch the

723

normalization/machine generation *)

724

if IMap.is_empty removed_table then

725

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

726

prog, machine_code, removed_table

727

else (

728

let prog = elim_prog_variables prog removed_table in

729

(* Mini stage1 *)

730

let prog = Normalization.normalize_prog params prog in

731

let prog = SortProg.sort_nodes_locals prog in

732

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

733

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

734

let prog, node_schs = Scheduling.schedule_prog prog in

735

let machine_code = Machine_code.translate_prog prog node_schs in

736

(* Mini stage2 machine optimiation *)

737

let machine_code, removed_table =

738

machines_unfold (Corelang.get_consts prog) node_schs machine_code in

739

prog, machine_code, removed_table

740

)

741


742

end

743

else

744

prog, machine_code, IMap.empty

745

in

746

(* Optimize machine code *)

747

let machine_code =

748

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

749

begin

750

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

751

let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in

752

let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in

753

machines_fusion (machines_reuse_variables machine_code reuse_tables)

754

end

755

else

756

machine_code

757

in

758


759


760

prog, List.rev machine_code

761


762


763

(* Local Variables: *)

764

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

765

(* End: *)
