search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
173 stars 72 forks source link

Float domain tests fail on arm64 #824

Closed sim642 closed 2 months ago

sim642 commented 2 years ago

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

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: # # # ------------------------------------------------------------------------------ # ============================================================================== # 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: # # # ------------------------------------------------------------------------------ # ============================================================================== # 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: # # # ------------------------------------------------------------------------------ # ============================================================================== # 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 commented 8 months ago

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 commented 8 months ago

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 commented 8 months ago

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

ksromanov commented 8 months ago 
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
sim642 commented 2 months ago

Somehow these didn't seem to be an issue for the 2.4.0 release. Although maybe they only were for Linux arm64, not MacOS, and we fail there for other reasons.