| Age | Commit message (Collapse) | Author |
|---|
|
This is a thread-local version of __cxa_atexit (but, in the absence
of threads, it is sufficient to just call __cxa_atexit).
The test is based on the existing test for atexit in
test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c
The motivation for adding this function is to support the Rust standard
library that calls __cxa_thread_atexit_impl.
This function is usually a weak symbol but, in KLEE, this behaves like a call
to an unknown function and chaos ensues.
Worse, it happens just as the program is cleanly shutting itself down,
so programs that are cleanly exiting crash with the wrong message.
|
|
outputting wrong data.
When KLEE crashes, it produces an empty info file, so it is not enough to check for the existence of an info file.
Previously, table columns would mismatch and return data labeled with the wrong directory names.
|
|
|
|
|
|
This change allows KLEE to be configured to use the LLVM version
that comes with the Rust compiler instead of a standard version.
e.g., one might configure with
-DLLVM_CONFIG_BINARY=${RUST_SRC}/build/x86_64-unknown-linux-gnu/llvm/bin/llvm-config
For which typical output might be
10.0.1-rust-dev
|
|
This instrinsic detects whether the program is being executed
symbolically or concretely (i.e., using the libkleeRuntest library).
The intended usage (illustrated in the test program) is to
allow the test program to display the input values by invoking
any libraries it wants to.
This is especially valuable if you are constructing complex,
structured values and for languages like Rust (or C++) that have
rich libraries and print libraries.
For example, you might pick a symbolic value N with the
assumption "0 <= N < 10" and then pick N symbolic
values and write them to an array.
The resulting ktest file is a bit hard to understand compared with the
output of the standard print function in Rust/C++.
|
|
|
|
* move global theRNG into Executor
* pass theRNG via ctor to searchers
* remove some type warnings from RNG.cpp
Fixes #1023.
|
|
|
|
|
|
This constructor has been a hack and was wrongly used, use ConstraintManager instead.
Allow copy-constructing states only via `ExecutionState::branch()` call.
|
|
Decouple ExecutionState from TimingSolver
Instead of providing an execution state to the timing solver use a set of
constraints and an additional object for metadata.
Fixes:
* correct accounting of metadata to a specific state
* accounting of all solver invocations (e.g. solver-getRange was not
accounted)
* allows to invoke the solver without a state (avoids costly copying of
states/constraints)
|
|
|
|
|
|
|
|
|
|
|
|
This reverts commit 0aed7731210d0eb41c0ea767edb8067130cf6252.
|
|
Changes:
- IntrinsicCleaner accepts fshr/fshl as accepted intrinsics
- Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract
- Klee/main suppresses warnings about externals that are LLVM reserved
(i.e., begin with "llvm.")
- New test exercises 32 and 7 bit versions including oversize shift values
Test values are based on LLVM's test for fshl/fshr
- Changes that depend on existence of fshr/fshl are guarded by
#if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0)
or
; REQUIRES: geq-llvm-7.0
|
|
|
|
|
|
|
|
* extend help messages for -max-memory and -max-memory-inhibit
* introduces branchingPermitted()
* enforces fork/branch limits in branch() (vector version)
* changes main loop
* calls updateStates() before checkMemoryUsage()
* calls updateStates() again in case we early terminate states
This should prevent double termination for now. Other solutions are
imho more expensive as we would have to compare possibly large
vectors of states (either states(arr) in checkMemoryUsage() or
removedStates in terminateState()).
|
|
|
|
|
|
mainly range-based for, code deduplication
|
|
|
|
|
|
|
|
|
|
|
|
This is the same check used in Executor::setModule. Without this check,
KLEE will segfault in StatisticsManager::incrementIndexedValue,
getIndexedValue, and setIndexedValue when `-output-stats=false` or
`-output-istats=false` because StatisticsManager::indexedStats has not
been allocated.
|
|
|
|
* add getID()/setID()
* use ExecutionStateIDCompare in Executor::states set
* output state id in .err files
|
|
|
|
variadic arguments
|
|
and reformatted comments.
|
|
|
|
|
|
"Instruction *i" declared at the beginning of the function. Reformatted this function.
|
|
byval attribute
|
|
* rename SQLITE3 to SQLite3
CMake Warning (dev) at /usr/share/cmake-3.17/Modules/FindPackageHandleStandardArgs.cmake:272 (message):
The package name passed to `find_package_handle_standard_args` (SQLITE3)
does not match the name of the calling package (SQLite3). This can lead to
problems in calling code that expects `find_package` result variables
(e.g., `_FOUND`) to follow a certain pattern.
Call Stack (most recent call first):
cmake/modules/FindSQLite3.cmake:26 (FIND_PACKAGE_HANDLE_STANDARD_ARGS)
CMakeLists.txt:430 (find_package)
This warning is for project developers. Use -Wno-dev to suppress it.
|
|
|
|
values
Inline asm used for memory barriers might use their operands and propagate them as
return value.
This is currently not supported. Tighten check for this condition and do not to
lift those inline asm instructions.
Fixes #1252
|
|
|
|
Array names used for STP queries used to be restricted to 32 characters,
with the last characters replaced by a unique number.
Similarly, an array is made unique by `klee_make_symbolic`.
Unfortunately, both combined can lead to the generation of the same STP array name for different arrays.
This leads to wrong queries with invalid results.
This is more likely be triggered with longer names for `klee_make_symbolic`
Fixes #1257
|
|
Co-authored with @MartinNowack
|
|
appropriate existing directories and a new directory Statistics; a few missing renames.
|
|
|
|
tly in lib/Core
|
