Skip to content

Commit 594a09d

Browse files
VincenzoArceriVincenzoArceri
committed
Keccak256 abstract semantics
1 parent 3385659 commit 594a09d

File tree

8 files changed

+209
-57
lines changed

8 files changed

+209
-57
lines changed

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
PUSH1 0x20
2+
PUSH1 0x00
3+
SHA3

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

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
{
2+
"warnings" : [ ],
3+
"files" : [ "report.json", "untyped_program.evm-testcases_cfs_keccak256_keccak.sol().json" ],
4+
"info" : {
5+
"cfgs" : "1",
6+
"duration" : "420ms",
7+
"end" : "2025-05-10T23:18:33.632+02:00",
8+
"expressions" : "2",
9+
"files" : "1",
10+
"globals" : "0",
11+
"members" : "1",
12+
"programs" : "1",
13+
"start" : "2025-05-10T23:18:33.212+02:00",
14+
"statements" : "3",
15+
"units" : "0",
16+
"version" : "0.1",
17+
"warnings" : "0"
18+
},
19+
"configuration" : {
20+
"analysisGraphs" : "NONE",
21+
"descendingPhaseType" : "NONE",
22+
"dumpForcesUnwinding" : "false",
23+
"fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet",
24+
"glbThreshold" : "5",
25+
"hotspots" : "unset",
26+
"jsonOutput" : "true",
27+
"openCallPolicy" : "WorstCasePolicy",
28+
"optimize" : "false",
29+
"recursionWideningThreshold" : "5",
30+
"semanticChecks" : "JumpSolver",
31+
"serializeInputs" : "false",
32+
"serializeResults" : "true",
33+
"syntacticChecks" : "",
34+
"useWideningPoints" : "false",
35+
"wideningThreshold" : "5",
36+
"workdir" : "evm-outputs/cfs/keccak256"
37+
}
38+
}

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

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
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+
}

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

Lines changed: 45 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,8 @@ public AbstractMemory mstore(StackElement offset, StackElement e) {
5757
}
5858

5959
if (offset.compareTo(new StackElement(Number.MAX_INT)) >= 0) {
60-
log.warn("Offset is greater than max int representation, ignoring mstore with offset {}, value {}.", offset, e);
60+
log.warn("Offset is greater than max int representation, ignoring mstore with offset {}, value {}.", offset,
61+
e);
6162
return AbstractMemory.BOTTOM; // fake path
6263
}
6364

@@ -86,12 +87,14 @@ public AbstractMemory mstore8(StackElement offset, StackElement value) {
8687
}
8788

8889
if (offset.compareTo(new StackElement(MAX_MEMORY_SIZE)) >= 0) {
89-
log.warn("Offset or value are greater than max memory size, ignoring mstore8 with offset {} and value {}.", offset, value);
90+
log.warn("Offset or value are greater than max memory size, ignoring mstore8 with offset {} and value {}.",
91+
offset, value);
9092
return AbstractMemory.BOTTOM;
9193
}
9294

9395
if (offset.compareTo(new StackElement(Number.MAX_INT)) >= 0) {
94-
log.warn("Offset is greater than max int representation, ignoring mstore8 with offset {} and value {}.", offset, value);
96+
log.warn("Offset is greater than max int representation, ignoring mstore8 with offset {} and value {}.",
97+
offset, value);
9598
return AbstractMemory.BOTTOM; // fake path
9699
}
97100

@@ -130,24 +133,36 @@ public StackElement mload(StackElement offset) {
130133

131134
public AbstractMemory mcopy(StackElement destOffset, StackElement srcOffset, StackElement length) {
132135
if (length.compareTo(new StackElement(MAX_MEMORY_SIZE)) >= 0) {
133-
log.warn("length is greater than max memory size, ignoring mcopy with destOffset {}, srcOffset {}, length {}.", destOffset, srcOffset, length);
136+
log.warn(
137+
"length is greater than max memory size, ignoring mcopy with destOffset {}, srcOffset {}, length {}.",
138+
destOffset, srcOffset, length);
134139
return AbstractMemory.TOP;
135140
} else if (destOffset.compareTo(new StackElement(MAX_MEMORY_SIZE)) >= 0) {
136-
log.warn("destOffset is greater than max memory size, ignoring mcopy with destOffset {}, srcOffset {}, length {}.", destOffset, srcOffset, length);
141+
log.warn(
142+
"destOffset is greater than max memory size, ignoring mcopy with destOffset {}, srcOffset {}, length {}.",
143+
destOffset, srcOffset, length);
137144
return AbstractMemory.TOP;
138145
} else if (srcOffset.compareTo(new StackElement(MAX_MEMORY_SIZE)) >= 0) {
139-
log.warn("srcOffset is greater than max memory size, ignoring mcopy with destOffset {}, srcOffset {}, length {}.", destOffset, srcOffset, length);
146+
log.warn(
147+
"srcOffset is greater than max memory size, ignoring mcopy with destOffset {}, srcOffset {}, length {}.",
148+
destOffset, srcOffset, length);
140149
return AbstractMemory.TOP;
141150
}
142151

143152
if (destOffset.compareTo(new StackElement(Number.MAX_INT)) >= 0) {
144-
log.warn("destOffset is greater than max int representation, ignoring mcopy with destOffset {}, srcOffset {}, length {}.", destOffset, srcOffset, length);
153+
log.warn(
154+
"destOffset is greater than max int representation, ignoring mcopy with destOffset {}, srcOffset {}, length {}.",
155+
destOffset, srcOffset, length);
145156
return AbstractMemory.BOTTOM; // fake path
146157
} else if (srcOffset.compareTo(new StackElement(Number.MAX_INT)) >= 0) {
147-
log.warn("srcOffset is greater than max int representation, ignoring mcopy with destOffset {}, srcOffset {}, length {}.", destOffset, srcOffset, length);
158+
log.warn(
159+
"srcOffset is greater than max int representation, ignoring mcopy with destOffset {}, srcOffset {}, length {}.",
160+
destOffset, srcOffset, length);
148161
return AbstractMemory.BOTTOM; // fake path
149162
} else if (length.compareTo(new StackElement(Number.MAX_INT)) >= 0) {
150-
log.warn("length is greater than max int representation, ignoring mcopy with destOffset {}, srcOffset {}, length {}.", destOffset, srcOffset, length);
163+
log.warn(
164+
"length is greater than max int representation, ignoring mcopy with destOffset {}, srcOffset {}, length {}.",
165+
destOffset, srcOffset, length);
151166
return AbstractMemory.BOTTOM; // fake path
152167
}
153168

@@ -369,10 +384,30 @@ public static void fill(AbstractByte[] bytes, byte value) {
369384
}
370385
}
371386

372-
private static boolean isUnknown(AbstractByte[] bytes) {
387+
public static boolean isUnknown(AbstractByte[] bytes) {
373388
for (int i = 0; i < 32; i++)
374389
if (bytes[i].isTop())
375390
return true;
376391
return false;
377392
}
393+
394+
public byte[] readBytes(int offset, int length) {
395+
if (offset < 0 || length < 0)
396+
throw new IllegalArgumentException("Negative offset or length");
397+
if (offset + length > MAX_MEMORY_SIZE)
398+
throw new IllegalArgumentException(
399+
"Read exceeds maximum memory size: " + (offset + length));
400+
401+
AbstractByte[] backing = ensureCapacity(offset + length);
402+
403+
byte[] out = new byte[length];
404+
for (int i = 0; i < length; i++) {
405+
AbstractByte b = backing[offset + i];
406+
// Treat TOP/unknown as 0x00
407+
if (b.isTop())
408+
return null;
409+
out[i] = b.isTop() ? (byte) 0 : b.getValue();
410+
}
411+
return out;
412+
}
378413
}

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

Lines changed: 7 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -267,24 +267,15 @@ public void push(StackElement element) {
267267
* @return the element at the top of the stack before popping
268268
*/
269269
public StackElement pop() {
270-
271270
int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT;
272-
StackElement popped = circularArray[topIndex];
273-
274-
// Shift
271+
StackElement poppedElement = circularArray[topIndex];
272+
StackElement oldBottom = circularArray[head];
273+
// rotate head back to shift everything up
275274
head = (head - 1 + STACK_LIMIT) % STACK_LIMIT;
276-
int bottomIndex = head;
277-
int secondLogicalIndex = (head + 1) % STACK_LIMIT;
278-
279-
if (circularArray[secondLogicalIndex].isTop())
280-
circularArray[bottomIndex] = StackElement.TOP;
281-
else
282-
circularArray[bottomIndex] = StackElement.BOTTOM;
283-
284-
tail = (head + STACK_LIMIT) % STACK_LIMIT;
285-
circularArray[topIndex] = StackElement.BOTTOM;
286-
287-
return popped;
275+
// tail follows head (stack remains “full” in structure)
276+
tail = head;
277+
circularArray[head] = oldBottom.isBottom() ? StackElement.BOTTOM : StackElement.TOP;
278+
return poppedElement;
288279
}
289280

290281
/**
@@ -431,31 +422,4 @@ private StackElement[] toLogicalArray() {
431422
logical[i] = circularArray[(head + i) % STACK_LIMIT];
432423
return logical;
433424
}
434-
435-
public static void main(String[] args) {
436-
AbstractStack.setStackLimit(3);
437-
438-
// Stack2: [4, 5, 6], head=0, tail=0 → logico: [4, 5, 6]
439-
AbstractStack stack2 = new AbstractStack();
440-
stack2.push(new StackElement(4));
441-
stack2.push(new StackElement(5));
442-
stack2.push(new StackElement(6));
443-
stack2.head = 0;
444-
stack2.tail = 0;
445-
System.out.println("Stack2: " + stack2);
446-
447-
/*Test2 - array fisicamente diversi ma logicamente uguali*/
448-
System.out.println("********** Test 2 ********** ");
449-
// Stack3: [1, 2, 3], head=1, tail=1 → logico: [2, 3, 1]
450-
AbstractStack stack3 = new AbstractStack();
451-
stack3.head = 1;
452-
stack3.tail = 1;
453-
System.out.println("Stack3: " + stack3);
454-
stack3.push(new StackElement(4));
455-
System.out.println("Stack3: " + stack3);
456-
stack3.push(new StackElement(5));
457-
System.out.println("Stack3: " + stack3);
458-
stack3.push(new StackElement(6));
459-
System.out.println("Stack3: " + stack3);
460-
}
461425
}

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -247,6 +247,7 @@ public Number not() {
247247
* Computes the modulo of this number by another number.
248248
*
249249
* @param other the number to divide by
250+
*
250251
* @return the result as a {@code Number}
251252
*/
252253
public Number modulo(Number other) {

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,6 @@
77
import it.unive.lisa.util.representation.StructuredRepresentation;
88
import java.math.BigInteger;
99
import java.util.Objects;
10-
import java.util.Stack;
11-
1210
import org.apache.logging.log4j.LogManager;
1311
import org.apache.logging.log4j.Logger;
1412

‎src/test/java/it/unipr/analysis/cron/semantics/EVMAbstractSemanticsTest.java‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -97,13 +97,13 @@ public void testMstore() throws AnalysisSetupException, IOException {
9797
CronConfiguration conf = createConfiguration("cfs", "mstore", "mstore_eth.sol", false);
9898
perform(conf);
9999
}
100-
100+
101101
@Test
102102
public void testMstore2() throws AnalysisSetupException, IOException {
103103
CronConfiguration conf = createConfiguration("cfs", "mstore2", "mstore_eth.sol", false);
104104
perform(conf);
105105
}
106-
106+
107107
@Test
108108
public void testMstore3() throws AnalysisSetupException, IOException {
109109
CronConfiguration conf = createConfiguration("cfs", "mstore3", "mstore_eth.sol", false);
@@ -122,6 +122,12 @@ public void testLT() throws AnalysisSetupException, IOException {
122122
perform(conf);
123123
}
124124

125+
@Test
126+
public void testKeccak256() throws AnalysisSetupException, IOException {
127+
CronConfiguration conf = createConfiguration("cfs", "keccak256", "keccak.sol", false);
128+
perform(conf);
129+
}
130+
125131
/**
126132
* All the items in the final stack must be 1
127133
*/

0 commit comments

Comments
 (0)