atgeller/WASM-Redex

Modeling foreign functions

Opened this issue · 0 comments

To represent external functions: Introduce a new cl production rule (host_func tf any).

To wrap and embed external functions: Have a macro to construct
(define/contract (f store x_1 ...) (-> ((redex-match? WASM-Admin s _) (wasm->racket t_t ...)) (((redex-match? WASM-Admin s store _) (wasm->racket t_2 ...))) (x s x_1 ...))
from x, where (-> (t_1 ...) (t_2 ...)) is the expected type x is imported under, wasm->racket turns i32 into integer32?, etc....

Store this in the table as (term (host_func (-> (t_1 ...) (t_2 ...)) ,f)), Then at run-time eval f with the current store and values from the stack based on annotation from closure, then return the (possibly updated) store and result values.