8.12

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  [2, 4]. 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.

The following snippet demonstrates the non-standard execution that the SVM needs to perform in order to assign the expected meaning to Rosette code:

Examples:
> (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

(vector 0 (ite b 3 1) (ite b 2 4))

> (define sol1 (solve (assert b)))
> (evaluate y sol1)

'#(0 3 2)

> (define sol2 (solve (assert (not b))))
> (evaluate y sol2)

'#(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.

Examples:
> (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
    (pretty-print (vc))
    (hash-clear! h))

(vc b #t)

> h

'#hash()

When is it safe to use a Racket procedure or macro? The answer depends on their semantics. A conservative rule is to only use an unlifted construct c in an effectively concrete program state. The SVM is in such a state when
  1. the current verification condition is true, i.e., (vc-true? (vc)); and,

  2. 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.

The above uses of hash-ref and hash-clear! violate these requirements: hash-ref is reading a symbolic value, and hash-clear! is evaluated in a state with a symbolic verification condition.

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.