about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2014-05-29Avoid non-explicit use of functions from std namespace in KLEEMartin Nowack
2014-05-29Remove #include <iostream> to avoid static constructorsMartin Nowack
iostream injects static constructor function into every compilation unit. Remove this to avoid it.
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
According to LLVM: lightweight and simpler implementation of streams.
2014-05-11Fix the logic in ExprSMTLIBPrinter::getSortPeter Collingbourne
This now corresponds to the sorts of the operations we emit, as far as I can tell. Read is one example of an operation that now works correctly (with 1-bit array ranges). It's also possible (but not very useful, and I don't think KLEE can produce it) for other operations such as Add to operate on 1-bit values, and this patch also fixes those.
2014-04-24Fixed order of domain and range in array creation in MetaSMTBuilder.Hristina Palikareva
2014-04-24Fixed creation of arrays with variable domains and ranges in STPBuilder and ↵Hristina Palikareva
MetaSMTBuilder.
2014-04-24Merge pull request #116 from MartinNowack/fix_mallocDan Liew
Fix handling of memory usage in KLEE.
2014-04-24Removed ununsed Executor field in WeightedRandomSearcher to silenceDan Liew
clang warning.
2014-04-24Remove unused pointer to STPSolver in STPSolverImpl to silence clangDan Liew
warning.
2014-04-24Renamed GetTotalMemoryUsage to GetTotalMallocUsageMartin Nowack
2014-04-24Modify klee::util::GetTotalMemoryUsage() so that if the system isDan Liew
not using glibc the malloc usage if computed differently.
2014-04-24Fix handling of memory usage in KLEE.Martin Nowack
Memory usage API in LLVM since 3.3 is not working the way it is intended by KLEE. This ports the pre 3.3. version to KLEE. Fixes the malloc test case.
2014-04-24Asserting that update lists have non-NULL roots within ReadExpr objects (updateHristina Palikareva
lists can have NULL roots, e.g. in MemoryObject instances with concrete contents, where root is allocated lazily only when the updates are required). Also checking whether array updates are typed correctly in UpdateList::extend() rather than in the constructor of UpdateNode (only for update lists with non-NULL roots).
2014-04-16Removing a few more hard-coded values for domains and ranges of Array objectsHristina Palikareva
2014-04-15Associate a domain and range with each arrayPeter Collingbourne
2014-04-14Fix mistake in StatsTracker. It should be reporting process ID butDan Liew
instead it was reporting real user ID of the process.
2014-04-14Replace sys::Process::GetCurrentUserId() with getuid() because itDan Liew
has been removed in LLVM3.4
2014-04-14Do not add SimplifyLibCallsPass for LLVM 3.4 and newer becauseDan Liew
it has been removed. From the LLVM 3.4 release notes: " The library call simplification pass has been removed. Its functionality has been integrated into the instruction combiner and function attribute marking passes. "
2014-04-14Tidy up code by using LLVM's V2 path API only and removing usesDan Liew
of old V1 path API. LLVM2.9 supports LLVM's V2 path API. Because that is the minimum version we support we should just use this API everywhere so we reduce the number of #if LLVM_VERSION_CODE macros and duplicated code.
2014-04-14Add missing include file for LLVM 3.4Martin Nowack
2014-04-14Use SmallString and llvm::sys::path/fs API of LLVM 3.4 becauseMartin Nowack
Old Path API was removed
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.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-12-13 11:36:40 +0000