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.

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

Limitations & missing Features

At the moment it is not possible to work with arrays containing floats, because there is no SMT solver supporting the QF_AFPBV logic (as of August 2016).

Also, float pointers are not supported yet.

what works

• Float literal translation
  • 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
• Rounding Modes
• compare operations
  • ==
  • !=
  • <=
  • >=
  • <
  • >
• basic arithmetic operators
  • +
  • -
  • *
  • /
• negation
• Float constants
  • +-NaN
  • +-Inf
  • +-Zero
• casts & implicit conversions
• post- & prefix increment and decrement
• classification functions

what does not work

• Remainder (%)
  • is implemented, but even the simplest examples run out of memory
• Arrays
• Pointers
• Complex Floats
• more sophisticated arithmetic operations like sqrt, pow or fma