`imports FOO.bar` made the cache.bin file increase in size

[virgil-serbanuta]

Motivation

• kprove and kprovex crash with OOM errors on the Multisig proofs

Example K Code

Example:

I would like to be able to specify the Java memory size on the command line for kprove and kprovex, perhaps also for kompile:

  kprove --java-memory=8G proof.k

Documentation

--java-memory=$SIZE sets the -Xmx$SIZE argument for the Java virtual machine used by kompile/kprove/kprovex.

Potential Alternatives/Work-arounds

A better solution would be to reduce the k memory usage, but allowing the user to set the memory limits is probably easier.

Testing Approach

N/A

[dwightguth]

This is doable via the K_OPTS environment variable. We will probably not support it as a command line flag because our option parsing is done by the jvm.

[radumereuta]

A bit of background.
Starting with this commit: #2144
Virgil's definition begun to fail with OOM.
I've looked at the cache.bin files of EVM and they've grown in size:

backend	before	after	diff
java	5.8MB	6.6MB	1.13
haskell	6.6MB	7.9MB	1.19
llvm	6.1MB	7.0MB	1.14

When this happens, just loading the caches slows down significantly because GC tries to squeeze everything into the little memory it had left.
Increase the memory size and everything runs smoothly again.

[virgil-serbanuta]

FWIW, I'm also seeing an increase in the cache.bin files on the K master relative to the latest commit on which my proofs still work (8555efc0656b2a5c25e3db0f8f868fb7a1bca970), but the increase is, sometimes, a bit more dramatic, e.g. one is going from 16M to 415M:

-r-xr-xr-x 1 virgil virgil 16M sep  3 22:26 ./execroot/__main__/bazel-out/k8-fastbuild/bin/protocol-correctness/proof/malicious-user/malicious-user-execute-kompiled/cache.bin

vs

-r-xr-xr-x 1 virgil virgil 415M sep  3 21:53 ./execroot/__main__/bazel-out/k8-fastbuild/bin/protocol-correctness/proof/malicious-user/malicious-user-execute-kompiled/cache.bin

However, for other cache.bin files, the size seems to stay roughly the same.

[radumereuta]

@virgil-serbanuta could you build a definition that replicates this issue?
Something that we can test locally. Doesn't need to be minimized, just to be easy to run.

[virgil-serbanuta]

Sorry for the delay.

kprove-timeout.zip

To reproduce, unzip the above, then:

cd kprove-timeout
kompile --backend haskell invariant-execute.k
kprove proof-discard-action-1-kompile.k --dry-run  --spec-module PROOF-DISCARD-ACTION-1

[dwightguth]

I was able to address the size of cache.bin relatively easily, but this does not seem to have actually addressed the OOM that Virgil was experiencing. Continuing to investigate.