Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CI: Build and test both x86-64 and AArch64 macOS #1173

Merged
merged 5 commits into from
Feb 15, 2024
Merged

Conversation

RyanGlScott
Copy link
Contributor

This also requires bumping the mir-json submodule to bring in the changes from GaloisInc/mir-json#65, which are necessary to make mir-json build with AArch64 Macs.

Previously, the conventions for crux-llvm and crux-mir were inconsistent in a
number of ways, which this PR fixes. We now:

* Build both using three recent versions of GHC on Linux
* Build other OSes using only a single version of GHC, which is now consistent
* Use the same naming conventions when uploading binary artifacts
This also requires bumping the `mir-json` submodule to bring in the changes
from GaloisInc/mir-json#65, which are necessary to make
`mir-json` build with AArch64 Macs.
@RyanGlScott
Copy link
Contributor Author

Happily, the crux-mir test suite passes on an M1 Mac without any further changes.

There is a single test that fails in the crux-llvm test suite:

    T972-fail.c
      solver=z3
        loop-merging=loop
          clang-range=pre-clang14
            z3 4.8.14
              T972-fail
                T972-fail crux run:                      OK (0.40s)
                T972-fail crux output:                   FAIL
                  test/Test.hs:310:
                  MISMATCH for expected (test-data/golden/T972-fail.pre-clang14.z3.good)
                             and actual (test-data/golden/T972-fail.pre-clang14.z3.z3.out) output:
                      F        |[Crux] Found counterexample for verification goal
                      F        |[Crux]   test-data/golden/T972-fail.c:8:3: error: in main
                      F-expect>|[Crux]   unsupported LLVM value: ValAsm True False "testl $0, $0; jne ${1:l};" "r,X,X,~{dirflag},~{fpsr},~{flags}" of type void(i32, i8*, i8*)*
                      F-actual>|[Crux]   unsupported LLVM value: ValAsm True False "testl $0, $0; jne ${1:l};" "r,X,X" of type void(i32, i8*, i8*)*
                      F-expect>|[Crux] Overall status: Invalid.
                      F-actual>|[Crux] Failed to build counterexample executable
                      F-actual>|`clang` compilation failed.
                      F-actual>|*** Exit code: 1
                      F-actual>|*** Standard out:
                      F-actual>|*** Standard error:
                      F-actual>|   test-data/golden/T972-fail.c:10:27: warning: value size does not match register size specified by the constraint and modifier [-Wasm-operand-widths]
                      F-actual>|                       : "r"(cond)
                      F-actual>|                             ^
                      F-actual>|   test-data/golden/T972-fail.c:8:28: note: use constraint modifier "w"
                      F-actual>|     asm volatile goto("testl %0, %0; jne %l1;"
                      F-actual>|                              ^~
                      F-actual>|                              %w0
                      F-actual>|   test-data/golden/T972-fail.c:10:27: warning: value size does not match register size specified by the constraint and modifier [-Wasm-operand-widths]
                      F-actual>|                       : "r"(cond)
                      F-actual>|                             ^
                      F-actual>|   test-data/golden/T972-fail.c:8:32: note: use constraint modifier "w"
                      F-actual>|     asm volatile goto("testl %0, %0; jne %l1;"
                      F-actual>|                                  ^~
                      F-actual>|                                  %w0
                      F-actual>|   test-data/golden/T972-fail.c:8:21: error: unrecognized instruction mnemonic, did you mean: tst?
                      F-actual>|     asm volatile goto("testl %0, %0; jne %l1;"
                      F-actual>|                       ^
                      F-actual>|   <inline asm>:1:2: note: instantiated into assembly here
                      F-actual>|           testl x8, x8; jne Ltmp0;
                      F-actual>|           ^
                      F-actual>|   2 warnings and 1 error generated.
                      F-actual>|[Crux] Found counterexample for verification goal
                      F-actual>|[Crux]   test-data/golden/T972-fail.c:8:3: error: in main
                      F-actual>|[Crux]   unsupported LLVM value: ValAsm True False "testl $0, $0; jne ${1:l};" "r,X,X" of type void(i32, i8*, i8*)*
                      F-actual>|[Crux] Overall status: Invalid.
                  
                  Use -p '/T972-fail crux output/' to rerun this test only.

And indeed, T972-fail.c uses inline x86-64 assembly, which won't work with an AArch64 compiler. The most direct solution would be to disable this test on non–x86-64 architectures.

This test case requires an x86-64 compiler in order to work, so it stands no
hope of working on other architectures (e.g., AArch64 on Apple silicon).
@RyanGlScott RyanGlScott marked this pull request as ready for review February 15, 2024 10:46
@RyanGlScott RyanGlScott merged commit c5dc719 into master Feb 15, 2024
31 checks passed
@RyanGlScott RyanGlScott deleted the macos-14-ci branch February 15, 2024 20:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants