Revision d3e4c22f src/machine_code.ml
| src/machine_code.ml | ||
|---|---|---|
| 157 | 157 |
node_checks = []; |
| 158 | 158 |
node_asserts = []; |
| 159 | 159 |
node_eqs= []; |
| 160 |
node_dec_stateless = false; |
|
| 161 |
node_stateless = Some false; |
|
| 160 | 162 |
node_spec = None; |
| 161 | 163 |
node_annot = None; } |
| 162 | 164 |
|
| ... | ... | |
| 193 | 195 |
mannot = None; |
| 194 | 196 |
} |
| 195 | 197 |
|
| 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 | 198 |
let new_instance = |
| 205 | 199 |
let cpt = ref (-1) in |
| 206 | 200 |
fun caller callee tag -> |
| 207 | 201 |
begin |
| 208 | 202 |
let o = |
| 209 |
if is_stateless_node callee then
|
|
| 203 |
if Corelang.check_stateless_node callee then
|
|
| 210 | 204 |
node_name callee |
| 211 | 205 |
else |
| 212 | 206 |
Printf.sprintf "ni_%d" (incr cpt; !cpt) in |
| ... | ... | |
| 220 | 214 |
let const_of_carrier cr = |
| 221 | 215 |
match (carrier_repr cr).carrier_desc with |
| 222 | 216 |
| Carry_const id -> id |
| 223 |
| Carry_name -> assert false
|
|
| 224 |
| Carry_var -> assert false
|
|
| 225 |
| Carry_link _ -> assert false (* TODO check this Xavier *)
|
|
| 217 |
| Carry_name |
|
| 218 |
| Carry_var |
|
| 219 |
| Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
|
|
| 226 | 220 |
|
| 227 | 221 |
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *) |
| 228 | 222 |
(* the context contains m : state aka memory variables *) |
| ... | ... | |
| 370 | 364 |
NodeDep.filter_static_inputs (node_inputs node_f) el in |
| 371 | 365 |
let o = new_instance node node_f eq.eq_rhs.expr_tag in |
| 372 | 366 |
(m, |
| 373 |
(if is_stateless_node node_f then si else MReset o :: si),
|
|
| 367 |
(if check_stateless_node node_f then si else MReset o :: si),
|
|
| 374 | 368 |
(if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j), |
| 375 | 369 |
d, |
| 376 | 370 |
reset_instance node args o r eq.eq_rhs.expr_clock @ |
| ... | ... | |
| 442 | 436 |
mname = nd; |
| 443 | 437 |
mmemory = ISet.elements m; |
| 444 | 438 |
mcalls = mmap; |
| 445 |
minstances = List.filter (fun (_, (n,_)) -> not (is_stateless_node n)) mmap;
|
|
| 439 |
minstances = List.filter (fun (_, (n,_)) -> not (check_stateless_node n)) mmap;
|
|
| 446 | 440 |
minit = init; |
| 447 | 441 |
mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs; |
| 448 | 442 |
mstep = {
|
Also available in: Unified diff