From aacd555894fb559365774ddfa899656b95205e4e Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 20 Jul 2021 15:10:50 +0100 Subject: Complete Section 2 - Structure. --- src/Wasm/Expression/Instructions.agda | 219 ++++++++++++++++++++++++++++++++++ src/Wasm/Expression/Modules.agda | 128 ++++++++++++++++++++ src/Wasm/Expression/Types.agda | 88 ++++++++++++++ src/Wasm/Expression/Utilities.agda | 51 ++++++++ src/Wasm/Expression/Values.agda | 118 ++++++++++++++++++ 5 files changed, 604 insertions(+) create mode 100644 src/Wasm/Expression/Instructions.agda create mode 100644 src/Wasm/Expression/Modules.agda create mode 100644 src/Wasm/Expression/Types.agda create mode 100644 src/Wasm/Expression/Utilities.agda create mode 100644 src/Wasm/Expression/Values.agda (limited to 'src/Wasm') diff --git a/src/Wasm/Expression/Instructions.agda b/src/Wasm/Expression/Instructions.agda new file mode 100644 index 0000000..6cd006b --- /dev/null +++ b/src/Wasm/Expression/Instructions.agda @@ -0,0 +1,219 @@ +{-# OPTIONS --without-K --safe #-} + +------------------------------------------------------------------------ +-- 2.4 Types + +module Wasm.Expression.Instructions where + +open import Data.List using (List) +open import Data.Maybe using (Maybe) +open import Data.Product using (∃) +open import Data.Sum using (_⊎_) +open import Wasm.Expression.Values using (UnsignedInteger; UninterpretedInteger; Float) +open import Wasm.Expression.Types using (ValType; RefType) +open import Wasm.Expression.Utilities + +------------------------------------------------------------------------ +-- 2.4.1 Numeric Instructions + +module IntOp (w : BitWidth) where + data Unary : Set where + clz : Unary + ctz : Unary + popcnt : Unary + + data Binary : Set where + add : Binary + sub : Binary + mul : Binary + div : Signedness → Binary + rem : Signedness → Binary + and : Binary + or : Binary + xor : Binary + shl : Binary + shr : Signedness → Binary + rotl : Binary + rotr : Binary + + data Test : Set where + eqz : Test + + data Rel : Set where + eq : Rel + ne : Rel + lt : Signedness → Rel + gt : Signedness → Rel + le : Signedness → Rel + ge : Signedness → Rel + + data IntInstr : Set where + const : UninterpretedInteger (BitWidth′.toℕ w) → IntInstr + iunop : Unary → IntInstr + ibinop : Binary → IntInstr + itestop : Test → IntInstr + irelop : Rel → IntInstr + extend8-s : IntInstr + extend16-s : IntInstr + trunc-f : BitWidth → Signedness → IntInstr + trunc-sat-f : BitWidth → Signedness → IntInstr + reinterpret-f : IntInstr + +data IntInstr : Set where + ixx : ∀ w → IntOp.IntInstr w → IntInstr + i64-extend32-s : IntInstr + i32-wrap-i64 : IntInstr + i64-extend-i32 : Signedness → IntInstr + +module FloatOp (w : BitWidth) where + data Unary : Set where + abs : Unary + neg : Unary + sqrt : Unary + ceil : Unary + floor : Unary + trunc : Unary + nearest : Unary + + data Binary : Set where + add : Binary + sub : Binary + mul : Binary + div : Binary + min : Binary + max : Binary + copysign : Binary + + data Rel : Set where + eq : Rel + ne : Rel + lt : Rel + gt : Rel + le : Rel + ge : Rel + + data FloatInstr : Set where + const : Float w → FloatInstr + funop : Unary → FloatInstr + fbinop : Binary → FloatInstr + frelop : Rel → FloatInstr + convert-i : BitWidth → Signedness → FloatInstr + reinterpret-i : FloatInstr + +data FloatInstr : Set where + fxx : ∀ w → FloatOp.FloatInstr w → FloatInstr + f32-demote-f64 : FloatInstr + f64-promote-f32 : FloatInstr + +data NumInstr : Set where + int : IntInstr → NumInstr + float : FloatInstr → NumInstr + +------------------------------------------------------------------------ +-- 2.4.2 Reference Instructions + +data RefInstr : Set where + null : RefType → RefInstr + is-null : RefInstr + func : Indices.FuncIdx → RefInstr + +------------------------------------------------------------------------ +-- 2.4.3 Parametric Instructions + +data ParametricInstr : Set where + drop : ParametricInstr + select : List ValType → ParametricInstr + +------------------------------------------------------------------------ +-- 2.4.4 Variable Instructions + +data VarInstr : Set where + local-get : Indices.LocalIdx → VarInstr + local-set : Indices.LocalIdx → VarInstr + local-tee : Indices.LocalIdx → VarInstr + global-get : Indices.GlobalIdx → VarInstr + global-set : Indices.GlobalIdx → VarInstr + +------------------------------------------------------------------------ +-- 2.4.5 Table Instructions + +data TableInstr : Set where + table-get : Indices.TableIdx → TableInstr + table-set : Indices.TableIdx → TableInstr + table-size : Indices.TableIdx → TableInstr + table-grow : Indices.TableIdx → TableInstr + table-fill : Indices.TableIdx → TableInstr + table-copy : Indices.TableIdx → Indices.TableIdx → TableInstr + table-init : Indices.TableIdx → Indices.ElemIdx → TableInstr + elem-drop : Indices.ElemIdx → TableInstr + +------------------------------------------------------------------------ +-- 2.4.6 Memory Instructions + +record MemArg : Set where + field + offset : UnsignedInteger 32 + align : UnsignedInteger 32 + +module IntMem (w : BitWidth) where + data IntMemInstr : Set where + load : MemArg → IntMemInstr + store : MemArg → IntMemInstr + load8 : Signedness → MemArg → IntMemInstr + load16 : Signedness → MemArg → IntMemInstr + store8 : MemArg → IntMemInstr + store16 : MemArg → IntMemInstr + +data IntMemInstr : Set where + ixx : ∀ w → IntMem.IntMemInstr w → IntMemInstr + i64-load32 : Signedness → MemArg → IntMemInstr + i64-store32 : MemArg → IntMemInstr + +module FloatMem (w : BitWidth) where + data FloatMemInstr : Set where + load : MemArg → FloatMemInstr + store : MemArg → FloatMemInstr + +FloatMemInstr : Set +FloatMemInstr = ∃ FloatMem.FloatMemInstr + +data MemInstr : Set where + int : IntMemInstr → MemInstr + float : FloatMemInstr → MemInstr + size : MemInstr + grow : MemInstr + fill : MemInstr + copy : MemInstr + init : Indices.DataIdx → MemInstr + drop : Indices.DataIdx → MemInstr + +------------------------------------------------------------------------ +-- 2.4.7 Control Instructions + +BlockType : Set +BlockType = Indices.TypeIdx ⊎ Maybe ValType + +data Instr : Set where + num : NumInstr → Instr + ref : RefInstr → Instr + parametric : ParametricInstr → Instr + var : VarInstr → Instr + table : TableInstr → Instr + mem : MemInstr → Instr + nop : Instr + unreachable : Instr + block : BlockType → List Instr → Instr + loop : BlockType → List Instr → Instr + if-else : BlockType → List Instr → List Instr → Instr + br : Indices.LabelIdx → Instr + br-if : Indices.LabelIdx → Instr + br-table : Vec′ Indices.LabelIdx → Indices.LabelIdx → Instr + return : Instr + call : Indices.FuncIdx → Instr + call_indirect : Indices.TableIdx → Indices.TypeIdx → Instr + +------------------------------------------------------------------------ +-- 2.4.8 Expressions + +Expr : Set +Expr = List Instr diff --git a/src/Wasm/Expression/Modules.agda b/src/Wasm/Expression/Modules.agda new file mode 100644 index 0000000..912d6da --- /dev/null +++ b/src/Wasm/Expression/Modules.agda @@ -0,0 +1,128 @@ +{-# OPTIONS --without-K --safe #-} + +------------------------------------------------------------------------ +-- 2.5 Modules + +module Wasm.Expression.Modules where + +open import Data.Maybe using (Maybe) +open import Wasm.Expression.Types +open import Wasm.Expression.Utilities using (Vec′; module Indices) +open import Wasm.Expression.Values using (Byte; Name) +open import Wasm.Expression.Instructions using (Expr) + +------------------------------------------------------------------------ +-- 2.5.1 Indices + +-- NOTE: defined in Wasm.Expression.Utilities + +------------------------------------------------------------------------ +-- 2.5.2 Types + +-- NOTE: no new definitions + +------------------------------------------------------------------------ +-- 2.5.3 Functions + +record Func : Set where + field + type : Indices.TypeIdx + locals : Vec′ ValType + body : Expr + +------------------------------------------------------------------------ +-- 2.5.4 Tables + +Table : Set +Table = TableType + +------------------------------------------------------------------------ +-- 2.5.5 Memories + +Mem : Set +Mem = MemType + +------------------------------------------------------------------------ +-- 2.5.6 Globals + +record Global : Set where + field + type : GlobalType + init : Expr + +------------------------------------------------------------------------ +-- 2.5.7 Element Segments + +data ElemMode : Set where + passive : ElemMode + active : (table : Indices.TableIdx) → (offset : Expr) → ElemMode + declarative : ElemMode + +record Elem : Set where + field + type : RefType + init : Vec′ Expr + mode : ElemMode + +------------------------------------------------------------------------ +-- 2.5.8 Data Segments + +data DataMode : Set where + passive : DataMode + active : (memory : Indices.MemIdx) → (offset : Expr) → DataMode + +record Data : Set where + field + init : Vec′ Byte + mode : DataMode + +------------------------------------------------------------------------ +-- 2.5.9 Start Function + +Start : Set +Start = Indices.FuncIdx + +------------------------------------------------------------------------ +-- 2.5.10 Exports + +data ExportDesc : Set where + func : Indices.FuncIdx → ExportDesc + table : Indices.TableIdx → ExportDesc + mem : Indices.MemIdx → ExportDesc + global : Indices.GlobalIdx → ExportDesc + +record Export : Set where + field + name : Name + desc : ExportDesc + +------------------------------------------------------------------------ +-- 2.5.11 Imports + +data ImportDesc : Set where + func : Indices.TypeIdx → ImportDesc + table : TableType → ImportDesc + mem : MemType → ImportDesc + global : GlobalType → ImportDesc + +record Import : Set where + field + mod : Name + name : Name + desc : ImportDesc + +------------------------------------------------------------------------ +-- Module definition + +record Mod : Set where + field + types : Vec′ FuncType + funcs : Vec′ Func + tables : Vec′ Table + mems : Vec′ Mem + globals : Vec′ Global + elems : Vec′ Elem + datas : Vec′ Data + start : Maybe Start + imports : Vec′ Import + exports : Vec′ Export diff --git a/src/Wasm/Expression/Types.agda b/src/Wasm/Expression/Types.agda new file mode 100644 index 0000000..f72df93 --- /dev/null +++ b/src/Wasm/Expression/Types.agda @@ -0,0 +1,88 @@ +{-# OPTIONS --without-K --safe #-} + +------------------------------------------------------------------------ +-- 2.3 Types + +module Wasm.Expression.Types where + +open import Data.Maybe using (Maybe) +open import Data.Product using (_×_) +open import Data.Sum using (_⊎_) +open import Wasm.Expression.Values using (UnsignedInteger) +open import Wasm.Expression.Utilities using (Vec′) + +------------------------------------------------------------------------ +-- 2.3.1 Number Types + +data NumType : Set where + i32 : NumType + i64 : NumType + f32 : NumType + f64 : NumType + +------------------------------------------------------------------------ +-- 2.3.2 Reference Types + +data RefType : Set where + funcref : RefType + externref : RefType + +------------------------------------------------------------------------ +-- 2.3.3 Value Types + +ValType : Set +ValType = NumType ⊎ RefType + +------------------------------------------------------------------------ +-- 2.3.4 Result Types + +ResultType : Set +ResultType = Vec′ ValType + +------------------------------------------------------------------------ +-- 2.3.5 Function Types + +record FuncType : Set where + constructor _⟶_ + field + from : ResultType + to : ResultType + +------------------------------------------------------------------------ +-- 2.3.6 Limits + +record Limits : Set where + field + min : UnsignedInteger 32 + max : Maybe (UnsignedInteger 32) + +------------------------------------------------------------------------ +-- 2.3.7 Memory Types + +MemType : Set +MemType = Limits + +------------------------------------------------------------------------ +-- 2.3.8 Table Types + +TableType : Set +TableType = Limits × RefType + +------------------------------------------------------------------------ +-- 2.3.9 Global Types + +data Mut : Set where + const : Mut + var : Mut + +GlobalType : Set +GlobalType = Mut × ValType + +------------------------------------------------------------------------ +-- 2.3.10 External Types + +data ExternType : Set where + func : FuncType → ExternType + table : TableType → ExternType + mem : MemType → ExternType + global : GlobalType → ExternType diff --git a/src/Wasm/Expression/Utilities.agda b/src/Wasm/Expression/Utilities.agda new file mode 100644 index 0000000..b7f9af4 --- /dev/null +++ b/src/Wasm/Expression/Utilities.agda @@ -0,0 +1,51 @@ +{-# OPTIONS --without-K --safe #-} + +module Wasm.Expression.Utilities where + +open import Data.Fin using (Fin) +open import Data.Nat using (ℕ; _^_) +open import Data.Vec.Bounded using (Vec≤) + +Vec′ : ∀ {a} → Set a → Set a +Vec′ A = Vec≤ A (2 ^ 32) + +data Signedness : Set where + Signed : Signedness + Unsigned : Signedness + +data BitWidth : Set where + 32Bit : BitWidth + 64Bit : BitWidth + +module BitWidth′ where + toℕ : BitWidth → ℕ + toℕ 32Bit = 32 + toℕ 64Bit = 64 + +module Indices where + TypeIdx : Set + TypeIdx = Fin (2 ^ 32) + + FuncIdx : Set + FuncIdx = Fin (2 ^ 32) + + TableIdx : Set + TableIdx = Fin (2 ^ 32) + + MemIdx : Set + MemIdx = Fin (2 ^ 32) + + GlobalIdx : Set + GlobalIdx = Fin (2 ^ 32) + + ElemIdx : Set + ElemIdx = Fin (2 ^ 32) + + DataIdx : Set + DataIdx = Fin (2 ^ 32) + + LocalIdx : Set + LocalIdx = Fin (2 ^ 32) + + LabelIdx : Set + LabelIdx = Fin (2 ^ 32) diff --git a/src/Wasm/Expression/Values.agda b/src/Wasm/Expression/Values.agda new file mode 100644 index 0000000..d6bce60 --- /dev/null +++ b/src/Wasm/Expression/Values.agda @@ -0,0 +1,118 @@ +{-# OPTIONS --without-K --safe #-} + +------------------------------------------------------------------------ +-- 2.2 Values + +module Wasm.Expression.Values where + +open import Data.Char using (Char; toℕ) +open import Data.Empty using (⊥) +open import Data.Fin using (Fin) +open import Data.Nat using (ℕ; zero; suc; _^_; pred) +open import Wasm.Expression.Utilities using (BitWidth; 32Bit; 64Bit) + +infix 8 +_ -_ + +------------------------------------------------------------------------ +-- 2.2.1 Bytes + +Byte : Set +Byte = Fin 256 + +------------------------------------------------------------------------ +-- 2.2.2 Integers + +UnsignedInteger : ℕ → Set +UnsignedInteger n = Fin (2 ^ n) + +data SignedInteger : ℕ → Set where + +_ : ∀ {n} → Fin n → SignedInteger (suc n) + -[1+_] : ∀ {n} → Fin n → SignedInteger (suc n) + +UninterpretedInteger : ℕ → Set +UninterpretedInteger = UnsignedInteger + +------------------------------------------------------------------------ +-- 2.2.3 Floating-Point + +signif : BitWidth → ℕ +signif 32Bit = 23 +signif 64Bit = 52 + +expon : BitWidth → ℕ +expon 32Bit = 8 +expon 64Bit = 11 + +data FloatMag : BitWidth → Set where + nan : ∀ {w} → (n : Fin (pred (2 ^ (signif w)))) → FloatMag w + ∞ : ∀ {w} → FloatMag w + normal : ∀ {w} → (e : Fin (pred (pred (2 ^ (expon w))))) → (t : Fin (2 ^ (signif w))) → FloatMag w + subnormal : ∀ {w} → (t : Fin (pred (2 ^ (signif w)))) → FloatMag w + zero : ∀ {w} → FloatMag w + +data Float : BitWidth → Set where + +_ : ∀ {w} → FloatMag w → Float w + -_ : ∀ {w} → FloatMag w → Float w + +------------------------------------------------------------------------ +-- 2.2.4 Names + +module _ where + open import Data.Bool using (Bool; true; false; if_then_else_) + open import Data.List using (List; []; _∷_; length; map; sum) + open import Data.Nat using (_≤ᵇ_; _<_; z≤n; s≤s) + open import Data.Nat.Properties using (≤-step) + open import Data.Product using (_×_; _,_; proj₂; map₂) + open import Data.String using (String; toList) + + halfEven? : ℕ → Bool × ℕ + halfEven? zero = true , 0 + halfEven? (suc zero) = false , 0 + halfEven? (suc (suc n)) = map₂ suc (halfEven? n) + + n≢0⇒halfEven?