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 LustreSpec

14

open Corelang

15

open Causality

16

open Machine_code

17

open Dimension

18


19


20

let pp_elim fmt elim =

21

begin

22

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

23

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

24

Format.fprintf fmt "}@ @]";

25

end

26


27

let rec eliminate elim instr =

28

let e_expr = eliminate_expr elim in

29

match get_instr_desc instr with

30

 MComment _ > instr

31

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

32

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

33

 MReset i > instr

34

 MNoReset i > instr

35

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

36

 MBranch (g,hl) >

37

update_instr_desc instr (

38

MBranch

39

(e_expr g,

40

(List.map

41

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

42

hl

43

)

44

)

45

)

46


47

and eliminate_expr elim expr =

48

match expr.value_desc with

49

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

50

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

51

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

52

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

53

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

54

 Cst _  StateVar _ > expr

55


56

let eliminate_dim elim dim =

57

Dimension.expr_replace_expr

58

(fun v > try

59

dimension_of_value (IMap.find v elim)

60

with Not_found > mkdim_ident dim.dim_loc v)

61

dim

62


63


64

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

65

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

66

*)

67


68

let unfold_expr_offset m offset expr =

69

List.fold_left

70

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

71

(Types.array_element_type res.value_type)

72

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

73

expr offset

74


75

let rec simplify_cst_expr m offset typ cst =

76

match offset, cst with

77

 [] , _

78

> mk_val (Cst cst) typ

79

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

80

> let elt_typ = Types.array_element_type typ in

81

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

82

 Index i :: q, Const_array cl

83

> let elt_typ = Types.array_element_type typ in

84

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

85

 Field f :: q, Const_struct fl

86

> let fld_typ = Types.struct_field_type typ f in

87

simplify_cst_expr m q fld_typ (List.assoc f fl)

88

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

89


90

let simplify_expr_offset m expr =

91

let rec simplify offset expr =

92

match offset, expr.value_desc with

93

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

94

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

95

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

96

 _ , Fun _

97

 _ , StateVar _

98

 _ , LocalVar _ > unfold_expr_offset m offset expr

99

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

100

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

101

 [] , _ > expr

102

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

103

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

104

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

105

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

106

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

107

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

108

in simplify [] expr

109


110

let rec simplify_instr_offset m instr =

111

match get_instr_desc instr with

112

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

113

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

114

 MReset id > instr

115

 MNoReset id > instr

116

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

117

 MBranch (cond, brl)

118

> update_instr_desc instr (

119

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

120

)

121

 MComment _ > instr

122


123

and simplify_instrs_offset m instrs =

124

List.map (simplify_instr_offset m) instrs

125


126

let is_scalar_const c =

127

match c with

128

 Const_real _

129

 Const_int _

130

 Const_tag _ > true

131

 _ > false

132


133

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

134

 either expr is atomic

135

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

136

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

137

*)

138

let is_unfoldable_expr fanin expr =

139

let rec unfold_const offset cst =

140

match offset, cst with

141

 _ , Const_int _

142

 _ , Const_real _

143

 _ , Const_tag _ > true

144

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

145

 [] , Const_struct _ > false

146

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

147

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

148

 _ , Const_array _ > false

149

 _ > assert false in

150

let rec unfold offset expr =

151

match offset, expr.value_desc with

152

 _ , Cst cst > unfold_const offset cst

153

 _ , LocalVar _

154

 _ , StateVar _ > 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 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 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 fanin instrs elim instr

199

) (elim, []) instrs

200

in elim, List.rev rev_instrs

201


202

and instr_unfold 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 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 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

Machine_code.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 fanin elim machine.mconst in

241

let elim_vars, instrs = instrs_unfold 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 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) 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

let machines_unfold consts node_schs machines =

269

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

270

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

271

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

272

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

273

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

274

)

275

machines

276

([], IMap.empty)

277


278

let get_assign_lhs instr =

279

match get_instr_desc instr with

280

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

281

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

282

 _ > assert false

283


284

let get_assign_rhs instr =

285

match get_instr_desc instr with

286

 MLocalAssign(_, e)

287

 MStateAssign(_, e) > e

288

 _ > assert false

289


290

let is_assign instr =

291

match get_instr_desc instr with

292

 MLocalAssign _

293

 MStateAssign _ > true

294

 _ > false

295


296

let mk_assign v e =

297

match v.value_desc with

298

 LocalVar v > MLocalAssign(v, e)

299

 StateVar v > MStateAssign(v, e)

300

 _ > assert false

301


302

let rec assigns_instr instr assign =

303

match get_instr_desc instr with

304

 MLocalAssign (i,_)

305

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

306

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

307

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

308

 _ > assign

309


310

and assigns_instrs instrs assign =

311

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

312


313

(*

314

and substitute_expr subst expr =

315

match expr with

316

 StateVar v

317

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

318

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

319

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

320

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

321

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

322

 Cst _ > expr

323

*)

324

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

325

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

326

Then substitute this expression with the first assigned var

327

*)

328

let subst_instr subst instrs instr =

329

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

330

let instr = eliminate subst instr in

331

let v = get_assign_lhs instr in

332

let e = get_assign_rhs instr in

333

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

334


335

try

336

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

337

match v.value_desc with

338

 LocalVar v >

339

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

340

 StateVar v >

341

let lhs' = get_assign_lhs instr' in

342

let typ' = lhs'.value_type in

343

(match lhs'.value_desc with

344

 LocalVar v' >

345

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

346

subst, instr :: instrs

347

 StateVar v' >

348

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

349

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

350

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

351

 _ > assert false)

352

 _ > assert false

353

with Not_found > subst, instr :: instrs

354


355

*)

356


357

try

358

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

359

match v.value_desc with

360

 LocalVar v >

361

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

362

 StateVar stv >

363

let lhs = get_assign_lhs instr' in

364

(match lhs.value_desc with

365

 LocalVar v' >

366

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

367

subst, instr :: instrs

368

 StateVar stv' >

369

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

370

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

371

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

372

 _ > assert false)

373

 _ > assert false

374

with Not_found > subst, instr :: instrs

375


376

(** Common subexpression elimination for machine instructions *)

377

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

378

it is an equivalence table

379

 [elim] : set of eliminated variables

380

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

381

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

382

*)

383

let rec instr_cse (subst, instrs) instr =

384

match get_instr_desc instr with

385

(* Simple cases*)

386

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

387

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

388

 MLocalAssign(v, expr) when is_unfoldable_expr 2 expr

389

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

390

 _ when is_assign instr

391

> subst_instr subst instrs instr

392

 _ > (subst, instr :: instrs)

393


394

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

395

*)

396

let rec instrs_cse subst instrs =

397

let subst, rev_instrs =

398

List.fold_left instr_cse (subst, []) instrs

399

in subst, List.rev rev_instrs

400


401

(** Apply common subexpression elimination to a machine

402

 iterate through step instructions and remove simple local assigns

403

*)

404

let machine_cse subst machine =

405

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

406

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

407

let assigned = assigns_instrs instrs VSet.empty

408

in

409

{

410

machine with

411

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

412

mstep = {

413

machine.mstep with

414

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

415

step_instrs = instrs

416

}

417

}

418


419

let machines_cse machines =

420

List.map

421

(machine_cse IMap.empty)

422

machines

423


424

(* variable substitution for optimizing purposes *)

425


426

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

427

let rec instr_is_skip instr =

428

match get_instr_desc instr with

429

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

430

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

431

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

432

 _ > false

433

and instrs_are_skip instrs =

434

List.for_all instr_is_skip instrs

435


436

let instr_cons instr cont =

437

if instr_is_skip instr then cont else instr::cont

438


439

let rec instr_remove_skip instr cont =

440

match get_instr_desc instr with

441

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

442

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

443

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

444

 _ > instr::cont

445


446

and instrs_remove_skip instrs cont =

447

List.fold_right instr_remove_skip instrs cont

448


449

let rec value_replace_var fvar value =

450

match value.value_desc with

451

 Cst c > value

452

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

453

 StateVar v > value

454

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

455

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

456

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

457

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

458


459

let rec instr_replace_var fvar instr cont =

460

match get_instr_desc instr with

461

 MComment _ > instr_cons instr cont

462

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

463

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

464

 MReset i > instr_cons instr cont

465

 MNoReset i > instr_cons instr cont

466

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

467

 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

468


469

and instrs_replace_var fvar instrs cont =

470

List.fold_right (instr_replace_var fvar) instrs cont

471


472

let step_replace_var fvar step =

473

(* Some outputs may have been replaced by locals.

474

We then need to rename those outputs

475

without changing their clocks, etc *)

476

let outputs' =

477

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

478

let locals' =

479

List.fold_left (fun res l >

480

let l' = fvar l in

481

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

482

then res

483

else Utils.add_cons l' res)

484

[] step.step_locals in

485

{ step with

486

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

487

step_outputs = outputs';

488

step_locals = locals';

489

step_instrs = instrs_replace_var fvar step.step_instrs [];

490

}

491


492

let rec machine_replace_variables fvar m =

493

{ m with

494

mstep = step_replace_var fvar m.mstep

495

}

496


497

let machine_reuse_variables m reuse =

498

let fvar v =

499

try

500

Hashtbl.find reuse v.var_id

501

with Not_found > v in

502

machine_replace_variables fvar m

503


504

let machines_reuse_variables prog reuse_tables =

505

List.map

506

(fun m >

507

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

508

) prog

509


510

let rec instr_assign res instr =

511

match get_instr_desc instr with

512

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

513

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

514

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

515

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

516

 _ > res

517


518

and instrs_assign res instrs =

519

List.fold_left instr_assign res instrs

520


521

let rec instr_constant_assign var instr =

522

match get_instr_desc instr with

523

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

524

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

525

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

526

 _ > false

527


528

and instrs_constant_assign var instrs =

529

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

530


531

let rec instr_reduce branches instr1 cont =

532

match get_instr_desc instr1 with

533

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

534

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

535

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

536

 _ > instr1 :: cont

537


538

and instrs_reduce branches instrs cont =

539

match instrs with

540

 [] > cont

541

 [i] > instr_reduce branches i cont

542

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

543


544

let rec instrs_fusion instrs =

545

match instrs, List.map get_instr_desc instrs with

546

 [], []

547

 [_], [_] >

548

instrs

549

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

550

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

551

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

552

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

553

 i1::i2::q, _ >

554

i1 :: instrs_fusion (i2::q)

555

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

556


557

let step_fusion step =

558

{ step with

559

step_instrs = instrs_fusion step.step_instrs;

560

}

561


562

let rec machine_fusion m =

563

{ m with

564

mstep = step_fusion m.mstep

565

}

566


567

let machines_fusion prog =

568

List.map machine_fusion prog

569


570


571

(*** Main function ***)

572


573

let optimize prog node_schs machine_code =

574

let machine_code =

575

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

576

begin

577

Log.report ~level:1

578

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

579

let machine_code = machines_cse machine_code in

580

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

581

machine_code

582

end

583

else

584

machine_code

585

in

586

(* Optimize machine code *)

587

let machine_code, removed_table =

588

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

589

begin

590

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

591

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

592

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

593

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

594

(pp_imap pp_elim) removed_table);

595

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

596

machine_code, removed_table

597

end

598

else

599

machine_code, IMap.empty

600

in

601

(* Optimize machine code *)

602

let machine_code =

603

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

604

begin

605

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

606

let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in

607

let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in

608

machines_fusion (machines_reuse_variables machine_code reuse_tables)

609

end

610

else

611

machine_code

612

in

613


614

(* Salsa optimize machine code *)

615

(*

616

let machine_code =

617

if !Options.salsa_enabled then

618

begin

619

check_main ();

620

Log.report ~level:1 (fun fmt > fprintf fmt ".. salsa machines optimization: optimizing floatingpoint accuracy with Salsa@,");

621

(* Selecting float constants for Salsa *)

622

let constEnv = List.fold_left (

623

fun accu c_topdecl >

624

match c_topdecl.top_decl_desc with

625

 Const c when Types.is_real_type c.const_type >

626

(c.const_id, c.const_value) :: accu

627

 _ > accu

628

) [] (Corelang.get_consts prog)

629

in

630

List.map

631

(Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv)

632

machine_code

633

end

634

else

635

machine_code

636

in

637

Log.report ~level:3 (fun fmt > fprintf fmt "@[<v 2>@ %a@]@ "

638

(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)

639

machine_code);

640

*)

641


642


643

machine_code

644


645


646

(* Local Variables: *)

647

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

648

(* End: *)
