From cef8660c750084e93250d31e08651d8d076d0fad Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 12 Jul 2016 16:36:21 -0400 Subject: [PATCH] add all bv ops from rosette --- turnstile/examples/rosette/bv.rkt | 126 ++++++++++++++++-- turnstile/examples/tests/rosette/bv-tests.rkt | 79 ++++++++++- 2 files changed, 192 insertions(+), 13 deletions(-) diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt index 5d567b5..9af1920 100644 --- a/turnstile/examples/rosette/bv.rkt +++ b/turnstile/examples/rosette/bv.rkt @@ -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)) diff --git a/turnstile/examples/tests/rosette/bv-tests.rkt b/turnstile/examples/tests/rosette/bv-tests.rkt index 41154fe..96be45f 100644 --- a/turnstile/examples/tests/rosette/bv-tests.rkt +++ b/turnstile/examples/tests/rosette/bv-tests.rkt @@ -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)))