Implemented a Racket FFI

Semantics/AdministrativeSyntax.rkt

@@ -13,7 +13,9 @@
   (L ::= hole (v ... (label n (e ...) L) e ...))
 
   (s ::= ((inst ...) (tabinst ...) (meminst ...)))
-  (cl ::= (i (func tf (local (t ...) (e ...)))))
+  (cl ::= (i (func tf (local (t ...) (e ...))))
+      (host-func tf (side-condition any_1 (procedure? (term any_1))))
+      uninit)
   (inst ::= ((cl ...) (v ...) (i ...) (i ...)))
 
   (tabinst ::= (cl ...))

Semantics/Instantiation.rkt

@@ -0,0 +1,137 @@
+#lang racket
+
+(require redex/reduction-semantics
+         "RacketFFI.rkt"
+         "Semantics.rkt")
+
+(provide empty-store wasm-instantiate)
+
+(define empty-store (term (() () ())))
+
+;; s (listof (WASM mod)) import-dict -> s export-dict
+;; takes a WASM module, a start function name, and returns a store and a list of exports
+(define (wasm-instantiate s mod imports)
+
+  (define (lookup-import ns name)
+    (dict-ref (dict-ref imports
+                        ns
+                        (thunk (error (format "Link error: namespace ~a not in imports" ns)))
+              name
+              (thunk (error (format "Link error: imported object ~a not in namespace ~a" name ns))))))
+
+  (define (create-exports exs obj)
+    (map (λ (ex)
+           (match-let ([`(export ,name) ex])
+             (cons name obj)))
+         exs))
+
+  (match-let ([`(,insts ,tabinsts ,meminsts) s]
+              [`(module ,fs ,globs ,tab? ,mem?) mod])
+    (let ([inst-num (length insts)])
+
+      (define (instantiate-funcs fs (i 0))
+        (if (empty? fs)
+            (values '() '())
+            (let-values ([(cl cl-exs)
+                          (match (first fs)
+                            [`(,exs (func ,tf (import ,ns ,name)))
+                             (values (match (lookup-import ns name)
+                                       [(? procedure? proc)
+                                        (term (host-func ,tf ,proc))]
+                                       [(wasm-func import-inst import-index)
+                                        ;; lookup the cl from the previous store
+                                        (match-let ([`(,s-cls ,_ ,_ ,_) (list-ref insts import-inst)])
+                                          (list-ref s-cls import-index))]
+                                       [_ (error "Link error: imported object is not a function")])
+                                     exs)]
+                            [`(,exs (func ,tf (local ,ts ,es)))
+                             (values (term (,inst-num (func ,tf (local ,ts ,es)))) exs)])]
+
+                         [(cls exports) (instantiate-funcs (rest fs) (add1 i))])
+
+              (values (cons cl cls)
+                      (append (create-exports cl-exs (wasm-func inst-num i)) exports)))))
+
+      (define (instantiate-globs globs (i 0) (vs '()) (exports '()))
+        (if (empty? globs)
+            (values vs exports)
+            (let-values ([(vs-new v-exs)
+                          (match (first globs)
+                            [`(,exs (global (,_ ,t) (import ,ns ,name)))
+                             (values (match (lookup-import ns name)
+                                       [(? real? num)
+                                        (term (,t const ,(coerce-value t num)))]
+                                       [(wasm-global import-inst import-index)
+                                        ;; lookup the v from the previous store
+                                        (match-let ([`(,_ ,s-vs ,_ ,_) (list-ref insts import-inst)])
+                                          (list-ref s-vs import-index))]
+                                       [_ (error "Link error: imported object is not a global variable")])
+                                     exs)]
+                            [`(,exs (global ,_ ,es))
+                             (match-let ([`(((((() ,vs-new () ())) () ()) () (,v)))
+                                          (apply-reduction-relation*
+                                           (-> 0)
+                                           (term ((((() ,vs () ())) () ()) () ,es)))])
+                               (if (equal? v 'trap)
+                                   (error "Evaluating global initial value trapped")
+                                   (values (append vs-new (list v)) exs)))])])
+              (instantiate-globs
+               (rest globs)
+               (add1 i)
+               vs-new
+               (append exports (create-exports v-exs (wasm-global inst-num i)))))))
+
+      (define (instantiate-tab tab? cls)
+        (if (empty? tab?)
+            (values '() '() '())
+            (let-values ([(index tabinst tab-exs)
+                          (match (first tab?)
+                            [`(,exs (table ,n (import ,ns ,name)))
+                             (values (match (lookup-import ns name)
+                                       [(wasm-table import-index)
+                                        (unless (<= n (length (list-ref tabinsts import-index)))
+                                          (error "Link error: imported table does not have the right length"))
+                                        import-index]
+                                       [_ (error "Link error: imported object is not a table")])
+                                     '()
+                                     exs)]
+                            [`(,exs (table ,n ,is ...))
+                             (values (length tabinsts)
+                                     (map (curry list-ref cls) is)
+                                     exs)])])
+              (values (list index)
+                      (list tabinst)
+                      (create-exports tab-exs (wasm-table index))))))
+
+      (define (instantiate-mem mem?)
+        (if (empty? mem?)
+            (values '() '() '())
+            (let-values ([(index meminst mem-exs)
+                          (match (first mem?)
+                            [`(,exs (memory ,n (import ,ns ,name)))
+                             (values (match (lookup-import ns name)
+                                       [(wasm-memory import-index)
+                                        (unless (<= (* n (memory-page-size)) (bytes-length (list-ref meminsts import-index)))
+                                          (error "Link error: imported memory does not have the right length"))
+                                        import-index]
+                                       [_ (error "Link error: imported object is not a memory")])
+                                     '()
+                                     exs)]
+                            [`(,exs (memory ,n))
+                             (values (length meminsts)
+                                     (make-bytes (* n (memory-page-size)) 0)
+                                     exs)])])
+              (values (list index)
+                      (list meminst)
+                      (create-exports mem-exs (wasm-memory index))))))
+
+      (let*-values ([(cls fs-exports) (instantiate-funcs fs)]
+                    [(vs globs-exports) (instantiate-globs globs)]
+                    [(tab-index mod-tabinsts tab-exports) (instantiate-tab tab? cls)]
+                    [(mem-index mod-meminsts mem-exports) (instantiate-mem mem?)]
+                    [(inst) (term (,cls ,vs ,tab-index ,mem-index))])
+
+        (values (term (,(append insts (list inst))
+                       ,(append tabinsts mod-tabinsts)
+                       ,(append meminsts mod-meminsts)))
+                (append fs-exports globs-exports tab-exports mem-exports))))))

Semantics/RacketFFI.rkt

@@ -0,0 +1,159 @@
+#lang racket
+
+(require racket/flonum
+         redex/reduction-semantics
+         "AdministrativeSyntax.rkt"
+         "../Utilities.rkt"
+         "StoreUtilities.rkt"
+         "SizedOps.rkt")
+
+(provide racket-trampoline
+         memory-page-size
+         wasm-grow-memory
+         wasm-mem-read-integer
+         wasm-mem-write-integer!
+         wasm-grow-table!
+         wasm-table-get
+         wasm-table-set!
+         wasm-lookup-export
+
+         coerce-value
+
+         ;; These structs are provided so instantiation can use them,
+         ;; but they should not be constructed by ffi functions
+         (struct-out wasm-memory)
+         (struct-out wasm-table)
+         (struct-out wasm-func)
+         (struct-out wasm-global))
+
+
+(define memory-page-size (make-parameter 65536))
+
+;; these parameters are set when calling racket ffi procedures as the getter/setter for the wasm store
+(define get-store (make-parameter #f))
+(define set-store! (make-parameter #f))
+
+(define wasm-exports (make-parameter #f))
+
+(struct wasm-memory (index))
+
+;; wasm-memory natural -> void
+(define (wasm-grow-memory mem n)
+  (let ([i (wasm-memory-index mem)])
+    (match-let ([`(,insts ,tabinsts ,meminsts) ((get-store))])
+      ((set-store!) (term (,insts ,tabinsts (with-index ,meminsts ,i ,(bytes-append (list-ref meminsts i) (make-bytes (* (memory-page-size) n) 0)))))))))
+
+;; wasm-memory natural natural boolean -> integer
+(define (wasm-mem-read-integer mem offset width signed?)
+  (unless (or (= width 1) (= width 2) (= width 4) (= width 8))
+    (error "Integer width must be one of 1, 2, 4, 8"))
+  (match-let ([`(,_ ,_ ,meminsts) ((get-store))])
+    (let ([mem-bytes (list-ref meminsts (wasm-memory-index mem))])
+      (integer-bytes->integer mem-bytes signed? #f offset (+ offset width)))))
+
+;; wasm-memory natural natural integer -> void
+(define (wasm-mem-write-integer! mem offset width value)
+  (unless (or (= width 1) (= width 2) (= width 4) (= width 8))
+    (error "Integer width must be one of 1, 2, 4, 8"))
+  (match-let ([`(,insts ,tabinsts ,meminsts) ((get-store))])
+    (let* ([i (wasm-memory-index mem)]
+           [mem-bytes (bytes-copy (list-ref meminsts i))])
+      ((set-store!) (term (,insts ,tabinsts (with-index ,meminsts ,i ,(integer->integer-bytes value width (< value 0) #f mem-bytes offset))))))))
+
+(struct wasm-table (index))
+
+;; wasm-table natural -> void
+(define (wasm-grow-table! table n)
+  (let ([i (wasm-table-index table)])
+    (match-let ([`(,insts ,tabinsts ,meminsts) ((get-store))])
+      ((set-store!) (term (,insts (with-index ,tabinsts ,i ,(append (list-ref tabinsts i) (build-list n (λ (_) (term uninit))))) ,meminsts))))))
+
+;; wasm-table natural -> cl
+(define (wasm-table-get table n)
+  (let ([i (wasm-table-index table)])
+    (match-let ([`(,insts ,tabinsts ,meminsts) ((get-store))])
+      (list-ref (list-ref tabinsts i) n))))
+
+(struct wasm-func (inst index))
+
+;; wasm-table natural (or/c wasm-func 'uninit) -> void
+(define (wasm-table-set! table n func)
+  (unless (or (wasm-func? func) (equal? func 'uninit))
+    (error "Table entry must be an exported function or 'uninit"))
+  (let* ([i (wasm-table-index table)]
+         [s ((get-store))]
+         [cl (if (wasm-func? func)
+                 (term (store-func ,s ,(wasm-func-inst func) ,(wasm-func-index func)))
+                 'uninit)])
+    (match-let ([`(,insts ,tabinsts ,meminsts) s])
+      ((set-store!) (term (,insts (with-index ,tabinsts ,i (with-index ,(list-ref tabinsts i) n cl)) ,meminsts))))))
+
+
+;; wasm-func . args -> e e
+#;(define (wasm-func-call func . args)
+  ; need to change trampoline code to return es, then produce a local call and foreign call with the continuation
+  'TODO)
+
+(struct wasm-global (inst index))
+
+;; wasm-global real -> void
+;; commented out since you can't export mutable globals with the current WASM version modelled
+#;(define (wasm-set-global! global v)
+  (let ([inst (wasm-global-inst global)]
+        [i (wasm-global-index global)])
+    (match-let* ([`(,insts ,tabinsts ,meminsts) ((get-store))]
+                 [`(,cls ,globs ,tab ,mem) (list-ref insts inst)]
+                 [`(,t const ,_) (list-ref globs i)])
+      ((set-store!) (term ((with-index ,insts ,inst
+                             (,cls (with-index ,globs ,i (,t const ,(coerce-value t v))) ,tab ,mem))
+                           ,tabinsts
+                           ,meminsts))))))
+
+;; wasm-global -> real
+(define (wasm-get-global global)
+  (match-let* ([`(,insts ,_ ,_) ((get-store))]
+               [`(,_ ,globs ,_ ,_) (list-ref insts (wasm-global-inst global))]
+               [`(,_ const ,v) (list-ref globs (wasm-global-index global))])
+    v))
+
+
+;; Exports are assumed to be valid
+(define (wasm-lookup-export name)
+  (dict-ref (wasm-exports) name))
+
+(define (racket-trampoline post exports proc s args)
+  (let* ([s-box (box s)]
+         [ret-vals (filter (λ (rv) (not (void? rv)))
+                           (call-with-values (thunk
+                                              (parameterize ([get-store (λ () (unbox s-box))]
+                                                             [set-store! (λ (s-new) (set-box! s-box s-new))]
+                                                             [wasm-exports exports])
+                                                (apply proc args)))
+                                             list))])
+    (unless (= (length post) (length ret-vals))
+      (error "Racket procedure produced an incorrect number of values"))
+
+    (term (,(unbox s-box) ,(map coerce-value post ret-vals)))))
+
+(define (coerce-value t n)
+  (unless (real? n)
+    (error "Cannot coerce a non-real value"))
+  (match t
+    ['i32
+     (unless (exact? n)
+       (error "Cannot coerce an inexact to an i32"))
+     (unless (<= (- (expt 2 31)) n (sub1 (expt 2 32)))
+       (error "Value outside of i32 range"))
+     (to-unsigned-sized 32 n)]
+
+    ['i64
+     (unless (exact? n)
+       (error "Cannot coerce an inexact to an i64"))
+     (unless (<= (- (expt 2 63)) n (sub1 (expt 2 64)))
+       (error "Value outside of i64 range"))
+     (to-unsigned-sized 64 n)]
+
+    ['f32 (flsingle (real->double-flonum n))]
+
+    ['f64 (real->double-flonum n)]))
+

Semantics/Semantics.rkt

@@ -6,16 +6,15 @@
          "Utilities.rkt"
          "SimpleOps.rkt"
          "StoreUtilities.rkt"
-         "ConstUtilities.rkt")
+         "ConstUtilities.rkt"
+         "RacketFFI.rkt")
 
 (provide -> memory-page-size)
 
-(define memory-page-size (make-parameter 65536))
-
 ;; TL;DR about stack: the stack is implicit in the stream of instructions being processed.
 ;; This is because v \subset e, so although we say (e ...) it ends up looking like (v ... e ...).
 ;; Thus, the next instruction to execute is the head of e ..., and the stack is v ...
-(define (-> i)
+(define (-> i (exports '()))
   (reduction-relation
    WASM-Admin
    #:domain (s (v ...) (e ...))
@@ -157,7 +156,7 @@
 
    (c-> (s (v_l ...) (in-hole L (v_0 ... (i32 const j) (call-indirect tf) e_0 ...)))
         (s (v_l ...) (in-hole L (v_0 ... (call (store-tab s ,i j)) e_0 ...)))
-        (where (func tf (local (t ...) (e ...))) (cl-code-opt (store-tab s ,i j))))
+        (where (func tf _) (cl-code-opt (store-tab s ,i j))))
 
    (c-> (s (v_l ...) (in-hole L (v_0 ... (i32 const j) (call-indirect tf) e_0 ...)))
         (s (v_l ...) (in-hole L (v_0 ... trap e_0 ...)))
@@ -178,6 +177,12 @@
         (side-condition (= (length (term (v ...))) (length (term (t_1 ...)))))
         (where m ,(length (term (t_2 ...)))))
 
+   ;; Foreign function calls
+   (c-> (s (v_l ...) (in-hole L (v_0 ... (t_1 const c_1) ... (call cl) e_0 ...)))
+        (s_new (v_l ...) (in-hole L (v_0 ... (t_2 const c_2) ... e_0 ...)))
+        (where (host-func ((t_1 ...) -> (t_2 ...)) (name proc any)) cl)
+        (where (s_new (c_2 ...)) ,(racket-trampoline (term (t_2 ...)) exports (term proc) (term s) (term (c_1 ...)))))
+
    ;; Stuff inside functions calls!
    (c-> (s (v_l ...) (in-hole L (v_0 ... (local n (j (v_1 ...)) (v ...)) e_0 ...)))
         (s (v_l ...) (in-hole L (v_0 ... v ... e_0 ...)))

Semantics/StoreUtilities.rkt

@@ -9,9 +9,11 @@
 ; closure accessors
 ;; implements cl_code
 (define-metafunction WASM-Admin
-  cl-code : cl -> (func tf (local (t ...) (e ...)))
+  cl-code : cl -> any
   [(cl-code (i (func tf (local (t ...) (e ...)))))
-   (func tf (local (t ...) (e ...)))])
+   (func tf (local (t ...) (e ...)))]
+  ;; all other cl cases are undefined
+  [(cl-code _) #f])
 
 ;; returns the cl_code field if the input is a well-defined cl
 ;; otherwise returns #f