Fix resource leaks from the POSIX runtime #16
Conversation
Otherwise, memsafety would always fail due to leaked memory.
This is not the right way how to it because with this change, KLEE creates a symbolic size array of symbolic size arrays of symbolic bytes. Which is way too time and resource consuming.
| @@ -43,6 +43,7 @@ LLVMCC.Flags += $(LLVMCC.ExtraFlags) \ | |||
| -I@CMAKE_BINARY_DIR@/include \ | |||
| -emit-llvm \ | |||
| -std=gnu89 \ | |||
| -g \ | |||
There was a problem hiding this comment.
Why is this change needed? If it is important for functioning, it would be nice to have it in a separate commit for the documentation purposes.
There was a problem hiding this comment.
I'll move it to a separate commit (and send a similar PR to upstream). It's useful so that all reports in these files are not missing location info.
| klee_destroy_fds(); | ||
|
|
||
| char **ptr; | ||
| for (ptr = argvPtr; *ptr; ptr++) { |
There was a problem hiding this comment.
Why to bother with freeing the arguments if they are made global for KLEE?
There was a problem hiding this comment.
My local copy of KLEE with POSIX runtime enabled was still detecting those leaks.
There was a problem hiding this comment.
That sounds like a bug in the leak detection inside KLEE to me. I would expect KLEE not to report global memory as leaked.
| ie = rl.end(); it != ie; ++it) { | ||
| const MemoryObject *mo = it->first.first; | ||
| assert(!mo->isLocal); | ||
| mo->isGlobal = false; |
There was a problem hiding this comment.
When 'mo' is neither global nor local, what kind of variable it is?
| @@ -511,6 +511,10 @@ void klee_mark_global(void *object) { | |||
| ; | |||
| } | |||
|
|
|||
| void klee_unmark_global(void *object) { | |||
There was a problem hiding this comment.
klee-replay takes a generated test, creates an executable from it and runs it. This is needed to make the executable compile.
| char *s = malloc(numChars+1); | ||
| int argSize = klee_range(0, maxSize + 1, "argSize"); | ||
|
|
||
| char *s = malloc(argSize + 1); |
There was a problem hiding this comment.
The allocation in KLEE never fails, so this should be ok (as long as it is linked to bitcode by KLEE and not by Symbiotic).
|
If #16 (comment) is indeed true, this PR, in general, is redundant work. I'll convert to a Draft for now. |
Otherwise, memsafety would always fail due to leaked memory.