about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.cpp
AgeCommit message (Collapse)Author
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.
2018-10-23Make valueOnly parameter of optimizeExpr explicitMartin Nowack
avoid ambiguity of valueOnly parameter
2018-10-23Added support for KLEE value-based array optimizationAndrea Mattavelli
2018-10-23Added support for KLEE index-based array optimizationAndrea Mattavelli
2018-10-16Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file is meant ↵Cristian Cadar
to have only solver options.
2018-09-30Fix a crash when the last running state is terminated during mergingLukas Wölfer
2018-09-18llvm4: PointerType is not SequentialTypeJiri Slaby
So handle the type specially whenever needed. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-18llvm4: APFloat members are functionsJiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-14llvm: make KLEE compile against LLVM 3.9Jiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-07-12llvm38: no rounding in APFloatJiri Slaby
The rounding was removed because it was never needed: llvm-mirror/llvm@ff278be Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-07-04Reorder linking and optimizationsMartin Nowack
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.
2018-05-24remove switch fallthrough in floating point comparisionDaniel Schemmel
2018-05-22Renamed printFileLine to getSourceLocation (as suggested by @delcypher) to ↵Cristian Cadar
reflect the fact that it simply returns a string
2018-05-22Simplified printFileLine by using std::to_string, and removed unneeded ↵Cristian Cadar
version that takes an argument a stream
2018-05-21fix some casts for LLP64 compilersFrank Busse
2018-05-17Abort execution if --only-output-states-covering-new is enabled but its ↵Cristian Cadar
dependency --output-istats is not
2018-05-17Add support for concretizing symbolic objects passed to external functionsTimotej Kapus
2018-05-15Implemented incomplete mergingLukas Wölfer
2018-05-05Fix handling of errno if external functions are invokedMartin Nowack
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
2018-05-01add blockaddress and indirectbr instructionsFrank Busse
2018-04-09doDumpStates: incorrectly increments statsFrank Busse
doDumpStates calls stepInstruction and therefore indirectly increases time and instruction statistics for all dangling (dumped) states. This patch removes the call, but now the timing stats for the last executed state are lost, as StatsTracker::stepInstruction isn't called anymore.
2018-02-18Fail for aggegrations with big endian orderingMartin Nowack
2018-02-18Fix correct element order of InsertElement/ExtractElementMartin Nowack
2018-02-01llvm50: use auto variable instead of SwitchInst::CaseItJiri Slaby
llvm50 changed the semantics of SwitchInst::CaseIt and started using "auto" variable type. So use it here too for all versions greater than 3.4 -- 3.4 does not support this semantics yet. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-11-30Implemented bounded merging functionalityLukas Wölfer
2017-11-30Added pause and continue functionality for states in ExecutorLukas Wölfer
2017-10-25fixing huge allocation size constant to be unsignedDavid Trabish
2017-10-12Removed unnecessary and redundant variableAndrea Mattavelli
2017-10-09Fixed initialization of distance to uncovered instructions when KLEE relies ↵Andrea Mattavelli
on default searchers
2017-08-27Remove unnecessary null pointer checksOscar Deits
Fixes klee/klee#717 delete on null pointer is always safe.
2017-07-26Now that LLVM 2.9 is gone, we can use cl::bits instead of cl::listCristian Cadar
2017-07-25This commit simply moves evalConstant to ExecutorUtil (where ↵Cristian Cadar
evalConstantExpr also resides), as suggested by an old comment.
2017-07-23Remove support for LLVM < 3.4Martin Nowack
Request LLVM 3.4 as minimal requirement for KLEE
2017-07-20Merge pull request #657 from delcypher/vectorized_instructionsCristian Cadar
Implement basic support for vectorized instructions.
2017-07-20Replace assertions of types on LLVM instructions in the Executor with aDan Liew
pass that checks these assertions. This improves several things. * This pass provides more friendly messages than assertions in that it just emits a warning and carries on checking the rest of the instructions. * The takes the checks outside of the Executor's hot path and so avoids checking the same instruction multiple times. Now each instruction is only checked once just before execution starts. The disadvantage of this approach is the check for invariants we expect to hold have been pulled far away from where we expect them to hold. After discussion with @ccadar and @MartinNowack it was decided we will take this hit to readability for better performance and simpler code in the Executor.
2017-07-19Implement basic support for vectorized instructions.Dan Liew
We use LLVM's Scalarizer pass to remove most vectorized code so that the Executor only needs to support the InsertElement and ExtractElement instructions. This pass was not available in LLVM 3.4 so to support that LLVM version the pass has been back ported. To check that the Executor is not receiving vector operand types that it can't handle assertions have been added. There are a few limitations to this implementation. * The InsertElement and ExtractElement index cannot be symbolic. * There is no support for LLVM < 3.4.
2017-07-18Use assembly line for printing debug informationMartin Nowack
Instead of using an id, use the assembly line number executed
2017-07-18Merge pull request #672 from jirislaby/llvm40_static_castsAndrea Mattavelli
llvm: get rid of static_casts from iterators
2017-06-16Added location info for external calls and improved a message.Cristian Cadar
2017-06-15llvm: get rid of static_casts from iteratorsJiri Slaby
In commit b7a6aec4eeb4 (convert iterators using static_cast), I switched all implicit casts to static_cast. It turned out that llvm 4.0 banned casting via static_cast. See e.g. 1e2bc42eb988 in the llvm repo what they do. So similarly to the above commit, change all the casts of iterators to "&*" which is what they do in LLVM. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-06-12llvm: don't use clEnumValEnd for LLVM 4.0Jiri Slaby
It became unnecessary when defining options and mainly undefined. So introduce KLEE_LLVM_CL_VAL_END as suggested by @delcypher. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-06-08Merge pull request #675 from ccadar/varargsAndrea Mattavelli
Fixed typos in comments related to vararg support.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-14 02:10:11 +0000