about summary refs log tree commit diff homepage
path: root/lib/Core
AgeCommit message (Collapse)Author
2017-11-30Implemented bounded merging functionalityLukas Wölfer
2017-11-30Added pause and continue functionality for states in ExecutorLukas Wölfer
2017-11-24klee_make_symbolic: warn on deprecated usageFrank Busse
* terminates state instead of using assertion for illegal argument number * renames empty names to "unnamed" (otherwise test generation fails) * deprecates two argument version
2017-10-25fixing huge allocation size constant to be unsignedDavid Trabish
2017-10-15Fixed assert in BFSSearcher that does not hold as part of interleaved searcherJulian Büning
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-10-06Removed the word 'unsigned' from integer overflow error messagesAndrew Santosa
2017-10-04Remove Autoconf/Makefile build system and adjust the TravisCIDan Liew
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.
2017-10-03Silenced some warnings about unused variables when assertions are disabled.Cristian Cadar
2017-08-27Remove unnecessary null pointer checksOscar Deits
Fixes klee/klee#717 delete on null pointer is always safe.
2017-08-09Merge pull request #742 from ccadar/foldCristian Cadar
Added checks for div/mod by zero and overshifts in constant expressio…
2017-08-07Untabify this file, which was using a mix of spaces and tabs for alignment.Cristian Cadar
2017-08-07Added checks for div/mod by zero and overshifts in constant expressions. ↵Cristian Cadar
Such div/mod by zero expressions would previously crash KLEE. Added two test cases, one for div/mod by zero, the other for overshift. This fixes the bug reported in #268.
2017-08-04Removed merging searchersLukas Wölfer
2017-07-29Added an optional KInstruction* argument to evalConstant and ↵Cristian Cadar
evalConstantExpr which allows us to print the location associated with the constant in any error messages. Added a test case for the unsupported features for taking the address of a label, which exercises the patch.
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-20Core: TimingSolver, use TimerStatIncrementerJiri Slaby
Do not opencode what we already have in TimerStatIncrementer. This simplifies the code a lot and makes transition to LLVM 4.0 a lot easier. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
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.
2017-06-08Fixed typos in comments related to vararg support.Cristian Cadar
2017-05-30Merge pull request #655 from Mic92/loggingCristian Cadar
Fixed some KLEE messages and added build to .gitignore
2017-05-24Rearchitect ExternalDispatcherDan Liew
Previous changes for LLVM 3.6 using the MCJIT were incredibly hacky. Those changes required creating and destroying the ExternalDispatcher for every call to an external function. This is really bad * It's very poor design. The Executor should not need to know about the internal implementation details of the ExternalDispatcher. * It's likely very inefficient to keep creating and destroying the external dispatcher. The new code does several things. * Moves all of the implementation details into a `ExternalDispatcherImpl` class so that implementation details are not exposed in `ExternalDispatcher.h`. * When using the MCJIT a module is compiled for every (instruction, function) tuple. This is necessary because the MCJIT compiles whole modules at a time and once a module is compiled it cannot be modified and re-compiled. Doing this means we get to reuse already generated code for call sites which hopefully will reduce the overhead of repeatedly executing the same call site. A consequence of this change is that now the dispatcher function name needs to be unique across all modules. To do this we just append the module name because we guarantee that the module name is unique by construction. The code has also been clang-formatted.
2017-05-24llvm: make KLEE compile against LLVM 3.5 and 3.6Richard Trembecký
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>
2017-05-24Remove redundant KLEE prefix while loggingJörg Thalheim
2017-04-09Removed unused variable 'fake_object' in MemoryObjectAndrea Mattavelli
2017-03-23[WIP] Fix bug where stats would not be updated on early exit caused byDan Liew
finding a bug with the `-exit-on-error` option enabled.
2017-03-06Merge pull request #611 from jirislaby/getDirectCallTargetAndrea Mattavelli
Core: explicitly create CallSite from Instruction
2017-03-05Merge pull request #607 from jirislaby/dispatcherAndrea Mattavelli
Core: MCJIT functions need unique names
2017-03-03Merge pull request #613 from ccadar/minor2Andrea Mattavelli
Moved printFileLine() to be part of KInstruction
2017-03-03Moved printFileLine() to be part of KInstructionCristian Cadar
2017-03-01fix for PathOS.idgladtbx
2017-03-01Core: explicitly create CallSite from InstructionJiri Slaby
Newer LLVMs do not allow implicit conversion from Instruction to CallSite. We see this error: Internal/Support/ModuleUtil.h:36:19: note: candidate function not viable: no known conversion from 'llvm::Instruction *' to 'llvm::CallSite' for 1st argument llvm::Function *getDirectCallTarget(llvm::CallSite); ^ So explicitly create a CallSite from Instruction. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-28Core: MCJIT functions need unique namesJiri Slaby
We will use newer MCJIT with newer LLVM versions. But it needs unique names of functions or a wrong function can be called. So prepend "dispatcher_" to function names (even for older LLVMs). Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-28convert iterators using static_castJiri Slaby
Newer versions of LLVM do not allow to implicitly cast iterators to pointers where they point. So convert all such uses to explicit static_cast, the same as LLVM code does. Otherwise we see errors like: lib/Core/Executor.cpp:548:15: error: no viable conversion from 'Module::iterator' (aka 'ilist_iterator<llvm::Function>') to 'llvm::Function *' Function *f = i; ^ ~ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-28Merge pull request #547 from delcypher/fix_alignment_of_alloc_memoryCristian Cadar
Teach KLEE to respect the requested memory alignment of allocated memory
2017-02-25llvm: stop using global contextJiri Slaby
It was marked as deprecated long time ago and finally removed in LLVM 3.9. Remove all uses of getGlobalContext and create our own context. Propagate it all over the code then. [v2] use ctx, not C as name Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-24Teach KLEE to respect the requested memory alignment of globals and stackDan Liew
variables when possible. Previously an alignment 8 was always used which did not faithfully emulate what was either explicitly requested in the LLVM IR or what the default alignment was for the target.
2017-02-21Teach `klee::getDirectCallTarget()` to resolve weak aliases. This isDan Liew
controlled by a new parameter `moduleIsFullyLinked`. When true the linkage type of a weak alias is ignored. It is legal to do this when the module is fully linked because there won't be another function that could override the weak alias. This fixes a previous assertion failure in `klee::getDirectCallTarget()` triggered by the `test/regression/2016-11-24-bitcast-weak-alias.c` test case.
2017-02-14Increased the type size for the stop-after-n-instructions option to avoid ↵Andrea Mattavelli
too strict limitations (LLVM >= 3.0)
2017-02-13Silenced two "control may reach end of non-void function [-Wreturn-type]" ↵Cristian Cadar
compiler warnings, one by adding an assert, and the other by refactoring the choose() function.