Version 2.0.0 test failures on x86_32, arm32 and s390x

sim642 commented 2 years ago

Submitting goblint-cil 2.0.0 to opam-repository revealed (even after some basic fixes) that we fail some of our tests on these architectures.

x86_32

[ ] testrun/math1

# /usr/include/i386-linux-gnu/bits/mathcalls-helper-functions.h:21: Error: float128 only supported on machines where it is an alias (w.r.t. to size and align) of long double: size: 12 align: 4 
# Fatal error: exception GoblintCil__Errormsg.Error
# make: *** [Makefile:184: testrun/math1] Error 2

[ ] testrun/nan-global

# /usr/include/i386-linux-gnu/bits/mathcalls-helper-functions.h:21: Error: float128 only supported on machines where it is an alias (w.r.t. to size and align) of long double: size: 12 align: 4 
# Fatal error: exception GoblintCil__Errormsg.Error
# make: *** [Makefile:184: testrun/nan-global] Error 2

[ ] testrun/packed

# old type = TArray(TInt(int, ), Some(Const(Int(9,unsigned int,9U))), )
# new type = TArray(TInt(int, ), Some(sizeofE(Lval(Var(foo, NoOffset)))), )
# packed.c:13: Error: Declaration of x9 does not match previous declaration from packed.c:12 (different array lengths).
# error in createGlobal(x9: packed.c:13): GoblintCil__Errormsg.ErrorError: Cabs2cil had some errors
# Fatal error: exception GoblintCil__Errormsg.Error
# make: *** [Makefile:184: testrun/packed] Error 2

[ ] testrunc99/c99-complex

# /usr/include/i386-linux-gnu/bits/mathcalls-helper-functions.h:21: Error: float128 only supported on machines where it is an alias (w.r.t. to size and align) of long double: size: 12 align: 4 
# Fatal error: exception GoblintCil__Errormsg.Error
# make: *** [Makefile:190: testrunc99/c99-complex] Error 2

[ ] testrunc99/c99-float-pragma

# /usr/include/i386-linux-gnu/bits/mathcalls-helper-functions.h:21: Error: float128 only supported on machines where it is an alias (w.r.t. to size and align) of long double: size: 12 align: 4 
# Fatal error: exception GoblintCil__Errormsg.Error
# make: *** [Makefile:190: testrunc99/c99-float-pragma] Error 2

[ ] testrunc99/c99-tgmath

# /usr/include/i386-linux-gnu/bits/mathcalls-helper-functions.h:21: Error: float128 only supported on machines where it is an alias (w.r.t. to size and align) of long double: size: 12 align: 4 
# Fatal error: exception GoblintCil__Errormsg.Error
# make: *** [Makefile:190: testrunc99/c99-tgmath] Error 2

[ ] testrunc99/c99-tgmath2

# /usr/include/i386-linux-gnu/bits/mathcalls-helper-functions.h:21: Error: float128 only supported on machines where it is an alias (w.r.t. to size and align) of long double: size: 12 align: 4 
# Fatal error: exception GoblintCil__Errormsg.Error
# make: *** [Makefile:190: testrunc99/c99-tgmath2] Error 2

[ ] testrungcc/builtin_object_size

# /usr/lib/gcc/i686-linux-gnu/10/include/stddef.h:415: Error: float128 only supported on machines where it is an alias (w.r.t. to size and align) of long double: size: 12 align: 4 
# Error on A.TYPEDEF (GoblintCil__Errormsg.Error)
# Error: Cabs2cil had some errors
# Fatal error: exception GoblintCil__Errormsg.Error
# make: *** [Makefile:208: testrungcc/builtin_object_size] Error 2

[ ] testrungcc/enum3

# ./enum3.cil.c: In function 'main':
# ./enum3.cil.c:112:19: error: '__int128' is not supported on this target
#   112 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                   ^~~~~~~~
# ./enum3.cil.c:112:48: error: '__int128' is not supported on this target
#   112 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                                                ^~~~~~~~
# ./enum3.cil.c:112:72: error: '__int128' is not supported on this target
#   112 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                                                                        ^~~~~~~~
# make: *** [Makefile:208: testrungcc/enum3] Error 1

[ ] testrungcc/enum3g

# ./enum3g.cil.c: In function 'main':
# ./enum3g.cil.c:27:19: error: '__int128' is not supported on this target
#    27 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                   ^~~~~~~~
# ./enum3g.cil.c:27:48: error: '__int128' is not supported on this target
#    27 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                                                ^~~~~~~~
# ./enum3g.cil.c:27:72: error: '__int128' is not supported on this target
#    27 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                                                                        ^~~~~~~~
# make: *** [Makefile:208: testrungcc/enum3g] Error 1

arm32

[ ] testrungcc/enum3

# ./enum3.cil.c: In function 'main':
# ./enum3.cil.c:112:19: error: '__int128' is not supported on this target
#   112 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                   ^~~~~~~~
# ./enum3.cil.c:112:48: error: '__int128' is not supported on this target
#   112 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                                                ^~~~~~~~
# ./enum3.cil.c:112:72: error: '__int128' is not supported on this target
#   112 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                                                                        ^~~~~~~~
# make: *** [Makefile:208: testrungcc/enum3] Error 1

[ ] testrungcc/enum3g

# ./enum3g.cil.c: In function 'main':
# ./enum3g.cil.c:27:19: error: '__int128' is not supported on this target
#    27 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                   ^~~~~~~~
# ./enum3g.cil.c:27:48: error: '__int128' is not supported on this target
#    27 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                                                ^~~~~~~~
# ./enum3g.cil.c:27:72: error: '__int128' is not supported on this target
#    27 |     if ((unsigned __int128 )magic2 + (unsigned __int128)1 == (unsigned __int128 )(magic1 + 1LL)) {
#       |                                                                        ^~~~~~~~
# make: *** [Makefile:208: testrungcc/enum3g] Error 1

s390x

[ ] testrun/wchar3

# Error 1
# make: *** [Makefile:185: testrun/wchar3] Error 1

[ ] testrun/wchar4

# Error 2
# make: *** [Makefile:185: testrun/wchar4] Error 2

michael-schwarz commented 2 years ago

I'm not sure how relevant support for x32 and mainframes is, I'd suggest to just disable those specific tests for legacy or exotic architectures.

sim642 commented 2 years ago

The float128 errors come from here: https://github.com/goblint/cil/blob/51180df8d240b128098370d62a5b0c1f0c306f31/src/frontc/cabs2cil.ml#L2525-L2533

There's no explanation why that check is needed and especially why the memory alignment has anything to do with our ability to analyze them. Also, that check is not actually checking what it's claiming to check: it's comparing sizes and alignments _of long double not float128 to some constant values from some particular architecture (probably x86_64) instead of comparing them between two types.

sim642 commented 2 years ago

The s390x wchar errors are related to multi-character character literals. The only relevant change since 1.8.2 that I could find is when that function was converted from int64 to cilint: https://github.com/goblint/cil/commit/1bb71407676c5791d228ad30c48580c3c0ff32f4#diff-ded244e1032a1d7ef47ebce532dadfa1f0c07727e2d3e70e678af36fef96299bR225-R238. Maybe there was an intended overflow in that process or something?

michael-schwarz commented 2 years ago

There's no explanation why that check is needed and especially why the memory alignment has anything to do with our ability to analyze them.

We just treat them as FLongDouble to not have separate (potentially aliasing) ftypes for them, and I'd suggest we stick with this.

michael-schwarz commented 2 years ago

Maybe there was an intended overflow in that process or something?

Maybe, but I don't understand where in the code an overflow would be desirable. Might also be that it his some issues that were there before? One would need to verify whether gcc can even compile the input files on this architecture before they go through CIL.

michael-schwarz commented 2 years ago

If you want I can look into these, but it would have to be in early September. But ofc also feel free to do it yourself if you find the time to do it before me :smile:

sim642 commented 2 years ago

I'm not sure how relevant support for x32 and mainframes is, I'd suggest to just disable those specific tests for legacy or exotic architectures.

Sure, s390x is exotic, but x86_32 isn't at all. It's the most basic 32-bit support and most of those failures are simply in programs that #include <math.h>. A large proportion of SV-COMP tasks are 32-bit (just preprocessed with some old enough math.h that doesn't include float128) and being able to handle the correct 32-bit sizes of types is kind of important for detecting overflows.

sim642 commented 2 years ago

Might also be that it his some issues that were there before? One would need to verify whether gcc can even compile the input files on this architecture before they go through CIL.

Version 1.8.2 at least got through the CI without these failures coming up, so they used to work.

If you want I can look into these, but it would have to be in early September. But ofc also feel free to do it yourself if you find the time to do it before me smile

Given the number of issues here and how some aren't easily reproducible, I'll just add all three architectures to goblint-cil's incompatible architectures list in opam. We already have PowerPC there. If we manage to fix any, then later versions can lift this restriction.

michael-schwarz commented 2 years ago

and being able to handle the correct 32-bit sizes of types is kind of important for detecting overflows.

True, we should at some point do https://github.com/goblint/analyzer/issues/54. Currently, we just assume everything is 64 bits. Kind of impressive we never saw any unsoundness because of this...

sim642 commented 2 years ago

Kind of impressive we never saw any unsoundness because of this...

It looks like the majority of tasks in NoOverflows are LP64. A smaller proportion from bitvector, recursive and loop-zilu use ILP32, but they're either too hard or too easy, never trivially checking the bound used. sv-benchmarks would benefit from such simple task, but we'd shoot ourselves in the foot with that right now.

goblint / cil