8 Unsafe Operations
Throughout this guide, we have assumed that Rosette programs are written in the rosette/safe dialect of the full language. This dialect extends a core subset of Racket with solver-aided functionality. In this chapter, we briefly discuss the rosette dialect of the language, which exports all of Racket.
Safe use of the full rosette language requires a basic understanding of how Rosette’s Symbolic Virtual Machine (SVM) works [3]. Briefly, the SVM hijacks the normal Racket execution for all procedures and constructs that are exported by rosette/safe. Any programs that are implemented exclusively in the rosette/safe language are therefore fully under the SVM’s control. This means that the SVM can correctly interpret the application of a procedure or a macro to a symbolic value, and it can correctly handle any side-effects (in particular, writes to memory) performed by rosette/safe code.
> (define y (vector 0 1 2)) > (define-symbolic b boolean?) ; If b is true, then y[1] should be 3, otherwise y[2] should be 4:
> (if b (vector-set! y 1 3) (vector-set! y 2 4)) ; The state of y correctly accounts for both possibilities: ; * If the solver finds that b must be #t, then the contents ; of y will be #(0 3 2). ; * Otherwise, the contents of y will be #(0 1 4) > y '#(0 (ite b 3 1) (ite b 2 4))
> (define env1 (solve (assert b))) > (evaluate y env1) '#(0 3 2)
> (define env2 (solve (assert (not b)))) > (evaluate y env2) '#(0 1 4)
Because the SVM controls only the execution of rosette/safe code, it cannot, in general, guarantee the safety or correctness of arbitrary rosette programs. As soon as a rosette program calls an unlifted Racket construct (that is, a procedure or a macro not implemented in or provided by the rosette/safe language), the execution escapes back to the Racket interpreter. The SVM has no control over the side-effects performed by the Racket interpreter, or the meaning that it (perhaps incorrectly) assigns to programs in the presence of symbolic values. As a result, the programmer is responsible for ensuring that a rosette program continues to behave correctly after the execution returns from the Racket interpreter.
As an example of incorrect behavior, consider the following rosette snippet. The procedures make-hash, hash-ref, and hash-clear! are not in rosette/safe. Whenever they are invoked, the execution escapes to the Racket interpreter.
(define h (make-hash '((1 . 2)))) (define-symbolic key integer?) (define-symbolic b boolean?)
; The following call produces an incorrect value. Intuitively, we expect the ; output to be the symbolic number that is either 2 or 0, depending on whether ; the key is 1 or something else. > (hash-ref h key 0) 0
; The following call produces an incorrect state. Intuitively, we expect h ; to be empty if b is true and unchanged otherwise.
> (when b (hash-clear! h)) > h '#hash()
the current path condition is #t;
the assertion store is empty; and,
all local and global variables that may be read by c contain fully concrete values. A value (e.g., a list) is fully concrete if no symbolic values can be reached by recursively traversing its structure.
Being conservative, the above rule disallows many scenarios in which it is still safe to use Racket constructs. These, however, have to be considered on a case-by-case basis. For example, it is safe to use Racket’s iteration and comprehension constructs, such as for or for/list, as long as they iterate over concrete sequences, and all guard expressions produce fully concrete values in each iteration. In practice, Rosette programs can safely use many common Racket constructs, and with a bit of experience, it becomes easy to see when it is okay to break the effectively-concrete rule.