[klee-dev] deterministic memory in KLEE

[Daniel Schemmel]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev