Skip to content

Commit

Permalink
Add symbolic profiling to Rosette.
Browse files Browse the repository at this point in the history
  • Loading branch information
jamesbornholt committed Aug 23, 2018
1 parent eb5a390 commit e4b56fa
Show file tree
Hide file tree
Showing 71 changed files with 7,466 additions and 35 deletions.
2 changes: 1 addition & 1 deletion .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ before_install:


install:
- raco pkg install
- raco pkg install --auto

script:
- time raco make test/all-rosette-tests.rkt
Expand Down
2 changes: 2 additions & 0 deletions NOTES.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,11 @@ The semantics of Rosette 3.0 differs from Rosette 2.x in two ways:

This release also includes the following new functionality and features contributed by [James Bornholt][] and [Phitchaya Mangpo Phothilimthana][]:

- Developed a new *symbolic profiler* for diagnosing performance issues in Rosette programs. The symbolic profiler instruments Rosette and tracks key performance metrics to identify potential issues. To use the symbolic profiler, run the command `raco symprofile program.rkt`. A new [performance][] chapter in the Rosette guide details common performance issues and how to use the symbolic profiler to identify them.
- Extended and generalized the interface to constraint solvers. The new interface allows the client code to specify a path to the solver, set the logic, provide solver-specific configuration options, and export the problem encodings sent to the solver.
- Added support for four new solvers: [Boolector][], [CVC4][], [Yices][], and [CPLEX][]. These solvers are not included in the default distribution and need to be installed separately for use with Rosette.

[performance]: https://docs.racket-lang.org/rosette-guide/ch_performance.html
[Boolector]: https://docs.racket-lang.org/rosette-guide/sec_solvers-and-solutions.html#%28def._%28%28lib._rosette%2Fsolver%2Fsmt%2Fboolector..rkt%29._boolector%29%29
[CVC4]: https://docs.racket-lang.org/rosette-guide/sec_solvers-and-solutions.html#%28def._%28%28lib._rosette%2Fsolver%2Fsmt%2Fcvc4..rkt%29._cvc4%29%29
[Yices]: https://docs.racket-lang.org/rosette-guide/sec_solvers-and-solutions.html#%28def._%28%28lib._rosette%2Fsolver%2Fsmt%2Fyices..rkt%29._yices%29%29
Expand Down
3 changes: 2 additions & 1 deletion info.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -3,13 +3,14 @@
(define collection 'multi)

(define deps '("r6rs-lib"
"rfc6455"
"rackunit-lib"
"slideshow-lib"
"base"))

(define build-deps '("pict-doc"
"scribble-lib"
"racket-doc"))
"racket-doc"))

(define test-omit-paths (if (getenv "PLT_PKG_BUILD_SERVICE") 'all '()))

Expand Down
4 changes: 2 additions & 2 deletions rosette/base/core/lift.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -52,12 +52,12 @@
(define-syntax (define/lift stx)
(syntax-case stx (: :: ->)
[(_ (id0 id ...) :: contracted? -> rosette-type?)
(or (identifier? #'contracted) (raise-argument-error "identifier?" #'contracted?))
(or (identifier? #'contracted?) (raise-argument-error "identifier?" #'contracted?))
#'(begin
(define/lift id0 :: contracted? -> rosette-type?)
(define/lift id :: contracted? -> rosette-type?) ...)]
[(_ id :: contracted? -> rosette-type?) ; repeated from (_ id : contracted? -> rosette-type?) - params don't work
(or (identifier? #'contracted) (raise-argument-error "identifier?" #'contracted?))
(or (identifier? #'contracted?) (raise-argument-error "identifier?" #'contracted?))
#`(define (#,(lift-id #'id) val)
(if (contracted? val)
(id val)
Expand Down
12 changes: 7 additions & 5 deletions rosette/base/core/merge.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

(require (only-in rnrs/base-6 assert)
(only-in racket/unsafe/ops [unsafe-car car] [unsafe-cdr cdr])
"term.rkt" "union.rkt" "bool.rkt")
"term.rkt" "union.rkt" "bool.rkt" "reporter.rkt")

(provide merge merge* unsafe-merge* merge-same)

Expand Down Expand Up @@ -32,10 +32,12 @@
(do-merge* #t ps))

(define-syntax-rule (do-merge* force? ps)
(match (compress force? (simplify ps))
[(list (cons g v)) (assert (not (false? g))) v]
[(list _ (... ...) (cons #t v) _ (... ...)) v]
[vs (apply union vs)]))
(let ([simp (simplify ps)])
((current-reporter) 'merge (length simp))
(match (compress force? simp)
[(list (cons g v)) (assert (not (false? g))) v]
[(list _ (... ...) (cons #t v) _ (... ...)) v]
[vs (apply union vs)])))

(define (guard-&& a b)
(match b
Expand Down
15 changes: 15 additions & 0 deletions rosette/base/core/reporter.rkt
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
#lang racket

(require racket/generic (for-syntax racket/syntax))
(provide (all-defined-out))

; The reporter is called when "interesting"
; events happen during symbolic execution; for example,
; when a merge occurs or a new term is created.
(define current-reporter
(make-parameter
void
(lambda (new-reporter)
(unless (procedure? new-reporter)
(raise-argument-error 'current-reporder "procedure?" new-reporter))
new-reporter)))
8 changes: 5 additions & 3 deletions rosette/base/core/term.rkt
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
#lang racket

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

(provide
term-cache clear-terms!
Expand All @@ -18,7 +19,7 @@
; of expressions with commutative operators.
#|-----------------------------------------------------------------------------------|#
(define term-cache (make-parameter (make-hash)))
(define term-count (make-parameter 0))
(define term-count (make-parameter 0))

; Clears the entire term-cache if invoked with #f (default), or
; it clears all terms reachable from the given set of leaf terms.
Expand Down Expand Up @@ -67,11 +68,12 @@
(define (term<? s1 s2) (< (term-ord s1) (term-ord s2)))

(define-syntax-rule (make-term term-constructor args type rest ...)
(let ([val args])
(let ([val args])
(or (hash-ref (term-cache) val #f)
(let* ([ord (term-count)]
[out (term-constructor val type ord rest ...)])
(term-count (add1 ord))
((current-reporter) 'new-term out)
(hash-set! (term-cache) val out)
out))))

Expand Down
11 changes: 3 additions & 8 deletions rosette/base/core/union.rkt
Original file line number Diff line number Diff line change
@@ -1,11 +1,10 @@
#lang racket

(require "term.rkt")
(require "term.rkt" "reporter.rkt")

(provide union? (rename-out [a-union union])
union-contents union-type union-guards union-values union-filter
in-union in-union* in-union-guards in-union-values
union-count union-sum)
in-union in-union* in-union-guards in-union-values)

; Represents a symbolic union of guarded values that evaluates either to a
; single value of a given type, or no value at all.
Expand Down Expand Up @@ -51,12 +50,8 @@
#:transparent
#:property prop:procedure [struct-field-index procedure])

(define union-count (make-parameter 0))
(define union-sum (make-parameter 0))

(define (make-union . vs)
(union-count (add1 (union-count)))
(union-sum (+ (length vs) (union-sum)))
((current-reporter) 'new-union (length vs))
(match vs
[(list) nil]
[_
Expand Down
Loading

0 comments on commit e4b56fa

Please sign in to comment.