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