about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2020-01-28updatecomet
2020-01-19Remove statistics limit from istats.Martin Nowack
Statistics encoded in `run.istats` were limited to a maximum number of 13 due to encoding in a `uint64_t` variable. This approach has multiple limitations: - a maximum number of 13 statistics were allowed - a subtle bug can be triggered if many more statistics are added - independent of the selected statistics for `run.istats` Depending on the linking order, statistics will get a different ID. Previously, the ID was used to shift a `1` to its position marking the statistic as being used. This will lead to undefined behaviour if more than 63 statistics are used. Using an llvm::SmallBitVector instead fixes both problems.
2020-01-18Fix handling of debug information for functionsMartin Nowack
Tracking function locations separately correctly without prefixing it with a directory.
2020-01-13Assume assembly.ll is local to the run.istats fileMartin Nowack
Assuming a `klee-out-*` directory is moved to a different path location, subsequent analysis of the run.istats with KCachegrind focusing on assembly is impossible as the `assembly.ll` cannot be found. The reason is that the absolute path of the object file (assembly.ll) is hard-coded as part of the generated run.istats. To fix this, assume that the file is local to the `run.istats`.
2019-12-13Remove unnecessary std::move's that prevent copy elisionCristian Cadar
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-12-12[Searchers] Remove weight from es, add nurs_depthTimotej 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-28Move merging related code from Executor into MergingSearcherLukas Wölfer
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de>
2019-11-15Implement @llvm.is.constant() intrinsic handling and add a test for it.Gleb Popov
2019-11-07Handle llvm.objectsize explicitlyMartin 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-05Core: Executor, remove unused variableJiri Slaby
numSeeds is unused since commit 4eb050e2999b (ExecutorTimers: refactor and move to support lib), so remove it.
2019-11-05Mark all constant global memory objects as constantMartin 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-04Remove the duplicated check for DebugInfoIntrinsicHui Peng
2019-10-31Executor: fix missing default case in switch instructionFrank Busse
2019-10-31LLVM 9.0: fourth parameter for @llvm.objectsize()Julian Büning
2019-10-31support compilation against LLVM 9.0Julian Büning
2019-10-29ExecutorTimers: refactor and move to support libFrank 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-29ExecutorTimers: remove signalling, fix endless looping forkFrank Busse
- adds -timer-interval threshold for timer checks - fixes #831
2019-10-08Executor.h: remove defined functions without implementationFrank Busse
2019-09-20refactor PTree: use unique_ptrFrank Busse
2019-09-20refactor PTree: remove split(), add attach() methodFrank Busse
2019-09-20Add saturated arithmetic intrinsicsMateusz Naściszewski
2019-09-03Moved solver-related header files into a separate klee/Solver/ directory.Cristian Cadar
2019-09-03Moved ConstructSolverChain.cpp to the Solver library.Cristian Cadar
2019-09-03Renamed CmdLineOptions.cpp to SolverCmdLine.cpp (in line with the associated ↵Cristian Cadar
header SolverCmdLine.h) and moved it to the Solver library.
2019-08-15ExecutorTimers: move dumpStates/dumpPTree into ExecutorFrank Busse
* creates two new methods: dumpStates, dumpPTree
2019-08-14Update basic block iterator after deleting instruction; add test caseMartin Nowack
2019-08-14fixed bug in IntrinsicCleaner trap cleanerMichael Bryman
2019-08-14Replace sprintf with snprintf throughout codebaseCristian Cadar
2019-08-12StatsTracker: switch from TRUNCATE to WAL journal modeFrank Busse
2019-08-01Renamed misspelled fileCristian Cadar
2019-07-30Use #include "klee/..." (instead of #include <klee/...>) consistently.Cristian 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-07-23Refactor ConstraintManager to more modern coding standardsDaniel Schemmel
Eliminates -Wdeprecated-copy warnings Performed clang-format on touched file
2019-07-23Refactor ValueRange to more modern coding standardsDaniel Schemmel
Eliminates -Wdeprecated-copy warnings Performed partia clang-format on touched file
2019-06-04fix some incorrect first linesJulian Büning
2019-06-04make endif guard naming consistentJulian Büning
2019-06-04make include guard naming consistentJulian Büning
2019-06-04Fixed identifiers used in ifdefs to (1) not use reserved names and (2) use a ↵Cristian Cadar
consistent naming convention
2019-06-04Remove parenthesis around returns, as reported and discussed in #891Cristian Cadar
2019-05-31PTree: fix dump() methodFrank Busse
2019-05-30ExecutionState: remove fnAliasesJulian Büning
2019-05-30implement FunctionAliasPassJulian Büning
2019-05-30remove 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-28Implement handling of the llvm.fabs intrinsicFelix Rath
2019-04-04some minor refactoringsFrank Busse
2019-04-04Clean klee-stats, StatsTracker and cmakeTimotej Kapus
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 11:08:14 +0000