## lustrec / src / machine_code.ml @ fc476249

History | View | Annotate | Download (23.9 KB)

1 | e2068500 | Temesghen Kahsai | (********************************************************************) |
---|---|---|---|

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 | open LustreSpec |
||

13 | open Corelang |
||

14 | open Clocks |
||

15 | open Causality |
||

16 | |||

17 | exception NormalizationError |
||

18 | |||

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

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

21 | |||

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

23 | |||

24 | let rec pp_val fmt v = |
||

25 | 3b2bd83d | Teme | match v.value_desc with |

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

27 | e2068500 | Temesghen Kahsai | | LocalVar v -> Format.pp_print_string fmt v.var_id |

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

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

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

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

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

33 | |||

34 | let rec pp_instr fmt i = |
||

35 | match i with |
||

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

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

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

39 | 3b2bd83d | Teme | | MNoReset i -> Format.fprintf fmt "noreset %s" i |

40 | e2068500 | Temesghen Kahsai | | MStep (il, i, vl) -> |

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

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

43 | i |
||

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

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

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

47 | pp_val g |
||

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

49 | 3b2bd83d | Teme | | MComment s -> Format.pp_print_string fmt s |

50 | e2068500 | Temesghen Kahsai | |

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

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

53 | |||

54 | and pp_instrs fmt il = |
||

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

56 | |||

57 | type step_t = { |
||

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

59 | step_inputs: var_decl list; |
||

60 | step_outputs: var_decl list; |
||

61 | step_locals: var_decl list; |
||

62 | step_instrs: instr_t list; |
||

63 | step_asserts: value_t list; |
||

64 | } |
||

65 | |||

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

67 | |||

68 | type machine_t = { |
||

69 | mname: node_desc; |
||

70 | mmemory: var_decl list; |
||

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

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

73 | minit: instr_t list; |
||

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

75 | mconst: instr_t list; (* assignments of node constant locals *) |
||

76 | mstep: step_t; |
||

77 | mspec: node_annot option; |
||

78 | mannot: expr_annot list; |
||

79 | } |
||

80 | |||

81 | let pp_step fmt s = |
||

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

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

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

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

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

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

88 | (Utils.fprintf_list ~sep:", " pp_val) s.step_asserts |
||

89 | |||

90 | |||

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

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

93 | (node_name node) |
||

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

95 | |||

96 | let pp_machine fmt m = |
||

97 | Format.fprintf fmt |
||

98 | "@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ " |
||

99 | m.mname.node_id |
||

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

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

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

103 | (Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst |
||

104 | pp_step m.mstep |
||

105 | (fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec) |
||

106 | (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot |
||

107 | |||

108 | 3b2bd83d | Teme | let rec is_const_value v = |

109 | match v.value_desc with |
||

110 | | Cst _ -> true |
||

111 | | Fun (id, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args |
||

112 | | _ -> false |
||

113 | |||

114 | e2068500 | Temesghen Kahsai | (* Returns the declared stateless status and the computed one. *) |

115 | let get_stateless_status m = |
||

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

117 | |||

118 | let is_input m id = |
||

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

120 | |||

121 | let is_output m id = |
||

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

123 | |||

124 | let is_memory m id = |
||

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

126 | |||

127 | let conditional c t e = |
||

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

129 | |||

130 | let dummy_var_decl name typ = |
||

131 | { |
||

132 | var_id = name; |
||

133 | var_orig = false; |
||

134 | var_dec_type = dummy_type_dec; |
||

135 | var_dec_clock = dummy_clock_dec; |
||

136 | var_dec_const = false; |
||

137 | var_dec_value = None; |
||

138 | var_type = typ; |
||

139 | 3b2bd83d | Teme | var_clock = Clocks.new_ck Clocks.Cvar true; |

140 | e2068500 | Temesghen Kahsai | var_loc = Location.dummy_loc |

141 | } |
||

142 | |||

143 | let arrow_id = "_arrow" |
||

144 | |||

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

146 | |||

147 | let arrow_desc = |
||

148 | { |
||

149 | node_id = arrow_id; |
||

150 | node_type = Type_predef.type_bin_poly_op; |
||

151 | node_clock = Clock_predef.ck_bin_univ; |
||

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

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

154 | node_locals= []; |
||

155 | node_gencalls = []; |
||

156 | node_checks = []; |
||

157 | node_asserts = []; |
||

158 | node_stmts= []; |
||

159 | node_dec_stateless = false; |
||

160 | node_stateless = Some false; |
||

161 | node_spec = None; |
||

162 | node_annot = []; } |
||

163 | |||

164 | fc476249 | Teme | (*let arrow_top_decl = |

165 | e2068500 | Temesghen Kahsai | { |

166 | top_decl_desc = Node arrow_desc; |
||

167 | top_decl_owner = Version.include_path; |
||

168 | top_decl_itf = false; |
||

169 | top_decl_loc = Location.dummy_loc |
||

170 | fc476249 | Teme | }*) |

171 | |||

172 | let arrow_top_decl = |
||

173 | { |
||

174 | top_decl_desc = Node arrow_desc; |
||

175 | top_decl_owner = !Options.include_dir; |
||

176 | top_decl_itf = false; |
||

177 | top_decl_loc = Location.dummy_loc |
||

178 | e2068500 | Temesghen Kahsai | } |

179 | |||

180 | fc476249 | Teme | |

181 | 3b2bd83d | Teme | let mk_val v t = { value_desc = v; |

182 | value_type = t; |
||

183 | value_annot = None } |
||

184 | |||

185 | e2068500 | Temesghen Kahsai | let arrow_machine = |

186 | let state = "_first" in |
||

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

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

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

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

191 | 3b2bd83d | Teme | let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in |

192 | let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *) |
||

193 | e2068500 | Temesghen Kahsai | { |

194 | mname = arrow_desc; |
||

195 | mmemory = [var_state]; |
||

196 | mcalls = []; |
||

197 | minstances = []; |
||

198 | 3b2bd83d | Teme | minit = [MStateAssign(var_state, cst true)]; |

199 | e2068500 | Temesghen Kahsai | mstatic = []; |

200 | 3b2bd83d | Teme | mconst = []; |

201 | e2068500 | Temesghen Kahsai | mstep = { |

202 | step_inputs = arrow_desc.node_inputs; |
||

203 | step_outputs = arrow_desc.node_outputs; |
||

204 | step_locals = []; |
||

205 | step_checks = []; |
||

206 | 3b2bd83d | Teme | step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool) |

207 | [MStateAssign(var_state, cst false); |
||

208 | MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)] |
||

209 | [MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)] ]; |
||

210 | step_asserts = []; |
||

211 | }; |
||

212 | mspec = None; |
||

213 | mannot = []; |
||

214 | } |
||

215 | |||

216 | let empty_desc = |
||

217 | { |
||

218 | node_id = arrow_id; |
||

219 | node_type = Types.bottom; |
||

220 | node_clock = Clocks.bottom; |
||

221 | node_inputs= []; |
||

222 | node_outputs= []; |
||

223 | node_locals= []; |
||

224 | node_gencalls = []; |
||

225 | node_checks = []; |
||

226 | node_asserts = []; |
||

227 | node_stmts= []; |
||

228 | node_dec_stateless = true; |
||

229 | node_stateless = Some true; |
||

230 | node_spec = None; |
||

231 | node_annot = []; } |
||

232 | |||

233 | let empty_machine = |
||

234 | { |
||

235 | mname = empty_desc; |
||

236 | mmemory = []; |
||

237 | mcalls = []; |
||

238 | minstances = []; |
||

239 | minit = []; |
||

240 | mstatic = []; |
||

241 | mconst = []; |
||

242 | mstep = { |
||

243 | step_inputs = []; |
||

244 | step_outputs = []; |
||

245 | step_locals = []; |
||

246 | step_checks = []; |
||

247 | step_instrs = []; |
||

248 | e2068500 | Temesghen Kahsai | step_asserts = []; |

249 | }; |
||

250 | mspec = None; |
||

251 | mannot = []; |
||

252 | } |
||

253 | |||

254 | let new_instance = |
||

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

256 | fun caller callee tag -> |
||

257 | begin |
||

258 | let o = |
||

259 | if Stateless.check_node callee then |
||

260 | node_name callee |
||

261 | else |
||

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

263 | let o = |
||

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

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

266 | else o in |
||

267 | o |
||

268 | end |
||

269 | |||

270 | |||

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

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

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

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

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

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

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

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

279 | let var_id = get_node_var id node in |
||

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

281 | 3b2bd83d | Teme | then mk_val (StateVar var_id) var_id.var_type |

282 | else mk_val (LocalVar var_id) var_id.var_type |
||

283 | e2068500 | Temesghen Kahsai | with Not_found -> |

284 | try (* id is a constant *) |
||

285 | 3b2bd83d | Teme | let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in |

286 | mk_val (LocalVar vdecl) vdecl.var_type |
||

287 | e2068500 | Temesghen Kahsai | with Not_found -> |

288 | (* id is a tag *) |
||

289 | 3b2bd83d | Teme | (* DONE construire une liste des enum declarรฉs et alors chercher dedans la liste |

290 | qui contient id *) |
||

291 | try |
||

292 | let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in |
||

293 | mk_val (Cst (Const_tag id)) (Type_predef.type_const typ) |
||

294 | with Not_found -> (Format.eprintf "internal error: Machine_code.translate_ident %s" id; |
||

295 | assert false) |
||

296 | e2068500 | Temesghen Kahsai | |

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

298 | match (Clocks.repr ck).cdesc with |
||

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

300 | let id = Clocks.const_of_carrier cr in |
||

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

302 | [l, [inst]] )) |
||

303 | | _ -> inst |
||

304 | |||

305 | let rec join_branches hl1 hl2 = |
||

306 | match hl1, hl2 with |
||

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

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

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

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

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

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

313 | |||

314 | and join_guards inst1 insts2 = |
||

315 | match inst1, insts2 with |
||

316 | | _ , [] -> |
||

317 | [inst1] |
||

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

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

320 | :: q |
||

321 | | _ -> inst1 :: insts2 |
||

322 | |||

323 | let join_guards_list insts = |
||

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

325 | |||

326 | (* specialize predefined (polymorphic) operators |
||

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

328 | is preserved *) |
||

329 | let specialize_to_c expr = |
||

330 | match expr.expr_desc with |
||

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

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

333 | then let id = |
||

334 | match id with |
||

335 | | "=" -> "equi" |
||

336 | | "!=" -> "xor" |
||

337 | | _ -> id in |
||

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

339 | else expr |
||

340 | | _ -> expr |
||

341 | |||

342 | let specialize_op expr = |
||

343 | match !Options.output with |
||

344 | | "C" -> specialize_to_c expr |
||

345 | | _ -> expr |
||

346 | |||

347 | 3b2bd83d | Teme | let rec translate_expr node ((m, si, j, d, s) as args) expr = |

348 | e2068500 | Temesghen Kahsai | let expr = specialize_op expr in |

349 | 3b2bd83d | Teme | let value_desc = |

350 | match expr.expr_desc with |
||

351 | | Expr_const v -> Cst v |
||

352 | | Expr_ident x -> (translate_ident node args x).value_desc |
||

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

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

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

356 | | Expr_tuple _ |
||

357 | | Expr_arrow _ |
||

358 | | Expr_fby _ |
||

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

360 | | Expr_when (e1, _, _) -> (translate_expr node args e1).value_desc |
||

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

362 | | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr -> |
||

363 | let nd = node_from_name id in |
||

364 | Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e)) |
||

365 | (*| Expr_ite (g,t,e) -> ( |
||

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

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

368 | backends. *) |
||

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

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

371 | | "C" | "java" | _ -> |
||

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

373 | )*) |
||

374 | | _ -> raise NormalizationError |
||

375 | in |
||

376 | mk_val value_desc expr.expr_type |
||

377 | e2068500 | Temesghen Kahsai | |

378 | let translate_guard node args expr = |
||

379 | match expr.expr_desc with |
||

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

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

382 | |||

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

384 | match expr.expr_desc with |
||

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

386 | 3b2bd83d | Teme | conditional g |

387 | [translate_act node args (y, t)] |
||

388 | e2068500 | Temesghen Kahsai | [translate_act node args (y, e)] |

389 | 3b2bd83d | Teme | | Expr_merge (x, hl) -> MBranch (translate_ident node args x, |

390 | List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl) |
||

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

392 | e2068500 | Temesghen Kahsai | |

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

394 | match r with |
||

395 | | None -> [] |
||

396 | | Some r -> let g = translate_guard node args r in |
||

397 | 3b2bd83d | Teme | [control_on_clock node args c (conditional g [MReset i] [MNoReset i])] |

398 | e2068500 | Temesghen Kahsai | |

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

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

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

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

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

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

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

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

407 | (m, |
||

408 | MReset o :: si, |
||

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

410 | d, |
||

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

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

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

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

415 | si, |
||

416 | j, |
||

417 | d, |
||

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

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

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

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

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

423 | j, |
||

424 | d, |
||

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

426 | |||

427 | 3b2bd83d | Teme | | p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) -> |

428 | e2068500 | Temesghen Kahsai | let var_p = List.map (fun v -> get_node_var v node) p in |

429 | let el = expr_list_of_expr arg in |
||

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

431 | let node_f = node_from_name f in |
||

432 | let call_f = |
||

433 | node_f, |
||

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

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

436 | let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in |
||

437 | let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in |
||

438 | (*Clocks.new_var true in |
||

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

440 | Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*) |
||

441 | (m, |
||

442 | (if Stateless.check_node node_f then si else MReset o :: si), |
||

443 | Utils.IMap.add o call_f j, |
||

444 | d, |
||

445 | (if Stateless.check_node node_f |
||

446 | then [] |
||

447 | else reset_instance node args o r call_ck) @ |
||

448 | (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s) |
||

449 | 3b2bd83d | Teme | (* |

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

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

452 | backends. *) |
||

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

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

455 | -> |
||

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

457 | (m, |
||

458 | si, |
||

459 | j, |
||

460 | d, |
||

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

462 | (MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s) |
||

463 | ) |
||

464 | |||

465 | 3b2bd83d | Teme | *) |

466 | e2068500 | Temesghen Kahsai | | [x], _ -> ( |

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

468 | (m, si, j, d, |
||

469 | control_on_clock |
||

470 | node |
||

471 | args |
||

472 | eq.eq_rhs.expr_clock |
||

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

474 | ) |
||

475 | ) |
||

476 | | _ -> |
||

477 | begin |
||

478 | 3b2bd83d | Teme | Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq; |

479 | e2068500 | Temesghen Kahsai | assert false |

480 | end |
||

481 | |||

482 | let find_eq xl eqs = |
||

483 | let rec aux accu eqs = |
||

484 | match eqs with |
||

485 | | [] -> |
||

486 | begin |
||

487 | Format.eprintf "Looking for variables %a in the following equations@.%a@." |
||

488 | (Utils.fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) xl |
||

489 | Printers.pp_node_eqs eqs; |
||

490 | assert false |
||

491 | end |
||

492 | | hd::tl -> |
||

493 | if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl |
||

494 | in |
||

495 | aux [] eqs |
||

496 | |||

497 | (* Sort the set of equations of node [nd] according |
||

498 | to the computed schedule [sch] |
||

499 | *) |
||

500 | let sort_equations_from_schedule nd sch = |
||

501 | 3b2bd83d | Teme | (* Format.eprintf "%s schedule: %a@." *) |

502 | (* nd.node_id *) |
||

503 | (* (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *) |
||

504 | e2068500 | Temesghen Kahsai | let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in |

505 | let eqs_rev, remainder = |
||

506 | List.fold_left |
||

507 | (fun (accu, node_eqs_remainder) vl -> |
||

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

509 | then |
||

510 | (accu, node_eqs_remainder) |
||

511 | else |
||

512 | let eq_v, remainder = find_eq vl node_eqs_remainder in |
||

513 | eq_v::accu, remainder |
||

514 | ) |
||

515 | ([], split_eqs) |
||

516 | sch |
||

517 | in |
||

518 | begin |
||

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

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

521 | Printers.pp_node_eqs remainder |
||

522 | Printers.pp_node_eqs (get_node_eqs nd); |
||

523 | assert false); |
||

524 | List.rev eqs_rev |
||

525 | end |
||

526 | |||

527 | let constant_equations nd = |
||

528 | List.fold_right (fun vdecl eqs -> |
||

529 | if vdecl.var_dec_const |
||

530 | then |
||

531 | { eq_lhs = [vdecl.var_id]; |
||

532 | eq_rhs = Utils.desome vdecl.var_dec_value; |
||

533 | eq_loc = vdecl.var_loc |
||

534 | } :: eqs |
||

535 | else eqs) |
||

536 | nd.node_locals [] |
||

537 | |||

538 | let translate_eqs node args eqs = |
||

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

540 | |||

541 | let translate_decl nd sch = |
||

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

543 | |||

544 | let sorted_eqs = sort_equations_from_schedule nd sch in |
||

545 | let constant_eqs = constant_equations nd in |
||

546 | |||

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

548 | (* memories, init instructions, node calls, local variables (including memories), step instrs *) |
||

549 | let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in |
||

550 | assert (ISet.is_empty m0); |
||

551 | assert (init0 = []); |
||

552 | assert (Utils.IMap.is_empty j0); |
||

553 | a1daa793 | Temesghen Kahsai | let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, []) sorted_eqs in |

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

555 | { |
||

556 | mname = nd; |
||

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

558 | mcalls = mmap; |
||

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

560 | minit = init; |
||

561 | mconst = s0; |
||

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

563 | mstep = { |
||

564 | step_inputs = nd.node_inputs; |
||

565 | step_outputs = nd.node_outputs; |
||

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

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

568 | step_instrs = ( |
||

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

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

571 | backends. *) |
||

572 | 3b2bd83d | Teme | (*match !Options.output with |

573 | e2068500 | Temesghen Kahsai | | "horn" -> s |

574 | 3b2bd83d | Teme | | "C" | "java" | _ ->*) join_guards_list s |

575 | e2068500 | Temesghen Kahsai | ); |

576 | step_asserts = |
||

577 | let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in |
||

578 | List.map (translate_expr nd init_args) exprl |
||

579 | ; |
||

580 | }; |
||

581 | mspec = nd.node_spec; |
||

582 | mannot = nd.node_annot; |
||

583 | } |
||

584 | |||

585 | (** takes the global declarations and the scheduling associated to each node *) |
||

586 | let translate_prog decls node_schs = |
||

587 | let nodes = get_nodes decls in |
||

588 | List.map |
||

589 | (fun decl -> |
||

590 | let node = node_of_top decl in |
||

591 | let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in |
||

592 | translate_decl node sch |
||

593 | ) nodes |
||

594 | |||

595 | let get_machine_opt name machines = |
||

596 | List.fold_left |
||

597 | (fun res m -> |
||

598 | match res with |
||

599 | | Some _ -> res |
||

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

601 | None machines |
||

602 | |||

603 | let get_const_assign m id = |
||

604 | try |
||

605 | match (List.find (fun instr -> match instr with MLocalAssign (v, _) -> v == id | _ -> false) m.mconst) with |
||

606 | | MLocalAssign (_, e) -> e |
||

607 | | _ -> assert false |
||

608 | with Not_found -> assert false |
||

609 | |||

610 | |||

611 | 3b2bd83d | Teme | let value_of_ident loc m id = |

612 | e2068500 | Temesghen Kahsai | (* is is a state var *) |

613 | try |
||

614 | 3b2bd83d | Teme | let v = List.find (fun v -> v.var_id = id) m.mmemory |

615 | in mk_val (StateVar v) v.var_type |
||

616 | e2068500 | Temesghen Kahsai | with Not_found -> |

617 | 3b2bd83d | Teme | try (* id is a node var *) |

618 | let v = get_node_var id m.mname |
||

619 | in mk_val (LocalVar v) v.var_type |
||

620 | e2068500 | Temesghen Kahsai | with Not_found -> |

621 | try (* id is a constant *) |
||

622 | 3b2bd83d | Teme | let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)) |

623 | in mk_val (LocalVar c) c.var_type |
||

624 | e2068500 | Temesghen Kahsai | with Not_found -> |

625 | (* id is a tag *) |
||

626 | 3b2bd83d | Teme | let t = Const_tag id |

627 | in mk_val (Cst t) (Typing.type_const loc t) |
||

628 | |||

629 | (* type of internal fun used in dimension expression *) |
||

630 | let type_of_value_appl f args = |
||

631 | if List.mem f Basic_library.arith_funs |
||

632 | then (List.hd args).value_type |
||

633 | else Type_predef.type_bool |
||

634 | e2068500 | Temesghen Kahsai | |

635 | let rec value_of_dimension m dim = |
||

636 | match dim.Dimension.dim_desc with |
||

637 | 3b2bd83d | Teme | | Dimension.Dbool b -> |

638 | mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool |
||

639 | | Dimension.Dint i -> |
||

640 | mk_val (Cst (Const_int i)) Type_predef.type_int |
||

641 | | Dimension.Dident v -> value_of_ident dim.Dimension.dim_loc m v |
||

642 | | Dimension.Dappl (f, args) -> |
||

643 | let vargs = List.map (value_of_dimension m) args |
||

644 | in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) |
||

645 | | Dimension.Dite (i, t, e) -> |
||

646 | (match List.map (value_of_dimension m) [i; t; e] with |
||

647 | | [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type |
||

648 | | _ -> assert false) |
||

649 | e2068500 | Temesghen Kahsai | | Dimension.Dlink dim' -> value_of_dimension m dim' |

650 | | _ -> assert false |
||

651 | |||

652 | let rec dimension_of_value value = |
||

653 | 3b2bd83d | Teme | match value.value_desc with |

654 | e2068500 | Temesghen Kahsai | | Cst (Const_tag t) when t = Corelang.tag_true -> Dimension.mkdim_bool Location.dummy_loc true |

655 | | Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool Location.dummy_loc false |
||

656 | | Cst (Const_int i) -> Dimension.mkdim_int Location.dummy_loc i |
||

657 | | LocalVar v -> Dimension.mkdim_ident Location.dummy_loc v.var_id |
||

658 | | Fun (f, args) -> Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args) |
||

659 | | _ -> assert false |
||

660 | |||

661 | (* Local Variables: *) |
||

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

663 | (* End: *) |