cached modules cause problems due to changed filepath

[mhhf]

k's java-backend caches compiled modules including the filepath to that module across executions. If now the module is compiled again from a different location without being changed the old filepath is used through the execution. Which causes problems if the old file is deleted.

A solution could be an additional flag which prevents k from caching compiled modules across executions or k rebuilding modules if its path changed.

[dwightguth]

This is more generally because k's caching relies on Object.equals which was not implemented to compare attributes. We have similar problems with the integrity of the cache at compile time. The solution is to compare attributes when caching, but it might take some effort to get everything to work properly when we make the change.

The workaround for now is to delete the kompiled directory and recompile the definition. I will look into fixing this when I get back to the office next week.

[dwightguth]

I was not able to reproduce this behavior; can you provide me with a sequence of steps that you can reproduce the issue with if you want this resolved?

[mhhf]

I work with klab and can give you a step by step example where it fails. Best way to reproduce it is to talk to @ehildenb:

1. Set up a fresh klab + fresh evm-semantics (make clean)
2. run the example proof e.g. SafeAdd and make sure it succeed
3. change the the lemma file so that the proof should not change (e.g. add a new line somewhere)
4. remove everything in $TMPDIR/klab/
5. run the proof and make sure the proofid is a different one (by hitting d in klab (pid))
6. In the directory $TMPDIR/klab/ search for a file which contains abstract-semantics.k - its path should be pointing to the path of the proof executed in step 2.

the path comes directly from here

[ehildenb]

KLab's cacheing (and K's) has changed significantly since this issue was opened, so it's not likely we can reproduce it now. If it's still an issue @mhhf feel free to re-open with an example of the problem on latest K/KEVM/KLab.