about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.cpp
AgeCommit message (Collapse)Author
2016-01-12Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providingDan Liew
a ``createCoreSolver()`` function. The solver used is set by the new ``--solver-backend`` command line argument. The default is STP. This change necessitated refactoring the MetaSMT stuff. That clearly didn't belong in the Executor! The MetaSMT command line option is now ``--metasmt-backend`` as this only picks the MetaSMT backend. In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed. Note I don't have MetaSMT built on my development machine so I don't know if the MetaSMT stuff even compiles...
2015-12-18Move lib/Solver/SolverStats.h -> include/klee/SolverStats.hDan Liew
so that it is possible to ``#include "klee/util/ArrayExprHash.h"``
2015-12-18Fix memory leaks of ``Array`` objects detected by ASan.Dan Liew
Some of these leaks were introduced by the factory constructor for Array objects (f049ff3bc04daead8c3bb9f06e89e71e2054c82a) but a few others have been around for far longer. This leak was fixed by introducing a ``ArrayCache`` object which has two purposes * Retains ownership of all created ``Array`` objects and destroys them when the ``ArrayCache`` destructor is called. * Mimic the caching behaviour for symbolic arrays that was introduced by f049ff3bc04daead8c3bb9f06e89e71e2054c82a where arrays with the same name and size get "uniqued". The Executor now maintains a ``arrayCache`` member that it uses and passes by pointer to objects that need to construct ``Array`` objects (i.e. ``ObjectState``). This way when the Executor is destroyed all the ``Array`` objects get freed which seems like the right time to do this. For Kleaver the ``ParserImpl`` has a ``TheArrayCache`` member that is used for building ``Array`` objects. This means that the Parser must live as long as the built expressions will be used otherwise we will have a use after free. I'm not sure this is the right design choice. It might be better to transfer ownership of the ``Array`` objects to the root ``Decl`` returned by the parser.
2015-12-17Refactoring: Moving klee_warning/_error functions to ErrorHandling in ↵Martin Nowack
Support directory
2015-06-03Added an option --readable-posix-inputs which is used to turn on/off the CEX ↵Cristian Cadar
preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences.
2015-05-31Make use of prefer-cex optional rather than defaultEric Rizzi
Previously, default Klee would go through every byte in a test case and attempt to bound it to be between 0 and 127, making it human readable. While this may be useful when attempting to understand Klee, it also means that the time required to create large test suites was greatly increased. By making this behavior default off, unsuspecting users won't incur these additional costs.
2015-03-12[Core] Always warn if states get deleted due to memory limitsMartin Nowack
2015-02-27Improved some comments and fixed some formatting issues in the Array factory ↵Cristian Cadar
patch.
2015-02-22Added factory method for Arrays + hid constructors from outside callsEric Rizzi
The way that Arrays were handled in the past led to the possibility of aliasing issues. This occured whenever a new branch discovered an array for the first time. Each branch would create a new instance of the same array without seeing if it had been created before. Therefore, should a new branch encounter the same state as some previous branch, the previous branch's solution wouldn't satisfy the new state since they didn't recognize they were referencing the same array. By creating an array factory that creates a single symbolic array, that problem is handled. Note: Concrete arrays should not be created by the factory method since their values are never shared between branches. The factory works by seeing if an array with a similar hash has been created before (the hash is based on the name and size of array). If there has been it then searches through all of the arrays with the same hash (stored in a vector) to see if there is one with an exact match. If there is one, the address of this previously created equivalent array is returned. Otherwise, the newly created array is unique, it is added to the map, and it's address is returned. This aliasing issue can be seen by comparing the output of the Dogfood/ImmutableSet.cpp test cases with and with out this commit. Both act correctly, but the number of queries making it to the solver in the previous version is much greater 244 vs 211. This is because the UBTree in the CexCachingSolver and the cache in the CachingSolver do not recognize queries whose solutions were previously calculated because it doesn't think the arrays in the two queries are the same. While this does not cause an error, it does mean that extra calls are made.
2014-12-19Merge pull request #168 from willemp/fix-va-args-passing-for-big-typesCristian Cadar
Fix va args passing for big types
2014-12-02Implement :named and let abbreviation modes in ExprSMTLIBPrinterRaimondas Sasnauskas
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET) * Remove the now defunct ExprSMTLIBLetPrinter * Improve performance of ExprSMTLIBPrinter::scan() by keeping track of visited Expr to avoid visiting them again * Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
2014-10-09Fixed passing of long double (and other big types) in var_args on x86_64. ↵Willem
Removed XFAIL tag from the Feature/VarArgLongDouble.c test Fixed Executor to (more) correctly handle the alignment of types larger than 64bit (such as long double) when those are passed in var_args on x86_64. Specifically: From http://www.x86-64.org/documentation/abi.pdf AMD64-ABI 3.5.7p5: Step 7. Align l->overflow_arg_area upwards to a 16 byte boundary if alignment needed by type exceeds 8 byte boundary.
2014-09-14[LLVM3.5] Update for CallSite.h move into IR/.Daniel Dunbar
2014-09-14[Core] Remove support for "--use-asm-addresses".Daniel Dunbar
- I suspect no one is using this feature, and I'm not sure it is well conceived either. Ripping it out for now in lieu of bothering to maintain it.
2014-09-13[Core] Fix implementation of FRem for LLVM 3.3+, which was wrong (caught by ↵Daniel Dunbar
FloatingPointOps.ll).
2014-09-13Small edits to test the Travis CI trigger.Cristian Cadar
2014-09-12[Core] Fix some warnings in -Asserts builds.Daniel Dunbar
2014-07-04Fix regression reported by Michael Esser and Andrew WatsonDan Liew
(independently). In our recently switch to llvm::raw_ostream (and friends) (I think this is d934d983692c8952cdb887cbcd59f2df0001b9c0) we forgot to flush the llvm::raw_string_ostream to the underlying string used for error report files (e.g. test000001.overshift.err) so we would end up writing an empty string to error report files. Also added a test case to catch this.
2014-06-06Merge pull request #129 from ahorn/masterCristian Cadar
Add SimplifyExpressions command line option
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
According to LLVM: lightweight and simpler implementation of streams.
2014-05-19Rename command line option for equality substitutionsahorn
2014-05-12Add SimplifyExpressions command line optionahorn
Allow users to bypass ConstraintManager::simplifyExpr(ref<Expr>).
2014-04-24Renamed GetTotalMemoryUsage to GetTotalMallocUsageMartin Nowack
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-02-24Improved help message for make-concrete-symbolic and fixed some typos.Cristian Cadar
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-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-06Deprecate LLVM 2.8 and lowerMartin Nowack
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-11MetaSMT builder, solver and command-line options.Hristina Palikareva
2013-09-25Merge pull request #25 from paulmar/masterCristian Cadar
Added some of the common *at functions & others to the model. Obey --max-forks in switch statements.
2013-09-25Obey --max-forks in switch statementsPaul Marinescu
2013-09-21Merge pull request #17 from MartinNowack/LLVM33Cristian Cadar
Make KLEE compile with LLVM 2.3.
2013-08-28Merge branch 'CompilerWarnings' of https://github.com/MartinNowack/klee into ↵Cristian Cadar
MartinNowack-CompilerWarnings
2013-08-28Fix constness warnings issued by gcc 4.7Martin Nowack
2013-08-27Handle constant arrays as wellMartin Nowack
2013-08-27Port to LLVM 3.3Martin Nowack
Major changes are: - Switching to llvm-link to build archive files - Use GetMallocUsage instead of GetTotalMemoryUsage (be aware of bug in LLVM 3.3 http://llvm.org/bugs/show_bug.cgi?id=16847) - intrinsic library functions like memcpy/mov/set use weak linkage to be replaced by e.g. uclibc functions - rewrote linking with library - enhanced MemoryLimit test case to check if mallocs were successful
2013-08-14Slight refactor of code initialising memory for argments/environment c-stringsDan Liew
so that it is easier to read.
2013-08-06TimingSolver and constructSolverChain() no longer coupled with pointers to ↵Hristina Palikareva
STPSolver objects. Timeout is now set by the solver at the top of the solver chain rather than by STPSolver.
2013-08-06Renaming solver-related command-line options in order to decouple them from ↵Hristina Palikareva
STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively. Option of running the SMT solver in a separate process (i.e. forked) set to true by default. Options of running SMT solver forked and with optimized divides made available to Kleaver as well.
2013-04-04Patch by Michael Contreras and Jiri Slaby for compiling KLEE with LLVM 3.2Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@178759 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-27Patch by Jonathan Neuschäfer adding a missing newline.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@178168 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-18Patch and test case by Jiri Slaby to handle "initializing globals whenCristian Cadar
a global has an undef fill of holes inside structures." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@177285 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-11Patch by Dan Liew which unifies the solver construction between KLEECristian Cadar
and Kleaver and fixes --use-query-log in Kleaver. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176811 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-06Patch by Tomek Kuchta which adds the --max-stp-time option to Kleaver.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176571 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-29Patch by Tomasz Kuchta that fixes the fragile way in which KLEE and Kleaver ↵Cristian Cadar
options were shared. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173819 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-22Patch by Hristina Palikareva which enables Kleaver to configure theCristian Cadar
solver chain. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173180 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-13 07:30:31 +0000