Skip to content

Commit c72048a

Browse files
merendamattiamerendamattia
committed
Added cast checks in SHA3 semantic.
1 parent fdbdda8 commit c72048a

File tree

4 files changed

+19
-117
lines changed

4 files changed

+19
-117
lines changed

‎evm-testcases/cfs/keccak256/keccak.sol‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
11
PUSH1 0x20
22
PUSH1 0x00
3+
SHA3
4+
PUSH32 0xFFFFFFFF00000000000000000000000000000000000000000000000000000000
5+
PUSH1 0x00
6+
MSTORE
7+
PUSH1 0x04
8+
PUSH1 0x00
39
SHA3

‎evm-testcases/cfs/keccak256/report.json‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,15 @@
33
"files" : [ "report.json", "untyped_program.evm-testcases_cfs_keccak256_keccak.sol().json" ],
44
"info" : {
55
"cfgs" : "1",
6-
"duration" : "420ms",
7-
"end" : "2025-05-10T23:18:33.632+02:00",
8-
"expressions" : "2",
6+
"duration" : "83ms",
7+
"end" : "2025-05-11T16:13:02.675+02:00",
8+
"expressions" : "6",
99
"files" : "1",
1010
"globals" : "0",
1111
"members" : "1",
1212
"programs" : "1",
13-
"start" : "2025-05-10T23:18:33.212+02:00",
14-
"statements" : "3",
13+
"start" : "2025-05-11T16:13:02.592+02:00",
14+
"statements" : "9",
1515
"units" : "0",
1616
"version" : "0.1",
1717
"warnings" : "0"

‎evm-testcases/cfs/keccak256/untyped_program.evm-testcases_cfs_keccak256_keccak.sol().json‎

Lines changed: 1 addition & 107 deletions
Original file line numberDiff line numberDiff line change
@@ -1,107 +1 @@
1-
{
2-
"name": "untyped program::evm-testcases/cfs/keccak256/keccak.sol()",
3-
"description": null,
4-
"nodes": [
5-
{
6-
"id": 0,
7-
"subNodes": [
8-
1
9-
],
10-
"text": "PUSH1 0x20"
11-
},
12-
{
13-
"id": 1,
14-
"text": "0x20"
15-
},
16-
{
17-
"id": 2,
18-
"subNodes": [
19-
3
20-
],
21-
"text": "PUSH1 0x00"
22-
},
23-
{
24-
"id": 3,
25-
"text": "0x00"
26-
},
27-
{
28-
"id": 4,
29-
"text": "SHA3"
30-
}
31-
],
32-
"edges": [
33-
{
34-
"sourceId": 0,
35-
"destId": 2,
36-
"kind": "SequentialEdge"
37-
},
38-
{
39-
"sourceId": 2,
40-
"destId": 4,
41-
"kind": "SequentialEdge"
42-
}
43-
],
44-
"descriptions": [
45-
{
46-
"nodeId": 0,
47-
"description": {
48-
"expressions": [
49-
"push \"0x20\""
50-
],
51-
"state": {
52-
"heap": "monolith",
53-
"type": "#TOP#",
54-
"value": "{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 32]], memory: EMPTY, storage: #TOP# }"
55-
}
56-
}
57-
},
58-
{
59-
"nodeId": 1,
60-
"description": {
61-
"expressions": [
62-
"\"0x20\""
63-
],
64-
"state": "#TOP#"
65-
}
66-
},
67-
{
68-
"nodeId": 2,
69-
"description": {
70-
"expressions": [
71-
"push \"0x00\""
72-
],
73-
"state": {
74-
"heap": "monolith",
75-
"type": "#TOP#",
76-
"value": "{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 32, 0]], memory: EMPTY, storage: #TOP# }"
77-
}
78-
}
79-
},
80-
{
81-
"nodeId": 3,
82-
"description": {
83-
"expressions": [
84-
"\"0x00\""
85-
],
86-
"state": {
87-
"heap": "monolith",
88-
"type": "#TOP#",
89-
"value": "{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 32]], memory: EMPTY, storage: #TOP# }"
90-
}
91-
}
92-
},
93-
{
94-
"nodeId": 4,
95-
"description": {
96-
"expressions": [
97-
"sha3 1"
98-
],
99-
"state": {
100-
"heap": "monolith",
101-
"type": "#TOP#",
102-
"value": "{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947]], memory: EMPTY, storage: #TOP# }"
103-
}
104-
}
105-
}
106-
]
107-
}
1+
{"name":"untyped program::evm-testcases/cfs/keccak256/keccak.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x20"},{"id":1,"text":"0x20"},{"id":2,"subNodes":[3],"text":"PUSH1 0x00"},{"id":3,"text":"0x00"},{"id":4,"text":"SHA3"},{"id":5,"subNodes":[6],"text":"PUSH32 0xFFFFFFFF00000000000000000000000000000000000000000000000000000000"},{"id":6,"text":"0xFFFFFFFF00000000000000000000000000000000000000000000000000000000"},{"id":7,"subNodes":[8],"text":"PUSH1 0x00"},{"id":8,"text":"0x00"},{"id":9,"text":"MSTORE"},{"id":10,"subNodes":[11],"text":"PUSH1 0x04"},{"id":11,"text":"0x04"},{"id":12,"subNodes":[13],"text":"PUSH1 0x00"},{"id":13,"text":"0x00"},{"id":14,"text":"SHA3"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":4,"kind":"SequentialEdge"},{"sourceId":4,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":10,"kind":"SequentialEdge"},{"sourceId":10,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":14,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x20\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 32]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":1,"description":{"expressions":["\"0x20\""],"state":"#TOP#"}},{"nodeId":2,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 32, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":3,"description":{"expressions":["\"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 32]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":4,"description":{"expressions":["sha3 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":5,"description":{"expressions":["push \"0xFFFFFFFF00000000000000000000000000000000000000000000000000000000\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947, 115792089210356248756420345214020892766250353992003419616917011526809519390720]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":6,"description":{"expressions":["\"0xFFFFFFFF00000000000000000000000000000000000000000000000000000000\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":7,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947, 115792089210356248756420345214020892766250353992003419616917011526809519390720, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":8,"description":{"expressions":["\"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947, 115792089210356248756420345214020892766250353992003419616917011526809519390720]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":9,"description":{"expressions":["mstore 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947]], memory: FFFFFFFF00000000000000000000000000000000000000000000000000000000, storage: #TOP# }"}}},{"nodeId":10,"description":{"expressions":["push \"0x04\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947, 4]], memory: FFFFFFFF00000000000000000000000000000000000000000000000000000000, storage: #TOP# }"}}},{"nodeId":11,"description":{"expressions":["\"0x04\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947]], memory: FFFFFFFF00000000000000000000000000000000000000000000000000000000, storage: #TOP# }"}}},{"nodeId":12,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947, 4, 0]], memory: FFFFFFFF00000000000000000000000000000000000000000000000000000000, storage: #TOP# }"}}},{"nodeId":13,"description":{"expressions":["\"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947, 4]], memory: FFFFFFFF00000000000000000000000000000000000000000000000000000000, storage: #TOP# }"}}},{"nodeId":14,"description":{"expressions":["sha3 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 18569430475105882587588266137607568536673111973893317399460219858819262702947, 18552517740152708416751806921020054235891601220706205192958828703704562188856]], memory: FFFFFFFF00000000000000000000000000000000000000000000000000000000, storage: #TOP# }"}}}]}

‎src/main/java/it/unipr/analysis/EVMAbstractState.java‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -807,16 +807,18 @@ else if (indexOfByte.compareTo(new StackElement(Number.MAX_INT)) < 0) {
807807

808808
if (offset.isUnknown() || size.isUnknown() || memory.isTop())
809809
resultStack.push(StackElement.NOT_JUMPDEST_TOP);
810-
else {
810+
else if (offset.compareTo(new StackElement(Number.MAX_INT)) <= 0
811+
|| size.compareTo(new StackElement(Number.MAX_INT)) <= 0){
811812

812-
// Read exactly size bytes from your abstract
813-
// memory.
814-
byte[] chunk = memory.readBytes(offset.getNumber().getInt(), size.getNumber().getInt());
813+
/* Read exactly size bytes from your abstract memory. */
814+
byte[] chunk = memory.readBytes(
815+
offset.getNumber().getInt(),
816+
size.getNumber().getInt());
815817

816818
if (chunk == null)
817819
resultStack.push(StackElement.NOT_JUMPDEST_TOP);
818820
else {
819-
// Keccak256 hash
821+
/* Keccak256 hash */
820822
Digest256 kecc = new Keccak.Digest256();
821823
kecc.update(chunk, 0, chunk.length);
822824
byte[] hash = kecc.digest();

0 commit comments

Comments
 (0)