about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2020-03-27Ensure that temp_builder is used when adding constant array value assertion ↵Daniel Grumberg
constraints
2020-03-22StatsTracker: remove NumObjects, fix assignment of and always write ↵Frank Busse
ArrayHashTime * fix binding order for assignments when KLEE_ARRAY_DEBUG enabled * always write ArrayHashTime column to run.stats, assign -1 when KLEE_ARRAY_DEBUG disabled * remove unused NumObjects column from run.stats * remove NumObjects panel from Grafana
2020-03-22[posix-runtime] Simple GET/SET_LK modelTimotej Kapus
2020-03-19Additional test for dealing with vector instructionsCristian Cadar
2020-03-18Added another `ScalarizerLegacyPass` run to remove vectorized code ↵Frederic Kehrein
introduced during the optimization step
2020-03-17Fixed compiler warning when printing variable of type off_tCristian Cadar
2020-03-17stat64 is deprecated on macOS; use stat insteadCristian Cadar
2020-03-10Use -snap VMs on Cirrus for FreeBSDCristian Cadar
2020-03-06Updating KLEE's version post-releaseCristian Cadar
2020-03-03Release notes for 2.1 v2.1 2.1.xCristian Cadar
2020-03-03Set version to 2.1Cristian Cadar
2020-03-02fix lit.cfg: numerical comparison of LLVM version numbersJulian Büning
2020-03-02travis: add LLVM 10.0Julian Büning
2020-03-02test/lit.cfg: add LLVM 10.0Julian Büning
2020-03-02stats: enforce table creationFrank Busse
2020-03-01[klee-stats] Grafana: Limit number of entries to query for column namesMartin Nowack
2020-03-01[klee-stats] Use the last row inserted instead of the row with highest ↵Martin Nowack
Instructions Last `Instructions` is not a good identifier to retrieve the correct row. For the default setup, KLEE will generate two entries with the same last instruction. One before clean-up and one after clean-up (i.e. if states are terminated on halt). Using `rowid` will select the last line.
2020-03-01[klee-stats] Refactor preparing and printing the tableMartin Nowack
The number and order of statistics in klee-stats is hard coded. Moreover, adding new statistics to KLEE lead to crashes. Rewriting that part of the script generalises and streamlines the process. List of changes: * Extend legend: this is used for known columns to provide shorter names * simplify sqlite handling and make it more robust and reading of data * select columns based on internal KLEE names * streamline addition of artificial columns and make it robust * handle the case if different runs should be compared but not all have the same statistics * fix calculation of summary row: - avg of column if column is showing a relative value or avg value - max of column if column is showing a max value - sum of column entries, else
2020-03-01[klee-stats] Check for existence of stats file for Grafana as wellMartin Nowack
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