## lustrec / src / optimize_machine.ml @ e8250987

History | View | Annotate | Download (26 KB)

1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|

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 | d0b1ec56 | xthirioux | open Utils |

13 | 8446bf03 | ploc | open Lustre_types |

14 | open Machine_code_types |
||

15 | cf78a589 | ploc | open Corelang |

16 | b1655a21 | xthirioux | open Causality |

17 | 2863281f | ploc | open Machine_code_common |

18 | ec433d69 | xthirioux | open Dimension |

19 | cf78a589 | ploc | |

20 | 55537f48 | xthirioux | |

21 | c35de73b | ploc | let pp_elim m fmt elim = |

22 | d0b1ec56 | xthirioux | begin |

23 | 521e2a6b | ploc | Format.fprintf fmt "@[{ /* elim table: */@ "; |

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

25 | 521e2a6b | ploc | Format.fprintf fmt "}@ @]"; |

26 | d0b1ec56 | xthirioux | end |

27 | |||

28 | c35de73b | ploc | let rec eliminate m elim instr = |

29 | let e_expr = eliminate_expr m elim in |
||

30 | 3ca27bc7 | ploc | match get_instr_desc instr with |

31 | 04a63d25 | xthirioux | | MComment _ -> instr |

32 | 3ca27bc7 | ploc | | 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 | cf78a589 | ploc | | MReset i -> instr |

35 | 45f0f48d | xthirioux | | MNoReset i -> instr |

36 | 3ca27bc7 | ploc | | MStep (il, i, vl) -> update_instr_desc instr (MStep(il, i, List.map e_expr vl)) |

37 | cf78a589 | ploc | | MBranch (g,hl) -> |

38 | 3ca27bc7 | ploc | update_instr_desc instr ( |

39 | MBranch |
||

40 | (e_expr g, |
||

41 | (List.map |
||

42 | c35de73b | ploc | (fun (l, il) -> l, List.map (eliminate m elim) il) |

43 | 3ca27bc7 | ploc | hl |

44 | ) |
||

45 | ) |
||

46 | ) |
||

47 | cf78a589 | ploc | |

48 | c35de73b | ploc | and eliminate_expr m elim expr = |

49 | let eliminate_expr = eliminate_expr m in |
||

50 | 04a63d25 | xthirioux | match expr.value_desc with |

51 | c35de73b | ploc | | Var v -> if is_memory m v then expr else (try IMap.find v.var_id elim with Not_found -> expr) |

52 | 04a63d25 | xthirioux | | 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 | c35de73b | ploc | | Cst _ -> expr |

57 | cf78a589 | ploc | |

58 | ec433d69 | xthirioux | let eliminate_dim elim dim = |

59 | 45f0f48d | xthirioux | 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 | ec433d69 | xthirioux | |

65 | ca88e660 | Ploc | |

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 | d2d9d4cb | ploc | *) |

69 | ca88e660 | Ploc | |

70 | d7b73fed | xthirioux | let unfold_expr_offset m offset expr = |

71 | 04a63d25 | xthirioux | 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 | d7b73fed | xthirioux | |

77 | 04a63d25 | xthirioux | let rec simplify_cst_expr m offset typ cst = |

78 | d7b73fed | xthirioux | match offset, cst with |

79 | | [] , _ |
||

80 | 04a63d25 | xthirioux | -> mk_val (Cst cst) typ |

81 | d7b73fed | xthirioux | | Index i :: q, Const_array cl when Dimension.is_dimension_const i |

82 | 04a63d25 | xthirioux | -> 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 | d7b73fed | xthirioux | | Index i :: q, Const_array cl |

85 | 04a63d25 | xthirioux | -> 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 | d7b73fed | xthirioux | | Field f :: q, Const_struct fl |

88 | 04a63d25 | xthirioux | -> let fld_typ = Types.struct_field_type typ f in |

89 | simplify_cst_expr m q fld_typ (List.assoc f fl) |
||

90 | d7b73fed | xthirioux | | _ -> (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 | 04a63d25 | xthirioux | match offset, expr.value_desc with |

95 | d7b73fed | xthirioux | | Field f ::q , _ -> failwith "not yet implemented" |

96 | 04a63d25 | xthirioux | | _ , 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 | d7b73fed | xthirioux | | _ , Fun _ |

99 | c35de73b | ploc | | _ , Var _ -> unfold_expr_offset m offset expr |

100 | 04a63d25 | xthirioux | | _ , Cst cst -> simplify_cst_expr m offset expr.value_type cst |

101 | d7b73fed | xthirioux | | _ , 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 | 04a63d25 | xthirioux | | Index i :: q, Array vl -> unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify q) vl)) expr.value_type) |

107 | d7b73fed | xthirioux | (*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 | 3ca27bc7 | ploc | 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 | d7b73fed | xthirioux | | MReset id -> instr |

116 | 45f0f48d | xthirioux | | MNoReset id -> instr |

117 | 3ca27bc7 | ploc | | MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs)) |

118 | d7b73fed | xthirioux | | MBranch (cond, brl) |

119 | 3ca27bc7 | ploc | -> 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 | 04a63d25 | xthirioux | | MComment _ -> instr |

123 | d7b73fed | xthirioux | |

124 | and simplify_instrs_offset m instrs = |
||

125 | List.map (simplify_instr_offset m) instrs |
||

126 | |||

127 | d0b1ec56 | xthirioux | let is_scalar_const c = |

128 | match c with |
||

129 | | Const_real _ |
||

130 | 04a63d25 | xthirioux | | Const_int _ |

131 | d0b1ec56 | xthirioux | | Const_tag _ -> true |

132 | | _ -> false |
||

133 | |||

134 | d7b73fed | xthirioux | (* 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 | 04a63d25 | xthirioux | match offset, expr.value_desc with |

153 | d7b73fed | xthirioux | | _ , Cst cst -> unfold_const offset cst |

154 | c35de73b | ploc | | _ , Var _ -> true |

155 | d7b73fed | xthirioux | | [] , 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 | 04a63d25 | xthirioux | | _ , Fun (id, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr |

163 | d7b73fed | xthirioux | -> List.for_all (unfold offset) vl |

164 | | _ , Fun _ -> false |
||

165 | | _ -> assert false |
||

166 | in unfold [] expr |
||

167 | c287ba28 | xthirioux | |

168 | 04a63d25 | xthirioux | let basic_unfoldable_assign fanin v expr = |

169 | d0b1ec56 | xthirioux | try |

170 | let d = Hashtbl.find fanin v.var_id |
||

171 | d7b73fed | xthirioux | in is_unfoldable_expr d expr |

172 | with Not_found -> false |
||

173 | 04a63d25 | xthirioux | |

174 | d7b73fed | xthirioux | let unfoldable_assign fanin v expr = |

175 | 04a63d25 | xthirioux | (if !Options.mpfr then Mpfr.unfoldable_value expr else true) |

176 | && basic_unfoldable_assign fanin v expr |
||

177 | |||

178 | d0b1ec56 | xthirioux | 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 | cf78a589 | ploc | (* see if elim has to take in account the provided instr: |

188 | 54d032f5 | xthirioux | if so, update elim and return the remove flag, |

189 | cf78a589 | ploc | otherwise, the expression should be kept and elim is left untouched *) |

190 | c35de73b | ploc | let rec instrs_unfold m fanin elim instrs = |

191 | d0b1ec56 | xthirioux | 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 | c35de73b | ploc | let instr = eliminate m elim instr in |

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

197 | is stored as the elim set *) |
||

198 | c35de73b | ploc | instr_unfold m fanin instrs elim instr |

199 | d0b1ec56 | xthirioux | ) (elim, []) instrs |

200 | in elim, List.rev rev_instrs |
||

201 | |||

202 | c35de73b | ploc | and instr_unfold m fanin instrs elim instr = |

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

204 | 3ca27bc7 | ploc | match get_instr_desc instr with |

205 | cf78a589 | ploc | (* Simple cases*) |

206 | 04a63d25 | xthirioux | | MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type) |

207 | c35de73b | ploc | -> instr_unfold m fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))) |

208 | d0b1ec56 | xthirioux | | 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 | c35de73b | ploc | -> let elim_branches = List.map (fun (h, l) -> (h, instrs_unfold m fanin elim l)) hl in |

212 | d0b1ec56 | xthirioux | 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 | 3ca27bc7 | ploc | in elim, ((update_instr_desc instr (MBranch (g, branches))) :: instrs) |

217 | d0b1ec56 | xthirioux | | _ |

218 | -> (elim, instr :: instrs) |
||

219 | cf78a589 | ploc | (* 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 | ec433d69 | xthirioux | let static_call_unfold elim (inst, (n, args)) = |

228 | let replace v = |
||

229 | try |
||

230 | 2863281f | ploc | dimension_of_value (IMap.find v elim) |

231 | ec433d69 | xthirioux | with Not_found -> Dimension.mkdim_ident Location.dummy_loc v |

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

233 | |||

234 | cf78a589 | ploc | (** Perform optimization on machine code: |

235 | - iterate through step instructions and remove simple local assigns |
||

236 | |||

237 | *) |
||

238 | d0b1ec56 | xthirioux | let machine_unfold fanin elim machine = |

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

240 | c35de73b | ploc | 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 | d7b73fed | xthirioux | let instrs = simplify_instrs_offset machine instrs in |

243 | c35de73b | ploc | let checks = List.map (fun (loc, check) -> loc, eliminate_expr machine elim_vars check) machine.mstep.step_checks in |

244 | ec433d69 | xthirioux | 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 | cf78a589 | ploc | in |

248 | { |
||

249 | machine with |
||

250 | mstep = { |
||

251 | machine.mstep with |
||

252 | ec433d69 | xthirioux | step_locals = locals; |

253 | d7b73fed | xthirioux | step_instrs = instrs; |

254 | step_checks = checks |
||

255 | ec433d69 | xthirioux | }; |

256 | mconst = mconst; |
||

257 | minstances = minstances; |
||

258 | mcalls = mcalls; |
||

259 | 04a63d25 | xthirioux | }, |

260 | elim_vars |
||

261 | cf78a589 | ploc | |

262 | d0b1ec56 | xthirioux | let instr_of_const top_const = |

263 | let const = const_of_top top_const in |
||

264 | 66359a5e | ploc | 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 | d0b1ec56 | xthirioux | let vdecl = { vdecl with var_type = const.const_type } |

266 | 3ca27bc7 | ploc | in mkinstr (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type)) |

267 | cf78a589 | ploc | |

268 | d0b1ec56 | xthirioux | let machines_unfold consts node_schs machines = |

269 | 04a63d25 | xthirioux | List.fold_right (fun m (machines, removed) -> |

270 | 95fb046e | ploc | let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in |

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

272 | 04a63d25 | xthirioux | 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 | d0b1ec56 | xthirioux | machines |

276 | 04a63d25 | xthirioux | ([], IMap.empty) |

277 | cf78a589 | ploc | |

278 | c287ba28 | xthirioux | let get_assign_lhs instr = |

279 | 3ca27bc7 | ploc | match get_instr_desc instr with |

280 | c35de73b | ploc | | MLocalAssign(v, e) -> mk_val (Var v) e.value_type |

281 | | MStateAssign(v, e) -> mk_val (Var v) e.value_type |
||

282 | c287ba28 | xthirioux | | _ -> assert false |

283 | |||

284 | let get_assign_rhs instr = |
||

285 | 3ca27bc7 | ploc | match get_instr_desc instr with |

286 | c287ba28 | xthirioux | | MLocalAssign(_, e) |

287 | | MStateAssign(_, e) -> e |
||

288 | | _ -> assert false |
||

289 | |||

290 | let is_assign instr = |
||

291 | 3ca27bc7 | ploc | match get_instr_desc instr with |

292 | c287ba28 | xthirioux | | MLocalAssign _ |

293 | | MStateAssign _ -> true |
||

294 | | _ -> false |
||

295 | |||

296 | c35de73b | ploc | let mk_assign m v e = |

297 | 04a63d25 | xthirioux | match v.value_desc with |

298 | c35de73b | ploc | | Var v -> if is_memory m v then MStateAssign(v, e) else MLocalAssign(v, e) |

299 | c287ba28 | xthirioux | | _ -> assert false |

300 | |||

301 | let rec assigns_instr instr assign = |
||

302 | 3ca27bc7 | ploc | match get_instr_desc instr with |

303 | c287ba28 | xthirioux | | MLocalAssign (i,_) |

304 | 017eec6a | ploc | | MStateAssign (i,_) -> VSet.add i assign |

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

306 | c287ba28 | xthirioux | | MBranch (_,hl) -> List.fold_right (fun (_, il) -> assigns_instrs il) hl assign |

307 | | _ -> assign |
||

308 | |||

309 | and assigns_instrs instrs assign = |
||

310 | List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs |
||

311 | |||

312 | (* |
||

313 | and substitute_expr subst expr = |
||

314 | match expr with |
||

315 | c35de73b | ploc | | Var v -> (try IMap.find expr subst with Not_found -> expr) |

316 | c287ba28 | xthirioux | | Fun (id, vl) -> Fun (id, List.map (substitute_expr subst) vl) |

317 | | Array(vl) -> Array(List.map (substitute_expr subst) vl) |
||

318 | | Access(v1, v2) -> Access(substitute_expr subst v1, substitute_expr subst v2) |
||

319 | | Power(v1, v2) -> Power(substitute_expr subst v1, substitute_expr subst v2) |
||

320 | | Cst _ -> expr |
||

321 | *) |
||

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

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

324 | Then substitute this expression with the first assigned var |
||

325 | *) |
||

326 | c35de73b | ploc | let subst_instr m subst instrs instr = |

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

328 | c35de73b | ploc | let instr = eliminate m subst instr in |

329 | let instr_v = get_assign_lhs instr in |
||

330 | let instr_e = get_assign_rhs instr in |
||

331 | try |
||

332 | (* Searching for equivalent asssign *) |
||

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

334 | get_assign_rhs instr' = instr_e) instrs in |
||

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

336 | match instr_v.value_desc with |
||

337 | | Var v -> |
||

338 | if not (is_memory m v) then |
||

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

340 | memory, we can just record the relationship and continue |
||

341 | *) |
||

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

343 | else ( |
||

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

345 | the definition, simplified *) |
||

346 | let instr'_v = get_assign_lhs instr' in |
||

347 | (match instr'_v.value_desc with |
||

348 | | Var v' -> |
||

349 | if not (is_memory m v') then |
||

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

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

352 | subst, instr :: instrs |
||

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

354 | definition is, itself, a memory *) |
||

355 | |||

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

357 | (* Filtering out the list of instructions: |
||

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

359 | - if the current instr is this instr' then apply |
||

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

361 | *) |
||

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

363 | let instrs' = |
||

364 | snd |
||

365 | (List.fold_right |
||

366 | (fun instr (ok, instrs) -> |
||

367 | (ok || instr = instr', |
||

368 | if ok then |
||

369 | instr :: instrs |
||

370 | else |
||

371 | if instr = instr' then |
||

372 | instrs |
||

373 | else |
||

374 | eliminate m subst_v' instr :: instrs)) |
||

375 | instrs (false, [])) |
||

376 | in |
||

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

378 | ) |
||

379 | | _ -> assert false) |
||

380 | ) |
||

381 | c287ba28 | xthirioux | | _ -> assert false |

382 | c35de73b | ploc | |

383 | with Not_found -> |
||

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

385 | subst, instr :: instrs |
||

386 | |||

387 | c287ba28 | xthirioux | (** Common sub-expression elimination for machine instructions *) |

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

389 | it is an equivalence table |
||

390 | - [elim] : set of eliminated variables |
||

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

392 | - [instr] : current instruction, normalized by [subst] |
||

393 | *) |
||

394 | c35de73b | ploc | let rec instr_cse m (subst, instrs) instr = |

395 | 3ca27bc7 | ploc | match get_instr_desc instr with |

396 | c287ba28 | xthirioux | (* Simple cases*) |

397 | 04a63d25 | xthirioux | | MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl) |

398 | c35de73b | ploc | -> instr_cse m (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))) |

399 | d7b73fed | xthirioux | | MLocalAssign(v, expr) when is_unfoldable_expr 2 expr |

400 | c287ba28 | xthirioux | -> (IMap.add v.var_id expr subst, instr :: instrs) |

401 | | _ when is_assign instr |
||

402 | c35de73b | ploc | -> subst_instr m subst instrs instr |

403 | c287ba28 | xthirioux | | _ -> (subst, instr :: instrs) |

404 | |||

405 | (** Apply common sub-expression elimination to a sequence of instrs |
||

406 | *) |
||

407 | c35de73b | ploc | let instrs_cse m subst instrs = |

408 | c287ba28 | xthirioux | let subst, rev_instrs = |

409 | c35de73b | ploc | List.fold_left (instr_cse m) (subst, []) instrs |

410 | c287ba28 | xthirioux | in subst, List.rev rev_instrs |

411 | |||

412 | (** Apply common sub-expression elimination to a machine |
||

413 | - iterate through step instructions and remove simple local assigns |
||

414 | *) |
||

415 | let machine_cse subst machine = |
||

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

417 | c35de73b | ploc | let subst, instrs = instrs_cse machine subst machine.mstep.step_instrs in |

418 | 017eec6a | ploc | let assigned = assigns_instrs instrs VSet.empty |

419 | c287ba28 | xthirioux | in |

420 | { |
||

421 | machine with |
||

422 | 017eec6a | ploc | mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory; |

423 | c287ba28 | xthirioux | mstep = { |

424 | machine.mstep with |
||

425 | 017eec6a | ploc | step_locals = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mstep.step_locals; |

426 | c287ba28 | xthirioux | step_instrs = instrs |

427 | } |
||

428 | } |
||

429 | |||

430 | let machines_cse machines = |
||

431 | List.map |
||

432 | (machine_cse IMap.empty) |
||

433 | machines |
||

434 | |||

435 | 45c13277 | xthirioux | (* variable substitution for optimizing purposes *) |

436 | |||

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

438 | let rec instr_is_skip instr = |
||

439 | 3ca27bc7 | ploc | match get_instr_desc instr with |

440 | c35de73b | ploc | | MLocalAssign (i, { value_desc = (Var v) ; _}) when i = v -> true |

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

442 | 45c13277 | xthirioux | | MBranch (g, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl |

443 | | _ -> false |
||

444 | and instrs_are_skip instrs = |
||

445 | List.for_all instr_is_skip instrs |
||

446 | |||

447 | let instr_cons instr cont = |
||

448 | if instr_is_skip instr then cont else instr::cont |
||

449 | |||

450 | let rec instr_remove_skip instr cont = |
||

451 | 3ca27bc7 | ploc | match get_instr_desc instr with |

452 | c35de73b | ploc | | MLocalAssign (i, { value_desc = Var v; _ }) when i = v -> cont |

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

454 | 3ca27bc7 | ploc | | MBranch (g, hl) -> update_instr_desc instr (MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl)) :: cont |

455 | 45c13277 | xthirioux | | _ -> instr::cont |

456 | |||

457 | and instrs_remove_skip instrs cont = |
||

458 | List.fold_right instr_remove_skip instrs cont |
||

459 | |||

460 | let rec value_replace_var fvar value = |
||

461 | 04a63d25 | xthirioux | match value.value_desc with |

462 | 45c13277 | xthirioux | | Cst c -> value |

463 | c35de73b | ploc | | Var v -> { value with value_desc = Var (fvar v) } |

464 | 04a63d25 | xthirioux | | Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) } |

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

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

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

468 | 45c13277 | xthirioux | |

469 | let rec instr_replace_var fvar instr cont = |
||

470 | 3ca27bc7 | ploc | match get_instr_desc instr with |

471 | 04a63d25 | xthirioux | | MComment _ -> instr_cons instr cont |

472 | 3ca27bc7 | ploc | | MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont |

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

474 | 45c13277 | xthirioux | | MReset i -> instr_cons instr cont |

475 | eb837d74 | xthirioux | | MNoReset i -> instr_cons instr cont |

476 | 3ca27bc7 | ploc | | MStep (il, i, vl) -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont |

477 | | 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 |
||

478 | 45c13277 | xthirioux | |

479 | and instrs_replace_var fvar instrs cont = |
||

480 | List.fold_right (instr_replace_var fvar) instrs cont |
||

481 | |||

482 | let step_replace_var fvar step = |
||

483 | (* Some outputs may have been replaced by locals. |
||

484 | We then need to rename those outputs |
||

485 | without changing their clocks, etc *) |
||

486 | let outputs' = |
||

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

488 | let locals' = |
||

489 | List.fold_left (fun res l -> |
||

490 | let l' = fvar l in |
||

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

492 | then res |
||

493 | else Utils.add_cons l' res) |
||

494 | [] step.step_locals in |
||

495 | { step with |
||

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

497 | step_outputs = outputs'; |
||

498 | step_locals = locals'; |
||

499 | step_instrs = instrs_replace_var fvar step.step_instrs []; |
||

500 | } |
||

501 | |||

502 | let rec machine_replace_variables fvar m = |
||

503 | { m with |
||

504 | mstep = step_replace_var fvar m.mstep |
||

505 | } |
||

506 | |||

507 | let machine_reuse_variables m reuse = |
||

508 | let fvar v = |
||

509 | try |
||

510 | Hashtbl.find reuse v.var_id |
||

511 | with Not_found -> v in |
||

512 | machine_replace_variables fvar m |
||

513 | |||

514 | 04a63d25 | xthirioux | let machines_reuse_variables prog reuse_tables = |

515 | 45c13277 | xthirioux | List.map |

516 | (fun m -> |
||

517 | 04a63d25 | xthirioux | machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables) |

518 | 45c13277 | xthirioux | ) prog |

519 | |||

520 | b1655a21 | xthirioux | let rec instr_assign res instr = |

521 | 3ca27bc7 | ploc | match get_instr_desc instr with |

522 | b1655a21 | xthirioux | | MLocalAssign (i, _) -> Disjunction.CISet.add i res |

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

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

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

526 | | _ -> res |
||

527 | |||

528 | and instrs_assign res instrs = |
||

529 | List.fold_left instr_assign res instrs |
||

530 | |||

531 | let rec instr_constant_assign var instr = |
||

532 | 3ca27bc7 | ploc | match get_instr_desc instr with |

533 | 04a63d25 | xthirioux | | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ }) |

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

535 | b1655a21 | xthirioux | | MBranch (g, hl) -> List.for_all (fun (h, b) -> instrs_constant_assign var b) hl |

536 | | _ -> false |
||

537 | |||

538 | and instrs_constant_assign var instrs = |
||

539 | 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 |
||

540 | |||

541 | let rec instr_reduce branches instr1 cont = |
||

542 | 3ca27bc7 | ploc | match get_instr_desc instr1 with |

543 | 04a63d25 | xthirioux | | MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont) |

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

545 | 3ca27bc7 | ploc | | MBranch (g, hl) -> (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl))) :: cont |

546 | b1655a21 | xthirioux | | _ -> instr1 :: cont |

547 | |||

548 | and instrs_reduce branches instrs cont = |
||

549 | match instrs with |
||

550 | | [] -> cont |
||

551 | | [i] -> instr_reduce branches i cont |
||

552 | | i1::i2::q -> i1 :: instrs_reduce branches (i2::q) cont |
||

553 | |||

554 | let rec instrs_fusion instrs = |
||

555 | 3ca27bc7 | ploc | match instrs, List.map get_instr_desc instrs with |

556 | | [], [] |
||

557 | | [_], [_] -> |
||

558 | b1655a21 | xthirioux | instrs |

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

560 | b1655a21 | xthirioux | instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q) |

561 | 3ca27bc7 | ploc | | i1::i2::q, _ -> |

562 | b1655a21 | xthirioux | i1 :: instrs_fusion (i2::q) |

563 | 3ca27bc7 | ploc | | _ -> assert false (* Other cases should not happen since both lists are of same size *) |

564 | |||

565 | b1655a21 | xthirioux | let step_fusion step = |

566 | { step with |
||

567 | step_instrs = instrs_fusion step.step_instrs; |
||

568 | } |
||

569 | |||

570 | let rec machine_fusion m = |
||

571 | { m with |
||

572 | mstep = step_fusion m.mstep |
||

573 | } |
||

574 | |||

575 | let machines_fusion prog = |
||

576 | List.map machine_fusion prog |
||

577 | cf78a589 | ploc | |

578 | 13507742 | ploc | |

579 | (*** Main function ***) |
||

580 | |||

581 | let optimize prog node_schs machine_code = |
||

582 | let machine_code = |
||

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

584 | begin |
||

585 | Log.report ~level:1 |
||

586 | (fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,"); |
||

587 | let machine_code = machines_cse machine_code in |
||

588 | 2863281f | ploc | Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "pp_machines machine_code); |

589 | 13507742 | ploc | machine_code |

590 | end |
||

591 | else |
||

592 | machine_code |
||

593 | in |
||

594 | (* Optimize machine code *) |
||

595 | let machine_code, removed_table = |
||

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

597 | begin |
||

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

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

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

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

602 | c35de73b | ploc | (pp_imap (pp_elim empty_machine)) removed_table); |

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

604 | 13507742 | ploc | machine_code, removed_table |

605 | end |
||

606 | else |
||

607 | machine_code, IMap.empty |
||

608 | in |
||

609 | (* Optimize machine code *) |
||

610 | let machine_code = |
||

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

612 | begin |
||

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

614 | let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in |
||

615 | let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in |
||

616 | machines_fusion (machines_reuse_variables machine_code reuse_tables) |
||

617 | end |
||

618 | else |
||

619 | machine_code |
||

620 | in |
||

621 | |||

622 | |||

623 | machine_code |
||

624 | |||

625 | |||

626 | cf78a589 | ploc | (* Local Variables: *) |

627 | (* compile-command:"make -C .." *) |
||

628 | (* End: *) |