about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2024-01-30Concretize constants using seed values, when available. Added two tests (w/ ↵Cristian Cadar
and w/o seed extension) based on FP concretization.
2024-01-12Follow-up: applied review comments, implemented meta-data cleanup (one more ↵Tomasz Kuchta
map added to ExecutionState); now storing addresses of MemoryObjects for easier cleanup
2024-01-12Feature: implement single memory object resolution for symbolic addresses.Tomasz Kuchta
This feature implements tracking of and resolution of memory objects in the presence of symbolic addresses. For example, an expression like the following: int x; klee_make_symbolic(&x, sizeof(x), "x"); int* tmp = &b.y[x].z; For a concrete array object "y", which is a member of struct "b", a symbolic offset "x" would normally be resolved to any matching memory object - including the ones outside of the object "b". This behaviour is consistent with symbex approach of exploring all execution paths. However, from the point of view of security testing, we would only be interested to know if we are still in-bounds or there is a buffer overflow. The implemented feature creates and tracks (via the GEP instruction) the mapping between the current symbolic offset and the base object it refers to: in our example we are able to tell that the reference should happen within the object "b" (as the array "y" is inside the same memory blob). As a result, we are able to minimize the symbolic exploration to only two paths: one within the bounds of "b", the other with a buffer overflow bug. The feature is turned on via the single-object-resolution command line flag. A new test case was implemented to illustrate how the feature works.
2024-01-12Renamed PTree to ExecutionTree (and similar)Cristian Cadar
2024-01-12Rename files from PTree to ExecutionTree (and similar)Cristian Cadar
2024-01-12new: persistent ptree (-write-ptree) and klee-ptreeFrank Busse
Introduce three different kinds of process trees: 1. Noop: does nothing (e.g. no allocations for DFS) 2. InMemory: same behaviour as before (e.g. RandomPathSearcher) 3. Persistent: similar to InMemory but writes nodes to ptree.db and tracks information such as branch type, termination type or source location (asm) in nodes. Enabled with -write-ptree ptree.db files can be analysed/plotted with the new "klee-ptree" tool.
2023-09-11Make KDAlloc the default memory allocatorCristian Cadar
2023-09-07Remove broken experimental optimisation for validity (--cex-cache-exp)Cristian Cadar
2023-07-21Add code to only keep in the --help menu the KLEE/Kleaver option categoriesCristian Cadar
2023-07-21Move some options to the klee namespace and declare them in OptionCategories.hCristian Cadar
2023-07-12Replaced --suppress-external-warnings and --all-external-warnings with ↵Cristian Cadar
--external-call-warnings=none|once-per-function|all. This eliminates the ambiguity when both of the old options were set. Added test for the new option.
2023-07-08Combine all `ConstantExpr::toMemory` cases into one.Daniel Schemmel
Note that (as it did previously), this relies on the native types having the same internal representation as the ApInt type.
2023-07-08Using std::memcpy prevents alignment problems and removes an unnecessary ↵Daniel Schemmel
special case
2023-07-06rename Allocator::location_info to Allocator::locationInfo forDaniel Schemmel
consistency
2023-06-26Remove parentheses around klee_ intrinsics from the help menuCristian Cadar
2023-06-26Fixed a couple of spelling issues in the help menuCristian Cadar
2023-06-26Improved help message for --exit-on-error-type=AbortCristian Cadar
2023-06-11SpecialFunctionHandler: use std::array for handlerInfoJulian Büning
2023-06-09Fixed a format specifier pointed to by a compiler warning.Cristian Cadar
2023-06-05make BatchingSearcher more readableJulian Büning
2023-06-05fix BatchingSearcher's disabled time budgetJulian Büning
The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own.
2023-06-05CMake: use built-in FindSQLite3 moduleJulian Büning
available since CMake version 3.14
2023-05-26Improve error message when KDAlloc fails to create a mappingDaniel Schemmel
2023-05-26Use unique_ptr for MemoryManager and avoid re-creating it in the first placeMartin Nowack
No need to re-create and re-alloc all the memory again after execution.
2023-04-21use unique_ptr all throughout the solver chainDaniel Schemmel
2023-04-21use unique_ptr in SolverDaniel Schemmel
2023-04-21use unique_ptr in QueryLoggingSolverDaniel Schemmel
2023-04-21use unique_ptr in IndependentSolverDaniel Schemmel
2023-04-21use unique_ptr in CexCachingSolverDaniel Schemmel
2023-04-21use unique_ptr in AssignmentValidatingSolverDaniel Schemmel
2023-04-21use unique_ptr in CachingSolverDaniel Schemmel
2023-04-21use unique_ptr in StagedSolverImplDaniel Schemmel
2023-04-21use unique_ptr in Z3SolverImplDaniel Schemmel
2023-04-21use unique_ptr in ValidatingSolverDaniel Schemmel
2023-04-21use unique_ptr in STPSolverImplDaniel Schemmel
2023-04-20ensure that the right mt19937 constructor is chosen during overload resolutionDaniel Schemmel
2023-04-20remove unused rng adaptor functionsDaniel Schemmel
2023-04-20use `std::mt19937` instead of the custom implementationDaniel Schemmel
2023-04-06Use newer C++ standard for KLEE's iterators; fixes deprecation warningMartin Nowack
2023-04-06Support disabling compiler warnings; Use with external headersMartin Nowack
2023-04-06Mark variable as potentially unusedMartin Nowack
2023-04-01remove include/klee/Support/IntEvaluation.hDaniel Schemmel
2023-03-30Prevent fallthrough warningDaniel Schemmel
2023-03-27Core/Executor: long double on i686 must be aligned to 4 bytesLukáš Zaoral
According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes. Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes were used. This commit fixes the following out of bound pointer access. ``` $ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc $ klee varalign.bc KLEE: output directory is "/home/lukas/klee/klee-out-19" KLEE: Using Z3 solver backend KLEE: WARNING: undefined reference to function: printf KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17 i1, i2, i3: 1, 2, 3 l1: 4 i4: 5 ld1: 6.000000 KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 499 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ```
2023-03-23stats: add termination class statsFrank Busse
2023-03-23stats: add branch type statsFrank Busse
2023-03-23stats: rename States -> ActiveStates, add StatesFrank Busse
2023-03-23stats: add AllocationsFrank Busse
2023-03-23stats: rename numQueries/Queries -> SolverQueries, add QueriesFrank Busse
2023-03-23stats: add ExternalCallsFrank Busse
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 07:05:45 +0000