Different behaviors, when not found function in module in -libc=klee and -libc=uclibc #1572
Comments
8 tasks
ccadar
added a commit
to ccadar/klee
that referenced
this issue
Mar 14, 2023
This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (klee#1572) Add tests for missing entry points.
8 tasks
ccadar
added a commit
to ccadar/klee
that referenced
this issue
Mar 16, 2023
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) Add tests for missing entry points.
ccadar
added a commit
to ccadar/klee
that referenced
this issue
Mar 17, 2023
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) Add tests for missing entry points.
ccadar
added a commit
to ccadar/klee
that referenced
this issue
Apr 6, 2023
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)
ccadar
added a commit
to ccadar/klee
that referenced
this issue
Apr 20, 2023
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)
ccadar
added a commit
to ccadar/klee
that referenced
this issue
Apr 20, 2023
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)
ccadar
added a commit
that referenced
this issue
May 26, 2023
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 (#1572)
|
This was fixed in #1574 |
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
added a commit
to ccadar/klee
that referenced
this issue
Oct 19, 2023
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)
ccadar
added a commit
to ccadar/klee
that referenced
this issue
Oct 20, 2023
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)
ccadar
added a commit
to ccadar/klee
that referenced
this issue
Oct 20, 2023
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)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Run klee on module without function
fooWhen run KLEE with libc=klee KLEE fail on
klee_errorWhen run KLEE with libc=uclibc KLEE fail on assert
It would be better if KLEE had the same behavior in these cases
The text was updated successfully, but these errors were encountered: