Merge pull request #11748 from ethereum/optimize_signextend

Optimizer rules for signextend.

libevmasm/RuleList.h

@@ -248,8 +248,8 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart4(
 
 template <class Pattern>
 std::vector<SimplificationRule<Pattern>> simplificationRuleListPart4_5(
-	Pattern,
-	Pattern,
+	Pattern A,
+	Pattern B,
 	Pattern,
 	Pattern X,
 	Pattern Y
@@ -266,13 +266,17 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart4_5(
 		{Builtins::OR(Y, Builtins::OR(X, Y)), [=]{ return Builtins::OR(X, Y); }},
 		{Builtins::OR(Builtins::OR(Y, X), Y), [=]{ return Builtins::OR(Y, X); }},
 		{Builtins::OR(Y, Builtins::OR(Y, X)), [=]{ return Builtins::OR(Y, X); }},
+		{Builtins::SIGNEXTEND(X, Builtins::SIGNEXTEND(X, Y)), [=]() { return Builtins::SIGNEXTEND(X, Y); }},
+		{Builtins::SIGNEXTEND(A, Builtins::SIGNEXTEND(B, X)), [=]() {
+			return Builtins::SIGNEXTEND(A.d() < B.d() ? A.d() : B.d(), X);
+		}},
 	};
 }
 
 template <class Pattern>
 std::vector<SimplificationRule<Pattern>> simplificationRuleListPart5(
 	Pattern A,
-	Pattern,
+	Pattern B,
 	Pattern,
 	Pattern X,
 	Pattern
@@ -314,6 +318,31 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart5(
 		[=]() { return A.d() >= Pattern::WordSize / 8; }
 	});
 
+	// Replace SIGNEXTEND(A, X), A >= 31 with ID
+	rules.push_back({
+		Builtins::SIGNEXTEND(A, X),
+		[=]() -> Pattern { return X; },
+		[=]() { return A.d() >= Pattern::WordSize / 8 - 1; }
+	});
+	rules.push_back({
+		Builtins::AND(A, Builtins::SIGNEXTEND(B, X)),
+		[=]() -> Pattern { return Builtins::AND(A, X); },
+		[=]() {
+			return
+				B.d() < Pattern::WordSize / 8 - 1 &&
+				(A.d() & ((u256(1) << static_cast<size_t>((B.d() + 1) * 8)) - 1)) == A.d();
+		}
+	});
+	rules.push_back({
+		Builtins::AND(Builtins::SIGNEXTEND(B, X), A),
+		[=]() -> Pattern { return Builtins::AND(A, X); },
+		[=]() {
+			return
+				B.d() < Pattern::WordSize / 8 - 1 &&
+				(A.d() & ((u256(1) << static_cast<size_t>((B.d() + 1) * 8)) - 1)) == A.d();
+		}
+	});
+
 	for (auto instr: {
 		Instruction::ADDRESS,
 		Instruction::CALLER,
@@ -597,6 +626,24 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart7(
 		}
 	});
 
+	rules.push_back({
+		Builtins::SHL(A, Builtins::SIGNEXTEND(B, X)),
+		[=]() -> Pattern { return Builtins::SIGNEXTEND((A.d() >> 3) + B.d(), Builtins::SHL(A, X)); },
+		[=] { return (A.d() & 7) == 0 && A.d() <= Pattern::WordSize && B.d() <= Pattern::WordSize / 8; }
+	});
+
+	rules.push_back({
+		Builtins::SIGNEXTEND(A, Builtins::SHR(B, X)),
+		[=]() -> Pattern { return Builtins::SAR(B, X); },
+		[=] {
+			return
+				B.d() % 8 == 0 &&
+				B.d() <= Pattern::WordSize &&
+				A.d() <= Pattern::WordSize &&
+				(Pattern::WordSize - B.d()) / 8 == A.d() + 1;
+		}
+	});
+
 	return rules;
 }
 

test/formal/opcodes.py

@@ -64,3 +64,18 @@ def BYTE(i, x):
 		BitVecVal(0, x.size()),
 		(LShR(x, (x.size() - bit))) & 0xff
 	)
+
+def SIGNEXTEND(i, x):
+	bitBV = i * 8 + 7
+	bitInt = BV2Int(i) * 8 + 7
+	test = BitVecVal(1, x.size()) << bitBV
+	mask = test - 1
+	return If(
+		bitInt >= x.size(),
+		x,
+		If(
+			(x & test) == 0,
+			x & mask,
+			x | ~mask
+		)
+	)

test/formal/signextend.py

@@ -0,0 +1,37 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+1) SIGNEXTEND(A, X) -> X if A >= Pattern::WordSize / 8 - 1;
+
+2) SIGNEXTEND(X, SIGNEXTEND(X, Y)) -> SIGNEXTEND(X, Y)
+
+3) SIGNEXTEND(A, SIGNEXTEND(B, X)) -> SIGNEXTEND(min(A, B), X)
+"""
+
+n_bits = 128
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule1 = Rule()
+# Requirements
+rule1.require(UGE(A, BitVecVal(n_bits // 8 - 1, n_bits)))
+rule1.check(SIGNEXTEND(A, X), X)
+
+rule2 = Rule()
+rule2.check(
+    SIGNEXTEND(X, SIGNEXTEND(X, Y)),
+    SIGNEXTEND(X, Y)
+)
+
+rule3 = Rule()
+rule3.check(
+    SIGNEXTEND(A, SIGNEXTEND(B, X)),
+    SIGNEXTEND(If(ULT(A, B), A, B), X)
+)
+

test/formal/signextend_and.py

@@ -0,0 +1,26 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+AND(A, SIGNEXTEND(B, X)) -> AND(A, X)
+given
+    B < WordSize / 8 - 1 AND
+    A & (1 << ((B + 1) * 8) - 1) == A
+"""
+
+n_bits = 128
+
+# Input vars
+X = BitVec('X', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule = Rule()
+# Requirements
+rule.require(ULT(B, BitVecVal(n_bits // 8 - 1, n_bits)))
+rule.require((A & ((BitVecVal(1, n_bits) << ((B + 1) * 8)) - 1)) == A)
+rule.check(
+    AND(A, SIGNEXTEND(B, X)),
+    AND(A, X)
+)

test/formal/signextend_equivalence.py

@@ -0,0 +1,24 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Checking the implementation of SIGNEXTEND using Z3's native SignExt and Extract
+"""
+
+rule = Rule()
+n_bits = 256
+
+x = BitVec('X', n_bits)
+
+def SIGNEXTEND_native(i, x):
+    return SignExt(256 - 8 * i - 8, Extract(8 * i + 7, 0, x))
+
+for i in range(0, 32):
+    rule.check(
+        SIGNEXTEND(BitVecVal(i, n_bits), x),
+        SIGNEXTEND_native(i, x)
+    )
+
+i = BitVec('I', n_bits)
+rule.require(UGT(i, BitVecVal(31, n_bits)))
+rule.check(SIGNEXTEND(i, x), x)

test/formal/signextend_shl.py

@@ -0,0 +1,25 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+SHL(A, SIGNEXTEND(B, X)) -> SIGNEXTEND((A >> 3) + B, SHL(A, X))
+given return A & 7 == 0  AND  A <= WordSize  AND  B <= WordSize / 8
+"""
+
+n_bits = 256
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule = Rule()
+rule.require(A & 7 == 0)
+rule.require(ULE(A, n_bits))
+rule.require(ULE(B, n_bits / 8))
+rule.check(
+    SHL(A, SIGNEXTEND(B, X)),
+    SIGNEXTEND(LShR(A, 3) + B, SHL(A, X))
+)

test/formal/signextend_shr.py

@@ -0,0 +1,31 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+SIGNEXTEND(A, SHR(B, X)) -> SAR(B, X)
+given
+    B % 8 == 0 AND
+    A <= WordSize AND
+    B <= wordSize AND
+    (WordSize - B) / 8 == A + 1
+"""
+
+n_bits = 256
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule = Rule()
+rule.require(B % 8 == 0)
+rule.require(ULE(A, n_bits))
+rule.require(ULE(B, n_bits))
+rule.require((BitVecVal(n_bits, n_bits) - B) / 8 == A + 1)
+rule.check(
+    SIGNEXTEND(A, SHR(B, X)),
+    SAR(B, X)
+)
+

test/libyul/yulOptimizerTests/fullSuite/shift_signextend.yul

@@ -0,0 +1,15 @@
+{
+    let x := calldataload(0)
+    let a := shl(sub(256, 8), signextend(0, x))
+    sstore(0, a)
+}
+// ====
+// EVMVersion: >=constantinople
+// ----
+// step: fullSuite
+//
+// {
+//     {
+//         sstore(0, shl(248, calldataload(0)))
+//     }
+// }