Open ehildenb opened 6 months ago
@qian-hu I don't quite see the nodes mentioned in the merges in the KCFG output there. Node 19 appears to be a target node, and node 13 and 14 are on either side of the same branch. Nodes 26 and 31 don't exist. Can we see the original KCFG output as well?
Also, what is the process needed to go from the original merged node to the invariant there? What manual steps need to be taken?
Another thought is this. The invariant has the form:
rule LOOP => LOOP_ENDED requires LOOP_INVARIANT
The LOOP
node is the node we are currently trying to infer by merging a bunch of other nodes which show up in a repeating pattern for the loop. The LOOP_ENDED
and LOOP_INVARIANT
ones we probably can't infer as automatically.
But every loop should have structure a -branch-> {b, c}
, where b
is "stepping into the loop", and c
is "stepping out of the loop" (because of the loop head condition). In this example, we've collected several b_1, b_2, b_3, ...
and merged them to try and discover LHS of the invariant (the LOOP
part). We could also consider collecting several c_1, c_2, c_3, ...
and merge them to try and discover the RHS of the loop invariant (the LOOP_ENDED
part).
I've pushed an update to the foundry_merge_nodes()
of foundry.py
allowing for the merging nodes belonging to the same loop but with different K cells. Comparing the result of merging nodes with different K cells against those with the same cells yields valuable information about the dependencies. The merged loop nodes now provide additional information regarding requires related to localMem
of the LHS.
Here https://github.com/runtimeverification/kontrol/pull/444, we update the
merge-nodes
functionality to allow specifying loop heads in looping code. Here, we have an example that uses a loop invariant to allow verifying a small piece of code with a simple loop: https://github.com/runtimeverification/kontrol/pull/369.The
merge-nodes
functionality should help us in identifying the loop invariant needed in order to verify such simple loops. We probably can't infer the entire loop invariant, but at least we can make an initial guess ath the correct LHS of the loop to use.Here, we should:
merge-nodes
functionality on the loop heads to produce a new state taht is more general than teh loop heads.