## lustrec / src / optimize_machine.ml @ 37419cf4

History | View | Annotate | Download (22.9 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 | cf78a589 | ploc | open LustreSpec |

14 | open Corelang |
||

15 | b1655a21 | xthirioux | open Causality |

16 | cf78a589 | ploc | open Machine_code |

17 | ec433d69 | xthirioux | open Dimension |

18 | cf78a589 | ploc | |

19 | 55537f48 | xthirioux | |

20 | d0b1ec56 | xthirioux | let pp_elim fmt elim = |

21 | begin |
||

22 | 521e2a6b | ploc | 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 | d0b1ec56 | xthirioux | end |

26 | |||

27 | cf78a589 | ploc | let rec eliminate elim instr = |

28 | let e_expr = eliminate_expr elim in |
||

29 | 04a63d25 | xthirioux | match instr with |

30 | | MComment _ -> instr |
||

31 | cf78a589 | ploc | | MLocalAssign (i,v) -> MLocalAssign (i, e_expr v) |

32 | | MStateAssign (i,v) -> MStateAssign (i, e_expr v) |
||

33 | | MReset i -> instr |
||

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

35 | cf78a589 | ploc | | MStep (il, i, vl) -> MStep(il, i, List.map e_expr vl) |

36 | | MBranch (g,hl) -> |
||

37 | MBranch |
||

38 | (e_expr g, |
||

39 | (List.map |
||

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

41 | hl |
||

42 | ) |
||

43 | ) |
||

44 | |||

45 | and eliminate_expr elim expr = |
||

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

47 | d0b1ec56 | xthirioux | | LocalVar v -> (try IMap.find v.var_id elim with Not_found -> expr) |

48 | 04a63d25 | xthirioux | | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)} |

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

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

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

52 | | Cst _ | StateVar _ -> expr |
||

53 | cf78a589 | ploc | |

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

55 | 45f0f48d | xthirioux | Dimension.expr_replace_expr |

56 | (fun v -> try |
||

57 | dimension_of_value (IMap.find v elim) |
||

58 | with Not_found -> mkdim_ident dim.dim_loc v) |
||

59 | dim |
||

60 | ec433d69 | xthirioux | |

61 | ca88e660 | Ploc | |

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

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

64 | d2d9d4cb | ploc | *) |

65 | ca88e660 | Ploc | |

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

67 | 04a63d25 | xthirioux | List.fold_left |

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

69 | (Types.array_element_type res.value_type) |
||

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

71 | expr offset |
||

72 | d7b73fed | xthirioux | |

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

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

75 | | [] , _ |
||

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

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

78 | 04a63d25 | xthirioux | -> let elt_typ = Types.array_element_type typ in |

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

80 | d7b73fed | xthirioux | | Index i :: q, Const_array cl |

81 | 04a63d25 | xthirioux | -> let elt_typ = Types.array_element_type typ in |

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

83 | d7b73fed | xthirioux | | Field f :: q, Const_struct fl |

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

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

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

87 | |||

88 | let simplify_expr_offset m expr = |
||

89 | let rec simplify offset expr = |
||

90 | 04a63d25 | xthirioux | match offset, expr.value_desc with |

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

92 | 04a63d25 | xthirioux | | _ , Fun (id, vl) when Basic_library.is_value_internal_fun expr |

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

94 | d7b73fed | xthirioux | | _ , Fun _ |

95 | | _ , StateVar _ |
||

96 | | _ , LocalVar _ -> unfold_expr_offset m offset expr |
||

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

98 | d7b73fed | xthirioux | | _ , Access (expr, i) -> simplify (Index (dimension_of_value i) :: offset) expr |

99 | | [] , _ -> expr |
||

100 | | Index _ :: q, Power (expr, _) -> simplify q expr |
||

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

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

103 | 04a63d25 | xthirioux | | Index i :: q, Array vl -> unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify q) vl)) expr.value_type) |

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

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

106 | in simplify [] expr |
||

107 | |||

108 | let rec simplify_instr_offset m instr = |
||

109 | match instr with |
||

110 | | MLocalAssign (v, expr) -> MLocalAssign (v, simplify_expr_offset m expr) |
||

111 | | MStateAssign (v, expr) -> MStateAssign (v, simplify_expr_offset m expr) |
||

112 | | MReset id -> instr |
||

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

114 | d7b73fed | xthirioux | | MStep (outputs, id, inputs) -> MStep (outputs, id, List.map (simplify_expr_offset m) inputs) |

115 | | MBranch (cond, brl) |
||

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

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

118 | d7b73fed | xthirioux | |

119 | and simplify_instrs_offset m instrs = |
||

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

121 | |||

122 | d0b1ec56 | xthirioux | let is_scalar_const c = |

123 | match c with |
||

124 | | Const_real _ |
||

125 | 04a63d25 | xthirioux | | Const_int _ |

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

127 | | _ -> false |
||

128 | |||

129 | d7b73fed | xthirioux | (* An instruction v = expr may (and will) be unfolded iff: |

130 | - either expr is atomic |
||

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

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

133 | *) |
||

134 | let is_unfoldable_expr fanin expr = |
||

135 | let rec unfold_const offset cst = |
||

136 | match offset, cst with |
||

137 | | _ , Const_int _ |
||

138 | | _ , Const_real _ |
||

139 | | _ , Const_tag _ -> true |
||

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

141 | | [] , Const_struct _ -> false |
||

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

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

144 | | _ , Const_array _ -> false |
||

145 | | _ -> assert false in |
||

146 | let rec unfold offset expr = |
||

147 | 04a63d25 | xthirioux | match offset, expr.value_desc with |

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

149 | | _ , LocalVar _ |
||

150 | | _ , StateVar _ -> true |
||

151 | | [] , Power _ |
||

152 | | [] , Array _ -> false |
||

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

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

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

156 | | _ , Array _ -> false |
||

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

158 | 04a63d25 | xthirioux | | _ , Fun (id, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr |

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

160 | | _ , Fun _ -> false |
||

161 | | _ -> assert false |
||

162 | in unfold [] expr |
||

163 | c287ba28 | xthirioux | |

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

165 | d0b1ec56 | xthirioux | try |

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

167 | d7b73fed | xthirioux | in is_unfoldable_expr d expr |

168 | with Not_found -> false |
||

169 | 04a63d25 | xthirioux | |

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

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

172 | && basic_unfoldable_assign fanin v expr |
||

173 | |||

174 | d0b1ec56 | xthirioux | let merge_elim elim1 elim2 = |

175 | let merge k e1 e2 = |
||

176 | match e1, e2 with |
||

177 | | Some e1, Some e2 -> if e1 = e2 then Some e1 else None |
||

178 | | _ , Some e2 -> Some e2 |
||

179 | | Some e1, _ -> Some e1 |
||

180 | | _ -> None |
||

181 | in IMap.merge merge elim1 elim2 |
||

182 | |||

183 | cf78a589 | ploc | (* see if elim has to take in account the provided instr: |

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

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

186 | d0b1ec56 | xthirioux | let rec instrs_unfold fanin elim instrs = |

187 | let elim, rev_instrs = |
||

188 | List.fold_left (fun (elim, instrs) instr -> |
||

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

190 | rewritten *) |
||

191 | let instr = eliminate elim instr in |
||

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

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

194 | instr_unfold fanin instrs elim instr |
||

195 | ) (elim, []) instrs |
||

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

197 | |||

198 | and instr_unfold fanin instrs elim instr = |
||

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

200 | cf78a589 | ploc | match instr with |

201 | (* Simple cases*) |
||

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

203 | -> instr_unfold fanin instrs elim (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)) |
||

204 | d0b1ec56 | xthirioux | | MLocalAssign(v, expr) when unfoldable_assign fanin v expr |

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

206 | | MBranch(g, hl) when false |
||

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

208 | let (elim, branches) = |
||

209 | List.fold_right |
||

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

211 | elim_branches (elim, []) |
||

212 | in elim, (MBranch (g, branches) :: instrs) |
||

213 | | _ |
||

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

215 | cf78a589 | ploc | (* default case, we keep the instruction and do not modify elim *) |

216 | |||

217 | |||

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

219 | 1. each expression is rewritten according to the accumulator |
||

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

221 | *) |
||

222 | |||

223 | ec433d69 | xthirioux | let static_call_unfold elim (inst, (n, args)) = |

224 | let replace v = |
||

225 | try |
||

226 | Machine_code.dimension_of_value (IMap.find v elim) |
||

227 | with Not_found -> Dimension.mkdim_ident Location.dummy_loc v |
||

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

229 | |||

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

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

232 | |||

233 | *) |
||

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

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

236 | ec433d69 | xthirioux | let elim_consts, mconst = instrs_unfold fanin elim machine.mconst in |

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

238 | d7b73fed | xthirioux | let instrs = simplify_instrs_offset machine instrs in |

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

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

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

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

243 | cf78a589 | ploc | in |

244 | { |
||

245 | machine with |
||

246 | mstep = { |
||

247 | machine.mstep with |
||

248 | ec433d69 | xthirioux | step_locals = locals; |

249 | d7b73fed | xthirioux | step_instrs = instrs; |

250 | step_checks = checks |
||

251 | ec433d69 | xthirioux | }; |

252 | mconst = mconst; |
||

253 | minstances = minstances; |
||

254 | mcalls = mcalls; |
||

255 | 04a63d25 | xthirioux | }, |

256 | elim_vars |
||

257 | cf78a589 | ploc | |

258 | d0b1ec56 | xthirioux | let instr_of_const top_const = |

259 | let const = const_of_top top_const in |
||

260 | ec433d69 | xthirioux | 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 |

261 | d0b1ec56 | xthirioux | let vdecl = { vdecl with var_type = const.const_type } |

262 | 04a63d25 | xthirioux | in MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type) |

263 | cf78a589 | ploc | |

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

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

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

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

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

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

270 | ) |
||

271 | d0b1ec56 | xthirioux | machines |

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

273 | cf78a589 | ploc | |

274 | c287ba28 | xthirioux | let get_assign_lhs instr = |

275 | match instr with |
||

276 | 04a63d25 | xthirioux | | MLocalAssign(v, e) -> mk_val (LocalVar v) e.value_type |

277 | | MStateAssign(v, e) -> mk_val (StateVar v) e.value_type |
||

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

279 | |||

280 | let get_assign_rhs instr = |
||

281 | match instr with |
||

282 | | MLocalAssign(_, e) |
||

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

284 | | _ -> assert false |
||

285 | |||

286 | let is_assign instr = |
||

287 | match instr with |
||

288 | | MLocalAssign _ |
||

289 | | MStateAssign _ -> true |
||

290 | | _ -> false |
||

291 | |||

292 | let mk_assign v e = |
||

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

294 | c287ba28 | xthirioux | | LocalVar v -> MLocalAssign(v, e) |

295 | | StateVar v -> MStateAssign(v, e) |
||

296 | | _ -> assert false |
||

297 | |||

298 | let rec assigns_instr instr assign = |
||

299 | match instr with |
||

300 | | MLocalAssign (i,_) |
||

301 | | MStateAssign (i,_) -> ISet.add i assign |
||

302 | | MStep (ol, _, _) -> List.fold_right ISet.add ol assign |
||

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

304 | | _ -> assign |
||

305 | |||

306 | and assigns_instrs instrs assign = |
||

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

308 | |||

309 | (* |
||

310 | and substitute_expr subst expr = |
||

311 | match expr with |
||

312 | | StateVar v |
||

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

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

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

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

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

318 | | Cst _ -> expr |
||

319 | *) |
||

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

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

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

323 | *) |
||

324 | let subst_instr subst instrs instr = |
||

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

326 | let instr = eliminate subst instr in |
||

327 | let v = get_assign_lhs instr in |
||

328 | let e = get_assign_rhs instr in |
||

329 | 85da3a4b | ploc | (* Difficulties to merge with unstable. Here is the other code: |

330 | |||

331 | try |
||

332 | c287ba28 | xthirioux | let instr' = List.find (fun instr' -> is_assign instr' && get_assign_rhs instr' = e) instrs in |

333 | 53206908 | xthirioux | match v.value_desc with |

334 | c287ba28 | xthirioux | | LocalVar v -> |

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

336 | | StateVar v -> |
||

337 | 53206908 | xthirioux | let lhs' = get_assign_lhs instr' in |

338 | let typ' = lhs'.value_type in |
||

339 | (match lhs'.value_desc with |
||

340 | c287ba28 | xthirioux | | LocalVar v' -> |

341 | 53206908 | xthirioux | let instr = eliminate subst (mk_assign (mk_val (StateVar v) typ') (mk_val (LocalVar v') typ')) in |

342 | c287ba28 | xthirioux | subst, instr :: instrs |

343 | | StateVar v' -> |
||

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

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

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

347 | c287ba28 | xthirioux | | _ -> assert false) |

348 | | _ -> assert false |
||

349 | with Not_found -> subst, instr :: instrs |
||

350 | |||

351 | 85da3a4b | ploc | *) |

352 | |||

353 | try |
||

354 | c287ba28 | xthirioux | let instr' = List.find (fun instr' -> is_assign instr' && get_assign_rhs instr' = e) instrs in |

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

356 | c287ba28 | xthirioux | | LocalVar v -> |

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

358 | 04a63d25 | xthirioux | | StateVar stv -> |

359 | let lhs = get_assign_lhs instr' in |
||

360 | (match lhs.value_desc with |
||

361 | c287ba28 | xthirioux | | LocalVar v' -> |

362 | 04a63d25 | xthirioux | let instr = eliminate subst (mk_assign v lhs) in |

363 | c287ba28 | xthirioux | subst, instr :: instrs |

364 | 04a63d25 | xthirioux | | StateVar stv' -> |

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

366 | c287ba28 | xthirioux | 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 |

367 | 04a63d25 | xthirioux | IMap.add stv'.var_id v subst, instr :: instrs' |

368 | c287ba28 | xthirioux | | _ -> assert false) |

369 | | _ -> assert false |
||

370 | with Not_found -> subst, instr :: instrs |
||

371 | |||

372 | (** Common sub-expression elimination for machine instructions *) |
||

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

374 | it is an equivalence table |
||

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

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

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

378 | *) |
||

379 | let rec instr_cse (subst, instrs) instr = |
||

380 | match instr with |
||

381 | (* Simple cases*) |
||

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

383 | -> instr_cse (subst, instrs) (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)) |
||

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

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

386 | | _ when is_assign instr |
||

387 | -> subst_instr subst instrs instr |
||

388 | | _ -> (subst, instr :: instrs) |
||

389 | |||

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

391 | *) |
||

392 | let rec instrs_cse subst instrs = |
||

393 | let subst, rev_instrs = |
||

394 | List.fold_left instr_cse (subst, []) instrs |
||

395 | in subst, List.rev rev_instrs |
||

396 | |||

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

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

399 | *) |
||

400 | let machine_cse subst machine = |
||

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

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

403 | let assigned = assigns_instrs instrs ISet.empty |
||

404 | in |
||

405 | { |
||

406 | machine with |
||

407 | mmemory = List.filter (fun vdecl -> ISet.mem vdecl assigned) machine.mmemory; |
||

408 | mstep = { |
||

409 | machine.mstep with |
||

410 | step_locals = List.filter (fun vdecl -> ISet.mem vdecl assigned) machine.mstep.step_locals; |
||

411 | step_instrs = instrs |
||

412 | } |
||

413 | } |
||

414 | |||

415 | let machines_cse machines = |
||

416 | List.map |
||

417 | (machine_cse IMap.empty) |
||

418 | machines |
||

419 | |||

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

421 | |||

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

423 | let rec instr_is_skip instr = |
||

424 | match instr with |
||

425 | 04a63d25 | xthirioux | | MLocalAssign (i, { value_desc = (LocalVar v) ; _}) when i = v -> true |

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

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

428 | | _ -> false |
||

429 | and instrs_are_skip instrs = |
||

430 | List.for_all instr_is_skip instrs |
||

431 | |||

432 | let instr_cons instr cont = |
||

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

434 | |||

435 | let rec instr_remove_skip instr cont = |
||

436 | match instr with |
||

437 | 04a63d25 | xthirioux | | MLocalAssign (i, { value_desc = LocalVar v; _ }) when i = v -> cont |

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

439 | 45c13277 | xthirioux | | MBranch (g, hl) -> MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl) :: cont |

440 | | _ -> instr::cont |
||

441 | |||

442 | and instrs_remove_skip instrs cont = |
||

443 | List.fold_right instr_remove_skip instrs cont |
||

444 | |||

445 | let rec value_replace_var fvar value = |
||

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

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

448 | 04a63d25 | xthirioux | | LocalVar v -> { value with value_desc = LocalVar (fvar v) } |

449 | 45c13277 | xthirioux | | StateVar v -> value |

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

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

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

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

454 | 45c13277 | xthirioux | |

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

456 | match instr with |
||

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

458 | 45c13277 | xthirioux | | MLocalAssign (i, v) -> instr_cons (MLocalAssign (fvar i, value_replace_var fvar v)) cont |

459 | | MStateAssign (i, v) -> instr_cons (MStateAssign (i, value_replace_var fvar v)) cont |
||

460 | | MReset i -> instr_cons instr cont |
||

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

462 | 45c13277 | xthirioux | | MStep (il, i, vl) -> instr_cons (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)) cont |

463 | | MBranch (g, hl) -> instr_cons (MBranch (value_replace_var fvar g, List.map (fun (h, il) -> (h, instrs_replace_var fvar il [])) hl)) cont |
||

464 | |||

465 | and instrs_replace_var fvar instrs cont = |
||

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

467 | |||

468 | let step_replace_var fvar step = |
||

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

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

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

472 | let outputs' = |
||

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

474 | let locals' = |
||

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

476 | let l' = fvar l in |
||

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

478 | then res |
||

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

480 | [] step.step_locals in |
||

481 | { step with |
||

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

483 | step_outputs = outputs'; |
||

484 | step_locals = locals'; |
||

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

486 | } |
||

487 | |||

488 | let rec machine_replace_variables fvar m = |
||

489 | { m with |
||

490 | mstep = step_replace_var fvar m.mstep |
||

491 | } |
||

492 | |||

493 | let machine_reuse_variables m reuse = |
||

494 | let fvar v = |
||

495 | try |
||

496 | Hashtbl.find reuse v.var_id |
||

497 | with Not_found -> v in |
||

498 | machine_replace_variables fvar m |
||

499 | |||

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

501 | 45c13277 | xthirioux | List.map |

502 | (fun m -> |
||

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

504 | 45c13277 | xthirioux | ) prog |

505 | |||

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

507 | match instr with |
||

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

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

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

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

512 | | _ -> res |
||

513 | |||

514 | and instrs_assign res instrs = |
||

515 | List.fold_left instr_assign res instrs |
||

516 | |||

517 | let rec instr_constant_assign var instr = |
||

518 | match instr with |
||

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

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

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

522 | | _ -> false |
||

523 | |||

524 | and instrs_constant_assign var instrs = |
||

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

526 | |||

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

528 | match instr1 with |
||

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

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

531 | b1655a21 | xthirioux | | MBranch (g, hl) -> MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl) :: cont |

532 | | _ -> instr1 :: cont |
||

533 | |||

534 | and instrs_reduce branches instrs cont = |
||

535 | match instrs with |
||

536 | | [] -> cont |
||

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

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

539 | |||

540 | let rec instrs_fusion instrs = |
||

541 | match instrs with |
||

542 | | [] |
||

543 | | [_] -> |
||

544 | instrs |
||

545 | 04a63d25 | xthirioux | | i1::(MBranch ({ value_desc = LocalVar v; _}, hl))::q when instr_constant_assign v i1 -> |

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

547 | 04a63d25 | xthirioux | | i1::(MBranch ({ value_desc = StateVar v; _}, hl))::q when instr_constant_assign v i1 -> |

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

549 | | i1::i2::q -> |
||

550 | i1 :: instrs_fusion (i2::q) |
||

551 | |||

552 | let step_fusion step = |
||

553 | { step with |
||

554 | step_instrs = instrs_fusion step.step_instrs; |
||

555 | } |
||

556 | |||

557 | let rec machine_fusion m = |
||

558 | { m with |
||

559 | mstep = step_fusion m.mstep |
||

560 | } |
||

561 | |||

562 | let machines_fusion prog = |
||

563 | List.map machine_fusion prog |
||

564 | cf78a589 | ploc | |

565 | (* Local Variables: *) |
||

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

567 | (* End: *) |