What we learned while building JayHorn.
In a previous post we have discussed how to eliminate implicit control-flow from exception handling and virtual calls. However, there was some implicit control-flow that we couldn’t eliminate easily, like calls to static initializers. Even if we would make calls to those explicit, the JVM would still call the original static initializers when the class is loaded. Its easy to get this wrong because the static initializer may get called twice and thus we probably do not want to do this on the Java level.
Remember our example from the overview (here slightly modified to make it more interesting):
While the new memory model using pull and push is conceptually neat and relatively easy to implement (at least the basic version) it has one significant disadvantage: it is tricky to test. If something goes wrong in the encoding and we try to pull an object from the heap that has not been initialized (by a preceding push), the Horn clause solver will try to use false as an invariant. That is, we just added an assume false somewhere in our program and things might be verified for all the wrong reasons.
This has been a major issue for us throughout the development. There are always bugs. And there is always confirmation bias. If JayHorn finally verifies a program, or always has verified it, it is easy to not look for an assume false.
While this still remains an issue, we want to discuss which steps we take to identify and prevent bugs that could introduce an assume false.