Plugins

Herbie plugins define new functions, add rewrite rules, and even implement number representations.

Herbie plugins are installed separately. Herbie then automatically loads and uses them.

Posit arithmetic

The softposit-herbie plugin implements support for posit arithmetic. Install it with:

raco pkg install --auto softposit-herbie

This plugin uses the SoftPosit library, only supported on Linux. Even then is reported to misbehave on some machines. The plugin support arithmetic operations, sqrt, and quires.

Once softposit-herbie is installed, specify :precision posit16 to inform Herbie that it should assume the core's inputs and outputs are posit numbers. Other posit sizes (with 8 or 32 bits) and also quires (for 8, 16, and 32 bit posits) are available, but are poorly supported.

Complex Numbers

The complex-herbie plugin implements support for complex numbers. Install it with:

raco pkg install --auto complex-herbie

Herbie input parameters are always real numbers; complex numbers must be constructed with complex. The functions re, im, and conj are available on complex numbers, along with the arithmetic operators, exp, log, pow, and sqrt. Complex and real operations use the same syntax, but cannot be mixed: (+ (complex 1 2) 1) is not valid. Herbie reports type errors in such situations.

Complex operations are implemented by Racket, so results may differ (slightly) from complex numbers in some other language, especially for non-finite complex numbers. In the future, we hope to support complex-number arguments and fully support all complex-number operations.

Developing plugins

The following is a guide to creating a Herbie plugin. Plugins are considered experimental and may change considerably between releases. If you run into issues, please write to the mailing list.

First Steps
All plugins are implemented as Racket packages. The easiest way to initialize a new Racket package is to run

raco pkg new pkg-name
in a new folder. Make sure the folder name is the same as the package name! This will initialize a Racket package with all the necessary files. Read the official Racket documentation on the raco tool for more information.

A single entry needs to be added to the package manifest stored in info.rkt, and Add the following line at the bottom of the file (define herbie-plugin 'name) where name is a unique symbol that doesn't conflict with other Herbie plugins. As a suggestion, this should just be the package name.

Next, edit the main.rkt file by erasing everything except the language specifier on the first line, and add the line (require herbie/plugin). This gives the package access to the Herbie plugin interface. Optionally add the following for debugging purposes (eprintf "Loading pkg-name support...\n").

Finally, run the following in the folder containing info.rkt and main.rkt:

raco pkg install
This should install your package and check for errors. Now everything is set up! Of course, your plugin is empty and doesn't add any useful features. If you added the debugging line in main.rkt, you should see the string when you run Herbie.

Adding Features
Now that you have an empty plugin, you can begin adding new functions, rewrite rules, and number representatons. The procedures exported by the Herbie plugin interface can be roughly divided into two categories: unique and parameterized. Whether or not you use the unique or parameterized half of the interface (or maybe both!) depends entirely on the number representation a feature is being implemented for. First, identify if your number representation is unique or parameterized. For example, if you are adding features for double precision (or rather binary64), the representation is unique. If you are adding features for a generic floating point format, say (float ebits nbits), then the representation is parameterized.

Plugin Interface (Unique)
The following are the signatures and descriptions of the plugin procedures for unique representations. These procedures should be called from the top-level of main.rkt rather than inside a function.

(define-type name (exact? inexact?) exact->inexact inexact->exact)
Adds a new type with the unique identifier name. The arguments exact? and inexact? return true if a value is an exact or high-precision approximate representation. For Herbie's real type, exact? is implemented with real? and inexact? is implemented with bigfloat?. The procedures exact->inexact and inexact->exact convert between exact? and inexact? values.
(define-representation (name type repr?) bigfloat->repr
repr->bigfloat
ordinal->repr
repr->ordinal
width
special?)
Adds a new representation with the unique identifier name. The representation will inherit all rewrite rules defined for type. By default, Herbie defines two types: real and bool. Your representation will most likely inherit from real. The width argument should be the bitwidth of the representation, e.g. 64 for binary64. The argument repr? is a procedure that accepts any argument and returns true if the argument is a value in the representation, e.g. an integer representation should use Racket's integer?, while special? takes a value in the representation and returns true if it is not finite, e.g. NaN or infinity.

The other four arguments are single-argument procedures that implement different conversions. The first two convert between a value in your representation and a Racket bigfloat (you need to import math/bigfloat). The last two convert between a value in your representation and its corresponding ordinal value. Ordinal values for any representation must be within the interval [0, 2width - 1]. Check Racket's definition of ordinals for floats. Note that those ordinal values can be negative.
(define-operator (name itypes ...) otype
[bf bf-fn]
[ival ival-fn]
[nonffi nonffi-fn]
...)
Adds a new operator. Operators describe pure mathematical functions, i.e. + or sin. The parameters itypes and otype are the input type(s) and output type. For example, + takes two real inputs and produces one real output. The bf-fn argument is the bigfloat implementation of your operator. The ival-fn argument is the Rival implementation of your operator. This is optional but improves the quality of Herbie's output. If you don't want to implement this, set ival-fn to false. The nonffi-fn argument is the exact implementation of your operator (see define-type for a description of exact). To define operators with an unknown number of arguments, e.g. comparators, add the attribute [itype itype]. This will override the input types defined by itypes.
(define-operator-impl (op name ireprs ...)orepr
[fl fl-fn]
...)
Implements op with input representation(s) ireprs and output representation orepr. The field name must be unique. For example, Herbie implements +.f64 and +.f32 for double- and single-precision floats. The argument fl-fn is the actual procedure that does the computation. Like define-operator, the input representations can be overridden with [itype irepr]. By default, the attributes bf, ival, and nonffi are inherited from op but can be overridden as previously described.
(define-constant name [bf bf-thunk] [ival ival-thunk])
Adds a new constant. Constants describe pure mathematical values. i.e. π or e. The bf-fn argument is a thunk that returns the bigfloat value of the constant. The ival-fn argument is a thunk that returns the Rival interval value of the constant.
(define-constant-impl (const name)repr
[fl fl-thunk]
...)
Implements const for the representation repr. The argument fl-thunk is a thunk that returns the approximate value of the constant in the representation repr. By default, the attributes bf and ival are inherited from const but can be overridden (see define-operator or define-operator-impl for overriding attributes).
(define-ruleset name (groups ...) #:type ([var repr] ...)
[rule-name match replace]
...)
Defines a set of rewrite rules. The name of the ruleset as well as each rule-name must be a unique symbol. Each ruleset must be marked with a set of groups (read here on ruleset groups). Each rewrite rule takes the form match ⇝ replace where Herbie's rewriter will replace match with replace (not vice-versa). Each match and replace is an expression whose operators are the names of operator implementations rather than pure mathematical operators. Any variable must be listed in the type information with its associated representation. See the softposit-herbie plugin for a more concrete example.
(define-ruleset* name (groups ...) #:type ([var type] ...)
[rule-name match replace]
...)
Like define-ruleset, but it defines a ruleset for every representation that inherits from type. Currently, every type must be the same, e.g. all real, for this procedure to function correctly. Unlike define-ruleset, match and replace contain the names of operators rather than operator implementations.

Plugin Interface (Parameterized)
Defining operators, constants, and representations for parameterized functions requires a generator procedure for just-in-time loading of features for a particular representation. When Herbie encounters a representation it does not recognize (not explicitly defined using define-representation) it queries a list of generators in case the representation requires just-in-time loading.

The following procedure handles generators:

(register-generator! gen)
Adds a generator procedure to Herbie's set of generators. Generator procedures take the name of a representation and return whether it successfully created the operators, constants, and rules associated with a particular representation. In the case that your plugin does not define the requested representation, the generator procedure(s) need not do anything and should just return false.

To actually add representations, operators, etc. within a generator procedure, you must use a set of alternate procedures.

(register-representation! name
type
repr?
bigfloat->repr
repr->bigfloat
ordinal->repr
repr->ordinal
width
special?)
Like define-representation, but used within generators.
(register-operator! op name itypes otype attribs)
Like define-operator, but used within generators. The argument itypes is a list of the input types while the argument attribs are the same attributes for define-operator, e.g. bf. In this case, attribs is an association: (list (cons 'bf bf-fn) ...).
(register-operator-impl! op name ireprs orepr attribs)
Like define-operator-impl, but used within generators. See register-operator! for a description of ireprs and attribs.
(register-constant! name attribs)
Like define-constant, but used within generators. The argument attribs are the same attributes for define-constant. In this case, attribs is an association: (list (cons 'bf bf-thunk) ...).
(register-constant-impl! const name type attribs)
Like define-constant-impl, but used within generators. See register-constant! for a description of attribs.
(register-ruleset! name groups var-reprs rules)
Like define-ruleset, but used within generators. In this case, groups is a list of rule groups; var-reprs is an association pairing each variable in the ruleset with its representation, e.g. (list (cons 'x '(float 5 16)) ...); and rules is a list of rules of the following form (list (list rule-name match replace) ...).