From 031f7a99f4a610ee94be68c8d85ba3ec45f8a1e0 Mon Sep 17 00:00:00 2001 From: Pavel Panchekha Date: Mon, 9 Sep 2024 10:49:52 -0600 Subject: [PATCH] Deleted tools.html --- tools.html | 217 ----------------------------------------------------- 1 file changed, 217 deletions(-) delete mode 100644 tools.html diff --git a/tools.html b/tools.html deleted file mode 100644 index e959ea9..0000000 --- a/tools.html +++ /dev/null @@ -1,217 +0,0 @@ - - - - - FPBench Tools - - - -
- - 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: -

- - 
racket
-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
-
C, using the C 99 version of the language.
-
cakeml
-
CakeML version v1217 from the GitHub repository.
-
f03
-
Fortran 2003 using the gfortran compiler
-
go
-
Go, using version 1.12 of the language.
-
hs
-
Haskell version 9.8.1
-
java
-
Java version 11 as provided by Temurin
-
js
-
JavaScript, specifically as standardized in ECMAScript Harmony.
-
jl
-
Julia version 1.8.
-
mat
-
Matlab language release version R2023a.
-
ocaml
-
OCaml using version 4.04.2 of the compiler.
-
py
-
Python version 3.10.
-
rs
-
The Rust programming language version 1.71.0.
- -
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.
-
tex
-
The math sublanguage in LaTeX
-
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.

- - -