CI: Run crux-llvm test suite in macOS #1172
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
These packages do not require using an LLVM toolchain in order to run their test suites, so they are relatively portable.
On the Darwin family of operating systems, which includes macOS, various `libc` functions are defined in terms of aliases that contain various odd prefixes and suffixes. For instance, the `write()` function is actually defined in terms of a lower-level `\01_write()` function, and if you compile a C program containing an occurrence of `write()` with Clang on Darwin, the resulting LLVM bitcode will mention `\01_write()`, not `write()`. This poses an issue for `crucible-llvm`'s override for `write()`, since it now mentions the wrong name on Darwin. Moreover, it isn't feasible to make the LLVM bitcode mention `write()` instead. To compensate for this oddity, we introduce a new `DarwinAliasMatch` template matcher and use it in `basic_llvm_override` when compiling on Darwin. This matcher indicates that a function name is allowed to match the override name after possibly removing some Darwin-related prefixes or suffixes. See `Note [Darwin aliases]` for the full story. Fixes #885.
The `crux-llvm` test suite had accumulated quite a bit of non-portable code which causes various test cases to fail when compiled with macOS. This commit attempts to bring some sanity to the test case: * Several test cases use non-standard C functions that are not present on macOS. When appropriate, we section off any uses of non-portable functions with `#if !defined(__APPLE__)` CPP. * Several test cases were missing `#include`s that were added behind the scenes on Linux, but not on macOS. These are simple enough to fix by just making the necessary `#include`s explicit. * Some `math.h` functions compile down to low-level functions that are exclusive to macOS. For instance, `isnan(x)` compiles to `__isnand(x)` on macOS when `x` is a `double`, and we had neglected to add an override for `__isnand()`. This is easily fixed by adding the appropriate overrides. * Clang on macOS is pickier about the placement of `__attribute__((noinline))` in a function declaration, so one occurrence of this attribute was moved to avoid macOS-specific warnings. * We had special SV-COMP treatment for the `__assert_fail()` function on Linux, but not for the macOS counterpart `__assert_rtn()`. This seems inconsistent, causes some test cases to fail, and has caused us issues with debugging things previously (see #940 (comment)). For these reasons, we now treat `__assert_fail()` and `__assert_rtn()` uniformly. Fixes #1013.
On Ubuntu, `isinf(x)` will return `1` if `x` is positive infinity and `-1` if `x` is negative infinity. The C standard doesn't guarantee this, however, as it only requires that `isinf(x)` return _some_ non-zero value if `x` is infinite. More to the point, Apple Clang's version of `isinf` doesn't return the same values that Ubuntu's Clang does, but the `isinf.c` test case in the `crux-llvm` test suite specifically checks for these values, making the test fail on macOS. This patch makes the checks in `isinf.c` more general so that they will pass regardless of which non-zero value gets returned from `isinf(x)`.
Previous, we concocted a `clang-withIncl` script for running Clang on macOS CI runners, but this neglected to pass any arguments to Clang (among other issues). This patch replaces the `clang-withIncl` machinery with a much simpler, Homebrew-based setup for install Clang/LLVM. With this in place, we can finally run the `crux-llvm` test suite on macOS. Fixes #999.
kquick
approved these changes
Feb 14, 2024
Yes. I added this to the commit message:
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Previously, we concocted a
clang-withInclscript for running Clang on macOS CI runners, but this neglected to pass any arguments to Clang (among other issues). This patch replaces theclang-withInclmachinery with a much simpler, Homebrew-based setup for install Clang/LLVM. With this in place, we can finally run thecrux-llvmtest suite on macOS.Fixes #999.
Running the test suite on macOS reveals several additional issues, among them #885 and #1013. This PR also applies a series of fixes for these issues.