File tree 10 files changed +33
-496
lines changed
src/pykwasm/kdist/wasm-semantics
10 files changed +33
-496
lines changed Original file line number Diff line number Diff line change @@ -800,7 +800,7 @@ This is the full definition of the `(memory.grow)` operation:
800
800
#then SIZE
801
801
#else -1
802
802
#fi ... </k>
803
- <memAddrs> wrap(0) Int2Int |-> wrap( ADDR) </memAddrs>
803
+ <memAddrs> 0 |-> ADDR </memAddrs>
804
804
<memInst>
805
805
<memAddr> ADDR </memAddr>
806
806
<mmax> MAX </mmax>
Original file line number Diff line number Diff line change @@ -2,14 +2,14 @@ module MEMORY-SPEC
2
2
imports WASM
3
3
4
4
rule <k> ( memory.size ) => (i32.const SZ) ... </k>
5
- <memAddrs> wrap(0) Int2Int |-> wrap(A) </memAddrs>
5
+ <memAddrs> 0 |-> A </memAddrs>
6
6
<memInst>
7
7
<memAddr> A </memAddr>
8
8
<memSize> SZ </memSize>
9
9
</memInst>
10
10
11
11
rule <k> (memory.grow (i32.const X)) => (i32.const SZ) ...</k>
12
- <memAddrs> wrap(0) Int2Int |-> wrap(A) </memAddrs>
12
+ <memAddrs> 0 |-> A </memAddrs>
13
13
<memInst>
14
14
<memAddr> A </memAddr>
15
15
<memSize> SZ => (SZ +Int X) </memSize>
@@ -21,7 +21,7 @@ module MEMORY-SPEC
21
21
andBool SZ >=Int 0
22
22
23
23
rule <k> (memory.grow (i32.const X)) => (i32.const -1) ...</k>
24
- <memAddrs> wrap(0) Int2Int |-> wrap(A) </memAddrs>
24
+ <memAddrs> 0 |-> A </memAddrs>
25
25
<memInst>
26
26
<memAddr> A </memAddr>
27
27
<memSize> SZ </memSize>
Original file line number Diff line number Diff line change @@ -104,7 +104,7 @@ endmodule
104
104
<spuriousMemoryFail> false </spuriousMemoryFail>
105
105
106
106
rule <k> (( memory ) ~> ELSE) => ELSE </k>
107
- <memAddrs> .MapIntToInt => wrap(0) Int2Int |-> wrap( NEXT) </memAddrs>
107
+ <memAddrs> .Map => 0 |-> NEXT </memAddrs>
108
108
<nextMemAddr> NEXT => NEXT +Int 1 </nextMemAddr>
109
109
<mems>
110
110
(.Bag =>
@@ -118,7 +118,7 @@ endmodule
118
118
syntax Instr ::= "(" "memory.size" ")"
119
119
// --------------------------------------
120
120
rule <k> ( memory.size ) => ( i32.const SZ ) ... </k>
121
- <memAddrs> wrap(0) Int2Int |-> wrap(A) </memAddrs>
121
+ <memAddrs> 0 |-> A </memAddrs>
122
122
<memInst>
123
123
<memAddr> A </memAddr>
124
124
<memSize> SZ </memSize>
@@ -131,7 +131,7 @@ endmodule
131
131
rule <k> (memory.grow I:Instr) => I ~> (memory.grow) ... </k>
132
132
rule <k> (memory.grow) => (i32.const SZ) ... </k>
133
133
<stack> < i32 > V : S => S </stack>
134
- <memAddrs> wrap(0) Int2Int |-> wrap(A) </memAddrs>
134
+ <memAddrs> 0 |-> A </memAddrs>
135
135
<memInst>
136
136
<memAddr> A </memAddr>
137
137
<memSize> SZ => SZ +Int V </memSize>
Original file line number Diff line number Diff line change 1
- 0.1.70
1
+ 0.1.71
Original file line number Diff line number Diff line change @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
4
4
5
5
[tool .poetry ]
6
6
name = " pykwasm"
7
- version = " 0.1.70 "
7
+ version = " 0.1.71 "
8
8
description = " "
9
9
authors = [
10
10
" Runtime Verification, Inc. <[email protected] >" ,
You can’t perform that action at this time.
0 commit comments