7.1 Reflecting on Symbolic Values
There are two kinds of symbolic values in Rosette: symbolic terms and symbolic unions. A Rosette program can inspect the representation of both kinds of values. This is useful for lifting additional (unlifted) Racket procedures to work on symbolic values, and for controlling the performance of Rosette’s symbolic evaluator.
7.1.1 Symbolic Terms
A symbolic term is either a symbolic constant, created via define-symbolic[*], or a symbolic expression, produced by a lifted operator. Terms are strongly typed, and always belong to a solvable type. Symbolic values of all other (unsolvable) types take the form of symbolic unions.
procedure
v : any/c
procedure
(expression? v) → boolean?
v : any/c
procedure
v : any/c
> (define-symbolic x integer?) ; constant > (define e (+ x 1)) ; expression > (list (term? x) (term? e)) '(#t #t)
> (list (constant? x) (constant? e)) '(#t #f)
> (list (expression? x) (expression? e)) '(#f #t)
> (term? 1) #f
syntax
(term content type)
syntax
(expression op child ...+)
syntax
(constant id type)
> (define-symbolic x integer?) ; constant > (define e (+ x 1)) ; expression
> (match x [(constant identifier type) (list identifier type)]) '(#<syntax:eval:8:0 x> integer?)
> (match x [(term content type) (list content type)]) '(#<syntax:eval:8:0 x> integer?)
> (match e [(expression op child ...) (cons op child)]) '(+ 1 x)
> (match e [(term content type) (list content type)]) '((+ 1 x) integer?)
7.1.2 Symbolic Unions
> (define-symbolic b boolean?) > (define v (vector 1)) > (define w (vector 2 3)) > (define s (if b v w)) > s {[b #(1)] [(! b) #(2 3)]}
> (type-of s) vector?
> (eq? s v) b
> (eq? s w) (! b)
> (define-symbolic b boolean?) > (define-symbolic c boolean?) > (define v (if c "c" 0)) > (define u (if b (vector v) 4)) > u {[b #({3675081740876851646:2})] [(! b) 4]}
> (type-of u) any/c
Symbolic unions are recognized by the union? predicate, and Rosette programs can inspect union contents using the union-contents procedure. Applications may use union? and union-contents directly to lift Racket code to work on symbolic unions, but Rosette also provides dedicated lifting constructs, described in the next section, to make this process easier and the resulting lifted code more efficient.
> (define-symbolic b boolean?) > (define v (if b '(1 2) 3)) > (union-contents v) '((b 1 2) ((! b) . 3))
7.1.3 Symbolic Lifting
Rosette provides two main constructs for lifting Racket code to work on symbolic unions: for/all and define-lift. The for/all construct is built into the language. It is used internally by Rosette to lift operations on unsolvable types. The define-lift construct is syntactic sugar implemented on top of for/all; it is exported by the rosette/lib/lift library.
syntax
(for/all ([id val-expr]) body ...+)
If val-expr evaluates to a symbolic union, then for each
guard-value pair '(g . v) in that union, for/all
binds id to v and evaluates the body
under the guard g. The results of the individual evaluations of
the body are re-assembled into a single (concrete or symbolic)
output value, which is the result of the for/all expression.
If the evaluation of body executes any procedure p that is neither
implemented in nor provided by the rosette/safe language, then p
must be pure—
The for/all construct is useful both for lifting pure Racket procedures to work on symbolic unions and for controling the performance of Rosette’s symbolic evaluation. The following examples show both use cases:
Lifting a pure Racket procedure to work on symbolic unions.
(require (only-in racket [string-length racket/string-length])) (define (string-length value) (for/all ([str value]) (racket/string-length str))) > (string-length "abababa") 7
> (string-length 3) string-length: contract violation
expected: string?
given: 3
> (define-symbolic b boolean?) > (string-length (if b "a" "abababa")) (ite b 1 7)
> (string-length (if b "a" 3)) 1
> (asserts) '(b)
> (string-length (if b 3 #f)) for/all: all paths infeasible
- Making symbolic evaluation more efficient.
(require (only-in racket build-list)) (define limit 1000) (define (slow xs) (and (= (length xs) limit) (car (map add1 xs)))) (define (fast xs) (for/all ([xs xs]) (slow xs))) (define ys (build-list limit identity)) (define-symbolic a boolean?) (define xs (if a ys (cdr ys))) > (time (slow xs)) cpu time: 1 real time: 1 gc time: 0
{[a 1] [(! a) #f]}
> (time (fast xs)) cpu time: 0 real time: 0 gc time: 0
{[a 1] [(! a) #f]}
Note that the above transformation will not always lead to better performance. Experimenting is the best way to determine whether and where to insert performance-guiding for/alls.
syntax
(for*/all ([id val-expr] ...+) body ...+)
| (require rosette/lib/lift) | package: rosette |
syntax
(define-lift id [(arg-type ...) racket-procedure-id])
(define-lift id [arg-type racket-procedure-id])
When racket-procedure-id takes a specific number of arguments, the first form should be used, and the type of each argument should be given. When racket-procedure-id takes a variable number of arguments, the type of all arguments should be given. Note that the second form omits the parentheses around the argument type to indicate a variable number of arguments, just like Racket’s case-lambda form.
The following example shows how to lift Racket’s string-length procedure to work on symbolic unions that contain strings.
(require rosette/lib/lift) (require (only-in racket [string-length racket/string-length] string?)) (define-lift string-length [(string?) racket/string-length])
> (string-length "abababa") 7
> (define-symbolic b boolean?) > (string-length (if b "a" "abababa")) (ite b 1 7)
> (string-length (if b "a" 3)) 1
> (asserts) '(b)