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

crux-llvm test suite failures with Clang 12 #977

Closed
RyanGlScott opened this issue May 9, 2022 · 0 comments · Fixed by #979
Closed

crux-llvm test suite failures with Clang 12 #977

RyanGlScott opened this issue May 9, 2022 · 0 comments · Fixed by #979

Comments

@RyanGlScott
Copy link
Contributor

The crux-llvm test suite produces the following errors when built with Clang 12.0.1, but not with earlier versions of Clang:

$ PATH=~/Software/clang+llvm-12.0.1/bin:$PATH cabal test crux-llvm -w ghc-9.2
<snip>
Running 1 test suites...
Test suite crux-llvm-test: RUNNING...
<snip>
    T847-fail2.ll
      z3
        loop
          at-least-clang12
            z3 4.8.14
              T847-fail2
                T847-fail2 crux run:                     OK (0.18s)
                T847-fail2 crux output:                  FAIL
                  test/Test.hs:234:
                  MISMATCH for expected (test-data/golden/golden/T847-fail2.at-least-clang12.good)
                             and actual (test-data/golden/golden/T847-fail2.at-least-clang12.z3.out) output:
                      F        |[Crux] Found counterexample for verification goal
                      F        |[Crux]   internal: error: in my_abs
                      F        |[Crux]   Undefined behavior encountered
                      F        |[Crux]   Details:
                      F        |[Crux]     Poison value created
                      F        |[Crux]     The first argument of `llvm.abs.*` was `INT_MIN` even though the
                      F        |[Crux]     second argument was `1`
                      F        |[Crux]     Argument: 0x80000000:[32]
                      F        |[Crux]     Reference: 
                      F        |[Crux]       The LLVM language reference, version 12
                      F        |[Crux]       �llvm.abs.*� Intrinsic (Semantics)
                      F        |[Crux]       Document URL: https://releases.llvm.org/12.0.0/docs/LangRef.html
                      F-expect>|[Crux] Overall status: Invalid.
                      F-actual>|[Crux]     in context:
                      F-actual>|[Crux]       my_abs
                      F-actual>|[Crux]       main
                      F-actual>|[Crux] Overall status: Invalid.
                  
                  Use -p '/T847-fail2 crux output/' to rerun this test only.
<snip>
    invoke-test.ll
      z3
        loop
          at-least-clang12
            z3 4.8.14
              invoke-test
                invoke-test crux run:                    OK
                invoke-test crux result:                 FAIL
                  test/Test.hs:234:
                  MISMATCH for expected (test-data/golden/golden/invoke-test.result)
                             and actual (test-data/golden/golden/invoke-test.z3.result.out) output:
                      F-expect>|***[test]*** Crux failed with non-zero result: "1"
                      F-actual>|***[test]*** Crux failed with exception: "ExitFailure 1"
                  
                  Use -p '/loop.at-least-clang12.z3 4.8.14.invoke-test.invoke-test crux result/' to rerun this test only.
                invoke-test crux output:                 FAIL
                  test/Test.hs:234:
                  MISMATCH for expected (test-data/golden/golden/invoke-test.good)
                             and actual (test-data/golden/golden/invoke-test.z3.out) output:
                      F-expect>|[Crux] Found counterexample for verification goal
                      F-actual>|`clang` compilation failed.
                      F-expect>|[Crux]   internal: error: in _ZN3std2rt10lang_start17h4f32aa1279b9079fE
                      F-actual>|*** Exit code: 1
                      F-expect>|[Crux]   Failed to load function handle
                      F-actual>|*** Standard out:
                      F-expect>|[Crux]   Details:
                      F-actual>|*** Standard error:
                      F-expect>|[Crux]     No implementation or override found for pointer
                      F-actual>|   test-data/golden/golden/invoke-test.ll:104:132: error: expected '('
                      F-expect>|[Crux]     The given pointer could not be resolved to a callable function
                      F-actual>|   define internal void @_ZN4core3fmt9Arguments16new_v1_formatted17hd5e9ced080c81dfaE(%"core::fmt::Arguments"* noalias nocapture sret dereferenceable(48), [0 x { [0 x i8]*, i64 }]* noalias nonnull readonly align 8 %pieces.0, i64 %pieces.1, [0 x { i8*, i8* }]* noalias nonnull readonly align 8 %args.0, i64 %args.1, [0 x %"core::fmt::rt::v1::Argument"]* noalias nonnull readonly align 8 %fmt.0, i64 %fmt.1) unnamed_addr #1 {
                      F-expect>|[Crux]     No implementation or override found for pointer
                      F-actual>|                                                                                                                                      ^
                      F-expect>|[Crux]     Attempting to load callable function with type: i64({ }*, [3 x i64]*, i64, i8**)
                      F-actual>|   1 error generated.
                      F-expect>|[Crux]       Via pointer: Global symbol "_ZN3std2rt19lang_start_internal17h3dc68cf5532522d7E" (1, 0x0:[64])
                      F-expect>|[Crux]     In memory state:
                      F-expect>|[Crux]       Stack frame _ZN3std2rt10lang_start17h4f32aa1279b9079fE
                      F-expect>|[Crux]         Allocations:
                      F-expect>|[Crux]           StackAlloc 48 0x8:[64] Mutable 8-byte-aligned internal
                      F-expect>|[Crux]         Writes:
                      F-expect>|[Crux]           Indexed chunk:
                      F-expect>|[Crux]             48 |->   *(48, 0x0:[64]) := (39, 0x0:[64])
                      F-expect>|[Crux]       Stack frame main
                      F-expect>|[Crux]         No writes or allocations
                      F-expect>|[Crux]       Base memory
                      F-expect>|[Crux]         Allocations:
                      F-expect>|[Crux]           StackAlloc 47 0x0:[64] Mutable 8-byte-aligned crux-llvm main(argc, argv) simulation
                      F-expect>|[Crux]           GlobalAlloc 46 0x1:[64] Immutable 1-byte-aligned [global variable  ] 
                      F-expect>|[Crux]           GlobalAlloc 45 0x0:[64] Immutable 1-byte-aligned [global variable  ] 
                      F-expect>|[Crux]           GlobalAlloc 44 0x40:[64] Immutable 8-byte-aligned [global variable  ] 
                      F-expect>|[Crux]           GlobalAlloc 43 0x20:[64] Immutable 8-byte-aligned [global variable  ] 
                      F-expect>|[Crux]           GlobalAlloc 42 0x30:[64] Immutable 8-byte-aligned [global variable  ] vtable.0
                      F-expect>|[Crux]           GlobalAlloc 41 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3fmt9Arguments16new_v1_formatted17hd5e9ced080c81dfaE
                      F-expect>|[Crux]           GlobalAlloc 40 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3fmt10ArgumentV13new17h0af350dc6d28844eE
                      F-expect>|[Crux]           GlobalAlloc 39 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4test4main17h21e0b94bad749a9eE
                      F-expect>|[Crux]           GlobalAlloc 38 0x0:[64] Immutable 1-byte-aligned [defined function ] main
                      F-expect>|[Crux]           GlobalAlloc 37 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ptr31_$LT$impl$u20$$BP$mut$u20$T$GT$3add17h8c3ba94a5f9e63b3E
                      F-expect>|[Crux]           GlobalAlloc 36 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core5slice29_$LT$impl$u20$$u5b$T$u5d$$GT$3len17hd158f8061ea13277E
                      F-expect>|[Crux]           GlobalAlloc 35 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core5slice29_$LT$impl$u20$$u5b$T$u5d$$GT$10as_mut_ptr17h0cc7f77ba7a559f2E
                      F-expect>|[Crux]           GlobalAlloc 34 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ptr31_$LT$impl$u20$$BP$mut$u20$T$GT$6offset17hdf0bba33c31d7941E
                      F-expect>|[Crux]           GlobalAlloc 33 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3mem7size_of17h24506033ef7ef062E
                      F-expect>|[Crux]           GlobalAlloc 32 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ptr31_$LT$impl$u20$$BP$mut$u20$T$GT$7is_null17heb54d174dd3ad0e3E
                      F-expect>|[Crux]           GlobalAlloc 31 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ptr31_$LT$impl$u20$$BP$mut$u20$T$GT$3add17he8137b02ed5a1862E
                      F-expect>|[Crux]           GlobalAlloc 30 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ptr31_$LT$impl$u20$$BP$mut$u20$T$GT$12wrapping_add17h3f944d3e55c804bdE
                      F-expect>|[Crux]           GlobalAlloc 29 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core5slice29_$LT$impl$u20$$u5b$T$u5d$$GT$3len17hfcd8fb803edc91ecE
                      F-expect>|[Crux]           GlobalAlloc 28 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core5slice29_$LT$impl$u20$$u5b$T$u5d$$GT$10as_mut_ptr17hf0bc8639b7d66054E
                      F-expect>|[Crux]           GlobalAlloc 27 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ptr8null_mut17h236caeaa39cf68eeE
                      F-expect>|[Crux]           GlobalAlloc 26 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ptr31_$LT$impl$u20$$BP$mut$u20$T$GT$6offset17h1a0a27c95852d960E
                      F-expect>|[Crux]           GlobalAlloc 25 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ptr31_$LT$impl$u20$$BP$mut$u20$T$GT$15wrapping_offset17h835906e17eda2d9eE
                      F-expect>|[Crux]           GlobalAlloc 24 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3mem7size_of17h901aeab6d69720f2E
                      F-expect>|[Crux]           GlobalAlloc 23 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ptr31_$LT$impl$u20$$BP$mut$u20$T$GT$7is_null17hefda0dbc6462cbcdE
                      F-expect>|[Crux]           GlobalAlloc 22 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN94_$LT$core..slice..IterMut$LT$$u27$a$C$$u20$T$GT$$u20$as$u20$core..iter..iterator..Iterator$GT$4next17hb33d39b685e46f5aE
                      F-expect>|[Crux]           GlobalAlloc 21 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN54_$LT$I$u20$as$u20$core..iter..traits..IntoIterator$GT$9into_iter17h8263e821b42cf117E
                      F-expect>|[Crux]           GlobalAlloc 20 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core5slice29_$LT$impl$u20$$u5b$T$u5d$$GT$8iter_mut17h705dbea5bcc6571dE
                      F-expect>|[Crux]           GlobalAlloc 19 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN94_$LT$core..slice..IterMut$LT$$u27$a$C$$u20$T$GT$$u20$as$u20$core..iter..iterator..Iterator$GT$4next17h54ce825ac39c65a6E
                      F-expect>|[Crux]           GlobalAlloc 18 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN54_$LT$I$u20$as$u20$core..iter..traits..IntoIterator$GT$9into_iter17h664642be175905efE
                      F-expect>|[Crux]           GlobalAlloc 17 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core5slice29_$LT$impl$u20$$u5b$T$u5d$$GT$8iter_mut17h9ec72aa0f1adbb13E
                      F-expect>|[Crux]           GlobalAlloc 16 0x0:[64] Immutable 1-byte-aligned [defined function ] f
                      F-expect>|[Crux]           GlobalAlloc 15 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN3std3sys4unix7process14process_common8ExitCode6as_i3217h131bd83b3a6fff4bE
                      F-expect>|[Crux]           GlobalAlloc 14 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN68_$LT$std..process..ExitCode$u20$as$u20$std..process..Termination$GT$6report17h269423f2b50d143fE
                      F-expect>|[Crux]           GlobalAlloc 13 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17ha97fdaad4e15facaE
                      F-expect>|[Crux]           GlobalAlloc 12 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ops8function6FnOnce9call_once17h27d755cee67a2edbE
                      F-expect>|[Crux]           GlobalAlloc 11 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ops8function6FnOnce9call_once32_$u7b$$u7b$vtable.shim$u7d$$u7d$17hbfe54a791614f945E
                      F-expect>|[Crux]           GlobalAlloc 10 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h6e1c450892b1f754E
                      F-expect>|[Crux]           GlobalAlloc 9 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN4core3ptr18real_drop_in_place17h96afe4d514bb3c38E
                      F-expect>|[Crux]           GlobalAlloc 8 0x0:[64] Immutable 1-byte-aligned [defined function ] _ZN3std2rt10lang_start17h4f32aa1279b9079fE
                      F-expect>|[Crux]           GlobalAlloc 7 0x0:[64] Immutable 1-byte-aligned [external function] llvm.memcpy.p0i8.p0i8.i64
                      F-expect>|[Crux]           GlobalAlloc 6 0x0:[64] Immutable 1-byte-aligned [external function] _ZN3std2io5stdio6_print17hdec9324a4622df1eE
                      F-expect>|[Crux]           GlobalAlloc 5 0x0:[64] Immutable 1-byte-aligned [external function] _ZN4core3fmt3num52_$LT$impl$u20$core..fmt..Display$u20$for$u20$i32$GT$3fmt17h7a9374c1576dce31E
                      F-expect>|[Crux]           GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned [external function] llvm.memset.p0i8.i64
                      F-expect>|[Crux]           GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [external function] llvm.assume
                      F-expect>|[Crux]           GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] rust_eh_personality
                      F-expect>|[Crux]           GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] _ZN3std2rt19lang_start_internal17h3dc68cf5532522d7E
                      F-expect>|[Crux]         Writes:
                      F-expect>|[Crux]           Indexed chunk:
                      F-expect>|[Crux]             42 |->   *(42, 0x0:[64]) := {base+0 = (9, 0x0:[64])
                      F-expect>|[Crux]                      ,base+8 = 0x8:[64]
                      F-expect>|[Crux]                      ,base+16 = 0x8:[64]
                      F-expect>|[Crux]                      ,base+24 = (10, 0x0:[64])
                      F-expect>|[Crux]                      ,base+32 = (10, 0x0:[64])
                      F-expect>|[Crux]                      ,base+40 = (11, 0x0:[64])}
                      F-expect>|[Crux]             46 |->   *(46, 0x0:[64]) := {base+0 = "\n"}
                      F-expect>|[Crux]     in context:
                      F-expect>|[Crux]       _ZN3std2rt10lang_start17h4f32aa1279b9079fE
                      F-expect>|[Crux]       main
                      F-expect>|[Crux] Overall status: Invalid.
                  
                  Use -p '/loop.at-least-clang12.z3 4.8.14.invoke-test.invoke-test crux output/' to rerun this test only.
<snip>

Here is an explanation for each of these failures:

  1. invoke-test.ll fails because LLVM's syntax for the sret attribute has changed in LLVM 12. Now, instead of simply writing sret, one must write sret(<ty>), where <ty> is the type of the structure being returned. (See here). In the case of invoke-test.ll, this can be fixed by changing sret to sret(%"core::fmt::Arguments").
  2. T847-fail2.ll fails because the error message now prints a call stack due to crucible-llvm: Annotate errors with call stacks #914. This is straightforward to fix: just accept the call stack in the expected error message.
@RyanGlScott RyanGlScott self-assigned this May 9, 2022
RyanGlScott added a commit that referenced this issue May 9, 2022
Fixing `T847-fail2` is as simple as accepting the new output resulting from
#914.

Fixing `invoke-test` requires updating the LLVM to use `sret` syntax specific
to LLVM 12 or later. (See
https://releases.llvm.org/12.0.0/docs/LangRef.html#parameter-attributes).
As a result, this test is now only ran on Clang 12 or later.

Fixes #977.
RyanGlScott added a commit that referenced this issue May 10, 2022
Fixing `T847-fail2` is as simple as accepting the new output resulting from
#914.

Fixing `invoke-test` requires updating the LLVM to use `sret` syntax specific
to LLVM 12 or later. (See
https://releases.llvm.org/12.0.0/docs/LangRef.html#parameter-attributes).
As a result, this test is now only ran on Clang 12 or later.

Fixes #977.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant