about summary refs log tree commit diff homepage
path: root/lib/Expr
AgeCommit message (Collapse)Author
2023-03-20ConstantArrayExprVisitor: Fix detection of multiple array indicesLukáš Zaoral
Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the `incompatible` flag would not be set. Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected: if ((array1[k] + array2[x] + array2[k]) == 0) Resulting in the following output: KLEE: WARNING: OPT_I: infeasible branch! KLEE: WARNING: OPT_I: successful
2023-03-20ConstantArrayExprVisitor: Deduplicate `visitConcat` and `visitRead`Lukáš Zaoral
2023-03-17[cmake] Use LLVM's CMake functionality onlyMartin Nowack
LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0).
2022-07-24Support arguments of width 128, 256 and 512 bits for external callsPavel
2022-03-17remove obsolete KLEE_LLVM legacy definesJulian Büning
2022-03-17remove LLVM < 6 from sourcesFrank Busse
2021-12-20llvm13: llvm::APInt::toString has been moved to StringExtras.hLukas Zaoral
See: https://reviews.llvm.org/D103888
2020-11-12Casting.h: isa_and_nonnull<>Julian Büning
2020-11-12Ref: implement operator bool()Julian Büning
2020-07-01Clean-up and add documentationMartin Nowack
2020-07-01Separate constraint set and constraint managerMartin Nowack
2020-07-01Move constraint implementation from header to cpp filesMartin Nowack
2020-04-30Moved header files that were placed directly in include/klee/ into ↵Cristian Cadar
appropriate existing directories and a new directory Statistics; a few missing renames.
2020-04-30Removed include/klee/util and moved header files to appropriate placesCristian Cadar
2020-04-30Move header files from lib/Expr to include/klee/Expr to eliminate includes ↵Cristian Cadar
using "../"
2020-04-30Removed the Internal directory from include/kleeCristian Cadar
2020-02-19Use `ref<>` for UpdateNodeMartin Nowack
Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code.
2019-12-12[optimize-array] Fix value transformationTimotej Kapus
Value transformation operates on word instead of byte arrays. That means the Read indicies need to be adjusted to reflect that. Previously IndexCleanerVisitor tried to remove the multiplications in the index to covert byte indicies to word indicies. However as the two added test cases show this is not sufficent. Therefore we remove the IndexCleanerVisistor and just divide the index with word size which should always be correct.
2019-12-12[optimize-array] Fix hole index in buildMixedSelectExprTimotej Kapus
buildMixedSelectExpr was using the byte index for holes in the select condition instead of the word based one. This only occured if there was more than 1 hole.
2019-12-12[optimize-array] Fix hash collisionsTimotej Kapus
The caching maps in ArrayExpr are broken, they only consider hashes and don't check for structural equality. This can lead to hash collisions and invalid Expr replacement. This is especially potetent for UpdateLists, who only put the array name in the hash, so there can be a lot of colisions.
2019-12-12[optimize-array] Fix update list read orderTimotej Kapus
ArrayExprOptimizer read the UpdateList in the wrong order, which meant that it used least recent update instead of the most recent one. This patch fixes this as well as adds a test to illustrate the issue.
2019-09-03Moved solver-related header files into a separate klee/Solver/ directory.Cristian Cadar
2019-08-01Renamed misspelled fileCristian Cadar
2019-07-30Consolidated Expr-related include files into a single include/klee/Expr ↵Cristian Cadar
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
2019-06-04make endif guard naming consistentJulian Büning
2019-06-04make include guard naming consistentJulian Büning
2019-03-19Add Read consistency test case, spellingTimotej Kapus
2019-03-19Fix representation of ReadExpr of equivalent arraysMartin Nowack
ObjectStates can be shared between multiple states. A read expression of a symbolic object can be represented differently depending on previous read expression on the same object. If the read expression uses a symbolic index, all pending updates will become entries in the update list of the object state. If the same object state is read again, with a concrete index, the latest update list item will be referenced, even though it might contain more recent but non-essential updates. If, instead, a concrete read will be executed first, it does not contain the non-essential updates. For both executions, the ReadExpr with a constant index will have two different representations, which is not intented. This patch makes sure, we do not include more recent, non-essential updates for concrete reads. Fixes #921
2019-03-15Placed --rewrite-constraints in the constraint solving categoryCristian Cadar
2019-03-13Placed --use-visitor-hash in the expresion building/printing categoryCristian Cadar
2019-03-13Added --const-array-opt to building&printing expression categoryCristian Cadar
2019-03-13Moved options in ExprSMTLIBPrinter.cpp to the expression building and ↵Cristian Cadar
printing category
2019-03-13Documented options in ExprPPrinter.cpp and placed them into a new option ↵Cristian Cadar
category for building and printing expressions
2019-03-13Consistently use "default=true" and "default=false" instead of "default=on" ↵Cristian Cadar
and "default=off" in --help
2019-03-13Added options in ArrayExprOptimizer.cpp to the constraint solving categoryCristian Cadar
2019-03-13Reordered includes in ArrayExprOptimizer.cpp for consistency with the other ↵Cristian Cadar
files
2018-10-26llvm5: APInt->getSignBit -> getSignMaskJiri Slaby
This was renamed in LLVM commit 54f0462d2b7f, so handle the rename. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: integerPartWidth is from llvm::APFloatBaseJiri Slaby
Otherwise we see: ../lib/Expr/Expr.cpp:331:14: error: no member named 'integerPartWidth' in namespace 'llvm'; did you mean 'llvm::APFloatBase::integerPartWidth'? Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-23Updated an include to reflect a recent filename changeCristian Cadar
2018-10-23Move unrelated function from ReadExpr classMartin Nowack
2018-10-23Avoid unsafe static downcastsMartin Nowack
2018-10-23Modernize codeMartin Nowack
* use `using` instead of typdef * use `collection.empty()` instead of size * use `auto` if clear * use `emplace_back` where useful * use `nullptr` instead of NULL * use `override` if applicable * use `explicit` for constructor to avoid implicit conversion
2018-10-23Move optimization specific headers away from the project include directoryMartin Nowack
Don't pollute the project include directory with optimization specific headers.
2018-10-23Clean-up headersMartin Nowack
Remove unneeded headers from include files
2018-10-23Remove condition check before function invocationMartin Nowack
Conditions are checked inside of `optimizeExpr()` anyway. This simplifies the code a lot.
2018-10-23Move ConstantExpr check inside optimizeExpr functionMartin Nowack
2018-10-23optimizeExpr: return the result as return value instead as function argumentMartin Nowack
simplifies code a lot.
2018-10-23Fixed compilation of array optimization patch with LLVM >= 4.0Cristian Cadar
2018-10-23Added missing headers and clang-format the filesCristian Cadar
2018-10-23Added support for KLEE value-based array optimizationAndrea Mattavelli
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-29 15:08:42 +0000