Merge branch 'bug-fix-benchmark-script' of https://github.com/lisa-analyzer/evm-lisa into bug-fix-benchmark-script

Author: VincenzoArceri

evm-testcases/cfs/sar/report.json

@@ -3,15 +3,15 @@
   "files" : [ "report.json", "untyped_program.evm-testcases_cfs_sar_sar_eth.sol().json" ],
   "info" : {
     "cfgs" : "1",
-    "duration" : "11ms",
-    "end" : "2025-02-26T11:44:05.873+01:00",
-    "expressions" : "6",
+    "duration" : "118ms",
+    "end" : "2025-05-12T21:39:27.481+02:00",
+    "expressions" : "48",
     "files" : "1",
     "globals" : "0",
     "members" : "1",
     "programs" : "1",
-    "start" : "2025-02-26T11:44:05.862+01:00",
-    "statements" : "10",
+    "start" : "2025-05-12T21:39:27.363+02:00",
+    "statements" : "80",
     "units" : "0",
     "version" : "0.1",
     "warnings" : "0"

evm-testcases/cfs/sar/sar_eth.sol

@@ -7,4 +7,74 @@ PUSH32 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0
 PUSH1 0x04
 SAR
 PUSH32 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
+EQ
+PUSH32 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+PUSH2 0x0100
+SAR
+PUSH1 0x00
+EQ
+PUSH32 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+PUSH1 0xff
+SAR
+PUSH1 0x00
+EQ
+PUSH32 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+PUSH1 0xfe
+SAR
+PUSH1 0x01
+EQ
+PUSH32 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+PUSH1 0xf8
+SAR
+PUSH32 0x000000000000000000000000000000000000000000000000000000000000007f
+EQ
+PUSH32 0x4000000000000000000000000000000000000000000000000000000000000000
+PUSH1 0xfe
+SAR
+PUSH32 0x0000000000000000000000000000000000000000000000000000000000000001
+EQ
+PUSH32 0x0000000000000000000000000000000000000000000000000000000000000000
+PUSH1 0x01
+SAR
+PUSH32 0x0000000000000000000000000000000000000000000000000000000000000000
+EQ
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+PUSH1 0x0100
+SAR
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+EQ
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+PUSH1 0xff
+SAR
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+EQ
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+PUSH1 0x01
+SAR
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+EQ
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+PUSH1 0x00
+SAR
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+EQ
+PUSH32 0x8000000000000000000000000000000000000000000000000000000000000000
+PUSH2 0x0101
+SAR
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+EQ
+PUSH32 0x8000000000000000000000000000000000000000000000000000000000000000
+PUSH2 0x0100
+SAR
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+EQ
+PUSH32 0x8000000000000000000000000000000000000000000000000000000000000000
+PUSH1 0xff
+SAR
+PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+EQ
+PUSH32 0x8000000000000000000000000000000000000000000000000000000000000000
+PUSH1 0x01
+SAR
+PUSH32 0xc000000000000000000000000000000000000000000000000000000000000000
 EQ

evm-testcases/cfs/sar/untyped_program.evm-testcases_cfs_sar_sar_eth.sol().json

@@ -1,5 +1,6 @@
 package it.unipr.analysis;
 
+import it.unipr.utils.BitManager;
 import it.unive.lisa.analysis.BaseLattice;
 import it.unive.lisa.analysis.Lattice;
 import it.unive.lisa.analysis.SemanticException;
@@ -451,11 +452,14 @@ else if (isTop() || other.isTop())
 			return top();
 		else if (isTopNotJumpdest() || other.isTopNotJumpdest())
 			return NOT_JUMPDEST_TOP;
-		else if (n.compareTo(new Number(256)) >= 0)
-			return ZERO;
+		else if (n.compareTo(new Number(Number.MAX_INT)) > 0)
+			return bottom(); // fake path
 
-		return new StackElement(other.n.shiftLeft(this.n.getInt()));
+		int[] bits = BitManager.toBitArray(Number.toBigInteger(other.n));
+		int[] shiftedBits = BitManager.shiftLeft(bits, n.getInt());
+		BigInteger result = BitManager.fromBitArray(shiftedBits);
 
+		return new StackElement(new Number(result));
 	}
 
 	public StackElement shr(StackElement other) {
@@ -465,10 +469,14 @@ else if (isTop() || other.isTop())
 			return top();
 		else if (isTopNotJumpdest() || other.isTopNotJumpdest())
 			return NOT_JUMPDEST_TOP;
-		else if (n.compareTo(new Number(256)) >= 0)
-			return ZERO;
+		else if (n.compareTo(new Number(Number.MAX_INT)) > 0)
+			return bottom(); // fake path
+
+		int[] bits = BitManager.toBitArray(Number.toBigInteger(other.n));
+		int[] shiftedBits = BitManager.shiftRight(bits, n.getInt());
+		BigInteger result = BitManager.fromBitArray(shiftedBits);
 
-		return new StackElement(other.n.shiftRight(this.n.getInt()));
+		return new StackElement(new Number(result));
 	}
 
 	public StackElement sar(StackElement other) {
@@ -478,126 +486,14 @@ else if (isTop() || other.isTop())
 			return top();
 		else if (isTopNotJumpdest() || other.isTopNotJumpdest())
 			return NOT_JUMPDEST_TOP;
-		else if (n.compareTo(new Number(256)) > 0)
-			return ZERO;
-
-		return new StackElement(
-				new Number(
-						new BigInteger(
-								StackElement.shiftArithmeticRight(
-										other.n.toByteArray(),
-										this.n.getInt()))));
-	}
-
-	/**
-	 * Shifts the given byte array to the left by the specified number of bits.
-	 *
-	 * @param byteArray     The byte array to be left-shifted.
-	 * @param shiftBitCount The number of bits by which to shift the byte array
-	 *                          to the left.
-	 * 
-	 * @return The resulting byte array after left-shifting by the specified bit
-	 *             count.
-	 *             <p>
-	 *             This method performs a left shift on the provided byte array,
-	 *             where each byte is shifted to the left by the given number of
-	 *             bits. The shift operation is performed in a bitwise manner,
-	 *             and the bits shifted beyond the byte boundary are wrapped
-	 *             around to the opposite end. The shift is done in place, and
-	 *             the modified byte array is returned as the result.
-	 *             </p>
-	 *             <p>
-	 *             The {@code shiftBitCount} parameter determines the number of
-	 *             bits to shift.
-	 *             </p>
-	 * 
-	 * @throws IllegalArgumentException If the input {@code byteArray} is
-	 *                                      {@code null}.
-	 */
-	public static byte[] shiftLeft(byte[] byteArray, int shiftBitCount) {
-		final int shiftMod = shiftBitCount % 8;
-		final byte carryMask = (byte) ((1 << shiftMod) - 1);
-		final int offsetBytes = (shiftBitCount / 8);
+		else if (n.compareTo(new Number(Number.MAX_INT)) > 0)
+			return bottom(); // fake path
 
-		int start;
+		int[] bits = BitManager.toBitArray(Number.toBigInteger(other.n));
+		int[] shiftedBits = BitManager.arithmeticShiftRight(bits, n.getInt());
+		BigInteger result = BitManager.fromBitArray(shiftedBits);
 
-		if (byteArray.length > 32)
-			start = 1;
-		else
-			start = 0;
-
-		int sourceIndex;
-		for (int i = start; i < byteArray.length; i++) {
-			sourceIndex = i + offsetBytes;
-			if (sourceIndex >= byteArray.length) {
-				byteArray[i] = 0;
-			} else {
-				byte src = byteArray[sourceIndex];
-				byte dst = (byte) (src << shiftMod);
-				if (sourceIndex + 1 < byteArray.length) {
-					dst |= byteArray[sourceIndex + 1] >>> (8 - shiftMod) & carryMask;
-				}
-				byteArray[i] = dst;
-			}
-		}
-		return byteArray;
-	}
-
-	/**
-	 * Shifts the bits of the given byte array towards the least significant bit
-	 * (SAR - Shift Arithmetic Right). The bits moved before the first one are
-	 * discarded, and the new bits are set to 0 if the previous most significant
-	 * bit was 0; otherwise, the new bits are set to 1.
-	 *
-	 * @param byteArray     The byte array to be right-shifted.
-	 * @param shiftBitCount The number of bits by which to shift the byte array
-	 *                          to the right.
-	 * 
-	 * @return The resulting byte array after right-shifting by the specified
-	 *             bit count.
-	 *             <p>
-	 *             This method performs a right shift on the provided byte array
-	 *             (SAR operation), where each byte is shifted to the right by
-	 *             the given number of bits. The shift operation is performed in
-	 *             a bitwise manner, and the bits shifted beyond the byte
-	 *             boundary are discarded. The new bits introduced during the
-	 *             shift are set based on the value of the previous most
-	 *             significant bit (0 or 1).
-	 *             </p>
-	 *             <p>
-	 *             The {@code shiftBitCount} parameter determines the number of
-	 *             bits to shift.
-	 *             </p>
-	 *
-	 * @throws IllegalArgumentException If the input {@code byteArray} is
-	 *                                      {@code null}.
-	 */
-	public static byte[] shiftArithmeticRight(byte[] byteArray, int shiftBitCount) {
-		final int shiftMod = shiftBitCount % 8;
-		final byte carryMask = (byte) (0xFF << (8 - shiftMod));
-		final int offsetBytes = (shiftBitCount / 8);
-
-		int sourceIndex;
-		int start;
-
-		if (byteArray.length > 32)
-			start = 1;
-		else
-			start = 0;
-		for (int i = start; i < byteArray.length; i++) {
-			sourceIndex = i + offsetBytes;
-			if (sourceIndex >= byteArray.length) {
-				byteArray[i] = (byte) (byteArray[i] < 0 ? 0xFF : 0);
-			} else {
-				byte src = byteArray[sourceIndex];
-				byte dst = (byte) (src >>> shiftMod);
-				if (sourceIndex + 1 < byteArray.length) {
-					dst |= byteArray[sourceIndex + 1] << (8 - shiftMod) & carryMask;
-				}
-				byteArray[i] = dst;
-			}
-		}
-		return byteArray;
+		return new StackElement(new Number(result));
 	}
 
 	/**

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

@@ -0,0 +1,94 @@
+package it.unipr.utils;
+
+import java.math.BigInteger;
+
+public class BitManager {
+	public static final int SIZE = 256;
+
+	/**
+	 * Converts a BigInteger to an array of bits (0s and 1s), MSB first.
+	 */
+	public static int[] toBitArray(BigInteger value) {
+		if (value.signum() < 0) {
+			throw new IllegalArgumentException("Negative numbers not supported.");
+		}
+
+		String binaryString = value.toString(2); // base 2 string
+		int[] bits = new int[SIZE];
+		int padding = SIZE - binaryString.length();
+
+		for (int i = 0; i < binaryString.length(); i++) {
+			bits[padding + i] = (binaryString.charAt(i) == '1') ? 1 : 0;
+		}
+		return bits;
+	}
+
+	/**
+	 * Converts an array of bits (0s and 1s), MSB first, to a BigInteger.
+	 */
+	public static BigInteger fromBitArray(int[] bits) {
+		BigInteger result = BigInteger.ZERO;
+		for (int bit : bits) {
+			result = result.shiftLeft(1).or(BigInteger.valueOf(bit));
+		}
+		return result;
+	}
+
+	/**
+	 * Logical left shift (<<): discards MSBs, fills with 0s at LSBs.
+	 */
+	public static int[] shiftLeft(int[] bits, int n) {
+		if (bits.length != SIZE)
+			throw new IllegalArgumentException("Input must be 256 bits");
+
+		int[] result = new int[SIZE];
+		if (n >= SIZE)
+			return result; // all zeros
+
+		System.arraycopy(bits, n, result, 0, SIZE - n);
+		return result;
+	}
+
+	/**
+	 * Logical right shift (>>>): discards LSBs, fills with 0s at MSBs.
+	 */
+	public static int[] shiftRight(int[] bits, int n) {
+		if (bits.length != SIZE)
+			throw new IllegalArgumentException("Input must be 256 bits");
+
+		int[] result = new int[SIZE];
+		if (n >= SIZE)
+			return result; // all zeros
+
+		System.arraycopy(bits, 0, result, n, SIZE - n);
+		return result;
+	}
+
+	/**
+	 * Arithmetic right shift (>>): discards LSBs, fills with sign bit at MSBs.
+	 */
+	public static int[] arithmeticShiftRight(int[] bits, int n) {
+		if (bits.length != SIZE)
+			throw new IllegalArgumentException("Input must be 256 bits");
+
+		int[] result = new int[SIZE];
+		int sign = bits[0]; // MSB = sign bit
+		if (n >= SIZE) {
+			// All bits set to sign
+			for (int i = 0; i < SIZE; i++)
+				result[i] = sign;
+			return result;
+		}
+		for (int i = 0; i < n; i++)
+			result[i] = sign;
+		System.arraycopy(bits, 0, result, n, SIZE - n);
+		return result;
+	}
+
+	public static void print(String label, int[] bits) {
+		System.out.print(label + ": ");
+		for (int b : bits)
+			System.out.print(b);
+		System.out.println();
+	}
+}

src/main/java/it/unipr/utils/BitManager.java

@@ -181,7 +181,7 @@ public void testShr() throws AnalysisSetupException, IOException {
 		CronConfiguration conf = createConfiguration("cfs", "shr", "shr_eth.sol", false);
 		perform(conf);
 	}
-	
+
 	@Test
 	public void testShr2() throws AnalysisSetupException, IOException {
 		CronConfiguration conf = createConfiguration("cfs", "shr2", "shr_eth.sol", false);
@@ -259,7 +259,7 @@ public void testShl2() throws AnalysisSetupException, IOException {
 		CronConfiguration conf = createConfiguration("cfs", "shl2", "shl.sol", false);
 		perform(conf);
 	}
-	
+
 	/**
 	 * All the items in the final stack must be 1
 	 */