Plugins

Herbie plugins define new functions, add rewrite rules, and number representations. Users install plugins separately, and 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 supports 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.

Generic floating-point numbers

The float-herbie plugin implements support for any IEEE-754 binary floating-point number. To install, check out the source code and run

raco pkg install

at the top-level directory of the repository. Once float-herbie is installed, specify :precision (float ex nb) to inform Herbie that it should assume the core's inputs and outputs are floating-point numbers with ex exponent bits and nb total bits (sign bit + mantissa bits + exponent bits).

Generic fixed-point numbers

The fixedpoint-herbie plugin implements support for any fixed-point number. To install, check out the source code and run

raco pkg install

at the top-level directory of the repository. Once fixedpoint-herbie is installed, specify :precision (fixed nb sc) to inform Herbie that it should assume the core's inputs and outputs are signed fixed-point numbers with nb total bits and a scaling factor of 2sc (integer formats have a scaling factor of 20). This plugin also supports unsigned fixed-point numbers specified by :precision (ufixed nb sc) and provides simpler aliases for integer formats with :precision (integer nb) and :precision (uinteger nb).

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 file a bug. Be sure to check out the built-in plugins in the Herbie repository before getting started.

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: add (define herbie-plugin 'name) to the bottom of the file where name is a unique symbol that doesn't conflict with other Herbie plugins, like 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") directly after the require statement.

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

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

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 are required to be at 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 itype-names ...) otype-name
[bf bf-fn]
[ival ival-fn])
Adds a new operator. Operators describe pure mathematical functions, i.e. + or sin. The parameters itype-names and otype-name are the input type(s) and output type names. 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. To define operators with an unknown number of arguments, e.g. comparators, add the attribute [itype itype]. This will override the input type names defined by itype-names. See the bottom of this section for support for constants.
(define-operator-impl (op name irepr-names ...)orepr-name
[fl fl-fn]
...)
Implements op with input representation(s) irepr-names and output representation orepr-name. 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 and ival are inherited from op but can be overridden as previously described. See the bottom of this section for support for constant implementations.
(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.

Procedures for declaring constants are not a part of the plugin interface. Instead, constants and constant implementations are defined as zero-argument operators and operator implementations. The fields fl-fn, bf-fn, and ival-fn should be implemented with zero-argument procedures (thunks). Similar to operator and operator implementations, constants describe pure mathematical values like π or e while constant implementations define an approximation of those constants in a particular representation.

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 represention objects:

(get-representation name)
Takes a representation name and returns a representation object. Do not call this function before the associated representation has been registered!

The following procedures handle generators:

(register-generator! gen)
Adds a representation generator procedure to Herbie's set of generators. Representation generator procedures take the name of a representation and return the associated representation object if it successfully created the operators, constants, and rules for that representation. In the case that your plugin does not register the requested representation, the generator procedure need not do anything and should just return false.
(register-conversion-generator! gen)
Adds a conversion generator procedure to Herbie's set of generators. Conversion generator procedures take the names of two representations and returns true if it successfully registered conversion(s) between the two representations. Conversions are one-argument operator implementations of the cast operator that have one representation as an input representation and a different representation as an output representation. User-defined conversions are OPTIONAL for multi-precision optimization, since Herbie can synthesize these by default. However Herbie's implementations are often slow since they are representation-agnostic and work for any two representations. In the case that your plugin does not register the requested conversion(s), the generator procedure 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-representation-alias! name repr)
Adds an alias name for an existing representation repr. If two representations are equivalent, e.g. (float 8 32) and binary32, this procedure can be used to declare the two representations equivalent.
(register-operator! op name itype-names otype-name attribs)
Like define-operator, but used within generators. The argument itype-names 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. Unlike define-operator-impl, this procedure takes representation objects rather than representation names for ireprs and orepr. Use get-representation to produce these objects. See register-operator! for a description of attribs.
(register-ruleset! name groups var-repr-names rules)
Like define-ruleset, but used within generators. In this case, groups is a list of rule groups; var-repr-names 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) ...).