FPBench Logo

FPBench Tools

Interpreters and exporters for FPCore

FPBench develops two compiler tools for FPCore programs: 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:

racket
Welcome to Racket v7.3.
> (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
C, using the C 99 version of the language.
go
Go, using version 1.12 of the language.
js
JavaScript, specifically as standardized in ECMAScript Harmony.
fptaylor
The input format for the FPTaylor error estimation tool.
gappa
The input format for the Gappa verification tool.
scala
Scala, or more specifically the input format for the Daisy compiler.
sollya
The input format for the Sollya tool.
smt2
SMT-LIB2 using the floating-point theory.
wls
Wolfram Language, for use in Mathematica.

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

--bare
For c, go, and scala export, skip the file header and footer.
--namespace
For go and scala export, the name of the top-level object or package name.
--runtime
For js export, a library to invoke mathematical operations on instead of Math.
--rel-error
For gappa export, produce expressions for relative instead of absolute error.
--scale
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.
--skip-loops
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*.
--precondition-ranges
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.
--precondition-range
Like --precondition-ranges, but further weakens to precondition to a conjunction of single ranges for each variable.
--expand-let*
Expands each let* to a series of nested let expressions.
--expand-while*
Expands each while* to a while loop with nested let* expressions.
--cse
Lifts each common subexpression to an intermediate variable bound by a let* expression.
--subexprs
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.