7.2 Reflecting on Symbolic State
Like standard program execution, Rosette’s symbolic evaluation can be viewed as a function that operates on program states. The state of a Rosette program includes its Racket state (memory, environment, and so on) and its symbolic state. The key parts of the symbolic state are the current verification condition (VC) and the current symbolic heap. The heap consists of all the symbolic terms created so far. The verification condition tracks all the assumptions and assertions issued on any path between the starting program state and the current state. Unlike concrete execution, which evaluates just one path through a program, Rosette evaluates all possible paths when the decision on which path to take depends on a symbolic value. The symbolic heap and the verification condition reflect the current state of this all-path evaluation.
(define-symbolic a b c d boolean?) (terms) ; Symbolic heap. (list a c d b)
(assume a) (vc) ; Verification condition. (vc a #t)
(if b (begin (printf "Then branch:\n ~a\n" (vc)) (assert c) (printf " ~a\n" (vc)) 1) (begin (printf "Else branch:\n ~a\n" (vc)) (assert d) (printf " ~a\n" (vc)) 2))
Then branch:
#(struct:vc (&& a b) #t)
#(struct:vc (&& a b) (|| c (! (&& a b))))
Else branch:
#(struct:vc (&& a (! b)) #t)
#(struct:vc (&& a (! b)) (|| d (! (&& a (! b)))))
(ite b 1 2)
(vc) (vc a (&& (|| (! b) (|| c (! (&& a b)))) (|| b (|| d (! (&& a (! b)))))))
(terms)
(list
a
c
d
b
(&& (|| (! b) (|| c (! (&& a b)))) (|| b (|| d (! (&& a (! b))))))
...)
This section describes the built-in facilities for accessing and modifying various aspects of the symbolic state from within a Rosette program. These facilites are useful for low-level debugging and optimizations of Rosette-based tools. But they also make it possible to violate the state invariants maintained by Rosette, so it is best to use them sparingly.
7.2.1 Verification Conditions
procedure
v : any/c
procedure
(vc-assumes v) → boolean?
v : vc?
procedure
(vc-asserts v) → boolean?
v : vc?
> vc-true (vc #t #t)
> (vc? vc-true) #t
> (vc-assumes vc-true) #t
> (vc-asserts vc-true) #t
> (vc-true? vc-true) #t
> (vc-true? 1) #f
The current (vc) state can be cleared using clear-vc!. This resets (vc) to its starting value, vc-true.
> (vc) (vc #t #t)
> (define-symbolic a b boolean?) > (vc) (vc #t #t)
> (assume a) > (vc) (vc a #t)
> (assert b) > (vc) (vc a (|| b (! a)))
> (clear-vc!) > (vc) (vc #t #t)
The result of a with-vc expression is a value of type result?. If expr terminates normally, then the result is normal?, and its result-value contains the value computed by expr. If expr fails, the result is failed?, and its result-value contains an exn:fail? exception that represents the cause of the abnormal termination. In either case, result-state holds the final verification condition generated during the evaluation of expr, starting with vc-expr, or (vc), as the initial verification condition.
In the context of symbolic evaluation, expr
terminates normally if it has at least one path of execution
that terminates normally. A path terminates normally if it
is free of any assumption or assertion violations—
> (define-symbolic a b boolean?) > (assume a) > (vc) (vc a #t)
; Normal termination, starting with (vc). ; The error along the path where b is true ; is treated as an assertion violation.
> (with-vc (begin (when b (error 'b "No b allowed!")) 1)) (normal 1 (vc a (|| (! b) (! (&& a b)))))
> (vc) ; (vc) is unchanged. (vc a #t)
; Abnormal termination, starting with vc-true.
> (with-vc vc-true (if b (assume #f) (assert #f)))
(failed
(exn:fail:svm:merge "[merge] failed" #<continuation-mark-set>)
(vc (! b) b))
> (vc) ; (vc) is unchanged. (vc a #t)
procedure
v : any/c
procedure
(result-value v) → any/c
v : result?
procedure
(result-state v) → any/c
v : result?
procedure
v : any/c
procedure
v : any/c
See also with-vc.
7.2.2 Symbolic Heap
The symbolic heap is not garbage collected, which means that long running applications may experience memory pressure. There are two ways to solve this issue, depending on the application’s behavior.
If the application is performing many independent queries that do not share any symbolic constants, then the application may safely clear the heap between query invocations using clear-terms!. This is the most common scenario.
If the application is solving a series of related queries, using clear-terms! can lead to incorrect behavior. In this scenario, the safe solution is to use a garbage-collected heap by invoking (gc-terms!). This has the effect of changing the internal representation of the heap to use a more expensive data structure that cooperates with Racket’s garbage collector. Because of the added runtime overhead, this setting is best saved for when the default heap consumes too much memory.
> (terms) '()
> (define (get-a) (define-symbolic a integer?) a) > (define a0 (get-a)) > (+ a0 3) (+ 3 a)
> (terms) (list a (+ 3 a))
; In the following scenario, using clear-terms! leads to ; incorrect behavior: (query-a a0) should always return ; unsat? according to the semantics of define-symbolic. ; But if the heap is cleared, it returns sat? because a0 ; is bound to a constant that no longer exists in the heap.
> (define (query-a a) (verify (assert (= a (get-a))))) > (query-a a0) (unsat)
> (terms) (list a (+ 3 a))
> (clear-terms!) > (terms) '()
> (query-a a0) ; Wrong result.
(model
[a 1]
[a 0])
> (terms) (list a (! (= a a)) (= a a))
procedure
(clear-terms! [ts]) → void?
ts : (or/c #f (listof term?)) = #f
; Creates n unreachable terms of the form (+ a (+ a ...)).
> (define (unused-terms! n) (define-symbolic* a integer?) (let loop ([n n]) (if (<= n 1) a (+ a (loop (- n 1))))) (void)) > (length (terms)) ; Empty heap. 0
> (time (unused-terms! 50000)) cpu time: 357 real time: 365 gc time: 17
> (length (terms)) 50000
> (collect-garbage) > (length (terms)) ; GC has no effect on the default heap. 50000
> (clear-terms!) > (collect-garbage) > (gc-terms!) ; Use gc-terms! to change the representation. > (length (terms)) 0
> (time (unused-terms! 50000)) cpu time: 410 real time: 416 gc time: 40
> (length (terms)) 50000
> (collect-garbage) > (length (terms)) ; The heap now cooperates with GC. 0
syntax
(with-terms expr)
(with-terms terms-expr expr)
terms-expr : (listof term?)
The result of a with-terms expression is the output of expr.
Note that none of the terms created during the evaluation of expr are preserved in the heap, and having those terms escape the dynamic extent of expr is usually a sign of a programming error. It can lead to incorrect behavior, similarly to using clear-terms!.
> (define-symbolic a b integer?) > (terms) (list b a)
> (with-terms (begin0 (verify (assert (= (+ a b) 0))) (println (terms)))) (list (+ a b) b a (! (= 0 (+ a b))) (= 0 (+ a b)))
(model
[a 1]
[b 0])
> (terms) (list b a)
> (with-terms (list) (begin (println (terms)) (define-symbolic c integer?) (println (terms))))
'()
(list c)
> (terms) (list b a)