## lustrec / src / machine_code.ml @ 01c7d5e1

History | View | Annotate | Download (18 KB)

1 | 22fe1c93 | ploc | |
---|---|---|---|

2 | (* ---------------------------------------------------------------------------- |
||

3 | * SchedMCore - A MultiCore Scheduling Framework |
||

4 | * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
||

5 | * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE |
||

6 | * |
||

7 | * This file is part of Prelude |
||

8 | * |
||

9 | * Prelude is free software; you can redistribute it and/or |
||

10 | * modify it under the terms of the GNU Lesser General Public License |
||

11 | * as published by the Free Software Foundation ; either version 2 of |
||

12 | * the License, or (at your option) any later version. |
||

13 | * |
||

14 | * Prelude is distributed in the hope that it will be useful, but |
||

15 | * WITHOUT ANY WARRANTY ; without even the implied warranty of |
||

16 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
||

17 | * Lesser General Public License for more details. |
||

18 | * |
||

19 | * You should have received a copy of the GNU Lesser General Public |
||

20 | * License along with this program ; if not, write to the Free Software |
||

21 | * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
||

22 | * USA |
||

23 | *---------------------------------------------------------------------------- *) |
||

24 | |||

25 | (* This module is used for the lustre to C compiler *) |
||

26 | |||

27 | open LustreSpec |
||

28 | open Corelang |
||

29 | open Clocks |
||

30 | open Causality |
||

31 | |||

32 | exception NormalizationError |
||

33 | |||

34 | module OrdVarDecl:Map.OrderedType with type t=var_decl = |
||

35 | struct type t = var_decl;; let compare = compare end |
||

36 | |||

37 | module ISet = Set.Make(OrdVarDecl) |
||

38 | |||

39 | type value_t = |
||

40 | | Cst of constant |
||

41 | | LocalVar of var_decl |
||

42 | | StateVar of var_decl |
||

43 | | Fun of ident * value_t list |
||

44 | | Array of value_t list |
||

45 | | Access of value_t * value_t |
||

46 | | Power of value_t * value_t |
||

47 | |||

48 | type instr_t = |
||

49 | | MLocalAssign of var_decl * value_t |
||

50 | | MStateAssign of var_decl * value_t |
||

51 | | MReset of ident |
||

52 | | MStep of var_decl list * ident * value_t list |
||

53 | | MBranch of value_t * (label * instr_t list) list |
||

54 | |||

55 | let rec pp_val fmt v = |
||

56 | match v with |
||

57 | | Cst c -> Printers.pp_const fmt c |
||

58 | | LocalVar v -> Format.pp_print_string fmt v.var_id |
||

59 | | StateVar v -> Format.pp_print_string fmt v.var_id |
||

60 | | Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl |
||

61 | | Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i |
||

62 | | Power (v, n) -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n |
||

63 | | Fun (n, vl) -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl |
||

64 | |||

65 | let rec pp_instr fmt i = |
||

66 | match i with |
||

67 | | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v |
||

68 | | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v |
||

69 | | MReset i -> Format.fprintf fmt "reset %s" i |
||

70 | | MStep (il, i, vl) -> |
||

71 | Format.fprintf fmt "%a = %s (%a)" |
||

72 | (Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il |
||

73 | i |
||

74 | (Utils.fprintf_list ~sep:", " pp_val) vl |
||

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

76 | Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]" |
||

77 | pp_val g |
||

78 | (Utils.fprintf_list ~sep:"@," pp_branch) hl |
||

79 | |||

80 | and pp_branch fmt (t, h) = |
||

81 | Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h |
||

82 | |||

83 | type step_t = { |
||

84 | step_checks: (Location.t * value_t) list; |
||

85 | step_inputs: var_decl list; |
||

86 | step_outputs: var_decl list; |
||

87 | step_locals: var_decl list; |
||

88 | step_instrs: instr_t list; |
||

89 | } |
||

90 | |||

91 | type static_call = top_decl * (Dimension.dim_expr list) |
||

92 | |||

93 | type machine_t = { |
||

94 | mname: node_desc; |
||

95 | mmemory: var_decl list; |
||

96 | mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *) |
||

97 | minstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *) |
||

98 | minit: instr_t list; |
||

99 | mstatic: var_decl list; (* static inputs only *) |
||

100 | mstep: step_t; |
||

101 | mspec: node_annot option; |
||

102 | 01c7d5e1 | ploc | mannot: expr_annot list; |

103 | 22fe1c93 | ploc | } |

104 | |||

105 | let pp_step fmt s = |
||

106 | Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@]@ " |
||

107 | (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs |
||

108 | (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs |
||

109 | (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals |
||

110 | (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val fmt c)) s.step_checks |
||

111 | (Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs |
||

112 | |||

113 | let pp_static_call fmt (node, args) = |
||

114 | Format.fprintf fmt "%s<%a>" |
||

115 | (node_name node) |
||

116 | (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args |
||

117 | |||

118 | let pp_machine fmt m = |
||

119 | Format.fprintf fmt |
||

120 | "@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ step :@ @[<v 2>%a@]@ @]@ " |
||

121 | m.mname.node_id |
||

122 | (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory |
||

123 | (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances |
||

124 | (Utils.fprintf_list ~sep:"@ " pp_instr) m.minit |
||

125 | pp_step m.mstep |
||

126 | |||

127 | e135421f | xthirioux | (* Returns the declared stateless status and the computed one. *) |

128 | let get_stateless_status m = |
||

129 | (m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless) |
||

130 | |||

131 | 4e07ac7f | xthirioux | let is_input m id = |

132 | List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs |
||

133 | |||

134 | 22fe1c93 | ploc | let is_output m id = |

135 | List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs |
||

136 | |||

137 | 4e07ac7f | xthirioux | let is_memory m id = |

138 | List.exists (fun o -> o.var_id = id.var_id) m.mmemory |
||

139 | |||

140 | 22fe1c93 | ploc | let conditional c t e = |

141 | MBranch(c, [ (tag_true, t); (tag_false, e) ]) |
||

142 | |||

143 | let dummy_var_decl name typ = |
||

144 | { |
||

145 | var_id = name; |
||

146 | var_dec_type = dummy_type_dec; |
||

147 | var_dec_clock = dummy_clock_dec; |
||

148 | var_dec_const = false; |
||

149 | var_type = typ; |
||

150 | var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true; |
||

151 | var_loc = Location.dummy_loc |
||

152 | } |
||

153 | |||

154 | let arrow_id = "_arrow" |
||

155 | |||

156 | let arrow_typ = Types.new_ty Types.Tunivar |
||

157 | |||

158 | let arrow_desc = |
||

159 | { |
||

160 | node_id = arrow_id; |
||

161 | node_type = Type_predef.type_bin_poly_op; |
||

162 | node_clock = Clock_predef.ck_bin_univ; |
||

163 | node_inputs= [dummy_var_decl "_in1" arrow_typ; dummy_var_decl "_in2" arrow_typ]; |
||

164 | node_outputs= [dummy_var_decl "_out" arrow_typ]; |
||

165 | node_locals= []; |
||

166 | node_gencalls = []; |
||

167 | node_checks = []; |
||

168 | node_asserts = []; |
||

169 | node_eqs= []; |
||

170 | 52cfee34 | xthirioux | node_dec_stateless = false; |

171 | node_stateless = Some false; |
||

172 | 22fe1c93 | ploc | node_spec = None; |

173 | 01c7d5e1 | ploc | node_annot = []; } |

174 | 22fe1c93 | ploc | |

175 | let arrow_top_decl = |
||

176 | { |
||

177 | top_decl_desc = Node arrow_desc; |
||

178 | top_decl_loc = Location.dummy_loc |
||

179 | } |
||

180 | |||

181 | let arrow_machine = |
||

182 | let state = "_first" in |
||

183 | let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in |
||

184 | let var_input1 = List.nth arrow_desc.node_inputs 0 in |
||

185 | let var_input2 = List.nth arrow_desc.node_inputs 1 in |
||

186 | let var_output = List.nth arrow_desc.node_outputs 0 in |
||

187 | { |
||

188 | mname = arrow_desc; |
||

189 | mmemory = [var_state]; |
||

190 | mcalls = []; |
||

191 | minstances = []; |
||

192 | minit = [MStateAssign(var_state, Cst (const_of_bool true))]; |
||

193 | mstatic = []; |
||

194 | mstep = { |
||

195 | step_inputs = arrow_desc.node_inputs; |
||

196 | step_outputs = arrow_desc.node_outputs; |
||

197 | step_locals = []; |
||

198 | step_checks = []; |
||

199 | step_instrs = [conditional (StateVar var_state) |
||

200 | [MStateAssign(var_state, Cst (const_of_bool false)); |
||

201 | MLocalAssign(var_output, LocalVar var_input1)] |
||

202 | [MLocalAssign(var_output, LocalVar var_input2)] ] |
||

203 | }; |
||

204 | mspec = None; |
||

205 | 01c7d5e1 | ploc | mannot = []; |

206 | 22fe1c93 | ploc | } |

207 | |||

208 | let new_instance = |
||

209 | let cpt = ref (-1) in |
||

210 | fun caller callee tag -> |
||

211 | begin |
||

212 | let o = |
||

213 | e135421f | xthirioux | if Stateless.check_node callee then |

214 | 22fe1c93 | ploc | node_name callee |

215 | else |
||

216 | Printf.sprintf "ni_%d" (incr cpt; !cpt) in |
||

217 | let o = |
||

218 | if !Options.ansi && is_generic_node callee |
||

219 | then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e -> e.expr_tag = tag) caller.node_gencalls) |
||

220 | else o in |
||

221 | o |
||

222 | end |
||

223 | |||

224 | (* translate_<foo> : node -> context -> <foo> -> machine code/expression *) |
||

225 | (* the context contains m : state aka memory variables *) |
||

226 | (* si : initialization instructions *) |
||

227 | (* j : node aka machine instances *) |
||

228 | (* d : local variables *) |
||

229 | (* s : step instructions *) |
||

230 | let translate_ident node (m, si, j, d, s) id = |
||

231 | try (* id is a node var *) |
||

232 | 01c7d5e1 | ploc | let var_id = get_node_var id node in |

233 | 22fe1c93 | ploc | if ISet.exists (fun v -> v.var_id = id) m |

234 | then StateVar var_id |
||

235 | else LocalVar var_id |
||

236 | with Not_found -> (* id is a constant *) |
||

237 | LocalVar (Corelang.var_decl_of_const (Hashtbl.find Corelang.consts_table id)) |
||

238 | |||

239 | let rec control_on_clock node ((m, si, j, d, s) as args) ck inst = |
||

240 | 89b9e25c | xthirioux | match (Clocks.repr ck).cdesc with |

241 | 22fe1c93 | ploc | | Con (ck1, cr, l) -> |

242 | d4807c3d | xthirioux | let id = Clocks.const_of_carrier cr in |

243 | 22fe1c93 | ploc | control_on_clock node args ck1 (MBranch (translate_ident node args id, |

244 | [l, [inst]] )) |
||

245 | | _ -> inst |
||

246 | |||

247 | let rec join_branches hl1 hl2 = |
||

248 | match hl1, hl2 with |
||

249 | | [] , _ -> hl2 |
||

250 | | _ , [] -> hl1 |
||

251 | | (t1, h1)::q1, (t2, h2)::q2 -> |
||

252 | if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else |
||

253 | if t1 > t2 then (t2, h2) :: join_branches hl1 q2 |
||

254 | else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2 |
||

255 | |||

256 | and join_guards inst1 insts2 = |
||

257 | match inst1, insts2 with |
||

258 | | _ , [] -> |
||

259 | [inst1] |
||

260 | | MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 -> |
||

261 | MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)) |
||

262 | :: q |
||

263 | | _ -> inst1 :: insts2 |
||

264 | |||

265 | let join_guards_list insts = |
||

266 | List.fold_right join_guards insts [] |
||

267 | |||

268 | let find_eq x eqs = |
||

269 | let rec aux accu eqs = |
||

270 | match eqs with |
||

271 | | [] -> |
||

272 | begin |
||

273 | Format.eprintf "Looking for variable %a in the following equations@.%a@." |
||

274 | Format.pp_print_string x |
||

275 | Printers.pp_node_eqs eqs; |
||

276 | assert false |
||

277 | end |
||

278 | | hd::tl -> |
||

279 | if List.mem x hd.eq_lhs then hd, accu@tl else aux (hd::accu) tl |
||

280 | in |
||

281 | aux [] eqs |
||

282 | |||

283 | 25b4311f | xthirioux | (* specialize predefined (polymorphic) operators |

284 | wrt their instances, so that the C semantics |
||

285 | is preserved *) |
||

286 | let specialize_to_c expr = |
||

287 | match expr.expr_desc with |
||

288 | | Expr_appl (id, e, r) -> |
||

289 | if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e) |
||

290 | then let id = |
||

291 | match id with |
||

292 | | "=" -> "equi" |
||

293 | | "!=" -> "xor" |
||

294 | | _ -> id in |
||

295 | { expr with expr_desc = Expr_appl (id, e, r) } |
||

296 | else expr |
||

297 | | _ -> expr |
||

298 | |||

299 | let specialize_op expr = |
||

300 | match !Options.output with |
||

301 | | "C" -> specialize_to_c expr |
||

302 | | _ -> expr |
||

303 | |||

304 | 22fe1c93 | ploc | let rec translate_expr node ((m, si, j, d, s) as args) expr = |

305 | 25b4311f | xthirioux | let expr = specialize_op expr in |

306 | 22fe1c93 | ploc | match expr.expr_desc with |

307 | | Expr_const v -> Cst v |
||

308 | | Expr_ident x -> translate_ident node args x |
||

309 | | Expr_array el -> Array (List.map (translate_expr node args) el) |
||

310 | | Expr_access (t, i) -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i)) |
||

311 | | Expr_power (e, n) -> Power (translate_expr node args e, translate_expr node args (expr_of_dimension n)) |
||

312 | | Expr_tuple _ |
||

313 | | Expr_arrow _ |
||

314 | | Expr_fby _ |
||

315 | | Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) |
||

316 | | Expr_when (e1, _, _) -> translate_expr node args e1 |
||

317 | | Expr_merge (x, _) -> raise NormalizationError |
||

318 | | Expr_appl (id, e, _) when Basic_library.is_internal_fun id -> |
||

319 | let nd = node_from_name id in |
||

320 | 25b4311f | xthirioux | Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e)) |

321 | 0777a7be | ploc | | Expr_ite (g,t,e) -> ( |

322 | (* special treatment depending on the active backend. For horn backend, ite |
||

323 | are preserved in expression. While they are removed for C or Java |
||

324 | backends. *) |
||

325 | match !Options.output with | "horn" -> |
||

326 | Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e]) |
||

327 | | "C" | "java" | _ -> |
||

328 | (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) |
||

329 | ) |
||

330 | 22fe1c93 | ploc | | _ -> raise NormalizationError |

331 | |||

332 | let translate_guard node args expr = |
||

333 | 0777a7be | ploc | match expr.expr_desc with |

334 | | Expr_ident x -> translate_ident node args x |
||

335 | d4807c3d | xthirioux | | _ -> (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false) |

336 | 22fe1c93 | ploc | |

337 | let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = |
||

338 | 0777a7be | ploc | match expr.expr_desc with |

339 | | Expr_ite (c, t, e) -> let g = translate_guard node args c in |
||

340 | conditional g [translate_act node args (y, t)] |
||

341 | [translate_act node args (y, e)] |
||

342 | | Expr_merge (x, hl) -> MBranch (translate_ident node args x, List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl) |
||

343 | | _ -> MLocalAssign (y, translate_expr node args expr) |
||

344 | 22fe1c93 | ploc | |

345 | let reset_instance node args i r c = |
||

346 | 0777a7be | ploc | match r with |

347 | | None -> [] |
||

348 | | Some (x, l) -> [control_on_clock node args c (MBranch (translate_ident node args x, [l, [MReset i]]))] |
||

349 | 22fe1c93 | ploc | |

350 | let translate_eq node ((m, si, j, d, s) as args) eq = |
||

351 | 89b9e25c | xthirioux | (*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*) |

352 | 22fe1c93 | ploc | match eq.eq_lhs, eq.eq_rhs.expr_desc with |

353 | | [x], Expr_arrow (e1, e2) -> |
||

354 | 01c7d5e1 | ploc | let var_x = get_node_var x node in |

355 | 22fe1c93 | ploc | let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in |

356 | let c1 = translate_expr node args e1 in |
||

357 | let c2 = translate_expr node args e2 in |
||

358 | (m, |
||

359 | MReset o :: si, |
||

360 | Utils.IMap.add o (arrow_top_decl, []) j, |
||

361 | d, |
||

362 | (control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s) |
||

363 | 01c7d5e1 | ploc | | [x], Expr_pre e1 when ISet.mem (get_node_var x node) d -> |

364 | let var_x = get_node_var x node in |
||

365 | 22fe1c93 | ploc | (ISet.add var_x m, |

366 | si, |
||

367 | j, |
||

368 | d, |
||

369 | control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s) |
||

370 | 01c7d5e1 | ploc | | [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d -> |

371 | let var_x = get_node_var x node in |
||

372 | 22fe1c93 | ploc | (ISet.add var_x m, |

373 | MStateAssign (var_x, translate_expr node args e1) :: si, |
||

374 | j, |
||

375 | d, |
||

376 | control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s) |
||

377 | 6d89b953 | ploc | |

378 | | p , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) -> |
||

379 | 01c7d5e1 | ploc | let var_p = List.map (fun v -> get_node_var v node) p in |

380 | 22fe1c93 | ploc | let el = |

381 | match arg.expr_desc with |
||

382 | | Expr_tuple el -> el |
||

383 | | _ -> [arg] in |
||

384 | let vl = List.map (translate_expr node args) el in |
||

385 | let node_f = node_from_name f in |
||

386 | let call_f = |
||

387 | node_f, |
||

388 | NodeDep.filter_static_inputs (node_inputs node_f) el in |
||

389 | let o = new_instance node node_f eq.eq_rhs.expr_tag in |
||

390 | d4807c3d | xthirioux | let call_ck = Clocks.new_var true in |

391 | Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock; |
||

392 | 22fe1c93 | ploc | (m, |

393 | e135421f | xthirioux | (if Stateless.check_node node_f then si else MReset o :: si), |

394 | 6d89b953 | ploc | Utils.IMap.add o call_f j, |

395 | 22fe1c93 | ploc | d, |

396 | reset_instance node args o r eq.eq_rhs.expr_clock @ |
||

397 | d4807c3d | xthirioux | (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s) |

398 | 0777a7be | ploc | |

399 | (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) |
||

400 | are preserved. While they are replaced as if g then x = t else x = e in C or Java |
||

401 | backends. *) |
||

402 | | [x], Expr_ite (c, t, e) |
||

403 | when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false) |
||

404 | -> |
||

405 | 01c7d5e1 | ploc | let var_x = get_node_var x node in |

406 | 7a19992d | ploc | (m, |

407 | si, |
||

408 | j, |
||

409 | d, |
||

410 | (control_on_clock node args eq.eq_rhs.expr_clock |
||

411 | 0777a7be | ploc | (MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s) |

412 | 7a19992d | ploc | ) |

413 | 0777a7be | ploc | |

414 | | [x], _ -> ( |
||

415 | 01c7d5e1 | ploc | let var_x = get_node_var x node in |

416 | 22fe1c93 | ploc | (m, si, j, d, |

417 | 6d89b953 | ploc | control_on_clock |

418 | node |
||

419 | args |
||

420 | eq.eq_rhs.expr_clock |
||

421 | (translate_act node args (var_x, eq.eq_rhs)) :: s |
||

422 | ) |
||

423 | 0777a7be | ploc | ) |

424 | 22fe1c93 | ploc | | _ -> |

425 | begin |
||

426 | Format.eprintf "unsupported equation: %a@?" Printers.pp_node_eq eq; |
||

427 | assert false |
||

428 | end |
||

429 | |||

430 | let translate_eqs node args eqs = |
||

431 | List.fold_right (fun eq args -> translate_eq node args eq) eqs args;; |
||

432 | |||

433 | 88486aaf | ploc | let translate_decl nd sch = |

434 | 22fe1c93 | ploc | (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*) |

435 | let split_eqs = Splitting.tuple_split_eq_list nd.node_eqs in |
||

436 | let eqs_rev, remainder = |
||

437 | List.fold_left |
||

438 | (fun (accu, node_eqs_remainder) v -> |
||

439 | if List.exists (fun eq -> List.mem v eq.eq_lhs) accu |
||

440 | then |
||

441 | (accu, node_eqs_remainder) |
||

442 | else |
||

443 | 7afcba5a | xthirioux | (*if List.exists (fun vdecl -> vdecl.var_id = v) nd.node_locals |

444 | 22fe1c93 | ploc | || List.exists (fun vdecl -> vdecl.var_id = v) nd.node_outputs |

445 | 7afcba5a | xthirioux | then*) |

446 | 22fe1c93 | ploc | let eq_v, remainder = find_eq v node_eqs_remainder in |

447 | eq_v::accu, remainder |
||

448 | 7afcba5a | xthirioux | (* else it is a constant value, checked during typing phase |

449 | 22fe1c93 | ploc | else |

450 | 7afcba5a | xthirioux | accu, node_eqs_remainder *) |

451 | 22fe1c93 | ploc | ) |

452 | ([], split_eqs) |
||

453 | sch |
||

454 | in |
||

455 | if List.length remainder > 0 then ( |
||

456 | Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?" |
||

457 | Printers.pp_node_eqs remainder |
||

458 | Printers.pp_node_eqs nd.node_eqs; |
||

459 | assert false ) |
||

460 | ; |
||

461 | |||

462 | let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in |
||

463 | let m, init, j, locals, s = translate_eqs nd init_args (List.rev eqs_rev) in |
||

464 | let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in |
||

465 | { |
||

466 | mname = nd; |
||

467 | mmemory = ISet.elements m; |
||

468 | mcalls = mmap; |
||

469 | e135421f | xthirioux | minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap; |

470 | 22fe1c93 | ploc | minit = init; |

471 | mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs; |
||

472 | mstep = { |
||

473 | step_inputs = nd.node_inputs; |
||

474 | step_outputs = nd.node_outputs; |
||

475 | step_locals = ISet.elements (ISet.diff locals m); |
||

476 | step_checks = List.map (fun d -> d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks; |
||

477 | 0777a7be | ploc | step_instrs = ( |

478 | (* special treatment depending on the active backend. For horn backend, |
||

479 | common branches are not merged while they are in C or Java |
||

480 | backends. *) |
||

481 | match !Options.output with |
||

482 | | "horn" -> s |
||

483 | | "C" | "java" | _ -> join_guards_list s |
||

484 | ); |
||

485 | 22fe1c93 | ploc | }; |

486 | mspec = nd.node_spec; |
||

487 | mannot = nd.node_annot; |
||

488 | } |
||

489 | |||

490 | 88486aaf | ploc | (** takes the global delcarations and the scheduling associated to each node *) |

491 | let translate_prog decls node_schs = |
||

492 | 22fe1c93 | ploc | let nodes = get_nodes decls in |

493 | 88486aaf | ploc | List.map |

494 | (fun node -> |
||

495 | 3bfed7f9 | xthirioux | let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in |

496 | 88486aaf | ploc | translate_decl node sch |

497 | ) nodes |
||

498 | 3ee1012f | ploc | |

499 | let get_machine_opt name machines = |
||

500 | List.fold_left |
||

501 | (fun res m -> |
||

502 | match res with |
||

503 | | Some _ -> res |
||

504 | | None -> if m.mname.node_id = name then Some m else None) |
||

505 | None machines |
||

506 | |||

507 | 22fe1c93 | ploc | |

508 | (* Local Variables: *) |
||

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

510 | (* End: *) |