Merge pull request #13177 from ethereum/check-overflow-after-mul-operation

Check overflow after multiplication operation.

Author: matheusaaguiar

Changelog.md

@@ -7,6 +7,7 @@ Language Features:
 
 
 Compiler Features:
+ * Code Generator: More efficient overflow checks for multiplication.
 
 
 Bugfixes:

libsolidity/codegen/YulUtilFunctions.cpp

@@ -684,28 +684,46 @@ string YulUtilFunctions::overflowCheckedIntMulFunction(IntegerType const& _type)
 			function <functionName>(x, y) -> product {
 				x := <cleanupFunction>(x)
 				y := <cleanupFunction>(y)
+				let product_raw := mul(x, y)
+				product := <cleanupFunction>(product_raw)
 				<?signed>
-					// overflow, if x > 0, y > 0 and x > (maxValue / y)
-					if and(and(sgt(x, 0), sgt(y, 0)), gt(x, div(<maxValue>, y))) { <panic>() }
-					// underflow, if x > 0, y < 0 and y < (minValue / x)
-					if and(and(sgt(x, 0), slt(y, 0)), slt(y, sdiv(<minValue>, x))) { <panic>() }
-					// underflow, if x < 0, y > 0 and x < (minValue / y)
-					if and(and(slt(x, 0), sgt(y, 0)), slt(x, sdiv(<minValue>, y))) { <panic>() }
-					// overflow, if x < 0, y < 0 and x < (maxValue / y)
-					if and(and(slt(x, 0), slt(y, 0)), slt(x, sdiv(<maxValue>, y))) { <panic>() }
+					<?gt128bit>
+						<?256bit>
+							// special case
+							if and(slt(x, 0), eq(y, <minValue>)) { <panic>() }
+						</256bit>
+						// overflow, if x != 0 and y != product/x
+						if iszero(
+							or(
+								iszero(x),
+								eq(y, sdiv(product, x))
+							)
+						) { <panic>() }
+					<!gt128bit>
+						if iszero(eq(product, product_raw)) { <panic>() }
+					</gt128bit>
 				<!signed>
-					// overflow, if x != 0 and y > (maxValue / x)
-					if and(iszero(iszero(x)), gt(y, div(<maxValue>, x))) { <panic>() }
+					<?gt128bit>
+						// overflow, if x != 0 and y != product/x
+						if iszero(
+							or(
+								iszero(x),
+								eq(y, div(product, x))
+							)
+						) { <panic>() }
+					<!gt128bit>
+						if iszero(eq(product, product_raw)) { <panic>() }
+					</gt128bit>
 				</signed>
-				product := mul(x, y)
 			}
 			)")
 			("functionName", functionName)
 			("signed", _type.isSigned())
-			("maxValue", toCompactHexWithPrefix(u256(_type.maxValue())))
-			("minValue", toCompactHexWithPrefix(u256(_type.minValue())))
 			("cleanupFunction", cleanupFunction(_type))
 			("panic", panicFunction(PanicCode::UnderOverflow))
+			("minValue", toCompactHexWithPrefix(u256(_type.minValue())))
+			("256bit", _type.numBits() == 256)
+			("gt128bit", _type.numBits() > 128)
 			.render();
 	});
 }

test/formal/checked_int_mul_12.py

@@ -0,0 +1,46 @@
+from opcodes import AND, SDIV, MUL, EQ, ISZERO, OR, SLT
+from rule import Rule
+from util import BVSignedUpCast, BVSignedMin, BVSignedCleanupFunction
+from z3 import BVMulNoOverflow, BVMulNoUnderflow, BitVec, Not, Or
+
+"""
+Overflow checked signed integer multiplication.
+"""
+
+# Approximation with 16-bit base types.
+n_bits = 12
+
+for type_bits in [4, 6, 8, 12]:
+
+	rule = Rule()
+
+	# Input vars
+	X_short = BitVec('X', type_bits)
+	Y_short = BitVec('Y', type_bits)
+
+	# Z3's overflow and underflow conditions
+	actual_overflow = Not(BVMulNoOverflow(X_short, Y_short, True))
+	actual_underflow = Not(BVMulNoUnderflow(X_short, Y_short))
+
+	# cast to full n_bits values
+	X = BVSignedUpCast(X_short, n_bits)
+	Y = BVSignedUpCast(Y_short, n_bits)
+	product_raw = MUL(X, Y)
+	#remove any overflown bits
+	product = BVSignedCleanupFunction(product_raw, type_bits)
+
+	# Constants
+	min_value = BVSignedMin(type_bits, n_bits)
+
+	# Overflow and underflow checks in YulUtilFunction::overflowCheckedIntMulFunction
+	if type_bits > n_bits / 2:
+		sol_overflow_check_1 = ISZERO(OR(ISZERO(X), EQ(Y, SDIV(product, X))))
+		if type_bits == n_bits:
+			sol_overflow_check_2 = AND(SLT(X, 0), EQ(Y, min_value))
+			sol_overflow_check = Or(sol_overflow_check_1 != 0, sol_overflow_check_2 != 0)
+		else:
+			sol_overflow_check = (sol_overflow_check_1 != 0)
+	else:
+		sol_overflow_check = (ISZERO(EQ(product, product_raw)) != 0)
+
+	rule.check(Or(actual_overflow, actual_underflow), sol_overflow_check)

test/formal/checked_int_mul_16.py

@@ -1,17 +1,16 @@
-from opcodes import AND, ISZERO, GT, DIV
+from opcodes import ISZERO, DIV, MUL, EQ, OR
 from rule import Rule
-from util import BVUnsignedUpCast, BVUnsignedMax
+from util import BVUnsignedUpCast, BVUnsignedCleanupFunction
 from z3 import BitVec, Not, BVMulNoOverflow
 
 """
 Overflow checked unsigned integer multiplication.
 """
 
 # Approximation with 16-bit base types.
-n_bits = 16
-type_bits = 8
+n_bits = 12
 
-while type_bits <= n_bits:
+for type_bits in [4, 6, 8, 12]:
 
 	rule = Rule()
 
@@ -25,13 +24,14 @@
 	# cast to full n_bits values
 	X = BVUnsignedUpCast(X_short, n_bits)
 	Y = BVUnsignedUpCast(Y_short, n_bits)
+	product_raw = MUL(X, Y)
+	#remove any overflown bits
+	product = BVUnsignedCleanupFunction(product_raw, type_bits)
 
-	# Constants
-	maxValue = BVUnsignedMax(type_bits, n_bits)
-
-	# Overflow check in YulUtilFunction::overflowCheckedIntMulFunction
-	overflow_check = AND(ISZERO(ISZERO(X)), GT(Y, DIV(maxValue, X)))
+	# Overflow check in YulUtilFunction::overflowCheckedIntMulFunctions
+	if type_bits > n_bits / 2:
+		overflow_check = ISZERO(OR(ISZERO(X), EQ(Y, DIV(product, X))))
+	else:
+		overflow_check = ISZERO(EQ(product, product_raw))
 
 	rule.check(overflow_check != 0, actual_overflow)
-
-	type_bits *= 2

test/formal/checked_uint_mul_16.py renamed to test/formal/checked_uint_mul_12.py

@@ -0,0 +1,41 @@
+from opcodes import SIGNEXTEND
+from rule import Rule
+from util import BVSignedCleanupFunction, BVSignedUpCast
+from z3 import BitVec, BitVecVal, Concat
+
+"""
+Overflow checked signed integer multiplication.
+"""
+
+n_bits = 256
+
+# Check that YulUtilFunction::cleanupFunction cleanup matches BVSignedCleanupFunction
+for type_bits in range(8,256,8):
+
+	rule = Rule()
+
+	# Input vars
+	X = BitVec('X', n_bits)
+	arg = BitVecVal(type_bits / 8 - 1, n_bits)
+
+	cleaned_reference = BVSignedCleanupFunction(X, type_bits)
+	cleaned = SIGNEXTEND(arg, X)
+
+	rule.check(cleaned, cleaned_reference)
+
+
+# Check that BVSignedCleanupFunction properly cleans up values.
+for type_bits in range(8,256,8):
+
+	rule = Rule()
+
+	# Input vars
+	X_short = BitVec('X', type_bits)
+	dirt = BitVec('dirt', n_bits - type_bits)
+
+	X = BVSignedUpCast(X_short, n_bits)
+	X_dirty = Concat(dirt, X_short)
+	X_cleaned = BVSignedCleanupFunction(X_dirty, type_bits)
+
+
+	rule.check(X, X_cleaned)

test/formal/signed_integer_cleanup_function.py

@@ -0,0 +1,40 @@
+from opcodes import AND
+from rule import Rule
+from util import BVUnsignedCleanupFunction, BVUnsignedUpCast
+from z3 import BitVec, BitVecVal, Concat
+
+"""
+Overflow checked unsigned integer multiplication.
+"""
+
+n_bits = 256
+
+# Check that YulUtilFunction::cleanupFunction cleanup matches BVUnsignedCleanupFunction
+for type_bits in range(8,256,8):
+
+	rule = Rule()
+
+	# Input vars
+	X = BitVec('X', n_bits)
+	mask = BitVecVal((1 << type_bits) - 1, n_bits)
+
+	cleaned_reference = BVUnsignedCleanupFunction(X, type_bits)
+	cleaned = AND(X, mask)
+
+	rule.check(cleaned, cleaned_reference)
+
+# Check that BVUnsignedCleanupFunction properly cleans up values.
+for type_bits in range(8,256,8):
+
+	rule = Rule()
+
+	# Input vars
+	X_short = BitVec('X', type_bits)
+	dirt = BitVec('dirt', n_bits - type_bits)
+
+	X = BVUnsignedUpCast(X_short, n_bits)
+	X_dirty = Concat(dirt, X_short)
+	X_cleaned = BVUnsignedCleanupFunction(X_dirty, type_bits)
+
+
+	rule.check(X, X_cleaned)

test/formal/unsigned_integer_cleanup_function.py

@@ -25,3 +25,18 @@ def BVSignedMax(type_bits, n_bits):
 def BVSignedMin(type_bits, n_bits):
 	assert type_bits <= n_bits
 	return BitVecVal(-(1 << (type_bits - 1)), n_bits)
+
+def BVSignedCleanupFunction(x, type_bits):
+	assert x.size() >= type_bits
+	sign_mask = BitVecVal(1, x.size()) << (type_bits - 1)
+	bit_mask = (BitVecVal(1, x.size()) << type_bits) - 1
+	return If(
+		x & sign_mask == 0,
+		x & bit_mask,
+		x | ~bit_mask
+	)
+
+def BVUnsignedCleanupFunction(x, type_bits):
+	assert x.size() >= type_bits
+	bit_mask = (BitVecVal(1, x.size()) << type_bits) - 1
+	return x & bit_mask

test/formal/util.py

@@ -18,10 +18,10 @@ contract C {
 // EVMVersion: >homestead
 // ----
 // h(uint256[2][]): 0x20, 3, 123, 124, 223, 224, 323, 324 -> 32, 256, 0x20, 3, 123, 124, 223, 224, 323, 324
-// gas irOptimized: 180726
+// gas irOptimized: 180829
 // gas legacy: 184921
 // gas legacyOptimized: 181506
 // i(uint256[2][2]): 123, 124, 223, 224 -> 32, 128, 123, 124, 223, 224
-// gas irOptimized: 112453
+// gas irOptimized: 112464
 // gas legacy: 115460
 // gas legacyOptimized: 112990

test/libsolidity/semanticTests/abiEncoderV2/storage_array_encoding.sol

@@ -35,12 +35,12 @@ contract c {
 }
 // ----
 // test() -> 0x02000202
-// gas irOptimized: 4649903
-// gas legacy: 4578320
-// gas legacyOptimized: 4548312
+// gas irOptimized: 4649835
+// gas legacy: 4578446
+// gas legacyOptimized: 4548309
 // storageEmpty -> 1
 // clear() -> 0, 0
-// gas irOptimized: 4477229
+// gas irOptimized: 4477223
 // gas legacy: 4410748
 // gas legacyOptimized: 4382489
 // storageEmpty -> 1