Floating Point Support

Overview

Ultimate is able to verify C programs, that are using 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 the control flow graph is done in two steps. First, we translate the C 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 Our Boogie dialect).

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 Rounding Mode, which is the default behavior in C, except for the conversion functions from floating to int types, which use RTZ (RoundTowardsZero) 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
• Rounding Modes
• compare operations
  • ==
  • !=
  • <=
  • >=
  • <
  • >
• basic arithmetics
  • +
  • -
  • *
  • /
• negation
• Float contstants
  • +-NaN
  • +-Inf
  • +-Zero
• casts & implicit conversions
• post- & präfix Inc-/Decrementer
• classification functions

what does not work

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