## lustrec / src / machine_code.ml @ 22fe1c93

History | View | Annotate | Download (16 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 | 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 | let is_output m id = |
||

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

129 | |||

130 | let conditional c t e = |
||

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

132 | |||

133 | let dummy_var_decl name typ = |
||

134 | { |
||

135 | var_id = name; |
||

136 | var_dec_type = dummy_type_dec; |
||

137 | var_dec_clock = dummy_clock_dec; |
||

138 | var_dec_const = false; |
||

139 | var_type = typ; |
||

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

141 | var_loc = Location.dummy_loc |
||

142 | } |
||

143 | |||

144 | let arrow_id = "_arrow" |
||

145 | |||

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

147 | |||

148 | let arrow_desc = |
||

149 | { |
||

150 | node_id = arrow_id; |
||

151 | node_type = Type_predef.type_bin_poly_op; |
||

152 | node_clock = Clock_predef.ck_bin_univ; |
||

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

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

155 | node_locals= []; |
||

156 | node_gencalls = []; |
||

157 | node_checks = []; |
||

158 | node_asserts = []; |
||

159 | node_eqs= []; |
||

160 | node_spec = None; |
||

161 | node_annot = None; } |
||

162 | |||

163 | let arrow_top_decl = |
||

164 | { |
||

165 | top_decl_desc = Node arrow_desc; |
||

166 | top_decl_loc = Location.dummy_loc |
||

167 | } |
||

168 | |||

169 | let arrow_machine = |
||

170 | let state = "_first" in |
||

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

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

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

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

175 | { |
||

176 | mname = arrow_desc; |
||

177 | mmemory = [var_state]; |
||

178 | mcalls = []; |
||

179 | minstances = []; |
||

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

181 | mstatic = []; |
||

182 | mstep = { |
||

183 | step_inputs = arrow_desc.node_inputs; |
||

184 | step_outputs = arrow_desc.node_outputs; |
||

185 | step_locals = []; |
||

186 | step_checks = []; |
||

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

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

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

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

191 | }; |
||

192 | mspec = None; |
||

193 | mannot = None; |
||

194 | } |
||

195 | |||

196 | let is_stateless_node node = |
||

197 | (node_name node <> arrow_id) && |
||

198 | match node.top_decl_desc with |
||

199 | | Node id -> false (* TODO: add a check after the machines are produced. Start from the main node and do a DFS to compute the stateless/statefull property of nodes. Stateless nodes should not be reset *) |
||

200 | | ImportedNode id -> id.nodei_stateless |
||

201 | | ImportedFun _ -> true |
||

202 | | _ -> assert false |
||

203 | |||

204 | let new_instance = |
||

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

206 | fun caller callee tag -> |
||

207 | begin |
||

208 | let o = |
||

209 | if is_stateless_node callee then |
||

210 | node_name callee |
||

211 | else |
||

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

213 | let o = |
||

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

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

216 | else o in |
||

217 | o |
||

218 | end |
||

219 | |||

220 | let const_of_carrier cr = |
||

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

222 | | Carry_const id -> id |
||

223 | | Carry_name -> assert false |
||

224 | | Carry_var -> assert false |
||

225 | | Carry_link _ -> assert false (* TODO check this Xavier *) |
||

226 | |||

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

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

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

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

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

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

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

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

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

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

237 | then StateVar var_id |
||

238 | else LocalVar var_id |
||

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

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

241 | |||

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

243 | match ck.cdesc with |
||

244 | | Con (ck1, cr, l) -> |
||

245 | let id = const_of_carrier cr in |
||

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

247 | [l, [inst]] )) |
||

248 | | _ -> inst |
||

249 | |||

250 | let rec join_branches hl1 hl2 = |
||

251 | match hl1, hl2 with |
||

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

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

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

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

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

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

258 | |||

259 | and join_guards inst1 insts2 = |
||

260 | match inst1, insts2 with |
||

261 | | _ , [] -> |
||

262 | [inst1] |
||

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

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

265 | :: q |
||

266 | | _ -> inst1 :: insts2 |
||

267 | |||

268 | let join_guards_list insts = |
||

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

270 | |||

271 | let find_eq x eqs = |
||

272 | let rec aux accu eqs = |
||

273 | match eqs with |
||

274 | | [] -> |
||

275 | begin |
||

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

277 | Format.pp_print_string x |
||

278 | Printers.pp_node_eqs eqs; |
||

279 | assert false |
||

280 | end |
||

281 | | hd::tl -> |
||

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

283 | in |
||

284 | aux [] eqs |
||

285 | |||

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

287 | match expr.expr_desc with |
||

288 | | Expr_const v -> Cst v |
||

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

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

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

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

293 | | Expr_tuple _ |
||

294 | | Expr_ite _ |
||

295 | | Expr_arrow _ |
||

296 | | Expr_fby _ |
||

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

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

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

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

301 | let nd = node_from_name id in |
||

302 | (match e.expr_desc with |
||

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

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

305 | | _ -> raise NormalizationError |
||

306 | |||

307 | let translate_guard node args expr = |
||

308 | match expr.expr_desc with |
||

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

310 | | _ -> assert false |
||

311 | |||

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

313 | match expr.expr_desc with |
||

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

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

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

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

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

319 | |||

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

321 | match r with |
||

322 | | None -> [] |
||

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

324 | |||

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

326 | (*Format.eprintf "translate_eq %a@." Printers.pp_node_eq eq;*) |
||

327 | match eq.eq_lhs, eq.eq_rhs.expr_desc with |
||

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

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

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

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

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

333 | (m, |
||

334 | MReset o :: si, |
||

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

336 | d, |
||

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

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

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

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

341 | si, |
||

342 | j, |
||

343 | d, |
||

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

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

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

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

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

349 | j, |
||

350 | d, |
||

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

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

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

354 | let el = |
||

355 | match arg.expr_desc with |
||

356 | | Expr_tuple el -> el |
||

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

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

359 | let node_f = node_from_name f in |
||

360 | let call_f = |
||

361 | node_f, |
||

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

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

364 | (m, |
||

365 | (if is_stateless_node node_f then si else MReset o :: si), |
||

366 | (if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j), |
||

367 | d, |
||

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

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

370 | | [x], _ -> |
||

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

372 | (m, si, j, d, |
||

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

374 | | _ -> |
||

375 | begin |
||

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

377 | assert false |
||

378 | end |
||

379 | |||

380 | let translate_eqs node args eqs = |
||

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

382 | |||

383 | let translate_decl nd = |
||

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

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

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

387 | let eqs_rev, remainder = |
||

388 | List.fold_left |
||

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

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

391 | then |
||

392 | (accu, node_eqs_remainder) |
||

393 | else |
||

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

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

396 | then |
||

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

398 | eq_v::accu, remainder |
||

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

400 | else |
||

401 | accu, node_eqs_remainder |
||

402 | ) |
||

403 | ([], split_eqs) |
||

404 | sch |
||

405 | in |
||

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

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

408 | Printers.pp_node_eqs remainder |
||

409 | Printers.pp_node_eqs nd.node_eqs; |
||

410 | assert false ) |
||

411 | ; |
||

412 | |||

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

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

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

416 | { |
||

417 | mname = nd; |
||

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

419 | mcalls = mmap; |
||

420 | minstances = List.filter (fun (_, (n,_)) -> not (is_stateless_node n)) mmap; |
||

421 | minit = init; |
||

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

423 | mstep = { |
||

424 | step_inputs = nd.node_inputs; |
||

425 | step_outputs = nd.node_outputs; |
||

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

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

428 | step_instrs = join_guards_list s; |
||

429 | }; |
||

430 | mspec = nd.node_spec; |
||

431 | mannot = nd.node_annot; |
||

432 | } |
||

433 | |||

434 | |||

435 | let translate_prog decls = |
||

436 | let nodes = get_nodes decls in |
||

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

438 | arrow_machine :: List.map translate_decl nodes |
||

439 | |||

440 | |||

441 | (* Local Variables: *) |
||

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

443 | (* End: *) |