## lustrec / src / machine_code.ml @ 63f10e14

History | View | Annotate | Download (25 KB)

1 |
(********************************************************************) |
---|---|

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 |
match v.value_desc with |

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

27 |
| 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 |
| MNoReset i -> Format.fprintf fmt "noreset %s" i |

40 |
| 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 |
| MComment s -> Format.pp_print_string fmt s |

50 | |

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 machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory |

82 | |

83 |
let pp_step fmt s = |

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

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

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

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

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

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

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

91 | |

92 | |

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

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

95 |
(node_name node) |

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

97 | |

98 |
let pp_machine fmt m = |

99 |
Format.fprintf fmt |

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

101 |
m.mname.node_id |

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

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

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

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

106 |
pp_step m.mstep |

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

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

109 | |

110 |
let rec is_const_value v = |

111 |
match v.value_desc with |

112 |
| Cst _ -> true |

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

114 |
| _ -> false |

115 | |

116 |
(* Returns the declared stateless status and the computed one. *) |

117 |
let get_stateless_status m = |

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

119 | |

120 |
let is_input m id = |

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

122 | |

123 |
let is_output m id = |

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

125 | |

126 |
let is_memory m id = |

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

128 | |

129 |
let conditional c t e = |

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

131 | |

132 |
let dummy_var_decl name typ = |

133 |
{ |

134 |
var_id = name; |

135 |
var_orig = false; |

136 |
var_dec_type = dummy_type_dec; |

137 |
var_dec_clock = dummy_clock_dec; |

138 |
var_dec_const = false; |

139 |
var_dec_value = None; |

140 |
var_type = typ; |

141 |
var_clock = Clocks.new_ck Clocks.Cvar true; |

142 |
var_loc = Location.dummy_loc |

143 |
} |

144 | |

145 |
let arrow_id = "_arrow" |

146 | |

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

148 | |

149 |
let arrow_desc = |

150 |
{ |

151 |
node_id = arrow_id; |

152 |
node_type = Type_predef.type_bin_poly_op; |

153 |
node_clock = Clock_predef.ck_bin_univ; |

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

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

156 |
node_locals= []; |

157 |
node_gencalls = []; |

158 |
node_checks = []; |

159 |
node_asserts = []; |

160 |
node_stmts= []; |

161 |
node_dec_stateless = false; |

162 |
node_stateless = Some false; |

163 |
node_spec = None; |

164 |
node_annot = []; } |

165 | |

166 |
let arrow_top_decl = |

167 |
{ |

168 |
top_decl_desc = Node arrow_desc; |

169 |
top_decl_owner = !Options.include_dir; |

170 |
top_decl_itf = false; |

171 |
top_decl_loc = Location.dummy_loc |

172 |
} |

173 | |

174 |
let mk_val v t = { value_desc = v; |

175 |
value_type = t; |

176 |
value_annot = None } |

177 | |

178 |
let arrow_machine = |

179 |
let state = "_first" in |

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

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

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

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

184 |
let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in |

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

186 |
{ |

187 |
mname = arrow_desc; |

188 |
mmemory = [var_state]; |

189 |
mcalls = []; |

190 |
minstances = []; |

191 |
minit = [MStateAssign(var_state, cst true)]; |

192 |
mstatic = []; |

193 |
mconst = []; |

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 (mk_val (StateVar var_state) Type_predef.type_bool) |

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

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

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

203 |
step_asserts = []; |

204 |
}; |

205 |
mspec = None; |

206 |
mannot = []; |

207 |
} |

208 | |

209 |
let empty_desc = |

210 |
{ |

211 |
node_id = arrow_id; |

212 |
node_type = Types.bottom; |

213 |
node_clock = Clocks.bottom; |

214 |
node_inputs= []; |

215 |
node_outputs= []; |

216 |
node_locals= []; |

217 |
node_gencalls = []; |

218 |
node_checks = []; |

219 |
node_asserts = []; |

220 |
node_stmts= []; |

221 |
node_dec_stateless = true; |

222 |
node_stateless = Some true; |

223 |
node_spec = None; |

224 |
node_annot = []; } |

225 | |

226 |
let empty_machine = |

227 |
{ |

228 |
mname = empty_desc; |

229 |
mmemory = []; |

230 |
mcalls = []; |

231 |
minstances = []; |

232 |
minit = []; |

233 |
mstatic = []; |

234 |
mconst = []; |

235 |
mstep = { |

236 |
step_inputs = []; |

237 |
step_outputs = []; |

238 |
step_locals = []; |

239 |
step_checks = []; |

240 |
step_instrs = []; |

241 |
step_asserts = []; |

242 |
}; |

243 |
mspec = None; |

244 |
mannot = []; |

245 |
} |

246 | |

247 |
let new_instance = |

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

249 |
fun caller callee tag -> |

250 |
begin |

251 |
let o = |

252 |
if Stateless.check_node callee then |

253 |
node_name callee |

254 |
else |

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

256 |
let o = |

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

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

259 |
else o in |

260 |
o |

261 |
end |

262 | |

263 | |

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

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

266 |
(* si : initialization instructions *) |

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

268 |
(* d : local variables *) |

269 |
(* s : step instructions *) |

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

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

272 |
let var_id = get_node_var id node in |

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

274 |
then mk_val (StateVar var_id) var_id.var_type |

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

276 |
with Not_found -> |

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

278 |
let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in |

279 |
mk_val (LocalVar vdecl) vdecl.var_type |

280 |
with Not_found -> |

281 |
(* id is a tag *) |

282 |
(* DONE construire une liste des enum declarés et alors chercher dedans la liste |

283 |
qui contient id *) |

284 |
try |

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

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

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

288 |
assert false) |

289 | |

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

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

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

293 |
let id = Clocks.const_of_carrier cr in |

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

295 |
[l, [inst]] )) |

296 |
| _ -> inst |

297 | |

298 |
let rec join_branches hl1 hl2 = |

299 |
match hl1, hl2 with |

300 |
| [] , _ -> hl2 |

301 |
| _ , [] -> hl1 |

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

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

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

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

306 | |

307 |
and join_guards inst1 insts2 = |

308 |
match inst1, insts2 with |

309 |
| _ , [] -> |

310 |
[inst1] |

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

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

313 |
:: q |

314 |
| _ -> inst1 :: insts2 |

315 | |

316 |
let join_guards_list insts = |

317 |
List.fold_right join_guards insts [] |

318 | |

319 |
(* specialize predefined (polymorphic) operators |

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

321 |
is preserved *) |

322 |
let specialize_to_c expr = |

323 |
match expr.expr_desc with |

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

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

326 |
then let id = |

327 |
match id with |

328 |
| "=" -> "equi" |

329 |
| "!=" -> "xor" |

330 |
| _ -> id in |

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

332 |
else expr |

333 |
| _ -> expr |

334 | |

335 |
let specialize_op expr = |

336 |
match !Options.output with |

337 |
| "C" -> specialize_to_c expr |

338 |
| _ -> expr |

339 | |

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

341 |
let expr = specialize_op expr in |

342 |
let value_desc = |

343 |
match expr.expr_desc with |

344 |
| Expr_const v -> Cst v |

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

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

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

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

349 |
| Expr_tuple _ |

350 |
| Expr_arrow _ |

351 |
| Expr_fby _ |

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

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

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

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

356 |
let nd = node_from_name id in |

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

358 |
| Expr_ite (g,t,e) -> ( |

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

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

361 |
backends. *) |

362 |
match !Options.output with |

363 |
| "horn" -> |

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

365 |
| "C" | "java" | _ -> |

366 |
(Format.eprintf "Normalization error for backend %s: %a@." |

367 |
!Options.output |

368 |
Printers.pp_expr expr; |

369 |
raise NormalizationError) |

370 |
) |

371 |
| _ -> raise NormalizationError |

372 |
in |

373 |
mk_val value_desc expr.expr_type |

374 | |

375 |
let translate_guard node args expr = |

376 |
match expr.expr_desc with |

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

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

379 | |

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

381 |
match expr.expr_desc with |

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

383 |
conditional g |

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

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

386 |
| Expr_merge (x, hl) -> MBranch (translate_ident node args x, |

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

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

389 | |

390 |
let reset_instance node args i r c = |

391 |
match r with |

392 |
| None -> [] |

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

394 |
[control_on_clock node args c (conditional g [MReset i] [MNoReset i])] |

395 | |

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

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

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

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

400 |
let var_x = get_node_var x node in |

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

402 |
let c1 = translate_expr node args e1 in |

403 |
let c2 = translate_expr node args e2 in |

404 |
(m, |

405 |
MReset o :: si, |

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

407 |
d, |

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

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

410 |
let var_x = get_node_var x node in |

411 |
(ISet.add var_x m, |

412 |
si, |

413 |
j, |

414 |
d, |

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

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

417 |
let var_x = get_node_var x node in |

418 |
(ISet.add var_x m, |

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

420 |
j, |

421 |
d, |

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

423 | |

424 |
| p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) -> |

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

426 |
let el = expr_list_of_expr arg in |

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

428 |
let node_f = node_from_name f in |

429 |
let call_f = |

430 |
node_f, |

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

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

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

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

435 |
(*Clocks.new_var true in |

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

437 |
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;*) |

438 |
(m, |

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

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

441 |
d, |

442 |
(if Stateless.check_node node_f |

443 |
then [] |

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

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

446 |
(* |

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

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

449 |
backends. *) |

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

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

452 |
-> |

453 |
let var_x = get_node_var x node in |

454 |
(m, |

455 |
si, |

456 |
j, |

457 |
d, |

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

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

460 |
) |

461 | |

462 |
*) |

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

464 |
let var_x = get_node_var x node in |

465 |
(m, si, j, d, |

466 |
control_on_clock |

467 |
node |

468 |
args |

469 |
eq.eq_rhs.expr_clock |

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

471 |
) |

472 |
) |

473 |
| _ -> |

474 |
begin |

475 |
Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq; |

476 |
assert false |

477 |
end |

478 | |

479 |
let find_eq xl eqs = |

480 |
let rec aux accu eqs = |

481 |
match eqs with |

482 |
| [] -> |

483 |
begin |

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

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

486 |
Printers.pp_node_eqs eqs; |

487 |
assert false |

488 |
end |

489 |
| hd::tl -> |

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

491 |
in |

492 |
aux [] eqs |

493 | |

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

495 |
to the computed schedule [sch] |

496 |
*) |

497 |
let sort_equations_from_schedule nd sch = |

498 |
(* Format.eprintf "%s schedule: %a@." *) |

499 |
(* nd.node_id *) |

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

501 |
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in |

502 |
let eqs_rev, remainder = |

503 |
List.fold_left |

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

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

506 |
then |

507 |
(accu, node_eqs_remainder) |

508 |
else |

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

510 |
eq_v::accu, remainder |

511 |
) |

512 |
([], split_eqs) |

513 |
sch |

514 |
in |

515 |
begin |

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

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

518 |
Printers.pp_node_eqs remainder |

519 |
Printers.pp_node_eqs (get_node_eqs nd); |

520 |
assert false); |

521 |
List.rev eqs_rev |

522 |
end |

523 | |

524 |
let constant_equations nd = |

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

526 |
if vdecl.var_dec_const |

527 |
then |

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

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

530 |
eq_loc = vdecl.var_loc |

531 |
} :: eqs |

532 |
else eqs) |

533 |
nd.node_locals [] |

534 | |

535 |
let translate_eqs node args eqs = |

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

537 | |

538 |
let translate_decl nd sch = |

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

540 | |

541 |
let sorted_eqs = sort_equations_from_schedule nd sch in |

542 |
let constant_eqs = constant_equations nd in |

543 | |

544 |
(* In case of non functional backend (eg. C), additional local variables have |

545 |
to be declared for each assert *) |

546 |
let new_locals, assert_instrs, nd_node_asserts = |

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

548 |
if Corelang.functional_backend () then |

549 |
[], [], exprl |

550 |
else (* Each assert(e) is associated to a fresh variable v and declared as |

551 |
v=e; assert (v); *) |

552 |
let _, vars, eql, assertl = |

553 |
List.fold_left (fun (i, vars, eqlist, assertlist) expr -> |

554 |
let loc = expr.expr_loc in |

555 |
let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in |

556 |
let assert_var = |

557 |
mkvar_decl |

558 |
loc |

559 |
~orig:false (* fresh var *) |

560 |
(var_id, |

561 |
mktyp loc Tydec_bool, |

562 |
mkclock loc Ckdec_any, |

563 |
false, (* not a constant *) |

564 |
None (* no default value *) |

565 |
) |

566 |
in |

567 |
assert_var.var_type <- Types.new_ty (Types.Tbool); |

568 |
let eq = mkeq loc ([var_id], expr) in |

569 |
(i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist) |

570 |
) (1, [], [], []) exprl |

571 |
in |

572 |
vars, eql, assertl |

573 |
in |

574 |
let locals_list = nd.node_locals @ new_locals in |

575 | |

576 |
let nd = { nd with node_locals = locals_list } in |

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

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

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

580 |
assert (ISet.is_empty m0); |

581 |
assert (init0 = []); |

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

583 |
let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, []) (sorted_eqs@assert_instrs) in |

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

585 |
{ |

586 |
mname = nd; |

587 |
mmemory = ISet.elements m; |

588 |
mcalls = mmap; |

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

590 |
minit = init; |

591 |
mconst = s0; |

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

593 |
mstep = { |

594 |
step_inputs = nd.node_inputs; |

595 |
step_outputs = nd.node_outputs; |

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

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

598 |
step_instrs = ( |

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

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

601 |
backends. *) |

602 |
(*match !Options.output with |

603 |
| "horn" -> s |

604 |
| "C" | "java" | _ ->*) join_guards_list s |

605 |
); |

606 |
step_asserts = List.map (translate_expr nd init_args) nd_node_asserts; |

607 |
}; |

608 |
mspec = nd.node_spec; |

609 |
mannot = nd.node_annot; |

610 |
} |

611 | |

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

613 |
let translate_prog decls node_schs = |

614 |
let nodes = get_nodes decls in |

615 |
List.map |

616 |
(fun decl -> |

617 |
let node = node_of_top decl in |

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

619 |
translate_decl node sch |

620 |
) nodes |

621 | |

622 |
let get_machine_opt name machines = |

623 |
List.fold_left |

624 |
(fun res m -> |

625 |
match res with |

626 |
| Some _ -> res |

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

628 |
None machines |

629 | |

630 |
let get_const_assign m id = |

631 |
try |

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

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

634 |
| _ -> assert false |

635 |
with Not_found -> assert false |

636 | |

637 | |

638 |
let value_of_ident loc m id = |

639 |
(* is is a state var *) |

640 |
try |

641 |
let v = List.find (fun v -> v.var_id = id) m.mmemory |

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

643 |
with Not_found -> |

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

645 |
let v = get_node_var id m.mname |

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

647 |
with Not_found -> |

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

649 |
let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)) |

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

651 |
with Not_found -> |

652 |
(* id is a tag *) |

653 |
let t = Const_tag id |

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

655 | |

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

657 |
let type_of_value_appl f args = |

658 |
if List.mem f Basic_library.arith_funs |

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

660 |
else Type_predef.type_bool |

661 | |

662 |
let rec value_of_dimension m dim = |

663 |
match dim.Dimension.dim_desc with |

664 |
| Dimension.Dbool b -> |

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

666 |
| Dimension.Dint i -> |

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

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

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

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

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

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

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

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

675 |
| _ -> assert false) |

676 |
| Dimension.Dlink dim' -> value_of_dimension m dim' |

677 |
| _ -> assert false |

678 | |

679 |
let rec dimension_of_value value = |

680 |
match value.value_desc with |

681 |
| Cst (Const_tag t) when t = Corelang.tag_true -> Dimension.mkdim_bool Location.dummy_loc true |

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

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

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

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

686 |
| _ -> assert false |

687 | |

688 |
(* Local Variables: *) |

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

690 |
(* End: *) |