wip: feat: add support for z3 bit rotate exts

rosette (for convenience) provides functionality to download and install
a z3 binary during raco installation. unfortunately this package is
currently very out of date, so this commit removes all install-time
functionality, causing rosette to fall back to searching for the z3
binary in the system PATH

rosette/base/base.rkt

@@ -33,6 +33,7 @@
      @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
      @bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
      @concat @extract @sign-extend @zero-extend 
+     @z3_ext_rotate_left @z3_ext_rotate_right
      @integer->bitvector @bitvector->integer @bitvector->natural
      ; core/bvlib.rkt
      bit lsb msb bvzero? bvadd1 bvsub1

rosette/base/core/bitvector.rkt

@@ -14,6 +14,7 @@
  @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
  @bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
  @concat @extract @sign-extend @zero-extend
+ @z3_ext_rotate_left @z3_ext_rotate_right
  @integer->bitvector @bitvector->integer @bitvector->natural)
 
 ;; ----------------- Bitvector Types ----------------- ;; 
@@ -338,6 +339,13 @@
      (ite (bveq (bv 0 t) (bvand x (bv (bvsmin t) t))) (bv 0 t) (bv -1 t))]
     [(_ _) (expression @bvashr x y)]))
 
+
+(define (z3_ext_rotate_left x y)
+  (expression @z3_ext_rotate_left x y))
+
+(define (z3_ext_rotate_right x y)
+  (expression @z3_ext_rotate_right x y))
+
 (define-lifted-operator @bvnot bvnot T*->T)
 (define-lifted-operator @bvand bvand T*->T)
 (define-lifted-operator @bvor bvor T*->T)
@@ -345,6 +353,8 @@
 (define-lifted-operator @bvshl bvshl T*->T)
 (define-lifted-operator @bvlshr bvlshr T*->T)
 (define-lifted-operator @bvashr bvashr T*->T)
+(define-lifted-operator @z3_ext_rotate_left z3_ext_rotate_left T*->T)
+(define-lifted-operator @z3_ext_rotate_right z3_ext_rotate_right T*->T)
 
 ;; ----------------- Simplification ruules for bitwise operators ----------------- ;;
 

rosette/info.rkt

@@ -14,11 +14,7 @@
      (experimental))))
      ;; Documentation category. On Racket 6.3+ this can be any string.
 
-;; Runs the code in `private/install.rkt` before and after installing this collection.
-(define pre-install-collection "private/install.rkt")
-(define post-install-collection "private/install.rkt")
-(define compile-omit-files '("private/install.rkt"
-                             "lib/trace/report/node_modules"))
+(define compile-omit-files '("lib/trace/report/node_modules"))
 
 (define raco-commands
   '(("symprofile"

rosette/private/install.rkt

@@ -1,84 +0,0 @@
-#lang racket/base
-
-;; Check whether z3 is installed during package setup.
-;; If missing, builds & links a z3 binary.
-
-
-(provide pre-installer post-installer)
-
-(require racket/match
-         racket/file
-         racket/port
-         net/url
-         file/unzip)
-
-; We need to run the Z3 installer as a pre-install step, because building the
-; documentation relies on Z3 being available. But pre-install is so early in
-; the build that its output gets pushed off screen by the later steps. So we
-; use this little hack to repeat the failure message as a post-install step,
-; which happens at the very end of the install and so makes the error message
-; far more obvious.
-(define z3-install-failure #f)
-
-(define z3-version "4.8.8")
-
-(define (print-failure path msg)
-  (printf "\n\n********** Failed to install Z3 **********\n\n")
-  (printf "Rosette installed successfully, but wasn't able to install the Z3 SMT solver.\n\n")
-  (printf "You'll need to manually install a Z3 binary at this location:\n")
-  (printf "    ~a\n" path)
-  (printf "or anywhere that is on your PATH. Alternatively, in your programs, you can\n")
-  (printf "construct a solver object manually:\n")
-  (printf "    (current-solver (z3 #:path \"/path/to/z3\"))\n\n")
-  (printf "Note that Rosette ships with a specific release of Z3 (v~a). Installing a\n" z3-version)
-  (printf "different version of Z3 may change the performance of Rosette programs.\n\n")
-  (printf "The problem was:\n    ~a\n\n" msg)
-  (printf "**********\n\n\n"))
-
-(define (post-installer collections-top-path)
-  (match z3-install-failure
-    [(cons z3-path msg) (print-failure z3-path msg)]
-    [_ (void)]))
-
-(define (pre-installer collections-top-path racl-path)
-  (define bin-path (simplify-path (build-path racl-path ".." "bin")))
-  (define z3-path (build-path bin-path "z3"))
-  (with-handlers ([exn:fail? (lambda (e)
-                               (set! z3-install-failure (cons z3-path (exn-message e)))
-                               (print-failure z3-path (exn-message e)))])
-    (unless (custom-z3-symlink? z3-path)
-      (define-values (z3-url z3-path-in-zip) (get-z3-url))
-      (define z3-port (get-pure-port (string->url z3-url) #:redirections 10))  
-      (make-directory* bin-path) ;; Ensure that `bin-path` exists
-      (delete-directory/files z3-path #:must-exist? #f) ;; Delete old version of Z3, if any
-      (parameterize ([current-directory bin-path])    
-        (call-with-unzip z3-port
-                         (λ (dir)
-                           (copy-directory/files (build-path dir z3-path-in-zip) z3-path)))
-        ;; Unzipping loses file permissions, so we reset the z3 binary here
-        (file-or-directory-permissions 
-          z3-path 
-          (if (equal? (system-type) 'windows) #o777 #o755))))))
-
-(define (custom-z3-symlink? z3-path)
-  (and (file-exists? z3-path)
-       (let ([p (simplify-path z3-path)])
-         (not (equal? (resolve-path p) p)))))
-
-(define (get-z3-url)
-  ; TODO: Z3 packages a macOS aarch64 binary as of 4.8.16, so remove this special case when we update
-  ; to a newer Z3 version.
-  (if (and (equal? (system-type 'os*) 'macosx) (equal? (system-type 'arch) 'aarch64))
-      (values "https://github.com/emina/rosette/releases/download/4.1/z3-4.8.8-aarch64-osx-13.3.1.zip" "z3")
-      (let ()
-        (define site "https://github.com/Z3Prover/z3/releases/download")
-        (define-values (os exe)
-          (match (list (system-type 'os*) (system-type 'arch))
-            ['(linux x86_64)   (values "x64-ubuntu-16.04" "z3")]
-            [`(macosx ,_)      (values "x64-osx-10.14.6" "z3")]
-            ['(windows x86_64) (values "x64-win" "z3.exe")]
-            [any               (raise-user-error 'get-z3-url "No Z3 binary available for system type '~a" any)]))
-        (define name (format "z3-~a-~a" z3-version os))
-        (values
-         (format "~a/z3-~a/~a.zip" site z3-version name)
-         (format "~a/bin/~a" name exe)))))

rosette/solver/smt/bitwuzla.rkt

@@ -14,7 +14,8 @@
 
 (provide (rename-out [make-bitwuzla bitwuzla]) bitwuzla? bitwuzla-available?)
 
-(define-runtime-path bitwuzla-path (build-path ".." ".." ".." "bin" "bitwuzla"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define bitwuzla-path (build-path bin-path "bitwuzla"))
 (define bitwuzla-opts '("-m"))
 
 (define (bitwuzla-available?)

rosette/solver/smt/boolector.rkt

@@ -14,7 +14,8 @@
 
 (provide (rename-out [make-boolector boolector]) boolector? boolector-available?)
 
-(define-runtime-path boolector-path (build-path ".." ".." ".." "bin" "boolector"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define boolector-path (build-path bin-path "boolector"))
 (define boolector-opts '("-m" "--output-format=smt2" "-i"))
 
 (define (boolector-available?)

rosette/solver/smt/cvc4.rkt

@@ -7,7 +7,8 @@
 
 (provide (rename-out [make-cvc4 cvc4]) cvc4? cvc4-available?)
 
-(define-runtime-path cvc4-path (build-path ".." ".." ".." "bin" "cvc4"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define cvc4-path (build-path bin-path "cvc4"))
 (define cvc4-opts '("-L" "smt2" "-q" "-m" "-i" "--bv-print-consts-as-indexed-symbols" "--bv-div-zero-const"))
 
 (define (cvc4-available?)

rosette/solver/smt/cvc5.rkt

@@ -7,7 +7,8 @@
 
 (provide (rename-out [make-cvc5 cvc5]) cvc5? cvc5-available?)
 
-(define-runtime-path cvc5-path (build-path ".." ".." ".." "bin" "cvc5"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define cvc5-path (build-path bin-path "cvc5"))
 (define cvc5-opts '("-L" "smt2" "-q" "-m" "-i" "--bv-print-consts-as-indexed-symbols"))
 
 (define (cvc5-available?)

rosette/solver/smt/dec.rkt

@@ -14,6 +14,7 @@
                   @bvslt @bvsle @bvult @bvule   
                   @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
                   @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
+                  @z3_ext_rotate_left @z3_ext_rotate_right
                   @concat @extract))
 
 
@@ -161,6 +162,7 @@
         'bvslt @bvslt 'bvsle @bvsle 'bvult @bvult 'bvule @bvule   
         'bvnot @bvnot 'bvor @bvor 'bvand @bvand 'bvxor @bvxor
         'bvshl @bvshl 'bvlshr @bvlshr 'bvashr @bvashr
+        'ext_rotate_left @z3_ext_rotate_left 'ext_rotate_right @z3_ext_rotate_right
         'bvneg @bvneg 'bvadd @bvadd 'bvmul @bvmul
         'bvudiv @bvudiv 'bvsdiv @bvsdiv
         'bvurem @bvurem 'bvsrem @bvsrem

rosette/solver/smt/enc.rkt

@@ -16,6 +16,7 @@
                   @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
                   @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
                   @concat @extract @zero-extend @sign-extend 
+                  @z3_ext_rotate_left @z3_ext_rotate_right
                   @integer->bitvector @bitvector->integer @bitvector->natural))
 
 (provide enc)
@@ -108,6 +109,7 @@
   [@bveq $=] [@bvslt $bvslt] [@bvsle $bvsle] [@bvult $bvult] [@bvule $bvule] 
   [@bvnot $bvnot] [@bvor $bvor] [@bvand $bvand] [@bvxor $bvxor] 
   [@bvshl $bvshl] [@bvlshr $bvlshr] [@bvashr $bvashr]
+  [@z3_ext_rotate_left $ext_rotate_left] [@z3_ext_rotate_right $ext_rotate_right]
   [@bvneg $bvneg] [@bvadd $bvadd] [@bvmul $bvmul] [@bvudiv $bvudiv] [@bvsdiv $bvsdiv]
   [@bvurem $bvurem] [@bvsrem $bvsrem] [@bvsmod $bvsmod] [@concat $concat])
 

rosette/solver/smt/smtlib2.rkt

@@ -68,7 +68,8 @@
   bvnot bvand bvor bvxor 
   bvule bvult bvuge bvugt bvsle bvslt bvsge bvsgt
   bvneg bvadd bvsub bvmul bvsdiv bvudiv bvurem bvsrem bvsmod
-  bvshl bvlshr bvashr concat) 
+  bvshl bvlshr bvashr concat
+  ext_rotate_left ext_rotate_right) 
 
 (define (extract i j s)
   `((_ extract ,i ,j) ,s))

rosette/solver/smt/stp.rkt

@@ -7,7 +7,8 @@
 
 (provide (rename-out [make-stp stp]) stp? stp-available?)
 
-(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define stp-path (build-path bin-path "stp"))
 (define stp-opts '("--SMTLIB2"))
 
 (define (stp-available?)
@@ -66,4 +67,3 @@
 
 (define (set-default-options server)
   void)
-  

rosette/solver/smt/yices.rkt

@@ -7,7 +7,8 @@
 
 (provide (rename-out [make-yices yices]) yices? yices-available?)
 
-(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices-smt2"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define yices-path (build-path bin-path "yices-smt2"))
 (define yices-opts '("--incremental"))
 
 (define (yices-available?)
@@ -66,4 +67,3 @@
 
 (define (set-default-options server)
   void)
-  

rosette/solver/smt/z3.rkt

@@ -12,7 +12,8 @@
 
 (provide (rename-out [make-z3 z3]) z3?)
 
-(define-runtime-path z3-path (build-path ".." ".." ".." "bin" "z3"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define z3-path (build-path bin-path "z3"))
 (define z3-opts '("-smt2" "-in"))
 
 (define default-options
@@ -76,7 +77,7 @@
      (base/solver-pop self k))
    
    (define (solver-check self)
-     (base/solver-check self))
+     (base/solver-check self z3-read-solution))
 
    (define (solver-debug self)
      (match-define (z3 server _ (app unique asserts) _ _ _ _) self)
@@ -88,7 +89,7 @@
                   server
                   (begin (encode-for-proof (base/solver-env self) asserts)
                          (check-sat)))
-                 (base/read-solution server (base/solver-env self) #:unsat-core? #t)]))])
+                 (z3-read-solution server (base/solver-env self) #:unsat-core? #t)]))])
 
 (define (set-core-options server)
   (server-write server
@@ -101,3 +102,27 @@
     (match t
       [(term _ (or (== @integer?) (== @real?) (? bitvector?))) t]
       [_ (error caller "expected a numeric term, given ~s" t)])))
+
+(define (z3-read-solution server env #:unsat-core? [unsat-core? #f])
+  (decode (match (base/parse-solution server #:unsat-core? unsat-core?)
+            [(? hash? sol) (prune-model sol)]
+            [soln soln])
+          env))
+
+; Given a map M from symbols to SMTLib function definitions of the form
+; (define-fun id ((param type) ...) ret body),
+; this procedure eliminate bindings for intermediate expressions,
+; which are ids that start with "e" (e.g. "e20"),
+; originally defined with define-fun (as opposed to declare-fun) in the query.
+; In particular, old versions of Z3 did this pruning automatically,
+; and Rosette had been working under this assumption.
+; Newer versions of Z3 however included extra bindings,
+; so we are pruning them away.
+(define (prune-model sol)
+  (for/hash ([(k v) (in-immutable-hash sol)]
+             #:unless (match v
+                        [`(define-fun ,(? symbol? (app symbol->string id)) ,_ ,_ ,_)
+                         #:when (string-prefix? id "e")
+                         #t]
+                        [_ #f]))
+    (values k v)))

test/query/solve.rkt

@@ -65,8 +65,9 @@
       (check-pred
        unknown?
        (solve
-        (begin (assert (> (* xi xi) 3))
-               (assert (= (+ (* xr xr xr) (* xr yr)) 3.0))))))))
+        (assert (forall (list xi)
+                        (exists (list xr)
+                                (= yi (* (- xi xr) (- xi xr)))))))))))
      
 (define regression-tests 
   (test-suite+ "Solve regression tests."