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 .
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:
|> (define y (vector 0 1 2))|
|> (define-symbolic b boolean?)|
|; If b is true, then y should be 3, otherwise y should be 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)|
'#(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.
|; 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)|
|; The following call produces an incorrect state. Intuitively, we expect h|
|; to be empty if b is true and unchanged otherwise.|
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
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.
The two uses of hash-ref
in our buggy example violate the third and first
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.