Bug in detecting initialization

[jon-bell]

Hi Milos, I came across the following bug in Ekstazi: When you access a static field, Ekstazi is recording that we depend on the class that the access-site bytecode says owns the field. But this may not necessarily be the class that actually declares the field. Consider the case where interface I declares field f, and Class C implements I. If I access the field as “C.f” then during the first test that runs, Ekstazi will see a dependency on I (because I will have its clinit called), but in the second test that runs, there will not be the dependency on I (which there should be), there will be just the dependency on C (which it does not actually depend on, by the way - accessing this field will NOT trigger the initialization of C).

I've attached a small example that demonstrate this. Build and test it, then change the declared array length of “field” on the interface - this should cause both tests to be selected to run, but only one does.

If you are planning to make Ekstazi open source I’d be happy to just send a pull request with a patch :) We have a few tricks for handling this sort of dynamic resolution of interface fields in the new version of VMVM - the old version required advanced knowledge of the entire class hierarchy (not a great requirement), but now we do it entirely dynamically.

[ghost]

Thanks a lot Jon,

We will take a closer look at the example; our previous experiment that evaluated this issue discovered very few cases. We will keep you posted.

Happy Holidays, Milos