Regression test failure for cbmc/SIMD1 on M1 machines

[NlightNFotis]

CBMC version: 516f109 (should be manifestable on develop)
Operating system: macOS 11.3.1 on M1
Exact command line resulting in the issue: ctest -V --test-dir regression/cbmc
What behaviour did you expect: All tests passing successfully.
What happened instead: The test under the folder regression/cbmc/SIMD1 fails with conversion error.

I am getting this (augmented) debug output:

[DEBUG] src_type:
signedbv
  * width: 32
  * #c_type: signed_int
[DEBUG] dest_type:
vector
  * #source_location: 
    * file: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/lib/clang/13.0.0/include/mmintrin.h
    * line: 13
    * function: 
    * working_directory: /Users/fotiskoutoulakis/Devel/cbmc/regression/cbmc/SIMD1
  * size: constant
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      * #source_location: 
        * file: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/lib/clang/13.0.0/include/mmintrin.h
        * line: 13
        * function: 
        * working_directory: /Users/fotiskoutoulakis/Devel/cbmc/regression/cbmc/SIMD1
      * value: 1
  0: signedbv
      * width: 64
      * #c_type: signed_long_long_int
file /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/lib/clang/13.0.0/include/mmintrin.h line 1082 function _mm_and_si64: in expression '__builtin_ia32_pand((__gcc_v1di)__m1, (__gcc_v1di)__m2)':
conversion from 'signed int' to '__gcc_v1di': implicit conversion not permitted
CONVERSION ERROR

It seems that for a strange kind of fashion, check_c_implicit_typecast in c_typecast.cpp gets a src_type argument that is completely incompatible with the dest_type argument.

I can observe that behaviour only on an M1 machine (MacBooks with Intel seem to not have this problem, at least in my current experiments) so I believe it's probably a type definition in the includes of the file (mmintrin.h seems to be the culprit in this case) that's causing issues.

[NlightNFotis]

@tautschnig I see that you're the author of this test - is this something that's easy for you take care of?

If not, I can probably fix this, but I'm not sure of exactly what a fix for this entails (as I haven't seen these headers before and I'm not familiar with SIMD and its associated types/operations) so I would appreciate any pointers.

[tautschnig]

I'll check whether #5918 already addresses this issue (and if it doesn't, then it should).

[tautschnig]

Hmm, no, #5918 does not yet include this. But then the current code already has a comment here:

gcc_builtin_headers_ia32.h:__gcc_v2si __builtin_ia32_pand(__gcc_v2si, __gcc_v2si); // maybe di

(and indeed the right types would really be __gcc_v1di instead of __gcc_v2si).