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

enable regression tests for the ARM64 build #1581

Draft
wants to merge 14 commits into
base: master
Choose a base branch
from
Draft

Conversation

fbrausse
Copy link
Member

@fbrausse fbrausse commented Jan 6, 2024

No description provided.

@fbrausse fbrausse added the CI label Jan 6, 2024
@fbrausse fbrausse force-pushed the fb/ci-arm-tests branch 2 times, most recently from 271aae5 to 0707f36 Compare January 6, 2024 11:04
@fbrausse
Copy link
Member Author

fbrausse commented Jan 7, 2024

The remaining failing regression test on arm64 is due to wrong path for the libstdc++ headers:

  • regression/esbmc-cpp/cpp/ch20_1-32
    missing C++ header <cstddef> for 32-bit on the system, need to install some Ubuntu package to get them installed g++-11-arm-linux-gnueabihf libstdc++-11-dev-armhf-cross, now clang -target arm-unknown-linux-gnueabihf -m32 --sysroot=/usr/arm-linux-gnueabihf finds this GCC installation, but still selects the wrong include path for the libstdc++.

    Giving the right paths to ESBMC via --idirafter, this test still fails parsing due to usage of __builtin_memset in the libstdc++. I think @mikhailramalho's comment here Implement the __builtin_memcpy function #569 (comment) shows an approach how to avoid these errors.

Fixed:

  • regression/esbmc/github_151-2
    find the failed assertion CHAR_MIN == -128 in the user program; ARM has unsigned chars by default
  • regression/incremental-smt/incremental-28
    Clang already fails to convert it because of an __asm__ directive which is not valid on arm64:
    ../regression/incremental-smt/incremental-28/main.c:3847:32: error: invalid output constraint '=q' in asm
    __asm__ ("movb %%gs:%P1,%0": "=q" (pfo_ret__): "p" (& current_task));
    
  • regression/esbmc-cpp/cpp/ch18_[456] and regression/esbmc-cpp/cpp/ch5_17
    triggers internal assertion because the operands of cond ? '0' : '1' are (implicitly) typecast to int, which is correct for C, but not for C++. This is a general bug of the C++ frontend and it only surfaced on arm64, because char is unsigned there. Solutions could be to implement a C++ version of util/c_typecast.cpp, or to only use it in the C++ frontend for ternary-if when the types are not equal.
  • csmith-{incremental,kind,kind-parallel}
    Fixed by installing libcsmith-dev
  • Interval Analysis - Typecast (signed)
  • Interval Analysis - Mult Arithmetic (signed)

@fbrausse
Copy link
Member Author

fbrausse commented Jan 8, 2024

now clang -target arm-unknown-linux-gnueabihf -m32 --sysroot=/usr/arm-linux-gnueabihf finds this GCC installation, but still selects the wrong include path for the libstdc++.

OK, traced this down to Clang handling the include paths wrongly in v11 and v12. Starting with clang-13, the proper include paths are added for the selected GCC toolchain and manual specification is no longer necessary.

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

Successfully merging this pull request may close these issues.

None yet

1 participant