## lustrec / src / machine_code.ml @ 5538b7ac

History | View | Annotate | Download (17.3 KB)

1 | 0cbf0839 | 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 | mannot: expr_annot option; |
||

103 | } |
||

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 | 5538b7ac | 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 | 0cbf0839 | ploc | let is_output m id = |

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

133 | |||

134 | let conditional c t e = |
||

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

136 | |||

137 | let dummy_var_decl name typ = |
||

138 | { |
||

139 | var_id = name; |
||

140 | var_dec_type = dummy_type_dec; |
||

141 | var_dec_clock = dummy_clock_dec; |
||

142 | var_dec_const = false; |
||

143 | var_type = typ; |
||

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

145 | var_loc = Location.dummy_loc |
||

146 | } |
||

147 | |||

148 | let arrow_id = "_arrow" |
||

149 | |||

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

151 | |||

152 | let arrow_desc = |
||

153 | { |
||

154 | node_id = arrow_id; |
||

155 | node_type = Type_predef.type_bin_poly_op; |
||

156 | node_clock = Clock_predef.ck_bin_univ; |
||

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

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

159 | node_locals= []; |
||

160 | node_gencalls = []; |
||

161 | node_checks = []; |
||

162 | node_asserts = []; |
||

163 | node_eqs= []; |
||

164 | d3e4c22f | xthirioux | node_dec_stateless = false; |

165 | node_stateless = Some false; |
||

166 | 0cbf0839 | ploc | node_spec = None; |

167 | node_annot = None; } |
||

168 | |||

169 | let arrow_top_decl = |
||

170 | { |
||

171 | top_decl_desc = Node arrow_desc; |
||

172 | top_decl_loc = Location.dummy_loc |
||

173 | } |
||

174 | |||

175 | let arrow_machine = |
||

176 | let state = "_first" in |
||

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

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

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

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

181 | { |
||

182 | mname = arrow_desc; |
||

183 | mmemory = [var_state]; |
||

184 | mcalls = []; |
||

185 | minstances = []; |
||

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

187 | mstatic = []; |
||

188 | mstep = { |
||

189 | step_inputs = arrow_desc.node_inputs; |
||

190 | step_outputs = arrow_desc.node_outputs; |
||

191 | step_locals = []; |
||

192 | step_checks = []; |
||

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

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

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

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

197 | }; |
||

198 | mspec = None; |
||

199 | mannot = None; |
||

200 | } |
||

201 | |||

202 | let new_instance = |
||

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

204 | fun caller callee tag -> |
||

205 | begin |
||

206 | let o = |
||

207 | 5538b7ac | xthirioux | if Stateless.check_node callee then |

208 | 0cbf0839 | ploc | node_name callee |

209 | else |
||

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

211 | let o = |
||

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

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

214 | else o in |
||

215 | o |
||

216 | end |
||

217 | |||

218 | let const_of_carrier cr = |
||

219 | match (carrier_repr cr).carrier_desc with |
||

220 | | Carry_const id -> id |
||

221 | d3e4c22f | xthirioux | | Carry_name |

222 | | Carry_var |
||

223 | | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *) |
||

224 | 0cbf0839 | ploc | |

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

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

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

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

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

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

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

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

233 | let var_id = node_var id node in |
||

234 | if ISet.exists (fun v -> v.var_id = id) m |
||

235 | then StateVar var_id |
||

236 | else LocalVar var_id |
||

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

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

239 | |||

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

241 | 2ea1e4a6 | xthirioux | match (Clocks.repr ck).cdesc with |

242 | 0cbf0839 | ploc | | Con (ck1, cr, l) -> |

243 | let id = const_of_carrier cr in |
||

244 | control_on_clock node args ck1 (MBranch (translate_ident node args id, |
||

245 | [l, [inst]] )) |
||

246 | | _ -> inst |
||

247 | |||

248 | let rec join_branches hl1 hl2 = |
||

249 | match hl1, hl2 with |
||

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

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

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

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

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

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

256 | |||

257 | and join_guards inst1 insts2 = |
||

258 | match inst1, insts2 with |
||

259 | | _ , [] -> |
||

260 | [inst1] |
||

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

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

263 | :: q |
||

264 | | _ -> inst1 :: insts2 |
||

265 | |||

266 | let join_guards_list insts = |
||

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

268 | |||

269 | let find_eq x eqs = |
||

270 | let rec aux accu eqs = |
||

271 | match eqs with |
||

272 | | [] -> |
||

273 | begin |
||

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

275 | Format.pp_print_string x |
||

276 | Printers.pp_node_eqs eqs; |
||

277 | assert false |
||

278 | end |
||

279 | | hd::tl -> |
||

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

281 | in |
||

282 | aux [] eqs |
||

283 | |||

284 | let rec translate_expr node ((m, si, j, d, s) as args) expr = |
||

285 | match expr.expr_desc with |
||

286 | | Expr_const v -> Cst v |
||

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

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

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

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

291 | | Expr_tuple _ |
||

292 | | Expr_arrow _ |
||

293 | | Expr_fby _ |
||

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

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

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

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

298 | let nd = node_from_name id in |
||

299 | (match e.expr_desc with |
||

300 | | Expr_tuple el -> Fun (node_name nd, List.map (translate_expr node args) el) |
||

301 | | _ -> Fun (node_name nd, [translate_expr node args e])) |
||

302 | 29ad4531 | ploc | | Expr_ite (g,t,e) -> ( |

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

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

305 | backends. *) |
||

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

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

308 | | "C" | "java" | _ -> |
||

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

310 | ) |
||

311 | 0cbf0839 | ploc | | _ -> raise NormalizationError |

312 | |||

313 | let translate_guard node args expr = |
||

314 | 29ad4531 | ploc | match expr.expr_desc with |

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

316 | | _ -> assert false |
||

317 | 0cbf0839 | ploc | |

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

319 | 29ad4531 | ploc | match expr.expr_desc with |

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

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

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

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

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

325 | 0cbf0839 | ploc | |

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

327 | 29ad4531 | ploc | match r with |

328 | | None -> [] |
||

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

330 | 0cbf0839 | ploc | |

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

332 | 2ea1e4a6 | xthirioux | (*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*) |

333 | 0cbf0839 | ploc | match eq.eq_lhs, eq.eq_rhs.expr_desc with |

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

335 | let var_x = node_var x node in |
||

336 | let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in |
||

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

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

339 | (m, |
||

340 | MReset o :: si, |
||

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

342 | d, |
||

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

344 | | [x], Expr_pre e1 when ISet.mem (node_var x node) d -> |
||

345 | let var_x = node_var x node in |
||

346 | (ISet.add var_x m, |
||

347 | si, |
||

348 | j, |
||

349 | d, |
||

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

351 | | [x], Expr_fby (e1, e2) when ISet.mem (node_var x node) d -> |
||

352 | let var_x = node_var x node in |
||

353 | (ISet.add var_x m, |
||

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

355 | j, |
||

356 | d, |
||

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

358 | | p , Expr_appl (f, arg, r) -> |
||

359 | let var_p = List.map (fun v -> node_var v node) p in |
||

360 | let el = |
||

361 | match arg.expr_desc with |
||

362 | | Expr_tuple el -> el |
||

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

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

365 | let node_f = node_from_name f in |
||

366 | let call_f = |
||

367 | node_f, |
||

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

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

370 | (m, |
||

371 | 5538b7ac | xthirioux | (if Stateless.check_node node_f then si else MReset o :: si), |

372 | 0cbf0839 | ploc | (if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j), |

373 | d, |
||

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

375 | (control_on_clock node args eq.eq_rhs.expr_clock (MStep (var_p, o, vl))) :: s) |
||

376 | 29ad4531 | ploc | |

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

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

379 | backends. *) |
||

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

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

382 | -> |
||

383 | 04a7df69 | ploc | let var_x = node_var x node in |

384 | (m, |
||

385 | si, |
||

386 | j, |
||

387 | d, |
||

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

389 | 29ad4531 | ploc | (MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s) |

390 | 04a7df69 | ploc | ) |

391 | 29ad4531 | ploc | |

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

393 | 0cbf0839 | ploc | let var_x = node_var x node in |

394 | (m, si, j, d, |
||

395 | control_on_clock node args eq.eq_rhs.expr_clock (translate_act node args (var_x, eq.eq_rhs)) :: s) |
||

396 | 29ad4531 | ploc | ) |

397 | 0cbf0839 | ploc | | _ -> |

398 | begin |
||

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

400 | assert false |
||

401 | end |
||

402 | |||

403 | let translate_eqs node args eqs = |
||

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

405 | |||

406 | let translate_decl nd = |
||

407 | (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*) |
||

408 | let nd, sch = Scheduling.schedule_node nd in |
||

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

410 | let eqs_rev, remainder = |
||

411 | List.fold_left |
||

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

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

414 | then |
||

415 | (accu, node_eqs_remainder) |
||

416 | else |
||

417 | if List.exists (fun vdecl -> vdecl.var_id = v) nd.node_locals |
||

418 | || List.exists (fun vdecl -> vdecl.var_id = v) nd.node_outputs |
||

419 | then |
||

420 | let eq_v, remainder = find_eq v node_eqs_remainder in |
||

421 | eq_v::accu, remainder |
||

422 | (* else it is a constant value, checked during typing phase *) |
||

423 | else |
||

424 | accu, node_eqs_remainder |
||

425 | ) |
||

426 | ([], split_eqs) |
||

427 | sch |
||

428 | in |
||

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

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

431 | Printers.pp_node_eqs remainder |
||

432 | Printers.pp_node_eqs nd.node_eqs; |
||

433 | assert false ) |
||

434 | ; |
||

435 | |||

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

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

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

439 | { |
||

440 | mname = nd; |
||

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

442 | mcalls = mmap; |
||

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

444 | 0cbf0839 | ploc | minit = init; |

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

446 | mstep = { |
||

447 | step_inputs = nd.node_inputs; |
||

448 | step_outputs = nd.node_outputs; |
||

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

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

451 | 29ad4531 | ploc | step_instrs = ( |

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

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

454 | backends. *) |
||

455 | match !Options.output with |
||

456 | | "horn" -> s |
||

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

458 | ); |
||

459 | 0cbf0839 | ploc | }; |

460 | mspec = nd.node_spec; |
||

461 | mannot = nd.node_annot; |
||

462 | } |
||

463 | |||

464 | |||

465 | let translate_prog decls = |
||

466 | let nodes = get_nodes decls in |
||

467 | (* What to do with Imported/Sensor/Actuators ? *) |
||

468 | 5538b7ac | xthirioux | (*arrow_machine ::*) List.map translate_decl nodes |

469 | f6923c9e | ploc | |

470 | let get_machine_opt name machines = |
||

471 | List.fold_left |
||

472 | (fun res m -> |
||

473 | match res with |
||

474 | | Some _ -> res |
||

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

476 | None machines |
||

477 | |||

478 | 0cbf0839 | ploc | |

479 | (* Local Variables: *) |
||

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

481 | (* End: *) |