From 80e0ccd4f77c51d8ab03344b23da33f78c929cf2 Mon Sep 17 00:00:00 2001 From: Shivam Kumar Date: Sun, 16 Mar 2025 22:15:22 +0100 Subject: [PATCH 01/14] Refactored stack structure from linear array to circular array + update javadoc --- .../java/it/unipr/analysis/AbstractStack.java | 173 +++++++++++------- 1 file changed, 110 insertions(+), 63 deletions(-) diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java index 99f27e178..1ed3920de 100644 --- a/src/main/java/it/unipr/analysis/AbstractStack.java +++ b/src/main/java/it/unipr/analysis/AbstractStack.java @@ -26,18 +26,19 @@ public class AbstractStack implements ValueDomain, BaseLattice= STACK_LIMIT) // not valid index + return StackElement.BOTTOM; + return circularArray[(head + index) % STACK_LIMIT]; } @Override @@ -182,42 +215,64 @@ public AbstractStack assume(ValueExpression expression, ProgramPoint src, Progra * @return the StackElement at the top of the stack. */ public StackElement getTop() { - return this.stack[STACK_LIMIT - 1]; // Get the last element + return circularArray[(tail - 1 + STACK_LIMIT) % STACK_LIMIT]; } @Override public AbstractStack clone() { - if (isBottom() || isTop()) + if(isBottom() || isTop()) return this; - return new AbstractStack(stack.clone()); + AbstractStack clone = new AbstractStack(circularArray.clone()); + clone.head = this.head; + clone.tail = this.tail; + return clone; } /** * Pushes the specified element onto the stack. + *

+ * This method inserts the given {@link StackElement} at the tail of the circular array, + * effectively updating the top of the stack. The head of the stack is also updated + * to maintain the circular nature of the structure. * - * @param target the element to be pushed onto the stack. + * @param element the element to be pushed onto the stack */ - public void push(StackElement target) { - // Shift all elements one position to the left - System.arraycopy(stack, 1, stack, 0, STACK_LIMIT - 1); - stack[STACK_LIMIT - 1] = target; + public void push(StackElement element) { + circularArray[tail] = element; + tail = (tail + 1) % STACK_LIMIT; + head = (head + 1) % STACK_LIMIT; } /** * Pops the element from the stack. + *

+ * This method removes and returns the topmost element of the stack. + * After popping, the stack structure is adjusted by shifting the head, + * and the previous bottommost element is updated based on the next element. + * If the next element is {@link StackElement#TOP}, the bottom is set to TOP, + * otherwise, it is set to {@link StackElement#BOTTOM}. * - * @return the element at the top of the stack. + * @return the element at the top of the stack before popping */ public StackElement pop() { - StackElement result = stack[STACK_LIMIT - 1]; - // Shift all elements one position to the right - System.arraycopy(stack, 0, stack, 1, STACK_LIMIT - 1); - if (!stack[1].isTop()) - stack[0] = StackElement.BOTTOM; + + int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; + StackElement popped = circularArray[topIndex]; + + // Shift + head = (head - 1 + STACK_LIMIT) % STACK_LIMIT; + int bottomIndex = head; + int secondLogicalIndex = (head + 1) % STACK_LIMIT; + + if (circularArray[secondLogicalIndex].isTop()) + circularArray[bottomIndex] = StackElement.TOP; else - stack[0] = StackElement.TOP; + circularArray[bottomIndex] = StackElement.BOTTOM; + + tail = (head + STACK_LIMIT) % STACK_LIMIT; + circularArray[topIndex] = StackElement.BOTTOM; - return result; + return popped; } @Override @@ -237,13 +292,12 @@ public AbstractStack glbAux(AbstractStack other) throws SemanticException { @Override public boolean lessOrEqualAux(AbstractStack other) throws SemanticException { - // Starting from the top of the stack and moving downward - for (int i = STACK_LIMIT - 1; i >= 0; i--) { - if (!this.stack[i].lessOrEqual(other.stack[i])) { + for(int i = 0; i < STACK_LIMIT; i++) { + int thisIndex = (tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; + int otherIndex = (other.tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; + if(!this.circularArray[thisIndex].lessOrEqual(other.circularArray[otherIndex])) return false; - } } - return true; } @@ -255,9 +309,11 @@ public boolean lessOrEqualAux(AbstractStack other) throws SemanticException { public StackElement getSecondElement() { if (isBottom()) return StackElement.BOTTOM; - else if (isTop()) + if (isTop()) return StackElement.TOP; - return this.stack[STACK_LIMIT - 2]; + + int secondElementPos = (tail - 2 + STACK_LIMIT) % STACK_LIMIT; + return circularArray[secondElementPos]; } /** @@ -290,10 +346,13 @@ public static int getStackLimit() { * @return {@code true} if between 0 and x-positions of the stack an element * is bottom, {@code false} otherwise. */ + public boolean hasBottomUntil(int x) { - for (int i = 0; i < x; i++) - if (this.stack[(STACK_LIMIT - 1) - i].isBottom()) + for(int i = 0; i < x; i++) { + int pos = (tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; + if(circularArray[pos].isBottom()) return true; + } return false; } @@ -314,20 +373,10 @@ public boolean knowsIdentifier(Identifier id) { public AbstractStack dupX(int x) { if (hasBottomUntil(x)) return bottom(); - - StackElement[] stackArray = this.stack.clone(); - - int topIndex = STACK_LIMIT - 1; - int targetIndex = topIndex - x + 1; - StackElement elementToDuplicate = stackArray[targetIndex]; - - StackElement[] resultArray = new StackElement[STACK_LIMIT]; - - System.arraycopy(stackArray, 1, resultArray, 0, STACK_LIMIT - 1); - - resultArray[topIndex] = elementToDuplicate; - - return new AbstractStack(resultArray); + int posX = (tail - x + STACK_LIMIT) % STACK_LIMIT; + AbstractStack clone = clone(); + clone.push(circularArray[posX]); + return clone; } /** @@ -335,22 +384,20 @@ public AbstractStack dupX(int x) { * returns the modified stack. * * @param x The position of the element to swap with the top of the stack. - * + * * @return A new stack with the specified elements swapped. */ public AbstractStack swapX(int x) { if (hasBottomUntil(x + 1)) return bottom(); - - int topIndex = STACK_LIMIT - 1; - int swapIndex = topIndex - x; - - StackElement[] newStack = this.stack.clone(); - - StackElement temp = newStack[topIndex]; - newStack[topIndex] = newStack[swapIndex]; - newStack[swapIndex] = temp; - - return new AbstractStack(newStack); + x++; + int posX = (tail - x + STACK_LIMIT) % STACK_LIMIT; // Index of the element to swap with + int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; + + AbstractStack clone = clone(); + StackElement temp = clone.circularArray[posX]; + clone.circularArray[posX] = clone.circularArray[topIndex]; + clone.circularArray[topIndex] = temp; + return clone; } } \ No newline at end of file From 5dfee670ef701b041deed23f343c3eed4d01adda Mon Sep 17 00:00:00 2001 From: Shivam Kumar Date: Sun, 16 Mar 2025 22:21:55 +0100 Subject: [PATCH 02/14] Apply spotless --- .../java/it/unipr/analysis/AbstractStack.java | 38 ++++++++++--------- 1 file changed, 21 insertions(+), 17 deletions(-) diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java index 1ed3920de..33219fab1 100644 --- a/src/main/java/it/unipr/analysis/AbstractStack.java +++ b/src/main/java/it/unipr/analysis/AbstractStack.java @@ -154,10 +154,10 @@ public AbstractStack bottom() { @Override public boolean isTop() { - if(isBottom()) + if (isBottom()) return false; - for(StackElement element : this.circularArray) - if(!element.isTop()) + for (StackElement element : this.circularArray) + if (!element.isTop()) return false; return true; } @@ -195,10 +195,11 @@ public boolean equals(Object obj) { * Get a specific element of the stack. * * @param index the index of the element + * * @return the StackElement at the given index, or BOTTOM if out of bounds */ public StackElement get(int index) { - if(index < 0 || index >= STACK_LIMIT) // not valid index + if (index < 0 || index >= STACK_LIMIT) // not valid index return StackElement.BOTTOM; return circularArray[(head + index) % STACK_LIMIT]; } @@ -220,7 +221,7 @@ public StackElement getTop() { @Override public AbstractStack clone() { - if(isBottom() || isTop()) + if (isBottom() || isTop()) return this; AbstractStack clone = new AbstractStack(circularArray.clone()); clone.head = this.head; @@ -231,9 +232,10 @@ public AbstractStack clone() { /** * Pushes the specified element onto the stack. *

- * This method inserts the given {@link StackElement} at the tail of the circular array, - * effectively updating the top of the stack. The head of the stack is also updated - * to maintain the circular nature of the structure. + * This method inserts the given {@link StackElement} at the tail of the + * circular array, effectively updating the top of the stack. The head of + * the stack is also updated to maintain the circular nature of the + * structure. * * @param element the element to be pushed onto the stack */ @@ -246,10 +248,10 @@ public void push(StackElement element) { /** * Pops the element from the stack. *

- * This method removes and returns the topmost element of the stack. - * After popping, the stack structure is adjusted by shifting the head, - * and the previous bottommost element is updated based on the next element. - * If the next element is {@link StackElement#TOP}, the bottom is set to TOP, + * This method removes and returns the topmost element of the stack. After + * popping, the stack structure is adjusted by shifting the head, and the + * previous bottommost element is updated based on the next element. If the + * next element is {@link StackElement#TOP}, the bottom is set to TOP, * otherwise, it is set to {@link StackElement#BOTTOM}. * * @return the element at the top of the stack before popping @@ -292,10 +294,10 @@ public AbstractStack glbAux(AbstractStack other) throws SemanticException { @Override public boolean lessOrEqualAux(AbstractStack other) throws SemanticException { - for(int i = 0; i < STACK_LIMIT; i++) { + for (int i = 0; i < STACK_LIMIT; i++) { int thisIndex = (tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; int otherIndex = (other.tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; - if(!this.circularArray[thisIndex].lessOrEqual(other.circularArray[otherIndex])) + if (!this.circularArray[thisIndex].lessOrEqual(other.circularArray[otherIndex])) return false; } return true; @@ -348,9 +350,9 @@ public static int getStackLimit() { */ public boolean hasBottomUntil(int x) { - for(int i = 0; i < x; i++) { + for (int i = 0; i < x; i++) { int pos = (tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; - if(circularArray[pos].isBottom()) + if (circularArray[pos].isBottom()) return true; } return false; @@ -391,7 +393,9 @@ public AbstractStack swapX(int x) { if (hasBottomUntil(x + 1)) return bottom(); x++; - int posX = (tail - x + STACK_LIMIT) % STACK_LIMIT; // Index of the element to swap with + int posX = (tail - x + STACK_LIMIT) % STACK_LIMIT; // Index of the + // element to swap + // with int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; AbstractStack clone = clone(); From 9c2e5d13f9d81b3c6e072041ec198536c24b5a7c Mon Sep 17 00:00:00 2001 From: Shivam Kumar Date: Mon, 17 Mar 2025 12:27:19 +0100 Subject: [PATCH 03/14] Added popX method + javadoc --- .../java/it/unipr/analysis/AbstractStack.java | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java index f15ac9f64..0fcf6163a 100644 --- a/src/main/java/it/unipr/analysis/AbstractStack.java +++ b/src/main/java/it/unipr/analysis/AbstractStack.java @@ -277,15 +277,14 @@ public StackElement pop() { return popped; } + /** + * Performs {@code pos} consecutive {@code pop()} operations on the stack. + * + * @param pos the number of elements to pop from the stack + */ public void popX(int pos) { - // Shift all elements pos position to the right - System.arraycopy(stack, 0, stack, pos, STACK_LIMIT - pos); - - for (int i = 1; i < pos; i++) - if (!stack[i].isTop()) - stack[i - 1] = StackElement.BOTTOM; - else - stack[i - 1] = StackElement.TOP; + for (int i = 0; i < pos; i++) + pop(); } @Override @@ -415,4 +414,5 @@ public AbstractStack swapX(int x) { clone.circularArray[topIndex] = temp; return clone; } + } \ No newline at end of file From 68dd9d107530626454186bfc8b0bde5e48fe072d Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Mon, 17 Mar 2025 14:00:36 +0100 Subject: [PATCH 04/14] Refactoring AbstractStack's equals --- .../java/it/unipr/analysis/AbstractStack.java | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java index 0fcf6163a..e7e8d5a75 100644 --- a/src/main/java/it/unipr/analysis/AbstractStack.java +++ b/src/main/java/it/unipr/analysis/AbstractStack.java @@ -1,5 +1,8 @@ package it.unipr.analysis; +import java.util.Arrays; +import java.util.function.Predicate; + import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.ScopeToken; @@ -12,9 +15,6 @@ import it.unive.lisa.symbolic.value.ValueExpression; import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; -import java.util.Arrays; -import java.util.Objects; -import java.util.function.Predicate; public class AbstractStack implements ValueDomain, BaseLattice { @@ -169,7 +169,7 @@ public boolean isBottom() { @Override public int hashCode() { - return Objects.hash(Arrays.hashCode(circularArray)); + return Arrays.hashCode(circularArray); } @Override @@ -182,13 +182,7 @@ public boolean equals(Object obj) { return false; AbstractStack other = (AbstractStack) obj; - if (isBottom() || other.isBottom()) - return isBottom() == other.isBottom(); - for (int i = 0; i < STACK_LIMIT; i++) - if (!get(i).equals(other.get(i))) - return false; - - return true; + return Arrays.equals(this.circularArray, other.circularArray); } /** From 461a639267e6dbdaaabf4e5843074e3915ef7586 Mon Sep 17 00:00:00 2001 From: Shivam Kumar Date: Mon, 17 Mar 2025 14:42:35 +0100 Subject: [PATCH 05/14] Added javadoc --- .../java/it/unipr/analysis/AbstractStack.java | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java index 0fcf6163a..466c3ca1b 100644 --- a/src/main/java/it/unipr/analysis/AbstractStack.java +++ b/src/main/java/it/unipr/analysis/AbstractStack.java @@ -37,8 +37,21 @@ public class AbstractStack implements ValueDomain, BaseLattice + * This pointer indicates the position in the array that corresponds to the bottom of the stack. + * Tracks the index of the oldest element in the circular array. + */ + private int head; + + /** + * The index representing the next insertion point in the circular array. + *

+ * This pointer is used to identify the top of the stack, where the next element will be pushed. + */ + private int tail; /** * Helper method to create and fill an array with a specific element. From 5403bc5598f5955cfe92eb3b3b250e328400cd9b Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Mon, 17 Mar 2025 15:39:23 +0100 Subject: [PATCH 06/14] Updating tests --- evm-testcases/cfs/while/report.json | 6 +++--- ...ped_program.evm-testcases_cfs_while_while_eth.sol().json | 2 +- evm-testcases/cfs/while_npbj/report.json | 6 +++--- ...m.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/evm-testcases/cfs/while/report.json b/evm-testcases/cfs/while/report.json index 68da929f8..510c9c890 100644 --- a/evm-testcases/cfs/while/report.json +++ b/evm-testcases/cfs/while/report.json @@ -3,14 +3,14 @@ "files" : [ "report.json", "untyped_program.evm-testcases_cfs_while_while_eth.sol().json" ], "info" : { "cfgs" : "1", - "duration" : "23ms", - "end" : "2025-02-26T11:44:06.360+01:00", + "duration" : "281ms", + "end" : "2025-03-17T15:38:36.216+01:00", "expressions" : "6", "files" : "1", "globals" : "0", "members" : "1", "programs" : "1", - "start" : "2025-02-26T11:44:06.337+01:00", + "start" : "2025-03-17T15:38:35.935+01:00", "statements" : "16", "units" : "0", "version" : "0.1", diff --git a/evm-testcases/cfs/while/untyped_program.evm-testcases_cfs_while_while_eth.sol().json b/evm-testcases/cfs/while/untyped_program.evm-testcases_cfs_while_while_eth.sol().json index 619f5aa3f..285e7d7a0 100644 --- a/evm-testcases/cfs/while/untyped_program.evm-testcases_cfs_while_while_eth.sol().json +++ b/evm-testcases/cfs/while/untyped_program.evm-testcases_cfs_while_while_eth.sol().json @@ -1 +1 @@ -{"name":"untyped program::evm-testcases/cfs/while/while_eth.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x00"},{"id":1,"text":"0x00"},{"id":2,"text":"JUMPDEST"},{"id":3,"subNodes":[4],"text":"PUSH1 0x03"},{"id":4,"text":"0x03"},{"id":5,"text":"DUP2"},{"id":6,"text":"LT"},{"id":7,"subNodes":[8],"text":"PUSH1 0x0D"},{"id":8,"text":"0x0D"},{"id":9,"text":"JUMPI"},{"id":10,"subNodes":[11],"text":"PUSH1 0x14"},{"id":11,"text":"0x14"},{"id":12,"text":"JUMP"},{"id":13,"text":"JUMPDEST"},{"id":14,"subNodes":[15],"text":"PUSH1 0x01"},{"id":15,"text":"0x01"},{"id":16,"text":"ADD"},{"id":17,"subNodes":[18],"text":"PUSH1 0x02"},{"id":18,"text":"0x02"},{"id":19,"text":"JUMP"},{"id":20,"text":"JUMPDEST"},{"id":21,"text":"STOP"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":10,"kind":"FalseEdge"},{"sourceId":9,"destId":13,"kind":"TrueEdge"},{"sourceId":10,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":20,"kind":"SequentialEdge"},{"sourceId":13,"destId":14,"kind":"SequentialEdge"},{"sourceId":14,"destId":16,"kind":"SequentialEdge"},{"sourceId":16,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":19,"kind":"SequentialEdge"},{"sourceId":19,"destId":2,"kind":"SequentialEdge"},{"sourceId":20,"destId":21,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":1,"description":{"expressions":["\"0x00\""],"state":"#TOP#"}},{"nodeId":2,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":3,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":4,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":5,"description":{"expressions":["dup2 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":6,"description":{"expressions":["lt 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":7,"description":{"expressions":["push \"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 13]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":8,"description":{"expressions":["\"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":9,"description":{"expressions":["jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]],[[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":10,"description":{"expressions":["push \"0x14\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 20]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":11,"description":{"expressions":["\"0x14\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":12,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":13,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":14,"description":{"expressions":["push \"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":15,"description":{"expressions":["\"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":16,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":17,"description":{"expressions":["push \"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":18,"description":{"expressions":["\"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":19,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":20,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":21,"description":"#TOP#"}]} \ No newline at end of file +{"name":"untyped program::evm-testcases/cfs/while/while_eth.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x00"},{"id":1,"text":"0x00"},{"id":2,"text":"JUMPDEST"},{"id":3,"subNodes":[4],"text":"PUSH1 0x03"},{"id":4,"text":"0x03"},{"id":5,"text":"DUP2"},{"id":6,"text":"LT"},{"id":7,"subNodes":[8],"text":"PUSH1 0x0D"},{"id":8,"text":"0x0D"},{"id":9,"text":"JUMPI"},{"id":10,"subNodes":[11],"text":"PUSH1 0x14"},{"id":11,"text":"0x14"},{"id":12,"text":"JUMP"},{"id":13,"text":"JUMPDEST"},{"id":14,"subNodes":[15],"text":"PUSH1 0x01"},{"id":15,"text":"0x01"},{"id":16,"text":"ADD"},{"id":17,"subNodes":[18],"text":"PUSH1 0x02"},{"id":18,"text":"0x02"},{"id":19,"text":"JUMP"},{"id":20,"text":"JUMPDEST"},{"id":21,"text":"STOP"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":10,"kind":"FalseEdge"},{"sourceId":9,"destId":13,"kind":"TrueEdge"},{"sourceId":10,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":20,"kind":"SequentialEdge"},{"sourceId":13,"destId":14,"kind":"SequentialEdge"},{"sourceId":14,"destId":16,"kind":"SequentialEdge"},{"sourceId":16,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":19,"kind":"SequentialEdge"},{"sourceId":19,"destId":2,"kind":"SequentialEdge"},{"sourceId":20,"destId":21,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":1,"description":{"expressions":["\"0x00\""],"state":"#TOP#"}},{"nodeId":2,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":3,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":4,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":5,"description":{"expressions":["dup2 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":6,"description":{"expressions":["lt 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":7,"description":{"expressions":["push \"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 13]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":8,"description":{"expressions":["\"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":9,"description":{"expressions":["jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":10,"description":{"expressions":["push \"0x14\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 20]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":11,"description":{"expressions":["\"0x14\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":12,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":13,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":14,"description":{"expressions":["push \"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":15,"description":{"expressions":["\"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":16,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":17,"description":{"expressions":["push \"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":18,"description":{"expressions":["\"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":19,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":20,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":21,"description":"#TOP#"}]} \ No newline at end of file diff --git a/evm-testcases/cfs/while_npbj/report.json b/evm-testcases/cfs/while_npbj/report.json index 5c4d391d7..314a4d072 100644 --- a/evm-testcases/cfs/while_npbj/report.json +++ b/evm-testcases/cfs/while_npbj/report.json @@ -3,14 +3,14 @@ "files" : [ "report.json", "untyped_program.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json" ], "info" : { "cfgs" : "1", - "duration" : "116ms", - "end" : "2025-02-26T11:44:06.312+01:00", + "duration" : "416ms", + "end" : "2025-03-17T15:37:51.705+01:00", "expressions" : "9", "files" : "1", "globals" : "0", "members" : "1", "programs" : "1", - "start" : "2025-02-26T11:44:06.196+01:00", + "start" : "2025-03-17T15:37:51.289+01:00", "statements" : "22", "units" : "0", "version" : "0.1", diff --git a/evm-testcases/cfs/while_npbj/untyped_program.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json b/evm-testcases/cfs/while_npbj/untyped_program.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json index 8ebbaca20..d18444cf1 100644 --- a/evm-testcases/cfs/while_npbj/untyped_program.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json +++ b/evm-testcases/cfs/while_npbj/untyped_program.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json @@ -1 +1 @@ -{"name":"untyped program::evm-testcases/cfs/while_npbj/while_npbj_eth.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x00"},{"id":1,"text":"0x00"},{"id":2,"text":"JUMPDEST"},{"id":3,"subNodes":[4],"text":"PUSH1 0x03"},{"id":4,"text":"0x03"},{"id":5,"text":"DUP2"},{"id":6,"text":"LT"},{"id":7,"subNodes":[8],"text":"PUSH1 0x10"},{"id":8,"text":"0x10"},{"id":9,"subNodes":[10],"text":"PUSH1 0x03"},{"id":10,"text":"0x03"},{"id":11,"text":"ADD"},{"id":12,"text":"JUMPI"},{"id":13,"subNodes":[14],"text":"PUSH1 0x10"},{"id":14,"text":"0x10"},{"id":15,"subNodes":[16],"text":"PUSH1 0x0D"},{"id":16,"text":"0x0D"},{"id":17,"text":"ADD"},{"id":18,"text":"JUMP"},{"id":19,"text":"JUMPDEST"},{"id":20,"subNodes":[21],"text":"PUSH1 0x01"},{"id":21,"text":"0x01"},{"id":22,"text":"ADD"},{"id":23,"subNodes":[24],"text":"PUSH1 0x00"},{"id":24,"text":"0x00"},{"id":25,"subNodes":[26],"text":"PUSH1 0x02"},{"id":26,"text":"0x02"},{"id":27,"text":"ADD"},{"id":28,"text":"JUMP"},{"id":29,"text":"JUMPDEST"},{"id":30,"text":"STOP"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":11,"kind":"SequentialEdge"},{"sourceId":11,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":13,"kind":"FalseEdge"},{"sourceId":12,"destId":19,"kind":"TrueEdge"},{"sourceId":13,"destId":15,"kind":"SequentialEdge"},{"sourceId":15,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":18,"kind":"SequentialEdge"},{"sourceId":18,"destId":29,"kind":"SequentialEdge"},{"sourceId":19,"destId":20,"kind":"SequentialEdge"},{"sourceId":20,"destId":22,"kind":"SequentialEdge"},{"sourceId":22,"destId":23,"kind":"SequentialEdge"},{"sourceId":23,"destId":25,"kind":"SequentialEdge"},{"sourceId":25,"destId":27,"kind":"SequentialEdge"},{"sourceId":27,"destId":28,"kind":"SequentialEdge"},{"sourceId":28,"destId":2,"kind":"SequentialEdge"},{"sourceId":29,"destId":30,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":1,"description":{"expressions":["\"0x00\""],"state":"#TOP#"}},{"nodeId":2,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":3,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":4,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":5,"description":{"expressions":["dup2 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":6,"description":{"expressions":["lt 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":7,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":8,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":9,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":10,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":11,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 19]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":12,"description":{"expressions":["jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]],[[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":13,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":14,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":15,"description":{"expressions":["push \"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16, 13]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":16,"description":{"expressions":["\"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":17,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 29]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":18,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":19,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":20,"description":{"expressions":["push \"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":21,"description":{"expressions":["\"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":22,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":23,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":24,"description":{"expressions":["\"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":25,"description":{"expressions":["push \"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":26,"description":{"expressions":["\"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":27,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":28,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":29,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":30,"description":"#TOP#"}]} \ No newline at end of file +{"name":"untyped program::evm-testcases/cfs/while_npbj/while_npbj_eth.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x00"},{"id":1,"text":"0x00"},{"id":2,"text":"JUMPDEST"},{"id":3,"subNodes":[4],"text":"PUSH1 0x03"},{"id":4,"text":"0x03"},{"id":5,"text":"DUP2"},{"id":6,"text":"LT"},{"id":7,"subNodes":[8],"text":"PUSH1 0x10"},{"id":8,"text":"0x10"},{"id":9,"subNodes":[10],"text":"PUSH1 0x03"},{"id":10,"text":"0x03"},{"id":11,"text":"ADD"},{"id":12,"text":"JUMPI"},{"id":13,"subNodes":[14],"text":"PUSH1 0x10"},{"id":14,"text":"0x10"},{"id":15,"subNodes":[16],"text":"PUSH1 0x0D"},{"id":16,"text":"0x0D"},{"id":17,"text":"ADD"},{"id":18,"text":"JUMP"},{"id":19,"text":"JUMPDEST"},{"id":20,"subNodes":[21],"text":"PUSH1 0x01"},{"id":21,"text":"0x01"},{"id":22,"text":"ADD"},{"id":23,"subNodes":[24],"text":"PUSH1 0x00"},{"id":24,"text":"0x00"},{"id":25,"subNodes":[26],"text":"PUSH1 0x02"},{"id":26,"text":"0x02"},{"id":27,"text":"ADD"},{"id":28,"text":"JUMP"},{"id":29,"text":"JUMPDEST"},{"id":30,"text":"STOP"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":11,"kind":"SequentialEdge"},{"sourceId":11,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":13,"kind":"FalseEdge"},{"sourceId":12,"destId":19,"kind":"TrueEdge"},{"sourceId":13,"destId":15,"kind":"SequentialEdge"},{"sourceId":15,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":18,"kind":"SequentialEdge"},{"sourceId":18,"destId":29,"kind":"SequentialEdge"},{"sourceId":19,"destId":20,"kind":"SequentialEdge"},{"sourceId":20,"destId":22,"kind":"SequentialEdge"},{"sourceId":22,"destId":23,"kind":"SequentialEdge"},{"sourceId":23,"destId":25,"kind":"SequentialEdge"},{"sourceId":25,"destId":27,"kind":"SequentialEdge"},{"sourceId":27,"destId":28,"kind":"SequentialEdge"},{"sourceId":28,"destId":2,"kind":"SequentialEdge"},{"sourceId":29,"destId":30,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":1,"description":{"expressions":["\"0x00\""],"state":"#TOP#"}},{"nodeId":2,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":3,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":4,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":5,"description":{"expressions":["dup2 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":6,"description":{"expressions":["lt 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":7,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":8,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":9,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":10,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":11,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 19]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":12,"description":{"expressions":["jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":13,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":14,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":15,"description":{"expressions":["push \"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16, 13]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":16,"description":{"expressions":["\"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":17,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 29]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":18,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":19,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":20,"description":{"expressions":["push \"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":21,"description":{"expressions":["\"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":22,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":23,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":24,"description":{"expressions":["\"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":25,"description":{"expressions":["push \"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":26,"description":{"expressions":["\"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":27,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":28,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":29,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":30,"description":"#TOP#"}]} \ No newline at end of file From f3cd70d0197d38ed7a38fc2efbff114174269feb Mon Sep 17 00:00:00 2001 From: Shivam Kumar Date: Thu, 20 Mar 2025 11:29:35 +0100 Subject: [PATCH 07/14] Refactored stack structure from ArrayList to circular array --- .../analysis/taint/TaintAbstractDomain.java | 262 +++++++++--------- .../TimestampDependencyAbstractDomain.java | 33 ++- .../taint/TxOriginAbstractDomain.java | 27 +- 3 files changed, 170 insertions(+), 152 deletions(-) diff --git a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java index 7ad3daaab..1da7aa379 100644 --- a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java @@ -1,5 +1,6 @@ package it.unipr.analysis.taint; +import it.unipr.analysis.StackElement; import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.ScopeToken; @@ -17,11 +18,8 @@ import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator; import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; -import java.util.ArrayList; -import java.util.Iterator; -import java.util.List; -import java.util.Objects; -import java.util.Set; + +import java.util.*; import java.util.function.Predicate; public abstract class TaintAbstractDomain @@ -33,9 +31,19 @@ public abstract class TaintAbstractDomain protected static int STACK_LIMIT = 32; /** - * The abstract stack domain. + * The abstract stack as a circular array. */ - private final ArrayList stack; + private final TaintElement[] circularArray; + + /** + * The index representing the beginning of the logical stack. + */ + private int head; + + /** + * The index representing the next insertion point. + */ + private int tail; /** * The local memory, tracking if it is clean or tainted. @@ -46,11 +54,14 @@ public abstract class TaintAbstractDomain * Builds a taint abstract stack starting from a given stack and a list of * elements that push taint. * - * @param stack the stack of values + * @param circularArray the stack of values */ - protected TaintAbstractDomain(ArrayList stack, TaintElement memory) { - this.stack = stack; + protected TaintAbstractDomain(TaintElement[] circularArray, TaintElement memory) { + this.circularArray = circularArray; this.memory = memory; + // TODO: CHECK + this.head = 0; + this.tail = 0; } @Override @@ -188,7 +199,7 @@ else if (memory.isClean()) TaintElement value = resultStack.pop(); if (value.isTaint()) - return mk(resultStack.stack, TaintElement.TAINT); + return mk(resultStack.circularArray, TaintElement.TAINT); // TODO: CHECK else if (value.isClean()) return resultStack; } @@ -624,73 +635,42 @@ else if (value.isClean()) private TaintAbstractDomain dupXoperator(int x, TaintAbstractDomain stack) { if (stack.isEmpty() || stack.hasBottomUntil(x)) return bottom(); - return dupX(x, stack.clone()); + return stack.dupX(x); } private TaintAbstractDomain swapXoperator(int x, TaintAbstractDomain stack) { - if (stack.isEmpty() || stack.hasBottomUntil(x)) + if (stack.isEmpty() || stack.hasBottomUntil(x + 1)) return bottom(); - return swapX(x, stack.clone()); + return stack.swapX(x); } - private TaintAbstractDomain swapX(int x, TaintAbstractDomain stack) { - List clone = stack.clone().getStack(); - - if (stack.size() < x + 1 || x < 1) - return stack.bottom(); - - Object[] obj = clone.toArray(); - int first; - - if (stack.size() < STACK_LIMIT) - first = STACK_LIMIT - 1; - else - first = clone.size() - 1; - - Object tmp = obj[first]; - obj[first] = obj[first - x]; - obj[first - x] = tmp; - - ArrayList result = new ArrayList<>(); - - for (int i = 0; i < clone.size(); i++) - result.add((TaintElement) obj[i]); - - return mk(result, stack.memory); + public TaintAbstractDomain swapX(int x) { + if (hasBottomUntil(x + 1)) + return bottom(); + x++; + int posX = (tail - x + STACK_LIMIT) % STACK_LIMIT; + int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; + TaintAbstractDomain copy = this.clone(); + TaintElement tmp = copy.circularArray[posX]; + copy.circularArray[posX] = copy.circularArray[topIndex]; + copy.circularArray[topIndex] = tmp; + return copy; } - private TaintAbstractDomain dupX(int x, TaintAbstractDomain stack) { - List clone = stack.clone().getStack(); - - if (stack.size() < x || x < 1) - return stack.bottom(); - - Object[] obj = clone.toArray(); - - int first; - if (stack.size() < STACK_LIMIT) - first = STACK_LIMIT; - else - first = clone.size(); - - TaintElement tmp = (TaintElement) obj[first - x]; - - ArrayList result = new ArrayList<>(); - - for (int i = 0; i < clone.size(); i++) - result.add((TaintElement) obj[i]); - - result.add(tmp); - result.remove(0); - - return mk(result, stack.memory); + public TaintAbstractDomain dupX(int x) { + if (hasBottomUntil(x)) + return bottom(); + int posX = (tail - x + STACK_LIMIT) % STACK_LIMIT; + TaintAbstractDomain copy = this.clone(); + copy.push(circularArray[posX]); + return copy; } - private ArrayList getStack() { + /*private ArrayList getStack() { return stack; - } + }*/ - private int size() { + /*private int size() { int bottomCounter = 0; for (TaintElement item : stack) { if (item.isBottom()) { @@ -698,13 +678,10 @@ private int size() { } } return stack.size() - bottomCounter; - } + }*/ - private boolean isEmpty() { - if (!stack.isEmpty()) - return false; - else - return true; + public boolean isEmpty() { // TODO: CHECK + return getFirstElement().isBottom(); } @Override @@ -746,17 +723,24 @@ public StructuredRepresentation representation() { else if (isTop()) return Lattice.topRepresentation(); - return new StringRepresentation(stack.toString()); + return new StringRepresentation(this.toString()); } @Override public String toString() { if (isBottom()) return Lattice.BOTTOM_STRING; - else if (isTop()) + if (isTop()) return Lattice.TOP_STRING; - - return stack.toString(); + StringBuilder sb = new StringBuilder("["); + for (int i = 0; i < STACK_LIMIT; i++) { + int pos = (head + i) % STACK_LIMIT; + sb.append(circularArray[pos]); + if (i < STACK_LIMIT - 1) + sb.append(", "); + } + sb.append("]"); + return sb.toString(); } @Override @@ -773,46 +757,33 @@ public TaintAbstractDomain popScope(ScopeToken token) throws SemanticException { @Override public TaintAbstractDomain glbAux(TaintAbstractDomain other) throws SemanticException { - ArrayList result = new ArrayList<>(STACK_LIMIT); - - Iterator thisIterator = this.stack.iterator(); - Iterator otherIterator = other.stack.iterator(); - - while (thisIterator.hasNext() && otherIterator.hasNext()) { - TaintElement thisElement = thisIterator.next(); - TaintElement otherElement = otherIterator.next(); - result.add(thisElement.glb(otherElement)); + TaintElement[] result = new TaintElement[STACK_LIMIT]; + for (int i = 0; i < STACK_LIMIT; i++) { + result[i] = this.get(i).glb(other.get(i)); } - return mk(result, this.memory.glb(other.memory)); } @Override public TaintAbstractDomain lubAux(TaintAbstractDomain other) throws SemanticException { - ArrayList result = new ArrayList<>(STACK_LIMIT); - - Iterator thisIterator = this.stack.iterator(); - Iterator otherIterator = other.stack.iterator(); - - while (thisIterator.hasNext() && otherIterator.hasNext()) { - TaintElement thisElement = thisIterator.next(); - TaintElement otherElement = otherIterator.next(); - result.add(thisElement.lub(otherElement)); + TaintElement[] result = new TaintElement[STACK_LIMIT]; + for (int i = 0; i < STACK_LIMIT; i++) { + result[i] = this.get(i).lub(other.get(i)); } - return mk(result, this.memory.lub(other.memory)); } + public TaintElement get(int index) { + if (index < 0 || index >= STACK_LIMIT) + return TaintElement.BOTTOM; + return circularArray[(head + index) % STACK_LIMIT]; + } + @Override public boolean lessOrEqualAux(TaintAbstractDomain other) throws SemanticException { - Iterator thisIterator = this.stack.iterator(); - Iterator otherIterator = other.stack.iterator(); - - while (thisIterator.hasNext() && otherIterator.hasNext()) { - if (!thisIterator.next().lessOrEqual(otherIterator.next())) { + for (int i = 0; i < STACK_LIMIT; i++) + if (!this.get(i).lessOrEqual(other.get(i))) return false; - } - } return true; } @@ -823,8 +794,9 @@ public boolean lessOrEqualAux(TaintAbstractDomain other) throws SemanticExceptio * @param target the element to be pushed onto the stack. */ public void push(TaintElement target) { - stack.remove(0); - stack.add(target); + circularArray[tail] = target; + tail = (tail + 1) % STACK_LIMIT; + head = (head + 1) % STACK_LIMIT; } /** @@ -832,14 +804,23 @@ public void push(TaintElement target) { * * @return the element at the top of the stack. */ + public TaintElement pop() { - TaintElement result = stack.remove(stack.size() - 1); - if (stack.get(0).isBottom()) - stack.add(0, TaintElement.BOTTOM); + int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; + TaintElement popped = circularArray[topIndex]; + + head = (head - 1 + STACK_LIMIT) % STACK_LIMIT; + int bottomIndex = head; + int nextIndex = (head + 1) % STACK_LIMIT; + + if (circularArray[nextIndex].isTop()) + circularArray[bottomIndex] = TaintElement.TOP; else - stack.add(0, TaintElement.TOP); + circularArray[bottomIndex] = TaintElement.BOTTOM; + tail = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; + circularArray[topIndex] = TaintElement.BOTTOM; - return result; + return popped; } /** @@ -853,55 +834,77 @@ public TaintElement pop() { * is bottom, {@code false} otherwise. */ public boolean hasBottomUntil(int x) { - for (int i = 0; i < x; i++) - if (this.stack.get((STACK_LIMIT - 1) - i).isBottom()) + for (int i = 0; i < x; i++) { + int index = (tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; + if (circularArray[index].isBottom()) return true; + } return false; } + @Override public TaintAbstractDomain clone() { - if (isBottom()) - return this; - return mk(new ArrayList<>(stack), this.memory); + TaintElement[] newArray = Arrays.copyOf(circularArray, STACK_LIMIT); + TaintAbstractDomain copy = mk(newArray, memory); + copy.head = this.head; + copy.tail = this.tail; + return copy; } @Override public boolean equals(Object obj) { if (this == obj) return true; - if (obj == null) - return false; - if (getClass() != obj.getClass()) + if (!(obj instanceof TaintAbstractDomain)) return false; TaintAbstractDomain other = (TaintAbstractDomain) obj; - return Objects.equals(memory, other.memory) && Objects.equals(stack, other.stack); + + if (isBottom() || other.isBottom()) + return isBottom() == other.isBottom(); + + if (!memory.equals(other.memory)) + return false; + + for (int i = 0; i < STACK_LIMIT; i++) + if (!get(i).equals(other.get(i))) + return false; + + return true; } + @Override public int hashCode() { - return Objects.hash(memory, stack); + return Arrays.hashCode(circularArray) + memory.hashCode(); } public TaintElement getSecondElement() { if (isBottom()) return TaintElement.BOTTOM; - else if (isTop()) + if (isTop()) return TaintElement.TOP; - return this.stack.get(STACK_LIMIT - 2); + return circularArray[(tail - 2 + STACK_LIMIT) % STACK_LIMIT]; } public TaintElement getFirstElement() { if (isBottom()) return TaintElement.BOTTOM; - else if (isTop()) + if (isTop()) return TaintElement.TOP; - return this.stack.get(STACK_LIMIT - 1); + return circularArray[(tail - 1 + STACK_LIMIT) % STACK_LIMIT]; } + /** + * @return copy of the array + */ + /*protected TaintElement[] getArrayCopy() { // TODO: CHECK + return Arrays.copyOf(circularArray, STACK_LIMIT); + }*/ + /** * Yields the set of opcodes that push taint elements. - * + * * @return the set of opcodes that push taint elements */ public abstract Set getTaintedOpcode(); @@ -916,12 +919,13 @@ else if (isTop()) /** * Utility for creating a concrete instance of {@link TaintAbstractDomain} * given the stack and the memory. - * - * @param list the stack + * + * @param array the stack // TODO: CHECK * @param memory the memory - * + * * @return a new concrete instance of {@link TaintAbstractDomain} */ - public abstract TaintAbstractDomain mk(ArrayList list, TaintElement memory); + //public abstract TaintAbstractDomain mk(ArrayList list, TaintElement memory); // TODO: CHECK + public abstract TaintAbstractDomain mk(TaintElement[] array, TaintElement memory); } \ No newline at end of file diff --git a/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java index 8c0cd8595..9623098ef 100644 --- a/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java @@ -1,37 +1,42 @@ package it.unipr.analysis.taint; +import it.unipr.analysis.StackElement; import it.unipr.analysis.operator.BalanceOperator; import it.unipr.analysis.operator.BlockhashOperator; import it.unipr.analysis.operator.DifficultyOperator; import it.unipr.analysis.operator.TimestampOperator; import it.unive.lisa.symbolic.value.Operator; -import java.util.ArrayList; -import java.util.Collections; -import java.util.HashSet; -import java.util.Set; + +import java.util.*; public class TimestampDependencyAbstractDomain extends TaintAbstractDomain { private static final TimestampDependencyAbstractDomain TOP = new TimestampDependencyAbstractDomain( - new ArrayList<>(Collections.nCopies(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM)), - TaintElement.CLEAN); - private static final TimestampDependencyAbstractDomain BOTTOM = new TimestampDependencyAbstractDomain(null, - TaintElement.BOTTOM); + createFilledArray(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); + private static final TimestampDependencyAbstractDomain BOTTOM = + new TimestampDependencyAbstractDomain(null, TaintElement.BOTTOM); + + + private static TaintElement[] createFilledArray(int size, TaintElement element) { + TaintElement[] array = new TaintElement[size]; + Arrays.fill(array, element); + return array; + } /** * Builds an initial symbolic stack. */ public TimestampDependencyAbstractDomain() { - this(new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM)), TaintElement.CLEAN); + this(createFilledArray(STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); } /** * Builds a taint abstract stack starting from a given stack and a list of * elements that push taint. * - * @param stack the stack of values + * @param circularArray the stack of values */ - protected TimestampDependencyAbstractDomain(ArrayList stack, TaintElement memory) { - super(stack, memory); + protected TimestampDependencyAbstractDomain(TaintElement[] circularArray, TaintElement memory) { + super(circularArray, memory); } @Override @@ -60,8 +65,8 @@ public TimestampDependencyAbstractDomain bottom() { } @Override - public TaintAbstractDomain mk(ArrayList list, TaintElement memory) { - return new TimestampDependencyAbstractDomain(list, memory); + public TaintAbstractDomain mk(TaintElement[] array, TaintElement memory) { + return new TimestampDependencyAbstractDomain(array, memory); } } \ No newline at end of file diff --git a/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java index 7a66d56db..f2e3325b2 100644 --- a/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java @@ -3,31 +3,40 @@ import it.unipr.analysis.operator.OriginOperator; import it.unive.lisa.symbolic.value.Operator; import java.util.ArrayList; +import java.util.Arrays; import java.util.Collections; import java.util.Set; public class TxOriginAbstractDomain extends TaintAbstractDomain { private static final TxOriginAbstractDomain TOP = new TxOriginAbstractDomain( - new ArrayList<>(Collections.nCopies(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM)), - TaintElement.CLEAN); - private static final TxOriginAbstractDomain BOTTOM = new TxOriginAbstractDomain(null, TaintElement.BOTTOM); + createFilledArray(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); + private static final TxOriginAbstractDomain BOTTOM = + new TxOriginAbstractDomain(null, TaintElement.BOTTOM); + + + private static TaintElement[] createFilledArray(int size, TaintElement element) { + TaintElement[] array = new TaintElement[size]; + Arrays.fill(array, element); + return array; + } + /** * Builds an initial symbolic stack. */ public TxOriginAbstractDomain() { - this(new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM)), TaintElement.CLEAN); + this(createFilledArray(STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); } /** * Builds a taint abstract stack starting from a given stack and a list of * elements that push taint. * - * @param stack the stack of values + * @param circularArray the stack of values */ - protected TxOriginAbstractDomain(ArrayList stack, TaintElement memory) { - super(stack, memory); + protected TxOriginAbstractDomain(TaintElement[] circularArray, TaintElement memory) { + super(circularArray, memory); } @Override @@ -51,7 +60,7 @@ public TxOriginAbstractDomain bottom() { } @Override - public TaintAbstractDomain mk(ArrayList list, TaintElement memory) { - return new TxOriginAbstractDomain(list, memory); + public TaintAbstractDomain mk(TaintElement[] array, TaintElement memory) { + return new TxOriginAbstractDomain(array, memory); } } From 7a9d589dc37993fc59711170f2ccb8ddfd3b03af Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Thu, 20 Mar 2025 13:48:10 +0100 Subject: [PATCH 08/14] Removed emptiness check in small-step semantics of TaintAbstractDomain --- .../analysis/taint/TaintAbstractDomain.java | 118 ++++-------------- 1 file changed, 27 insertions(+), 91 deletions(-) diff --git a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java index 1da7aa379..cccb182cf 100644 --- a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java @@ -1,6 +1,10 @@ package it.unipr.analysis.taint; -import it.unipr.analysis.StackElement; +import java.util.Arrays; +import java.util.Objects; +import java.util.Set; +import java.util.function.Predicate; + import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.ScopeToken; @@ -12,18 +16,14 @@ import it.unive.lisa.symbolic.value.Constant; import it.unive.lisa.symbolic.value.Identifier; import it.unive.lisa.symbolic.value.Operator; -import it.unive.lisa.symbolic.value.Skip; import it.unive.lisa.symbolic.value.UnaryExpression; import it.unive.lisa.symbolic.value.ValueExpression; import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator; import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; -import java.util.*; -import java.util.function.Predicate; - public abstract class TaintAbstractDomain - implements ValueDomain, BaseLattice { +implements ValueDomain, BaseLattice { /** * The stack limit. @@ -59,7 +59,7 @@ public abstract class TaintAbstractDomain protected TaintAbstractDomain(TaintElement[] circularArray, TaintElement memory) { this.circularArray = circularArray; this.memory = memory; - // TODO: CHECK + // TODO: CHECK this.head = 0; this.tail = 0; } @@ -267,11 +267,7 @@ else if (value.isClean()) return bottom(); TaintAbstractDomain resultStack = clone(); resultStack.pop(); - - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "SstoreOperator": { // pops 2 @@ -281,10 +277,7 @@ else if (value.isClean()) resultStack.pop(); resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "Dup1Operator": { // DUP1 @@ -390,10 +383,7 @@ else if (value.isClean()) TaintElement offset = resultStack.pop(); TaintElement length = resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "Log1Operator": { // LOG1 if (hasBottomUntil(3)) @@ -403,10 +393,7 @@ else if (value.isClean()) TaintElement length = resultStack.pop(); resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "Log2Operator": { // LOG2 if (hasBottomUntil(4)) @@ -417,10 +404,7 @@ else if (value.isClean()) resultStack.pop(); resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "Log3Operator": { // LOG3 if (hasBottomUntil(5)) @@ -432,10 +416,7 @@ else if (value.isClean()) resultStack.pop(); resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "Log4Operator": { // LOG4 if (hasBottomUntil(6)) @@ -448,10 +429,7 @@ else if (value.isClean()) resultStack.pop(); resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "CreateOperator": { // CREATE if (hasBottomUntil(3)) @@ -499,7 +477,7 @@ else if (value.isClean()) resultStack.push(TaintElement.TAINT); else resultStack - .push(TaintElement.semantics(gas, to, value, inOffset, inLength, outOffset, outLength)); + .push(TaintElement.semantics(gas, to, value, inOffset, inLength, outOffset, outLength)); return resultStack; } case "ReturnOperator": { // RETURN @@ -509,10 +487,7 @@ else if (value.isClean()) TaintElement offset = resultStack.pop(); TaintElement length = resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "DelegatecallOperator": case "StaticcallOperator": { // pops 6, push 1 @@ -539,10 +514,7 @@ else if (value.isClean()) TaintElement offset = resultStack.pop(); TaintElement length = resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "InvalidOperator": { // INVALID return this; @@ -553,10 +525,7 @@ else if (value.isClean()) TaintAbstractDomain resultStack = clone(); TaintElement recipient = resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "CodecopyOperator": { // CODECOPY if (hasBottomUntil(3)) @@ -566,10 +535,7 @@ else if (value.isClean()) TaintElement dataOffset = resultStack.pop(); TaintElement length = resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "ExtcodesizeOperator": { // EXTCODESIZE if (hasBottomUntil(1)) @@ -592,10 +558,7 @@ else if (value.isClean()) TaintElement dataOffset = resultStack.pop(); TaintElement length = resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "ReturndatacopyOperator": { // RETURNDATACOPY if (hasBottomUntil(3)) @@ -605,10 +568,7 @@ else if (value.isClean()) TaintElement dataOffset = resultStack.pop(); TaintElement length = resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "ExtcodehashOperator": { // EXTCODEHASH if (hasBottomUntil(1)) @@ -626,10 +586,7 @@ else if (value.isClean()) } } - if (!(expression instanceof Skip)) - throw new SemanticException("Reachable just with the skip node"); - - return top(); + throw new SemanticException("Unrecognized opcode: " + pp); } private TaintAbstractDomain dupXoperator(int x, TaintAbstractDomain stack) { @@ -643,6 +600,10 @@ private TaintAbstractDomain swapXoperator(int x, TaintAbstractDomain stack) { return bottom(); return stack.swapX(x); } + + public boolean isEmpty() { // TODO: CHECK + return getFirstElement().isBottom(); + } public TaintAbstractDomain swapX(int x) { if (hasBottomUntil(x + 1)) @@ -666,24 +627,6 @@ public TaintAbstractDomain dupX(int x) { return copy; } - /*private ArrayList getStack() { - return stack; - }*/ - - /*private int size() { - int bottomCounter = 0; - for (TaintElement item : stack) { - if (item.isBottom()) { - bottomCounter++; - } - } - return stack.size() - bottomCounter; - }*/ - - public boolean isEmpty() { // TODO: CHECK - return getFirstElement().isBottom(); - } - @Override public TaintAbstractDomain assume(ValueExpression expression, ProgramPoint src, ProgramPoint dest, SemanticOracle oracle) throws SemanticException { @@ -876,7 +819,7 @@ public boolean equals(Object obj) { @Override public int hashCode() { - return Arrays.hashCode(circularArray) + memory.hashCode(); + return Objects.hash(circularArray, memory); } public TaintElement getSecondElement() { @@ -895,13 +838,6 @@ public TaintElement getFirstElement() { return circularArray[(tail - 1 + STACK_LIMIT) % STACK_LIMIT]; } - /** - * @return copy of the array - */ - /*protected TaintElement[] getArrayCopy() { // TODO: CHECK - return Arrays.copyOf(circularArray, STACK_LIMIT); - }*/ - /** * Yields the set of opcodes that push taint elements. * From c528f2510e6d04e54a1fc114be362ea8f54f583e Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Thu, 20 Mar 2025 13:59:42 +0100 Subject: [PATCH 09/14] Changed equals for taint abstract domain --- .../java/it/unipr/analysis/taint/TaintAbstractDomain.java | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java index cccb182cf..675e9ac22 100644 --- a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java @@ -809,11 +809,7 @@ public boolean equals(Object obj) { if (!memory.equals(other.memory)) return false; - for (int i = 0; i < STACK_LIMIT; i++) - if (!get(i).equals(other.get(i))) - return false; - - return true; + return Arrays.equals(this.circularArray, other.circularArray); } @@ -861,7 +857,6 @@ public TaintElement getFirstElement() { * * @return a new concrete instance of {@link TaintAbstractDomain} */ - //public abstract TaintAbstractDomain mk(ArrayList list, TaintElement memory); // TODO: CHECK public abstract TaintAbstractDomain mk(TaintElement[] array, TaintElement memory); } \ No newline at end of file From 256a10f418463d248f49e06f090685322aeb9da9 Mon Sep 17 00:00:00 2001 From: Shivam Kumar Date: Thu, 20 Mar 2025 16:10:25 +0100 Subject: [PATCH 10/14] Added popX method and fix clone + javadoc --- .../analysis/taint/TaintAbstractDomain.java | 101 +++++++++++++++--- 1 file changed, 89 insertions(+), 12 deletions(-) diff --git a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java index 675e9ac22..03e85488b 100644 --- a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java @@ -5,6 +5,8 @@ import java.util.Set; import java.util.function.Predicate; +import it.unipr.analysis.AbstractStack; +import it.unipr.analysis.StackElement; import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.ScopeToken; @@ -36,12 +38,17 @@ public abstract class TaintAbstractDomain private final TaintElement[] circularArray; /** - * The index representing the beginning of the logical stack. + * The index representing the beginning of the logical stack in the circular array. + *

+ * This pointer indicates the position in the array that corresponds to the bottom of the stack. + * Tracks the index of the oldest element in the circular array. */ private int head; /** - * The index representing the next insertion point. + * The index representing the next insertion point in the circular array. + *

+ * This pointer is used to identify the top of the stack, where the next element will be pushed. */ private int tail; @@ -51,15 +58,14 @@ public abstract class TaintAbstractDomain private final TaintElement memory; /** - * Builds a taint abstract stack starting from a given stack and a list of - * elements that push taint. + * Builds a taint abstract stack starting from a given stack and a memory element. * * @param circularArray the stack of values + * @param memory the memory element */ protected TaintAbstractDomain(TaintElement[] circularArray, TaintElement memory) { this.circularArray = circularArray; this.memory = memory; - // TODO: CHECK this.head = 0; this.tail = 0; } @@ -600,11 +606,24 @@ private TaintAbstractDomain swapXoperator(int x, TaintAbstractDomain stack) { return bottom(); return stack.swapX(x); } - - public boolean isEmpty() { // TODO: CHECK + + /** + * Checks whether the stack is empty. + * + * @return {@code true} if the first element is bottom, {@code false} otherwise. + */ + public boolean isEmpty() { return getFirstElement().isBottom(); } + /** + * Swaps the 1st with the (x + 1)-th element from the top of the stack and + * returns the modified stack. + * + * @param x The position of the element to swap with the top of the stack. + * + * @return A new stack with the specified elements swapped. + */ public TaintAbstractDomain swapX(int x) { if (hasBottomUntil(x + 1)) return bottom(); @@ -618,6 +637,15 @@ public TaintAbstractDomain swapX(int x) { return copy; } + /** + * Duplicates the x-th element from the top of the stack and returns the + * modified stack. + * + * @param x The position of the element to duplicate from the top of the + * stack. + * + * @return A new stack with the specified element duplicated at the top. + */ public TaintAbstractDomain dupX(int x) { if (hasBottomUntil(x)) return bottom(); @@ -698,6 +726,12 @@ public TaintAbstractDomain popScope(ScopeToken token) throws SemanticException { return this; } + /** + * Computes the greatest lower bound (GLB) between this abstract domain and another. + * + * @param other the other domain + * @return a new domain representing the greatest lower bound of the two domains + */ @Override public TaintAbstractDomain glbAux(TaintAbstractDomain other) throws SemanticException { TaintElement[] result = new TaintElement[STACK_LIMIT]; @@ -707,6 +741,12 @@ public TaintAbstractDomain glbAux(TaintAbstractDomain other) throws SemanticExce return mk(result, this.memory.glb(other.memory)); } + /** + * Computes the least upper bound (LUB) between this abstract domain and another. + * + * @param other the other domain + * @return a new domain representing the least upper bound of the two domains + */ @Override public TaintAbstractDomain lubAux(TaintAbstractDomain other) throws SemanticException { TaintElement[] result = new TaintElement[STACK_LIMIT]; @@ -716,6 +756,13 @@ public TaintAbstractDomain lubAux(TaintAbstractDomain other) throws SemanticExce return mk(result, this.memory.lub(other.memory)); } + /** + * Get a specific element of the stack. + * + * @param index the index of the element + * + * @return the StackElement at the given index, or BOTTOM if out of bounds + */ public TaintElement get(int index) { if (index < 0 || index >= STACK_LIMIT) return TaintElement.BOTTOM; @@ -733,8 +780,13 @@ public boolean lessOrEqualAux(TaintAbstractDomain other) throws SemanticExceptio /** * Pushes the specified element onto the stack. + *

+ * This method inserts the given {@link TaintElement} at the tail of the + * circular array, effectively updating the top of the stack. The head of + * the stack is also updated to maintain the circular nature of the + * structure. * - * @param target the element to be pushed onto the stack. + * @param target the element to be pushed onto the stack */ public void push(TaintElement target) { circularArray[tail] = target; @@ -744,8 +796,14 @@ public void push(TaintElement target) { /** * Pops the element from the stack. + *

+ * This method removes and returns the topmost element of the stack. After + * popping, the stack structure is adjusted by shifting the head, and the + * previous bottommost element is updated based on the next element. If the + * next element is {@link TaintElement#TOP}, the bottom is set to TOP, + * otherwise, it is set to {@link TaintElement#BOTTOM}. * - * @return the element at the top of the stack. + * @return the element at the top of the stack before popping */ public TaintElement pop() { @@ -785,10 +843,9 @@ public boolean hasBottomUntil(int x) { return false; } - @Override public TaintAbstractDomain clone() { - TaintElement[] newArray = Arrays.copyOf(circularArray, STACK_LIMIT); + TaintElement[] newArray = circularArray.clone(); TaintAbstractDomain copy = mk(newArray, memory); copy.head = this.head; copy.tail = this.tail; @@ -818,6 +875,11 @@ public int hashCode() { return Objects.hash(circularArray, memory); } + /** + * Yields the second element of this abstract stack. + * + * @return the second element of this abstract stack + */ public TaintElement getSecondElement() { if (isBottom()) return TaintElement.BOTTOM; @@ -826,6 +888,11 @@ public TaintElement getSecondElement() { return circularArray[(tail - 2 + STACK_LIMIT) % STACK_LIMIT]; } + /** + * Yields the first element of this abstract stack. + * + * @return the first element of this abstract stack + */ public TaintElement getFirstElement() { if (isBottom()) return TaintElement.BOTTOM; @@ -834,6 +901,16 @@ public TaintElement getFirstElement() { return circularArray[(tail - 1 + STACK_LIMIT) % STACK_LIMIT]; } + /** + * Performs {@code pos} consecutive {@code pop()} operations on the stack. + * + * @param pos the number of elements to pop from the stack + */ + public void popX(int pos) { + for (int i = 0; i < pos; i++) + pop(); + } + /** * Yields the set of opcodes that push taint elements. * @@ -852,7 +929,7 @@ public TaintElement getFirstElement() { * Utility for creating a concrete instance of {@link TaintAbstractDomain} * given the stack and the memory. * - * @param array the stack // TODO: CHECK + * @param array the stack * @param memory the memory * * @return a new concrete instance of {@link TaintAbstractDomain} From 383d13b6914ca679d50f85043b9ec478de731657 Mon Sep 17 00:00:00 2001 From: Shivam Kumar Date: Thu, 20 Mar 2025 16:13:07 +0100 Subject: [PATCH 11/14] Apply spotless --- .../java/it/unipr/analysis/AbstractStack.java | 36 +++++++------ .../analysis/taint/TaintAbstractDomain.java | 52 +++++++++++-------- .../TimestampDependencyAbstractDomain.java | 7 +-- .../taint/TxOriginAbstractDomain.java | 6 +-- 4 files changed, 52 insertions(+), 49 deletions(-) diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java index 057b921f1..5b30b0261 100644 --- a/src/main/java/it/unipr/analysis/AbstractStack.java +++ b/src/main/java/it/unipr/analysis/AbstractStack.java @@ -1,8 +1,5 @@ package it.unipr.analysis; -import java.util.Arrays; -import java.util.function.Predicate; - import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.ScopeToken; @@ -15,6 +12,8 @@ import it.unive.lisa.symbolic.value.ValueExpression; import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; +import java.util.Arrays; +import java.util.function.Predicate; public class AbstractStack implements ValueDomain, BaseLattice { @@ -38,20 +37,23 @@ public class AbstractStack implements ValueDomain, BaseLattice - * This pointer indicates the position in the array that corresponds to the bottom of the stack. - * Tracks the index of the oldest element in the circular array. - */ - private int head; - - /** - * The index representing the next insertion point in the circular array. - *

- * This pointer is used to identify the top of the stack, where the next element will be pushed. - */ - private int tail; + /** + * The index representing the beginning of the logical stack in the circular + * array. + *

+ * This pointer indicates the position in the array that corresponds to the + * bottom of the stack. Tracks the index of the oldest element in the + * circular array. + */ + private int head; + + /** + * The index representing the next insertion point in the circular array. + *

+ * This pointer is used to identify the top of the stack, where the next + * element will be pushed. + */ + private int tail; /** * Helper method to create and fill an array with a specific element. diff --git a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java index 03e85488b..12cb354f6 100644 --- a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java @@ -1,12 +1,5 @@ package it.unipr.analysis.taint; -import java.util.Arrays; -import java.util.Objects; -import java.util.Set; -import java.util.function.Predicate; - -import it.unipr.analysis.AbstractStack; -import it.unipr.analysis.StackElement; import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.ScopeToken; @@ -23,9 +16,13 @@ import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator; import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; +import java.util.Arrays; +import java.util.Objects; +import java.util.Set; +import java.util.function.Predicate; public abstract class TaintAbstractDomain -implements ValueDomain, BaseLattice { + implements ValueDomain, BaseLattice { /** * The stack limit. @@ -38,17 +35,20 @@ public abstract class TaintAbstractDomain private final TaintElement[] circularArray; /** - * The index representing the beginning of the logical stack in the circular array. + * The index representing the beginning of the logical stack in the circular + * array. *

- * This pointer indicates the position in the array that corresponds to the bottom of the stack. - * Tracks the index of the oldest element in the circular array. + * This pointer indicates the position in the array that corresponds to the + * bottom of the stack. Tracks the index of the oldest element in the + * circular array. */ private int head; /** * The index representing the next insertion point in the circular array. *

- * This pointer is used to identify the top of the stack, where the next element will be pushed. + * This pointer is used to identify the top of the stack, where the next + * element will be pushed. */ private int tail; @@ -58,7 +58,8 @@ public abstract class TaintAbstractDomain private final TaintElement memory; /** - * Builds a taint abstract stack starting from a given stack and a memory element. + * Builds a taint abstract stack starting from a given stack and a memory + * element. * * @param circularArray the stack of values * @param memory the memory element @@ -205,7 +206,8 @@ else if (memory.isClean()) TaintElement value = resultStack.pop(); if (value.isTaint()) - return mk(resultStack.circularArray, TaintElement.TAINT); // TODO: CHECK + return mk(resultStack.circularArray, TaintElement.TAINT); // TODO: + // CHECK else if (value.isClean()) return resultStack; } @@ -483,7 +485,7 @@ else if (value.isClean()) resultStack.push(TaintElement.TAINT); else resultStack - .push(TaintElement.semantics(gas, to, value, inOffset, inLength, outOffset, outLength)); + .push(TaintElement.semantics(gas, to, value, inOffset, inLength, outOffset, outLength)); return resultStack; } case "ReturnOperator": { // RETURN @@ -610,7 +612,8 @@ private TaintAbstractDomain swapXoperator(int x, TaintAbstractDomain stack) { /** * Checks whether the stack is empty. * - * @return {@code true} if the first element is bottom, {@code false} otherwise. + * @return {@code true} if the first element is bottom, {@code false} + * otherwise. */ public boolean isEmpty() { return getFirstElement().isBottom(); @@ -727,10 +730,13 @@ public TaintAbstractDomain popScope(ScopeToken token) throws SemanticException { } /** - * Computes the greatest lower bound (GLB) between this abstract domain and another. + * Computes the greatest lower bound (GLB) between this abstract domain and + * another. * * @param other the other domain - * @return a new domain representing the greatest lower bound of the two domains + * + * @return a new domain representing the greatest lower bound of the two + * domains */ @Override public TaintAbstractDomain glbAux(TaintAbstractDomain other) throws SemanticException { @@ -742,10 +748,13 @@ public TaintAbstractDomain glbAux(TaintAbstractDomain other) throws SemanticExce } /** - * Computes the least upper bound (LUB) between this abstract domain and another. + * Computes the least upper bound (LUB) between this abstract domain and + * another. * * @param other the other domain - * @return a new domain representing the least upper bound of the two domains + * + * @return a new domain representing the least upper bound of the two + * domains */ @Override public TaintAbstractDomain lubAux(TaintAbstractDomain other) throws SemanticException { @@ -869,7 +878,6 @@ public boolean equals(Object obj) { return Arrays.equals(this.circularArray, other.circularArray); } - @Override public int hashCode() { return Objects.hash(circularArray, memory); @@ -929,7 +937,7 @@ public void popX(int pos) { * Utility for creating a concrete instance of {@link TaintAbstractDomain} * given the stack and the memory. * - * @param array the stack + * @param array the stack * @param memory the memory * * @return a new concrete instance of {@link TaintAbstractDomain} diff --git a/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java index 9623098ef..3af779d58 100644 --- a/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java @@ -1,20 +1,17 @@ package it.unipr.analysis.taint; -import it.unipr.analysis.StackElement; import it.unipr.analysis.operator.BalanceOperator; import it.unipr.analysis.operator.BlockhashOperator; import it.unipr.analysis.operator.DifficultyOperator; import it.unipr.analysis.operator.TimestampOperator; import it.unive.lisa.symbolic.value.Operator; - import java.util.*; public class TimestampDependencyAbstractDomain extends TaintAbstractDomain { private static final TimestampDependencyAbstractDomain TOP = new TimestampDependencyAbstractDomain( createFilledArray(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); - private static final TimestampDependencyAbstractDomain BOTTOM = - new TimestampDependencyAbstractDomain(null, TaintElement.BOTTOM); - + private static final TimestampDependencyAbstractDomain BOTTOM = new TimestampDependencyAbstractDomain(null, + TaintElement.BOTTOM); private static TaintElement[] createFilledArray(int size, TaintElement element) { TaintElement[] array = new TaintElement[size]; diff --git a/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java index f2e3325b2..6cf263c60 100644 --- a/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java @@ -2,7 +2,6 @@ import it.unipr.analysis.operator.OriginOperator; import it.unive.lisa.symbolic.value.Operator; -import java.util.ArrayList; import java.util.Arrays; import java.util.Collections; import java.util.Set; @@ -11,9 +10,7 @@ public class TxOriginAbstractDomain extends TaintAbstractDomain { private static final TxOriginAbstractDomain TOP = new TxOriginAbstractDomain( createFilledArray(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); - private static final TxOriginAbstractDomain BOTTOM = - new TxOriginAbstractDomain(null, TaintElement.BOTTOM); - + private static final TxOriginAbstractDomain BOTTOM = new TxOriginAbstractDomain(null, TaintElement.BOTTOM); private static TaintElement[] createFilledArray(int size, TaintElement element) { TaintElement[] array = new TaintElement[size]; @@ -21,7 +18,6 @@ private static TaintElement[] createFilledArray(int size, TaintElement element) return array; } - /** * Builds an initial symbolic stack. */ From 40a6dd0187aad5671d5a322b74e1108e28f272a8 Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Thu, 20 Mar 2025 17:54:55 +0100 Subject: [PATCH 12/14] Introducing popX in taint abstract domain's small-step semantics --- .../analysis/taint/TaintAbstractDomain.java | 61 ++++++------------- 1 file changed, 20 insertions(+), 41 deletions(-) diff --git a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java index 12cb354f6..e9124a48b 100644 --- a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java @@ -147,9 +147,8 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement opnd1 = resultStack.pop(); - TaintElement opnd2 = resultStack.pop(); - + resultStack.popX(2); + return resultStack; } @@ -216,10 +215,7 @@ else if (value.isClean()) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement destOffset = resultStack.pop(); - TaintElement offset = resultStack.pop(); - TaintElement size = resultStack.pop(); - + resultStack.popX(3); return resultStack; } @@ -282,8 +278,7 @@ else if (value.isClean()) if (hasBottomUntil(2)) return bottom(); TaintAbstractDomain resultStack = clone(); - resultStack.pop(); - resultStack.pop(); + resultStack.popX(2); return resultStack; } @@ -388,8 +383,7 @@ else if (value.isClean()) if (hasBottomUntil(2)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); + resultStack.popX(2); return resultStack; } @@ -397,9 +391,7 @@ else if (value.isClean()) if (hasBottomUntil(3)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); - resultStack.pop(); + resultStack.popX(3); return resultStack; } @@ -407,10 +399,8 @@ else if (value.isClean()) if (hasBottomUntil(4)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); - resultStack.pop(); - resultStack.pop(); + resultStack.popX(4); + return resultStack; } @@ -418,11 +408,8 @@ else if (value.isClean()) if (hasBottomUntil(5)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); - resultStack.pop(); - resultStack.pop(); - resultStack.pop(); + resultStack.popX(5); + return resultStack; } @@ -430,12 +417,8 @@ else if (value.isClean()) if (hasBottomUntil(6)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); - resultStack.pop(); - resultStack.pop(); - resultStack.pop(); - resultStack.pop(); + resultStack.popX(6); + return resultStack; } @@ -519,8 +502,8 @@ else if (value.isClean()) if (hasBottomUntil(2)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); + resultStack.popX(2); + return resultStack; } @@ -539,9 +522,8 @@ else if (value.isClean()) if (hasBottomUntil(3)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement memOffset = resultStack.pop(); - TaintElement dataOffset = resultStack.pop(); - TaintElement length = resultStack.pop(); + resultStack.popX(3); + return resultStack; } @@ -561,10 +543,8 @@ else if (value.isClean()) if (hasBottomUntil(4)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement address = resultStack.pop(); - TaintElement memOffset = resultStack.pop(); - TaintElement dataOffset = resultStack.pop(); - TaintElement length = resultStack.pop(); + resultStack.popX(4); + return resultStack; } @@ -572,9 +552,8 @@ else if (value.isClean()) if (hasBottomUntil(3)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement memOffset = resultStack.pop(); - TaintElement dataOffset = resultStack.pop(); - TaintElement length = resultStack.pop(); + resultStack.popX(3); + return resultStack; } From cb0ba9306ebfa093a7e7ed126ab6e017f1a2d557 Mon Sep 17 00:00:00 2001 From: Shivam Kumar Date: Thu, 20 Mar 2025 21:31:58 +0100 Subject: [PATCH 13/14] Checked last TODO + spotless apply --- .../unipr/analysis/taint/TaintAbstractDomain.java | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java index e9124a48b..93ac7a96f 100644 --- a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java @@ -148,7 +148,7 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra TaintAbstractDomain resultStack = clone(); resultStack.popX(2); - + return resultStack; } @@ -205,8 +205,8 @@ else if (memory.isClean()) TaintElement value = resultStack.pop(); if (value.isTaint()) - return mk(resultStack.circularArray, TaintElement.TAINT); // TODO: - // CHECK + return mk(resultStack.circularArray, TaintElement.TAINT); + else if (value.isClean()) return resultStack; } @@ -401,7 +401,6 @@ else if (value.isClean()) TaintAbstractDomain resultStack = clone(); resultStack.popX(4); - return resultStack; } case "Log3Operator": { // LOG3 @@ -410,7 +409,6 @@ else if (value.isClean()) TaintAbstractDomain resultStack = clone(); resultStack.popX(5); - return resultStack; } case "Log4Operator": { // LOG4 @@ -419,7 +417,6 @@ else if (value.isClean()) TaintAbstractDomain resultStack = clone(); resultStack.popX(6); - return resultStack; } case "CreateOperator": { // CREATE @@ -504,7 +501,6 @@ else if (value.isClean()) TaintAbstractDomain resultStack = clone(); resultStack.popX(2); - return resultStack; } case "InvalidOperator": { // INVALID @@ -524,7 +520,6 @@ else if (value.isClean()) TaintAbstractDomain resultStack = clone(); resultStack.popX(3); - return resultStack; } case "ExtcodesizeOperator": { // EXTCODESIZE @@ -545,7 +540,6 @@ else if (value.isClean()) TaintAbstractDomain resultStack = clone(); resultStack.popX(4); - return resultStack; } case "ReturndatacopyOperator": { // RETURNDATACOPY @@ -554,7 +548,6 @@ else if (value.isClean()) TaintAbstractDomain resultStack = clone(); resultStack.popX(3); - return resultStack; } case "ExtcodehashOperator": { // EXTCODEHASH From f6e9b9d19fcdd1ffcd65ed4b1fc1471989476842 Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Fri, 21 Mar 2025 10:11:30 +0100 Subject: [PATCH 14/14] Minor changes --- src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java index 93ac7a96f..f8b9b144e 100644 --- a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java @@ -786,7 +786,6 @@ public void push(TaintElement target) { * * @return the element at the top of the stack before popping */ - public TaintElement pop() { int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; TaintElement popped = circularArray[topIndex];