fesetround support broken

[Heizmann]

Input: trunk/examples/svcomp/floats-cbmc-regression/float-rounding1_true-unreach-call.i Settings: trunk/examples/settings/default/automizer/svcomp-Reach-64bit-Automizer_Bitvector.epf Toolchain: trunk/examples/toolchains/AutomizerC.xml

There are actually two bugs.

1. If our "Let fesetround change the rounding mode" setting is set to false, we produce an incorrect verification result (expected: result UNKNOWN because in this setting we do not support the fesetround function")
2. If our "Let fesetround change the rounding mode" setting is set to true, we produce an incorrect verification result (expected: result TRUE because the specification holds)

[gschievelbein]

https://en.cppreference.com/w/c/numeric/fenv/feround

Our implementaion of fesetround returns 0 if successful, and -1 otherwise. When the setting is set to false, it always returns -1, and does not change the rounding mode. Could this be related to this behavior?

https://en.cppreference.com/w/c/numeric/fenv/FE_round

I checked the integer values of the rounding macros from FENV.h. They are: RTZ->3072 RNE-> 0 RTP -> 2048 RTN -> 1024

The values we are using internally are: 0, 1, 2, 3, respectively. I believe the actual values of the macros might change depending on the implementation, just as more macros may be defined? Should I change the integer values we use to be the same?

[Heizmann]

Thanks. But when does our implementation return -1? How can fesetround be not successful in our implementation? The behavior for the "Let fesetround change the rounding mode" should as explained in 1. above. I think there is not need to change the integer values, but it would be nice if you could find out why the implementation produces incorrect results on the above mentioned program.

[danieldietsch]

Perhaps we need three settings for fesetround: 1) Enable 2) Disable (report error) 3) Disable (do not change rounding mode and return -1)

The standard specifies that fesetround might return non-zero if the platform does not support changing the rounding mode. Therefore, we currently have only option 1. and 3. implemented.

[Heizmann]

I did not knew that we want to support 3. (that the architecture cannot change the rounding mode) But then three different settings are a good idea. I would however call them differently. I propose the following three names for the settings A. ARCHITECTURE_CAN_CHANGE_ROUNDING_MODE B. ARCHITECTURE_CANNOT_CHANGE_ROUNDING_MODE C. FESETROUND_UNSUPPORTED_BY_VERIFIER

[gschievelbein]

So, what is happening is that in the code fromfloat-rounding1_true-unreach-call.i, first we have fesetround(0);, which sets the rounding mode to RTZ. Later, we have fesetround(0x400); (0x400=1024), which fails, but the program continues its execution.

It seems like the desired rounding modes are RNE-> 0 and RTN -> 1024.

I could change our integer constants to be:

• RTZ->3072
• RNE-> 0
• RTP -> 2048
• RTN -> 1024

the problem is, I am not sure the macros are always translated to these integer constants in every platform. If we have a c code using the macros (FE_DOWNWARD, etc), we can map them to the integers we use, the problem would be with code such as this that uses fesetround directly with the integer value.

[Heizmann]

Thanks. What does the C standard (C11) say about the values of these constants? If the standard defines the values as mentioned above, we should use the same values.

[gschievelbein]

Hi, so the integer values for the current rounding mode are define here: https://en.cppreference.com/w/c/types/limits/FLT_ROUNDS

These are the values we are currently using, and are returned by the fegetround() method.

Now the integer values from the macros from fenv.h don't seem to be defined. I got these values by running a c program. The C11 standard says the following:

Even though the rounding direction macros may expand to constants corresponding to the values of FLT_ROUNDS, they are not required to do so.

[Heizmann]

Ok, so my (possibly faulty) analysis of the problem is the following.

• The C11 standard says in 5.2.4.2.2.8 that 0, 1, 2, 3 are each mapped to rounding modes. The C standard says in 7.6.8 that additionally the values of four macros from fenv.h (FE_DOWNWARD, ...) are mapped to rounding modes.
• The C11 standard says that the values of these four macros are implementation defined.
• In the above mentioned SV-COMP benchmark, fenv.h is inlined and defines values for each of the four macros.
• We however fail to map the values of these macros to the respective rounding modes.
• The current glibc uses the following values FE_TONEAREST =0, FE_DOWNWARD = 0x400, FE_UPWARD = 0x800, FE_TOWARDZERO =0xc00

Do you agree with this analysis? Do you have an idea how we can address the problem? Do we really have a mapping from rounding modes to integer constants? If yes, could we instead map integer constants to rounding modes? The a makeshift solution could be that we also hardcode the current glibc values in this map. But if there is a better solution I would probably prefer that.

[gschievelbein]

Yes. Basically, we keep a variable to the current SMT-LIB rounding mode.

Calls fegetround() will check this variable and return an integer ([-1,3]) as defined in https://en.cppreference.com/w/c/numeric/fenv/FE_round.

The method to change the current rounding mode receives an integer as an argument (fesetround(int)), or one of the macros from https://en.cppreference.com/w/c/numeric/fenv/FE_round. Since their int values are not defined, I assumed they would have the same values from FLT_ROUNDS, considering that they have the same meaning, which unfortunately isn't the case.

I am not entirely sure what would be the best way to deal with different values from multiple implementations, probably yet another option in the settings to choose which implementation to use.

[Heizmann]

I think that is a good idea. If I understand you correctly, you add to every Boogie program also a variable that represents FLT_ROUNDS. Maybe let's call this variable #Ultimate.FLT_ROUNDS in addition to the currentRoundingMode variable.

• #Ultimate.FLT_ROUNDS has the same type as a signed int (type of FLT_ROUNDS not defined in standard but maybe signed int is a good choice.)
• Our implementation of fesetround sets both, #Ultimate.FLT_ROUNDS and currentRoundingMode.
• Our implementation of fegetround returns the value of #Ultimate.FLT_ROUNDS

However, for my construction of SMT benchmarks fegetround is not that important. The only thing that I need urgently is that implementation of fesetround supports also the following values. FE_TONEAREST =0, FE_DOWNWARD = 0x400, FE_UPWARD = 0x800, FE_TOWARDZERO =0xc00

[gschievelbein]

did it work with the last changes?

[Heizmann]

Sorry for not giving any feedback. We now output the expected result on the above mentioned program and it seems like I am producing meaningful benchmarks for the SMT-COMP.

[gschievelbein]

ok great