[Bug] [kompile|kprove] - Huge memory usage

[virgil-serbanuta]

K Version

$ kompile --version
K version:    v5.2.14-6-g119872b473-dirty
Build date:   Sat Nov 27 13:39:26 EET 2021

Description

Kompile needs between 8 and 16G of memory for a semantics that used to fit in 4G. Kprove uses between 32 and 64G for a proof that used to fit in 4G.

Input Files

oom.zip

Reproduction Steps

kompile --backend haskell can-be-deleted-execute.k

This fails with OOM if checkJava contains -Xmx4096m or -Xmx8G in the K_OPTS thing, but works with -Xmx16G. When it works, it takes ~4:36 min on my machine.

kprove --spec-module "PROOF-RUN-EXTERNAL-CALL-FROM-USER" --dry-run proof-run-external-call-from-user.k

This fails with OOM if checkJava contains -Xmx32G in the K_OPTS thing, but works with -Xmx64G. When it works, it takes ~9:57 min on my machine

Note that both fit in 4G of memory at commit 8555efc0656b2a5c25e3db0f8f868fb7a1bca970, finishing in 48s (kompile) and 42s (kprove)

Expected Behavior

kompile and kprove should use a reasonable amount of memory, and should take < 100 sec to finish.

[radumereuta]

Investigate this.

[radumereuta]

I did a git bisect and this is the first commit that fails: 41f2e80
It seems that imports FOO.bar OOM issue is not properly fixed.
@dwightguth should I revert #2292 or do you have time to look at it in the near future?

[radumereuta]

Revert this for now.

[radumereuta]

@virgil-serbanuta you can update to the latest master. I've removed the problematic commit and the times dropped to normal (tested).
@dwightguth when you find the time, you can have a look at what is actually wrong.

[virgil-serbanuta]

Thank you!

[radumereuta]

We removed the feature that caused the issue.