Update sdsl/bv and sdsl/synthcl.

jamestiotio · Dec 10, 2020 · c335d89 · c335d89
1 parent 8fc406a
commit c335d89
Show file tree

Hide file tree

Showing 6 changed files with 37 additions and 34 deletions.
diff --git a/sdsl/bv/lang/core.rkt b/sdsl/bv/lang/core.rkt
@@ -5,7 +5,8 @@
   (only-in "program.rkt" trace* trace-args trace-out well-formed-program well-formed-trace)
   rosette/query/eval "log.rkt"
   (only-in rosette/base/core/term term? constant? get-type term-cache term<?)
-  (only-in rosette/base/core/bool ! || && => with-asserts-only)
+  (only-in rosette/base/core/bool ! || && => with-vc spec-assumes spec-asserts)
+  (only-in rosette/base/core/result result-state)
   (only-in rosette/base/core/real @integer?)
   (only-in rosette/base/core/bitvector bitvector bitvector-size)
   (only-in rosette/solver/solution model sat sat? unsat? unsat)
@@ -62,13 +63,14 @@
 
   (define (init)
     (solver-clear guesser)
-    (solver-assert guesser (φ_wfp impl))
+    (define impl_wfp (normal? (φ_wfp impl)))  
+    (solver-assert guesser impl_wfp)
     (solver-assert guesser (φ_synth t0 spec))
     (log-solver-info [trial] "searching for an initial candidate at ~a" (BV))
     (begin0
       (solution->candidate (solver-check guesser))
       (solver-clear guesser)
-      (solver-assert guesser (φ_wfp impl))))
+      (solver-assert guesser impl_wfp)))
 
   (define (guess sol)
     (set! trial (add1 trial))
@@ -90,21 +92,24 @@
           (cond 
             [(unsat? cex) candidate]
             [else (loop (guess cex))]))])))
-
+
+(define (normal? sp) (list (spec-assumes sp) (spec-asserts sp)))
+(define (crash? sp)  (list (spec-assumes sp) (! (spec-asserts sp))))
+
 (define (φ_synth trace spec) ;(printf "φ_synth: ~a\n" trace)
-  (append (φ_wft trace) (φ_spec trace spec)))
+  `(,@(normal? (φ_wft trace)) ,@(normal? (φ_spec trace spec))))
 
 (define (φ_verify trace spec) ;(printf "φ_verify: ~a\n" trace)
-  `(,@(φ_wft trace) ,(apply || (map ! (φ_spec trace spec)))))
+  `(,@(normal? (φ_wft trace)) ,@(crash? (φ_spec trace spec))))
 
 (define (φ_wfp impl) ;(printf "φ_wfp: ~a\n" impl)
-  (with-asserts-only (well-formed-program impl)))
+  (result-state (with-vc (well-formed-program impl))))
 
 (define (φ_wft trace) 
-  (with-asserts-only (well-formed-trace trace)))
+  (result-state (with-vc (well-formed-trace trace))))
 
 (define (φ_spec trace spec)
-  (with-asserts-only (trace-out trace (apply spec (trace-args trace)))))
+  (result-state (with-vc (trace-out trace (apply spec (trace-args trace))))))
 
 (define (solution->candidate sol)
   (match sol

diff --git a/sdsl/synthcl/lang/forms.rkt b/sdsl/synthcl/lang/forms.rkt
@@ -32,11 +32,7 @@
   (syntax-case stx ()
     [(assert val) 
      (quasisyntax/loc stx 
-       (rosette/assert ((bool) val) 
-                       (thunk (raise-assertion-error #'assert))))]))
-
-(define (raise-assertion-error stx)
-  (error 'assert "failed at ~a:~a:~a" (syntax-source stx) (syntax-line stx) (syntax-column stx)))
+       (rosette/assert ((bool) val)))]))
 
 ; Variable declaration.  Declared real variables are bound to fresh symbolic constants created
 ; using define-symbolic*. Declared pointer variables with known length are bound to arrays (pointers)

diff --git a/sdsl/synthcl/model/memory.rkt b/sdsl/synthcl/model/memory.rkt
@@ -1,7 +1,7 @@
 #lang rosette
 
 (require "errors.rkt" "work.rkt" "type.rkt" "reals.rkt" 
-         (only-in "pointers.rkt" gen:pointer)               
+         (only-in "pointers.rkt" gen:pointer)           
          racket/generic rosette/lib/match)
 
 (provide (rename-out [make-memory memory]) memory? memory-empty?
@@ -11,7 +11,7 @@
 ; or 64 if no capacity is given.
 (define (make-memory [capacity 512])
   (assert (and (integer? capacity) (positive? capacity))
-          (thunk (raise-argument-error 'memory "positive capacity" capacity)))
+          (format "memory: contract violation\n  expected: positive capacity\n  given: ~a" capacity))
   (memory 0 (make-vector capacity)))
 
 ; Represents a memory structure that contains zero or more allocated
@@ -114,8 +114,8 @@
   (when writes 
     (for ([i len] [w (take (drop (vector->list writes) idx) len)])
       (assert (or (false? w) (equal? w (current-global-id)))
-              (thunk (error caller "access conflict detected on memory address #x~x[~a]"  
-                            address (+ idx i)))))))
+              (format "~a: access conflict detected on memory address #x~x[~a]" caller  
+                      address (+ idx i))))))
 
 ; Returns the value stored at the given offset from the 
 ; base address of the given pointer (i.e., ptr[idx]).

diff --git a/sdsl/synthcl/model/pointers.rkt b/sdsl/synthcl/model/pointers.rkt
@@ -69,7 +69,7 @@
   (pointer-type 
    void 
    (let* ([cast-void* (lambda (b) 
-                        (assert (pointer? b) (thunk (raise-pointer-cast-error b void)))
+                        (assert (pointer? b) (format "pointer-cast: cannot cast ~a to ~a*" b void))
                         b)]
           [void* (thunk cast-void*)])
      void*)))

diff --git a/sdsl/synthcl/model/reals.rkt b/sdsl/synthcl/model/reals.rkt
@@ -114,7 +114,7 @@
                        [(union (list _ (... ...) (cons g (or (? primitive p) 
                                                              (and (term _ (== base)) p))) 
                                      _ (... ...)) _)
-                        (assert g (thunk  (raise-argument-error 'id (~a 'id) v)))
+                        (assert g)
                         p]
                        [_ (raise-argument-error 'id (~a 'id) v)])]))
 

diff --git a/sdsl/synthcl/test/memory.rkt b/sdsl/synthcl/test/memory.rkt
@@ -1,6 +1,7 @@
 #lang rosette
 
-(require rackunit rackunit/text-ui rosette/lib/roseunit
+(require rackunit rackunit/text-ui (rename-in rackunit [check-exn rackunit/check-exn])
+         rosette/lib/roseunit
          "../model/memory.rkt" "../model/work.rkt" 
          "../model/reals.rkt"  "../model/pointers.rkt"
          "../model/context.rkt" "../model/buffer.rkt" "../model/flags.rkt")
@@ -114,35 +115,36 @@
     (parameterize ([current-global-id '(3)])
       (pointer-ref ptr 2))))
 
-(define (fails-with? msg)
-  (lambda (e)
-    (and (exn:fail? e) (for/and ([c0 msg][c1 (exn-message e)]) (equal? c0 c1)))))
-
+
+(define-syntax-rule (check-exn e ...)
+  (begin
+    (rackunit/check-exn e ...)
+    (clear-vc!)))
 
 (define memory-tests
   (test-suite+ 
    "Tests for memory functions"
 
-   (check-exn (fails-with? "pointer-ref: cannot read from a write-only memory address #x0[1]")
+   (check-exn #px"pointer-ref: cannot read from a write-only memory address #x0\\[1\\]"
               read-write-only-buffer)
-   (check-exn (fails-with? "pointer-set!: cannot write to a read-only memory address #x0[1]") 
+   (check-exn #px"pointer-set!: cannot write to a read-only memory address #x0\\[1\\]" 
               write-read-only-buffer)
-   (check-exn (fails-with? "pointer-set!: access conflict detected on memory address #x0[1]")
+   (check-exn #px"pointer-set!: access conflict detected on memory address #x0\\[1\\]"
               write-write-conflict)
-   (check-exn (fails-with? "pointer-ref: access conflict detected on memory address #x0[9]") 
+   (check-exn #px"pointer-ref: access conflict detected on memory address #x0\\[9\\]"
               read-write-conflict)
-   (check-exn (fails-with? "implicit-conversion: cannot convert #(4 5) to int3") 
+   (check-exn #px"implicit-conversion: cannot convert #\\(4 5\\) to int3"
               vector-write-type-error)
-   (check-exn (fails-with? "take") 
+   (check-exn #px"take" 
               vector-write-range-error)
    (check-equal? (vector-write-success) '(0 0 0 4 5 6))
-   (check-exn (fails-with? "int: contract violation")
+   (check-exn #px"int: contract violation"
               vector-read-type-error)
-   (check-exn (fails-with? "take") 
+   (check-exn #px"take" 
               vector-read-range-error)
    (check-equal? (vector-read-success) (int3 4 5 6))
    (check-equal? (vector-write-read-success) (int3 0 0 0))
-   (check-exn (fails-with? "pointer-ref: access conflict detected on memory address #x0[0]")
+   (check-exn #px"pointer-ref: access conflict detected on memory address #x0\\[0\\]"
               vector-write-read-conflict-error)
    (check-not-exn successful-synchronize)))