wip: feat: add support for z3 bit rotate exts

z3 > 4.8.8 will return sign_extend and zero_extend operators in the
model, which were not handled by the smt-lib2 decoder, despite being
handled in the encoder. support for these operators has been added

.github/workflows/docker.yml

@@ -14,7 +14,7 @@ jobs:
 
     steps:
       - name: Clone Repository
-        uses: actions/checkout@v6
+        uses: actions/checkout@v4
 
       - name: Configure Docker Metadata
         id: meta

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/dec.rkt

@@ -14,7 +14,8 @@
                   @bvslt @bvsle @bvult @bvule   
                   @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
                   @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
-                  @concat @extract))
+                  @z3_ext_rotate_left @z3_ext_rotate_right
+                  @concat @extract @sign-extend @zero-extend))
 
 
 (provide decode-model)
@@ -131,6 +132,10 @@
         (bv n (bitvector len))]
        [(list (list (== '_) (== 'extract) i j) s)
         `(, @extract ,(inline i sol ~env) ,(inline j sol ~env) ,(inline s sol ~env))]
+       [(list (list (== '_) (== 'sign_extend) i) s)
+        `(, @sign-extend ,(inline i sol ~env) ,(inline s sol ~env))]
+       [(list (list (== '_) (== 'zero_extend) i) s)
+        `(, @zero-extend ,(inline i sol ~env) ,(inline s sol ~env))]
        [(list (== 'let) binds body)
         (substitute (inline body sol ~env)
                     (for/hash ([id:expr binds])
@@ -161,6 +166,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))