| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
variables when possible.
Previously an alignment 8 was always used which did not faithfully
emulate what was either explicitly requested in the LLVM IR or what
the default alignment was for the target.
|
|
|
|
Deterministic allocation provides an internal allocator which
mmaps memory to a fixed static address.
This way, same allocation is assured across different KLEE runs
for the same application assuming a deterministic searcher.
In addition, this patch provides following options:
-allocate-determ: switch on/off deterministic allocation
-allocate-determ-size: adjust preallocated memory
-null-on-zero-malloc: returns null pointer in case a malloc
of size 0 was requested. According to standard, also a non-null pointer
can be returned (which happens with the default glibc malloc implementation)
-allocation-space: space between allocations can be adjusted. KLEE is not able
to detect out-of-bound accesses which are inside another but wrong object.
Due the implementation of typical allocators adjacent mallocs have space
in between for management purposes. This spaces helped KLEE to detect off-by-1/2 accesses.
For higher numbers, the allocation space has to be increased.
-allocate-determ-start-address: adjust deterministic start address. The addres
has to be page aligned. KLEE fails if it cannot acquire this address
|
|
For vararg handling, arguments of size bigger than 64 bit need
to be handled 128bit aligned according to AMD calling conventions
AMD64-ABI 3.5.7p5.
To handle that case correctly, we do:
1) make sure that every argument is aligned correctly in
an allocation for function arguments
2) the allocation itself is aligned correctly
|
|
Some of these leaks were introduced by the factory constructor for Array
objects (f049ff3bc04daead8c3bb9f06e89e71e2054c82a) but a few others have
been around for far longer.
This leak was fixed by introducing a ``ArrayCache`` object which has two
purposes
* Retains ownership of all created ``Array`` objects and destroys them when
the ``ArrayCache`` destructor is called.
* Mimic the caching behaviour for symbolic arrays that was introduced
by f049ff3bc04daead8c3bb9f06e89e71e2054c82a where arrays with the same
name and size get "uniqued".
The Executor now maintains a ``arrayCache`` member that it uses and
passes by pointer to objects that need to construct ``Array`` objects (i.e.
``ObjectState``). This way when the Executor is destroyed all the
``Array`` objects get freed which seems like the right time to do this.
For Kleaver the ``ParserImpl`` has a ``TheArrayCache`` member that is
used for building ``Array`` objects. This means that the Parser must
live as long as the built expressions will be used otherwise we will
have a use after free. I'm not sure this is the right design choice.
It might be better to transfer ownership of the ``Array`` objects to
the root ``Decl`` returned by the parser.
|
|
leak in KLEE.
From Gang Hu: "The memory leak is caused by two reasons. First, the
MemoryObject objects are not freed, until the MemoryManager is
destroyed. Second, when KLEE allocates a non-fixed MemoryObject
object, KLEE also allocates a block of memory which is the same as the
object's size. This block of memory is never freed. So, this patch
generally does reference counting on the MemoryObject objects, and
frees them as soon as the reference count drops to zero."
Many thanks to Paul Marinescu as well, who tested this patch
thoroughly on the Coreutils benchmarks. On 1h runs, the memory
consumption typically goes down by 1-5%, but some applications which
see more significant gains.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@148402 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Lots more tweaks, documentation, and web page content is needed,
but this should compile & work on OS X & Linux.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
|
