blob: 68f4219ca4d372c82240ca7f556ff4e97fdcc5ce (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
|
{-# OPTIONS --safe --without-K #-}
module Wasm.Semantics
{a} (ExternAddr : Set a)
where
open import Data.Fin using (Fin; zero; toℕ; inject≤)
open import Data.List using (List; []; _∷_; _++_; length; lookup; allFin)
open import Data.List.Relation.Unary.Linked using (Linked)
open import Data.Maybe using (Maybe; maybe; map)
open import Data.Nat using (ℕ; _≤_; _≥?_; _≤?_)
open import Data.Product using (_×_; ∃; ∃₂; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_)
open import Data.Unit using (⊤)
open import Data.Vec as Vec using (Vec)
open import Level using () renaming (suc to ℓsuc)
open import Relation.Binary using (REL)
open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst; module ≡-Reasoning)
open import Relation.Nary using (substₙ)
open import Relation.Nullary.Decidable using (True)
open import Wasm.Data
open import Wasm.Type hiding (_,_)
open import Wasm.Util.List.Map as Map using (Map)
open import Wasm.Util.List.Prefix as Prefix using (Prefix; length≤) renaming (Map to PrefixMap)
open import Wasm.Value
open import Wasm.Data.Instruction as Inst using ()
record StoreTypes : Set₁ where
field
hostFuncs : List FuncType
funcs : List FuncType
tables : List TableType
mems : List MemType
globals : List GlobalType
elems : List RefType
datas : ℕ
data Num : NumType → Set where
i32 : I32 → Num i32
i64 : I64 → Num i64
f32 : F32 → Num f32
f64 : F64 → Num f64
data Ref (S : StoreTypes) : RefType → Set a where
null : ∀ τ → Ref S τ
func : Fin (length (StoreTypes.funcs S)) → Ref S funcref
extern : ExternAddr → Ref S externref
data Value (S : StoreTypes) : ValType → Set a where
num : ∀ {τ} → Num τ → Value S (num τ)
ref : ∀ {τ} → Ref S τ → Value S (ref τ)
default : ∀ {S} τ → Value S τ
default (num i32) = num (i32 zero)
default (num i64) = num (i64 zero)
default (num f32) = num (f32 0f32)
default (num f64) = num (f64 0f64)
default (ref τ) = ref (null τ)
data Result (S : StoreTypes) : List ValType → Set a where
[_] : ∀ {τs} → Map (Value S) τs → Result S τs
trap : ∀ {τs} → Result S τs
record ExportsInst (S : StoreTypes) (Cₑ : ExternTypes) : Set where
private
module S = StoreTypes S
module Cₑ = ExternTypes Cₑ
field
funcs : Map (λ τ → ∃ λ i → lookup S.funcs i ≡ τ) Cₑ.funcs
tables : Map (λ τ → ∃ λ i → lookup S.tables i ≡ τ) Cₑ.tables
mems : Map (λ τ → ∃ λ i → lookup S.mems i ≡ τ) Cₑ.mems
globals : Map (λ τ → ∃ λ i → lookup S.globals i ≡ τ) Cₑ.globals
record ModuleInst (S : StoreTypes) (C : Inst.Context) : Set₁ where
private
module S = StoreTypes S
module C = Inst.Context C
field
{et} : ExternTypes
funcs : Map (λ τ → ∃ λ i → lookup S.funcs i ≡ τ) C.funcs
tables : Map (λ τ → ∃ λ i → lookup S.tables i ≡ τ) C.tables
mems : Map (λ τ → ∃ λ i → lookup S.mems i ≡ τ) C.mems
globals : Map (λ τ → ∃ λ i → lookup S.globals i ≡ τ) C.globals
elems : Map (λ τ → ∃ λ i → lookup S.elems i ≡ τ) C.elems
datas : Vec (Fin S.datas) C.datas
exports : ExportsInst S et
record TableInst (S : StoreTypes) (τ : TableType) : Set a where
private
module τ = TableType τ
field
elems : List (Ref S τ.type)
{minBound} : True (length elems ≥? toℕ (Limits.min′ τ.limits))
{maxBound} : maybe (λ max → True (length elems ≤? toℕ max)) ⊤ (Limits.max τ.limits)
record MemInst (τ : MemType) : Set where
private
module τ = MemType τ
field
pages : List (Vec Byte 65536)
{minBound} : True (length pages ≥? toℕ (Limits.min′ τ.limits))
{maxBound} : maybe (λ max → True (length pages ≤? toℕ max)) ⊤ (Limits.max τ.limits)
record WasmFuncInst (S : StoreTypes) (τ : FuncType) : Set₁ where
field
{context} : Inst.Context
modinst : ModuleInst S context
code : Function context τ
data FunctionInst (S : StoreTypes) (τ : FuncType) : Set₁ where
host : ∀ {i} → lookup (StoreTypes.hostFuncs S) i ≡ τ → FunctionInst S τ
wasm : WasmFuncInst S τ → FunctionInst S τ
record Store (types : StoreTypes) : Set (ℓsuc a) where
inductive
private
module types = StoreTypes types
field
funcs : Map (FunctionInst types) types.funcs
tables : Map (TableInst types) types.tables
mems : Map MemInst types.mems
globals : Map (λ g → Value types (GlobalType.type g)) types.globals
elems : Map (λ τ → List (Ref types τ)) types.elems
datas : Vec (List Byte) types.datas
data FrameInstruction (C : Inst.Context) : (stackTy labelTy : List (List ValType)) (τ : FuncType) → Set where
[_] : ∀ {τ₁ τ₂ τ₃} → Inst.Sequence (record C {labels = []}) (τ₂ ++ τ₁ ⟶ τ₃) → FrameInstruction C (τ₁ ∷ []) [] (τ₂ ⟶ τ₃)
_∷_ : ∀ {τs₁ τs₂ τ₁′ τ₂′ τ′ τ} → let C′ = record C { labels = τ₂′ ∷ (Inst.Context.labels C) } in Inst.Sequence C′ (τ′ ++ τ₁′ ⟶ τ₂′) → FrameInstruction C τs₁ τs₂ (τ₁′ ⟶ τ) → FrameInstruction C (τ₁′ ∷ τs₁) (τ₂′ ∷ τs₂) (τ′ ⟶ τ)
record Frame (S : StoreTypes) (τ : FuncType) : Set (ℓsuc a) where
field
context : Inst.Context
private
module context = Inst.Context context
field
modinst : ModuleInst S context
{stackTy} : List (List ValType)
{labelTy} : List (List ValType)
locals : Map (Value S) (context.locals)
stack : Map (Map (Value S)) stackTy
insts : FrameInstruction context stackTy labelTy τ
record Thread (S : StoreTypes) (τ : List ValType) : Set (ℓsuc a) where
field
{frameTy} : List (List ValType)
frames : Linked (λ τ₁ τ₂ → Frame S (τ₁ ⟶ τ₂)) ([] ∷ frameTy ++ τ ∷ [])
|
