Evaluate moving to recent ABC #375
Assignees
Comments
|
I found What process did you use to try and find these files? That's not a negative question; I'm hoping there's a bug in what you did such that it makes it seem easier to move to ABC. |
|
Our |
|
@andrewvaughanj You caught it as I was fixing. See above. Apparently Note that I'm just showing the timestamp when these files were first added. So we have a lower bound on the import date, I guess. |
Agreed! Too many race conditions on this issue 😂 |
The dates for these are: Looks like https://github.com/berkeley-abc/abc/tree/0c6505a2/ might be our winner. The difference of ~1030 characters in many of those distances accounts for the copyright which was added in the STP sources but not in the original. |
|
A bit of background on this. I originally chopped into ABC so we used a bit of it because the compilation times were so long. ABC is massive and, at the time, compiling it was so slow it made developing STP painful. A lot has changed in ABC since I imported it, but not much in the AIG parts we use. So I don't expect changing to the use the current ABC version to alter STP's performance. I got ABC working OK in the extabc_trevor branch. @msoos has an extabc branch, but I don't remember how they differ. Also, I don't remember why we gave up working on it. |
|
Some more history #159 |
|
Haha, wow, so it looks like me, you and Mate have all pretty much done the same work! Links for reference:
@TrevorHansen, please correct me if I'm wrong, but I feel like the only true downside of moving to an "upstream" version of ABC is:
Is this really all that's stopping us? Honestly, there are parts of CVC4's dependancy tree that take longer than ABC (e.g., GLPK). I just built ABC from source on my box (12 Xeon cores @ 3.60GHz): So 20 seconds user vs. 3.5 minutes sequential. However, if you're building STP, you don't need to build ABC for every build -- build it once, put it somewhere, STP's build system should find it. It also probably isn't ideal that we would now be linking in a On #159 there's some discussion about CMake version -- however, STP currently has I'm happy to keep poking around in this area, but honestly, I don't feel like we have any major blockers to ripping-out ABC. |
|
If the binary size is problematic it might be possible to include the ABC sources into our CMake project (with |
|
Given we use submodules for other stuff in STP, I guess it would be reasonable to have a submodule for this (and maybe Bit-Vector) in a That being said, it seems nicer if we could add this a CMake option to ABC -- the project seems pretty active currently, so that might be a nice way to go. |
|
Re build times: sure, we should only need to build libabc once and be done with it. I think Trevor may have referred to something else. @TrevorHansen maybe we are misunderstanding something here? Re submodule: I'd rather not have this as a submodule. Submodules tend to get outdated, just like our current setup. In contrast, with the Thanks Trevor for digging out the histories. Seems like many of us had a go at this. It does indeed seem like not good practice. Perhaps this time around we can really make this work :) Thanks Andrew for picking this up and coordinating efforts! |
|
@msoos what are your thoughts on the size of libabc.a? Is this an issue to you? I’m fine with this being like CMS (i.e., not a submodule): you build it somewhere and point CMake to where you’ve built it. |
|
39MB is not an issue unless this needs to run on some embedded device. I don't expect that to be a requirement, so I think it's good from my end! |
|
Okay, I will move forward with this. I’ll get this wrapped-up and get ABC pulled down as part of CI. I also want to open-up some PRs against ABC to resolve warnings in STP due to ABC headers. However, I don’t want that to block us moving forward, so it is going to come second. |
|
I think it's a good change to make, too. I've been assuming that there are only slight changes to ABC's AIG code since 2007, but perhaps that's not true. @rgov did you notice substantial changes in ABC when you were looking? We might need to re-tune how we use ABC's AIGs. |
|
I did not look at the code, just wrote some scripts to find minimal edit distance across the commit history of each file in order to figure out which commit they were pulled from. I did notice that some files are now considerably different / larger so it's likely that new APIs (and/or documentation comments) were added. I can say most of the files haven't been updated recently, or even in years. |
|
@TrevorHansen shall I attempt to get it working then we can try and assess performance? On that line: do we have a good way to easily measure if anything has made STP slower? Of course, we could re-run parts of SMTCOMP, but has anyone looked at making a “cutdown” performance suite like that, which isn’t running the whole thing? |
|
If ABC's AIG stuff hasn't changed much it's hard to imagine much going wrong. Yes @andrewvaughanj I'm happy to evaluate the performance later. Personally, I use the full QF_BV SMTLIB non-incremental to measure STP's performance. It'd be good to have a more comprehensive but smaller benchmark set, and also to all agree on what constitutes making STP faster/slower, but that seems like a long-term goal. |
|
By the way, there are some issues with the outdated ABC's aig that the security scanner is picking up, so updating to newer version could probably be a benefit from this perspective as well: |
|
FetchContent can be used to easily integrate ABC. But this will require raising the minimum CMake version to 3.11. |
|
Just a short comment: raising the minimum cake version to 3.11 is not a problem at all :) |
Merged
It would be cool, but according to @andrewvaughanj comment we can't. |
|
To save people clicking through: KLEE is currently on 3.5, I don't think that STP's CMake should "outpace" KLEE unless we have a really good reason to. |
6 tasks
MartinNowack
added a commit
to MartinNowack/klee
that referenced
this issue
Mar 22, 2023
This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment))
MartinNowack
added a commit
to MartinNowack/klee
that referenced
this issue
Mar 22, 2023
This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment))
MartinNowack
added a commit
to MartinNowack/klee
that referenced
this issue
Mar 22, 2023
This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment))
ccadar
pushed a commit
to klee/klee
that referenced
this issue
Mar 22, 2023
This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment))
|
While it's almost two years later, we finally managed to increase the minimal required version of CMake on KLEE's side. Thanks for the patience and great solver! |
misonijnik
pushed a commit
to UnitTestBot/klee
that referenced
this issue
Jul 21, 2023
Update the Dockerfile to use the correct path for llvm-110 use mallinfo2 if available Make Uclibc support a runtime option, not a compile-time one. Switch FreeBSD 12 CI to a supported release. cl flags: document default values, remove dead option: --replay-keep-symbolic cmake: try using system installation of GTest if it's present This is a patch that I made few months ago as Fedora forbids bundling and using pieces of software provided by other packages in its repositories but forgot to upstream it at that time. [1] It has been rebased and improved so that it also reflects changes made in klee#1458. This should also make the compilation of unittests easier for our users as they don't need to clone googletest from GitHub anymore and just use package manager in the distro of their choice, provided that the gtest package includes a corresponding CMake module. [1]: https://src.fedoraproject.org/rpms/klee/blob/4c81b78/f/use-system-gtest.patch tests: make function pointer tests more robust Renamed gen-bout to ktest-gen Updated klee-zesti to use ktest-gen instead of gen-bout Updated tests to use ktest-gen instead of gen-bout Renamed gen-random-bout to ktest-randgen Updated tests to use ktest-randgen instead of gen-random-bout Utilise Docker build artifact cache for more components Switch to newer KLEE uClibc release Instead of using a branch that doesn't allow build artifact caching, use the newer released version instead. tests: invoke LLVM tools through their corresponding macros Update SpecialFunctionHandler.cpp use size() to get N in bind(), just like the way in prepare(). .err files: minor readability changes to stack trace output tests: add StackTraceOutput.c Spelling Fixes Update Dockerfile to install tabulate Install tabulate package for klee-stats to work when used within KLEE Docker. Use `klee` user to install system dependencies As a follow-up to recent build script enhancements (klee@818275b), finally build KLEE inside of the Docker image as artefact owned by the `klee` user, including user-installed Python3 modules. This fixes issues with non-writable build directories. In addition `$HOME/.local/bin` directory is made available in search path. Intrinsics: Add support for @llvm.f{ma,muladd}.f* Fix error with empty EntryPoint Define stat64 to be stat on MacOS. This fixes compilation on more recent macOS versions, where stat64 is not defined anymore. Implement getArrayForUpdate iteratively Remove the CI target metaSMT(Boolector). metaSMT(STP) already runs the test suite with all solvers supported by metaSMT, so the extra target provides marginal benefits. forward ci environment variables used to exercise metasmt backends into the docker container Perform coverage analysis for z3 as well remove LLVM < 9 rename CallSite to CallBase update github checkout action to v3 checkout KLEE with depth > 1 when running codecov Fix memory leak in crosscheck core solver mechanism Inline asm external call POSIX runtime: fstatat: check for nonnull path APIs Switch FreeBSD CI to 13.1 and Python 3.9 Support arguments of width 128, 256 and 512 bits for external calls Corrected wrong usage of klee_report_error in __cxa_atexit handler Use true instead of Z3_TRUE (removed in z3 4.11.0) Support UBSan-enabled binaries Introduce separate categories for different kinds of undefined behavior Remove LLVM version < 6 Check extensions of generated files in tests Remove LLVM version < 9 Eliminate .undefined_behavior.err category and simplify tests Add README to UBSan runtime Improve pattern for FileCheck in UBSan's tests Improve pattern for FileCheck in UBSan's tests Add notes about how to keep in sync runtime with LLVM project Pass llvm.experimental.noalias.scope.decl to IntrinsicLowering so that it strips out these intrinsics Improve the message for when large arrays become symbolic. Only print this warning once per array. Add test case. fix FileCheck cmd of VarArgByVal test Fixed some leaks in klee-replay add missing FileCheck command to test fix output check in test const_arr_opt1 Use LLVM 11 for FreeBSD testing (package llvm90 is not available anymore) Add an extra check to test/Runtime/FreeStanding/memcpy_chk_err.c ensuring that a call to __memcpy_chk is emitted Disable memcpy_chk_err.c on FreeBSD, where a call to __memcpy_chk is not generated Fix integer overflow create klee-last as a relative link Add a few simple solver tests Have the STP coverage build also provide Z3, so that the crosscheck solver can also be tested Do not escape "@". This triggers an error now in the CI. The KDAlloc slot allocator is useful for small sized allocations The KDAlloc loh allocator is useful for variable sized (large) allocations Add the KDAlloc allocator using both of its suballocators Add some unit tests for KDAlloc Integrate KDAlloc into KLEE Add some system tests for KDAlloc Fixed a bug in KLEE libc's implementation of strcmp: according to the C standard, characters should be compared as unsigned chars. [cmake] Use LLVM's CMake functionality only LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0). Use bitcode library paths via config generation instead of `-D` flags Fix compiler warning with newer compilers [MemSan] Mark memory objects modified by syscalls as initialised Update build scripts * Support for Ubuntu 22.04 * Remove support for Python2 * Better separation between sanitizer builds and non-sanitizer builds * Fix build of metaSMT on newer Ubuntu versions * Use ninja to build LLVM * Simplifying building arbitrary LLVM configurations, e.g. different LLVM sanitizer builds (MemSan, UBSan, ASan) * Use MemSan with origin tracking * Build sqlite3 container correctly * Add support to provide sqlite3 version number Add support to disable memsan instrumentation; update UB/Asan suppression Fix building of runtime library and klee-replay Former build system provided additional flags for building bitcode while they were not required, e.g. under BSD or MacOS. Fix uninitialised memory access while reading last path entry `>>` can fail and sets internal error information in the istream. Check the state of istream before pushing the value onto the buffer. Disable `const_array_opt1` for ubsan as well Don't fail `KleeStats.c` test if it takes 1s or longer Use newer LLVM_DIR config option to build FreeBSD Update Docker build components * Use Ubuntu 22.04 * Use newer TCMalloc 2.9.1 * use Z3 4.8.15 * Use SQLite 3400100 Fix script to build all the containers we require for GitHub actions Update CI components * Use Ubuntu 22.04 instead of 18.04 * Use LLVM 11 instead of 9 * Use TCMalloc 2.9.1 * Use Z3 4.8.15 * Use Sqlite3 3400100 Clean-up comments and structure to satisfy yaml linter Update KDAlloc unittests llvm14: Add LLVM 14 to lit.cfg llvm14: Add LLVM 14 job to GitHub Actions llvm14: TargetRegistry.h was moved from Support to MC llvm14: PointerType::getElementType() was deprecated ... for LLVM 14 in [1] and has already been removed from the LLVM 15 branch in [2]. Some changes are only temporary to silence the warning though, as Type::getPointerElementType() is planned to be removed as well. [3] [1] https://reviews.llvm.org/D117885/new/ [2] llvm/llvm-project@d593cf7 [3] https://llvm.org/docs/OpaquePointers.html#migration-instructions llvm14: port test/Feature/VarArgByVal.c to LLVM 14 LLVM 14 has introduced the noundef function argument attribute. ConstantArrayExprVisitor: Deduplicate `visitConcat` and `visitRead` ConstantArrayExprVisitor: Fix detection of multiple array indices Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the `incompatible` flag would not be set. Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected: if ((array1[k] + array2[x] + array2[k]) == 0) Resulting in the following output: KLEE: WARNING: OPT_I: infeasible branch! KLEE: WARNING: OPT_I: successful Explicitly check if 32bit support is enabled for testing Ignore test in the first place, if no 32bit is enabled. Handle fail of KLEE gracefully Under 64bit architecture, a ptr-error might be found. Ignore this for now. Fixed typo klee-stats: improve error message for missing tabulate package Remove hard to understand and debug pcregrep test Require minimal version of CMake 3.16 for KLEE This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment)) use C++17 Change `llvm_map_components_to_libnames` to `llvm_config` CMake function With recent LLVM versions, this should allow to link against dynamic LLVM libraries. STP: add option to switch SAT solver: --stp-sat-solver and set default to CryptoMinisat Added more test cases for --entry-point. EntryPointMissing is currently expected to fail. Run KDAlloc/rusage unittest a few times to allow for swapfile interference remove obsolete header stats: add InhibitedForks stats: add QCacheHits/Misses stats: add ExternalCalls stats: rename numQueries/Queries -> SolverQueries, add Queries stats: add Allocations stats: rename States -> ActiveStates, add States stats: add branch type stats tests: add Feature/KleeStatsBranches.c stats: add termination class stats tests: add Feature/KleeStatsTermClasses.c Remove model_version from the POSIX runtime, as we have never used it. fix unused variable warning Transition to GitHub Container Registry hosting Fix detection and installation of Ubuntu-provided llvm/clang packages fix unused variables warning tests: add some missing headers (gcc-13) include cstdint for *int*_t Otherwise we see errors like this with gcc13: include/klee/Statistics/Statistic.h:31:10: error: no type named 'uint32_t' in namespace 'std' Core/Executor: long double on i686 must be aligned to 4 bytes According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes. Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes were used. This commit fixes the following out of bound pointer access. ``` $ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc $ klee varalign.bc KLEE: output directory is "/home/lukas/klee/klee-out-19" KLEE: Using Z3 solver backend KLEE: WARNING: undefined reference to function: printf KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17 i1, i2, i3: 1, 2, 3 l1: 4 i4: 5 ld1: 6.000000 KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 499 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ``` ci(lint): add shell linter - Differential ShellCheck It performs differential ShellCheck scans and report results directly in pull request. documentation: https://github.com/redhat-plumbers-in-action/differential-shellcheck Signed-off-by: Jan Macku <jamacku@redhat.com> fix CMake: -UNDEBUG Prevent fallthrough warning remove include/klee/Support/IntEvaluation.h Mark variable as potentially unused Support disabling compiler warnings; Use with external headers Use newer C++ standard for KLEE's iterators; fixes deprecation warning Disable "disabling of warnings" for LLVM >= 14 Modify name of variables in generated cvc files. ci: run ShellCheck on `*.inc` shell scripts change some obsolete KDAlloc comments - mappings were only shared in a former version of KDAlloc - `AllocationFactory(std::size_t, std::uint32_t)`'s second parameter is used for quarantine size, not the location of the mapping use `std::mt19937` instead of the custom implementation remove unused rng adaptor functions ensure that the right mt19937 constructor is chosen during overload resolution Remove additional quotation marks use unique_ptr in STPSolverImpl use unique_ptr in ValidatingSolver use unique_ptr in Z3SolverImpl use unique_ptr in StagedSolverImpl use unique_ptr in CachingSolver use unique_ptr in AssignmentValidatingSolver use unique_ptr in CexCachingSolver use unique_ptr in IndependentSolver use unique_ptr in QueryLoggingSolver use unique_ptr in Solver use unique_ptr all throughout the solver chain Replaced "-data" and "-stat" by "_data" and "_stat" in the ktest-(rand)gen tools for consistency with recent changes. Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency with recent changes. Cleaned up and updated codecov file. Use unique_ptr for MemoryManager and avoid re-creating it in the first place No need to re-create and re-alloc all the memory again after execution. Write `Control::meta` in C++17 style prevent assertions from failing unnecessarily Add `getSize` primitive to kdalloc Add `getMapping` primitive to allocator directly Improve error message when KDAlloc fails to create a mapping Improve LOH deallocation scheme add unsized free to kdalloc Refactored and fixed the code dealing with the entry point. main() should not be processed if the entry point is a different function. This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (klee#1572) Some basic refactoring and pass through comments. In particular, it brings some related code together (deadline with EntryPoint and ReplayPathFile respectively) which was unnecessarily separated. Copy stats to test directory when running tests The sqlite3 databases used for the stats are journalled and potentially must be written to. Therefore, the sqlite3 driver used by `klee-stats` requires write permissions on the database files. By copying the stats files to the test directory, we can now compile and test an out-of-tree build without requiring any write permissions on the source folder at all. CMake: remove unused TARGET_LIBS variable It appears that this variable was never used, already when it was first set in 7e75b49. CMake: remove obsolete KLEE_COMPONENT_EXTRA_LIBRARIES This variable was previously used by `klee_add_component()`, which got removed as part of 3ef5c9d. CMake: remove obsolete comments obsoleted by changes in 3ef5c9d docs/CMakeLists.txt: drop support for old CMake versions minimum CMake version is 3.16.0 as of 3a0e434 README-CMake.md: clean up top-level targets * the old build system is long gone * clean_doxygen was removed by d5cbc20 * clean_runtime was removed by 6156b4e * clean_all was removed by a00424e CMake: use built-in FindSQLite3 module available since CMake version 3.14 doxygen.cfg.in: DOXYGEN_OUTPUT_DIR resolves a FIXME to streamline doxygen.cfg generation a bit .clang-format: c++17 From the `clang-format` documentation: - "`Cpp11` is a deprecated alias for `Latest`" - `Latest`: "Parse and format using the latest supported language version." config.h: include FSTATAT_PATH_ACCEPTS_NULL This variable was introduced by d2f5906 but not included in `config.h` before. As a result `#ifdef` would always fail. Moving the code is necessary to set the variable before `config.h` is created using `configure_file()` in CMakeLists.txt. CMake: use check_c_source_compiles() for FSTATAT_PATH_ACCEPTS_NULL is a bit more convenient and avoids an extra file also check for default CHECK directive in ArrayOpt Tests fix BatchingSearcher's disabled time budget The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own. make BatchingSearcher more readable re-enable StackTraceOutput.c test This test previously had a REQUIRES line with geq-llvm-7.0. Because LLVM version 7.0 is no longer "known" (test/lit.cfg), the required feature is not available and the test is discarded as unsupported by llvm-lit. test/Feature/StackTraceOutput.c: relative checks, clang-format Further improve KDAlloc memory usage with infinite quarantine ktest-gen: remove unused function unittests/CMakeLists.txt: gtest check for LLVM 13+ We previously used `LLVM_EXPORTED_TARGETS` defined in LLVMConfig.cmake. This variable is no longer defined starting from LLVM 13. Alternatively, we use the fact that LLVM's gtest target always depends on LLVMSupport. unittests/CMakeLists.txt: fix LLVM find_package support broken by 3ef5c9d, which removed the "USE_CMAKE_FIND_PACKAGE_LLVM" variable and no longer includes AddLLVM.cmake unittests/CMakeLists.txt: remove obsolete policy Checking for policy CMP0077 is obsolete as we now require CMake 3.16.0 as minimum version. unittests/CMakeLists.txt: no UNITTEST_MAIN_LIBS variable obsoleted by 5607a7f unittests/CMakeLists.txt: do not echo GTEST_SRC_DIR on error This prevents the error message to include the internal "GTEST_SRC_DIR-NOTFOUND" value. unittests/CMakeLists.txt: set gtest include dir only if necessary Use recommended LLVM 13 as part of the Docker image Build and push Docker image as part of a release Fixed end date in the 2.3 release notes Set version number to 3.0 Release notes for KLEE 3.0
misonijnik
pushed a commit
to UnitTestBot/klee
that referenced
this issue
Jul 21, 2023
Update the Dockerfile to use the correct path for llvm-110 use mallinfo2 if available Make Uclibc support a runtime option, not a compile-time one. Switch FreeBSD 12 CI to a supported release. cl flags: document default values, remove dead option: --replay-keep-symbolic cmake: try using system installation of GTest if it's present This is a patch that I made few months ago as Fedora forbids bundling and using pieces of software provided by other packages in its repositories but forgot to upstream it at that time. [1] It has been rebased and improved so that it also reflects changes made in klee#1458. This should also make the compilation of unittests easier for our users as they don't need to clone googletest from GitHub anymore and just use package manager in the distro of their choice, provided that the gtest package includes a corresponding CMake module. [1]: https://src.fedoraproject.org/rpms/klee/blob/4c81b78/f/use-system-gtest.patch tests: make function pointer tests more robust Renamed gen-bout to ktest-gen Updated klee-zesti to use ktest-gen instead of gen-bout Updated tests to use ktest-gen instead of gen-bout Renamed gen-random-bout to ktest-randgen Updated tests to use ktest-randgen instead of gen-random-bout Utilise Docker build artifact cache for more components Switch to newer KLEE uClibc release Instead of using a branch that doesn't allow build artifact caching, use the newer released version instead. tests: invoke LLVM tools through their corresponding macros Update SpecialFunctionHandler.cpp use size() to get N in bind(), just like the way in prepare(). .err files: minor readability changes to stack trace output tests: add StackTraceOutput.c Spelling Fixes Update Dockerfile to install tabulate Install tabulate package for klee-stats to work when used within KLEE Docker. Use `klee` user to install system dependencies As a follow-up to recent build script enhancements (klee@818275b), finally build KLEE inside of the Docker image as artefact owned by the `klee` user, including user-installed Python3 modules. This fixes issues with non-writable build directories. In addition `$HOME/.local/bin` directory is made available in search path. Intrinsics: Add support for @llvm.f{ma,muladd}.f* Fix error with empty EntryPoint Define stat64 to be stat on MacOS. This fixes compilation on more recent macOS versions, where stat64 is not defined anymore. Implement getArrayForUpdate iteratively Remove the CI target metaSMT(Boolector). metaSMT(STP) already runs the test suite with all solvers supported by metaSMT, so the extra target provides marginal benefits. forward ci environment variables used to exercise metasmt backends into the docker container Perform coverage analysis for z3 as well remove LLVM < 9 rename CallSite to CallBase update github checkout action to v3 checkout KLEE with depth > 1 when running codecov Fix memory leak in crosscheck core solver mechanism Inline asm external call POSIX runtime: fstatat: check for nonnull path APIs Switch FreeBSD CI to 13.1 and Python 3.9 Support arguments of width 128, 256 and 512 bits for external calls Corrected wrong usage of klee_report_error in __cxa_atexit handler Use true instead of Z3_TRUE (removed in z3 4.11.0) Support UBSan-enabled binaries Introduce separate categories for different kinds of undefined behavior Remove LLVM version < 6 Check extensions of generated files in tests Remove LLVM version < 9 Eliminate .undefined_behavior.err category and simplify tests Add README to UBSan runtime Improve pattern for FileCheck in UBSan's tests Improve pattern for FileCheck in UBSan's tests Add notes about how to keep in sync runtime with LLVM project Pass llvm.experimental.noalias.scope.decl to IntrinsicLowering so that it strips out these intrinsics Improve the message for when large arrays become symbolic. Only print this warning once per array. Add test case. fix FileCheck cmd of VarArgByVal test Fixed some leaks in klee-replay add missing FileCheck command to test fix output check in test const_arr_opt1 Use LLVM 11 for FreeBSD testing (package llvm90 is not available anymore) Add an extra check to test/Runtime/FreeStanding/memcpy_chk_err.c ensuring that a call to __memcpy_chk is emitted Disable memcpy_chk_err.c on FreeBSD, where a call to __memcpy_chk is not generated Fix integer overflow create klee-last as a relative link Add a few simple solver tests Have the STP coverage build also provide Z3, so that the crosscheck solver can also be tested Do not escape "@". This triggers an error now in the CI. The KDAlloc slot allocator is useful for small sized allocations The KDAlloc loh allocator is useful for variable sized (large) allocations Add the KDAlloc allocator using both of its suballocators Add some unit tests for KDAlloc Integrate KDAlloc into KLEE Add some system tests for KDAlloc Fixed a bug in KLEE libc's implementation of strcmp: according to the C standard, characters should be compared as unsigned chars. [cmake] Use LLVM's CMake functionality only LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0). Use bitcode library paths via config generation instead of `-D` flags Fix compiler warning with newer compilers [MemSan] Mark memory objects modified by syscalls as initialised Update build scripts * Support for Ubuntu 22.04 * Remove support for Python2 * Better separation between sanitizer builds and non-sanitizer builds * Fix build of metaSMT on newer Ubuntu versions * Use ninja to build LLVM * Simplifying building arbitrary LLVM configurations, e.g. different LLVM sanitizer builds (MemSan, UBSan, ASan) * Use MemSan with origin tracking * Build sqlite3 container correctly * Add support to provide sqlite3 version number Add support to disable memsan instrumentation; update UB/Asan suppression Fix building of runtime library and klee-replay Former build system provided additional flags for building bitcode while they were not required, e.g. under BSD or MacOS. Fix uninitialised memory access while reading last path entry `>>` can fail and sets internal error information in the istream. Check the state of istream before pushing the value onto the buffer. Disable `const_array_opt1` for ubsan as well Don't fail `KleeStats.c` test if it takes 1s or longer Use newer LLVM_DIR config option to build FreeBSD Update Docker build components * Use Ubuntu 22.04 * Use newer TCMalloc 2.9.1 * use Z3 4.8.15 * Use SQLite 3400100 Fix script to build all the containers we require for GitHub actions Update CI components * Use Ubuntu 22.04 instead of 18.04 * Use LLVM 11 instead of 9 * Use TCMalloc 2.9.1 * Use Z3 4.8.15 * Use Sqlite3 3400100 Clean-up comments and structure to satisfy yaml linter Update KDAlloc unittests llvm14: Add LLVM 14 to lit.cfg llvm14: Add LLVM 14 job to GitHub Actions llvm14: TargetRegistry.h was moved from Support to MC llvm14: PointerType::getElementType() was deprecated ... for LLVM 14 in [1] and has already been removed from the LLVM 15 branch in [2]. Some changes are only temporary to silence the warning though, as Type::getPointerElementType() is planned to be removed as well. [3] [1] https://reviews.llvm.org/D117885/new/ [2] llvm/llvm-project@d593cf7 [3] https://llvm.org/docs/OpaquePointers.html#migration-instructions llvm14: port test/Feature/VarArgByVal.c to LLVM 14 LLVM 14 has introduced the noundef function argument attribute. ConstantArrayExprVisitor: Deduplicate `visitConcat` and `visitRead` ConstantArrayExprVisitor: Fix detection of multiple array indices Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the `incompatible` flag would not be set. Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected: if ((array1[k] + array2[x] + array2[k]) == 0) Resulting in the following output: KLEE: WARNING: OPT_I: infeasible branch! KLEE: WARNING: OPT_I: successful Explicitly check if 32bit support is enabled for testing Ignore test in the first place, if no 32bit is enabled. Handle fail of KLEE gracefully Under 64bit architecture, a ptr-error might be found. Ignore this for now. Fixed typo klee-stats: improve error message for missing tabulate package Remove hard to understand and debug pcregrep test Require minimal version of CMake 3.16 for KLEE This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment)) use C++17 Change `llvm_map_components_to_libnames` to `llvm_config` CMake function With recent LLVM versions, this should allow to link against dynamic LLVM libraries. STP: add option to switch SAT solver: --stp-sat-solver and set default to CryptoMinisat Added more test cases for --entry-point. EntryPointMissing is currently expected to fail. Run KDAlloc/rusage unittest a few times to allow for swapfile interference remove obsolete header stats: add InhibitedForks stats: add QCacheHits/Misses stats: add ExternalCalls stats: rename numQueries/Queries -> SolverQueries, add Queries stats: add Allocations stats: rename States -> ActiveStates, add States stats: add branch type stats tests: add Feature/KleeStatsBranches.c stats: add termination class stats tests: add Feature/KleeStatsTermClasses.c Remove model_version from the POSIX runtime, as we have never used it. fix unused variable warning Transition to GitHub Container Registry hosting Fix detection and installation of Ubuntu-provided llvm/clang packages fix unused variables warning tests: add some missing headers (gcc-13) include cstdint for *int*_t Otherwise we see errors like this with gcc13: include/klee/Statistics/Statistic.h:31:10: error: no type named 'uint32_t' in namespace 'std' Core/Executor: long double on i686 must be aligned to 4 bytes According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes. Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes were used. This commit fixes the following out of bound pointer access. ``` $ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc $ klee varalign.bc KLEE: output directory is "/home/lukas/klee/klee-out-19" KLEE: Using Z3 solver backend KLEE: WARNING: undefined reference to function: printf KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17 i1, i2, i3: 1, 2, 3 l1: 4 i4: 5 ld1: 6.000000 KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 499 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ``` ci(lint): add shell linter - Differential ShellCheck It performs differential ShellCheck scans and report results directly in pull request. documentation: https://github.com/redhat-plumbers-in-action/differential-shellcheck Signed-off-by: Jan Macku <jamacku@redhat.com> fix CMake: -UNDEBUG Prevent fallthrough warning remove include/klee/Support/IntEvaluation.h Mark variable as potentially unused Support disabling compiler warnings; Use with external headers Use newer C++ standard for KLEE's iterators; fixes deprecation warning Disable "disabling of warnings" for LLVM >= 14 Modify name of variables in generated cvc files. ci: run ShellCheck on `*.inc` shell scripts change some obsolete KDAlloc comments - mappings were only shared in a former version of KDAlloc - `AllocationFactory(std::size_t, std::uint32_t)`'s second parameter is used for quarantine size, not the location of the mapping use `std::mt19937` instead of the custom implementation remove unused rng adaptor functions ensure that the right mt19937 constructor is chosen during overload resolution Remove additional quotation marks use unique_ptr in STPSolverImpl use unique_ptr in ValidatingSolver use unique_ptr in Z3SolverImpl use unique_ptr in StagedSolverImpl use unique_ptr in CachingSolver use unique_ptr in AssignmentValidatingSolver use unique_ptr in CexCachingSolver use unique_ptr in IndependentSolver use unique_ptr in QueryLoggingSolver use unique_ptr in Solver use unique_ptr all throughout the solver chain Replaced "-data" and "-stat" by "_data" and "_stat" in the ktest-(rand)gen tools for consistency with recent changes. Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency with recent changes. Cleaned up and updated codecov file. Use unique_ptr for MemoryManager and avoid re-creating it in the first place No need to re-create and re-alloc all the memory again after execution. Write `Control::meta` in C++17 style prevent assertions from failing unnecessarily Add `getSize` primitive to kdalloc Add `getMapping` primitive to allocator directly Improve error message when KDAlloc fails to create a mapping Improve LOH deallocation scheme add unsized free to kdalloc Refactored and fixed the code dealing with the entry point. main() should not be processed if the entry point is a different function. This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (klee#1572) Some basic refactoring and pass through comments. In particular, it brings some related code together (deadline with EntryPoint and ReplayPathFile respectively) which was unnecessarily separated. Copy stats to test directory when running tests The sqlite3 databases used for the stats are journalled and potentially must be written to. Therefore, the sqlite3 driver used by `klee-stats` requires write permissions on the database files. By copying the stats files to the test directory, we can now compile and test an out-of-tree build without requiring any write permissions on the source folder at all. CMake: remove unused TARGET_LIBS variable It appears that this variable was never used, already when it was first set in 7e75b49. CMake: remove obsolete KLEE_COMPONENT_EXTRA_LIBRARIES This variable was previously used by `klee_add_component()`, which got removed as part of 3ef5c9d. CMake: remove obsolete comments obsoleted by changes in 3ef5c9d docs/CMakeLists.txt: drop support for old CMake versions minimum CMake version is 3.16.0 as of 3a0e434 README-CMake.md: clean up top-level targets * the old build system is long gone * clean_doxygen was removed by d5cbc20 * clean_runtime was removed by 6156b4e * clean_all was removed by a00424e CMake: use built-in FindSQLite3 module available since CMake version 3.14 doxygen.cfg.in: DOXYGEN_OUTPUT_DIR resolves a FIXME to streamline doxygen.cfg generation a bit .clang-format: c++17 From the `clang-format` documentation: - "`Cpp11` is a deprecated alias for `Latest`" - `Latest`: "Parse and format using the latest supported language version." config.h: include FSTATAT_PATH_ACCEPTS_NULL This variable was introduced by d2f5906 but not included in `config.h` before. As a result `#ifdef` would always fail. Moving the code is necessary to set the variable before `config.h` is created using `configure_file()` in CMakeLists.txt. CMake: use check_c_source_compiles() for FSTATAT_PATH_ACCEPTS_NULL is a bit more convenient and avoids an extra file also check for default CHECK directive in ArrayOpt Tests fix BatchingSearcher's disabled time budget The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own. make BatchingSearcher more readable re-enable StackTraceOutput.c test This test previously had a REQUIRES line with geq-llvm-7.0. Because LLVM version 7.0 is no longer "known" (test/lit.cfg), the required feature is not available and the test is discarded as unsupported by llvm-lit. test/Feature/StackTraceOutput.c: relative checks, clang-format Further improve KDAlloc memory usage with infinite quarantine ktest-gen: remove unused function unittests/CMakeLists.txt: gtest check for LLVM 13+ We previously used `LLVM_EXPORTED_TARGETS` defined in LLVMConfig.cmake. This variable is no longer defined starting from LLVM 13. Alternatively, we use the fact that LLVM's gtest target always depends on LLVMSupport. unittests/CMakeLists.txt: fix LLVM find_package support broken by 3ef5c9d, which removed the "USE_CMAKE_FIND_PACKAGE_LLVM" variable and no longer includes AddLLVM.cmake unittests/CMakeLists.txt: remove obsolete policy Checking for policy CMP0077 is obsolete as we now require CMake 3.16.0 as minimum version. unittests/CMakeLists.txt: no UNITTEST_MAIN_LIBS variable obsoleted by 5607a7f unittests/CMakeLists.txt: do not echo GTEST_SRC_DIR on error This prevents the error message to include the internal "GTEST_SRC_DIR-NOTFOUND" value. unittests/CMakeLists.txt: set gtest include dir only if necessary Use recommended LLVM 13 as part of the Docker image Build and push Docker image as part of a release Fixed end date in the 2.3 release notes Set version number to 3.0 Release notes for KLEE 3.0
misonijnik
pushed a commit
to UnitTestBot/klee
that referenced
this issue
Jul 21, 2023
Update the Dockerfile to use the correct path for llvm-110 use mallinfo2 if available Make Uclibc support a runtime option, not a compile-time one. Switch FreeBSD 12 CI to a supported release. cl flags: document default values, remove dead option: --replay-keep-symbolic cmake: try using system installation of GTest if it's present This is a patch that I made few months ago as Fedora forbids bundling and using pieces of software provided by other packages in its repositories but forgot to upstream it at that time. [1] It has been rebased and improved so that it also reflects changes made in klee#1458. This should also make the compilation of unittests easier for our users as they don't need to clone googletest from GitHub anymore and just use package manager in the distro of their choice, provided that the gtest package includes a corresponding CMake module. [1]: https://src.fedoraproject.org/rpms/klee/blob/4c81b78/f/use-system-gtest.patch tests: make function pointer tests more robust Renamed gen-bout to ktest-gen Updated klee-zesti to use ktest-gen instead of gen-bout Updated tests to use ktest-gen instead of gen-bout Renamed gen-random-bout to ktest-randgen Updated tests to use ktest-randgen instead of gen-random-bout Utilise Docker build artifact cache for more components Switch to newer KLEE uClibc release Instead of using a branch that doesn't allow build artifact caching, use the newer released version instead. tests: invoke LLVM tools through their corresponding macros Update SpecialFunctionHandler.cpp use size() to get N in bind(), just like the way in prepare(). .err files: minor readability changes to stack trace output tests: add StackTraceOutput.c Spelling Fixes Update Dockerfile to install tabulate Install tabulate package for klee-stats to work when used within KLEE Docker. Use `klee` user to install system dependencies As a follow-up to recent build script enhancements (klee@818275b), finally build KLEE inside of the Docker image as artefact owned by the `klee` user, including user-installed Python3 modules. This fixes issues with non-writable build directories. In addition `$HOME/.local/bin` directory is made available in search path. Intrinsics: Add support for @llvm.f{ma,muladd}.f* Fix error with empty EntryPoint Define stat64 to be stat on MacOS. This fixes compilation on more recent macOS versions, where stat64 is not defined anymore. Implement getArrayForUpdate iteratively Remove the CI target metaSMT(Boolector). metaSMT(STP) already runs the test suite with all solvers supported by metaSMT, so the extra target provides marginal benefits. forward ci environment variables used to exercise metasmt backends into the docker container Perform coverage analysis for z3 as well remove LLVM < 9 rename CallSite to CallBase update github checkout action to v3 checkout KLEE with depth > 1 when running codecov Fix memory leak in crosscheck core solver mechanism Inline asm external call POSIX runtime: fstatat: check for nonnull path APIs Switch FreeBSD CI to 13.1 and Python 3.9 Support arguments of width 128, 256 and 512 bits for external calls Corrected wrong usage of klee_report_error in __cxa_atexit handler Use true instead of Z3_TRUE (removed in z3 4.11.0) Support UBSan-enabled binaries Introduce separate categories for different kinds of undefined behavior Remove LLVM version < 6 Check extensions of generated files in tests Remove LLVM version < 9 Eliminate .undefined_behavior.err category and simplify tests Add README to UBSan runtime Improve pattern for FileCheck in UBSan's tests Improve pattern for FileCheck in UBSan's tests Add notes about how to keep in sync runtime with LLVM project Pass llvm.experimental.noalias.scope.decl to IntrinsicLowering so that it strips out these intrinsics Improve the message for when large arrays become symbolic. Only print this warning once per array. Add test case. fix FileCheck cmd of VarArgByVal test Fixed some leaks in klee-replay add missing FileCheck command to test fix output check in test const_arr_opt1 Use LLVM 11 for FreeBSD testing (package llvm90 is not available anymore) Add an extra check to test/Runtime/FreeStanding/memcpy_chk_err.c ensuring that a call to __memcpy_chk is emitted Disable memcpy_chk_err.c on FreeBSD, where a call to __memcpy_chk is not generated Fix integer overflow create klee-last as a relative link Add a few simple solver tests Have the STP coverage build also provide Z3, so that the crosscheck solver can also be tested Do not escape "@". This triggers an error now in the CI. The KDAlloc slot allocator is useful for small sized allocations The KDAlloc loh allocator is useful for variable sized (large) allocations Add the KDAlloc allocator using both of its suballocators Add some unit tests for KDAlloc Integrate KDAlloc into KLEE Add some system tests for KDAlloc Fixed a bug in KLEE libc's implementation of strcmp: according to the C standard, characters should be compared as unsigned chars. [cmake] Use LLVM's CMake functionality only LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0). Use bitcode library paths via config generation instead of `-D` flags Fix compiler warning with newer compilers [MemSan] Mark memory objects modified by syscalls as initialised Update build scripts * Support for Ubuntu 22.04 * Remove support for Python2 * Better separation between sanitizer builds and non-sanitizer builds * Fix build of metaSMT on newer Ubuntu versions * Use ninja to build LLVM * Simplifying building arbitrary LLVM configurations, e.g. different LLVM sanitizer builds (MemSan, UBSan, ASan) * Use MemSan with origin tracking * Build sqlite3 container correctly * Add support to provide sqlite3 version number Add support to disable memsan instrumentation; update UB/Asan suppression Fix building of runtime library and klee-replay Former build system provided additional flags for building bitcode while they were not required, e.g. under BSD or MacOS. Fix uninitialised memory access while reading last path entry `>>` can fail and sets internal error information in the istream. Check the state of istream before pushing the value onto the buffer. Disable `const_array_opt1` for ubsan as well Don't fail `KleeStats.c` test if it takes 1s or longer Use newer LLVM_DIR config option to build FreeBSD Update Docker build components * Use Ubuntu 22.04 * Use newer TCMalloc 2.9.1 * use Z3 4.8.15 * Use SQLite 3400100 Fix script to build all the containers we require for GitHub actions Update CI components * Use Ubuntu 22.04 instead of 18.04 * Use LLVM 11 instead of 9 * Use TCMalloc 2.9.1 * Use Z3 4.8.15 * Use Sqlite3 3400100 Clean-up comments and structure to satisfy yaml linter Update KDAlloc unittests llvm14: Add LLVM 14 to lit.cfg llvm14: Add LLVM 14 job to GitHub Actions llvm14: TargetRegistry.h was moved from Support to MC llvm14: PointerType::getElementType() was deprecated ... for LLVM 14 in [1] and has already been removed from the LLVM 15 branch in [2]. Some changes are only temporary to silence the warning though, as Type::getPointerElementType() is planned to be removed as well. [3] [1] https://reviews.llvm.org/D117885/new/ [2] llvm/llvm-project@d593cf7 [3] https://llvm.org/docs/OpaquePointers.html#migration-instructions llvm14: port test/Feature/VarArgByVal.c to LLVM 14 LLVM 14 has introduced the noundef function argument attribute. ConstantArrayExprVisitor: Deduplicate `visitConcat` and `visitRead` ConstantArrayExprVisitor: Fix detection of multiple array indices Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the `incompatible` flag would not be set. Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected: if ((array1[k] + array2[x] + array2[k]) == 0) Resulting in the following output: KLEE: WARNING: OPT_I: infeasible branch! KLEE: WARNING: OPT_I: successful Explicitly check if 32bit support is enabled for testing Ignore test in the first place, if no 32bit is enabled. Handle fail of KLEE gracefully Under 64bit architecture, a ptr-error might be found. Ignore this for now. Fixed typo klee-stats: improve error message for missing tabulate package Remove hard to understand and debug pcregrep test Require minimal version of CMake 3.16 for KLEE This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment)) use C++17 Change `llvm_map_components_to_libnames` to `llvm_config` CMake function With recent LLVM versions, this should allow to link against dynamic LLVM libraries. STP: add option to switch SAT solver: --stp-sat-solver and set default to CryptoMinisat Added more test cases for --entry-point. EntryPointMissing is currently expected to fail. Run KDAlloc/rusage unittest a few times to allow for swapfile interference remove obsolete header stats: add InhibitedForks stats: add QCacheHits/Misses stats: add ExternalCalls stats: rename numQueries/Queries -> SolverQueries, add Queries stats: add Allocations stats: rename States -> ActiveStates, add States stats: add branch type stats tests: add Feature/KleeStatsBranches.c stats: add termination class stats tests: add Feature/KleeStatsTermClasses.c Remove model_version from the POSIX runtime, as we have never used it. fix unused variable warning Transition to GitHub Container Registry hosting Fix detection and installation of Ubuntu-provided llvm/clang packages fix unused variables warning tests: add some missing headers (gcc-13) include cstdint for *int*_t Otherwise we see errors like this with gcc13: include/klee/Statistics/Statistic.h:31:10: error: no type named 'uint32_t' in namespace 'std' Core/Executor: long double on i686 must be aligned to 4 bytes According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes. Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes were used. This commit fixes the following out of bound pointer access. ``` $ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc $ klee varalign.bc KLEE: output directory is "/home/lukas/klee/klee-out-19" KLEE: Using Z3 solver backend KLEE: WARNING: undefined reference to function: printf KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17 i1, i2, i3: 1, 2, 3 l1: 4 i4: 5 ld1: 6.000000 KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 499 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ``` ci(lint): add shell linter - Differential ShellCheck It performs differential ShellCheck scans and report results directly in pull request. documentation: https://github.com/redhat-plumbers-in-action/differential-shellcheck Signed-off-by: Jan Macku <jamacku@redhat.com> fix CMake: -UNDEBUG Prevent fallthrough warning remove include/klee/Support/IntEvaluation.h Mark variable as potentially unused Support disabling compiler warnings; Use with external headers Use newer C++ standard for KLEE's iterators; fixes deprecation warning Disable "disabling of warnings" for LLVM >= 14 Modify name of variables in generated cvc files. ci: run ShellCheck on `*.inc` shell scripts change some obsolete KDAlloc comments - mappings were only shared in a former version of KDAlloc - `AllocationFactory(std::size_t, std::uint32_t)`'s second parameter is used for quarantine size, not the location of the mapping use `std::mt19937` instead of the custom implementation remove unused rng adaptor functions ensure that the right mt19937 constructor is chosen during overload resolution Remove additional quotation marks use unique_ptr in STPSolverImpl use unique_ptr in ValidatingSolver use unique_ptr in Z3SolverImpl use unique_ptr in StagedSolverImpl use unique_ptr in CachingSolver use unique_ptr in AssignmentValidatingSolver use unique_ptr in CexCachingSolver use unique_ptr in IndependentSolver use unique_ptr in QueryLoggingSolver use unique_ptr in Solver use unique_ptr all throughout the solver chain Replaced "-data" and "-stat" by "_data" and "_stat" in the ktest-(rand)gen tools for consistency with recent changes. Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency with recent changes. Cleaned up and updated codecov file. Use unique_ptr for MemoryManager and avoid re-creating it in the first place No need to re-create and re-alloc all the memory again after execution. Write `Control::meta` in C++17 style prevent assertions from failing unnecessarily Add `getSize` primitive to kdalloc Add `getMapping` primitive to allocator directly Improve error message when KDAlloc fails to create a mapping Improve LOH deallocation scheme add unsized free to kdalloc Refactored and fixed the code dealing with the entry point. main() should not be processed if the entry point is a different function. This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (klee#1572) Some basic refactoring and pass through comments. In particular, it brings some related code together (deadline with EntryPoint and ReplayPathFile respectively) which was unnecessarily separated. Copy stats to test directory when running tests The sqlite3 databases used for the stats are journalled and potentially must be written to. Therefore, the sqlite3 driver used by `klee-stats` requires write permissions on the database files. By copying the stats files to the test directory, we can now compile and test an out-of-tree build without requiring any write permissions on the source folder at all. CMake: remove unused TARGET_LIBS variable It appears that this variable was never used, already when it was first set in 7e75b49. CMake: remove obsolete KLEE_COMPONENT_EXTRA_LIBRARIES This variable was previously used by `klee_add_component()`, which got removed as part of 3ef5c9d. CMake: remove obsolete comments obsoleted by changes in 3ef5c9d docs/CMakeLists.txt: drop support for old CMake versions minimum CMake version is 3.16.0 as of 3a0e434 README-CMake.md: clean up top-level targets * the old build system is long gone * clean_doxygen was removed by d5cbc20 * clean_runtime was removed by 6156b4e * clean_all was removed by a00424e CMake: use built-in FindSQLite3 module available since CMake version 3.14 doxygen.cfg.in: DOXYGEN_OUTPUT_DIR resolves a FIXME to streamline doxygen.cfg generation a bit .clang-format: c++17 From the `clang-format` documentation: - "`Cpp11` is a deprecated alias for `Latest`" - `Latest`: "Parse and format using the latest supported language version." config.h: include FSTATAT_PATH_ACCEPTS_NULL This variable was introduced by d2f5906 but not included in `config.h` before. As a result `#ifdef` would always fail. Moving the code is necessary to set the variable before `config.h` is created using `configure_file()` in CMakeLists.txt. CMake: use check_c_source_compiles() for FSTATAT_PATH_ACCEPTS_NULL is a bit more convenient and avoids an extra file also check for default CHECK directive in ArrayOpt Tests fix BatchingSearcher's disabled time budget The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own. make BatchingSearcher more readable re-enable StackTraceOutput.c test This test previously had a REQUIRES line with geq-llvm-7.0. Because LLVM version 7.0 is no longer "known" (test/lit.cfg), the required feature is not available and the test is discarded as unsupported by llvm-lit. test/Feature/StackTraceOutput.c: relative checks, clang-format Further improve KDAlloc memory usage with infinite quarantine ktest-gen: remove unused function unittests/CMakeLists.txt: gtest check for LLVM 13+ We previously used `LLVM_EXPORTED_TARGETS` defined in LLVMConfig.cmake. This variable is no longer defined starting from LLVM 13. Alternatively, we use the fact that LLVM's gtest target always depends on LLVMSupport. unittests/CMakeLists.txt: fix LLVM find_package support broken by 3ef5c9d, which removed the "USE_CMAKE_FIND_PACKAGE_LLVM" variable and no longer includes AddLLVM.cmake unittests/CMakeLists.txt: remove obsolete policy Checking for policy CMP0077 is obsolete as we now require CMake 3.16.0 as minimum version. unittests/CMakeLists.txt: no UNITTEST_MAIN_LIBS variable obsoleted by 5607a7f unittests/CMakeLists.txt: do not echo GTEST_SRC_DIR on error This prevents the error message to include the internal "GTEST_SRC_DIR-NOTFOUND" value. unittests/CMakeLists.txt: set gtest include dir only if necessary Use recommended LLVM 13 as part of the Docker image Build and push Docker image as part of a release Fixed end date in the 2.3 release notes Set version number to 3.0 Release notes for KLEE 3.0
misonijnik
pushed a commit
to UnitTestBot/klee
that referenced
this issue
Jul 21, 2023
Update the Dockerfile to use the correct path for llvm-110 use mallinfo2 if available Make Uclibc support a runtime option, not a compile-time one. Switch FreeBSD 12 CI to a supported release. cl flags: document default values, remove dead option: --replay-keep-symbolic cmake: try using system installation of GTest if it's present This is a patch that I made few months ago as Fedora forbids bundling and using pieces of software provided by other packages in its repositories but forgot to upstream it at that time. [1] It has been rebased and improved so that it also reflects changes made in klee#1458. This should also make the compilation of unittests easier for our users as they don't need to clone googletest from GitHub anymore and just use package manager in the distro of their choice, provided that the gtest package includes a corresponding CMake module. [1]: https://src.fedoraproject.org/rpms/klee/blob/4c81b78/f/use-system-gtest.patch tests: make function pointer tests more robust Renamed gen-bout to ktest-gen Updated klee-zesti to use ktest-gen instead of gen-bout Updated tests to use ktest-gen instead of gen-bout Renamed gen-random-bout to ktest-randgen Updated tests to use ktest-randgen instead of gen-random-bout Utilise Docker build artifact cache for more components Switch to newer KLEE uClibc release Instead of using a branch that doesn't allow build artifact caching, use the newer released version instead. tests: invoke LLVM tools through their corresponding macros Update SpecialFunctionHandler.cpp use size() to get N in bind(), just like the way in prepare(). .err files: minor readability changes to stack trace output tests: add StackTraceOutput.c Spelling Fixes Update Dockerfile to install tabulate Install tabulate package for klee-stats to work when used within KLEE Docker. Use `klee` user to install system dependencies As a follow-up to recent build script enhancements (klee@818275b), finally build KLEE inside of the Docker image as artefact owned by the `klee` user, including user-installed Python3 modules. This fixes issues with non-writable build directories. In addition `$HOME/.local/bin` directory is made available in search path. Intrinsics: Add support for @llvm.f{ma,muladd}.f* Fix error with empty EntryPoint Define stat64 to be stat on MacOS. This fixes compilation on more recent macOS versions, where stat64 is not defined anymore. Implement getArrayForUpdate iteratively Remove the CI target metaSMT(Boolector). metaSMT(STP) already runs the test suite with all solvers supported by metaSMT, so the extra target provides marginal benefits. forward ci environment variables used to exercise metasmt backends into the docker container Perform coverage analysis for z3 as well remove LLVM < 9 rename CallSite to CallBase update github checkout action to v3 checkout KLEE with depth > 1 when running codecov Fix memory leak in crosscheck core solver mechanism Inline asm external call POSIX runtime: fstatat: check for nonnull path APIs Switch FreeBSD CI to 13.1 and Python 3.9 Support arguments of width 128, 256 and 512 bits for external calls Corrected wrong usage of klee_report_error in __cxa_atexit handler Use true instead of Z3_TRUE (removed in z3 4.11.0) Support UBSan-enabled binaries Introduce separate categories for different kinds of undefined behavior Remove LLVM version < 6 Check extensions of generated files in tests Remove LLVM version < 9 Eliminate .undefined_behavior.err category and simplify tests Add README to UBSan runtime Improve pattern for FileCheck in UBSan's tests Improve pattern for FileCheck in UBSan's tests Add notes about how to keep in sync runtime with LLVM project Pass llvm.experimental.noalias.scope.decl to IntrinsicLowering so that it strips out these intrinsics Improve the message for when large arrays become symbolic. Only print this warning once per array. Add test case. fix FileCheck cmd of VarArgByVal test Fixed some leaks in klee-replay add missing FileCheck command to test fix output check in test const_arr_opt1 Use LLVM 11 for FreeBSD testing (package llvm90 is not available anymore) Add an extra check to test/Runtime/FreeStanding/memcpy_chk_err.c ensuring that a call to __memcpy_chk is emitted Disable memcpy_chk_err.c on FreeBSD, where a call to __memcpy_chk is not generated Fix integer overflow create klee-last as a relative link Add a few simple solver tests Have the STP coverage build also provide Z3, so that the crosscheck solver can also be tested Do not escape "@". This triggers an error now in the CI. The KDAlloc slot allocator is useful for small sized allocations The KDAlloc loh allocator is useful for variable sized (large) allocations Add the KDAlloc allocator using both of its suballocators Add some unit tests for KDAlloc Integrate KDAlloc into KLEE Add some system tests for KDAlloc Fixed a bug in KLEE libc's implementation of strcmp: according to the C standard, characters should be compared as unsigned chars. [cmake] Use LLVM's CMake functionality only LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0). Use bitcode library paths via config generation instead of `-D` flags Fix compiler warning with newer compilers [MemSan] Mark memory objects modified by syscalls as initialised Update build scripts * Support for Ubuntu 22.04 * Remove support for Python2 * Better separation between sanitizer builds and non-sanitizer builds * Fix build of metaSMT on newer Ubuntu versions * Use ninja to build LLVM * Simplifying building arbitrary LLVM configurations, e.g. different LLVM sanitizer builds (MemSan, UBSan, ASan) * Use MemSan with origin tracking * Build sqlite3 container correctly * Add support to provide sqlite3 version number Add support to disable memsan instrumentation; update UB/Asan suppression Fix building of runtime library and klee-replay Former build system provided additional flags for building bitcode while they were not required, e.g. under BSD or MacOS. Fix uninitialised memory access while reading last path entry `>>` can fail and sets internal error information in the istream. Check the state of istream before pushing the value onto the buffer. Disable `const_array_opt1` for ubsan as well Don't fail `KleeStats.c` test if it takes 1s or longer Use newer LLVM_DIR config option to build FreeBSD Update Docker build components * Use Ubuntu 22.04 * Use newer TCMalloc 2.9.1 * use Z3 4.8.15 * Use SQLite 3400100 Fix script to build all the containers we require for GitHub actions Update CI components * Use Ubuntu 22.04 instead of 18.04 * Use LLVM 11 instead of 9 * Use TCMalloc 2.9.1 * Use Z3 4.8.15 * Use Sqlite3 3400100 Clean-up comments and structure to satisfy yaml linter Update KDAlloc unittests llvm14: Add LLVM 14 to lit.cfg llvm14: Add LLVM 14 job to GitHub Actions llvm14: TargetRegistry.h was moved from Support to MC llvm14: PointerType::getElementType() was deprecated ... for LLVM 14 in [1] and has already been removed from the LLVM 15 branch in [2]. Some changes are only temporary to silence the warning though, as Type::getPointerElementType() is planned to be removed as well. [3] [1] https://reviews.llvm.org/D117885/new/ [2] llvm/llvm-project@d593cf7 [3] https://llvm.org/docs/OpaquePointers.html#migration-instructions llvm14: port test/Feature/VarArgByVal.c to LLVM 14 LLVM 14 has introduced the noundef function argument attribute. ConstantArrayExprVisitor: Deduplicate `visitConcat` and `visitRead` ConstantArrayExprVisitor: Fix detection of multiple array indices Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the `incompatible` flag would not be set. Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected: if ((array1[k] + array2[x] + array2[k]) == 0) Resulting in the following output: KLEE: WARNING: OPT_I: infeasible branch! KLEE: WARNING: OPT_I: successful Explicitly check if 32bit support is enabled for testing Ignore test in the first place, if no 32bit is enabled. Handle fail of KLEE gracefully Under 64bit architecture, a ptr-error might be found. Ignore this for now. Fixed typo klee-stats: improve error message for missing tabulate package Remove hard to understand and debug pcregrep test Require minimal version of CMake 3.16 for KLEE This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment)) use C++17 Change `llvm_map_components_to_libnames` to `llvm_config` CMake function With recent LLVM versions, this should allow to link against dynamic LLVM libraries. STP: add option to switch SAT solver: --stp-sat-solver and set default to CryptoMinisat Added more test cases for --entry-point. EntryPointMissing is currently expected to fail. Run KDAlloc/rusage unittest a few times to allow for swapfile interference remove obsolete header stats: add InhibitedForks stats: add QCacheHits/Misses stats: add ExternalCalls stats: rename numQueries/Queries -> SolverQueries, add Queries stats: add Allocations stats: rename States -> ActiveStates, add States stats: add branch type stats tests: add Feature/KleeStatsBranches.c stats: add termination class stats tests: add Feature/KleeStatsTermClasses.c Remove model_version from the POSIX runtime, as we have never used it. fix unused variable warning Transition to GitHub Container Registry hosting Fix detection and installation of Ubuntu-provided llvm/clang packages fix unused variables warning tests: add some missing headers (gcc-13) include cstdint for *int*_t Otherwise we see errors like this with gcc13: include/klee/Statistics/Statistic.h:31:10: error: no type named 'uint32_t' in namespace 'std' Core/Executor: long double on i686 must be aligned to 4 bytes According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes. Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes were used. This commit fixes the following out of bound pointer access. ``` $ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc $ klee varalign.bc KLEE: output directory is "/home/lukas/klee/klee-out-19" KLEE: Using Z3 solver backend KLEE: WARNING: undefined reference to function: printf KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17 i1, i2, i3: 1, 2, 3 l1: 4 i4: 5 ld1: 6.000000 KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 499 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ``` ci(lint): add shell linter - Differential ShellCheck It performs differential ShellCheck scans and report results directly in pull request. documentation: https://github.com/redhat-plumbers-in-action/differential-shellcheck Signed-off-by: Jan Macku <jamacku@redhat.com> fix CMake: -UNDEBUG Prevent fallthrough warning remove include/klee/Support/IntEvaluation.h Mark variable as potentially unused Support disabling compiler warnings; Use with external headers Use newer C++ standard for KLEE's iterators; fixes deprecation warning Disable "disabling of warnings" for LLVM >= 14 Modify name of variables in generated cvc files. ci: run ShellCheck on `*.inc` shell scripts change some obsolete KDAlloc comments - mappings were only shared in a former version of KDAlloc - `AllocationFactory(std::size_t, std::uint32_t)`'s second parameter is used for quarantine size, not the location of the mapping use `std::mt19937` instead of the custom implementation remove unused rng adaptor functions ensure that the right mt19937 constructor is chosen during overload resolution Remove additional quotation marks use unique_ptr in STPSolverImpl use unique_ptr in ValidatingSolver use unique_ptr in Z3SolverImpl use unique_ptr in StagedSolverImpl use unique_ptr in CachingSolver use unique_ptr in AssignmentValidatingSolver use unique_ptr in CexCachingSolver use unique_ptr in IndependentSolver use unique_ptr in QueryLoggingSolver use unique_ptr in Solver use unique_ptr all throughout the solver chain Replaced "-data" and "-stat" by "_data" and "_stat" in the ktest-(rand)gen tools for consistency with recent changes. Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency with recent changes. Cleaned up and updated codecov file. Use unique_ptr for MemoryManager and avoid re-creating it in the first place No need to re-create and re-alloc all the memory again after execution. Write `Control::meta` in C++17 style prevent assertions from failing unnecessarily Add `getSize` primitive to kdalloc Add `getMapping` primitive to allocator directly Improve error message when KDAlloc fails to create a mapping Improve LOH deallocation scheme add unsized free to kdalloc Refactored and fixed the code dealing with the entry point. main() should not be processed if the entry point is a different function. This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (klee#1572) Some basic refactoring and pass through comments. In particular, it brings some related code together (deadline with EntryPoint and ReplayPathFile respectively) which was unnecessarily separated. Copy stats to test directory when running tests The sqlite3 databases used for the stats are journalled and potentially must be written to. Therefore, the sqlite3 driver used by `klee-stats` requires write permissions on the database files. By copying the stats files to the test directory, we can now compile and test an out-of-tree build without requiring any write permissions on the source folder at all. CMake: remove unused TARGET_LIBS variable It appears that this variable was never used, already when it was first set in 7e75b49. CMake: remove obsolete KLEE_COMPONENT_EXTRA_LIBRARIES This variable was previously used by `klee_add_component()`, which got removed as part of 3ef5c9d. CMake: remove obsolete comments obsoleted by changes in 3ef5c9d docs/CMakeLists.txt: drop support for old CMake versions minimum CMake version is 3.16.0 as of 3a0e434 README-CMake.md: clean up top-level targets * the old build system is long gone * clean_doxygen was removed by d5cbc20 * clean_runtime was removed by 6156b4e * clean_all was removed by a00424e CMake: use built-in FindSQLite3 module available since CMake version 3.14 doxygen.cfg.in: DOXYGEN_OUTPUT_DIR resolves a FIXME to streamline doxygen.cfg generation a bit .clang-format: c++17 From the `clang-format` documentation: - "`Cpp11` is a deprecated alias for `Latest`" - `Latest`: "Parse and format using the latest supported language version." config.h: include FSTATAT_PATH_ACCEPTS_NULL This variable was introduced by d2f5906 but not included in `config.h` before. As a result `#ifdef` would always fail. Moving the code is necessary to set the variable before `config.h` is created using `configure_file()` in CMakeLists.txt. CMake: use check_c_source_compiles() for FSTATAT_PATH_ACCEPTS_NULL is a bit more convenient and avoids an extra file also check for default CHECK directive in ArrayOpt Tests fix BatchingSearcher's disabled time budget The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own. make BatchingSearcher more readable re-enable StackTraceOutput.c test This test previously had a REQUIRES line with geq-llvm-7.0. Because LLVM version 7.0 is no longer "known" (test/lit.cfg), the required feature is not available and the test is discarded as unsupported by llvm-lit. test/Feature/StackTraceOutput.c: relative checks, clang-format Further improve KDAlloc memory usage with infinite quarantine ktest-gen: remove unused function unittests/CMakeLists.txt: gtest check for LLVM 13+ We previously used `LLVM_EXPORTED_TARGETS` defined in LLVMConfig.cmake. This variable is no longer defined starting from LLVM 13. Alternatively, we use the fact that LLVM's gtest target always depends on LLVMSupport. unittests/CMakeLists.txt: fix LLVM find_package support broken by 3ef5c9d, which removed the "USE_CMAKE_FIND_PACKAGE_LLVM" variable and no longer includes AddLLVM.cmake unittests/CMakeLists.txt: remove obsolete policy Checking for policy CMP0077 is obsolete as we now require CMake 3.16.0 as minimum version. unittests/CMakeLists.txt: no UNITTEST_MAIN_LIBS variable obsoleted by 5607a7f unittests/CMakeLists.txt: do not echo GTEST_SRC_DIR on error This prevents the error message to include the internal "GTEST_SRC_DIR-NOTFOUND" value. unittests/CMakeLists.txt: set gtest include dir only if necessary Use recommended LLVM 13 as part of the Docker image Build and push Docker image as part of a release Fixed end date in the 2.3 release notes Set version number to 3.0 Release notes for KLEE 3.0
misonijnik
pushed a commit
to UnitTestBot/klee
that referenced
this issue
Jul 24, 2023
Update the Dockerfile to use the correct path for llvm-110 use mallinfo2 if available Make Uclibc support a runtime option, not a compile-time one. Switch FreeBSD 12 CI to a supported release. cl flags: document default values, remove dead option: --replay-keep-symbolic cmake: try using system installation of GTest if it's present This is a patch that I made few months ago as Fedora forbids bundling and using pieces of software provided by other packages in its repositories but forgot to upstream it at that time. [1] It has been rebased and improved so that it also reflects changes made in klee#1458. This should also make the compilation of unittests easier for our users as they don't need to clone googletest from GitHub anymore and just use package manager in the distro of their choice, provided that the gtest package includes a corresponding CMake module. [1]: https://src.fedoraproject.org/rpms/klee/blob/4c81b78/f/use-system-gtest.patch tests: make function pointer tests more robust Renamed gen-bout to ktest-gen Updated klee-zesti to use ktest-gen instead of gen-bout Updated tests to use ktest-gen instead of gen-bout Renamed gen-random-bout to ktest-randgen Updated tests to use ktest-randgen instead of gen-random-bout Utilise Docker build artifact cache for more components Switch to newer KLEE uClibc release Instead of using a branch that doesn't allow build artifact caching, use the newer released version instead. tests: invoke LLVM tools through their corresponding macros Update SpecialFunctionHandler.cpp use size() to get N in bind(), just like the way in prepare(). .err files: minor readability changes to stack trace output tests: add StackTraceOutput.c Spelling Fixes Update Dockerfile to install tabulate Install tabulate package for klee-stats to work when used within KLEE Docker. Use `klee` user to install system dependencies As a follow-up to recent build script enhancements (klee@818275b), finally build KLEE inside of the Docker image as artefact owned by the `klee` user, including user-installed Python3 modules. This fixes issues with non-writable build directories. In addition `$HOME/.local/bin` directory is made available in search path. Intrinsics: Add support for @llvm.f{ma,muladd}.f* Fix error with empty EntryPoint Define stat64 to be stat on MacOS. This fixes compilation on more recent macOS versions, where stat64 is not defined anymore. Implement getArrayForUpdate iteratively Remove the CI target metaSMT(Boolector). metaSMT(STP) already runs the test suite with all solvers supported by metaSMT, so the extra target provides marginal benefits. forward ci environment variables used to exercise metasmt backends into the docker container Perform coverage analysis for z3 as well remove LLVM < 9 rename CallSite to CallBase update github checkout action to v3 checkout KLEE with depth > 1 when running codecov Fix memory leak in crosscheck core solver mechanism Inline asm external call POSIX runtime: fstatat: check for nonnull path APIs Switch FreeBSD CI to 13.1 and Python 3.9 Support arguments of width 128, 256 and 512 bits for external calls Corrected wrong usage of klee_report_error in __cxa_atexit handler Use true instead of Z3_TRUE (removed in z3 4.11.0) Support UBSan-enabled binaries Introduce separate categories for different kinds of undefined behavior Remove LLVM version < 6 Check extensions of generated files in tests Remove LLVM version < 9 Eliminate .undefined_behavior.err category and simplify tests Add README to UBSan runtime Improve pattern for FileCheck in UBSan's tests Improve pattern for FileCheck in UBSan's tests Add notes about how to keep in sync runtime with LLVM project Pass llvm.experimental.noalias.scope.decl to IntrinsicLowering so that it strips out these intrinsics Improve the message for when large arrays become symbolic. Only print this warning once per array. Add test case. fix FileCheck cmd of VarArgByVal test Fixed some leaks in klee-replay add missing FileCheck command to test fix output check in test const_arr_opt1 Use LLVM 11 for FreeBSD testing (package llvm90 is not available anymore) Add an extra check to test/Runtime/FreeStanding/memcpy_chk_err.c ensuring that a call to __memcpy_chk is emitted Disable memcpy_chk_err.c on FreeBSD, where a call to __memcpy_chk is not generated Fix integer overflow create klee-last as a relative link Add a few simple solver tests Have the STP coverage build also provide Z3, so that the crosscheck solver can also be tested Do not escape "@". This triggers an error now in the CI. The KDAlloc slot allocator is useful for small sized allocations The KDAlloc loh allocator is useful for variable sized (large) allocations Add the KDAlloc allocator using both of its suballocators Add some unit tests for KDAlloc Integrate KDAlloc into KLEE Add some system tests for KDAlloc Fixed a bug in KLEE libc's implementation of strcmp: according to the C standard, characters should be compared as unsigned chars. [cmake] Use LLVM's CMake functionality only LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0). Use bitcode library paths via config generation instead of `-D` flags Fix compiler warning with newer compilers [MemSan] Mark memory objects modified by syscalls as initialised Update build scripts * Support for Ubuntu 22.04 * Remove support for Python2 * Better separation between sanitizer builds and non-sanitizer builds * Fix build of metaSMT on newer Ubuntu versions * Use ninja to build LLVM * Simplifying building arbitrary LLVM configurations, e.g. different LLVM sanitizer builds (MemSan, UBSan, ASan) * Use MemSan with origin tracking * Build sqlite3 container correctly * Add support to provide sqlite3 version number Add support to disable memsan instrumentation; update UB/Asan suppression Fix building of runtime library and klee-replay Former build system provided additional flags for building bitcode while they were not required, e.g. under BSD or MacOS. Fix uninitialised memory access while reading last path entry `>>` can fail and sets internal error information in the istream. Check the state of istream before pushing the value onto the buffer. Disable `const_array_opt1` for ubsan as well Don't fail `KleeStats.c` test if it takes 1s or longer Use newer LLVM_DIR config option to build FreeBSD Update Docker build components * Use Ubuntu 22.04 * Use newer TCMalloc 2.9.1 * use Z3 4.8.15 * Use SQLite 3400100 Fix script to build all the containers we require for GitHub actions Update CI components * Use Ubuntu 22.04 instead of 18.04 * Use LLVM 11 instead of 9 * Use TCMalloc 2.9.1 * Use Z3 4.8.15 * Use Sqlite3 3400100 Clean-up comments and structure to satisfy yaml linter Update KDAlloc unittests llvm14: Add LLVM 14 to lit.cfg llvm14: Add LLVM 14 job to GitHub Actions llvm14: TargetRegistry.h was moved from Support to MC llvm14: PointerType::getElementType() was deprecated ... for LLVM 14 in [1] and has already been removed from the LLVM 15 branch in [2]. Some changes are only temporary to silence the warning though, as Type::getPointerElementType() is planned to be removed as well. [3] [1] https://reviews.llvm.org/D117885/new/ [2] llvm/llvm-project@d593cf7 [3] https://llvm.org/docs/OpaquePointers.html#migration-instructions llvm14: port test/Feature/VarArgByVal.c to LLVM 14 LLVM 14 has introduced the noundef function argument attribute. ConstantArrayExprVisitor: Deduplicate `visitConcat` and `visitRead` ConstantArrayExprVisitor: Fix detection of multiple array indices Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the `incompatible` flag would not be set. Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected: if ((array1[k] + array2[x] + array2[k]) == 0) Resulting in the following output: KLEE: WARNING: OPT_I: infeasible branch! KLEE: WARNING: OPT_I: successful Explicitly check if 32bit support is enabled for testing Ignore test in the first place, if no 32bit is enabled. Handle fail of KLEE gracefully Under 64bit architecture, a ptr-error might be found. Ignore this for now. Fixed typo klee-stats: improve error message for missing tabulate package Remove hard to understand and debug pcregrep test Require minimal version of CMake 3.16 for KLEE This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment)) use C++17 Change `llvm_map_components_to_libnames` to `llvm_config` CMake function With recent LLVM versions, this should allow to link against dynamic LLVM libraries. STP: add option to switch SAT solver: --stp-sat-solver and set default to CryptoMinisat Added more test cases for --entry-point. EntryPointMissing is currently expected to fail. Run KDAlloc/rusage unittest a few times to allow for swapfile interference remove obsolete header stats: add InhibitedForks stats: add QCacheHits/Misses stats: add ExternalCalls stats: rename numQueries/Queries -> SolverQueries, add Queries stats: add Allocations stats: rename States -> ActiveStates, add States stats: add branch type stats tests: add Feature/KleeStatsBranches.c stats: add termination class stats tests: add Feature/KleeStatsTermClasses.c Remove model_version from the POSIX runtime, as we have never used it. fix unused variable warning Transition to GitHub Container Registry hosting Fix detection and installation of Ubuntu-provided llvm/clang packages fix unused variables warning tests: add some missing headers (gcc-13) include cstdint for *int*_t Otherwise we see errors like this with gcc13: include/klee/Statistics/Statistic.h:31:10: error: no type named 'uint32_t' in namespace 'std' Core/Executor: long double on i686 must be aligned to 4 bytes According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes. Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes were used. This commit fixes the following out of bound pointer access. ``` $ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc $ klee varalign.bc KLEE: output directory is "/home/lukas/klee/klee-out-19" KLEE: Using Z3 solver backend KLEE: WARNING: undefined reference to function: printf KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17 i1, i2, i3: 1, 2, 3 l1: 4 i4: 5 ld1: 6.000000 KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 499 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ``` ci(lint): add shell linter - Differential ShellCheck It performs differential ShellCheck scans and report results directly in pull request. documentation: https://github.com/redhat-plumbers-in-action/differential-shellcheck Signed-off-by: Jan Macku <jamacku@redhat.com> fix CMake: -UNDEBUG Prevent fallthrough warning remove include/klee/Support/IntEvaluation.h Mark variable as potentially unused Support disabling compiler warnings; Use with external headers Use newer C++ standard for KLEE's iterators; fixes deprecation warning Disable "disabling of warnings" for LLVM >= 14 Modify name of variables in generated cvc files. ci: run ShellCheck on `*.inc` shell scripts change some obsolete KDAlloc comments - mappings were only shared in a former version of KDAlloc - `AllocationFactory(std::size_t, std::uint32_t)`'s second parameter is used for quarantine size, not the location of the mapping use `std::mt19937` instead of the custom implementation remove unused rng adaptor functions ensure that the right mt19937 constructor is chosen during overload resolution Remove additional quotation marks use unique_ptr in STPSolverImpl use unique_ptr in ValidatingSolver use unique_ptr in Z3SolverImpl use unique_ptr in StagedSolverImpl use unique_ptr in CachingSolver use unique_ptr in AssignmentValidatingSolver use unique_ptr in CexCachingSolver use unique_ptr in IndependentSolver use unique_ptr in QueryLoggingSolver use unique_ptr in Solver use unique_ptr all throughout the solver chain Replaced "-data" and "-stat" by "_data" and "_stat" in the ktest-(rand)gen tools for consistency with recent changes. Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency with recent changes. Cleaned up and updated codecov file. Use unique_ptr for MemoryManager and avoid re-creating it in the first place No need to re-create and re-alloc all the memory again after execution. Write `Control::meta` in C++17 style prevent assertions from failing unnecessarily Add `getSize` primitive to kdalloc Add `getMapping` primitive to allocator directly Improve error message when KDAlloc fails to create a mapping Improve LOH deallocation scheme add unsized free to kdalloc Refactored and fixed the code dealing with the entry point. main() should not be processed if the entry point is a different function. This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (klee#1572) Some basic refactoring and pass through comments. In particular, it brings some related code together (deadline with EntryPoint and ReplayPathFile respectively) which was unnecessarily separated. Copy stats to test directory when running tests The sqlite3 databases used for the stats are journalled and potentially must be written to. Therefore, the sqlite3 driver used by `klee-stats` requires write permissions on the database files. By copying the stats files to the test directory, we can now compile and test an out-of-tree build without requiring any write permissions on the source folder at all. CMake: remove unused TARGET_LIBS variable It appears that this variable was never used, already when it was first set in 7e75b49. CMake: remove obsolete KLEE_COMPONENT_EXTRA_LIBRARIES This variable was previously used by `klee_add_component()`, which got removed as part of 3ef5c9d. CMake: remove obsolete comments obsoleted by changes in 3ef5c9d docs/CMakeLists.txt: drop support for old CMake versions minimum CMake version is 3.16.0 as of 3a0e434 README-CMake.md: clean up top-level targets * the old build system is long gone * clean_doxygen was removed by d5cbc20 * clean_runtime was removed by 6156b4e * clean_all was removed by a00424e CMake: use built-in FindSQLite3 module available since CMake version 3.14 doxygen.cfg.in: DOXYGEN_OUTPUT_DIR resolves a FIXME to streamline doxygen.cfg generation a bit .clang-format: c++17 From the `clang-format` documentation: - "`Cpp11` is a deprecated alias for `Latest`" - `Latest`: "Parse and format using the latest supported language version." config.h: include FSTATAT_PATH_ACCEPTS_NULL This variable was introduced by d2f5906 but not included in `config.h` before. As a result `#ifdef` would always fail. Moving the code is necessary to set the variable before `config.h` is created using `configure_file()` in CMakeLists.txt. CMake: use check_c_source_compiles() for FSTATAT_PATH_ACCEPTS_NULL is a bit more convenient and avoids an extra file also check for default CHECK directive in ArrayOpt Tests fix BatchingSearcher's disabled time budget The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own. make BatchingSearcher more readable re-enable StackTraceOutput.c test This test previously had a REQUIRES line with geq-llvm-7.0. Because LLVM version 7.0 is no longer "known" (test/lit.cfg), the required feature is not available and the test is discarded as unsupported by llvm-lit. test/Feature/StackTraceOutput.c: relative checks, clang-format Further improve KDAlloc memory usage with infinite quarantine ktest-gen: remove unused function unittests/CMakeLists.txt: gtest check for LLVM 13+ We previously used `LLVM_EXPORTED_TARGETS` defined in LLVMConfig.cmake. This variable is no longer defined starting from LLVM 13. Alternatively, we use the fact that LLVM's gtest target always depends on LLVMSupport. unittests/CMakeLists.txt: fix LLVM find_package support broken by 3ef5c9d, which removed the "USE_CMAKE_FIND_PACKAGE_LLVM" variable and no longer includes AddLLVM.cmake unittests/CMakeLists.txt: remove obsolete policy Checking for policy CMP0077 is obsolete as we now require CMake 3.16.0 as minimum version. unittests/CMakeLists.txt: no UNITTEST_MAIN_LIBS variable obsoleted by 5607a7f unittests/CMakeLists.txt: do not echo GTEST_SRC_DIR on error This prevents the error message to include the internal "GTEST_SRC_DIR-NOTFOUND" value. unittests/CMakeLists.txt: set gtest include dir only if necessary Use recommended LLVM 13 as part of the Docker image Build and push Docker image as part of a release Fixed end date in the 2.3 release notes Set version number to 3.0 Release notes for KLEE 3.0
misonijnik
pushed a commit
to UnitTestBot/klee
that referenced
this issue
Jul 24, 2023
Update the Dockerfile to use the correct path for llvm-110 use mallinfo2 if available Make Uclibc support a runtime option, not a compile-time one. Switch FreeBSD 12 CI to a supported release. cl flags: document default values, remove dead option: --replay-keep-symbolic cmake: try using system installation of GTest if it's present This is a patch that I made few months ago as Fedora forbids bundling and using pieces of software provided by other packages in its repositories but forgot to upstream it at that time. [1] It has been rebased and improved so that it also reflects changes made in klee#1458. This should also make the compilation of unittests easier for our users as they don't need to clone googletest from GitHub anymore and just use package manager in the distro of their choice, provided that the gtest package includes a corresponding CMake module. [1]: https://src.fedoraproject.org/rpms/klee/blob/4c81b78/f/use-system-gtest.patch tests: make function pointer tests more robust Renamed gen-bout to ktest-gen Updated klee-zesti to use ktest-gen instead of gen-bout Updated tests to use ktest-gen instead of gen-bout Renamed gen-random-bout to ktest-randgen Updated tests to use ktest-randgen instead of gen-random-bout Utilise Docker build artifact cache for more components Switch to newer KLEE uClibc release Instead of using a branch that doesn't allow build artifact caching, use the newer released version instead. tests: invoke LLVM tools through their corresponding macros Update SpecialFunctionHandler.cpp use size() to get N in bind(), just like the way in prepare(). .err files: minor readability changes to stack trace output tests: add StackTraceOutput.c Spelling Fixes Update Dockerfile to install tabulate Install tabulate package for klee-stats to work when used within KLEE Docker. Use `klee` user to install system dependencies As a follow-up to recent build script enhancements (klee@818275b), finally build KLEE inside of the Docker image as artefact owned by the `klee` user, including user-installed Python3 modules. This fixes issues with non-writable build directories. In addition `$HOME/.local/bin` directory is made available in search path. Intrinsics: Add support for @llvm.f{ma,muladd}.f* Fix error with empty EntryPoint Define stat64 to be stat on MacOS. This fixes compilation on more recent macOS versions, where stat64 is not defined anymore. Implement getArrayForUpdate iteratively Remove the CI target metaSMT(Boolector). metaSMT(STP) already runs the test suite with all solvers supported by metaSMT, so the extra target provides marginal benefits. forward ci environment variables used to exercise metasmt backends into the docker container Perform coverage analysis for z3 as well remove LLVM < 9 rename CallSite to CallBase update github checkout action to v3 checkout KLEE with depth > 1 when running codecov Fix memory leak in crosscheck core solver mechanism Inline asm external call POSIX runtime: fstatat: check for nonnull path APIs Switch FreeBSD CI to 13.1 and Python 3.9 Support arguments of width 128, 256 and 512 bits for external calls Corrected wrong usage of klee_report_error in __cxa_atexit handler Use true instead of Z3_TRUE (removed in z3 4.11.0) Support UBSan-enabled binaries Introduce separate categories for different kinds of undefined behavior Remove LLVM version < 6 Check extensions of generated files in tests Remove LLVM version < 9 Eliminate .undefined_behavior.err category and simplify tests Add README to UBSan runtime Improve pattern for FileCheck in UBSan's tests Improve pattern for FileCheck in UBSan's tests Add notes about how to keep in sync runtime with LLVM project Pass llvm.experimental.noalias.scope.decl to IntrinsicLowering so that it strips out these intrinsics Improve the message for when large arrays become symbolic. Only print this warning once per array. Add test case. fix FileCheck cmd of VarArgByVal test Fixed some leaks in klee-replay add missing FileCheck command to test fix output check in test const_arr_opt1 Use LLVM 11 for FreeBSD testing (package llvm90 is not available anymore) Add an extra check to test/Runtime/FreeStanding/memcpy_chk_err.c ensuring that a call to __memcpy_chk is emitted Disable memcpy_chk_err.c on FreeBSD, where a call to __memcpy_chk is not generated Fix integer overflow create klee-last as a relative link Add a few simple solver tests Have the STP coverage build also provide Z3, so that the crosscheck solver can also be tested Do not escape "@". This triggers an error now in the CI. The KDAlloc slot allocator is useful for small sized allocations The KDAlloc loh allocator is useful for variable sized (large) allocations Add the KDAlloc allocator using both of its suballocators Add some unit tests for KDAlloc Integrate KDAlloc into KLEE Add some system tests for KDAlloc Fixed a bug in KLEE libc's implementation of strcmp: according to the C standard, characters should be compared as unsigned chars. [cmake] Use LLVM's CMake functionality only LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0). Use bitcode library paths via config generation instead of `-D` flags Fix compiler warning with newer compilers [MemSan] Mark memory objects modified by syscalls as initialised Update build scripts * Support for Ubuntu 22.04 * Remove support for Python2 * Better separation between sanitizer builds and non-sanitizer builds * Fix build of metaSMT on newer Ubuntu versions * Use ninja to build LLVM * Simplifying building arbitrary LLVM configurations, e.g. different LLVM sanitizer builds (MemSan, UBSan, ASan) * Use MemSan with origin tracking * Build sqlite3 container correctly * Add support to provide sqlite3 version number Add support to disable memsan instrumentation; update UB/Asan suppression Fix building of runtime library and klee-replay Former build system provided additional flags for building bitcode while they were not required, e.g. under BSD or MacOS. Fix uninitialised memory access while reading last path entry `>>` can fail and sets internal error information in the istream. Check the state of istream before pushing the value onto the buffer. Disable `const_array_opt1` for ubsan as well Don't fail `KleeStats.c` test if it takes 1s or longer Use newer LLVM_DIR config option to build FreeBSD Update Docker build components * Use Ubuntu 22.04 * Use newer TCMalloc 2.9.1 * use Z3 4.8.15 * Use SQLite 3400100 Fix script to build all the containers we require for GitHub actions Update CI components * Use Ubuntu 22.04 instead of 18.04 * Use LLVM 11 instead of 9 * Use TCMalloc 2.9.1 * Use Z3 4.8.15 * Use Sqlite3 3400100 Clean-up comments and structure to satisfy yaml linter Update KDAlloc unittests llvm14: Add LLVM 14 to lit.cfg llvm14: Add LLVM 14 job to GitHub Actions llvm14: TargetRegistry.h was moved from Support to MC llvm14: PointerType::getElementType() was deprecated ... for LLVM 14 in [1] and has already been removed from the LLVM 15 branch in [2]. Some changes are only temporary to silence the warning though, as Type::getPointerElementType() is planned to be removed as well. [3] [1] https://reviews.llvm.org/D117885/new/ [2] llvm/llvm-project@d593cf7 [3] https://llvm.org/docs/OpaquePointers.html#migration-instructions llvm14: port test/Feature/VarArgByVal.c to LLVM 14 LLVM 14 has introduced the noundef function argument attribute. ConstantArrayExprVisitor: Deduplicate `visitConcat` and `visitRead` ConstantArrayExprVisitor: Fix detection of multiple array indices Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the `incompatible` flag would not be set. Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected: if ((array1[k] + array2[x] + array2[k]) == 0) Resulting in the following output: KLEE: WARNING: OPT_I: infeasible branch! KLEE: WARNING: OPT_I: successful Explicitly check if 32bit support is enabled for testing Ignore test in the first place, if no 32bit is enabled. Handle fail of KLEE gracefully Under 64bit architecture, a ptr-error might be found. Ignore this for now. Fixed typo klee-stats: improve error message for missing tabulate package Remove hard to understand and debug pcregrep test Require minimal version of CMake 3.16 for KLEE This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment)) use C++17 Change `llvm_map_components_to_libnames` to `llvm_config` CMake function With recent LLVM versions, this should allow to link against dynamic LLVM libraries. STP: add option to switch SAT solver: --stp-sat-solver and set default to CryptoMinisat Added more test cases for --entry-point. EntryPointMissing is currently expected to fail. Run KDAlloc/rusage unittest a few times to allow for swapfile interference remove obsolete header stats: add InhibitedForks stats: add QCacheHits/Misses stats: add ExternalCalls stats: rename numQueries/Queries -> SolverQueries, add Queries stats: add Allocations stats: rename States -> ActiveStates, add States stats: add branch type stats tests: add Feature/KleeStatsBranches.c stats: add termination class stats tests: add Feature/KleeStatsTermClasses.c Remove model_version from the POSIX runtime, as we have never used it. fix unused variable warning Transition to GitHub Container Registry hosting Fix detection and installation of Ubuntu-provided llvm/clang packages fix unused variables warning tests: add some missing headers (gcc-13) include cstdint for *int*_t Otherwise we see errors like this with gcc13: include/klee/Statistics/Statistic.h:31:10: error: no type named 'uint32_t' in namespace 'std' Core/Executor: long double on i686 must be aligned to 4 bytes According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes. Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes were used. This commit fixes the following out of bound pointer access. ``` $ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc $ klee varalign.bc KLEE: output directory is "/home/lukas/klee/klee-out-19" KLEE: Using Z3 solver backend KLEE: WARNING: undefined reference to function: printf KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17 i1, i2, i3: 1, 2, 3 l1: 4 i4: 5 ld1: 6.000000 KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 499 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ``` ci(lint): add shell linter - Differential ShellCheck It performs differential ShellCheck scans and report results directly in pull request. documentation: https://github.com/redhat-plumbers-in-action/differential-shellcheck Signed-off-by: Jan Macku <jamacku@redhat.com> fix CMake: -UNDEBUG Prevent fallthrough warning remove include/klee/Support/IntEvaluation.h Mark variable as potentially unused Support disabling compiler warnings; Use with external headers Use newer C++ standard for KLEE's iterators; fixes deprecation warning Disable "disabling of warnings" for LLVM >= 14 Modify name of variables in generated cvc files. ci: run ShellCheck on `*.inc` shell scripts change some obsolete KDAlloc comments - mappings were only shared in a former version of KDAlloc - `AllocationFactory(std::size_t, std::uint32_t)`'s second parameter is used for quarantine size, not the location of the mapping use `std::mt19937` instead of the custom implementation remove unused rng adaptor functions ensure that the right mt19937 constructor is chosen during overload resolution Remove additional quotation marks use unique_ptr in STPSolverImpl use unique_ptr in ValidatingSolver use unique_ptr in Z3SolverImpl use unique_ptr in StagedSolverImpl use unique_ptr in CachingSolver use unique_ptr in AssignmentValidatingSolver use unique_ptr in CexCachingSolver use unique_ptr in IndependentSolver use unique_ptr in QueryLoggingSolver use unique_ptr in Solver use unique_ptr all throughout the solver chain Replaced "-data" and "-stat" by "_data" and "_stat" in the ktest-(rand)gen tools for consistency with recent changes. Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency with recent changes. Cleaned up and updated codecov file. Use unique_ptr for MemoryManager and avoid re-creating it in the first place No need to re-create and re-alloc all the memory again after execution. Write `Control::meta` in C++17 style prevent assertions from failing unnecessarily Add `getSize` primitive to kdalloc Add `getMapping` primitive to allocator directly Improve error message when KDAlloc fails to create a mapping Improve LOH deallocation scheme add unsized free to kdalloc Refactored and fixed the code dealing with the entry point. main() should not be processed if the entry point is a different function. This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (klee#1572) Some basic refactoring and pass through comments. In particular, it brings some related code together (deadline with EntryPoint and ReplayPathFile respectively) which was unnecessarily separated. Copy stats to test directory when running tests The sqlite3 databases used for the stats are journalled and potentially must be written to. Therefore, the sqlite3 driver used by `klee-stats` requires write permissions on the database files. By copying the stats files to the test directory, we can now compile and test an out-of-tree build without requiring any write permissions on the source folder at all. CMake: remove unused TARGET_LIBS variable It appears that this variable was never used, already when it was first set in 7e75b49. CMake: remove obsolete KLEE_COMPONENT_EXTRA_LIBRARIES This variable was previously used by `klee_add_component()`, which got removed as part of 3ef5c9d. CMake: remove obsolete comments obsoleted by changes in 3ef5c9d docs/CMakeLists.txt: drop support for old CMake versions minimum CMake version is 3.16.0 as of 3a0e434 README-CMake.md: clean up top-level targets * the old build system is long gone * clean_doxygen was removed by d5cbc20 * clean_runtime was removed by 6156b4e * clean_all was removed by a00424e CMake: use built-in FindSQLite3 module available since CMake version 3.14 doxygen.cfg.in: DOXYGEN_OUTPUT_DIR resolves a FIXME to streamline doxygen.cfg generation a bit .clang-format: c++17 From the `clang-format` documentation: - "`Cpp11` is a deprecated alias for `Latest`" - `Latest`: "Parse and format using the latest supported language version." config.h: include FSTATAT_PATH_ACCEPTS_NULL This variable was introduced by d2f5906 but not included in `config.h` before. As a result `#ifdef` would always fail. Moving the code is necessary to set the variable before `config.h` is created using `configure_file()` in CMakeLists.txt. CMake: use check_c_source_compiles() for FSTATAT_PATH_ACCEPTS_NULL is a bit more convenient and avoids an extra file also check for default CHECK directive in ArrayOpt Tests fix BatchingSearcher's disabled time budget The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own. make BatchingSearcher more readable re-enable StackTraceOutput.c test This test previously had a REQUIRES line with geq-llvm-7.0. Because LLVM version 7.0 is no longer "known" (test/lit.cfg), the required feature is not available and the test is discarded as unsupported by llvm-lit. test/Feature/StackTraceOutput.c: relative checks, clang-format Further improve KDAlloc memory usage with infinite quarantine ktest-gen: remove unused function unittests/CMakeLists.txt: gtest check for LLVM 13+ We previously used `LLVM_EXPORTED_TARGETS` defined in LLVMConfig.cmake. This variable is no longer defined starting from LLVM 13. Alternatively, we use the fact that LLVM's gtest target always depends on LLVMSupport. unittests/CMakeLists.txt: fix LLVM find_package support broken by 3ef5c9d, which removed the "USE_CMAKE_FIND_PACKAGE_LLVM" variable and no longer includes AddLLVM.cmake unittests/CMakeLists.txt: remove obsolete policy Checking for policy CMP0077 is obsolete as we now require CMake 3.16.0 as minimum version. unittests/CMakeLists.txt: no UNITTEST_MAIN_LIBS variable obsoleted by 5607a7f unittests/CMakeLists.txt: do not echo GTEST_SRC_DIR on error This prevents the error message to include the internal "GTEST_SRC_DIR-NOTFOUND" value. unittests/CMakeLists.txt: set gtest include dir only if necessary Use recommended LLVM 13 as part of the Docker image Build and push Docker image as part of a release Fixed end date in the 2.3 release notes Set version number to 3.0 Release notes for KLEE 3.0
ccadar
pushed a commit
to ccadar/klee
that referenced
this issue
Oct 19, 2023
This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment))
ccadar
pushed a commit
to ccadar/klee
that referenced
this issue
Oct 20, 2023
This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment))
ccadar
pushed a commit
to ccadar/klee
that referenced
this issue
Oct 20, 2023
This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (stp/stp#375 (comment))
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
If we can avoid having our own internal copy of ABC, we perhaps should. However, we should carefully evaluate the impact of doing so.
The copyright dates in the code that we have date back to 2007, but it's unclear when the code was imported. I looked for the first commit in which some of these files were introduced:
cnf_short.his the only missing one, and it just seems to be a subset ofcnf.h.The most recent revision referenced above is https://github.com/berkeley-abc/abc/tree/7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2/ from September 2007. So that's around when I would think the code was imported. Since then there have been over 4,000 commits to the ABC project.
We should also decide on our criteria for accepting the new version. What is the performance impact? Can we build only the parts we need?
The text was updated successfully, but these errors were encountered: