about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2014-04-04Add the ability to control whether the pretty printer uses line breaksPeter Collingbourne
This change makes it possible to more reliably write unit tests which check that an expression is equivalent to an expected pretty printed string.
2014-04-02Modify the SMT-LIB printer to declare arrays in a deterministic ↵Peter Collingbourne
(alphabetical) order.
2014-03-09Use clang-format to reformat SMT-LIB printer in LLVM style.Peter Collingbourne
2014-02-24Improved help message for make-concrete-symbolic and fixed some typos.Cristian Cadar
2014-02-14Explicitly get the width of the "shift" expression rather than assumingDan Liew
that is the samw width of the "expr" expression. It probably is the same width (it defintely is in SMT-LIB but I'm not sure about STP) but it is probably better to be explicit.
2014-02-14Remove STPBuilder::getShiftBits() which is no longer used.Dan Liew
2014-02-14Fixed overshift of arithmetic right shift by constant so that itDan Liew
overshifts to zero. Test case is included.
2014-02-14Fixed overshift of arithmetic right shift by symbolic so that it overshiftsDan Liew
to zero. Test case is included.
2014-02-14Fixed overshift of logical right shift by constant so that itDan Liew
overshifts to zero. Test case is included.
2014-02-14Fixed overshift of logical right shift by symbolic so that it overshiftsDan Liew
to zero. Test case is included.
2014-02-14Fixed overshifting an expression by a constant so that we overshift toDan Liew
zero. A test case was added for this. In addition the use to vc_bvExtract() was removed for shifting left by an expression because we don't want/need bitmasked behaviour anymore.
2014-02-14Added a test case for testing overshift behaviour of Shl and fixedDan Liew
a bug in the previous commit where 32-bit width was assumed.
2014-02-14Translate shl overshifts into 0Paul Marinescu
The other shift operators still need to be changed
2014-02-14When running with -debug-only=klee_linker do not report the numberDan Liew
of modules left because this information is no longer correct (we no longer shrink the vector).
2014-02-14Refactor cleaning up memory in linkBCA() so that if linking failsDan Liew
then clean up is performed.
2014-02-14Refactor variable name s/RemovedSymbols/SymbolsToRemove/Dan Liew
because "RemovedSymbols" implies that the symbols have already been removed which is misleading because we don't remove until the end.
2014-02-14Correct and tidy up comments.Dan Liew
2014-02-06Fix access of iterators after they have been invalidatedMartin Nowack
Iterators get invalidated after elements of std::vector/set are deleted. Avoid this by remembering which elements need to be deleted and do it after iterating over the data structure.
2014-02-06When using KLEE's built-in Bitcode archive linker do not considerDan Liew
KLEE intrinsics as undefined symbols
2014-02-06Implement const_iterator interface for SpecialFunctionHandler soDan Liew
that clients can access HandlerInfo nicely.
2014-02-06Do not consider llvm intrinsics as undefined symbols in KLEE'sDan Liew
bitcode archive linker.
2014-02-06Improved archive (of bitcode modules) linking performance forDan Liew
LLVM >= 3.3 by effectively reimplementing the linking algorithm used in LLVM <= 3.2. The LLVM specific bitcode archive format has been removed from LLVM >= 3.3 . Now archives are normal system archives that can contain LLVM bitcode modules as well as regular binary object files. The previous commit implemented an approach where ALL the bitcode modules get linked in which can be terribly slow when klee-uclibc gets linked (~600 LLVM modules). Here are the options that I considered to address this: * Use LD with LLVM gold plug-in and call as an external program. I Don't really want to add another dependency to KLEE. It already has enough! * Use the upcomming LLVM linker (lld). Not really an option because at the time of writing there is no support for linking archives of bitcode modules. * Don't use archives at all and just work with modules (i.e. replace uses of llvm-ar with llvm-link and tinker with the flags a little). This isn't so great because the resulting LLVM bitcode module we execute is bigger than it should be. * Reimpelent bitcode archive linking ourselves in a slightly better way. I've gone for the last option This implementation unfortunately loads all bitcode modules into memory first so we can query the module symbols tables. I would prefer to read the archive's index and link in modules on demand but unfortunately although the new Object::Archive interface in LLVM allows iteration over symbols it doesn't provide a way of knowing if that symbol is defined/undefined. This implementation is far from perfect!
2014-02-06Add support for archive and single bc file linkingMartin Nowack
With LLVM 3.3 the linker does not support reading of archive files directly. This brings the support back (based on llvm-mn). Furthermore, linking single bc files or archives with bc and object files mixed is supported as well.
2014-01-17Fix error message for failing linking of librariesMartin Nowack
In case linking of external libraries failed, user would only be informed if KLEE is compiled with assertions enabled. This fix lets KLEE always fail.
2014-01-17Make KLEE fail in case main function is missingMartin Nowack
Existence of main() function is checked with assertion. This check fails if KLEE is compiled in Release mode.
2014-01-12Merge pull request #68 from MartinNowack/feature_kleeInternalFunctionsDan Liew
Feature klee internal functions
2013-12-21Do not install KLEE's internal libraries.Dan Liew
2013-12-19Added a few comments to Executor::getLastNonKleeInternalInstruction()Dan Liew
emphasising that the function cannot be returned from early.
2013-12-19When writing stack traces for bugs write the location in the assembly.llDan Liew
file as well.
2013-12-19If error location information is missing be explicit about it. ThisDan Liew
is more helpful because often the next message is "Now ignoring error at this location". Which is slightly confusing when no location is shown.
2013-12-19Only record debug info into InstructionInfoTable if debug informationDan Liew
is actually available. In addition if doing a DEBUG build then the command line flag -debug-only=klee_missing_debug shows the instructions missing debug information and -debug-only=klee_obtained_debug show the instructions with debug information.
2013-12-19Remove old algorithm for acquiring debug info. Since LLVM 2.7,Dan Liew
debug information is attached directly to most instructions so the simpler algorithm added in 5ecfd6e2fd5becc10be355b3a20d014e76e40518 can be used. Since support for LLVM version < 2.9 has been removed the old algorithm should be removed. This has been tested with LLVM 2.9 and LLVM 3.3
2013-12-19Optimize inlineChecks functionMartin Nowack
* Just iterate over the instructions which use the function to be inlined * Handle each callsite (e.g. CallInst and InvokeInst)
2013-12-19Replicate debug information from checked instructions to checker call.Martin Nowack
2013-12-19Allow to specify KLEE-internal functionsMartin Nowack
KLEE provides runtime library functions to do detection of bugs (e.g. overflow). This runtime functions are not the location of the bugs but it is the next non-runtime library function from the stack. Use the caller inside that function to indicate where the bug is.
2013-12-19Simplify acquisition of debug informtion for instruction info with newer ↵Martin Nowack
LLVM versions With newer LLVM versions (starting with LLVM 2.7) debug information are directly associated as meta data with each instruction. Therefore, debug information can be acquired directly from each instruction.
2013-12-06Remove stoppoint referencesMartin Nowack
2013-12-06Deprecate LLVM 2.8 and lowerMartin Nowack
2013-12-05Fix unitialized valueMartin Nowack
2013-12-05Free used constants if not used anymoreMartin Nowack
Fixes memleak
2013-12-05Fix timer leakMartin Nowack
2013-11-13Fix using assembler addresses for global variablesMartin Nowack
Format of assembler address strings are different with newer LLVM version (They don't have a prefix anymore). This fix takes care of newer LLVM versions (>=3.3) as well.
2013-10-29Merge pull request #26 from delcypher/fix_divide_by_zeroPaul
Fixed bug where divide by zero bugs would only be detected once in a program
2013-10-15command-line option --use-metasmt declared and defined inside #ifdef ↵Hristina Palikareva
SUPPORT_METASMT ... #endif macros
2013-10-11getConstraintLog() of MetaSMTSolver explicitly states that this feature is ↵Hristina Palikareva
not supported; a test case modified to not fail because of this.
2013-10-11Bug fix in MetaSMTBuilderHristina Palikareva
2013-10-11MetaSMT builder, solver and command-line options.Hristina Palikareva
2013-10-11Merge pull request #40 from antiAgainst/intrinsic-trapCristian Cadar
Bugfix: Remove llvm.trap declaration after cleaning all uses.
2013-10-08Remove llvm.trap declaration after cleaning all uses.Lei Zhang
2013-10-08Merge pull request #34 from ddcc/masterCristian Cadar
Replace current implementation of linkWithLibrary()
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-29 02:08:03 +0000