about summary refs log tree commit diff homepage
path: root/tools
AgeCommit message (Collapse)Author
2022-01-07klee-stats: add --print-columnsFrank Busse
2022-01-07klee-stats: do not print summary line for csv/readable-csvFrank Busse
2022-01-07klee-stats: fix BCov calculation for zero br instructionsFrank Busse
2022-01-07klee-stats: rename/reorder/document columnsFrank Busse
* rename columns for consistency * reorder columns and group by "categories" * add missing documentation * fix existing documentation * show MaxMem as float
2022-01-05Do not use stat64 directly in gen-random-boutCristian Cadar
2021-12-20llvm13: llvm::cl::GeneralCategory is no longer a globalLukas Zaoral
Therefore, llvm::cl::getGeneralCategory() should be used instead. See: https://reviews.llvm.org/D105959
2021-11-02ktest-tool: --extract: warn if object can't be foundFrank Busse
2021-11-02klee-stats: order remaining columns alphabeticallyFrank Busse
2021-10-27tools/klee: Warn if module and host target triples differLukas Zaoral
... as running a bitcode with a different target triple may result in unexpected crashes or assertion violations.
2021-05-04differentiate between partial and completed paths in summary and fix paths ↵Frank Busse
stats when not dumping states
2021-04-29Fix erroneous klee-stats legend for --print-allJordy Ruiz
Only absolute times were displayed, and were marked as %. Fixes CexCacheTime, ForkTime and ResolveTime columns.
2021-04-18klee-replay: Fix -Wformat-truncation warningLukas Zaoral
Increase the size of the buffer to PATH_MAX in create_link as that is the maximal possible length of fname and check whether output truncation occurred. Fixes: tools/klee-replay/file-creator.c: In function 'create_file': tools/klee-replay/file-creator.c:55:31: warning: '%s' directive output may be truncated writing up to 4095 bytes into a region of size 64 [-Wformat-truncation=] 55 | snprintf(buf, sizeof(buf), "%s.lnk", fname); | ^~ ...... 344 | target = tmpname; | ~~~~~~~ In file included from /usr/include/stdio.h:866, from tools/klee-replay/file-creator.c:16: /usr/include/bits/stdio2.h:70:10: note: '__snprintf_chk' output between 5 and 4100 bytes into a destination of size 64 70 | return __builtin___snprintf_chk (__s, __n, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 71 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2021-02-16add klee_messages for C++ exception handling supportJulian Büning
otherwise, it is hard to tell whether EH support is available or not
2021-02-16add ifdefs for C++ exception handlingJulian Büning
restoring old behavior without EH support
2021-02-16renaming 'libcxx' -> 'libc++'Julian Büning
2020-12-04llvm11: Use getCalledOperand instead of getCalledValueLukas Zaoral
CallBase::getCalledValue has been deprecated by getCalledOperand since LLVM 8 and has been removed in LLVM 11 See: https://reviews.llvm.org/D78882
2020-12-04llvm11: Make conversions from StringRef to std::string explicitLukas Zaoral
The same applies to SmallString. See: llvm/llvm-project@777180a#diff-497ba4c0c527a125d382b51a34f32542
2020-11-11klee-stats: add (readable) csv format (--table-format=readable-csv/csv)Frank Busse
2020-11-11Do not redefine fgetc_unlocked and fputc_unlocked unconditionally.Gleb Popov
2020-11-09Added fortified library (for -D_FORTIFY_SOURCE), to be linked when uclibc is ↵Cristian Cadar
used.
2020-11-04Rename FreeStanding to Freestanding where appropriateMartin Nowack
2020-11-04Link to the different runtime libraries depending on the application to test.Martin Nowack
Currently, only 32bit vs. 64bit is supported.
2020-10-12Exception handling only for LLVM >= 8.0.0Julian Büning
2020-10-12Implemented support for C++ ExceptionsFelix Rath
We implement the Itanium ABI unwinding base-API, and leave the C++-specific parts to libcxxabi. Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de>
2020-09-30klee-stats: fix behaviour for broken/empty DBsFrank Busse
* fill missing columns in rows with None * fill previous rows with None if new column encountered * error for --to-csv when more than one input directory given
2020-09-17[gen-bout] Support multiple symbolic filesTimotej Kapus
2020-09-17Add klee-zesti a ZESTI like wrapper scriptTimotej Kapus
klee-zesti takes concrete arguments, files and stdin of the program under tests converts them to a seed and then runs klee with that seed. This emulates the interface of ZESTI.
2020-08-23klee-stats: check for a run.stats file in the klee-out directory, to prevent ↵Jordy Ruiz
outputting wrong data. When KLEE crashes, it produces an empty info file, so it is not enough to check for the existence of an info file. Previously, table columns would mismatch and return data labeled with the wrong directory names.
2020-07-01Separate constraint set and constraint managerMartin Nowack
2020-06-29Implement fshr/fshl intrinsicsAlastair Reid
Changes: - IntrinsicCleaner accepts fshr/fshl as accepted intrinsics - Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract - Klee/main suppresses warnings about externals that are LLVM reserved (i.e., begin with "llvm.") - New test exercises 32 and 7 bit versions including oversize shift values Test values are based on LLVM's test for fshl/fshr - Changes that depend on existence of fshr/fshl are guarded by #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) or ; REQUIRES: geq-llvm-7.0
2020-04-30Moved header files that were placed directly in include/klee/ into ↵Cristian Cadar
appropriate existing directories and a new directory Statistics; a few missing renames.
2020-04-30Created include/klee/Core directory and moved appropriate files direc\Cristian Cadar
tly in lib/Core
2020-04-30Removed the Internal directory from include/kleeCristian Cadar
2020-04-08stats: rename QueriesConstructs to QueryConstructsFrank Busse
2020-03-31Fixed some messages, particularly Klee -> KLEECristian Cadar
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-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-01-17Add support to provid a specific host address and port for grafana serverMartin Nowack
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-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
2019-11-07Allow main with 3 argumentsCristian Cadar