Conversation
| | FrameBlock (_, _, nes, nis) :: items -> | ||
| let* gs, lhss = mk_graph_node_items m items in | ||
| R.ok (union_dependency_analysis_data g gs, eqn_lhss eqn @ lhss) | ||
| | IfBlock (_, cond, nis1, nis2) :: items |
There was a problem hiding this comment.
The PR adds the condition edges only to each node's own dependency graph, here in mk_graph_node_items. The node summary is built separately by mk_node_summary, which reads equations through LH.extract_node_equation, and that helper drops block conditions. So a node's summary never records that an output depends on the inputs its block condition reads, and a cycle that goes through a node call is still accepted.
Reproduction:
node M(x:int) returns (y:int); let if x > 0 then y = 0; else y = 1; fi tel
node N() returns (z:int); let z = M(z); check z >= 0; tel
Kind 2 accepts this and reports the property as valid (k=1). The interpreter then fails with "Transition relation not satisfiable". Writing M as y = if x > 0 then 0 else 1 is correctly rejected as a cyclic dependency.
Suggested fix: make mk_node_summary include the same condition edges, either through an equation extractor that keeps block conditions or by building the summary from what mk_graph_node_items produces.
2 participants
No description provided.