Hello Oleg,
while KLEE does indeed treat function parameters and local variables
very similar to dynamic variables, it should automatically clean them up
whenever they are not needed anymore (i.e., automatically at function
return time). This part of the code has been tested for a long time, and
I think it is unlikely (although of course always possible) that KLEE
does not perform this cleanup.
KLEE's deterministic memory feature is mainly used to map program
addresses to system addresses. This code is fairly new, and although it
seems to work well, there may of course be a bug in there that prevents
some deallocations from being processed correctly. This would show as
running out of "deterministic memory" in the sense that eventually
there is not enough address space left to allocate new objects to. This
will also happen if you enabled a large or even infinite quarantine, as
that leaks the addresses by design.
An effect that we see often is KLEE just plain using all the memory.
Since KLEE forks the state of the program under test every time a
symbolic value may cause two different control-flows, it is easy to
create a lot of states - it often grows exponential. KLEE performs
various optimizations for that case, but eventually you will simply run
out of memory. The deterministic address space is accounted for each
state individually, so it should not cause any issues there.
What are your actual symptoms? How big is the (maximum) resident set and
how much memory does the machine have / what memory limit did you set?
How many states do you have? Did you configure the quarantine feature?
Best,
Daniel
On 02/08/2024 14:22, Oleg Sokolsky wrote:
Dear KLEE community,
I have a program that, after a long run in KLEE, runs out of
deterministic memory. To the best of my knowledge, it does not
allocate dynamic objects. But it does make a lot of non-recursive
function calls.
Our suspicion currently is that KLEE allocates memory objects for
function parameters and local variables and, after the function
returns, they stay in the deterministic memory until it is eventually
exhausted. Does this suspicion sound right and, if so, is there a way
around it. And, otherwise, what could be the reason?
Thanks,
Oleg
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
