FPBench Logo

FPBench Tools

Export and transform FPCores

FPBench ships two compiler tools for FPCore: an exporter and a transformation tool. Both are available on Github.

Installing the FPBench tools

The FPBench tools require Racket. Use the official installer to install Racket, or use distro-provided packages provided they are version 7.0 or later of Racket (earlier versions are not supported).

Test that Racket is installed correctly and has a correct version:

Welcome to Racket v7.7.
> (exit)

Now that Racket is installed, download the FPBench tools, and enter the downloaded directory. Run:

make setup

This byte-compiles the FPBench tools, making them fast to run.

Exporting FPCores to other languages

The FPBench exporter compiles FPCore programs to another language. The exporter allows FPBench's benchmarks to be used by tools with a custom input format. The exporter is invoked like so:

racket export.rkt input.fpcore output.lang

For example, to compile benchmarks/rump.fpcore to C, run:

racket export.rkt benchmarks/rump.fpcore rump.c

The exporter infers the output language from the file extension, and will signal an error if the extension is unknown. The --lang flag can be used to override the file extension.

Supported languages include:

C, using the C 99 version of the language.
CakeML version v1217 from the GitHub repository.
Fortran 2003 using the gfortran compiler
Go, using version 1.12 of the language.
Haskell version 9.8.1
Java version 11 as provided by Temurin
JavaScript, specifically as standardized in ECMAScript Harmony.
Julia version 1.8.
Matlab language release version R2023a.
OCaml using version 4.04.2 of the compiler.
Python version 3.10.
The Rust programming language version 1.71.0.
The input format for the FPTaylor error estimation tool.
The input format for the Gappa verification tool.
Scala, or more specifically the input format for the Daisy compiler.
The input format for the Sollya tool.
SMT-LIB2 using the floating-point theory.
The math sublanguage in LaTeX
Wolfram Language, for use in Mathematica.

The exporter also supports additional, language-dependent flags, including:

For c, go, and scala export, skip the file header and footer.
For go and scala export, the name of the top-level object or package name.
For js export, a library to invoke mathematical operations on instead of Math.
For gappa export, produce expressions for relative instead of absolute error.
For fptaylor export, the scale factor for operations which are not correctly rounded.

The argument - can be used in place of the input or output file names to use standard input and output. When outputting to standard out, the --lang flag is necessary to specify the output language.

Applying transformations to FPCores

The FPBench transformation tool applies a variety of transformations to FPCore programs, such as common subexpression elimination, precondition simplification, and de- and resugaring. The transformation tool is invoked like so:

racket transform.rkt args ... input.fpcore output.fpcore

The list args of arguments names a list of transformations, such as:

--unroll N
Unroll the first N iterations of each loop. Each iteration consists of a let or let* to bind initial values and an if to check the conditions. This sound transformation is frequently combined with the unsound --skip-loops to simulate loops by their first few iterations.
Replaces a while loop with a simple let which binds the initial values and executes the body (as if the loop executed zero time). while* loops are likewise transformed into let*.
Weakens the precondition to a conjunction (one conjunct per argument) of a disjunction of ranges. The precondition is guaranteed to be weaker. This transformation is useful for exporting to a language that only allows ranges as preconditions.
Like --precondition-ranges, but further weakens to precondition to a conjunction of single ranges for each variable.
Expands each let* to a series of nested let expressions.
Expands each while* to a while loop with nested let* expressions.
Lifts each common subexpression to an intermediate variable bound by a let* expression.
Converts each FPCore into multiple FPCores, one for each subexpression in the original.

The transformations which are applied in order (left to right) to each FPCore expression in the input file. The ordering is especially important for pairs of operations such as --unroll and --skip-loops.

Like for the exporter, the argument - can be used in place of the input or output file names to use standard input and output.