Skip to content

Commit

Permalink
Replace term-cache with (terms) and (with-terms ...).
Browse files Browse the repository at this point in the history
  • Loading branch information
@emina
emina committed Feb 16, 2021
1 parent 91d25ea commit 490c4fe
Show file tree
Hide file tree
Showing 18 changed files with 356 additions and 246 deletions.
3 changes: 2 additions & 1 deletion rosette/base/base.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,8 @@
symbolics type? solvable? @any/c type-of type-cast for/all for*/all
term? constant? expression?
term expression constant term-type
term=? term->datum clear-terms! term-cache weak-term-cache
term=? term->datum
terms terms-count terms-ref with-terms clear-terms! gc-terms!
union? union union-contents union-guards union-values
union-filter in-union in-union* in-union-guards in-union-values
result? result-value result-state normal normal? failed failed?
Expand Down
2 changes: 1 addition & 1 deletion rosette/base/core/bool.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -477,4 +477,4 @@
(parameterize ([current-vc vc0])
(with-handlers ([exn:fail:svm? halt-svm]
[exn:fail? halt-err])
(normal body (current-vc)))))]))
(normal (let () body) (current-vc)))))]))
4 changes: 2 additions & 2 deletions rosette/base/core/reflect.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@
(provide type? solvable? @any/c type-of type-cast for/all for*/all
term? constant? expression?
term expression constant
term-type term=?
term->datum clear-terms! term-cache weak-term-cache
term-type term=? term->datum
terms terms-count terms-ref with-terms clear-terms! gc-terms!
union? union union-contents union-guards union-values
union-filter in-union in-union* in-union-guards in-union-values
(struct-out normal) (struct-out failed) result? result-value result-state
Expand Down
70 changes: 52 additions & 18 deletions rosette/base/core/term.rkt
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
#lang racket

(require racket/syntax (for-syntax racket racket/syntax) racket/generic
(require racket/syntax (for-syntax racket racket/syntax syntax/parse)
racket/generic syntax/parse
"type.rkt" "reporter.rkt")

(provide
term-cache clear-terms! weak-term-cache
terms terms-count terms-ref with-terms clear-terms! gc-terms! term-cache
term? constant? expression?
(rename-out [a-term term] [an-expression expression] [a-constant constant] [term-ord term-id])
term-type term<? sublist? @app
Expand Down Expand Up @@ -40,22 +41,55 @@
(set-add! evicted t))
(loop))))))

; Returns a garbage-collected (weak) hash that can be used as a term-cache.
; The returned cache is populated with the contents of (term-cache).
(define (weak-term-cache)
(define cache
(impersonate-hash
(make-weak-hash)
(lambda (h k)
(values k (lambda (h k e) (ephemeron-value e #f))))
(lambda (h k v)
(values k (make-ephemeron k v)))
(lambda (h k) k)
(lambda (h k) k)
hash-clear!))
(for ([(k v) (term-cache)])
(hash-set! cache k v))
cache)
; Sets the current term-cache to a garbage-collected (weak) hash.
; The setting preserves all reachable terms from (term-cache).
(define (gc-terms!)
(unless (hash-weak? (term-cache)) ; Already a weak hash.
(define cache
(impersonate-hash
(make-weak-hash)
(lambda (h k)
(values k (lambda (h k e) (ephemeron-value e #f))))
(lambda (h k v)
(values k (make-ephemeron k v)))
(lambda (h k) k)
(lambda (h k) k)
hash-clear!))
(for ([(k v) (term-cache)])
(hash-set! cache k v))
(term-cache cache)))

; Returns the term in the given term cache that has the given contents. If
; no such term exists, failure-result is returned, unless it is a procedure.
; If failure-result is a procedure, it is called and its result is returned instead.
(define (terms-ref contents [failure-result (lambda () (error 'terms-ref "no term for ~a" contents))])
(hash-ref (term-cache) contents failure-result))

; Returns a list of all terms in the current term cache, in an unspecified order.
(define (terms)
(hash-values (term-cache)))

; Returns the size of the current term cache.
(define (terms-count)
(hash-count (term-cache)))

; Evaluates expr with (terms) set to terms-expr, returns the result, and
; restores (terms) to its old value. If terms-expr is not given, it defaults to
; (terms), so (with-terms expr) is equivalent to (with-terms (terms) expr).
(define-syntax (with-terms stx)
(syntax-parse stx
[(_ expr)
#'(parameterize ([term-cache (hash-copy (term-cache))])
expr)]
[(_ terms-expr expr)
#'(parameterize ([term-cache (hash-copy-clear (term-cache))])
(let ([ts terms-expr]
[cache (term-cache)])
(for ([t ts])
(hash-set! cache (term-val t) t))
expr))]))




#|-----------------------------------------------------------------------------------|#
Expand Down
2 changes: 1 addition & 1 deletion rosette/guide/scribble/essentials/bvmid.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@
(demo (bvsqrt (int32 4)))
(demo (bvsqrt (int32 15)))
(demo (bvsqrt (int32 16)))
(demo (parameterize ([term-cache (hash-copy (term-cache))])
(demo (with-terms
(with-deep-time-limit 10 (bvsqrt l)))))

(define-demo sound-finitization-demo
Expand Down
97 changes: 74 additions & 23 deletions rosette/guide/scribble/reflection/state-log.txt
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,4 @@
;; This file was created by make-log-based-eval
((require (only-in racket hash-values))
((3) 0 () 0 () () (c values c (void)))
#""
#"")
((require (only-in rosette/guide/scribble/util/lifted opaque))
((3) 0 () 0 () () (c values c (void)))
#""
Expand All @@ -11,7 +7,7 @@
((3) 0 () 0 () () (c values c (void)))
#""
#"")
((hash-values (term-cache))
((terms)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
Expand All @@ -20,7 +16,7 @@
0
()
()
(c values c (0 (u . "(list d b c a)"))))
(c values c (0 (u . "(list a d b c)"))))
#""
#"")
((assume a) ((3) 0 () 0 () () (c values c (void))) #"" #"")
Expand Down Expand Up @@ -76,7 +72,7 @@
"(vc a (&& (|| (! b) (|| c (! (&& a b)))) (|| b (|| d (! (&& a (! b)))))))"))))
#""
#"")
((append (take (hash-values (term-cache)) 5) (list (opaque "...")))
((append (take (terms) 5) (list (opaque "...")))
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
Expand All @@ -91,7 +87,7 @@
(0
(u
.
"(list\n (&& (|| (! b) (|| c (! (&& a b)))) (|| b (|| d (! (&& a (! b))))))\n b\n (&& a b)\n (&& a (! b))\n (! b)\n ...)\n"))))
"(list\n (|| d (! (&& a (! b))))\n (&& (|| (! b) (|| c (! (&& a b)))) (|| b (|| d (! (&& a (! b))))))\n (! d)\n (|| (! b) (|| c (! (&& a b))))\n (! a)\n ...)\n"))))
#""
#"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
Expand Down Expand Up @@ -246,7 +242,7 @@
#"")
((clear-terms!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((hash-values (term-cache))
((terms)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
Expand Down Expand Up @@ -275,7 +271,7 @@
(c values c (0 (u . "(+ 3 a)"))))
#""
#"")
((hash-values (term-cache))
((terms)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
Expand Down Expand Up @@ -303,7 +299,7 @@
(c values c (0 (u . "(unsat)"))))
#""
#"")
((hash-values (term-cache))
((terms)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
Expand All @@ -316,7 +312,7 @@
#""
#"")
((clear-terms!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((hash-values (term-cache))
((terms)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
Expand All @@ -340,7 +336,7 @@
(c values c (0 (u . "(model\n [a 1]\n [a 0])"))))
#""
#"")
((hash-values (term-cache))
((terms)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
Expand All @@ -349,11 +345,11 @@
0
()
()
(c values c (0 (u . "(list (= a a) a (! (= a a)))"))))
(c values c (0 (u . "(list (! (= a a)) (= a a) a)"))))
#""
#"")
((clear-terms!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((require (only-in racket collect-garbage hash-count))
((require (only-in racket collect-garbage))
((3) 0 () 0 () () (c values c (void)))
#""
#"")
Expand All @@ -364,22 +360,77 @@
((3) 0 () 0 () () (c values c (void)))
#""
#"")
((hash-count (term-cache)) ((3) 0 () 0 () () (q values 0)) #"" #"")
((length (terms)) ((3) 0 () 0 () () (q values 0)) #"" #"")
((time (unused-terms! 50000))
((3) 0 () 0 () () (c values c (void)))
#"cpu time: 245 real time: 246 gc time: 11\n"
#"cpu time: 240 real time: 240 gc time: 20\n"
#"")
((hash-count (term-cache)) ((3) 0 () 0 () () (q values 50000)) #"" #"")
((length (terms)) ((3) 0 () 0 () () (q values 50000)) #"" #"")
((collect-garbage) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((hash-count (term-cache)) ((3) 0 () 0 () () (q values 50000)) #"" #"")
((length (terms)) ((3) 0 () 0 () () (q values 50000)) #"" #"")
((clear-terms!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((collect-garbage) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((term-cache (weak-term-cache)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((hash-count (term-cache)) ((3) 0 () 0 () () (q values 0)) #"" #"")
((gc-terms!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((length (terms)) ((3) 0 () 0 () () (q values 0)) #"" #"")
((time (unused-terms! 50000))
((3) 0 () 0 () () (c values c (void)))
#"cpu time: 329 real time: 330 gc time: 29\n"
#"cpu time: 321 real time: 321 gc time: 27\n"
#"")
(50000 ((3) 0 () 0 () () (q values 50000)) #"" #"")
((collect-garbage) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((hash-count (term-cache)) ((3) 0 () 0 () () (q values 0)) #"" #"")
((length (terms)) ((3) 0 () 0 () () (q values 0)) #"" #"")
((define-symbolic a b integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((terms)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
()
()
(c values c (0 (u . "(list b a)"))))
#""
#"")
((with-terms (begin0 (verify (assert (= (+ a b) 0))) (println (terms))))
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
()
()
(c values c (0 (u . "(model\n [a 1]\n [b 0])"))))
#"(list (= 0 (+ a b)) b (! (= 0 (+ a b))) a (+ a b))\n"
#"")
((terms)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
()
()
(c values c (0 (u . "(list b a)"))))
#""
#"")
((with-terms
(list)
(begin (println (terms)) (define-symbolic c integer?) (println (terms))))
((3) 0 () 0 () () (c values c (void)))
#"'()\n(list c)\n"
#"")
((terms)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
()
()
(c values c (0 (u . "(list b a)"))))
#""
#"")
Loading

0 comments on commit 490c4fe

Please sign in to comment.