IndexTypes.rkt

#lang racket

(require redex/reduction-semantics "WASM-Redex/Syntax.rkt")

(provide WASMIndexTypes)

(define-extended-language WASMIndexTypes WASM
  (ibinop ::= .... div-u/unsafe div-s/unsafe rem-u/unsafe rem-s/unsafe)
  
  (e ::= .... (call-indirect/unsafe tfiann)
     (t load/unsafe a o) (t load/unsafe (tp sx) a o)
     (t store/unsafe a o) (t store/unsafe tp a o)
     (if tf (e ...) else (e ...)) (block tf (e ...)) (loop tf (e ...)))

  ;; Index language
  (ivar ::= variable-not-otherwise-mentioned)
  (x y ::= ivar (t c) ((t binop) x y) ((t testop) x) ((t relop) x y) ((t cvtop t) x) ((t cvtop t sx) x))
  (P ::= (= x y) (if P P P) (not P) (and P P) (or P P) (valid-address ivar o n n) ⊥)
  (φ ::= empty (φ P))
  (Γ ::= empty (Γ ti))
  (ti ::= (t ivar))

  ;; Instruction index types
  (locals ::= (ti ...))
  ;; Index-type pre/post-condition: types on stack, locals, and constraint context
  (ticond ::= ((ti ...) locals Γ φ))
  (labelty ::= ((ti ...) locals φ))
  (retty ::= ((ti ...) φ))
  ;; Function annotation
  (tfiann ::= (retty -> retty))
  (tfi ::= (ticond -> ticond))

  ;; Indexed module contexts
  (C ::= ((func tfiann ...) (global tg ...) (table (j tfiann ...)) (memory j) (local t ...) (label labelty  ...) (return retty))
     ((func tfiann ...) (global tg ...) (table (j tfiann ...)) (memory j) (local t ...) (label labelty ...) (return))
     ((func tfiann ...) (global tg ...) (table (j tfiann ...)) (memory) (local t ...) (label labelty  ...) (return retty))
     ((func tfiann ...) (global tg ...) (table (j tfiann ...)) (memory) (local t ...) (label labelty ...) (return))
     ((func tfiann ...) (global tg ...) (table) (memory j) (local t ...) (label labelty  ...) (return retty))
     ((func tfiann ...) (global tg ...) (table) (memory j) (local t ...) (label labelty ...) (return))
     ((func tfiann ...) (global tg ...) (table) (memory) (local t ...) (label labelty  ...) (return retty))
     ((func tfiann ...) (global tg ...) (table) (memory) (local t ...) (label labelty ...) (return)))

  (S ::= ((C ...) (table ((j (tfiann ...)) ...)) (memory (j ...))))

  ;; Module-level indexed declarations
  (f ::= ((ex ...) (func tfiann (local (t ...) (e ...))))
     ((ex ...) (func tfiann im)))
  (glob ::= ((ex ...) (global tg (e ...)))
        ((ex ...) (global tg im)))
  (tab ::= ((ex ...) (table n i ...))
       ((ex ...) (table n im tfi ...)))
  (mem ::= ((ex ...) (memory n))
       ((ex ...) (memory n im)))
  (im ::= (import string string))
  (ex ::= (export string))
  (mod ::= (module (f ...) (glob ...) (tab ...) (mem ...))))