Skip to content

Commit 7e01615

Browse files
authored
Merge pull request #1312 from herbie-fp/fl-generator
Implementation generators for platforms
2 parents 6fe2426 + 4b608ec commit 7e01615

File tree

16 files changed

+834
-695
lines changed

16 files changed

+834
-695
lines changed

infra/softposit.rkt

Lines changed: 4 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -92,16 +92,9 @@
9292

9393
;;;;;;;;;;;;;;;;;;;;;;;;;;;;; REPRESENTATIONS ;;;;;;;;;;;;;;;;;;;;;;;
9494

95-
(define bool
96-
(make-representation #:name 'bool
97-
#:type 'bool
98-
#:repr? boolean?
99-
#:bf->repr identity
100-
#:repr->bf identity
101-
#:ordinal->repr (λ (x) (= x 0))
102-
#:repr->ordinal (λ (x) (if x 1 0))
103-
#:total-bits 1
104-
#:special-value? (const #f)))
95+
(define bool <bool>)
96+
97+
(define binary64 <binary64>)
10598

10699
(define posit8
107100
(make-representation #:name 'posit8
@@ -169,26 +162,14 @@
169162
#:total-bits 64
170163
#:special-value? (const #f)))
171164

172-
; Binary64 is needed for casting from double to softposit formats
173-
(define binary64
174-
(make-representation #:name 'binary64
175-
#:type 'real
176-
#:repr? flonum?
177-
#:bf->repr bigfloat->flonum
178-
#:repr->bf bf
179-
#:ordinal->repr (shift 63 ordinal->flonum)
180-
#:repr->ordinal (unshift 63 flonum->ordinal)
181-
#:total-bits 64
182-
#:special-value? nan?))
183-
184165
(platform-register-representation! platform #:repr bool #:cost cost)
166+
(platform-register-representation! platform #:repr binary64 #:cost cost)
185167
(platform-register-representation! platform #:repr posit8 #:cost cost)
186168
(platform-register-representation! platform #:repr posit16 #:cost cost)
187169
(platform-register-representation! platform #:repr posit32 #:cost cost)
188170
(platform-register-representation! platform #:repr quire8 #:cost cost)
189171
(platform-register-representation! platform #:repr quire16 #:cost cost)
190172
(platform-register-representation! platform #:repr quire32 #:cost cost)
191-
(platform-register-representation! platform #:repr binary64 #:cost cost)
192173

193174
;;;;;;;;;;;;;;;;;;;;;;;;;;;;; OPERATORS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
194175

src/config.rkt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@
161161
(define *default-precision* (make-parameter 'binary64))
162162

163163
;; The platform that Herbie will evaluate with.
164-
(define *platform-name* (make-parameter "c"))
164+
(define *platform-name* (make-parameter (if (equal? (system-type 'os) 'windows) "c-windows" "c")))
165165

166166
;; Plugins loaded locally rather than through Racket.
167167
(define *loose-plugins* (make-parameter '()))

src/platforms/c-windows.rkt

Lines changed: 251 additions & 0 deletions
Large diffs are not rendered by default.

src/platforms/c.rkt

Lines changed: 95 additions & 112 deletions
Large diffs are not rendered by default.

src/platforms/herbie10.rkt

Lines changed: 96 additions & 115 deletions
Large diffs are not rendered by default.

src/platforms/herbie20.rkt

Lines changed: 96 additions & 113 deletions
Large diffs are not rendered by default.

src/platforms/math.rkt

Lines changed: 49 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@
66

77
(require math/bigfloat
88
math/flonum
9-
"runtime/libm.rkt" ; libm wrapper in Racket
109
"../utils/float.rkt" ; for shift/unshift
1110
"../syntax/platform.rkt")
1211
(provide platform)
@@ -100,64 +99,58 @@
10099

101100
;;;;;;;;;;;;;;;;;;;;;;;;;;;;; libm operators ;;;;;;;;;;;;;;;;;;;;;;;;
102101

103-
(define libm-impls.f64
104-
(make-libm-impls/binary64
105-
[(binary64 binary64)
106-
([fabs 0.10162]
107-
[sin 3.318128]
108-
[cos 3.32288]
109-
[tan 3.710904]
110-
[sinh 1.20954]
111-
[cosh 0.953896]
112-
[acos 0.357748]
113-
[acosh 0.659472]
114-
[asin 0.389788]
115-
[asinh 0.835028]
116-
[atan 0.83752]
117-
[atanh 0.36238]
118-
[cbrt 1.565176]
119-
[ceil 0.47299]
120-
[erf 0.806436]
121-
[exp 1.0806]
122-
[exp2 0.825484]
123-
[floor 0.468568]
124-
[lgamma 1.568012]
125-
[log 0.505724]
126-
[log10 0.868856]
127-
[log2 0.681276]
128-
[logb 0.220656]
129-
[rint 0.121864]
130-
[round 0.658564]
131-
[sqrt 0.191872]
132-
[tanh 0.824016]
133-
[tgamma 1.882576]
134-
[trunc 0.463644])]
135-
[(binary64 binary64 binary64)
136-
([pow 1.52482]
137-
[atan2 1.492804]
138-
[copysign 0.200452]
139-
[fdim 0.592576]
140-
[fmax 0.3106]
141-
[fmin 0.289256]
142-
[fmod 94.277144]
143-
[remainder 16.165012])]))
144-
145-
(for ([libm-impl.f64 (in-list libm-impls.f64)]
146-
#:when libm-impl.f64)
147-
(platform-register-implementation! platform libm-impl.f64))
102+
; ([name ([var : repr] ...) otype spec fl fpcore cost])
103+
(platform-register-implementations!
104+
platform
105+
(; Unary libm operators
106+
[fabs.f64 ([x : binary64]) binary64 (fabs x) (from-libm 'fabs) (! :precision binary64 (fabs x)) 0.10162]
107+
[sin.f64 ([x : binary64]) binary64 (sin x) (from-libm 'sin) (! :precision binary64 (sin x)) 3.318128]
108+
[cos.f64 ([x : binary64]) binary64 (cos x) (from-libm 'cos) (! :precision binary64 (cos x)) 3.32288]
109+
[tan.f64 ([x : binary64]) binary64 (tan x) (from-libm 'tan) (! :precision binary64 (tan x)) 3.710904]
110+
[sinh.f64 ([x : binary64]) binary64 (sinh x) (from-libm 'sinh) (! :precision binary64 (sinh x)) 1.20954]
111+
[cosh.f64 ([x : binary64]) binary64 (cosh x) (from-libm 'cosh) (! :precision binary64 (cosh x)) 0.953896]
112+
[acos.f64 ([x : binary64]) binary64 (acos x) (from-libm 'acos) (! :precision binary64 (acos x)) 0.357748]
113+
[acosh.f64 ([x : binary64]) binary64 (acosh x) (from-libm 'acosh) (! :precision binary64 (acosh x)) 0.659472]
114+
[asin.f64 ([x : binary64]) binary64 (asin x) (from-libm 'asin) (! :precision binary64 (asin x)) 0.389788]
115+
[asinh.f64 ([x : binary64]) binary64 (asinh x) (from-libm 'asinh) (! :precision binary64 (asinh x)) 0.835028]
116+
[atan.f64 ([x : binary64]) binary64 (atan x) (from-libm 'atan) (! :precision binary64 (atan x)) 0.83752]
117+
[atanh.f64 ([x : binary64]) binary64 (atanh x) (from-libm 'atanh) (! :precision binary64 (atanh x)) 0.36238]
118+
[cbrt.f64 ([x : binary64]) binary64 (cbrt x) (from-libm 'cbrt) (! :precision binary64 (cbrt x)) 1.565176]
119+
[ceil.f64 ([x : binary64]) binary64 (ceil x) (from-libm 'ceil) (! :precision binary64 (ceil x)) 0.47299]
120+
[erf.f64 ([x : binary64]) binary64 (erf x) (from-libm 'erf) (! :precision binary64 (erf x)) 0.806436]
121+
[exp.f64 ([x : binary64]) binary64 (exp x) (from-libm 'exp) (! :precision binary64 (exp x)) 1.0806]
122+
[exp2.f64 ([x : binary64]) binary64 (exp2 x) (from-libm 'exp2) (! :precision binary64 (exp2 x)) 0.825484]
123+
[floor.f64 ([x : binary64]) binary64 (floor x) (from-libm 'floor) (! :precision binary64 (floor x)) 0.468568]
124+
[lgamma.f64 ([x : binary64]) binary64 (lgamma x) (from-libm 'lgamma) (! :precision binary64 (lgamma x)) 1.568012]
125+
[log.f64 ([x : binary64]) binary64 (log x) (from-libm 'log) (! :precision binary64 (log x)) 0.505724]
126+
[log10.f64 ([x : binary64]) binary64 (log10 x) (from-libm 'log10) (! :precision binary64 (log10 x)) 0.868856]
127+
[log2.f64 ([x : binary64]) binary64 (log2 x) (from-libm 'log2) (! :precision binary64 (log2 x)) 0.681276]
128+
[logb.f64 ([x : binary64]) binary64 (logb x) (from-libm 'logb) (! :precision binary64 (logb x)) 0.220656]
129+
[rint.f64 ([x : binary64]) binary64 (rint x) (from-libm 'rint) (! :precision binary64 (rint x)) 0.121864]
130+
[round.f64 ([x : binary64]) binary64 (round x) (from-libm 'round) (! :precision binary64 (round x)) 0.658564]
131+
[sqrt.f64 ([x : binary64]) binary64 (sqrt x) (from-libm 'sqrt) (! :precision binary64 (sqrt x)) 0.191872]
132+
[tanh.f64 ([x : binary64]) binary64 (tanh x) (from-libm 'tanh) (! :precision binary64 (tanh x)) 0.824016]
133+
[tgamma.f64 ([x : binary64]) binary64 (tgamma x) (from-libm 'tgamma) (! :precision binary64 (tgamma x)) 1.882576]
134+
[trunc.f64 ([x : binary64]) binary64 (trunc x) (from-libm 'trunc) (! :precision binary64 (trunc x)) 0.463644]
135+
; Binary libm operators
136+
[pow.f64 ([x : binary64] [y : binary64]) binary64 (pow x y) (from-libm 'pow) (! :precision binary64 (pow x y)) 1.52482]
137+
[atan2.f64 ([x : binary64] [y : binary64]) binary64 (atan2 x y) (from-libm 'atan2) (! :precision binary64 (atan2 x y)) 1.492804]
138+
[copysign.f64 ([x : binary64] [y : binary64]) binary64 (copysign x y) (from-libm 'copysign) (! :precision binary64 (copysign x y)) 0.200452]
139+
[fdim.f64 ([x : binary64] [y : binary64]) binary64 (fdim x y) (from-libm 'fdim) (! :precision binary64 (fdim x y)) 0.592576]
140+
[fmax.f64 ([x : binary64] [y : binary64]) binary64 (fmax x y) (from-libm 'fmax) (! :precision binary64 (fmax x y)) 0.3106]
141+
[fmin.f64 ([x : binary64] [y : binary64]) binary64 (fmin x y) (from-libm 'fmin) (! :precision binary64 (fmin x y)) 0.289256]
142+
[fmod.f64 ([x : binary64] [y : binary64]) binary64 (fmod x y) (from-libm 'fmod) (! :precision binary64 (fmod x y)) 94.277144]
143+
[remainder.f64 ([x : binary64] [y : binary64]) binary64 (remainder x y) (from-libm 'remainder) (! :precision binary64 (remainder x y)) 16.165012]))
148144

149145
;;;;;;;;;;;;;;;;;;;;;;;;;;;;; libm accelerators ;;;;;;;;;;;;;;;;;;;;;
150146

151-
(define c_erfc (make-libm (erfc double double)))
152-
153-
(when c_erfc
154-
(platform-register-implementation! platform
155-
(make-operator-impl (erfc.f64 [x : binary64])
156-
binary64
157-
#:spec (- 1 (erf x))
158-
#:fpcore (! :precision binary64 (erfc x))
159-
#:fl c_erfc
160-
#:cost 0.816512)))
147+
(platform-register-implementation! platform
148+
(make-operator-impl (erfc.f64 [x : binary64])
149+
binary64
150+
#:spec (- 1 (erf x))
151+
#:fpcore (! :precision binary64 (erfc x))
152+
#:fl (from-libm 'erfc)
153+
#:cost 0.816512))
161154

162155
;;;;;;;;;;;;;;;;;;;;;;;;;;;;; REGISTER PLATFORM ;;;;;;;;;;;;;;;;;;;;;
163156

src/platforms/racket.rkt

Lines changed: 18 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -128,20 +128,25 @@
128128
(define res (apply fun xs))
129129
(if (real? res) res +nan.0))
130130

131-
(define ((from-bigfloat bff) . args)
132-
(bigfloat->flonum (apply bff (map bf args))))
133-
134131
(define (bffmod x mod)
135-
(bf- x (bf* (bftruncate (bf/ x mod)) mod)))
132+
(bigfloat->flonum (bf- (bf x) (bf* (bftruncate (bf/ (bf x) (bf mod))) (bf mod)))))
136133

137134
(define (bffma x y z)
138-
(bf+ (bf* x y) z))
135+
(bigfloat->flonum (bf+ (bf* (bf x) (bf y)) (bf z))))
139136

140137
;;;;;;;;;;;;;;;;;;;;;;;;;;;;; unary operators ;;;;;;;;;;;;;;;;;;;;;;;
141138

139+
;; neg operation has a specific format with regard to fpcore, (- x) instead of (neg x)
140+
(platform-register-implementation! platform
141+
(make-operator-impl (neg.rkt [x : binary64])
142+
binary64
143+
#:spec (neg x)
144+
#:fpcore (! :precision binary64 (- x))
145+
#:fl -
146+
#:cost 1))
147+
142148
; ([op fn cost] ...)
143149
(register-1ary-racket-operators
144-
[neg - 1]
145150
[acos (no-complex acos) 1]
146151
[acosh (no-complex acosh) 1]
147152
[asin (no-complex asin) 1]
@@ -160,7 +165,7 @@
160165
[lgamma log-gamma 1]
161166
[log (no-complex log) 1]
162167
[log10 (no-complex (λ (x) (log x 10))) 1]
163-
[log2 (from-bigfloat bflog2) 1]
168+
[log2 (from-bigfloat 'bflog2) 1]
164169
[logb (λ (x) (floor (bigfloat->flonum (bflog2 (bf (abs x)))))) 1]
165170
[rint round 1]
166171
[round round 1]
@@ -196,7 +201,7 @@
196201
[(nan? x) y]
197202
[(nan? y) x]
198203
[else (min x y)])) 1]
199-
[fmod (from-bigfloat bffmod) 1]
204+
[fmod bffmod 1]
200205
[pow (no-complex expt) 1]
201206
[remainder remainder 1])
202207

@@ -205,11 +210,11 @@
205210
; ([name ([var : repr] ...) otype spec fl fpcore cost])
206211
(platform-register-implementations!
207212
platform
208-
([erfc.rkt ([x : binary64]) binary64 (- 1 (erf x)) erfc (! :precision binary64 (erfc x)) 1]
209-
[expm1.rkt ([x : binary64]) binary64 (- (exp x) 1) (from-bigfloat bfexpm1) (! :precision binary64 (expm1 x)) 1]
210-
[log1p.rkt ([x : binary64]) binary64 (log (+ 1 x)) (from-bigfloat bflog1p) (! :precision binary64 (log1p x)) 1]
211-
[hypot.rkt ([x : binary64] [y : binary64]) binary64 (sqrt (+ (* x x) (* y y))) (from-bigfloat bfhypot) (! :precision binary64 (hypot x y)) 1]
212-
[fma.rkt ([x : binary64] [y : binary64] [z : binary64]) binary64 (+ (* x y) z) (from-bigfloat bffma) (! :precision binary64 (fma x y z)) 1]))
213+
([erfc.rkt ([x : binary64]) binary64 (- 1 (erf x)) erfc (! :precision binary64 (erfc x)) 1]
214+
[expm1.rkt ([x : binary64]) binary64 (- (exp x) 1) (from-bigfloat 'bfexpm1) (! :precision binary64 (expm1 x)) 1]
215+
[log1p.rkt ([x : binary64]) binary64 (log (+ 1 x)) (from-bigfloat 'bflog1p) (! :precision binary64 (log1p x)) 1]
216+
[hypot.rkt ([x : binary64] [y : binary64]) binary64 (sqrt (+ (* x x) (* y y))) (from-bigfloat 'bfhypot) (! :precision binary64 (hypot x y)) 1]
217+
[fma.rkt ([x : binary64] [y : binary64] [z : binary64]) binary64 (+ (* x y) z) bffma (! :precision binary64 (fma x y z)) 1]))
213218

214219
;;;;;;;;;;;;;;;;;;;;;;;;;;;;; REGISTER PLATFORM ;;;;;;;;;;;;;;;;;;;;;
215220

0 commit comments

Comments
 (0)