GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
617 stars 42 forks source link

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

Closed RyanGlScott closed 5 months ago

RyanGlScott commented 5 months ago

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

RyanGlScott commented 5 months ago

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.