add all bv ops from rosette
This commit is contained in:
Stephen Chang
parent
38ba3d273d
commit
cef8660c75
|
|
@ -1,8 +1,11 @@
|
|||
#lang turnstile
|
||||
;(require (only-in rosette bv bitvector))
|
||||
;(require (only-in rosette [exact-integer? integer?]))
|
||||
(require syntax/parse/define)
|
||||
(extends "../ext-stlc.rkt")
|
||||
(extends "../ext-stlc.rkt" #:except if)
|
||||
(require (only-in "../stlc+reco+var.rkt" define-type-alias))
|
||||
(require (prefix-in ro: rosette))
|
||||
(provide BVPred)
|
||||
|
||||
(define-simple-macro (define-rosette-primop op:id : ty)
|
||||
(begin
|
||||
|
|
@ -13,18 +16,66 @@
|
|||
(require (only-in rosette [op1 op2]))
|
||||
(define-primop op2 : ty)))
|
||||
|
||||
(provide BVPred)
|
||||
;; ----------------------------------------------------------------------------
|
||||
;; Rosette stuff
|
||||
|
||||
(define-typed-syntax define-symbolic
|
||||
[(_ x:id ...+ pred : ty:type) ≫
|
||||
[⊢ [[pred ≫ pred-] ⇐ : (→ ty.norm Bool)]]
|
||||
[#:with (y ...) (generate-temporaries #'(x ...))]
|
||||
--------
|
||||
[_ ≻ (begin-
|
||||
(define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ...
|
||||
(ro:define-symbolic y ... pred-))]])
|
||||
|
||||
(define-rosette-primop boolean? : (→ Bool Bool))
|
||||
(define-rosette-primop integer? : (→ Int Bool))
|
||||
(define-rosette-primop string? : (→ String Bool))
|
||||
|
||||
(define-typed-syntax if
|
||||
[(if e_tst e1 e2) ⇐ : τ-expected ≫
|
||||
[⊢ [[e_tst ≫ e_tst-] ⇒ : _]] ; Any non-false value is truthy.
|
||||
[⊢ [[e1 ≫ e1-] ⇐ : τ-expected]]
|
||||
[⊢ [[e2 ≫ e2-] ⇐ : τ-expected]]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:if e_tst- e1- e2-)] ⇐ : _]]]
|
||||
[(if e_tst e1 e2) ≫
|
||||
[⊢ [[e_tst ≫ e_tst-] ⇒ : _]] ; Any non-false value is truthy.
|
||||
[⊢ [[e1 ≫ e1-] ⇒ : τ1]]
|
||||
[⊢ [[e2 ≫ e2-] ⇒ : τ2]]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:if e_tst- e1- e2-)] ⇒ : (⊔ τ1 τ2)]]])
|
||||
|
||||
;; ----------------------------------------------------------------------------
|
||||
;; BV stuff
|
||||
|
||||
;; TODO: make BV parametric in a dependent n?
|
||||
(define-base-type BV) ; represents actual bitvectors
|
||||
|
||||
; a predicate recognizing bv's of a certain size
|
||||
(define-type-alias BVPred (→ BV Bool))
|
||||
|
||||
(define-rosette-primop bv : (→ Int BVPred BV))
|
||||
;; TODO: fix me --- need subtyping?
|
||||
(define-type-alias Nat Int)
|
||||
|
||||
;; TODO: support higher order case --- need intersect types?
|
||||
;(define-rosette-primop bv : (→ Int BVPred BV)
|
||||
(define-typed-syntax bv
|
||||
[(_ e_val e_size) ≫
|
||||
[⊢ [[e_val ≫ e_val-] ⇐ : Int]]
|
||||
[⊢ [[e_size ≫ e_size-] ⇐ : BVPred]]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:bv e_val- e_size-)] ⇒ : BV]]]
|
||||
[(_ e_val e_size) ≫
|
||||
[⊢ [[e_val ≫ e_val-] ⇐ : Int]]
|
||||
[⊢ [[e_size ≫ e_size-] ⇐ : Nat]]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:bv e_val- e_size-)] ⇒ : BV]]])
|
||||
|
||||
(define-rosette-primop bv? : (→ BV Bool))
|
||||
(define-rosette-primop bitvector : (→ Int BVPred))
|
||||
(define-rosette-primop bitvector : (→ Nat BVPred))
|
||||
(define-rosette-primop bitvector? : (→ BVPred Bool))
|
||||
(define-rosette-primop* bitvector bvpred : (→ Int BVPred))
|
||||
(define-rosette-primop* bitvector bvpred : (→ Nat BVPred))
|
||||
(define-rosette-primop* bitvector? bvpred? : (→ BVPred Bool))
|
||||
|
||||
(define-rosette-primop bveq : (→ BV BV Bool))
|
||||
|
|
@ -38,9 +89,62 @@
|
|||
(define-rosette-primop bvuge : (→ BV BV Bool))
|
||||
|
||||
(define-rosette-primop bvnot : (→ BV BV))
|
||||
;; (require (postfix-in - (rosette))
|
||||
;; (define-typed-syntax bvand
|
||||
;; [(_ e ...+)
|
||||
;; [⊢ [[e ≫ e-] ⇐ : BV] ...]
|
||||
;; --------
|
||||
;; [⊢ [[_ ≫ (bvand- e- ...)] ⇒ : Bool]]])
|
||||
|
||||
|
||||
(define-typed-syntax bvand
|
||||
[(_ e ...+) ≫
|
||||
[⊢ [[e ≫ e-] ⇐ : BV] ...]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:bvand e- ...)] ⇒ : BV]]])
|
||||
(define-typed-syntax bvor
|
||||
[(_ e ...+) ≫
|
||||
[⊢ [[e ≫ e-] ⇐ : BV] ...]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:bvor e- ...)] ⇒ : BV]]])
|
||||
(define-typed-syntax bvxor
|
||||
[(_ e ...+) ≫
|
||||
[⊢ [[e ≫ e-] ⇐ : BV] ...]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:bvxor e- ...)] ⇒ : BV]]])
|
||||
|
||||
(define-rosette-primop bvshl : (→ BV BV BV))
|
||||
(define-rosette-primop bvlshr : (→ BV BV BV))
|
||||
(define-rosette-primop bvashr : (→ BV BV BV))
|
||||
(define-rosette-primop bvneg : (→ BV BV))
|
||||
|
||||
(define-typed-syntax bvadd
|
||||
[(_ e ...+) ≫
|
||||
[⊢ [[e ≫ e-] ⇐ : BV] ...]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:bvadd e- ...)] ⇒ : BV]]])
|
||||
(define-typed-syntax bvsub
|
||||
[(_ e ...+) ≫
|
||||
[⊢ [[e ≫ e-] ⇐ : BV] ...]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:bvsub e- ...)] ⇒ : BV]]])
|
||||
(define-typed-syntax bvmul
|
||||
[(_ e ...+) ≫
|
||||
[⊢ [[e ≫ e-] ⇐ : BV] ...]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:bvmul e- ...)] ⇒ : BV]]])
|
||||
|
||||
(define-rosette-primop bvsdiv : (→ BV BV BV))
|
||||
(define-rosette-primop bvudiv : (→ BV BV BV))
|
||||
(define-rosette-primop bvsrem : (→ BV BV BV))
|
||||
(define-rosette-primop bvurem : (→ BV BV BV))
|
||||
(define-rosette-primop bvsmod : (→ BV BV BV))
|
||||
|
||||
(define-typed-syntax concat
|
||||
[(_ e ...+) ≫
|
||||
[⊢ [[e ≫ e-] ⇐ : BV] ...]
|
||||
--------
|
||||
[⊢ [[_ ≫ (ro:concat e- ...)] ⇒ : BV]]])
|
||||
|
||||
(define-rosette-primop extract : (→ Int Int BV BV))
|
||||
;; TODO: additionally support union in 2nd arg
|
||||
(define-rosette-primop sign-extend : (→ BV BVPred BV))
|
||||
(define-rosette-primop zero-extend : (→ BV BVPred BV))
|
||||
|
||||
(define-rosette-primop bitvector->integer : (→ BV Int))
|
||||
(define-rosette-primop bitvector->natural : (→ BV Int))
|
||||
(define-rosette-primop integer->bitvector : (→ Int BVPred BV))
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
#lang s-exp "../../rosette/bv.rkt"
|
||||
(require "../rackunit-typechecking.rkt")
|
||||
|
||||
(check-type bv : (→ Int BVPred BV))
|
||||
;(check-type bv : (→ Int BVPred BV))
|
||||
(typecheck-fail (bv "1" 2) #:with-msg "expected Int, given String")
|
||||
(check-type (bv 1 (bvpred 2)) : BV -> (bv 1 (bvpred 2)))
|
||||
|
||||
|
|
@ -15,14 +15,89 @@
|
|||
(check-type (bvpred 3) : BVPred)
|
||||
(typecheck-fail ((bvpred 4) 1))
|
||||
(check-type ((bvpred 4) (bv 10 (bvpred 4))) : Bool)
|
||||
;; TODO: add Nat to catch this at compile time?
|
||||
(check-type (bvpred -1) : BVPred) ; runtime exn
|
||||
(check-runtime-exn (bvpred -1))
|
||||
|
||||
(typecheck-fail (bitvector? "2"))
|
||||
(check-type (bitvector? (bitvector 10)) : Bool -> #t)
|
||||
(typecheck-fail (bvpred? "2"))
|
||||
(check-type (bvpred? (bvpred 10)) : Bool -> #t)
|
||||
|
||||
;; bvops
|
||||
(check-type (bveq (bv 1 (bvpred 3)) (bv 1 (bvpred 3))) : Bool -> #t)
|
||||
(typecheck-fail (bveq (bv 1 (bvpred 3)) 1))
|
||||
(check-type (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3))) : Bool) ; -> exn
|
||||
(check-type (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3))) : Bool) ; -> runtime exn
|
||||
(check-runtime-exn (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3))))
|
||||
|
||||
;; non-primop bvops
|
||||
(check-type (bvand (bv -1 (bvpred 4)) (bv 2 (bvpred 4))) : BV
|
||||
-> (bv 2 (bvpred 4)))
|
||||
(check-type (bvor (bv 0 (bvpred 3)) (bv 1 (bvpred 3))) : BV
|
||||
-> (bv 1 (bvpred 3)))
|
||||
(check-type (bvxor (bv -1 (bvpred 5)) (bv 1 (bvpred 5))) : BV
|
||||
-> (bv -2 (bvpred 5)))
|
||||
|
||||
;; examples from rosette guide
|
||||
(check-type (bvand (bv -1 4) (bv 2 4)) : BV -> (bv 2 4))
|
||||
(check-type (bvor (bv 0 3) (bv 1 3)) : BV -> (bv 1 3))
|
||||
(check-type (bvxor (bv -1 5) (bv 1 5)) : BV -> (bv -2 5))
|
||||
|
||||
(define-symbolic b boolean? : Bool)
|
||||
(check-type (bvand (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV
|
||||
-> (if b (bv 3 4) (bv 2 4)))
|
||||
|
||||
(check-type (bvshl (bv 1 4) (bv 2 4)) : BV -> (bv 4 4))
|
||||
(check-type (bvlshr (bv -1 3) (bv 1 3)) : BV -> (bv 3 3))
|
||||
(check-type (bvashr (bv -1 5) (bv 1 5)) : BV -> (bv -1 5))
|
||||
;; TODO: see issue #23
|
||||
(check-type (bvshl (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV)
|
||||
|
||||
(check-type (bvneg (bv -1 4)) : BV -> (bv 1 4))
|
||||
(check-type (bvneg (bv 0 4)) : BV -> (bv 0 4))
|
||||
(define-symbolic z (bitvector 3) : BV)
|
||||
(check-type (bvneg z) : BV)
|
||||
(check-type (bvadd (bv -1 4) (bv 2 4)) : BV -> (bv 1 4))
|
||||
(check-type (bvsub (bv 0 3) (bv 1 3)) : BV -> (bv -1 3))
|
||||
(check-type (bvmul (bv -1 5) (bv 1 5)) : BV -> (bv -1 5))
|
||||
;; TODO: see issue #23
|
||||
(check-type (bvadd (bv -1 4) (bv 2 4) (if b (bv 1 4) (bv 3 4))) : BV)
|
||||
(check-type (bvsdiv (bv -3 4) (bv 2 4)) : BV -> (bv -1 4))
|
||||
(check-type (bvudiv (bv -3 3) (bv 2 3)) : BV -> (bv 2 3))
|
||||
(check-type (bvsmod (bv 1 5) (bv 0 5)) : BV -> (bv 1 5))
|
||||
(check-type (bvsrem (bv -3 4) (if b (bv 2 4) (bv 3 4))) : BV
|
||||
-> (if b (bv -1 4) (bv 0 4)))
|
||||
|
||||
(check-type (concat (bv -1 4) (bv 0 1) (bv -1 3)) : BV -> (bv -9 8))
|
||||
(check-type (concat (bv -1 4) (if b (bv 0 1) (bv 0 2)) (bv -1 3)) : BV
|
||||
-> (if b (bv -9 8) (bv -25 9)))
|
||||
|
||||
(check-type (extract 2 1 (bv -1 4)) : BV -> (bv -1 2))
|
||||
(check-type (extract 3 3 (bv 1 4)) : BV -> (bv 0 1))
|
||||
(define-symbolic i j integer? : Int)
|
||||
(check-type (extract i j (bv 1 2)) : BV)
|
||||
; -> {[(&& (= 0 j) (= 1 i)) (bv 1 2)] ...})
|
||||
|
||||
(check-type (sign-extend (bv -3 4) (bitvector 6)) : BV -> (bv -3 6))
|
||||
(check-type (zero-extend (bv -3 4) (bitvector 6)) : BV -> (bv 13 6))
|
||||
(define-symbolic c boolean? : Bool)
|
||||
(check-type (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6)))
|
||||
: BV -> (if b (bv 13 5) (bv 13 6)))
|
||||
#;(check-type (zero-extend (bv -3 4) (if b (bitvector 5) "bad"))
|
||||
: BV -> (bv 13 5))
|
||||
(check-type (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1)))
|
||||
: BV -> (bv 13 5))
|
||||
|
||||
(check-type (bitvector->integer (bv -1 4)) : Int -> -1)
|
||||
(check-type (bitvector->natural (bv -1 4)) : Int -> 15)
|
||||
(check-type (bitvector->integer (if b (bv -1 3) (bv -3 4)))
|
||||
: Int -> (if b -1 -3))
|
||||
;(check-type (bitvector->integer (if b (bv -1 3) "bad")) : BV -> -1)
|
||||
(check-type (integer->bitvector 4 (bitvector 2)) : BV -> (bv 0 2))
|
||||
(check-type (integer->bitvector 15 (bitvector 4)) : BV -> (bv -1 4))
|
||||
#;(check-type (integer->bitvector (if b pi 3)
|
||||
(if c (bitvector 5) (bitvector 6)))
|
||||
: BV -> {[c (bv 3 5)] [(! c) (bv 3 6)]})
|
||||
(check-type (integer->bitvector 3
|
||||
(if c (bitvector 5) (bitvector 6)))
|
||||
: BV -> (if c (bv 3 5) (bv 3 6)))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user