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 ++++++++++++++++++++++++++++++++++ 1 file changed, 219 insertions(+) create mode 100644 src/Wasm/Expression/Instructions.agda (limited to 'src/Wasm/Expression/Instructions.agda') 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 -- cgit v1.2.3