about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.cpp
AgeCommit message (Collapse)Author
2021-02-16Executor: remove obsolete special case for __cxa_{re,}throwJulian Büning
__cxa_throw and __cxa_rethrow were not handled by special function handlers in the final version of #966 (which introduced support for C++ exception handling)
2021-02-16add ifdefs for C++ exception handlingJulian Büning
restoring old behavior without EH support
2020-12-04llvm11: CallBase::getParamAlignment has been deprecatedLukas Zaoral
and should be replaced with CallBase::getParamAlign
2020-12-04llvm11: GlobalValue::getAlignment has been removedLukas Zaoral
See: https://reviews.llvm.org/D80368
2020-12-04llvm11: Composite and Sequential types were removedLukas Zaoral
See: https://reviews.llvm.org/D75660 https://reviews.llvm.org/D75661
2020-12-04llvm11: Use getCalledOperand instead of getCalledValueLukas Zaoral
CallBase::getCalledValue has been deprecated by getCalledOperand since LLVM 8 and has been removed in LLVM 11 See: https://reviews.llvm.org/D78882
2020-12-04llvm11: Make conversions from StringRef to std::string explicitLukas Zaoral
The same applies to SmallString. See: llvm/llvm-project@777180a#diff-497ba4c0c527a125d382b51a34f32542
2020-11-12Casting.h: isa_and_nonnull<>Julian Büning
2020-11-12Ref: implement operator bool()Julian Büning
2020-11-04Link to the different runtime libraries depending on the application to test.Martin Nowack
Currently, only 32bit vs. 64bit is supported.
2020-10-21fix Executor: remove UB from bindInstructionConstantsJulian Büning
2020-10-12address MartinNowack's remaining feedbackJulian Büning
2020-10-12Implemented support for C++ ExceptionsFelix Rath
We implement the Itanium ABI unwinding base-API, and leave the C++-specific parts to libcxxabi. Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de>
2020-10-09implement fneg instructionJulian Büning
2020-10-09fix: fabs() working on the wrong argumentDavid Laprell
2020-09-26Replace llvm::CallSite with llvm::CallBase on LLVM 8+Lukas Zaoral
This is in preparation for LLVM 11 as the llvm:CallSite class has been removed.
2020-09-02More robust handling of unknown intrinsicsAlastair Reid
- If an unknown intrinsic appears in the bitcode file, it is reported but execution can proceed. - If an unknown intrinsic is encountered during execution of some path, - the intrinsic is reported - this path is treated as an error - execution of other paths can proceed To be more precise, there is a list of "known unknown intrinsics". Intrinsics not on this list will prevent execution.
2020-07-30introduce --rng-initial-seed=<unsigned>Frank Busse
* move global theRNG into Executor * pass theRNG via ctor to searchers * remove some type warnings from RNG.cpp Fixes #1023.
2020-07-01Use constraint sets and separate metadata for timing solver invocationMartin Nowack
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)
2020-07-01Use `unique_ptr` for solver in timing solverMartin Nowack
2020-07-01Separate constraint set and constraint managerMartin Nowack
2020-06-29Implement fshr/fshl intrinsicsAlastair Reid
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
2020-06-25Enforce fork/branch limits in branch() and fix double terminationFrank Busse
* 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()).
2020-06-25fix Executor: initializeGlobalAliasesJulian Büning
2020-06-25Executor: consolidate initialization of global objectsJulian Büning
2020-06-25Executor: light refactoring of {allocate,initialize}GlobalObjectsJulian Büning
mainly range-based for, code deduplication
2020-06-25Executor: split initializeGlobalsJulian Büning
2020-06-24print stateID with --debug-print-instructionsFrank Busse
2020-06-24add ExecutionState IDsFrank Busse
* add getID()/setID() * use ExecutionStateIDCompare in Executor::states set * output state id in .err files
2020-06-19Correctly copy variadic arguments with byval attributeCristian Cadar
2020-06-19Renamed loop index from "i" to "k" in executeCall() so that we can reuse ↵Cristian Cadar
"Instruction *i" declared at the beginning of the function. Reformatted this function.
2020-04-30Moved header files that were placed directly in include/klee/ into ↵Cristian Cadar
appropriate existing directories and a new directory Statistics; a few missing renames.
2020-04-30Removed include/klee/util and moved header files to appropriate placesCristian Cadar
2020-04-30Created include/klee/Core directory and moved appropriate files direc\Cristian Cadar
tly in lib/Core
2020-04-30Move header files from lib/Expr to include/klee/Expr to eliminate includes ↵Cristian Cadar
using "../"
2020-04-30Removed the Internal directory from include/kleeCristian Cadar
2020-02-19Use `ref<>` for MemoryObject handlingMartin Nowack
This uses the `ref<>`-based memory handling of MemoryObjects. This makes it explicit that references are held in: - ExecutionState::symbolics - ObjectState
2019-12-13Remove unnecessary std::move's that prevent copy elisionCristian Cadar
2019-12-12[Searchers] Remove weight from es, add nurs_depthTimotej Kapus
Having both weight and depth in execution state is wasteful, therefore this patch removes weight. The nurs:depth searcher is replaced by nurs:rp, which uses pow to compute the weight A new nurs:depth searcher is introduced that biases the search with depth, making it the only other searcher that prefers to go deep (similar to dfs).
2019-11-28Move merging related code from Executor into MergingSearcherLukas Wölfer
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de>
2019-11-05Core: Executor, remove unused variableJiri Slaby
numSeeds is unused since commit 4eb050e2999b (ExecutorTimers: refactor and move to support lib), so remove it.
2019-11-05Mark all constant global memory objects as constantMartin Nowack
Fixes #264. We first aggregate all constant memory objects initialise them and initialise their counter parts in the concrete memory. After that, we mark memory objects as constant such that they can't be modified (i.e. this includes marking them symbolic).
2019-11-04Remove the duplicated check for DebugInfoIntrinsicHui Peng
2019-10-31Executor: fix missing default case in switch instructionFrank Busse
2019-10-29ExecutorTimers: refactor and move to support libFrank Busse
- 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)
2019-09-20refactor PTree: remove split(), add attach() methodFrank Busse
2019-09-03Moved solver-related header files into a separate klee/Solver/ directory.Cristian Cadar
2019-08-15ExecutorTimers: move dumpStates/dumpPTree into ExecutorFrank Busse
* creates two new methods: dumpStates, dumpPTree
2019-07-30Consolidated Expr-related include files into a single include/klee/Expr ↵Cristian Cadar
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
2019-05-30ExecutionState: remove fnAliasesJulian Büning
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-13 21:30:14 +0000