Floating Point Support

Overview

Ultimate is able to verify C programs containing floating point data types. This is realized with the Floating Point SMT Theory.

Most verification algorithms in Ultimate do not operate directly on the input language but on a control flow graph whose semantics is given by SMT formulas. The transformation from a C program to this control flow graph is done using an intermediate language. First, we translate the C program (or any input program) into a Boogie program. Afterwards we translate the Boogie program into the control flow graph.

Because the Boogie language lacks native support for floating point operations, we represent constants, functions and types in C by uninterpreted constants, functions, and types in Boogie but give them a semantics using the "builtin" attribute (see Ultimate's Boogie dialect for details).

Every Boogie function name is suffixed with one of the floating types (FLOAT, DOUBLE, LONGDOUBLE), depending on which type is used as argument. This solves the problem of Boogies missing capability to overload functions by creating functions for each used argument type separately. Semantically equivalent functions (e.g. fp.addFLOAT, fp.addDOUBLE, fp.addLONGDOUBLE) are all translated to the same SMT function, which supports overloading.

At the moment, every function uses the RNE (round to nearest even) rounding mode, which is the default behaviour in C, except for the conversion functions from floating to integer types, which use RTZ (round towards zero) to simulate the integer truncation.

If you want to use floating types in combination with arrays (internally we use also arrays to represent the heap of the program) you have to use the ALL logic of Z3.

Usage

Some ultimate settings are needed to work with floating types:

• Automizer (Trace Abstraction)
  • use separate solver for trace checks
  • Logic for external solver: QF_BVFP
• C+ACSL to Boogie Translator
  • use bitvectors instead of ints
• RCFGBuilder
  • Logic for external solver: QF_BVFP

Features that are already implemented

(all section numbers below refer to the ISO/IEC 9899 C11 standard)

• Float literal translation (all formats according to §6.4.4.2)
  • decimal literal with and without suffix, e.g., 3.14, 3.14f
  • decimal literal with exponential sign, e.g., 3.42e2
  • hexadecimal floating literal, e.g., 0X2A
  • hexadecimal floating literal with exponential sign, e.g., 0X0.3p10
• Casts & implicit conversions (according to §6.5.3)
• The five Rounding Modes defined in §5.2.4.2.2-8 (the default is RNE and cannot be changed)
• Postfix increment and decrement (according to §6.5.2.4)
• Prefix increment and decrement (according to §6.5.3.1)
• Unary arithmetic operators + and - (according to §6.5.3.3)
• Multiplicative operators *, / and % (according to §6.5.5)
• Additive operators + and - (according to §6.5.6)
• Relational operators <, >, <= and <= (according to §6.5.8)
• Equality operators == and != (according to §6.5.9)
• The macros INFINITY and NaN (according to §7.12)
• The classification macros fpclassify, isfinite, isinf, isnan, isnormal, and signbit (according to §7.12.3). We note that signbit may return any int value, however we return only 0 or 1.
• The sqrt functions (according to §7.12.7.5)
• Floating point types in ACSL expressions and expressions of Correctness Witnesses

Limitations & Features that are not yet Implemented

• Floating types in combination with our bit-precise memory model.
• Execution-time change of rounding mode via fesetround from <fenv.h>
• Selection of rounding mode via preferences
• Precision of long double might not exactly reflect the precision of x86 computers. At least we did not yet investigate/test this carefully.
• Complex floating types (mentioned in §6.2.5-11), e.g., double complex c = 5 + 3 * I
• Remainder (%)
  • is implemented, but even the simplest examples run out of memory
• more sophisticated arithmetic operations like sin, pow or fma