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 expr else (try IMap.find v.var_id elim with Not_found > expr)

52

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

53

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

54

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

55

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

56

 Cst _ > expr

57


58

let eliminate_dim elim dim =

59

Dimension.expr_replace_expr

60

(fun v > try

61

dimension_of_value (IMap.find v elim)

62

with Not_found > mkdim_ident dim.dim_loc v)

63

dim

64


65


66

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

67

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

68

*)

69


70

let unfold_expr_offset m offset expr =

71

List.fold_left

72

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

73

(Types.array_element_type res.value_type)

74

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

75

expr offset

76


77

let rec simplify_cst_expr m offset typ cst =

78

match offset, cst with

79

 [] , _

80

> mk_val (Cst cst) typ

81

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

82

> let elt_typ = Types.array_element_type typ in

83

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

84

 Index i :: q, Const_array cl

85

> let elt_typ = Types.array_element_type typ in

86

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

87

 Field f :: q, Const_struct fl

88

> let fld_typ = Types.struct_field_type typ f in

89

simplify_cst_expr m q fld_typ (List.assoc f fl)

90

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

91


92

let simplify_expr_offset m expr =

93

let rec simplify offset expr =

94

match offset, expr.value_desc with

95

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

96

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

97

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

98

 _ , Fun _

99

 _ , Var _ > unfold_expr_offset m offset expr

100

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

101

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

102

 [] , _ > expr

103

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

104

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

105

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

106

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

107

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

108

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

109

in simplify [] expr

110


111

let rec simplify_instr_offset m instr =

112

match get_instr_desc instr with

113

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

114

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

115

 MReset id > instr

116

 MNoReset id > instr

117

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

118

 MBranch (cond, brl)

119

> update_instr_desc instr (

120

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

121

)

122

 MSpec _  MComment _ > instr

123


124

and simplify_instrs_offset m instrs =

125

List.map (simplify_instr_offset m) instrs

126


127

let is_scalar_const c =

128

match c with

129

 Const_real _

130

 Const_int _

131

 Const_tag _ > true

132

 _ > false

133


134

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

135

 either expr is atomic

136

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

137

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

138

*)

139

let is_unfoldable_expr fanin expr =

140

let rec unfold_const offset cst =

141

match offset, cst with

142

 _ , Const_int _

143

 _ , Const_real _

144

 _ , Const_tag _ > true

145

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

146

 [] , Const_struct _ > false

147

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

148

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

149

 _ , Const_array _ > false

150

 _ > assert false in

151

let rec unfold offset expr =

152

match offset, expr.value_desc with

153

 _ , Cst cst > unfold_const offset cst

154

 _ , Var _ > true

155

 [] , Power _

156

 [] , Array _ > false

157

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

158

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

159

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

160

 _ , Array _ > false

161

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

162

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

163

> List.for_all (unfold offset) vl

164

 _ , Fun _ > false

165

 _ > assert false

166

in unfold [] expr

167


168

let basic_unfoldable_assign fanin v expr =

169

try

170

let d = Hashtbl.find fanin v.var_id

171

in is_unfoldable_expr d expr

172

with Not_found > false

173


174

let unfoldable_assign fanin v expr =

175

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

176

&& basic_unfoldable_assign fanin v expr

177


178

let merge_elim elim1 elim2 =

179

let merge k e1 e2 =

180

match e1, e2 with

181

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

182

 _ , Some e2 > Some e2

183

 Some e1, _ > Some e1

184

 _ > None

185

in IMap.merge merge elim1 elim2

186


187

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

188

if so, update elim and return the remove flag,

189

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

190

let rec instrs_unfold m fanin elim instrs =

191

let elim, rev_instrs =

192

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

193

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

194

rewritten *)

195

let instr = eliminate m elim instr in

196

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

197

is stored as the elim set *)

198

instr_unfold m fanin instrs elim instr

199

) (elim, []) instrs

200

in elim, List.rev rev_instrs

201


202

and instr_unfold m fanin instrs elim instr =

203

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

204

match get_instr_desc instr with

205

(* Simple cases*)

206

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

207

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

208

 MLocalAssign(v, expr) when unfoldable_assign fanin v expr

209

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

210

 MBranch(g, hl) when false

211

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

212

let (elim, branches) =

213

List.fold_right

214

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

215

elim_branches (elim, [])

216

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

217

 _

218

> (elim, instr :: instrs)

219

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

220


221


222

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

223

1. each expression is rewritten according to the accumulator

224

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

225

*)

226


227

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

228

let replace v =

229

try

230

dimension_of_value (IMap.find v elim)

231

with Not_found > Dimension.mkdim_ident Location.dummy_loc v

232

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

233


234

(** Perform optimization on machine code:

235

 iterate through step instructions and remove simple local assigns

236


237

*)

238

let machine_unfold fanin elim machine =

239

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

240

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

241

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

242

let instrs = simplify_instrs_offset machine instrs in

243

let checks = List.map (fun (loc, check) > loc, eliminate_expr machine elim_vars check) machine.mstep.step_checks in

244

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

245

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

246

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

247

in

248

{

249

machine with

250

mstep = {

251

machine.mstep with

252

step_locals = locals;

253

step_instrs = instrs;

254

step_checks = checks

255

};

256

mconst = mconst;

257

minstances = minstances;

258

mcalls = mcalls;

259

},

260

elim_vars

261


262

let instr_of_const top_const =

263

let const = const_of_top top_const in

264

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

265

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

266

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

267


268

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

269

is not explicit dependence btw variables and their use in

270

contracts. *)

271

let machines_unfold consts node_schs machines =

272

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

273

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

274

if is_contract then

275

m::machines, removed

276

else

277

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

278

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

279

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

280

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

281

)

282

machines

283

([], IMap.empty)

284


285

let get_assign_lhs instr =

286

match get_instr_desc instr with

287

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

288

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

289

 _ > assert false

290


291

let get_assign_rhs instr =

292

match get_instr_desc instr with

293

 MLocalAssign(_, e)

294

 MStateAssign(_, e) > e

295

 _ > assert false

296


297

let is_assign instr =

298

match get_instr_desc instr with

299

 MLocalAssign _

300

 MStateAssign _ > true

301

 _ > false

302


303

let mk_assign m v e =

304

match v.value_desc with

305

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

306

 _ > assert false

307


308

let rec assigns_instr instr assign =

309

match get_instr_desc instr with

310

 MLocalAssign (i,_)

311

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

312

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

313

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

314

 _ > assign

315


316

and assigns_instrs instrs assign =

317

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

318


319

(*

320

and substitute_expr subst expr =

321

match expr with

322

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

323

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

324

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

325

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

326

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

327

 Cst _ > expr

328

*)

329

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

330

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

331

Then substitute this expression with the first assigned var

332

*)

333

let subst_instr m subst instrs instr =

334

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

335

let instr = eliminate m subst instr in

336

let instr_v = get_assign_lhs instr in

337

let instr_e = get_assign_rhs instr in

338

try

339

(* Searching for equivalent asssign *)

340

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

341

get_assign_rhs instr' = instr_e) instrs in

342

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

343

match instr_v.value_desc with

344

 Var v >

345

if not (is_memory m v) then

346

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

347

memory, we can just record the relationship and continue

348

*)

349

IMap.add v.var_id (get_assign_lhs instr') subst, instrs

350

else (

351

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

352

the definition, simplified *)

353

let instr'_v = get_assign_lhs instr' in

354

(match instr'_v.value_desc with

355

 Var v' >

356

if not (is_memory m v') then

357

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

358

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

359

subst, instr :: instrs

360

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

361

definition is, itself, a memory *)

362


363

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

364

(* Filtering out the list of instructions:

365

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

366

 if the current instr is this instr' then apply

367

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

368

*)

369

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

370

let instrs' =

371

snd

372

(List.fold_right

373

(fun instr (ok, instrs) >

374

(ok  instr = instr',

375

if ok then

376

instr :: instrs

377

else

378

if instr = instr' then

379

instrs

380

else

381

eliminate m subst_v' instr :: instrs))

382

instrs (false, []))

383

in

384

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

385

)

386

 _ > assert false)

387

)

388

 _ > assert false

389


390

with Not_found >

391

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

392

subst, instr :: instrs

393


394

(** Common subexpression elimination for machine instructions *)

395

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

396

it is an equivalence table

397

 [elim] : set of eliminated variables

398

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

399

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

400

*)

401

let rec instr_cse m (subst, instrs) instr =

402

match get_instr_desc instr with

403

(* Simple cases*)

404

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

405

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

406

 MLocalAssign(v, expr) when is_unfoldable_expr 2 expr

407

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

408

 _ when is_assign instr

409

> subst_instr m subst instrs instr

410

 _ > (subst, instr :: instrs)

411


412

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

413

*)

414

let instrs_cse m subst instrs =

415

let subst, rev_instrs =

416

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

417

in subst, List.rev rev_instrs

418


419

(** Apply common subexpression elimination to a machine

420

 iterate through step instructions and remove simple local assigns

421

*)

422

let machine_cse subst machine =

423

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

424

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

425

let assigned = assigns_instrs instrs VSet.empty

426

in

427

{

428

machine with

429

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

430

mstep = {

431

machine.mstep with

432

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

433

step_instrs = instrs

434

}

435

}

436


437

let machines_cse machines =

438

List.map

439

(machine_cse IMap.empty)

440

machines

441


442

(* variable substitution for optimizing purposes *)

443


444

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

445

let rec instr_is_skip instr =

446

match get_instr_desc instr with

447

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

448

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

449

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

450

 _ > false

451

and instrs_are_skip instrs =

452

List.for_all instr_is_skip instrs

453


454

let instr_cons instr cont =

455

if instr_is_skip instr then cont else instr::cont

456


457

let rec instr_remove_skip instr cont =

458

match get_instr_desc instr with

459

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

460

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

461

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

462

 _ > instr::cont

463


464

and instrs_remove_skip instrs cont =

465

List.fold_right instr_remove_skip instrs cont

466


467

let rec value_replace_var fvar value =

468

match value.value_desc with

469

 Cst c > value

470

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

471

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

472

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

473

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

474

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

475


476

let rec instr_replace_var fvar instr cont =

477

match get_instr_desc instr with

478

 MSpec _  MComment _ > instr_cons instr cont

479

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

480

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

481

 MReset i > instr_cons instr cont

482

 MNoReset i > instr_cons instr cont

483

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

484

 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

485


486

and instrs_replace_var fvar instrs cont =

487

List.fold_right (instr_replace_var fvar) instrs cont

488


489

let step_replace_var fvar step =

490

(* Some outputs may have been replaced by locals.

491

We then need to rename those outputs

492

without changing their clocks, etc *)

493

let outputs' =

494

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

495

let locals' =

496

List.fold_left (fun res l >

497

let l' = fvar l in

498

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

499

then res

500

else Utils.add_cons l' res)

501

[] step.step_locals in

502

{ step with

503

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

504

step_outputs = outputs';

505

step_locals = locals';

506

step_instrs = instrs_replace_var fvar step.step_instrs [];

507

}

508


509

let rec machine_replace_variables fvar m =

510

{ m with

511

mstep = step_replace_var fvar m.mstep

512

}

513


514

let machine_reuse_variables m reuse =

515

let fvar v =

516

try

517

Hashtbl.find reuse v.var_id

518

with Not_found > v in

519

machine_replace_variables fvar m

520


521

let machines_reuse_variables prog reuse_tables =

522

List.map

523

(fun m >

524

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

525

) prog

526


527

let rec instr_assign res instr =

528

match get_instr_desc instr with

529

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

530

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

531

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

532

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

533

 _ > res

534


535

and instrs_assign res instrs =

536

List.fold_left instr_assign res instrs

537


538

let rec instr_constant_assign var instr =

539

match get_instr_desc instr with

540

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

541

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

542

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

543

 _ > false

544


545

and instrs_constant_assign var instrs =

546

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

547


548

let rec instr_reduce branches instr1 cont =

549

match get_instr_desc instr1 with

550

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

551

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

552

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

553

 _ > instr1 :: cont

554


555

and instrs_reduce branches instrs cont =

556

match instrs with

557

 [] > cont

558

 [i] > instr_reduce branches i cont

559

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

560


561

let rec instrs_fusion instrs =

562

match instrs, List.map get_instr_desc instrs with

563

 [], []

564

 [_], [_] >

565

instrs

566

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

567

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

568

 i1::i2::q, _ >

569

i1 :: instrs_fusion (i2::q)

570

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

571


572

let step_fusion step =

573

{ step with

574

step_instrs = instrs_fusion step.step_instrs;

575

}

576


577

let rec machine_fusion m =

578

{ m with

579

mstep = step_fusion m.mstep

580

}

581


582

let machines_fusion prog =

583

List.map machine_fusion prog

584


585


586

(*** Main function ***)

587


588

let optimize prog node_schs machine_code =

589

let machine_code =

590

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

591

begin

592

Log.report ~level:1

593

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

594

let machine_code = machines_cse machine_code in

595

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

596

machine_code

597

end

598

else

599

machine_code

600

in

601

(* Optimize machine code *)

602

let machine_code, removed_table =

603

if !Options.optimization >= 2

604

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

605

then

606

begin

607

Log.report ~level:1 (fun fmt > Format.fprintf fmt

608

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

609

let machine_code, removed_table = machines_unfold (Corelang.get_consts prog) node_schs machine_code in

610

Log.report ~level:3 (fun fmt > Format.fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ "

611

(pp_imap (pp_elim empty_machine)) removed_table);

612

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

613

machine_code, removed_table

614

end

615

else

616

machine_code, IMap.empty

617

in

618

(* Optimize machine code *)

619

let machine_code =

620

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

621

begin

622

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

623

let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in

624

let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in

625

machines_fusion (machines_reuse_variables machine_code reuse_tables)

626

end

627

else

628

machine_code

629

in

630


631


632

List.rev machine_code

633


634


635

(* Local Variables: *)

636

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

637

(* End: *)
