Age | Commit message (Collapse) | Author |
|
This should not change the behaviour of KLEE and mimics the old API.
- functions moved from util into time namespace
- uses time points and time spans instead of double
- CLI arguments now have the form "3h5min8us"
Changed command line parameters:
- batch-time (double to string)
- istats-write-interval (double to string)
- max-instruction-time (double to string)
- max-solver-time (double to string)
- max-time (double to string)
- min-query-time-to-log (double to string)
- seed-time (double to string)
- stats-write-interval (double to string)
- uncovered-update-interval (double to string)
- added: log-timed-out-queries (replaces negative max-solver-time)
|
|
Since LLVM 5 commit 1f8f0490690b, CallSite.paramHasAttr is indexed from
0, so make sure we use correct indexing in klee. And use
CallSite.hasRetAttr for return attributes.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
In llvm 5, since commit 957caa243d9270df37a566aedae3f1244e7b62ef, the
first parameter to APFloat::convertToInteger is MutableArrayRef. So
handle that.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Starting llvm 5, SwitchInst->findCaseValue() now has to be dereferenced
using ->. So do so, otherwise we see:
../lib/Core/Executor.cpp:1598:38: error: no member named 'getCaseSuccessor' in 'llvm::SwitchInst::CaseIteratorImpl<llvm::SwitchInst::CaseHandle>'; did you mean to use '->' instead of '.'?
BasicBlock *caseSuccessor = i.getCaseSuccessor();
^
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
and introduce klee_open_compressed_output_file with similar behavior
along some other minor improvements
|
|
|
|
Don't pollute the project include directory with optimization specific
headers.
|
|
Conditions are checked inside of `optimizeExpr()`
anyway. This simplifies the code a lot.
|
|
|
|
simplifies code a lot.
|
|
avoid ambiguity of valueOnly parameter
|
|
|
|
|
|
to have only solver options.
|
|
Currently KLEE only handles the first segfault in external calls
as it doesn't unblock SIGSEGV afterwards. This patch unblocks the
signal and enables handling of multiple failing calls.
|
|
|
|
AddressSpace::checkPointerInObject() that is called in both the forward and the backward searches. This makes the code more modular and removes a large part of duplicated code and should also address the non-deterministic coverage in the resolve() function which affects Codecov reports.
|
|
|
|
Starting with LLVM 4, we have getStructTypeOrNull(), so use it.
operator* in post-4 will have a different semantics.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
So handle the type specially whenever needed.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
LLVM 4 removes the old time interface and starts using the C++11's
chrono. So switch to that in klee for LLVM 4 too.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
Replace the remaining occurrences of `Inst::Create()` with
`llvm::Builder` to manage metadata automatically and to fold
instructions.
C++11 it and clang-format
|
|
addresses comment made by @adrianherrera in #385
|
|
LLVM commit eac309550f25 removed implicit iterator conversions. So we
have to get the iterators explicitly now.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
The rounding was removed because it was never needed:
llvm-mirror/llvm@ff278be
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
clang-format on patch)
|
|
deprecated for many years now and causes problems during replay. Changed and simplified affected test case.
|
|
|
|
Link intrinsic library before executing optimizations.
This makes sure that any optimization run by KLEE on the module
is executed for the intrinsic library as well.
Support .ll files as input for KLEE as well.
|
|
|
|
|
|
|
|
LLVM 3.7 added a PointeeType parameter to GetElementPtrInst::Create.
Let's handle that by a macro called KLEE_LLVM_GEP_TYPE, defined in
Version.h.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
reflect the fact that it simply returns a string
|
|
version that takes an argument a stream
|
|
This is too generic and llvm 6.0 defines DEBUG as follows:
#define DEBUG(X) DEBUG_WITH_TYPE(DEBUG_TYPE, X)
This then results in various build failures where once the macro is
defined, once it is not.
So rename this generic macro to KLEE_ARRAY_DEBUG.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
dependency --output-istats is not
|
|
|
|
|
|
|
|
|
|
If an external function in KLEE is invoked, it might update errno.
Previously, the errno specific variable in a state was only updated
if it was part of the executed instructions.
That opened up a timeframe that increased the likelihood of errno being
overwritten by another method call.
This patch fixes two issues:
* the errno of the KLEE process state is updated before the external
function call allowing to detect changes to it later on
* after the external call, the memory object of errno is directly
updated
with its new value, reducing the likelihood to be overwritten by
another
call
Additional features:
* Add support for `errno()` for Darwin as well.
* Simplified errno handling in POSIX layer
|
|
|
|
|