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 fmt elim =

22

begin

23

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

24

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

25

Format.fprintf fmt "}@ @]";

26

end

27


28

let rec eliminate elim instr =

29

let e_expr = eliminate_expr elim in

30

match get_instr_desc instr with

31

 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 elim) il)

43

hl

44

)

45

)

46

)

47


48

and eliminate_expr elim expr =

49

match expr.value_desc with

50

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

51

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

52

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

53

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

54

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

55

 Cst _  StateVar _ > expr

56


57

let eliminate_dim elim dim =

58

Dimension.expr_replace_expr

59

(fun v > try

60

dimension_of_value (IMap.find v elim)

61

with Not_found > mkdim_ident dim.dim_loc v)

62

dim

63


64


65

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

66

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

67

*)

68


69

let unfold_expr_offset m offset expr =

70

List.fold_left

71

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

72

(Types.array_element_type res.value_type)

73

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

74

expr offset

75


76

let rec simplify_cst_expr m offset typ cst =

77

match offset, cst with

78

 [] , _

79

> mk_val (Cst cst) typ

80

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

81

> let elt_typ = Types.array_element_type typ in

82

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

83

 Index i :: q, Const_array cl

84

> let elt_typ = Types.array_element_type typ in

85

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

86

 Field f :: q, Const_struct fl

87

> let fld_typ = Types.struct_field_type typ f in

88

simplify_cst_expr m q fld_typ (List.assoc f fl)

89

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

90


91

let simplify_expr_offset m expr =

92

let rec simplify offset expr =

93

match offset, expr.value_desc with

94

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

95

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

96

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

97

 _ , Fun _

98

 _ , StateVar _

99

 _ , LocalVar _ > 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

 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

 _ , LocalVar _

155

 _ , StateVar _ > true

156

 [] , Power _

157

 [] , Array _ > false

158

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

159

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

160

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

161

 _ , Array _ > false

162

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

163

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

164

> List.for_all (unfold offset) vl

165

 _ , Fun _ > false

166

 _ > assert false

167

in unfold [] expr

168


169

let basic_unfoldable_assign fanin v expr =

170

try

171

let d = Hashtbl.find fanin v.var_id

172

in is_unfoldable_expr d expr

173

with Not_found > false

174


175

let unfoldable_assign fanin v expr =

176

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

177

&& basic_unfoldable_assign fanin v expr

178


179

let merge_elim elim1 elim2 =

180

let merge k e1 e2 =

181

match e1, e2 with

182

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

183

 _ , Some e2 > Some e2

184

 Some e1, _ > Some e1

185

 _ > None

186

in IMap.merge merge elim1 elim2

187


188

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

189

if so, update elim and return the remove flag,

190

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

191

let rec instrs_unfold fanin elim instrs =

192

let elim, rev_instrs =

193

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

194

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

195

rewritten *)

196

let instr = eliminate elim instr in

197

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

198

is stored as the elim set *)

199

instr_unfold fanin instrs elim instr

200

) (elim, []) instrs

201

in elim, List.rev rev_instrs

202


203

and instr_unfold fanin instrs elim instr =

204

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

205

match get_instr_desc instr with

206

(* Simple cases*)

207

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

208

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

209

 MLocalAssign(v, expr) when unfoldable_assign fanin v expr

210

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

211

 MBranch(g, hl) when false

212

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

213

let (elim, branches) =

214

List.fold_right

215

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

216

elim_branches (elim, [])

217

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

218

 _

219

> (elim, instr :: instrs)

220

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

221


222


223

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

224

1. each expression is rewritten according to the accumulator

225

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

226

*)

227


228

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

229

let replace v =

230

try

231

dimension_of_value (IMap.find v elim)

232

with Not_found > Dimension.mkdim_ident Location.dummy_loc v

233

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

234


235

(** Perform optimization on machine code:

236

 iterate through step instructions and remove simple local assigns

237


238

*)

239

let machine_unfold fanin elim machine =

240

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

241

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

242

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

243

let instrs = simplify_instrs_offset machine instrs in

244

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

245

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

246

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

247

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

248

in

249

{

250

machine with

251

mstep = {

252

machine.mstep with

253

step_locals = locals;

254

step_instrs = instrs;

255

step_checks = checks

256

};

257

mconst = mconst;

258

minstances = minstances;

259

mcalls = mcalls;

260

},

261

elim_vars

262


263

let instr_of_const top_const =

264

let const = const_of_top top_const in

265

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

266

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

267

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

268


269

let machines_unfold consts node_schs machines =

270

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

271

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

272

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

273

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

274

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

275

)

276

machines

277

([], IMap.empty)

278


279

let get_assign_lhs instr =

280

match get_instr_desc instr with

281

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

282

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

283

 _ > assert false

284


285

let get_assign_rhs instr =

286

match get_instr_desc instr with

287

 MLocalAssign(_, e)

288

 MStateAssign(_, e) > e

289

 _ > assert false

290


291

let is_assign instr =

292

match get_instr_desc instr with

293

 MLocalAssign _

294

 MStateAssign _ > true

295

 _ > false

296


297

let mk_assign v e =

298

match v.value_desc with

299

 LocalVar v > MLocalAssign(v, e)

300

 StateVar v > MStateAssign(v, e)

301

 _ > assert false

302


303

let rec assigns_instr instr assign =

304

match get_instr_desc instr with

305

 MLocalAssign (i,_)

306

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

307

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

308

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

309

 _ > assign

310


311

and assigns_instrs instrs assign =

312

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

313


314

(*

315

and substitute_expr subst expr =

316

match expr with

317

 StateVar v

318

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

319

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

320

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

321

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

322

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

323

 Cst _ > expr

324

*)

325

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

326

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

327

Then substitute this expression with the first assigned var

328

*)

329

let subst_instr subst instrs instr =

330

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

331

let instr = eliminate subst instr in

332

let v = get_assign_lhs instr in

333

let e = get_assign_rhs instr in

334

(* Difficulties to merge with unstable. Here is the other code:

335


336

try

337

let instr' = List.find (fun instr' > is_assign instr' && get_assign_rhs instr' = e) instrs in

338

match v.value_desc with

339

 LocalVar v >

340

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

341

 StateVar v >

342

let lhs' = get_assign_lhs instr' in

343

let typ' = lhs'.value_type in

344

(match lhs'.value_desc with

345

 LocalVar v' >

346

let instr = eliminate subst (mk_assign (mk_val (StateVar v) typ') (mk_val (LocalVar v') typ')) in

347

subst, instr :: instrs

348

 StateVar v' >

349

let subst_v' = IMap.add v'.var_id (mk_val (StateVar v) typ') IMap.empty in

350

let instrs' = snd (List.fold_right (fun instr (ok, instrs) > (ok  instr = instr', if ok then instr :: instrs else if instr = instr' then instrs else eliminate subst_v' instr :: instrs)) instrs (false, [])) in

351

IMap.add v'.var_id (mk_val (StateVar v) typ') subst, instr :: instrs'

352

 _ > assert false)

353

 _ > assert false

354

with Not_found > subst, instr :: instrs

355


356

*)

357


358

try

359

let instr' = List.find (fun instr' > is_assign instr' && get_assign_rhs instr' = e) instrs in

360

match v.value_desc with

361

 LocalVar v >

362

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

363

 StateVar stv >

364

let lhs = get_assign_lhs instr' in

365

(match lhs.value_desc with

366

 LocalVar v' >

367

let instr = eliminate subst (update_instr_desc instr (mk_assign v lhs)) in

368

subst, instr :: instrs

369

 StateVar stv' >

370

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

371

let instrs' = snd (List.fold_right (fun instr (ok, instrs) > (ok  instr = instr', if ok then instr :: instrs else if instr = instr' then instrs else eliminate subst_v' instr :: instrs)) instrs (false, [])) in

372

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

373

 _ > assert false)

374

 _ > assert false

375

with Not_found > subst, instr :: instrs

376


377

(** Common subexpression elimination for machine instructions *)

378

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

379

it is an equivalence table

380

 [elim] : set of eliminated variables

381

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

382

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

383

*)

384

let rec instr_cse (subst, instrs) instr =

385

match get_instr_desc instr with

386

(* Simple cases*)

387

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

388

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

389

 MLocalAssign(v, expr) when is_unfoldable_expr 2 expr

390

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

391

 _ when is_assign instr

392

> subst_instr subst instrs instr

393

 _ > (subst, instr :: instrs)

394


395

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

396

*)

397

let rec instrs_cse subst instrs =

398

let subst, rev_instrs =

399

List.fold_left instr_cse (subst, []) instrs

400

in subst, List.rev rev_instrs

401


402

(** Apply common subexpression elimination to a machine

403

 iterate through step instructions and remove simple local assigns

404

*)

405

let machine_cse subst machine =

406

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

407

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

408

let assigned = assigns_instrs instrs VSet.empty

409

in

410

{

411

machine with

412

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

413

mstep = {

414

machine.mstep with

415

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

416

step_instrs = instrs

417

}

418

}

419


420

let machines_cse machines =

421

List.map

422

(machine_cse IMap.empty)

423

machines

424


425

(* variable substitution for optimizing purposes *)

426


427

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

428

let rec instr_is_skip instr =

429

match get_instr_desc instr with

430

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

431

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

432

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

433

 _ > false

434

and instrs_are_skip instrs =

435

List.for_all instr_is_skip instrs

436


437

let instr_cons instr cont =

438

if instr_is_skip instr then cont else instr::cont

439


440

let rec instr_remove_skip instr cont =

441

match get_instr_desc instr with

442

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

443

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

444

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

445

 _ > instr::cont

446


447

and instrs_remove_skip instrs cont =

448

List.fold_right instr_remove_skip instrs cont

449


450

let rec value_replace_var fvar value =

451

match value.value_desc with

452

 Cst c > value

453

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

454

 StateVar v > value

455

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

456

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

457

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

458

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

459


460

let rec instr_replace_var fvar instr cont =

461

match get_instr_desc instr with

462

 MComment _ > instr_cons instr cont

463

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

464

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

465

 MReset i > instr_cons instr cont

466

 MNoReset i > instr_cons instr cont

467

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

468

 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

469


470

and instrs_replace_var fvar instrs cont =

471

List.fold_right (instr_replace_var fvar) instrs cont

472


473

let step_replace_var fvar step =

474

(* Some outputs may have been replaced by locals.

475

We then need to rename those outputs

476

without changing their clocks, etc *)

477

let outputs' =

478

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

479

let locals' =

480

List.fold_left (fun res l >

481

let l' = fvar l in

482

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

483

then res

484

else Utils.add_cons l' res)

485

[] step.step_locals in

486

{ step with

487

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

488

step_outputs = outputs';

489

step_locals = locals';

490

step_instrs = instrs_replace_var fvar step.step_instrs [];

491

}

492


493

let rec machine_replace_variables fvar m =

494

{ m with

495

mstep = step_replace_var fvar m.mstep

496

}

497


498

let machine_reuse_variables m reuse =

499

let fvar v =

500

try

501

Hashtbl.find reuse v.var_id

502

with Not_found > v in

503

machine_replace_variables fvar m

504


505

let machines_reuse_variables prog reuse_tables =

506

List.map

507

(fun m >

508

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

509

) prog

510


511

let rec instr_assign res instr =

512

match get_instr_desc instr with

513

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

514

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

515

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

516

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

517

 _ > res

518


519

and instrs_assign res instrs =

520

List.fold_left instr_assign res instrs

521


522

let rec instr_constant_assign var instr =

523

match get_instr_desc instr with

524

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

525

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

526

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

527

 _ > false

528


529

and instrs_constant_assign var instrs =

530

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

531


532

let rec instr_reduce branches instr1 cont =

533

match get_instr_desc instr1 with

534

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

535

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

536

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

537

 _ > instr1 :: cont

538


539

and instrs_reduce branches instrs cont =

540

match instrs with

541

 [] > cont

542

 [i] > instr_reduce branches i cont

543

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

544


545

let rec instrs_fusion instrs =

546

match instrs, List.map get_instr_desc instrs with

547

 [], []

548

 [_], [_] >

549

instrs

550

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

551

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

552

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

553

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

554

 i1::i2::q, _ >

555

i1 :: instrs_fusion (i2::q)

556

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

557


558

let step_fusion step =

559

{ step with

560

step_instrs = instrs_fusion step.step_instrs;

561

}

562


563

let rec machine_fusion m =

564

{ m with

565

mstep = step_fusion m.mstep

566

}

567


568

let machines_fusion prog =

569

List.map machine_fusion prog

570


571


572

(*** Main function ***)

573


574

let optimize prog node_schs machine_code =

575

let machine_code =

576

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

577

begin

578

Log.report ~level:1

579

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

580

let machine_code = machines_cse machine_code in

581

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

582

machine_code

583

end

584

else

585

machine_code

586

in

587

(* Optimize machine code *)

588

let machine_code, removed_table =

589

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

590

begin

591

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

592

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

593

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

594

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

595

(pp_imap pp_elim) removed_table);

596

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

597

machine_code, removed_table

598

end

599

else

600

machine_code, IMap.empty

601

in

602

(* Optimize machine code *)

603

let machine_code =

604

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

605

begin

606

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

607

let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in

608

let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in

609

machines_fusion (machines_reuse_variables machine_code reuse_tables)

610

end

611

else

612

machine_code

613

in

614


615


616

machine_code

617


618


619

(* Local Variables: *)

620

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

621

(* End: *)
