Abstract semantics of RETURNDATASIZE

Author: VincenzoArceri

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

@@ -56,6 +56,12 @@ public class AbstractStack implements ValueDomain<AbstractStack>, BaseLattice<Ab
 	 */
 	private int tail;
 
+	/**
+	 * Value of the output size of the last call (CALL, DELEGATECALL, CALLCODE,
+	 * STATICCALL).
+	 */
+	private StackElement outSize;
+
 	/**
 	 * Helper method to create and fill an array with a specific element.
 	 */
@@ -72,17 +78,19 @@ public AbstractStack() {
 		this(createFilledArray(STACK_LIMIT, StackElement.BOTTOM));
 		this.head = 0;
 		this.tail = 0;
+		this.outSize = StackElement.BOTTOM;
 	}
 
 	/**
 	 * Builds a symbolic stack starting from a given stack array.
 	 *
 	 * @param stack the stack of values
 	 */
-	public AbstractStack(StackElement[] stack) {
+	private AbstractStack(StackElement[] stack) {
 		this.circularArray = stack;
 		this.head = 0;
 		this.tail = 0;
+		this.outSize = StackElement.BOTTOM;
 	}
 
 	@Override
@@ -236,6 +244,7 @@ public AbstractStack clone() {
 		AbstractStack clone = new AbstractStack(circularArray.clone());
 		clone.head = this.head;
 		clone.tail = this.tail;
+		clone.outSize = this.outSize;
 		return clone;
 	}
 
@@ -359,7 +368,6 @@ 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++) {
 			int pos = (tail - 1 - i + STACK_LIMIT) % STACK_LIMIT;
@@ -422,4 +430,22 @@ private StackElement[] toLogicalArray() {
 			logical[i] = circularArray[(head + i) % STACK_LIMIT];
 		return logical;
 	}
+
+	/**
+	 * Sets size of output data from the previous call.
+	 * 
+	 * @param outSize the size of output data from the previous call.
+	 */
+	public void setOutSize(StackElement outSize) {
+		this.outSize = outSize;
+	}
+
+	/**
+	 * Gets size of output data from the previous call.
+	 * 
+	 * @return the size of output data from the previous call
+	 */
+	public StackElement getOutSize() {
+		return outSize;
+	}
 }

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

@@ -214,7 +214,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
 				case "GaslimitOperator": // GASLIMIT
 				case "ChainidOperator": // CHAINID
 				case "SelfbalanceOperator": // SELFBALANCE
-				case "ReturndatasizeOperator": // RETURNDATASIZE
 				case "GaspriceOperator": // GASPRICE
 				case "CodesizeOperator": // CODESIZE
 				case "OriginOperator": // ORIGIN
@@ -230,6 +229,23 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
 					return new EVMAbstractState(result, memory, storage);
 				}
 
+				case "ReturndatasizeOperator": { // RETURNDATASIZE
+					for (AbstractStack stack : stacks) {
+						// stack corresponding to the case when
+						// last call failed
+						AbstractStack resultStackFailing = stack.clone();
+						resultStackFailing.push(StackElement.ZERO);
+						result.add(resultStackFailing);
+
+						// stack corresponding to the case when
+						// last call was successful
+						AbstractStack resultStackSuccess = stack.clone();
+						resultStackSuccess.push(stack.getOutSize());
+						result.add(resultStackSuccess);
+					}
+
+					return new EVMAbstractState(result, memory, storage);
+				}
 				case "PcOperator": { // PC
 					for (AbstractStack stack : stacks) {
 						AbstractStack resultStack = stack.clone();
@@ -1755,7 +1771,11 @@ else if (indexOfByte.compareTo(new StackElement(Number.MAX_INT)) < 0) {
 						if (stack.hasBottomUntil(7))
 							continue;
 						AbstractStack resultStack = stack.clone();
-						resultStack.popX(7);
+						resultStack.popX(6);
+
+						// Setting outsize
+						StackElement outSize = resultStack.pop();
+						resultStack.setOutSize(outSize);
 
 						resultStack.push(StackElement.NOT_JUMPDEST_TOP);
 						result.add(resultStack);
@@ -1771,7 +1791,11 @@ else if (indexOfByte.compareTo(new StackElement(Number.MAX_INT)) < 0) {
 						if (stack.hasBottomUntil(7))
 							continue;
 						AbstractStack resultStack = stack.clone();
-						resultStack.popX(7);
+						resultStack.popX(6);
+
+						// Setting outsize
+						StackElement outSize = resultStack.pop();
+						resultStack.setOutSize(outSize);
 
 						resultStack.push(StackElement.NOT_JUMPDEST_TOP);
 						result.add(resultStack);
@@ -1803,7 +1827,11 @@ else if (indexOfByte.compareTo(new StackElement(Number.MAX_INT)) < 0) {
 						if (stack.hasBottomUntil(6))
 							continue;
 						AbstractStack resultStack = stack.clone();
-						resultStack.popX(6);
+						resultStack.popX(5);
+
+						// Setting outsize
+						StackElement outSize = resultStack.pop();
+						resultStack.setOutSize(outSize);
 
 						resultStack.push(StackElement.NOT_JUMPDEST_TOP);
 						result.add(resultStack);
@@ -1819,7 +1847,11 @@ else if (indexOfByte.compareTo(new StackElement(Number.MAX_INT)) < 0) {
 						if (stack.hasBottomUntil(6))
 							continue;
 						AbstractStack resultStack = stack.clone();
-						resultStack.popX(6);
+						resultStack.popX(5);
+
+						// Setting outsize
+						StackElement outSize = resultStack.pop();
+						resultStack.setOutSize(outSize);
 
 						resultStack.push(StackElement.NOT_JUMPDEST_TOP);
 						result.add(resultStack);