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.

The benchmark programs

Herbie ships a collection of binaries in its bench/ directory. For example, bench/tutorial.rkt 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.

Running Herbie

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.rkt > 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.