Revision 6d1693b9
Added by LĂ©lio Brun 7 months ago
src/machine_code.ml  

42  42 
} 
43  43  
44  44  
45 
let build_env locals non_locals = 

46 
let all = VSet.union locals non_locals in 

47 
{ 

48 
is_local = (fun id > VSet.exists (fun v > v.var_id = id) locals); 

49 
get_var = (fun id > try VSet.get id all with Not_found > 

45 
let build_env inputs locals outputs = 

46 
let all = List.sort_uniq VDeclModule.compare (locals @ inputs @ outputs) in 

47 
{ is_local = (fun id > List.exists (fun v > v.var_id = id) locals); 

48 
get_var = (fun id > try List.find (fun v > v.var_id = id) all with Not_found > 

50  49 
(* Format.eprintf "Impossible to find variable %s in set %a@.@?" 
51  50 
* id 
52  51 
* VSet.pp all; *) 
...  ...  
64  63 
(* id is a var that shall be visible here , ie. in vars *) 
65  64 
try 
66  65 
let var_id = env.get_var id in 
67 
mk_val (Var var_id) var_id.var_type


66 
vdecl_to_val var_id


68  67 
with Not_found > 
69  68  
70  69 
(* id is a constant *) 
...  ...  
72  71 
let vdecl = (Corelang.var_decl_of_const 
73  72 
(const_of_top (Hashtbl.find Corelang.consts_table id))) 
74  73 
in 
75 
mk_val (Var vdecl) vdecl.var_type


74 
vdecl_to_val vdecl


76  75 
with Not_found > 
77  76  
78  77 
(* id is a tag, getting its type in the list of declared enums *) 
79  78 
try 
80 
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in 

81 
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ) 

79 
id_to_tag id 

82  80 
with Not_found > 
83  81 
Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id; 
84  82 
assert false 
...  ...  
147  145 
let rec translate_act env (y, expr) = 
148  146 
let translate_act = translate_act env in 
149  147 
let translate_guard = translate_guard env in 
150 
let translate_ident = translate_ident env in


148 
(* let translate_ident = translate_ident env in *)


151  149 
let translate_expr = translate_expr env in 
152  150 
let lustre_eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in 
153  151 
match expr.expr_desc with 
154  152 
 Expr_ite (c, t, e) > 
155 
mk_conditional ~lustre_eq 

156 
(translate_guard c) 

157 
[translate_act (y, t)] 

158 
[translate_act (y, e)] 

153 
let c = translate_guard c in 

154 
let t, spec_t = translate_act (y, t) in 

155 
let e, spec_e = translate_act (y, e) in 

156 
mk_conditional ~lustre_eq c [t] [e], 

157 
mk_conditional_tr c spec_t spec_e 

159  158 
 Expr_merge (x, hl) > 
160 
mk_branch ~lustre_eq 

161 
(translate_ident x) 

162 
(List.map (fun (t, h) > t, [translate_act (y, h)]) hl) 

159 
let var_x = env.get_var x in 

160 
let hl, spec_hl = List.(split (map (fun (t, h) > 

161 
let h, spec_h = translate_act (y, h) in 

162 
(t, [h]), (t, spec_h)) 

163 
hl)) in 

164 
mk_branch ~lustre_eq var_x hl, 

165 
mk_branch_tr var_x spec_hl 

163  166 
 _ > 
164 
mk_assign ~lustre_eq y (translate_expr expr) 

167 
let e = translate_expr expr in 

168 
mk_assign ~lustre_eq y e, 

169 
mk_assign_tr y e 

170  
171 
let get_memory env mems eq = match eq.eq_lhs, eq.eq_rhs.expr_desc with 

172 
 ([x], Expr_pre _  [x], Expr_fby _) when env.is_local x > 

173 
let var_x = env.get_var x in 

174 
VSet.add var_x mems 

175 
 _ > mems 

176  
177 
let get_memories env = 

178 
List.fold_left (get_memory env) VSet.empty 

165  179  
166  180 
(* Datastructure updated while visiting equations *) 
167  181 
type machine_ctx = { 
168 
(* machine name *) 

169 
id: ident; 

170 
(* Memories *) 

171 
m: VSet.t; 

172  182 
(* Reset instructions *) 
173  183 
si: instr_t list; 
174  184 
(* Instances *) 
...  ...  
177  187 
s: instr_t list; 
178  188 
(* Memory pack spec *) 
179  189 
mp: mc_formula_t list; 
180 
(* Clocked spec *) 

181 
c: mc_formula_t IMap.t; 

182  190 
(* Transition spec *) 
183 
t: mc_formula_t list;


191 
t: (var_decl list * var_decl list * var_decl list * mc_formula_t) list;


184  192 
} 
185  193  
186 
let ctx_init id = { 

187 
id; 

188 
m = VSet.empty; 

194 
let ctx_init = { 

189  195 
si = []; 
190  196 
j = IMap.empty; 
191  197 
s = []; 
192  198 
mp = []; 
193 
c = IMap.empty; 

194  199 
t = [] 
195  200 
} 
196  201  
197 
let ctx_dummy = ctx_init "" 

198  
199  202 
(****************************************************************) 
200  203 
(* Main function to translate equations into this machine context we 
201  204 
are building *) 
...  ...  
203  206  
204  207 
let mk_control v l inst = 
205  208 
mkinstr 
206 
True 

207 
(* (Imply (mk_clocked_on id vs, inst.instr_spec)) *) 

208 
(MBranch (v, [l, [inst]])) 

209 
(MBranch (vdecl_to_val v, [l, [inst]])) 

209  210  
210 
let control_on_clock env ctx ck spec inst =


211 
let rec aux (ck_ids, vs, ctx, spec, inst as acc) ck =


211 
let control_on_clock env ck inst =


212 
let rec aux (fspec, inst as acc) ck =


212  213 
match (Clocks.repr ck).cdesc with 
213  214 
 Con (ck, cr, l) > 
214  215 
let id = Clocks.const_of_carrier cr in 
215 
let v = translate_ident env id in 

216 
let ck_ids' = String.concat "_" ck_ids in 

217 
let id' = id ^ "_" ^ ck_ids' in 

218 
let ck_spec = mk_condition v l in 

219 
aux (id :: ck_ids, 

220 
v :: vs, 

221 
{ ctx with 

222 
c = IMap.add id ck_spec 

223 
(IMap.add id' (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c) 

224 
}, 

225 
Imply (mk_clocked_on id' (v :: vs), spec), 

226 
mk_control v l inst) ck 

216 
let v = env.get_var id in 

217 
aux ((fun spec > Imply (Equal (Var v, Tag l), fspec spec)), 

218 
mk_control v l inst) 

219 
ck 

227  220 
 _ > acc 
228  221 
in 
229 
let _, _, ctx, spec, inst = aux ([], [], ctx, spec, inst) ck in


230 
ctx, spec, inst


222 
let fspec, inst = aux ((fun spec > spec), inst) ck in


223 
fspec, inst


231  224  
232  225 
let reset_instance env i r c = 
233  226 
match r with 
234  227 
 Some r > 
235 
let _, _, inst = control_on_clock env ctx_dummy c True


228 
let _, inst = control_on_clock env c


236  229 
(mk_conditional 
237  230 
(translate_guard env r) 
238 
[mkinstr True (MReset i)]


239 
[mkinstr True (MNoReset i)]) in


231 
[mkinstr (MSetReset i)]


232 
[mkinstr (MNoReset i)]) in 

240  233 
[ inst ] 
241  234 
 None > [] 
242  235  
243  
244 
let translate_eq env ctx i eq = 

236 
let translate_eq env ctx id inputs locals outputs i eq = 

245  237 
let translate_expr = translate_expr env in 
246  238 
let translate_act = translate_act env in 
247 
let control_on_clock ck spec inst = 

248 
let ctx, _spec, inst = control_on_clock env ctx ck spec inst in 

239 
let locals_pi = Lustre_live.inter_live_i_with id (i1) locals in 

240 
let outputs_pi = Lustre_live.inter_live_i_with id (i1) outputs in 

241 
let locals_i = Lustre_live.inter_live_i_with id i locals in 

242 
let outputs_i = Lustre_live.inter_live_i_with id i outputs in 

243 
let pred_mp ctx a = 

244 
And [mk_memory_pack ~i:(i1) id; a] :: ctx.mp in 

245 
let pred_t ctx a = 

246 
(inputs, locals_i, outputs_i, 

247 
Exists 

248 
(Lustre_live.existential_vars id i eq (locals @ outputs), 

249 
And [ 

250 
mk_transition ~i:(i1) id 

251 
(vdecls_to_vals inputs) 

252 
(vdecls_to_vals locals_pi) 

253 
(vdecls_to_vals outputs_pi); 

254 
a 

255 
])) 

256 
:: ctx.t in 

257 
let control_on_clock ck inst spec_mp spec_t = 

258 
let fspec, inst = control_on_clock env ck inst in 

249  259 
{ ctx with 
250  260 
s = { inst with 
251 
instr_spec = mk_transition ~i ctx.id [] } :: ctx.s } 

261 
instr_spec = [ 

262 
mk_memory_pack ~i id; 

263 
mk_transition ~i id 

264 
(vdecls_to_vals inputs) 

265 
(vdecls_to_vals locals_i) 

266 
(vdecls_to_vals outputs_i) 

267 
] } 

268 
:: ctx.s; 

269 
mp = pred_mp ctx spec_mp; 

270 
t = pred_t ctx (fspec spec_t); 

271 
} 

252  272 
in 
253  273 
let reset_instance = reset_instance env in 
254 
let mkinstr' = mkinstr ~lustre_eq:eq True in


255 
let ctl ?(ck=eq.eq_rhs.expr_clock) spec instr =


256 
control_on_clock ck spec (mkinstr' instr) in


274 
let mkinstr' = mkinstr ~lustre_eq:eq in 

275 
let ctl ?(ck=eq.eq_rhs.expr_clock) instr spec_mp spec_t =


276 
control_on_clock ck (mkinstr' instr) spec_mp spec_t in


257  277  
258  278 
(* Format.eprintf "translate_eq %a with clock %a@." 
259  279 
Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) 
...  ...  
261  281 
 [x], Expr_arrow (e1, e2) > 
262  282 
let var_x = env.get_var x in 
263  283 
let td = Arrow.arrow_top_decl () in 
264 
let o = new_instance td eq.eq_rhs.expr_tag in


284 
let inst = new_instance td eq.eq_rhs.expr_tag in


265  285 
let c1 = translate_expr e1 in 
266  286 
let c2 = translate_expr e2 in 
287 
assert (c1.value_desc = Cst (Const_tag "true")); 

288 
assert (c2.value_desc = Cst (Const_tag "false")); 

267  289 
let ctx = ctl 
268 
(mk_transition (node_name td) []) 

269 
(MStep ([var_x], o, [c1;c2])) in 

290 
(MStep ([var_x], inst, [c1; c2])) 

291 
(mk_memory_pack ~inst (node_name td)) 

292 
(mk_transition ~inst (node_name td) [] [] [vdecl_to_val var_x]) 

293 
in 

270  294 
{ ctx with 
271 
si = mkinstr True (MReset o) :: ctx.si;


272 
j = IMap.add o (td, []) ctx.j;


295 
si = mkinstr (MSetReset inst) :: ctx.si;


296 
j = IMap.add inst (td, []) ctx.j;


273  297 
} 
274  298  
275 
 [x], Expr_pre e1 when env.is_local x >


299 
 [x], Expr_pre e when env.is_local x > 

276  300 
let var_x = env.get_var x in 
277 
let ctx = ctl 

278 
True 

279 
(MStateAssign (var_x, translate_expr e1)) in 

280 
{ ctx with 

281 
m = VSet.add var_x ctx.m; 

282 
} 

301 
let e = translate_expr e in 

302 
ctl 

303 
(MStateAssign (var_x, e)) 

304 
(mk_state_variable_pack var_x) 

305 
(mk_state_assign_tr var_x e) 

283  306  
284  307 
 [x], Expr_fby (e1, e2) when env.is_local x > 
285  308 
let var_x = env.get_var x in 
309 
let e2 = translate_expr e2 in 

286  310 
let ctx = ctl 
287 
True 

288 
(MStateAssign (var_x, translate_expr e2)) in 

311 
(MStateAssign (var_x, e2)) 

312 
(mk_state_variable_pack var_x) 

313 
(mk_state_assign_tr var_x e2) 

314 
in 

289  315 
{ ctx with 
290 
m = VSet.add var_x ctx.m; 

291  316 
si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si; 
292  317 
} 
293  318  
...  ...  
298  323 
let vl = List.map translate_expr el in 
299  324 
let node_f = node_from_name f in 
300  325 
let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in 
301 
let o = new_instance node_f eq.eq_rhs.expr_tag in


326 
let inst = new_instance node_f eq.eq_rhs.expr_tag in


302  327 
let env_cks = List.fold_right (fun arg cks > arg.expr_clock :: cks) 
303  328 
el [eq.eq_rhs.expr_clock] in 
304  329 
let call_ck = Clock_calculus.compute_root_clock 
305  330 
(Clock_predef.ck_tuple env_cks) in 
306  331 
let ctx = ctl 
307  332 
~ck:call_ck 
308 
True 

309 
(MStep (var_p, o, vl)) in 

333 
(MStep (var_p, inst, vl)) 

334 
(mk_memory_pack ~inst (node_name node_f)) 

335 
(mk_transition ~inst (node_name node_f) vl [] (vdecls_to_vals var_p)) 

336 
in 

310  337 
(*Clocks.new_var true in 
311  338 
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; 
312  339 
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;*) 
313  340 
{ ctx with 
314  341 
si = if Stateless.check_node node_f 
315 
then ctx.si else mkinstr True (MReset o) :: ctx.si;


316 
j = IMap.add o call_f ctx.j;


342 
then ctx.si else mkinstr (MSetReset inst) :: ctx.si;


343 
j = IMap.add inst call_f ctx.j;


317  344 
s = (if Stateless.check_node node_f 
318  345 
then [] 
319 
else reset_instance o r call_ck)


320 
@ ctx.s 

346 
else reset_instance inst r call_ck)


347 
@ ctx.s;


321  348 
} 
322  349  
323  350 
 [x], _ > 
324  351 
let var_x = env.get_var x in 
325 
control_on_clock eq.eq_rhs.expr_clock True (translate_act (var_x, eq.eq_rhs)) 

352 
let instr, spec = translate_act (var_x, eq.eq_rhs) in 

353 
control_on_clock eq.eq_rhs.expr_clock instr True spec 

326  354  
327  355 
 _ > 
328  356 
Format.eprintf "internal error: Machine_code.translate_eq %a@?" 
...  ...  
330  358 
assert false 
331  359  
332  360 
let constant_equations locals = 
333 
VSet.fold (fun vdecl eqs >


361 
List.fold_left (fun eqs vdecl >


334  362 
if vdecl.var_dec_const 
335  363 
then 
336  364 
{ eq_lhs = [vdecl.var_id]; 
...  ...  
338  366 
eq_loc = vdecl.var_loc 
339  367 
} :: eqs 
340  368 
else eqs) 
341 
locals []


369 
[] locals


342  370  
343 
let translate_eqs env ctx eqs = 

371 
let translate_eqs env ctx id inputs locals outputs eqs =


344  372 
List.fold_right (fun eq (ctx, i) > 
345 
let ctx = translate_eq env ctx i eq in 

373 
let ctx = translate_eq env ctx id inputs locals outputs i eq in


346  374 
ctx, i  1) 
347  375 
eqs (ctx, List.length eqs) 
348  376 
> fst 
...  ...  
385  413 
in 
386  414 
vars, eql, assertl 
387  415  
388 
let translate_core nid sorted_eqs locals other_vars =


416 
let translate_core env nid sorted_eqs inputs locals outputs =


389  417 
let constant_eqs = constant_equations locals in 
390  418  
391 
let env = build_env locals other_vars in 

392  
393  419 
(* Compute constants' instructions *) 
394 
let ctx0 = translate_eqs env (ctx_init nid) constant_eqs in 

395 
assert (VSet.is_empty ctx0.m); 

420 
let ctx0 = translate_eqs env ctx_init nid inputs locals outputs constant_eqs in 

396  421 
assert (ctx0.si = []); 
397  422 
assert (IMap.is_empty ctx0.j); 
398  423  
399  424 
(* Compute ctx for all eqs *) 
400 
let ctx = translate_eqs env (ctx_init nid) sorted_eqs in


425 
let ctx = translate_eqs env ctx_init nid inputs locals outputs sorted_eqs in


401  426  
402  427 
ctx, ctx0.s 
403  428  
429 
let zero = mk_val (Cst (Const_int 0)) Type_predef.type_int 

430  
431 
let memory_pack_0 nd = 

432 
{ 

433 
mpname = nd; 

434 
mpindex = Some 0; 

435 
mpformula = And [StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero)] 

436 
} 

437  
438 
let memory_pack_toplevel nd i = 

439 
{ 

440 
mpname = nd; 

441 
mpindex = None; 

442 
mpformula = Ternary (Memory ResetFlag, 

443 
StateVarPack ResetFlag, 

444 
mk_memory_pack ~i nd.node_id) 

445 
} 

446  
447 
let transition_0 nd = 

448 
{ 

449 
tname = nd; 

450 
tindex = Some 0; 

451 
tinputs = nd.node_inputs; 

452 
tlocals = []; 

453 
toutputs = []; 

454 
tformula = True; 

455 
} 

456  
457 
let transition_toplevel nd i = 

458 
{ 

459 
tname = nd; 

460 
tindex = None; 

461 
tinputs = nd.node_inputs; 

462 
tlocals = []; 

463 
toutputs = nd.node_outputs; 

464 
tformula = ExistsMem (Predicate (ResetCleared nd.node_id), 

465 
mk_transition nd.node_id ~i 

466 
(vdecls_to_vals (nd.node_inputs)) 

467 
[] 

468 
(vdecls_to_vals nd.node_outputs)); 

469 
} 

404  470  
405  471 
let translate_decl nd sch = 
406  472 
(* Format.eprintf "Translating node %s@." nd.node_id; *) 
...  ...  
413  479 
let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in 
414  480  
415  481 
(* Build the env: variables visible in the current scope *) 
416 
let locals_list = nd.node_locals @ new_locals in


417 
let locals = VSet.of_list locals_list in


418 
let inout_vars = (VSet.of_list (nd.node_inputs @ nd.node_outputs)) in


419 
let env = build_env locals inout_vars in


482 
let locals = nd.node_locals @ new_locals in 

483 
(* let locals = VSet.of_list locals_list in *)


484 
(* let inout_vars = nd.node_inputs @ nd.node_outputs in *)


485 
let env = build_env nd.node_inputs locals nd.node_outputs in


420  486  
421  487 
(* Format.eprintf "Node content is %a@." Printers.pp_node nd; *) 
422  488  
...  ...  
430  496 
* VSet.pp inout_vars 
431  497 
* ; *) 
432  498  
433 
let ctx, ctx0_s = translate_core 

434 
nd.node_id (assert_instrs@sorted_eqs) locals inout_vars in 

499 
let equations = assert_instrs @ sorted_eqs in 

500 
let mems = get_memories env equations in 

501 
(* Removing computed memories from locals. We also removed unused variables. *) 

502 
let locals = List.filter 

503 
(fun v > not (VSet.mem v mems) && not (List.mem v.var_id unused)) locals in 

504 
(* Compute live sets for spec *) 

505 
Lustre_live.set_live_of nd.node_id nd.node_outputs locals equations; 

506  
507 
(* Translate equations *) 

508 
let ctx, ctx0_s = translate_core env nd.node_id equations 

509 
nd.node_inputs locals nd.node_outputs in 

435  510  
436  511 
(* Format.eprintf "ok4@.@?"; *) 
437  512  
438 
(* Removing computed memories from locals. We also removed unused variables. *) 

439 
let updated_locals = 

440 
let l = VSet.elements (VSet.diff locals ctx.m) in 

441 
List.fold_left (fun res v > if List.mem v.var_id unused then res else v::res) [] l 

442 
in 

513 
(* Build the machine *) 

443  514 
let mmap = IMap.bindings ctx.j in 
515 
let mmemory_packs = 

516 
memory_pack_0 nd 

517 
:: List.mapi (fun i f > 

518 
{ 

519 
mpname = nd; 

520 
mpindex = Some (i + 1); 

521 
mpformula = red f 

522 
}) ctx.mp 

523 
@ [memory_pack_toplevel nd (List.length ctx.mp)] 

524 
in 

525 
let mtransitions = 

526 
transition_0 nd 

527 
:: List.mapi (fun i (tinputs, tlocals, toutputs, f) > 

528 
{ 

529 
tname = nd; 

530 
tindex = Some (i + 1); 

531 
tinputs; 

532 
tlocals; 

533 
toutputs; 

534 
tformula = red f; 

535 
}) ctx.t 

536 
@ [transition_toplevel nd (List.length ctx.t)] 

537 
in 

538 
let clear_reset = mkinstr ~instr_spec:[ 

539 
mk_memory_pack ~i:0 nd.node_id; 

540 
mk_transition ~i:0 nd.node_id 

541 
(vdecls_to_vals nd.node_inputs) 

542 
[] 

543 
[]] MClearReset in 

444  544 
{ 
445  545 
mname = nd; 
446 
mmemory = VSet.elements ctx.m;


546 
mmemory = VSet.elements mems;


447  547 
mcalls = mmap; 
448  548 
minstances = List.filter (fun (_, (n,_)) > not (Stateless.check_node n)) mmap; 
449  549 
minit = ctx.si; 
...  ...  
452  552 
mstep = { 
453  553 
step_inputs = nd.node_inputs; 
454  554 
step_outputs = nd.node_outputs; 
455 
step_locals = updated_locals;


555 
step_locals = locals; 

456  556 
step_checks = List.map (fun d > d.Dimension.dim_loc, 
457  557 
translate_expr env 
458  558 
(expr_of_dimension d)) 
459  559 
nd.node_checks; 
460 
step_instrs = ( 

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

462 
common branches are not merged while they are in C or Java 

463 
backends. *) 

464 
if !Backends.join_guards then 

465 
join_guards_list ctx.s 

466 
else 

467 
ctx.s 

468 
); 

560 
step_instrs = clear_reset :: 

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

562 
common branches are not merged while they are in C or Java 

563 
backends. *) 

564 
(if !Backends.join_guards then 

565 
join_guards_list ctx.s 

566 
else 

567 
ctx.s); 

469  568 
step_asserts = List.map (translate_expr env) nd_node_asserts; 
470  569 
}; 
471  570  
...  ...  
474  573 
cocospec node, or the current one is a cocospec node. Contract do 
475  574 
not contain any statement or import. *) 
476  575  
477 
mspec = { mnode_spec = nd.node_spec; mtransitions = [] };


576 
mspec = { mnode_spec = nd.node_spec; mtransitions; mmemory_packs };


478  577 
mannot = nd.node_annot; 
479  578 
msch = Some sch; 
480  579 
} 
Also available in: Unified diff
work on spec generation almost done