about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2020-03-01[klee-stats] Do not crash if tabulate is not installed but requestedMartin Nowack
2020-03-01[klee-stats] Refactor writing table into own functionMartin Nowack
2020-03-01[klee-stats] Refactor CSV printout in own functionMartin Nowack
2020-03-01[klee-stats] Check if stats file exist before trying to open itMartin Nowack
Providing a list of directories might sometimes not contain the stats file. Check its existence before trying to access it.
2020-02-24Add leading zeros to genboutTimotej Kapus
2020-02-24fix p-llvm.inc: invocation for monorepo directory layoutJulian Büning
2020-02-24find_llvm.cmake: enable parsing for git versionJulian Büning
2020-02-23Use FreeBSD 11.3-STABLE instead of EoLed 11.2.Gleb Popov
2020-02-23Workaround `pkg` breakage on FreeBSD CI.Gleb Popov
2020-02-19Use `ref<>` for MemoryObject handlingMartin Nowack
This uses the `ref<>`-based memory handling of MemoryObjects. This makes it explicit that references are held in: - ExecutionState::symbolics - ObjectState
2020-02-19Use `ref<>` for UpdateNodeMartin Nowack
Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code.
2020-02-19Clean-up header filesMartin Nowack
* Replace c header with c++ header * remove unneeded header file
2020-02-19Add move assignment operator and move construct for `ref` class.Martin Nowack
2020-02-19Add `ReferenceCounter` struct utilized by ref<>Martin Nowack
Using KLEE's `ref<>` shared ptr requires the referenced object to contain a reference counter to be added and initialised to 0 as part of the constructor. To support better reuse of the `ref<>` ptr add a `ReferenceCounter` struct. Just adding this struct to a new class/struct as member enables reference counting with `ref<>` - no additional counter management needed.
2020-02-19Fix ptr reference invalidation if last reference gets freed before new ↵Martin Nowack
reference assigned.
2020-02-13Use call-by-reference for hash-function invocationMartin Nowack
2020-02-13Replace old TR1 implementations of unordered_map/set with std::* versionsMartin Nowack
TR1 implementation got replaced by the std::* equivalents with C++11. Start to use the standard versions instead of the old ones.
2020-02-13Use a newer Ubuntu 18.04 from the year 2020 to build KLEE DockerimageMartin Nowack
2020-02-13Use a newer Ubuntu 18.04 from the year 2020 to build KLEEMartin Nowack
2020-02-13Update Docker image template for KLEE.Martin Nowack
* Port changes from .Dockerfile to this * install emacs-nox and vim-nox instead of pulling all X dependencies * Clean apt cache
2020-02-13Use system's boost when building metasmt and user newer boolector versionMartin Nowack
2020-02-13Do not wait if SANITIZER_BUILD is emptyMartin Nowack
2020-02-13Add llvm as build dependency of clang in case no system packages are availableMartin Nowack
2020-02-13Add patch support for libcxxMartin Nowack
Building older LLVM/libcxx versions under Ubuntu 18.04 requirer patches
2020-02-13Use git repository to build LLVMMartin Nowack
LLVM changed from svn to github. Use the github mirror to have faster build times. Patches were updated to follow the new structure. Patches also support building underr Ubuntu 18.04
2020-02-13Update ubuntu build dependencies for KLEEMartin Nowack
Build dependencies for different components were tied to a specific Ubuntu version (16.04). Although, they are the same for newer versions as well. By renaming `p-component-linux-ubuntu-16.04.inc` to `p-component-linux-ubuntu.inc`, the script can be used for newer Ubuntu versions as well. Do some minor cleaning up.
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-17Add support to provid a specific host address and port for grafana serverMartin Nowack
2020-01-17Add additional packages to provide an out-of-the-box grafana supportMartin Nowack
2020-01-17Use current values for stats in GrafanaGeorge Ordish
2020-01-17Extended the grafana dashboard.knm17
Added units for some of the data and modified klee-stats source code to provide solver time as a fraction of walltime along with fork, resolve and cexcache time.
2020-01-17Add script to build and upload Grafana Docker imageGeorge Ordish
2020-01-17Add Dockerfile for preconfigured GrafanaGeorge Ordish
This Dockerfile provides a Grafana server with a preconfigured dashboard and a datasource that will connect to klee-stats, as soon as klee-stats is run.
2020-01-17Update objdump script to support python3Martin Nowack
2020-01-17Fixed documentation for command line argument link-llvm-libMartin Nowack
Currently, arbitrary *.bc files or archives containing .bc files (.bca or .a) can be linked using `--link-llvm-lib`. Change documentation of command line argument to make this clear. This feature is useful to keep avoid linking the bitcode libraries with the application as bitcode file in the first place. Fix error message in case library could not be loaded
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>
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 23:29:08 +0000