diff options
Diffstat (limited to 'src/Wasm/Validation/Instructions.agda')
| -rw-r--r-- | src/Wasm/Validation/Instructions.agda | 197 |
1 files changed, 197 insertions, 0 deletions
diff --git a/src/Wasm/Validation/Instructions.agda b/src/Wasm/Validation/Instructions.agda new file mode 100644 index 0000000..7aa9411 --- /dev/null +++ b/src/Wasm/Validation/Instructions.agda @@ -0,0 +1,197 @@ +{-# OPTIONS --without-K --safe #-} + +------------------------------------------------------------------------ +-- 3.3 Instructions + +module Wasm.Validation.Instructions where + +open import Data.Fin using (zero; toℕ) +open import Data.List using (List; []; _∷_; _++_; map) +open import Data.List.Membership.Propositional using (_∈_) +open import Data.List.Relation.Binary.Pointwise using (Pointwise) +open import Data.List.Relation.Unary.All using (All) +open import Data.Maybe using (just; nothing) +open import Data.Nat using (_+_; _^_) renaming (_≤_ to _≤ⁿ_) +open import Data.Product using (_,_; _×_; ∃) +open import Data.Sum using (inj₁; inj₂) +open import Data.Vec.Bounded using (toList) +open import Level using (0ℓ) +open import Relation.Binary using (Rel) +open import Relation.Binary.PropositionalEquality using (_≡_) +open import Wasm.Expression.Instructions +open import Wasm.Expression.Types +open import Wasm.Expression.Utilities using (BitWidth; 32Bit; 64Bit; module BitWidth′) +open import Wasm.Validation.Context +open import Wasm.Validation.Types + +infix 4 _≤_ _⟶_ + +data OpdType : Set where + [_] : ValType → OpdType + ⊥ : OpdType + +record StackType : Set where + constructor _⟶_ + field + from : List OpdType + to : List OpdType + +fromResult : ResultType → List OpdType +fromResult t = map [_] (toList t) + +fromFunc : FuncType → StackType +fromFunc (from ⟶ to) = fromResult from ⟶ fromResult to + +data _≤_ : Rel OpdType 0ℓ where + ⊥≤τ : ∀ {τ} → ⊥ ≤ τ + refl : ∀ {τ τ′} → τ ≡ τ′ → τ ≤ τ′ + +------------------------------------------------------------------------ +-- 3.3.1 Numeric Instructions + +intType : BitWidth → OpdType +intType 32Bit = [ inj₁ i32 ] +intType 64Bit = [ inj₁ i64 ] + +floatType : BitWidth → OpdType +floatType 32Bit = [ inj₁ f32 ] +floatType 64Bit = [ inj₁ f64 ] + +typeOfNum : NumInstr → StackType +typeOfNum (int (ixx w (IntOp.const _))) = [] ⟶ intType w ∷ [] +typeOfNum (int (ixx w (IntOp.iunop _))) = intType w ∷ [] ⟶ intType w ∷ [] +typeOfNum (int (ixx w (IntOp.ibinop _))) = intType w ∷ intType w ∷ [] ⟶ intType w ∷ [] +typeOfNum (int (ixx w (IntOp.itestop _))) = intType w ∷ [] ⟶ [ inj₁ i32 ] ∷ [] +typeOfNum (int (ixx w (IntOp.irelop _))) = intType w ∷ intType w ∷ [] ⟶ [ inj₁ i32 ] ∷ [] +typeOfNum (int (ixx w IntOp.extend8-s)) = intType w ∷ [] ⟶ intType w ∷ [] +typeOfNum (int (ixx w IntOp.extend16-s)) = intType w ∷ [] ⟶ intType w ∷ [] +typeOfNum (int (ixx w (IntOp.trunc-f w′ _))) = floatType w′ ∷ [] ⟶ intType w ∷ [] +typeOfNum (int (ixx w (IntOp.trunc-sat-f w′ _))) = floatType w′ ∷ [] ⟶ intType w ∷ [] +typeOfNum (int (ixx w IntOp.reinterpret-f)) = floatType w ∷ [] ⟶ intType w ∷ [] +typeOfNum (int i64-extend32-s) = [ inj₁ i64 ] ∷ [] ⟶ [ inj₁ i64 ] ∷ [] +typeOfNum (int i32-wrap-i64) = [ inj₁ i64 ] ∷ [] ⟶ [ inj₁ i32 ] ∷ [] +typeOfNum (int (i64-extend-i32 _)) = [ inj₁ i32 ] ∷ [] ⟶ [ inj₁ i64 ] ∷ [] +typeOfNum (float (fxx w (FloatOp.const _))) = [] ⟶ floatType w ∷ [] +typeOfNum (float (fxx w (FloatOp.funop _))) = floatType w ∷ [] ⟶ floatType w ∷ [] +typeOfNum (float (fxx w (FloatOp.fbinop _))) = floatType w ∷ floatType w ∷ [] ⟶ floatType w ∷ [] +typeOfNum (float (fxx w (FloatOp.frelop _))) = floatType w ∷ floatType w ∷ [] ⟶ [ inj₁ i32 ] ∷ [] +typeOfNum (float (fxx w (FloatOp.convert-i w′ _))) = intType w′ ∷ [] ⟶ floatType w ∷ [] +typeOfNum (float (fxx w FloatOp.reinterpret-i)) = intType w ∷ [] ⟶ floatType w ∷ [] +typeOfNum (float f32-demote-f64) = [ inj₁ f64 ] ∷ [] ⟶ [ inj₁ f32 ] ∷ [] +typeOfNum (float f64-promote-f32) = [ inj₁ f32 ] ∷ [] ⟶ [ inj₁ f64 ] ∷ [] + +------------------------------------------------------------------------ +-- 3.3.2 Reference Instructions + +data RefInstrType : Context → RefInstr → StackType → Set where + null : ∀ {C t} → RefInstrType C (null t) ([] ⟶ [ inj₂ t ] ∷ []) + is-null : ∀ {C t} → RefInstrType C is-null ([ inj₂ t ] ∷ [] ⟶ [ inj₁ i32 ] ∷ []) + func : ∀ {C x t} → Context.getFunc C x ≡ just t → x ∈ Context.refs C → RefInstrType C (func x) ([] ⟶ [ inj₂ funcref ] ∷ []) + +------------------------------------------------------------------------ +-- 3.3.3 Parametric Instructions + +data ParametricInstrType : Context → ParametricInstr → StackType → Set where + drop : ∀ {C t} → ParametricInstrType C drop ([ t ] ∷ [] ⟶ []) + select-t : ∀ {C t} → ParametricInstrType C (select (just (t ∷ []))) ([ inj₁ i32 ] ∷ [ t ] ∷ [ t ] ∷ [] ⟶ [ t ] ∷ []) + select-no-t : ∀ {C t} → ParametricInstrType C (select nothing) ([ inj₁ i32 ] ∷ [ inj₁ t ] ∷ [ inj₁ t ] ∷ [] ⟶ [ inj₁ t ] ∷ []) + +------------------------------------------------------------------------ +-- 3.3.4 Variable Instructions + +data VarInstrType : Context → VarInstr → StackType → Set where + local-get : ∀ {C x t} → Context.getLocal C x ≡ just t → VarInstrType C (local-get x) ([] ⟶ [ t ] ∷ []) + local-set : ∀ {C x t} → Context.getLocal C x ≡ just t → VarInstrType C (local-set x) ([ t ] ∷ [] ⟶ []) + local-tee : ∀ {C x t} → Context.getLocal C x ≡ just t → VarInstrType C (local-tee x) ([ t ] ∷ [] ⟶ [ t ] ∷ []) + global-get : ∀ {C x m t} → Context.getGlobal C x ≡ just (m , t) → VarInstrType C (global-get x) ([] ⟶ [ t ] ∷ []) + global-set : ∀ {C x t} → Context.getGlobal C x ≡ just (var , t) → VarInstrType C (global-set x) ([ t ] ∷ [] ⟶ []) + +------------------------------------------------------------------------ +-- 3.3.5 Table Instructions + +data TableInstrType : Context → TableInstr → StackType → Set where + get : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (get x) ([ inj₁ i32 ] ∷ [] ⟶ [ inj₂ t ] ∷ []) + set : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (set x) ([ inj₂ t ] ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + size : ∀ {C x lim,t} → Context.getTable C x ≡ just lim,t → TableInstrType C (size x) ([] ⟶ [ inj₁ i32 ] ∷ []) + grow : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (grow x) ([ inj₁ i32 ] ∷ [ inj₂ t ] ∷ [] ⟶ [ inj₁ i32 ] ∷ []) + fill : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (fill x) ([ inj₁ i32 ] ∷ [ inj₂ t ] ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + copy : ∀ {C x y lim₁ lim₂ t} → Context.getTable C x ≡ just (lim₁ , t) → Context.getTable C y ≡ just (lim₂ , t) → TableInstrType C (copy x y) ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + init : ∀ {C x y lim₁ t} → Context.getTable C x ≡ just (lim₁ , t) → Context.getElem C y ≡ just t → TableInstrType C (init x y) ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + drop : ∀ {C x t} → Context.getElem C x ≡ just t → TableInstrType C (drop x) ([] ⟶ []) + +------------------------------------------------------------------------ +-- 3.3.6 Memory Instructions + +data MemInstrType : Context → MemInstr → StackType → Set where + int-load : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (int (ixx w (IntMem.load arg))) ([ inj₁ i32 ] ∷ [] ⟶ intType w ∷ []) + int-load8 : ∀ {C w s arg lim} → Context.getMem C zero ≡ just lim → MemArg.align arg ≡ zero → MemInstrType C (int (ixx w (IntMem.load8 s arg))) ([ inj₁ i32 ] ∷ [] ⟶ intType w ∷ []) + int-load16 : ∀ {C w s arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 1 → MemInstrType C (int (ixx w (IntMem.load16 s arg))) ([ inj₁ i32 ] ∷ [] ⟶ intType w ∷ []) + int-load32 : ∀ {C s arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 2 → MemInstrType C (int (i64-load32 s arg)) ([ inj₁ i32 ] ∷ [] ⟶ [ inj₁ i64 ] ∷ []) + int-store : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (int (ixx w (IntMem.store arg))) (intType w ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + int-store8 : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → MemArg.align arg ≡ zero → MemInstrType C (int (ixx w (IntMem.store8 arg))) (intType w ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + int-store16 : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 1 → MemInstrType C (int (ixx w (IntMem.store16 arg))) (intType w ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + int-store32 : ∀ {C arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 2 → MemInstrType C (int (i64-store32 arg)) ([ inj₁ i64 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + float-load : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (float (w , (FloatMem.load arg))) ([ inj₁ i32 ] ∷ [] ⟶ floatType w ∷ []) + float-store : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (float (w , (FloatMem.store arg))) ([ inj₁ i32 ] ∷ floatType w ∷ [] ⟶ []) + size : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C size ([] ⟶ [ inj₁ i32 ] ∷ []) + grow : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C grow ([ inj₁ i32 ] ∷ [] ⟶ [ inj₁ i32 ] ∷ []) + fill : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C fill ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + copy : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C copy ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + init : ∀ {C x lim} → Context.getMem C zero ≡ just lim → Context.getData C x ≡ just _ → MemInstrType C (init x) ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ []) + drop : ∀ {C x} → Context.getData C x ≡ just _ → MemInstrType C (drop x) ([] ⟶ []) + +------------------------------------------------------------------------ +-- 3.3.7 Control Instructions + +infix 2 _⊢_∶_ _⊢*_∶_ + +data _⊢_∶_ : Context → Instr → StackType → Set +data _⊢*_∶_ : Context → List Instr → StackType → Set + +data _⊢_∶_ where + num : ∀ {C i} → C ⊢ num i ∶ typeOfNum i + ref : ∀ {C i t} → RefInstrType C i t → C ⊢ ref i ∶ t + parametric : ∀ {C i t} → ParametricInstrType C i t → C ⊢ parametric i ∶ t + var : ∀ {C i t} → VarInstrType C i t → C ⊢ var i ∶ t + table : ∀ {C i t} → TableInstrType C i t → C ⊢ table i ∶ t + mem : ∀ {C i t} → MemInstrType C i t → C ⊢ mem i ∶ t + nop : ∀ {C} → C ⊢ nop ∶ [] ⟶ [] + unreachable : ∀ {C ts₁ ts₂} → C ⊢ unreachable ∶ ts₁ ⟶ ts₂ + block : ∀ {C bt t₁ t₂ is} → blockType C bt ≡ just (t₁ ⟶ t₂) → record C { labels = t₂ ∷ Context.labels C } ⊢* is ∶ fromFunc (t₁ ⟶ t₂) → C ⊢ block bt is ∶ fromFunc (t₁ ⟶ t₂) + loop : ∀ {C bt t₁ t₂ is} → blockType C bt ≡ just (t₁ ⟶ t₂) → record C { labels = t₁ ∷ Context.labels C } ⊢* is ∶ fromFunc (t₁ ⟶ t₂) → C ⊢ block bt is ∶ fromFunc (t₁ ⟶ t₂) + if-else : ∀ {C bt t₁ t₂ is₁ is₂} → blockType C bt ≡ just (t₁ ⟶ t₂) → record C { labels = t₂ ∷ Context.labels C } ⊢* is₁ ∶ fromFunc (t₁ ⟶ t₂) → record C { labels = t₂ ∷ Context.labels C } ⊢* is₂ ∶ fromFunc (t₁ ⟶ t₂) → C ⊢ if-else bt is₁ is₂ ∶ [ inj₁ i32 ] ∷ fromResult t₁ ⟶ fromResult t₂ + br : ∀ {C l t t₁ t₂} → Context.getLabel C l ≡ just t → C ⊢ br l ∶ fromResult t ++ t₁ ⟶ t₂ + br_if : ∀ {C l t} → Context.getLabel C l ≡ just t → C ⊢ br l ∶ [ inj₁ i32 ] ∷ fromResult t ⟶ fromResult t + br_table : ∀ {C ls l t t′ t₁ t₂} → Context.getLabel C l ≡ just t′ → Pointwise _≤_ t (fromResult t′) → All (λ l′ → ∃ λ t′ → Context.getLabel C l′ ≡ just t′ × Pointwise _≤_ t (fromResult t′)) (toList ls) → C ⊢ br-table ls l ∶ t ++ t₁ ⟶ t₂ + return : ∀ {C t t₁ t₂} → Context.return C ≡ just t → C ⊢ return ∶ (fromResult t) ++ t₁ ⟶ t₂ + call : ∀ {C x t} → Context.getFunc C x ≡ just t → C ⊢ call x ∶ fromFunc t + call-indirect : ∀ {C x y lim t₁ t₂} → Context.getTable C x ≡ just (lim , funcref) → Context.getType C y ≡ just (t₁ ⟶ t₂) → C ⊢ call-indirect x y ∶ [ inj₁ i32 ] ∷ fromResult t₁ ⟶ fromResult t₂ + +------------------------------------------------------------------------ +-- 3.3.8 Instruction Sequences + +-- NOTE: fold is in reverse due to nature of lists in Agda. + +data _⊢*_∶_ where + empty : ∀ {C t} → C ⊢* [] ∶ t ⟶ t + step : ∀ {C i is t₀ t₁ t′ t t₃} → Pointwise _≤_ t′ t → C ⊢ i ∶ t ⟶ t₁ → C ⊢* is ∶ (t₁ ++ t₀) ⟶ t₃ → C ⊢* i ∷ is ∶ (t′ ++ t₀) ⟶ t₃ + +------------------------------------------------------------------------ +-- 3.3.9 Expressions + +infix 2 _⊢ᵉ_∶_ _⊢*_const _⊢_const + +_⊢ᵉ_∶_ : Context → Expr → ResultType → Set +C ⊢ᵉ expr ∶ t = ∃ λ t′ → (C ⊢* expr ∶ [] ⟶ t′) × Pointwise _≤_ t′ (fromResult t) + +data _⊢_const : Context → Instr → Set +_⊢*_const : Context → Expr → Set + +data _⊢_const where + int-const : ∀ {C w x} → C ⊢ num (int (ixx w (IntOp.const x))) const + float-const : ∀ {C w x} → C ⊢ num (float (fxx w (FloatOp.const x))) const + ref-null : ∀ {C t} → C ⊢ ref (null t) const + ref-func : ∀ {C x} → C ⊢ ref (func x) const + global-get : ∀ {C x t} → Context.getGlobal C x ≡ just (const , t) → C ⊢ var (global-get x) const + +C ⊢* expr const = All (C ⊢_const) expr |