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.
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.
The complex-herbie plugin has been removed as of Herbie 1.6. This plugin may be brought back in the future.
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).
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).
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-namein 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 (define herbie-plugin 'name) to the bottom of the file
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")
directly after the require statement.
Finally, run the following in the folder containing info.rkt
and main.rkt:
raco pkg installThis 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 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)
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?)
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.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])
+ 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] ...)
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] ...)
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] ...)
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)The following procedures handle generators:
(register-generator! gen)false.
(register-conversion-generator! gen)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?)
define-representation, but used within generators.
(register-representation-alias! name repr)
(register-operator! op name itype-names
otype-name attribs)
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)
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)
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) ...).