| Age | Commit message (Collapse) | Author |
|---|
|
Implement support for lowering the ``llvm.objectsize`` intrinsic
|
|
Fix a leak detected by ASan in the KQuery parser where on destruction of
|
|
Fix duplication of klee::ArrayHashFn
|
|
introduced in LLVM 2.7. Previously KLEE would emit the following error
message when ``IntrinsicLowering::LowerIntrinsicCall()`` was called on
the intrinsic
```
LLVM ERROR: Code generator does not support intrinsic function 'llvm.objectsize.i64.p0i8'!
```
The ``IntrinsicCleaner`` pass now lowers this intrinsic to a constant
integer depending on the second argument to the intrinsic. This
corresponds to the case where the size of the object pointed to by the
first argument is unknown.
An alternative design would be to handle this intrinsic in the Executor
where is actually possible to know the size of objects during execution.
However that would be much more complicated because if the pointer is
symbolic we would have to fork for every object that could be pointed
to.
The implementation is similar to #260 but we handle the second argument
to the intrinsic correctly and also have a simple test case.
Unfortunately we have to have a different version of the test case
for LLVM 2.9 because the expected suffix for the intrinsic is different
in LLVM 2.9.
|
|
the ``ParserImpl`` it wouldn't free allocated ``Identifier``s
|
|
``include/klee/util/ArrayCache.h``.
|
|
so that it is possible to ``#include "klee/util/ArrayExprHash.h"``
|
|
due to fixes from #315 and #316.
|
|
Try to fix leaking Array objects detected by ASan.
|
|
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.
|
|
helper functions.
|
|
for it
|
|
Use "-debug-dump-stp-queries" argument for KLEE/Kleaver
to print out each STP query sent to the STP Solver.
Queries have the format which `stp` frontend can understand.
|
|
|
|
|
|
|
|
Support directory
|
|
Fix a memory leak in ``UpdateList`` detected by AddressSanitizer.
|
|
The overloaded assignment operator previously only deleted the head
``UpdateNode`` if the ``UpdateList`` had exclusive ownership which left the remaining
list of ``UpdateNode``s dangling if those nodes had ``refCount`` of 1.
To fix this the logic that was previously in the ``UpdateList`` destructor
for deleting nodes that were exclusively referenced by the UpdateList
has been moved into ``UpdateList::tryFreeNodes()`` so that it can be
called from ``UpdateList::operator=()``.
It looks like this bug has been in KLEE since the beginning.
|
|
which is required to suppress all the leaks I'm currently seeing in KLEE
when running ``make unittests`` and ``make check``.
Ideally there should be no leaks but we aren't there yet. Hopefully
at some point we won't need to suppress any leaks and then we can
have a TravisCI build that builds with ASan.
The leak of the expression objects when running the executor is worrying
and I will investigate this next.
|
|
MemorySanitzer and ThreadSanitizer environment variables when running
lit tests.
This makes it easy suppress errors in sanitized versions of KLEE
|
|
build. Spotted by @domainexpert
|
|
|
|
template braces get reformatted the C++11 way and that breaks
compilation.
|
|
flag as suggested by @ccadar
|
|
``--silent-klee-assume=0`` is no longer passed. This ensures that we
also check that ``--silent-klee-assume`` is off by default.
|
|
infeasible assumptions.
|
|
``stp/stplog.h`` header file in the current version of STP
and no support in the build system for setting this define so
this code is completly dead.
|
|
|
|
Fixing klee-clang to strip all flags not understood by llvm-link
|
|
|
|
Removing -fstack-protector-strong for clang <= 3.4
|
|
It's not supported and breaks compilation. This affects in particular
Debian Jessie and probably all derived distros, too
|
|
|
|
|
|
[STPBuilder] Generate SRrem expressions correctly
|
|
Specify klee uclibc version
|
|
branch for klee-uclibc.
|
|
"klee_uclibc_v1.0.0" release of uclibc.
|
|
|
|
Don't use /tmp for futimesat unit test
|
|
This causes problems on a shared machine where multiple users are running the
KLEE unit tests.
|
|
The '%' operater in C is not Gauss Modulo
but remainder operations.
Using a negative number as right operand
can result in a negative number.
Fix appropriate SRem building
Note: MetaSMTlib implementation doesn't have that bug.
|
|
Fix signed division by constant 1/ -1
|
|
Allow to generate initial values for queries with empty constraint set.
|
|
|
|
Travis: Support KLEE with different STP versions, in particular 2.1.0; Disable r940
|
|
Say farewell to r940.
|
|
Build STP version based on provided branch.
Build current STP version 2.1.0 by default and test with master branch
as well
|
|
Division by constant divisor get optimized
using shift and multiplication operations in STP builder.
The used method cannot be applied for divisor 1 and -1.
In that case use slow path.
|
