Disallow define-symbolic with different types (emina#240)

Programs like: ``` (define (f type) (define-symbolic x type) x) (+ 1 (f integer?)) (+ 2 (f boolean?)) ``` should not work. The second call in particular should result in an error, rather than using the cached term (which is an integer). This PR makes the above program invalid. The SDSL benchmarks show that the performance was not affected by the change.
vcanumalla · Aug 17, 2022 · c407b87 · c407b87
1 parent ec1a0db
commit c407b87
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 9 deletions.
diff --git a/rosette/base/core/term.rkt b/rosette/base/core/term.rkt
@@ -121,14 +121,21 @@
 (define (term<? s1 s2) (< (term-ord s1) (term-ord s2)))
 
 (define-syntax-rule (make-term term-constructor args type rest ...) 
-  (let ([val args])
-    (or (hash-ref (current-terms) val #f)
-        (let* ([ord (current-index)]
-               [out (term-constructor val type ord rest ...)])
-          (current-index (add1 ord))
-          ((current-reporter) 'new-term out)
-          (hash-set! (current-terms) val out)
-          out))))
+  (let ([val args]
+        [ty type])
+    (define cached (hash-ref (current-terms) val #f))
+    (cond
+      [cached
+       (unless (equal? (term-type cached) ty)
+         (error 'define-symbolic "type should remain unchanged"))
+       cached]
+      [else
+       (define ord (current-index))
+       (define out (term-constructor val ty ord rest ...))
+       (current-index (add1 ord))
+       ((current-reporter) 'new-term out)
+       (hash-set! (current-terms) val out)
+       out])))
 
 (define (make-const id t) 
   (unless (and (type? t) (solvable? t))

diff --git a/test/base/term.rkt b/test/base/term.rkt
@@ -14,6 +14,10 @@
 (define-symbolic b @boolean?)
 (define-symbolic c @boolean?)
 
+(define (f type)
+  (define-symbolic x type)
+  x)
+
 (define (check-ordered v1 v2)
   (check-true (and (or (term<? v1 v2) (term<? v2 v1)) 
                    (not (and (term<? v1 v2) (term<? v2 v1))))))
@@ -49,7 +53,10 @@
    (check-cached @/ x y)
    (check-cached @remainder x y)
    (check-cached @= x y)
-   (check-cached @< x y)))
+   (check-cached @< x y)
+
+   (f @integer?)
+   (check-exn #px"type should remain unchanged" (lambda () (f @boolean?)))))
 
 (module+ test
   (time (run-tests value-tests)))