Using Herbie
Herbie rewrites floating point expressions to make them more accurate. The expressions could come from anywhere—your source code, mathematical papers, or even the output of Herbgrind, our tool for finding inaccurate expressions in binaries. This tutorial run Herbie on the benchmark programs that Herbie ships with.
Herbie ships a collection of binaries in its bench/
directory. For example, bench/tutorial.fpcore contains the following code:
(FPCore (x) :name "Cancel like terms" (- (+ 1 x) x)) (FPCore (x) :name "Expanding a square" (- (sqr (+ x 1)) 1)) (FPCore (x y z) :name "Commute and associate" (- (+ (+ x y) z) (+ x (+ y z))))
This code defines three floating point expressions that we want to
run Herbie on: the expression (1 + x) - x, the
expression (x + 1)² - 1, and finally the
expression ((x + y) + z) - (x + (y + z)). You can
check out our input format documentation
for more information about how to format Herbie inputs.
Let's analyze these three examples using Herbie. Run Herbie:
racket src/herbie.rkt
After a few seconds, Herbie will start up and wait for input:
$ racket src/herbie.rkt Seed: #(4084085515 1217806925 3915723770 1268025332 545417352 1092579889)
You can now paste inputs directly into your terminal for Herbie to improve:
(FPCore (x) :name "Cancel like terms" (- (+ 1 x) x)) [ 1586.644ms] Cancel like terms (29→ 0) (FPCore (x) :name "Cancel like terms" 1)
Alternatively, you can run Herbie on a file with expressions with:
$ racket src/herbie.rkt bench/tutorial.fpcore > out.rkt Seed: #(1637424072 4209802118 1686524629 1009825284 4285017075 2209820745) [ 1563.552ms] Cancel like terms (29→ 0) [ 4839.121ms] Expanding a square (38→ 0) [ 3083.238ms] Commute and associate ( 0→ 0)
The output file out.rkt contains more accurate
versions of each program:
(FPCore (x) :name "Cancel like terms" 1) (FPCore (x) :name "Expanding a square" (+ (* x 2) (* x x))) (FPCore (x y z) :name "Commute and associate" (- (+ (+ x y) z) (+ x (+ y z))))
Note that the final expression was not simplified to 0 by Herbie,
since the difference in accuracy is negligible.
For more control over Herbie, see the documentation of Herbie's command-line options.