florianschanda / fp_test_generator Goto Github PK

Random floating-point testcase generator for SMT-LIB

License: GNU General Public License v3.0

Python 89.72% Makefile 0.72% C 9.56%

fp_test_generator's Introduction

FP test generator

Random floating-point testcase generator for SMT-LIB. This was originally part of PyMPF, but it is actually cleaner to separate out the library part from the test-case generator.

This program creates small benchmarks for SMT-LIB that involve the Floating Point theory. The benchmarks created focus on checking for correct behaviour as opposed to performance. This was part of the verification argument of our TACAS'2019 paper.

Since running this tool is quite slow, the generated benchmarks are available in here as a convenience.

We used this to find soundness and completness bugs in all floating point solvers we tried (that could understand SMT-LIB). For the FP solvers that do not support SMT-LIB we're pretty sure we could also find bugs but honestly we can't be bothered to support different formats other than SMT-LIB. We have even found bugs in gcc and glibc using this approach.

To make sure the expected status (SAT/UNSAT) of each test is correct we are independently checking against as many of the following as is possible:

PyMPF (this is the main test oracle and the only library that supports everything)
MPFR (does not support RNA, except for roundToIntegral)
Your FPU (probably only supports float32 and float64, and does not support RNA except for roundToIntegral)

Note that the tests generated may rely on unspecified behaviour (following a strict reading of the FP theory): for example tests that involve min/max for +0 and -0 may rely on min/max being returning either of the two. Similarly for conversions to bitvectors that are out of range.

Dependencies

This project requires the following Python3 packages:

PyMPF (the main test oracle)
gmpy2 (to interface with MPFR)

This project requires the following system dependencies:

gcc (to build tiny C programs)

To install these on Debian based systems do as root:

$ apt-get install python3-pip libmpc-dev libmpfr-dev

And then:

$ pip3 install PyMPF gmpy2

Work in progress

This is a complete re-write of the original tool in Python3. It does not yet work completely. If you want the original tool, look at the python2 branch of PyMPF.

License and Copyright

Everything in this repository is licensed under the GNU GPL v3. The sole copyright owner is Florian Schanda.

fp_test_generator's People

Contributors

Watchers

Forkers

aytey

fp_test_generator's Issues

New benchmarks

High priority:

Low priority:

Float16
(_ FloatingPoint 8 8) (BFloat16)
(_ FloatingPoint 8 11) (TensorFloat32)

new tests: backwards reasoning for mul

New test schema as following:

define input_1
define result
assert (= result (fp.mul rm input_1 input_2))

Prove something about input_2. For example:

!= something
in interval
not in interval

define input_1
define input_2
define result

Then either:

assert (= result (fp.fma rm input_1 input_2 input_free))
assert (= result (fp.fma rm input_1 input_free input_2))

Prove something about input_free. For example:

!= something
in interval
not in interval

define result
assert (= result (fp.roundToIntegral rm input_1))

Prove something about input_1. For example:

!= something
in interval
not in interval

new tests: bitvector -> float

Signed and unsigned bitvectors to float

new tests: backwards reasoning for div

New test schema as following:

define input_1
define result
assert (= result (fp.div rm input_1 input_2))

Prove something about input_2. For example:

!= something
in interval
not in interval

add validation: host fpu

new tests: backwards reasoning for add/sub

New test schema as following:

define input_1
define result
assert (= result (op rm input_1 input_2))

Prove something about input_2. For example:

!= something
in interval
not in interval

#include <stdio.h>
#include <stdint.h>
#include <math.h>
#include <string.h>

int main()
{
  uint32_t bv = 0x7FACBA7E;
  // (0 11111111 01011001011101001111110)

  float a, b;
  a = -INFINITY;
  memcpy(&b, &bv, 4);

  printf("max(%f, %f) = %f\n", a, b, __builtin_fmaxf(a, b));

  b = NAN;
  printf("max(%f, %f) = %f\n", a, b, __builtin_fmaxf(a, b));
}

This program produces (with gcc):

max(-inf, nan) = nan
max(-inf, nan) = -inf

Which is mildly concerning.

new tests: backwards reasoning for sqrt

New test schema as following:

define result
assert (= result (fp.sqrt rm input_1))

Prove something about input_1. For example:

!= something
in interval
not in interval

work out why host validation on sqrt fails (float128)

The following program produces an off-by-one error:

#include <quadmath.h>
#include <stdio.h>
#include <stdint.h>

int main()
{
  union {
    __float128 f;
    uint32_t bv[2];
  } data;
  union {
    __float128 f;
    uint32_t bv[2];
  } result;
  char tmp[256];

  data.bv[3] = 0x000064B5;
  data.bv[2] = 0x59A3D7F7;
  data.bv[1] = 0x56924E4F;
  data.bv[0] = 0xE681141C;

  quadmath_snprintf(tmp, sizeof(tmp), "%Qa", data.f);
  printf("Input: %s\n", tmp);

  result.f = sqrtq(data.f);

  quadmath_snprintf(tmp, sizeof(tmp), "%Qa", result.f);
  printf("Output: %s\n", tmp);

  printf("As BV: 0x");
  for (int i=3; i>=0; --i) {
    printf("%08x", result.bv[i]);
  }
  printf("\n");
}

The result should be: 0x1FFF4121A5EFB86CD358C0F1BA4AE60B
However we're getting: 0x1FFF4121A5EFB86CD358C0F1BA4AE60C