Skip to content

Commit

Permalink
Revise the guide: Unsafe Operations.
Browse files Browse the repository at this point in the history
  • Loading branch information
emina committed Feb 17, 2021
1 parent c185cf7 commit 532aa8e
Show file tree
Hide file tree
Showing 3 changed files with 63 additions and 25 deletions.
2 changes: 1 addition & 1 deletion rosette/guide/scribble/rosette-guide.scrbl
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ Chapters @seclink["ch:syntactic-forms"]{3}-@seclink["ch:libraries"]{6} define th
@include-section["datatypes/defined-datatypes.scrbl"]
@include-section["libs/libraries.scrbl"]
@include-section["reflection/symbolic-reflection.scrbl"]
@;include-section["unsafe/unsafe.scrbl"]
@include-section["unsafe/unsafe.scrbl"]
@;include-section["performance/performance.scrbl"]
@;include-section["error-tracing/error-tracing.scrbl"]

Expand Down
50 changes: 43 additions & 7 deletions rosette/guide/scribble/unsafe/unsafe-log.txt
Original file line number Diff line number Diff line change
Expand Up @@ -14,19 +14,41 @@
0
()
()
(c values c (v! 0 (0 (u . "(ite b 3 1)")) (0 (u . "(ite b 2 4)")))))
(c values c (0 (u . "(vector 0 (ite b 3 1) (ite b 2 4))"))))
#""
#"")
((define env1 (solve (assert b)))
((define sol1 (solve (assert b)))
((3) 0 () 0 () () (c values c (void)))
#""
#"")
((evaluate y env1) ((3) 0 () 0 () () (c values c (v! 0 3 2))) #"" #"")
((define env2 (solve (assert (not b))))
((evaluate y sol1)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
()
()
(c values c (0 (u . "'#(0 3 2)"))))
#""
#"")
((define sol2 (solve (assert (not b))))
((3) 0 () 0 () () (c values c (void)))
#""
#"")
((evaluate y env2) ((3) 0 () 0 () () (c values c (v! 0 1 4))) #"" #"")
((evaluate y sol2)
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
()
()
(c values c (0 (u . "'#(0 1 4)"))))
#""
#"")
((require (only-in racket make-hash hash-clear! hash-ref))
((3) 0 () 0 () () (c values c (void)))
#""
Expand All @@ -38,5 +60,19 @@
((define-symbolic key integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((hash-ref h key 0) ((3) 0 () 0 () () (q values 0)) #"" #"")
((when b (hash-clear! h)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
(h ((3) 0 () 0 () () (c values c (h ! (equal)))) #"" #"")
((when b (pretty-print (vc)) (hash-clear! h))
((3) 0 () 0 () () (c values c (void)))
#"(vc b #t)\n"
#"")
(h
((3)
1
(((lib "rosette/guide/scribble/util/lifted.rkt")
.
deserialize-info:opaque-v0))
0
()
()
(c values c (0 (u . "'#hash()"))))
#""
#"")
36 changes: 19 additions & 17 deletions rosette/guide/scribble/unsafe/unsafe.scrbl
Original file line number Diff line number Diff line change
@@ -1,10 +1,9 @@
#lang scribble/manual

@(require (for-label racket) scribble/core scribble/eval)
@(require (for-label racket) scribble/core scribble/example)
@(require (for-label rosette/base/form/define rosette/query/query rosette/solver/solution
rosette/base/core/term
(only-in rosette/base/core/safe assert) )
racket/runtime-path)
(only-in rosette/base/base assert vc-true? vc) )
racket/runtime-path racket/sandbox)
@(require (only-in "../refs.scrbl" ~cite rosette:pldi14))
@(require "../util/lifted.rkt")

Expand All @@ -31,7 +30,7 @@ by @racket[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:
@interaction[#:eval rosette-eval
@examples[#:eval rosette-eval
(define y (vector 0 1 2))

(define-symbolic b boolean?)
Expand All @@ -48,11 +47,11 @@ perform in order to assign the expected meaning to Rosette code:

y

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

(define env2 (solve (assert (not b))))
(evaluate y env2)]
(define sol2 (solve (assert (not b))))
(evaluate y sol2)]

Because the SVM controls only the execution of @racket[rosette/safe] code,
it cannot, in general, guarantee the safety or correctness of arbitrary @racket[rosette] programs.
Expand All @@ -68,11 +67,11 @@ The procedures @racket[make-hash], @racket[hash-ref], and @racket[hash-clear!] a
Whenever they are invoked, the execution escapes to the Racket interpreter.

@(rosette-eval '(require (only-in racket make-hash hash-clear! hash-ref)))
@defs+int[#:eval rosette-eval
@examples[#:eval rosette-eval

[(define h (make-hash '((1 . 2))))
(define h (make-hash '((1 . 2))))
(define-symbolic key integer?)
(define-symbolic b boolean?)]
(define-symbolic b boolean?)


(code:comment "The following call produces an incorrect value. Intuitively, we expect the")
Expand All @@ -84,23 +83,26 @@ Whenever they are invoked, the execution escapes to the Racket interpreter.
(code:comment "The following call produces an incorrect state. Intuitively, we expect h")
(code:comment "to be empty if b is true and unchanged otherwise.")
(when b
(pretty-print (vc))
(hash-clear! h))
h]

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 @var[c] in an @deftech{effectively concrete} @tech{program state}.
The SVM is in such a state when
@itemlist[#:style 'ordered
@item{the current @tech{path condition} is @racket[#t];}
@item{the @tech{assertion store} is empty; and,}
@item{the current @tech{verification condition} is true, i.e., @racket[(vc-true? (vc))]; and,}
@item{all local and global variables that may be read by @var[c] contain @deftech{fully concrete value}s. 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 @racket[hash-ref] and @racket[hash-clear!] in our buggy example violate the third and first
requirements, respectively.
The above uses of @racket[hash-ref] and @racket[hash-clear!] violate these
requirements: @racket[hash-ref] is reading a symbolic value, and @racket[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 @racket[for] or @racket[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.
bit of experience, it becomes easy to see when it is okay to break the effectively-concrete rule.

@(kill-evaluator rosette-eval)

0 comments on commit 532aa8e

Please sign in to comment.