Skip to content

Commit f08a13d

Browse files
dwightguthdwightguth
authored
convert store cell to list (#27)
* convert store cell to list * fix bug in krun-sol * add test-clean makefile target * update k version * update output files * update tests
1 parent cb5ae6b commit f08a13d

26 files changed

+3112
-109103
lines changed

‎Makefile

+4-2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
.PHONY: build clean test test-tokens test-staking test-lending test-swap test-erc20 test-erc1155 test-liquid test-lido test-lendingpool test-aave test-regression
1+
.PHONY: build clean test test-clean test-tokens test-staking test-lending test-swap test-erc20 test-erc1155 test-liquid test-lido test-lendingpool test-aave test-regression
22

33
SEMANTICS_DIR = src
44
TEST_DIR = test
@@ -25,8 +25,10 @@ EXAMPLE_TESTS = $(patsubst %.txn, %.out, $(TRANSACTIONS))
2525
build: $(SEMANTICS_DIR)/$(SEMANTICS_FILE)
2626
kompile $(SEMANTICS_DIR)/$(SEMANTICS_FILE) --main-module $(MAIN_MODULE) --gen-glr-bison-parser -O2 --heuristic pbaL
2727

28-
clean:
28+
clean: test-clean
2929
rm -Rf $(SEMANTICS_FILE_NAME)-kompiled
30+
31+
test-clean:
3032
rm -Rf $(OUTPUT_DIR)
3133
rm -Rf $(TEST_DIR)/regression/*.out
3234
rm -Rf $(EXAMPLE_TESTS)

‎bin/krun-sol

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
contract="$1"
33
txn="$2"
44

5-
if [ "$#" -lt 3 ]; then
5+
if [[ "$3" == -* ]]; then
66
isuniswap=""
77
else
88
isuniswap="$3"

‎deps/k_release

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
7.1.130
1+
7.1.144

‎src/expression.md

+21-21
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ module SOLIDITY-EXPRESSION
1313
<this> THIS => ADDR </this>
1414
<this-type> TYPE => X </this-type>
1515
<env> E => .Map </env>
16-
<store> S => .Map </store>
16+
<store> S => .List </store>
1717
<current-function> FUNC => constructor </current-function>
1818
<call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) </call-stack>
1919
<contract-id> X </contract-id>
@@ -39,7 +39,7 @@ module SOLIDITY-EXPRESSION
3939
<this> THIS => ADDR </this>
4040
<this-type> TYPE => X </this-type>
4141
<env> E => .Map </env>
42-
<store> S => .Map </store>
42+
<store> S => .List </store>
4343
<current-function> FUNC => constructor </current-function>
4444
<call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) </call-stack>
4545
<contract-id> X </contract-id>
@@ -55,10 +55,10 @@ module SOLIDITY-EXPRESSION
5555
<next-address> ADDR => ADDR +MInt 1p160 </next-address>
5656
5757
// new array
58-
rule <k> new T[](Len:Int) => lv(!I:Int, .List, T[]) ...</k>
59-
<store> S => S [ !I:Int <- makeList(Len, default(T)) ] </store>
60-
rule <k> new T[](v(Len:MInt{256}, _)) => lv(!I:Int, .List, T[]) ...</k>
61-
<store> S => S [ !I:Int <- makeList(MInt2Unsigned(Len), default(T)) ] </store>
58+
rule <k> new T[](Len:Int) => lv(size(S), .List, T[]) ...</k>
59+
<store> S => S ListItem(makeList(Len, default(T))) </store>
60+
rule <k> new T[](v(Len:MInt{256}, _)) => lv(size(S), .List, T[]) ...</k>
61+
<store> S => S ListItem(makeList(MInt2Unsigned(Len), default(T))) </store>
6262
6363
// literal assignment to state variable
6464
rule <k> X:Id = N:Int => X = v(convert(N, LT), LT) ...</k>
@@ -141,7 +141,7 @@ module SOLIDITY-EXPRESSION
141141
// local variable lookup
142142
rule <k> X:Id => v(V, T) ...</k>
143143
<env>... X |-> var(I, T) ...</env>
144-
<store>... I |-> V ...</store>
144+
<store> _ [ I <- V ] </store>
145145
requires notBool isAggregateType(T)
146146
147147
rule <k> X:Id => lv(I, .List, T) ...</k>
@@ -152,10 +152,10 @@ module SOLIDITY-EXPRESSION
152152
context HOLE:Expression [ _:Expression ]
153153
context _:Expression [ HOLE:Expression ]
154154
rule <k> lv(I:Int, L, T []) [ Idx:Int ] => v(read(V, L ListItem(Idx), T[]), T) ...</k>
155-
<store>... I |-> V ...</store>
155+
<store> _ [ I <- V ] </store>
156156
requires notBool isAggregateType(T)
157157
rule <k> lv(I:Int, L, T []) [ v(Idx:MInt{256}, _) ] => v(read(V, L ListItem(MInt2Unsigned(Idx)), T[]), T) ...</k>
158-
<store>... I |-> V ...</store>
158+
<store> _ [ I <- V ] </store>
159159
requires notBool isAggregateType(T)
160160
rule <k> lv(X:Id, L, mapping(T1:ElementaryTypeName _ => T2)) [ v(Key, RT) ] => v(read({S [ X ] orDefault .Map}:>Value, L ListItem(convert(Key, RT, T1)), T), T2) ...</k>
161161
<this> THIS </this>
@@ -182,7 +182,7 @@ module SOLIDITY-EXPRESSION
182182
syntax Id ::= "length" [token]
183183
context HOLE . length
184184
rule <k> lv(I:Int, .List, T) . length => v(Int2MInt(size({read(V, .List, T)}:>List))::MInt{256}, uint) ...</k>
185-
<store>... I |-> V ...</store>
185+
<store> _ [ I <- V ] </store>
186186
187187
// external call
188188
context HOLE . _ ( _:CallArgumentList )
@@ -193,7 +193,7 @@ module SOLIDITY-EXPRESSION
193193
<this> THIS => ADDR </this>
194194
<this-type> TYPE => TYPE' </this-type>
195195
<env> E => .Map </env>
196-
<store> S => .Map </store>
196+
<store> S => .List </store>
197197
<current-function> FUNC => F </current-function>
198198
<call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) </call-stack>
199199
<contract-id> TYPE' </contract-id>
@@ -219,7 +219,7 @@ module SOLIDITY-EXPRESSION
219219
<this> THIS => ADDR </this>
220220
<this-type> TYPE => TYPE' </this-type>
221221
<env> E => .Map </env>
222-
<store> S => .Map </store>
222+
<store> S => .List </store>
223223
<current-function> FUNC => F </current-function>
224224
<call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) </call-stack>
225225
<contract-id> TYPE' </contract-id>
@@ -315,10 +315,10 @@ module SOLIDITY-EXPRESSION
315315
// local increment and decrement
316316
rule <k> X:Id ++ => v(V, T) ...</k>
317317
<env>... X |-> var(I, T) ...</env>
318-
<store>... I |-> (V => add(V, convert(1, T))) ...</store>
318+
<store> _ [ I <- (V => add(V, convert(1, T))) ] </store>
319319
rule <k> X:Id -- => v(V, T) ...</k>
320320
<env>... X |-> var(I, T) ...</env>
321-
<store>... I |-> (V => sub(V, convert(1, T))) ...</store>
321+
<store> _ [ I <- (V => sub(V, convert(1, T))) ] </store>
322322
323323
// equality and inequality
324324
rule v(V1:Value, T) == v(V2:Value, T) => v(eq(V1, V2), bool)
@@ -389,19 +389,19 @@ module SOLIDITY-EXPRESSION
389389
390390
syntax KItem ::= var(Int, TypeName)
391391
392-
syntax KItem ::= bind(Map, List, List, CallArgumentList, List, List)
392+
syntax KItem ::= bind(List, List, List, CallArgumentList, List, List)
393393
rule bind(_, .List, .List, .CallArgumentList, .List, .List) => .K
394394
rule bind(STORE, ListItem(noId) PARAMS, ListItem(_) TYPES, _, ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2)
395395
rule bind(STORE, .List, .List, .CallArgumentList, ListItem(_) TYPES, ListItem(noId) NAMES) => bind(STORE, .List, .List, .CallArgumentList, TYPES, NAMES)
396396
rule <k> bind(STORE, ListItem(X:Id) PARAMS, ListItem(T:TypeName) TYPES, lv(I:Int, .List, T:TypeName), ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) ...</k>
397-
<env> E => E [ X <- var(!I:Int, T) ] </env>
398-
<store> S => S [ !I <- STORE [ I ] ] </store>
397+
<env> E => E [ X <- var(size(S), T) ] </env>
398+
<store> S => S ListItem(STORE [ I ]) </store>
399399
rule <k> bind(STORE, ListItem(X:Id) PARAMS, ListItem(LT:TypeName) TYPES, v(V:Value, RT:TypeName), ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) ...</k>
400-
<env> E => E [ X <- var(!I:Int, LT) ] </env>
401-
<store> S => S [ !I <- convert(V, RT, LT) ] </store>
400+
<env> E => E [ X <- var(size(S), LT) ] </env>
401+
<store> S => S ListItem(convert(V, RT, LT)) </store>
402402
rule <k> bind(STORE, .List, .List, .CallArgumentList, ListItem(LT:TypeName) TYPES, ListItem(X:Id) NAMES) => bind(STORE, .List, .List, .CallArgumentList, TYPES, NAMES) ...</k>
403-
<env> E => E [ X <- var(!I:Int, LT) ] </env>
404-
<store> S => S [ !I <- default(LT) ] </store>
403+
<env> E => E [ X <- var(size(S), LT) ] </env>
404+
<store> S => S ListItem(default(LT)) </store>
405405
406406
syntax Value ::= convert(Value, from: TypeName, to: TypeName) [function]
407407
rule convert(V, T, T) => V

‎src/solidity.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ module SOLIDITY-CONFIGURATION
6969
<this> 0p160 </this>
7070
<this-type> Id </this-type>
7171
<env> .Map </env>
72-
<store> .Map </store>
72+
<store> .List </store>
7373
<current-function> Id </current-function>
7474
<call-stack> .List </call-stack>
7575
<live-contracts>
@@ -165,7 +165,7 @@ module SOLIDITY-DATA
165165
rule isAggregateType(_) => false [owise]
166166
167167
// external frame
168-
syntax Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id, value: MInt{256}, func: Id)
168+
syntax Frame ::= frame(continuation: K, env: Map, store: List, from: MInt{160}, type: Id, value: MInt{256}, func: Id)
169169
// internal frame
170170
| frame(continuation: K, env: Map, func: Id)
171171
syntax Event ::= event(name: Id, args: TypedVals)

‎src/statement.md

+9-9
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ module SOLIDITY-STATEMENT
3333
<call-stack>... ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) => .List </call-stack>
3434
3535
rule <k> return lv(I:Int, .List, T) ; => return v(L, T) ; ...</k>
36-
<store>... I |-> L ...</store>
36+
<store> _ [ I <- L ] </store>
3737
3838
rule <k> return V:TypedVal ; ~> _ => V ~> K </k>
3939
<env> _ => E </env>
@@ -42,19 +42,19 @@ module SOLIDITY-STATEMENT
4242
4343
// variable declaration
4444
rule <k> LT:TypeName X:Id = v(V, RT) ; => .K ...</k>
45-
<env> E => E [ X <- var(!I:Int, LT) ] </env>
46-
<store> S => S [ !I <- convert(V, RT, LT) ] </store>
45+
<env> E => E [ X <- var(size(S), LT) ] </env>
46+
<store> S => S ListItem(convert(V, RT, LT)) </store>
4747
rule <k> LT:TypeName X:Id = N:Int ; => .K ...</k>
48-
<env> E => E [ X <- var(!I:Int, LT) ] </env>
49-
<store> S => S [ !I <- convert(N, LT) ] </store>
48+
<env> E => E [ X <- var(size(S), LT) ] </env>
49+
<store> S => S ListItem(convert(N, LT)) </store>
5050
rule <k> LT:TypeName memory X:Id = v(V, RT) ; => .K ...</k>
51-
<env> E => E [ X <- var(!I:Int, LT) ] </env>
52-
<store> S => S [ !I <- convert(V, RT, LT) ] </store>
51+
<env> E => E [ X <- var(size(S), LT) ] </env>
52+
<store> S => S ListItem(convert(V, RT, LT)) </store>
5353
rule <k> T:TypeName memory X:Id = lv(I:Int, .List, T) ; => .K ...</k>
5454
<env> E => E [ X <- var(I, T) ] </env>
5555
rule <k> T:TypeName X:Id ;::VariableDeclarationStatement => .K ...</k>
56-
<env> E => E [ X <- var(!I:Int, T) ] </env>
57-
<store> S => S [ !I <- default(T) ] </store>
56+
<env> E => E [ X <- var(size(S), T) ] </env>
57+
<store> S => S ListItem(default(T)) </store>
5858
5959
// emit statement
6060
rule <k> emit X:Id ( ARGS ) ; => discard(Event2String(ARGS, ((.StringBuffer +String Id2String(X)) +String "("))) ...</k>

‎src/transaction.md

+5-5
Original file line numberDiff line numberDiff line change
@@ -7,15 +7,15 @@ module SOLIDITY-TRANSACTION
77
imports INT
88
imports private SOLIDITY-EXPRESSION
99
10-
rule <k> create(FROM, VALUE, NOW, CTOR, ARGS) => bind(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ...</k>
10+
rule <k> create(FROM, VALUE, NOW, CTOR, ARGS) => bind(.List, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ...</k>
1111
<msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
1212
<msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
1313
<tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
1414
<block-timestamp> _ => Int2MInt(Number2Int(NOW)) </block-timestamp>
1515
<this> _ => ADDR </this>
1616
<this-type> _ => CTOR </this-type>
1717
<env> _ => .Map </env>
18-
<store> _ => .Map </store>
18+
<store> _ => .List </store>
1919
<current-function> _ => constructor </current-function>
2020
<contract-id> CTOR </contract-id>
2121
<contract-init> INIT </contract-init>
@@ -42,7 +42,7 @@ module SOLIDITY-TRANSACTION
4242
<this> _ => ADDR </this>
4343
<this-type> _ => CTOR </this-type>
4444
<env> _ => .Map </env>
45-
<store> _ => .Map </store>
45+
<store> _ => .List </store>
4646
<current-function> _ => constructor </current-function>
4747
<contract-id> CTOR </contract-id>
4848
<contract-init> INIT </contract-init>
@@ -60,15 +60,15 @@ module SOLIDITY-TRANSACTION
6060
syntax Transaction ::= txn(from: Decimal, to: MInt{160}, value: Decimal, timestamp: Decimal, func: Id, args: CallArgumentList) [strict(6)]
6161
rule txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => txn(FROM, Int2MInt(Number2Int(TO)), VALUE, NOW, FUNC, ARGS)
6262
63-
rule <k> txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ...</k>
63+
rule <k> txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(.List, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ...</k>
6464
<msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
6565
<msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
6666
<tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
6767
<block-timestamp> _ => Int2MInt(Number2Int(NOW)) </block-timestamp>
6868
<this> _ => TO </this>
6969
<this-type> _ => TYPE </this-type>
7070
<env> _ => .Map </env>
71-
<store> _ => .Map </store>
71+
<store> _ => .List </store>
7272
<current-function> _ => FUNC </current-function>
7373
<live-contracts>
7474
<contract-address> TO </contract-address>

‎test/regression/addliquidity.ref

+5-5
Original file line numberDiff line numberDiff line change
@@ -2350,11 +2350,11 @@
23502350
testAmount |-> var ( 0 , uint256 )
23512351
</env>
23522352
<store>
2353-
0 |-> 131072p256
2354-
1 |-> 10000p256
2355-
2 |-> 10000p256
2356-
3 |-> 0p256
2357-
4 |-> 0p256
2353+
ListItem ( 131072p256 )
2354+
ListItem ( 10000p256 )
2355+
ListItem ( 10000p256 )
2356+
ListItem ( 0p256 )
2357+
ListItem ( 0p256 )
23582358
</store>
23592359
<current-function>
23602360
testRouterAddLiquidity

‎test/regression/arithmetic.ref

+8-8
Original file line numberDiff line numberDiff line change
@@ -87,14 +87,14 @@
8787
i256_2 |-> var ( 7 , uint8 )
8888
</env>
8989
<store>
90-
0 |-> 2p8
91-
1 |-> 4p8
92-
2 |-> 2p8
93-
3 |-> 4p8
94-
4 |-> 2p8
95-
5 |-> 4p8
96-
6 |-> 2p8
97-
7 |-> 4p8
90+
ListItem ( 2p8 )
91+
ListItem ( 4p8 )
92+
ListItem ( 2p8 )
93+
ListItem ( 4p8 )
94+
ListItem ( 2p8 )
95+
ListItem ( 4p8 )
96+
ListItem ( 2p8 )
97+
ListItem ( 4p8 )
9898
</store>
9999
<current-function>
100100
constructor

‎test/regression/arraystestcontract.ref

+1-1
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@
106106
.Map
107107
</env>
108108
<store>
109-
.Map
109+
.List
110110
</store>
111111
<current-function>
112112
constructor

‎test/regression/block.ref

+2-2
Original file line numberDiff line numberDiff line change
@@ -80,8 +80,8 @@
8080
x |-> var ( 0 , bool )
8181
</env>
8282
<store>
83-
0 |-> false
84-
1 |-> true
83+
ListItem ( false )
84+
ListItem ( true )
8585
</store>
8686
<current-function>
8787
constructor

‎test/regression/boolean.ref

+1-1
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@
105105
x |-> var ( 0 , bool )
106106
</env>
107107
<store>
108-
0 |-> false
108+
ListItem ( false )
109109
</store>
110110
<current-function>
111111
constructor

‎test/regression/contract.ref

+3-3
Original file line numberDiff line numberDiff line change
@@ -348,9 +348,9 @@
348348
_weth |-> var ( 0 , address )
349349
</env>
350350
<store>
351-
0 |-> 2p160
352-
1 |-> 3p160
353-
2 |-> 4p160
351+
ListItem ( 2p160 )
352+
ListItem ( 3p160 )
353+
ListItem ( 4p160 )
354354
</store>
355355
<current-function>
356356
constructor

‎test/regression/emit.ref

+1-1
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,7 @@
9898
.Map
9999
</env>
100100
<store>
101-
.Map
101+
.List
102102
</store>
103103
<current-function>
104104
constructor

‎test/regression/eventtestcontract.ref

+1-1
Original file line numberDiff line numberDiff line change
@@ -226,7 +226,7 @@
226226
.Map
227227
</env>
228228
<store>
229-
.Map
229+
.List
230230
</store>
231231
<current-function>
232232
constructor

‎test/regression/for.ref

+3-3
Original file line numberDiff line numberDiff line change
@@ -81,9 +81,9 @@
8181
y |-> var ( 1 , uint256 )
8282
</env>
8383
<store>
84-
0 |-> 5p256
85-
1 |-> 20p256
86-
2 |-> 10p256
84+
ListItem ( 5p256 )
85+
ListItem ( 20p256 )
86+
ListItem ( 10p256 )
8787
</store>
8888
<current-function>
8989
constructor

‎test/regression/funcnamefail.ref

+1-1
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@
130130
.Map
131131
</env>
132132
<store>
133-
.Map
133+
.List
134134
</store>
135135
<current-function>
136136
chaincall2

‎test/regression/funcnamesucceed.ref

+1-1
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@
130130
x |-> var ( 0 , uint256 )
131131
</env>
132132
<store>
133-
0 |-> 2p256
133+
ListItem ( 2p256 )
134134
</store>
135135
<current-function>
136136
constructor

‎test/regression/function.ref

+1-1
Original file line numberDiff line numberDiff line change
@@ -2074,7 +2074,7 @@
20742074
.Map
20752075
</env>
20762076
<store>
2077-
.Map
2077+
.List
20782078
</store>
20792079
<current-function>
20802080
setUp

0 commit comments

Comments
 (0)