Still SIMD1 failures with ia32_vec_ext_v4si

[rurban]

When I compile on AMD64 with -march=native
the SIMD1 test fails still after #5919 with

no body for function __builtin_ia32_vec_ext_v4si
main.c function main
[main.assertion.1] line 12 assertion val1 == 0x1234: FAILURE

CBMC version: cbmc-5.27.0-16-gd79e5f0b6
Operating system: Fedora Core 32
Exact command line resulting in the issue: make test
What behaviour did you expect:

LastTest-marchnative.log

See also my march-native branch with the -Denable_marchnative=true option to make it easier. https://github.com/rurban/cbmc/commits/march-native

[tautschnig]

Won't be today, but I'll take a look at this.

[tautschnig]

@rurban In the meantime, could you perhaps post the upload of running CBMC on this test with --preprocess? Also, could you post the full output, not just those three lines? I'm really surprised that __builtin_ia32_vec_ext_v4si is not found, it should be provided by the internal library. Thank you!

[rurban]

See the https://github.com/diffblue/cbmc/files/6302924/LastTest-marchnative.log link, already there. Or more?
Could be Fedora specific

[tautschnig]

See the https://github.com/diffblue/cbmc/files/6302924/LastTest-marchnative.log link, already there. Or more?
Could be Fedora specific

Ah, thank you, I thought this was a log of a successful run. (The Malloc13 failure is also surprising.) The output of running just that test with --preprocess would still be useful.

[tautschnig]

I got hold of a Fedora 33 system, but I'm unable to reproduce. Here is what I did:

$ $ cat /proc/cpuinfo
processor	: 0
vendor_id	: AuthenticAMD
cpu family	: 23
model		: 49
model name	: AMD EPYC 7R32
[...]
$ g++ --version
g++ (GCC) 10.2.1 20201125 (Red Hat 10.2.1-9)
[...]
$ cmake -Denable_marchnative=true -Bbuild
[...]
$ cmake --build build -- -j cbmc
[...]

The only test I'm getting to fail is integer-assignments1.

[tautschnig]

The only test I'm getting to fail is integer-assignments1.

Fixed in #6030.

[rurban]

This is the SIMD1 preprocess:

SIMD1.preprocess.out.gz

And this the strange Malloc13 (including preprocess and all)
Malloc13.out.tar.gz

plus gcc_popcount2
gcc_popcount2.tar.gz

So far only tested on my ryzen laptop with gcc-10. Will try more.

[tautschnig]

@rurban Thank you for sharing those inputs! I'm afraid even with those I'm unable to reproduce the failures :-( Is it exactly a single platform where you are able to produce these failing test results?

[tautschnig]

Resolving as not reproducible at this time. Please feel free to re-open if more information can be provided.