Hi Heming,
This is a KLEE bug, which I know about but never got around to fixing.
In the current implementation, we never free MemoryObjects. In the
code we were testing, this never turned out to be a big enough issue
to block testing, although its certainly something which is worth
fixing.
I don't recall all the details, unfortunately, but this is do able. It
does require reference counting on the MemoryObject objects, at least.
There are some additional issues, as well, for example if you free a
MemoryObject immediately then some use-of-free'd-memory errors might
not be caught. (the current strategy is effectively guaranteeing that
we don't recycle any memory addresses).
Personally, I would like to see this fixed as part of a more robust
heap allocation strategy, that addressed additional issues (for
example, supplying a deterministic malloc), but I am unable to devote
time to this myself.
- Daniel
On Wed, Mar 31, 2010 at 8:18 PM, Heming Cui <heming at cs.columbia.edu> wrote:
> Dear Daniel and Cristian,
> ??? I am Heming Cui, Prof. Junfeng Yang's student. May I ask you a question,
> please? Recently I?was running klee with some long running programs and
> found a question about the memory usage of local variable of functions in
> klee.
> ??? Please refer to the source code below (and also in the attachment).
> Foo() dedclares a function local var, and the main function calls fool()
> again and again. If I compile this code with llvm-gcc and run?the bit
> code?with klee, the memory usage increases to more than 90% as soon as the
> program starts and never drops.?The memory in my machine?is 2GB. If I
> compile this code with gcc and run it natively, and the memory usage is only
> 0.1% and never increases.
> ??? If I change "int a[100000];" to be "int a;", the memory usage would
> increase to more than 90% after about 10 seconds of start, and never drops.
> ??? It seems to me that we might need to unbind local vars in klee memory
> address?space after a function exits? I am a little confused of this part,
> since if my program runs for a long time, this problem would happen and
> affect the speed.
>
> Memory usage of klee is 93.3%:
> ? PID USER????? PR? NI? VIRT? RES? SHR S %CPU %MEM??? TIME+
> COMMAND
> ?3099 heming??? 20?? 0 1773m 469m??? 4 D? 1.7 93.3?? 0:04.18 klee
>
>
> Source code (also attached):
>
> #include <stdio.h>
>
> void foo() {
> ?int a[100000];
> ?return;
> }
>
> int main(int argc, char * argv[]) {
> ?while (1) {
> ??foo();
> ?}
>
> ?return 0;
> }
>
> --
> Regards,
> Heming Cui
>
