Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-12-13 | Remove unnecessary std::move's that prevent copy elision | Cristian Cadar | |
2019-12-12 | [optimize-array] Fix value transformation | Timotej 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 buildMixedSelectExpr | Timotej 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 collisions | Timotej 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 order | Timotej 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-12-12 | [Searchers] Remove weight from es, add nurs_depth | Timotej Kapus | |
Having both weight and depth in execution state is wasteful, therefore this patch removes weight. The nurs:depth searcher is replaced by nurs:rp, which uses pow to compute the weight A new nurs:depth searcher is introduced that biases the search with depth, making it the only other searcher that prefers to go deep (similar to dfs). | |||
2019-11-28 | Move merging related code from Executor into MergingSearcher | Lukas Wölfer | |
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de> | |||
2019-11-15 | Implement @llvm.is.constant() intrinsic handling and add a test for it. | Gleb Popov | |
2019-11-07 | Handle llvm.objectsize explicitly | Martin Nowack | |
llvm.objectsize is used in several optimisation during compile time. Lowering these intrinsics took a conservative approach returning always the value for unknown. Instead, lower to the object's real size, if possible. Otherwise, a conservative value is used. Since LLVM 4.0, the function `llvm::lowerObjectSizeCall()` does exactly this. Use this function or preserve the old behaviour for older LLVM versions. | |||
2019-11-05 | Core: Executor, remove unused variable | Jiri Slaby | |
numSeeds is unused since commit 4eb050e2999b (ExecutorTimers: refactor and move to support lib), so remove it. | |||
2019-11-05 | Mark all constant global memory objects as constant | Martin Nowack | |
Fixes #264. We first aggregate all constant memory objects initialise them and initialise their counter parts in the concrete memory. After that, we mark memory objects as constant such that they can't be modified (i.e. this includes marking them symbolic). | |||
2019-11-04 | Remove the duplicated check for DebugInfoIntrinsic | Hui Peng | |
2019-10-31 | Executor: fix missing default case in switch instruction | Frank Busse | |
2019-10-31 | LLVM 9.0: fourth parameter for @llvm.objectsize() | Julian Büning | |
2019-10-31 | support compilation against LLVM 9.0 | Julian Büning | |
2019-10-29 | ExecutorTimers: refactor and move to support lib | Frank Busse | |
- moves timer handling from Executor into support lib - introduces TimerGroup, removes TimerInfo/WriteStatsTimer/UpdateReachableTimer/WriteIStatsTimer classes - removes ExecutorTimers.cpp and ExecutorTimerInfo.h - removes -max-instruction-time flag (see #1114) | |||
2019-10-29 | ExecutorTimers: remove signalling, fix endless looping fork | Frank Busse | |
- adds -timer-interval threshold for timer checks - fixes #831 | |||
2019-10-08 | Executor.h: remove defined functions without implementation | Frank Busse | |
2019-09-20 | refactor PTree: use unique_ptr | Frank Busse | |
2019-09-20 | refactor PTree: remove split(), add attach() method | Frank Busse | |
2019-09-20 | Add saturated arithmetic intrinsics | Mateusz Naściszewski | |
2019-09-03 | Moved solver-related header files into a separate klee/Solver/ directory. | Cristian Cadar | |
2019-09-03 | Moved ConstructSolverChain.cpp to the Solver library. | Cristian Cadar | |
2019-09-03 | Renamed CmdLineOptions.cpp to SolverCmdLine.cpp (in line with the associated ↵ | Cristian Cadar | |
header SolverCmdLine.h) and moved it to the Solver library. | |||
2019-08-15 | ExecutorTimers: move dumpStates/dumpPTree into Executor | Frank Busse | |
* creates two new methods: dumpStates, dumpPTree | |||
2019-08-14 | Update basic block iterator after deleting instruction; add test case | Martin Nowack | |
2019-08-14 | fixed bug in IntrinsicCleaner trap cleaner | Michael Bryman | |
2019-08-14 | Replace sprintf with snprintf throughout codebase | Cristian Cadar | |
2019-08-12 | StatsTracker: switch from TRUNCATE to WAL journal mode | Frank Busse | |
2019-08-01 | Renamed misspelled file | Cristian Cadar | |
2019-07-30 | Use #include "klee/..." (instead of #include <klee/...>) consistently. | Cristian Cadar | |
2019-07-30 | Consolidated 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-07-23 | Refactor ConstraintManager to more modern coding standards | Daniel Schemmel | |
Eliminates -Wdeprecated-copy warnings Performed clang-format on touched file | |||
2019-07-23 | Refactor ValueRange to more modern coding standards | Daniel Schemmel | |
Eliminates -Wdeprecated-copy warnings Performed partia clang-format on touched file | |||
2019-06-04 | fix some incorrect first lines | Julian Büning | |
2019-06-04 | make endif guard naming consistent | Julian Büning | |
2019-06-04 | make include guard naming consistent | Julian Büning | |
2019-06-04 | Fixed identifiers used in ifdefs to (1) not use reserved names and (2) use a ↵ | Cristian Cadar | |
consistent naming convention | |||
2019-06-04 | Remove parenthesis around returns, as reported and discussed in #891 | Cristian Cadar | |
2019-05-31 | PTree: fix dump() method | Frank Busse | |
2019-05-30 | ExecutionState: remove fnAliases | Julian Büning | |
2019-05-30 | implement FunctionAliasPass | Julian Büning | |
2019-05-30 | remove klee_alias_function() | Julian Büning | |
this function can be used to modify the control flow of the program on different paths, enabling self-modifying code. | |||
2019-05-28 | Implement handling of the llvm.fabs intrinsic | Felix Rath | |
2019-04-04 | some minor refactorings | Frank Busse | |
2019-04-04 | Clean klee-stats, StatsTracker and cmake | Timotej Kapus | |
2019-04-04 | Change the .stats format into sqlite3 | Timotej Kapus | |
Improves querying of the .stats file, reduces its size, speeds up reads and writes and has better defined fail behaviour. | |||
2019-04-02 | Add FreeBSD OS triple in RaiseAsm | Gleb Popov | |
2019-04-02 | Handle __assert() function as handleAssertFail. This assert variant is used ↵ | Gleb Popov | |
on FreeBSD | |||
2019-04-02 | Fix build of Executor.cpp on FreeBSD. | Gleb Popov | |