Version 2.0.0 test failures on x86_32, arm32 and s390x

[sim642]

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]

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]

The float128 errors come from here:

cil/src/frontc/cabs2cil.ml

Lines 2525 to 2533 in 51180df

	| [A.Tfloat128] ->
	(* This is only correct w.r.t. to size and align. If we analyze floats, we need to be careful here *)
	if !Machdep.theMachine.Machdep.sizeof_longdouble = 16 && !Machdep.theMachine.Machdep.alignof_longdouble = 16 then
	TFloat(FLongDouble, [])
	else
	E.s (error "float128 only supported on machines where it is an alias (w.r.t. to size and align) of long double: size: %i align: %i "
	!Machdep.theMachine.Machdep.sizeof_longdouble
	!Machdep.theMachine.Machdep.alignof_longdouble
	)

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]

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: 1bb7140#diff-ded244e1032a1d7ef47ebce532dadfa1f0c07727e2d3e70e678af36fef96299bR225-R238.
Maybe there was an intended overflow in that process or something?

[michael-schwarz]

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]

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]

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 😄

[sim642]

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]

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]

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 goblint/analyzer#54. Currently, we just assume everything is 64 bits. Kind of impressive we never saw any unsoundness because of this...

[sim642]

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.