about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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`.
2020-01-10Fix update_list_order.cMartin Nowack
2020-01-08Link python3 on macOSCristian Cadar
2020-01-08Upgraded FreeBSD Python packages from 3.6 to 3.7Cristian Cadar
2019-12-19Reorganise Dockerfile to have KLEE user own the build directoryMartin Nowack
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] Hash collision testTimotej Kapus
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-26remove python2 from osx CIFelix Rath
Python 2 should not be needed anymore, so we remove it from osx CI.
2019-11-15Implement @llvm.is.constant() intrinsic handling and add a test for it.Gleb Popov
2019-11-09Compile fd_64.c file of POSIX runtime correctly on FreeBSD - append "64" suffixGleb Popov
to function names.
2019-11-07[expr-visitor] Remove unnecessary allocationTimotej Kapus
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-07Added test for 3-argument main.Cristian Cadar
2019-11-07Allow main with 3 argumentsCristian Cadar
2019-11-05Most libc++ tests require uclibc; add missing REQUIRES statements or remove ↵Cristian Cadar
dependency.
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-05Do not modify strings if they are read-only.Martin Nowack
Hoist increment of `sc` into the loop header. Memory locations can only be written to if they are writeable. Avoid concretising a value by writing it. If the location is not symbolic in the first place. This avoids writing read-only memory locations.
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-05[test] Fix missing includesMartin Nowack
Fix multiple missing includes
2019-11-05runtime: fix for glibc 2.30Jiri Slaby
glibc 2.30 moved definition of getdents64 to dirent_ext.h. Hence, it became visible to us (via dirent.h) and conflicts with our definition: runtime/POSIX/fd_64.c:112:5: error: conflicting types for 'getdents64' int getdents64(unsigned int fd, struct dirent *dirp, unsigned int count) { ^ /usr/include/bits/dirent_ext.h:29:18: note: previous declaration is here extern __ssize_t getdents64 (int __fd, void *__buffer, size_t __length) We use the parameters defined by kernel, not by userspace (libc). Both glibc and uclibc define it as: ssize_t __getdents64 (int fd, char *buf, size_t nbytes) so follow it.
2019-11-04Remove the duplicated check for DebugInfoIntrinsicHui Peng
2019-11-04Use default travis OS X version instead of outdated old oneMartin Nowack
2019-10-31Executor: fix missing default case in switch instructionFrank Busse
2019-10-31enable testing for LLVM 9.0Julian Büning
2019-10-31LLVM 9.0: fourth parameter for @llvm.objectsize()Julian Büning
2019-10-31klee-libc: add bcmpJulian Büning
2019-10-31support compilation against LLVM 9.0Julian Büning
2019-10-29[klee-replay] Fix relative executable pathsTimotej Kapus
2019-10-29Travis: double timeout for MetaSMT testsFrank Busse
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-16Add missing file utility in docker imageMartin Nowack
2019-10-08Executor.h: remove defined functions without implementationFrank Busse
2019-10-07test/Expr/Evaluate2.kquery: add link to issueJulian Büning
2019-10-07fix: make llvm 7.1 knownJulian Büning
2019-10-07test/Feature/SolverTimeout.c: re-enable for Z3Julian Büning
2019-10-07test/lit.cfg: test if current version is knownJulian Büning
2019-10-07test/lit.cfg: use lit_config instead of litJulian Büning
Since LLVM version 3.6.0 or lit version 0.5.0, `lit_config` is the name of the global object, not `lit`.
2019-10-07Do not use klee_range() in regression/2014-09-13-debug-info.c test, as it isGleb Popov
incompatible with klee_prefer_cex. Fixes https://github.com/klee/klee/issues/1161 While there, remove dependence on `sort` utility, which might help porting KLEE Windows eventually.
2019-09-20refactor PTree: use unique_ptrFrank Busse
2019-09-20refactor PTree: remove split(), add attach() methodFrank Busse
2019-09-20Move intrinsics tests to the proper directoryMateusz Naściszewski
2019-09-20Add tests for saturating arithmeticMateusz Naściszewski
2019-09-20Add saturated arithmetic intrinsicsMateusz Naściszewski
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-29 15:38:22 +0000