Rounding mode type isn't `integer`

[adpaco-aws]

With the recent change in types for architecture strings in #7215, all of them use integer except for __CPROVER_rounding_mode. Is there any reason to not use integer for it as well?

[tautschnig]

__CPROVER_rounding_mode is a program variable that may get assigned to/will be read when using floating-point operations. It's how we implement fesetround and friends. An architecture might specify what the default rounding mode is, but that's about all that it shares with other architecture strings. Those other architecture strings just inform the platform configuration, they will not be read or written to during execution of the program under verification.

[tautschnig]

That said, we might well decide to make it a 2-bit bitvector (or some other hard-coded width) rather than using an architecture-specific width.

[tautschnig]

Assigning to @kroening and @martin-cs who might be able to give additional context or correct me in case I misspoke.

[tautschnig]

Also noting that there are two related PRs:

• Move rounding_mode_identifier() to configt #6555 clarifies that the rounding mode is a part of the configuration.
• Permit initializers in library functions #6590 may open up an avenue to add the object on demand.

[kroening]

The rounding mode is naturally very architecture dependent, so I'd say it's ok that that variable has an architecture-specific type and interpretation.

[martin-cs]

@tautschnig I think I agree. There are the four modes from IEEE-754 1989, 1 that was added in 2008 but is not required for binary and then the 1 or 2 that are mentioned in 2019 IIRC. It's a small number anyway. We could have a uint_16t and comfortably "1 hot" encode all possible current and likely future rounding modes.

There is also a practical point which is that it is an input into all floating-point operations and avoiding mixing mathematical integers into bit-vector operations is generally a good thing.

[martin-cs]

@adpaco-aws Is that an answer? If so, please close the issue or, if not, let's discuss it more.

[adpaco-aws]

Thanks all for the answers! It makes sense to leave it as it is.