about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.cpp
AgeCommit message (Collapse)Author
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
2019-05-28Implement handling of the llvm.fabs intrinsicFelix Rath
2019-04-02Fix build of Executor.cpp on FreeBSD.Gleb Popov
2019-03-21drop support for LLVM <= 3.7Julian Büning
2019-03-19Add support to assign debug instructions to optimised codeMartin Nowack
2019-03-19Use debugging information from newer LLVM versionsMartin Nowack
2019-03-19Refactor InstructionInfoTableMartin Nowack
Better debug information
2019-03-17run VerifierPass after optimization and instrumentationJulian Büning
2019-03-15Placed option categories in the klee namespace and options in the anonymous ↵Cristian Cadar
namespace in Executor.cpp
2019-03-15Renamed --seed-out to --seed-file and --seed-out-dir to --seed-dir, and ↵Cristian Cadar
placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace.
2019-03-15Reformatted options and headers in Executor.cpp and did a proofreading pass ↵Cristian Cadar
over all help messages.
2019-03-15Added several options in Executor.cpp to the constraint solving categoryCristian Cadar
2019-03-13Consistently use "default=true" and "default=false" instead of "default=on" ↵Cristian Cadar
and "default=off" in --help
2019-03-12time: add double type for span multiplicationsFrank Busse
2019-03-11Add support for LLVM 8.0Martin Nowack
2019-03-05Renamed "Starting options" to "Startup options" and added a missing space in ↵Cristian Cadar
a help message.
2019-03-05fix Executor::initializeGlobals for aliases pointing to another aliasJulian Büning
2018-12-19Added debugging categoryCristian Cadar
2018-12-19Renamed --stop-after-n-instructions to --max-instructions, as suggested by @251Cristian Cadar
2018-12-19Added some descriptions suggested by @MartinNowack and placed ↵Cristian Cadar
--max-static-... options under the termination category of options
2018-12-19Added option categories for external call policy and termination criteriaCristian Cadar
2018-12-19Created two more option categories: test generation and seeding.Cristian Cadar
2018-11-23Implemented memalign with alignmentLukas Wölfer
2018-11-07Fix bug which resulted in an incorrect warning to be printed.Cristian Cadar
2018-11-05Check for stack overflow in a tested programMartin Nowack
Check if a state reaches the maximum number of stack frames allowed. To be performant, the number of stack frames are checked. In comparison, native execution checks the size of the stack. Still, this is good enough to find possible stack overflows. The limit can be changed with `-max-stack-frames`. The current default is 8192 frames.
2018-11-02Replaced --no-externals and --allow-external-sym-calls with ↵Cristian Cadar
--external-calls, updated tests accordingly, and improved documentation on external calls
2018-10-30Base time API upon std::chronoFrank Busse
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)
2018-10-26llvm5: CallSite.paramHasAttr is indexed from 0Jiri Slaby
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>
2018-10-26llvm5: use MutableArrayRef for APFloat::convertToIntegerJiri Slaby
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>
2018-10-26llvm5: SwitchInst case functions now return pointersJiri Slaby
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>
2018-10-24Added lowering passRafael Zaehl
2018-10-23refactor klee_open_output_file to return std::unique_ptrJulian Büning
and introduce klee_open_compressed_output_file with similar behavior along some other minor improvements
2018-10-23use klee_open_output_file for uncompressed logsJulian Büning
2018-10-23Move optimization specific headers away from the project include directoryMartin Nowack
Don't pollute the project include directory with optimization specific headers.
2018-10-23Remove condition check before function invocationMartin Nowack
Conditions are checked inside of `optimizeExpr()` anyway. This simplifies the code a lot.
2018-10-23Move ConstantExpr check inside optimizeExpr functionMartin Nowack
2018-10-23optimizeExpr: return the result as return value instead as function argumentMartin Nowack
simplifies code a lot.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-14 09:47:32 +0000