Investigate inference of loop invariants using merge-nodes functionality

[ehildenb]

Here #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: #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:

• Remove the loop invariant present here: https://github.com/runtimeverification/kontrol/pull/369/files#diff-a2ef7982f6abbbf7c35d297264226ea334b6dbd3830bc673bf68f2b62a755635R141.
• Run the program out to a certain number of iterations of the loop.
• Use the merge-nodes functionality on the loop heads to produce a new state taht is more general than teh loop heads.
• Compare the generated result with the LHS of the original invariant. Post the results here.
• Figure out how to automate more of the invariant generation.

[qian-hu]

• kontrol show output
• Result after merging loop heads 13 and 14
• Result after merging intermediate nodes (with the same K cell as in the original loop invariant) for the first three loops

[ehildenb]

@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?

[ehildenb]

Also, what is the process needed to go from the original merged node to the invariant there? What manual steps need to be taken?

[ehildenb]

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).

[qian-hu]

@ehildenb Please refer to the original KCFG here. Additionally, you can find the KCFG output after merging intermediate nodes here.

[qian-hu]

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.

[palinatolmach]

Related: runtimeverification/k#4425