Skip to content

Commit 17bb823

Browse files
authored
Merge branch 'main' into codex/plan-changes-to-remove-if-costs
2 parents 932d124 + 38a6a40 commit 17bb823

File tree

21 files changed

+1362
-870
lines changed

21 files changed

+1362
-870
lines changed

infra/softposit.rkt

Lines changed: 33 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -176,16 +176,15 @@
176176
[<=.p8 #:spec (<= x y) #:impl posit8<= #:cost 1]
177177
[>=.p8 #:spec (>= x y) #:impl posit8>= #:cost 1])
178178

179-
(parameterize ([fpcore-context '(:precision posit8)])
180-
(define-operations ([x <posit8>]) <posit8>
181-
[neg.p8 #:spec (neg x) #:impl posit8-neg #:fpcore (- x) #:cost 1]
182-
[sqrt.p8 #:spec (sqrt x) #:impl posit8-sqrt #:cost 1])
179+
(define-operations ([x <posit8>]) <posit8> #:fpcore (:precision posit8)
180+
[neg.p8 #:spec (neg x) #:impl posit8-neg #:fpcore (- x) #:cost 1]
181+
[sqrt.p8 #:spec (sqrt x) #:impl posit8-sqrt #:cost 1])
183182

184-
(define-operations ([x <posit8>] [y <posit8>]) <posit8>
185-
[+.p8 #:spec (+ x y) #:impl posit8-add #:cost 1]
186-
[-.p8 #:spec (- x y) #:impl posit8-sub #:cost 1]
187-
[*.p8 #:spec (* x y) #:impl posit8-mul #:cost 1]
188-
[/.p8 #:spec (/ x y) #:impl posit8-div #:cost 1]))
183+
(define-operations ([x <posit8>] [y <posit8>]) <posit8> #:fpcore (:precision posit8)
184+
[+.p8 #:spec (+ x y) #:impl posit8-add #:cost 1]
185+
[-.p8 #:spec (- x y) #:impl posit8-sub #:cost 1]
186+
[*.p8 #:spec (* x y) #:impl posit8-mul #:cost 1]
187+
[/.p8 #:spec (/ x y) #:impl posit8-div #:cost 1])
189188

190189
(define-operations ([x <posit16>] [y <posit16>]) <bool>
191190
[==.p16 #:spec (== x y) #:impl posit16= #:cost 1]
@@ -194,16 +193,15 @@
194193
[<=.p16 #:spec (<= x y) #:impl posit16<= #:cost 1]
195194
[>=.p16 #:spec (>= x y) #:impl posit16>= #:cost 1])
196195

197-
(parameterize ([fpcore-context '(:precision posit16)])
198-
(define-operations ([x <posit16>]) <posit16>
199-
[neg.p16 #:spec (neg x) #:impl posit16-neg #:fpcore (- x) #:cost 1]
200-
[sqrt.p16 #:spec (sqrt x) #:impl posit16-sqrt #:cost 1])
196+
(define-operations ([x <posit16>]) <posit16> #:fpcore (:precision posit16)
197+
[neg.p16 #:spec (neg x) #:impl posit16-neg #:fpcore (- x) #:cost 1]
198+
[sqrt.p16 #:spec (sqrt x) #:impl posit16-sqrt #:cost 1])
201199

202-
(define-operations ([x <posit16>] [y <posit16>]) <posit16>
203-
[+.p16 #:spec (+ x y) #:impl posit16-add #:cost 1]
204-
[-.p16 #:spec (- x y) #:impl posit16-sub #:cost 1]
205-
[*.p16 #:spec (* x y) #:impl posit16-mul #:cost 1]
206-
[/.p16 #:spec (/ x y) #:impl posit16-div #:cost 1]))
200+
(define-operations ([x <posit16>] [y <posit16>]) <posit16> #:fpcore (:precision posit16)
201+
[+.p16 #:spec (+ x y) #:impl posit16-add #:cost 1]
202+
[-.p16 #:spec (- x y) #:impl posit16-sub #:cost 1]
203+
[*.p16 #:spec (* x y) #:impl posit16-mul #:cost 1]
204+
[/.p16 #:spec (/ x y) #:impl posit16-div #:cost 1])
207205

208206
(define-operations ([x <posit32>] [y <posit32>]) <bool>
209207
[==.p32 #:spec (== x y) #:impl posit32= #:cost 1]
@@ -212,37 +210,33 @@
212210
[<=.p32 #:spec (<= x y) #:impl posit32<= #:cost 1]
213211
[>=.p32 #:spec (>= x y) #:impl posit32>= #:cost 1])
214212

215-
(parameterize ([fpcore-context '(:precision posit32)])
216-
(define-operations ([x <posit32>]) <posit32>
217-
[neg.p32 #:spec (neg x) #:impl posit32-neg #:fpcore (- x) #:cost 1]
218-
[sqrt.p32 #:spec (sqrt x) #:impl posit32-sqrt #:cost 1])
213+
(define-operations ([x <posit32>]) <posit32> #:fpcore (:precision posit32)
214+
[neg.p32 #:spec (neg x) #:impl posit32-neg #:fpcore (- x) #:cost 1]
215+
[sqrt.p32 #:spec (sqrt x) #:impl posit32-sqrt #:cost 1])
219216

220-
(define-operations ([x <posit32>] [y <posit32>]) <posit32>
221-
[+.p32 #:spec (+ x y) #:impl posit32-add #:cost 1]
222-
[-.p32 #:spec (- x y) #:impl posit32-sub #:cost 1]
223-
[*.p32 #:spec (* x y) #:impl posit32-mul #:cost 1]
224-
[/.p32 #:spec (/ x y) #:impl posit32-div #:cost 1]))
217+
(define-operations ([x <posit32>] [y <posit32>]) <posit32> #:fpcore (:precision posit32)
218+
[+.p32 #:spec (+ x y) #:impl posit32-add #:cost 1]
219+
[-.p32 #:spec (- x y) #:impl posit32-sub #:cost 1]
220+
[*.p32 #:spec (* x y) #:impl posit32-mul #:cost 1]
221+
[/.p32 #:spec (/ x y) #:impl posit32-div #:cost 1])
225222

226223
;;;;;;;;;;;;;;;;;;;;;;;;;;;;; QUIRE OPERATIONS ;;;;;;;;;;;;;;;;;;;;;;;
227224

228225
(define-representation <quire8> #:cost 1)
229226
(define-representation <quire16> #:cost 1)
230227
(define-representation <quire32> #:cost 1)
231228

232-
(parameterize ([fpcore-context '(:precision quire8)])
233-
(define-operations ([x <quire8>] [y <posit8>] [z <posit8>]) <quire8>
234-
[quire8-mul-add #:spec (+ x (* y z)) #:impl quire8-fdp-add #:fpcore (fdp x y z) #:cost 1]
235-
[quire8-mul-sub #:spec (- x (* y z)) #:impl quire8-fdp-sub #:fpcore (fds x y z) #:cost 1]))
229+
(define-operations ([x <quire8>] [y <posit8>] [z <posit8>]) <quire8> #:fpcore (:precision quire8)
230+
[quire8-mul-add #:spec (+ x (* y z)) #:impl quire8-fdp-add #:fpcore (fdp x y z) #:cost 1]
231+
[quire8-mul-sub #:spec (- x (* y z)) #:impl quire8-fdp-sub #:fpcore (fds x y z) #:cost 1])
236232

237-
(parameterize ([fpcore-context '(:precision quire16)])
238-
(define-operations ([x <quire16>] [y <posit16>] [z <posit16>]) <quire16>
239-
[quire16-mul-add #:spec (+ x (* y z)) #:impl quire16-fdp-add #:fpcore (fdp x y z) #:cost 1]
240-
[quire16-mul-sub #:spec (- x (* y z)) #:impl quire16-fdp-sub #:fpcore (fds x y z) #:cost 1]))
233+
(define-operations ([x <quire16>] [y <posit16>] [z <posit16>]) <quire16> #:fpcore (:precision quire16)
234+
[quire16-mul-add #:spec (+ x (* y z)) #:impl quire16-fdp-add #:fpcore (fdp x y z) #:cost 1]
235+
[quire16-mul-sub #:spec (- x (* y z)) #:impl quire16-fdp-sub #:fpcore (fds x y z) #:cost 1])
241236

242-
(parameterize ([fpcore-context '(:precision quire32)])
243-
(define-operations ([x <quire32>] [y <posit32>] [z <posit32>]) <quire32>
244-
[quire32-mul-add #:spec (+ x (* y z)) #:impl quire32-fdp-add #:fpcore (fdp x y z) #:cost 1]
245-
[quire32-mul-sub #:spec (- x (* y z)) #:impl quire32-fdp-sub #:fpcore (fds x y z) #:cost 1]))
237+
(define-operations ([x <quire32>] [y <posit32>] [z <posit32>]) <quire32> #:fpcore (:precision quire32)
238+
[quire32-mul-add #:spec (+ x (* y z)) #:impl quire32-fdp-add #:fpcore (fdp x y z) #:cost 1]
239+
[quire32-mul-sub #:spec (- x (* y z)) #:impl quire32-fdp-sub #:fpcore (fds x y z) #:cost 1])
246240

247241
;;;;;;;;;;;;;;;;;;;;;;;;;;;;; CONVERTERS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
248242

src/api/server.rkt

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -171,9 +171,7 @@
171171
*reeval-pts*
172172
*node-limit*
173173
*max-find-range-depth*
174-
*pareto-mode*
175174
*platform-name*
176-
*loose-plugins*
177175
*functions*)
178176
(activate-platform! (*platform-name*))
179177
; not sure if the above code is actaully needed.
@@ -292,9 +290,7 @@
292290
*reeval-pts*
293291
*node-limit*
294292
*max-find-range-depth*
295-
*pareto-mode*
296293
*platform-name*
297-
*loose-plugins*
298294
*functions*)
299295
(activate-platform! (*platform-name*))
300296
(define worker-thread
@@ -506,7 +502,7 @@
506502
`(:pre ,(prog->fpcore (test-pre test) (test-context test))))
507503
,@(if (equal? (test-spec test) empty)
508504
'()
509-
`(:herbie-spec ,(prog->fpcore (test-spec test) (test-context test))))
505+
`(:spec ,(prog->fpcore (test-spec test) (test-context test))))
510506
,@(if (equal? (test-expected test) #t)
511507
'()
512508
`(:herbie-expected ,(test-expected test)))

src/config.rkt

Lines changed: 9 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -28,16 +28,7 @@
2828
[localize . ()]
2929
[generate . (rr taylor proofs evaluate)]
3030
[reduce . (regimes binary-search branch-expressions)]
31-
[rules
32-
. (arithmetic polynomials
33-
fractions
34-
exponents
35-
trigonometry
36-
hyperbolic
37-
numerics
38-
special
39-
bools
40-
branches)]
31+
[rules . (arithmetic polynomials fractions exponents trigonometry hyperbolic)]
4132
[dump . ()]))
4233

4334
(define (flag-deprecated? category flag)
@@ -51,6 +42,10 @@
5142
[('reduce 'avg-error) #t]
5243
[('localize 'costs) #t]
5344
[('localize 'errors) #t]
45+
[('rules 'numerics) #t]
46+
[('rules 'special) #t]
47+
[('rules 'bools) #t]
48+
[('rules 'branches) #t]
5449
[(_ _) #f]))
5550

5651
; `hash-copy` returns a mutable hash, which makes `dict-update` invalid
@@ -111,6 +106,10 @@
111106
(eprintf "The localize:errors option has been removed.\n")
112107
(eprintf " Herbie no longer performs localization.\n")
113108
(eprintf "See <herbie://herbie.uwplse.org/doc/~a/options.html> for more.\n" *herbie-version*)]
109+
[('rules _)
110+
(eprintf "The rules:~a ruleset has been removed.\n")
111+
(eprintf " These rules are no longer used by Herbie.\n")
112+
(eprintf "See <herbie://herbie.uwplse.org/doc/~a/options.html> for more.\n" *herbie-version*)]
114113
[(_ _) (void)]))
115114

116115
(define (changed-flags)
@@ -154,7 +153,6 @@
154153
(define *binary-search-accuracy* (make-parameter 48))
155154

156155
;; Pherbie related options
157-
(define *pareto-mode* (make-parameter #t))
158156
(define *pareto-pick-limit* (make-parameter 5))
159157

160158
;; If `:precision` is unspecified, which representation should we use?
@@ -163,9 +161,6 @@
163161
;; The platform that Herbie will evaluate with.
164162
(define *platform-name* (make-parameter (if (equal? (system-type 'os) 'windows) "c-windows" "c")))
165163

166-
;; Plugins loaded locally rather than through Racket.
167-
(define *loose-plugins* (make-parameter '()))
168-
169164
;; Sets the number of total points for Herbie to sample.
170165
(define *reeval-pts* (make-parameter 8000))
171166

src/core/batch.rkt

Lines changed: 77 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,38 @@
11
#lang racket
22

33
(require "../syntax/syntax.rkt"
4-
"../utils/common.rkt")
4+
"../utils/common.rkt"
5+
"../utils/alternative.rkt") ; for unbatchify-alts
56

6-
(provide progs->batch ; (Listof Expr) -> Batch
7-
batch->progs ; Batch -> ?(or (Listof Root) (Vectorof Root)) -> (Listof Expr)
7+
(provide progs->batch ; List<Expr> -> Batch
8+
batch->progs ; Batch -> ?(or List<Root> Vector<Root>) -> List<Expr>
89
(struct-out batch)
9-
(struct-out batchref) ; temporarily for patch.rkt
10-
(struct-out mutable-batch) ; temporarily for patch.rkt
10+
(struct-out batchref)
11+
(struct-out mutable-batch)
1112
batch-length ; Batch -> Integer
1213
batch-tree-size ; Batch -> Integer
1314
batch-free-vars
1415
batch-ref ; Batch -> Idx -> Expr
1516
deref ; Batchref -> Expr
1617
batch-replace ; Batch -> (Expr<Batchref> -> Expr<Batchref>) -> Batch
1718
debatchref ; Batchref -> Expr
18-
batch-remove-zombie ; Batch -> ?(Vectorof Root) -> Batch
19+
batch-alive-nodes ; Batch -> ?Vector<Root> -> Vector<Idx>
20+
batch-reconstruct-exprs ; Batch -> Vector<Expr>
21+
batch-remove-zombie ; Batch -> ?Vector<Root> -> Batch
1922
mutable-batch-munge! ; Mutable-batch -> Expr -> Root
2023
make-mutable-batch ; Mutable-batch
2124
batch->mutable-batch ; Batch -> Mutable-batch
2225
batch-copy-mutable-nodes! ; Batch -> Mutable-batch -> Void
2326
mutable-batch-push! ; Mutable-batch -> Node -> Idx
24-
batch-copy)
27+
batch-copy
28+
unbatchify-alts)
29+
30+
;; Batches store these recursive structures, flattened
31+
(struct batch ([nodes #:mutable] [roots #:mutable]))
32+
33+
(struct mutable-batch ([nodes #:mutable] [index #:mutable] cache))
34+
35+
(struct batchref (batch idx) #:transparent)
2536

2637
;; This function defines the recursive structure of expressions
2738
(define (expr-recurse expr f)
@@ -31,17 +42,24 @@
3142
[(list op args ...) (cons op (map f args))]
3243
[_ expr]))
3344

34-
;; Batches store these recursive structures, flattened
35-
(struct batch ([nodes #:mutable] [roots #:mutable]))
45+
;; Converts batchrefs of altns into expressions, assuming that batchrefs refer to batch
46+
(define (unbatchify-alts batch altns)
47+
(define exprs (batch-reconstruct-exprs batch))
48+
(define (unmunge altn)
49+
(define expr (alt-expr altn))
50+
(match expr
51+
[(? batchref?)
52+
(define expr* (vector-ref exprs (batchref-idx expr)))
53+
(struct-copy alt altn [expr expr*])]
54+
[_ altn]))
55+
(map (curry alt-map unmunge) altns))
3656

3757
(define (batch-length b)
3858
(cond
3959
[(batch? b) (vector-length (batch-nodes b))]
4060
[(mutable-batch? b) (hash-count (mutable-batch-index b))]
4161
[else (error 'batch-length "Invalid batch" b)]))
4262

43-
(struct mutable-batch ([nodes #:mutable] [index #:mutable] cache))
44-
4563
(define (make-mutable-batch)
4664
(mutable-batch '() (make-hash) (make-hasheq)))
4765

@@ -67,8 +85,6 @@
6785
(define (batch-copy b)
6886
(batch (vector-copy (batch-nodes b)) (vector-copy (batch-roots b))))
6987

70-
(struct batchref (batch idx) #:transparent)
71-
7288
(define (deref x)
7389
(match-define (batchref b idx) x)
7490
(expr-recurse (vector-ref (batch-nodes b) idx) (lambda (ref) (batchref b ref))))
@@ -105,10 +121,7 @@
105121
(munge expr))
106122

107123
(define (batch->progs b [roots (batch-roots b)])
108-
(define exprs (make-vector (batch-length b)))
109-
(for ([node (in-vector (batch-nodes b))]
110-
[idx (in-naturals)])
111-
(vector-set! exprs idx (expr-recurse node (lambda (x) (vector-ref exprs x)))))
124+
(define exprs (batch-reconstruct-exprs b))
112125
(for/list ([root roots])
113126
(vector-ref exprs root)))
114127

@@ -146,40 +159,64 @@
146159
(define roots (vector-map (curry vector-ref mapping) (batch-roots b)))
147160
(mutable-batch->batch out roots))
148161

149-
; The function removes any zombie nodes from batch with respect to the roots
150-
; Time complexity: O(|R| + |N|), where |R| - number of roots, |N| - length of nodes
151-
; Space complexity: O(|N| + |N*| + |R|), where |N*| is a length of nodes without zombie nodes
152-
; The flag keep-vars is used in compiler.rkt when vars should be preserved no matter what
153-
(define (batch-remove-zombie input-batch [roots (batch-roots input-batch)] #:keep-vars [keep-vars #f])
154-
(define nodes (batch-nodes input-batch))
155-
(define nodes-length (batch-length input-batch))
162+
;; Function returns indices of alive nodes within a batch for given roots,
163+
;; where alive node is a child of a root + meets a condition - (condition node)
164+
(define (batch-alive-nodes batch
165+
[roots (batch-roots batch)]
166+
#:keep-vars-alive [keep-vars-alive #f]
167+
#:condition [condition (const #t)])
168+
(define nodes (batch-nodes batch))
169+
(define nodes-length (batch-length batch))
170+
(define alive-mask (make-vector nodes-length #f))
171+
(for ([root (in-vector roots)])
172+
(vector-set! alive-mask root #t))
173+
(for ([i (in-range (- nodes-length 1) -1 -1)]
174+
[node (in-vector nodes (- nodes-length 1) -1 -1)]
175+
[alv (in-vector alive-mask (- nodes-length 1) -1 -1)]
176+
#:when (or (and alv (condition node)) (and keep-vars-alive (symbol? node))))
177+
(unless alv ; if keep-vars-alive then alv may not be #t, making sure it's #t
178+
(vector-set! alive-mask i #t))
179+
(expr-recurse node
180+
(λ (n)
181+
(when (condition (vector-ref nodes n))
182+
(vector-set! alive-mask n #t)))))
183+
; Return indices of alive nodes in ascending order
184+
(for/vector ([alv (in-vector alive-mask)]
185+
[i (in-naturals)]
186+
#:when alv)
187+
i))
188+
189+
;; Function constructs a vector of expressions for the given nodes of a batch
190+
(define (batch-reconstruct-exprs batch)
191+
(define exprs (make-vector (batch-length batch)))
192+
(for ([node (in-vector (batch-nodes batch))]
193+
[idx (in-naturals)])
194+
(vector-set! exprs idx (expr-recurse node (lambda (x) (vector-ref exprs x)))))
195+
exprs)
196+
197+
;; The function removes any zombie nodes from batch with respect to the roots
198+
;; Time complexity: O(|R| + |N|), where |R| - number of roots, |N| - length of nodes
199+
;; Space complexity: O(|N| + |N*| + |R|), where |N*| is a length of nodes without zombie nodes
200+
;; The flag keep-vars is used in compiler.rkt when vars should be preserved no matter what
201+
(define (batch-remove-zombie batch [roots (batch-roots batch)] #:keep-vars [keep-vars #f])
202+
(define nodes (batch-nodes batch))
203+
(define nodes-length (batch-length batch))
156204
(match (zero? nodes-length)
157205
[#f
158-
(define zombie-mask (make-vector nodes-length #t))
159-
(for ([root (in-vector roots)])
160-
(vector-set! zombie-mask root #f))
161-
(for ([i (in-range (- nodes-length 1) -1 -1)]
162-
[node (in-vector nodes (- nodes-length 1) -1 -1)]
163-
[zmb (in-vector zombie-mask (- nodes-length 1) -1 -1)])
164-
(when (and keep-vars (symbol? node))
165-
(vector-set! zombie-mask i #f))
166-
(unless zmb
167-
(expr-recurse node (λ (n) (vector-set! zombie-mask n #f)))))
206+
(define alive-nodes (batch-alive-nodes batch roots #:keep-vars-alive keep-vars))
168207

169208
(define mappings (make-vector nodes-length -1))
170209
(define (remap idx)
171210
(vector-ref mappings idx))
172211

173212
(define out (make-mutable-batch))
174-
(for ([node (in-vector nodes)]
175-
[zmb (in-vector zombie-mask)]
176-
[n (in-naturals)]
177-
#:unless zmb)
178-
(vector-set! mappings n (mutable-batch-push! out (expr-recurse node remap))))
213+
(for ([alv (in-vector alive-nodes)])
214+
(define node (vector-ref nodes alv))
215+
(vector-set! mappings alv (mutable-batch-push! out (expr-recurse node remap))))
179216

180217
(define roots* (vector-map (curry vector-ref mappings) roots))
181218
(mutable-batch->batch out roots*)]
182-
[#t (batch-copy input-batch)]))
219+
[#t (batch-copy batch)]))
183220

184221
(define (batch-ref batch reg)
185222
(define (unmunge reg)

0 commit comments

Comments
 (0)