| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
With recent LLVM versions, this should allow to link against dynamic LLVM
libraries.
|
|
LLVM became more complex, use LLVM's CMake functionality directly instead
of replicating this behaviour in KLEE's build system.
Use the correct build flags provided by LLVM itself.
This is influenced by the way LLVM is built in the first place.
Remove older CMake support (< 3.0).
|
|
|
|
|
|
|
|
|
|
MemoryLimit.h fails on macOS 12.1 without this fix.)
|
|
... and should be replaced with llvm::fs::OF_None since LLVM 7.
See: https://reviews.llvm.org/D101506
https://github.com/llvm/llvm-project/commit/1f67a3cba9b09636c56e2109d8a35ae96dc15782
|
|
|
|
* move global theRNG into Executor
* pass theRNG via ctor to searchers
* remove some type warnings from RNG.cpp
Fixes #1023.
|
|
|
|
- moves timer handling from Executor into support lib
- introduces TimerGroup, removes TimerInfo/WriteStatsTimer/UpdateReachableTimer/WriteIStatsTimer classes
- removes ExecutorTimers.cpp and ExecutorTimerInfo.h
- removes -max-instruction-time flag (see #1114)
|
|
|
|
|
|
|
|
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)
|
|
In llvm commit 03bcb2143b5c, OpenFlags were split and openFileForWrite
accepts one more parameter. Fortunately, openFileForWrite now defaults
to F_None, so we remove the parameter completely from llvm 3.7 and
later.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
I.e. klee::printVersion should now have a parameter -- the output
stream. Change both the prototype and the implementation to handle this
properly.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
and introduce klee_open_compressed_output_file with similar behavior
along some other minor improvements
|
|
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>
|
|
|
|
|
|
configuration, TravisCI scripts and Dockerfile build appropriately.
There are a bunch of clean ups this enables but this commit doesn't
attempt them. We can do that in future commits.
|
|
|
|
Fixes klee/klee#717
delete on null pointer is always safe.
|
|
On FreeBSD <sys/capabilities.h> is present in libc, so we don't require libcap there.
Close and write functions are located in <unistd.h>.
|
|
Request LLVM 3.4 as minimal requirement for KLEE
|
|
removes commented out code from that function.
|
|
`klee_open_output_file()` function so that it can be used by
the Z3Solver.
|
|
Based on work by @ccadeptic23 and @delcypher.
Formatting fixed by @snf.
Fix compiler warning by @martijnthe.
Further fixes by @mchalupa.
Refactored, so that changes can be reviewed -- no massive changes in
whitespace and in the surrounding code.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
to warnings.txt only. Disabled by default.
|
|
When building with ASan the `mallinfo()` function is intercepted.
However the currently implementation is just a stub that always
returns 0. So instead use the public API of the sanitizer runtime
to get the amount of currently allocated memory when KLEE is built
with ASan.
Unfortunately it appears that the way to detect building with ASan
differs between Clang and GCC. There was also a sanitizer runtime
API change too.
This was tested with
* Clang 3.4, 3.5, and 3.9.0
* GCC 4.8, 4.9, 5.2, 5.4 and, 6.2.1.
|
|
This was confusing because it would emit something like
`v1.0.0-290-g08d4716` because the 1.1.0 and 1.2.0 releases
didn't have a tag on the master branch so `git describe --tags`
would just find the `v1.0.0` tag and report based on that tag.
|
|
|
|
transitive dependencies on KLEE's libraries rather than on the final
binaries. This is better because it means we can build
other tools that use KLEE's libraries and not need to express the
needed LLVM dependencies.
It also makes it clearer what the dependencies are between KLEE
libraries. This has illustrated a problem with the `kleeBasic`
library. It contains `ConstructSolverChain.cpp` which clearly
belongs in `kleaverSolver` not in `kleeBasic`. This will be fixed
later.
|
|
This is based off intial work by @jirislaby in #481. However it
has been substantially modified.
Notably it includes a separate build sytem to build the runtimes which
is inspired by the old build system. The reason for doing this is
because CMake is not well suited for building the runtime:
* CMake is configured to use the host compiler, not the bitcode
compiler. These are not the same thing.
* Building the runtime using `add_custom_command()` is flawed
because we can't automatically get transitive depencies (i.e.
header file dependencies) unless the CMake generator is makefiles.
(See `IMPLICIT_DEPENDS` of `add_custom_command()` in CMake).
So for now we have a very simple build system for building the runtimes.
In the future we can replace this with something more sophisticated if
we need it.
Support for all features of the old build system are implemented apart
from recording the git revision and showing it in the output of
`klee --help`.
Another notable change is the CMake build system works much better with
LLVM installs which don't ship with testing tools. The build system
will download the sources for `FileCheck` and `not` tools if the
corresponding binaries aren't available and will build them. However
`lit` (availabe via `pip install lit`) and GTest must already be
installed.
Apart from better support for testing a significant advantage of the
new CMake build system compared to the existing "Autoconf/Makefile"
build system is that it is **not** coupled to LLVM's build system
(unlike the existing build system). This means that LLVM's
autoconf/Makefiles don't need to be installed somewhere on the system.
Currently all tests pass.
Support has been implemented in TravisCI and the Dockerfile for
building with CMake.
The existing "Autoconf/Makefile" build system has been left intact
and so both build systems can coexist for a short while. We should
remove the old build system as soon as possible though because it
creates an unnecessary maintance burden.
|
|
It is pain for build systems to see __DATE__ or __TIME__ in sources as
the build is not reproducible. So disable the timestamping by default
and add an option to enable it if somebody is really after it.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
The mallinfo() interface is ill-designed. It returns 'int' as occupied
memory. This means at most 2G. This causes troubles when capping the
memory to 3G by -max-memory=3000 for example.
We cannot fix the interface, but we can at least extend the space to
4G. So cast those 'int's to 'unsigned int's to avoid sign extension.
Then do the addition on 'size_t' to count on 64bit values (on 64 bit).
Apart from that, the original 'int' + 'int' led to overflow which is
undefined on 'signed int's in C.
Also, when klee is run under valgrind, generic.current_allocated_bytes
from gperftools does not touch the passed pointer and in that case, we
return garbage from GetTotalMallocUsage. So initialize 'value' to 0 to
avoid the problem.
And since GetNumericProperty accepts 'size_t', let's define 'value' as
such. It was 'uint64_t' previously and they differ on 32 bit.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
Provide initial zlib-based compression support for
raw_outstreams. Replacing llvm::raw_fd_outstreams
with compressed_fd_outstreams automatically compresses
data in gzip format before writing to file.
Options added:
* --compress-log to compress all query log files (e.g. *.pc, *.smt2) on
the fly. Every query log file gets extended with .gz.
* --debug-compress-instructions to compress logfile for instruction
stream on the fly.
|
|
Beside improving performance of KLEE,
tcmalloc allows to track used memory correctly.
If available, tcmalloc is automatically used during compile time.
This can be forced to be:
- disabled using --without-tcmalloc
- enabled using --with-tcmalloc
In the second case, configure will fail if tcmalloc
is not found or usable.
Both versions of tcmalloc a minimal and normal version.
|
|
Support directory
|
|
and kleaver.
|
|
when they are given the --version command line option.
Unfortunately to make the build type and git revision available we
need to check this for every build which means KLEE's support library
will be rebuilt for every build which will slow down incremental builds.
This addresses issue #231
|
|
Replaced inefficient llvm::sys::Process::GetTimeUsage() with TimeValue::now(),
because in many cases only the wall clock time is needed, not the user
and sys times (which are significantly more expensive to get).
Updated TimingSolver and WallTimer accordingly.
|
|
|
|
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling
the checks in that mode).
- Eventually it would be nice to just move off of LLVM's DEBUG infrastructure
entirely and just have our own copy, but this works for now.
- Fixes #150.
|
