6.9

#### 7.1Reflecting 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.1Symbolic 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(term? v) → boolean? v : any/c
 procedure v : any/c
 procedure v : any/c
Predicates for recognizing symbolic terms, expressions, and constants, respectively.

Examples:
 > (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)
Pattern matching forms for symbolic terms, expressions, and constants, respectively.

Examples:
> (define-symbolic x integer?) ; constant
> (define e (+ x 1)) ; expression
 > (match x [(constant identifier type) (list identifier type)])

'(#<syntax:8:0 x> integer?)

 > (match x [(term content type) (list content type)])

'(#<syntax: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?)

 procedure(symbolics v) → (listof constant?) v : any/c
Returns all symbolic constants that are transitively contained in the given value.

Examples:
 > (define-symbolic x y z integer?) > (symbolics x) '(x) > (symbolics (if (= x y) 2 #f)) '(x y) > (symbolics (list y z y)) '(y z) > (struct cell (value) #:transparent) > (symbolics (list 5 (cons (box y) z) (vector (cell x) z))) '(y z x)

 procedure(type-of v ...+) → type? v : any/c
Returns the most specific type? predicate that accepts all of the given values.

Examples:
 > (define-symbolic x integer?) > (type-of x) integer? > (type-of (+ x 1)) integer? > (type-of x 3.14) real? > (type-of #t) boolean? > (type-of #t 1) any/c

 procedure(type? v) → boolean? v : any/c
Returns true when given a predicate that recognizes a built-in or a structure type. Otherwise returns false.

Examples:
 > (type? integer?) #t > (type? boolean?) #t > (type? list?) #t > (struct circle (radius)) > (type? circle?) #t > (type? any/c) #t > (type? 1) #f

 procedure v : any/c
Returns true if v is a type predicate for a solvable type.

Examples:
 > (solvable? boolean?) #t > (solvable? integer?) #t > (solvable? real?) #t > (solvable? (~> (bitvector 3) (bitvector 4))) #t > (solvable? list?) #f > (struct circle (radius)) > (solvable? circle?) #f > (solvable? any/c) #f

##### 7.1.2Symbolic Unions

Rosette represents symbolic values of an unsolvable type (e.g., list?) as symbolic unions. A symbolic union is a set of two or more guarded values. A guarded value, in turn, combines a guard, which is a symbolic boolean? term, and a (non-union) value. Rosette’s symbolic evaluator guarantees that the guards in a symbolic union are disjoint: only one of them can ever be true. For example, the symbolic vector s defined below is represented as a symbolic union of two guarded vectors:
 > (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)

The values that appear in a union are themselves never unions. They may, however, contain unions. They may also belong to several different types. In that case, the type of the union is the most specific type? predicate that accepts all members of the union. This will always be an unsolvable type—possibly any/c, the most general unsolvable type.
 > (define-symbolic b boolean?) > (define-symbolic c boolean?) > (define v (if c "c" 0)) > (define u (if b (vector v) 4)) > u {[b #({-4400030153516522962: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.

 procedure(union? v) → boolean? v : any/c
Returns true if the given value is a symbolic union. Otherwise returns false.

Examples:
 > (define-symbolic b boolean?) > (define u (if b '(1 2) 3)) > (union? u) #t > (union? b) #f

 procedure → (listof (cons/c (and/c boolean? term?) (not/c union?))) u : union?
Returns a list of guard-value pairs contained in the given union.

Examples:
 > (define-symbolic b boolean?) > (define v (if b '(1 2) 3)) > (union-contents v) '((b 1 2) ((! b) . 3))

##### 7.1.3Symbolic 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 value that is not a union?, for/all behaves like a let expression. It binds id to the value and evaluates the body with that binding.

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 pureit may not perform any observable side-effects, such as writes to memory or disk. There is no purity requirement for using procedures that are implemented in or exported by rosette/safe (e.g., vector-set!).

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: 2 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)
Expands to a nested use of for/all, just like let* expands to a nested use of let.

 (require rosette/lib/lift) package: rosette

 syntax(define-lift id [(arg-type ...) racket-procedure-id]) (define-lift id [arg-type racket-procedure-id])
Binds id to a procedure that lifts racket-procedure-id to work on symbolic unions. In particular, the lifted procedure will work when given either a concrete Racket value or a symbolic union contains a guarded value of a suitable type, as given by arg-type. Note that the lifted procedure will not work on symbolic terms, only on symbolic unions or concrete values. The Racket procedure bound to racket-procedure-id must be pure (see for/all).

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)