Float domain tests fail on arm64

[sim642]

Version 2.0.0 release on opam reveals the following float domain test failures on arm64:

• [ ] :1:floatDomainTest:3:float_interval_qcheck64:4:test_FI_lt_xor_ge
• [ ] :1:floatDomainTest:3:float_interval_qcheck64:5:test_FI_gt_xor_le
• [ ] :1:floatDomainTest:3:float_interval_qcheck64:6:test_FI_eq_xor_ne
• [x] :1:floatDomainTest:0:float_interval32:5:test_FI_casti2f_specific
• [x] :1:floatDomainTest:2:float_interval64:5:test_FI_casti2f_specific

Full log

# ==============================================================================
# Error: :1:floatDomainTest:3:float_interval_qcheck64:6:test_FI_lt_xor_ge.
# 
# File "/home/opam/.opam/4.14/.opam-switch/build/goblint.2.0.0/_build/default/unittest/oUnit--builder#01.log", line 181, characters 1-1:
# Error: :1:floatDomainTest:3:float_interval_qcheck64:6:test_FI_lt_xor_ge (in the log).
# 
# File "src/core/QCheck2.ml", line 1815, characters 1-1:
# Error: :1:floatDomainTest:3:float_interval_qcheck64:6:test_FI_lt_xor_ge (in the code).
# 
# 
# test `test_FI_lt_xor_ge` failed on ≥ 1 cases: <instance>
#                                                 
# 
# ------------------------------------------------------------------------------
# ==============================================================================
# Error: :1:floatDomainTest:3:float_interval_qcheck64:5:test_FI_lt_xor_ge.
# 
# File "/home/opam/.opam/4.14/.opam-switch/build/goblint.2.0.0/_build/default/unittest/oUnit--builder#01.log", line 165, characters 1-1:
# Error: :1:floatDomainTest:3:float_interval_qcheck64:5:test_FI_lt_xor_ge (in the log).
# 
# File "src/core/QCheck2.ml", line 1815, characters 1-1:
# Error: :1:floatDomainTest:3:float_interval_qcheck64:5:test_FI_lt_xor_ge (in the code).
# 
# 
# test `test_FI_lt_xor_ge` failed on ≥ 1 cases: <instance>
#                                                 
# 
# ------------------------------------------------------------------------------
# ==============================================================================
# Error: :1:floatDomainTest:3:float_interval_qcheck64:4:test_FI_lt_xor_ge.
# 
# File "/home/opam/.opam/4.14/.opam-switch/build/goblint.2.0.0/_build/default/unittest/oUnit--builder#01.log", line 149, characters 1-1:
# Error: :1:floatDomainTest:3:float_interval_qcheck64:4:test_FI_lt_xor_ge (in the log).
# 
# File "src/core/QCheck2.ml", line 1815, characters 1-1:
# Error: :1:floatDomainTest:3:float_interval_qcheck64:4:test_FI_lt_xor_ge (in the code).
# 
# 
# test `test_FI_lt_xor_ge` failed on ≥ 1 cases: <instance>
#                                                 
# 
# ------------------------------------------------------------------------------
# ==============================================================================
# Error: :1:floatDomainTest:2:float_interval64:5:test_FI_casti2f_specific.
# 
# File "/home/opam/.opam/4.14/.opam-switch/build/goblint.2.0.0/_build/default/unittest/oUnit--builder#01.log", line 116, characters 1-1:
# Error: :1:floatDomainTest:2:float_interval64:5:test_FI_casti2f_specific (in the log).
# 
# File "unittest/cdomains/floatDomainTest.ml", line 142, characters 1-1:
# Error: :1:floatDomainTest:2:float_interval64:5:test_FI_casti2f_specific (in the code).
# 
# expected: [-8.,-1.] but got: [248.,255.]
# ------------------------------------------------------------------------------
# ==============================================================================
# Error: :1:floatDomainTest:0:float_interval32:5:test_FI_casti2f_specific.
# 
# File "/home/opam/.opam/4.14/.opam-switch/build/goblint.2.0.0/_build/default/unittest/oUnit--builder#02.log", line 65, characters 1-1:
# Error: :1:floatDomainTest:0:float_interval32:5:test_FI_casti2f_specific (in the log).
# 
# File "unittest/cdomains/floatDomainTest.ml", line 142, characters 1-1:
# Error: :1:floatDomainTest:0:float_interval32:5:test_FI_casti2f_specific (in the code).
# 
# expected: [-8.,-1.] but got: [248.,255.]
# ------------------------------------------------------------------------------
# Ran: 2643 tests in: 22.94 seconds.
# FAILED: Cases: 2643 Tried: 2643 Errors: 0 Failures: 5 Skip:  1 Todo: 0 Timeouts: 0.

Thus, I have disabled Goblint on arm64, but that's quite bad since it means we cannot run on Apple M1.

My hypothesis is that our fabulous float domain C stubs are the reason for these qcheck failures on double. Using MPFR for float abstraction would avoid such architecture-dependent floating-point issues that we have no control over. Longer discussion in https://github.com/goblint/analyzer/pull/761#discussion_r899993066.

[michael-schwarz]

I think the solution to get availability on OS X back is to simply skip these if the machine is not x86 and produce a warning when float domains are enabled on a non-x86 machine. Otherwise, we are probably excluding too many potential users or making it difficult for them without reason.

[ksromanov]

I have checked analyzer just now (latest commit), it does not fail any test on M2 (Apple M2 Pro, MBP 16" 2023):

kromanov1@MM2M0W0HWL analyzer % make test
No errors :)

I had to pin cil to the latest commit.

It is very possible that I did something wrong, so please let me know how to test properly.

[sim642]

The failures were in unit tests, not regression tests. dune runtest should run them all.

[ksromanov]

kromanov1@MM2M0W0HWL analyzer % dune runtest
In file included from goblint.c:1:
../include/goblint.h:5:6: warning: a function declaration without a prototype is deprecated in all versions of C and is treated as a zero-parameter prototype in C2x, conflicting with a subsequent definition [-Wdeprecated-non-prototype]
void __goblint_assume_join(/* pthread_t thread */); // undeclared argument to avoid pthread.h interfering with Linux kernel headers
     ^
goblint.c:19:6: note: conflicting prototype is here
void __goblint_assume_join(pthread_t thread) {
     ^
1 warning generated.
..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
Ran: 2986 tests in: 32.63 seconds.
OK
No errors :)2 tutorials/first-extendturnitrnt-maineaded-betterpivnt-0ccessble

Ran just right now. System:

kromanov1@MM2M0W0HWL analyzer % uname -a
Darwin MM2M0W0HWL 23.3.0 Darwin Kernel Version 23.3.0: Wed Dec 20 21:31:00 PST 2023; root:xnu-10002.81.5~7/RELEASE_ARM64_T6020 arm64