From 16787ecfd6703568db5c0e520d99713449d9cf72 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 5 Aug 2021 11:32:28 +0200 Subject: [PATCH 1/4] Optimizer rules for signextend. --- libevmasm/RuleList.h | 53 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 50 insertions(+), 3 deletions(-) diff --git a/libevmasm/RuleList.h b/libevmasm/RuleList.h index 4674428ba..9f0b07fe1 100644 --- a/libevmasm/RuleList.h +++ b/libevmasm/RuleList.h @@ -248,8 +248,8 @@ std::vector> simplificationRuleListPart4( template std::vector> simplificationRuleListPart4_5( - Pattern, - Pattern, + Pattern A, + Pattern B, Pattern, Pattern X, Pattern Y @@ -266,13 +266,17 @@ std::vector> 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 std::vector> simplificationRuleListPart5( Pattern A, - Pattern, + Pattern B, Pattern, Pattern X, Pattern @@ -314,6 +318,31 @@ std::vector> 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((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((B.d() + 1) * 8)) - 1)) == A.d(); + } + }); + for (auto instr: { Instruction::ADDRESS, Instruction::CALLER, @@ -597,6 +626,24 @@ std::vector> 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; } From 5906d25a397bb704c39fe55a163369e0558dbb15 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 9 Aug 2021 17:36:19 +0200 Subject: [PATCH 2/4] Formalization of SIGNEXTEND and rule proofs --- test/formal/opcodes.py | 15 ++++++++++++++ test/formal/signextend.py | 37 +++++++++++++++++++++++++++++++++++ test/formal/signextend_and.py | 26 ++++++++++++++++++++++++ test/formal/signextend_shl.py | 25 +++++++++++++++++++++++ test/formal/signextend_shr.py | 31 +++++++++++++++++++++++++++++ 5 files changed, 134 insertions(+) create mode 100644 test/formal/signextend.py create mode 100644 test/formal/signextend_and.py create mode 100644 test/formal/signextend_shl.py create mode 100644 test/formal/signextend_shr.py diff --git a/test/formal/opcodes.py b/test/formal/opcodes.py index 64991f73b..6098d01ed 100644 --- a/test/formal/opcodes.py +++ b/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 + ) + ) diff --git a/test/formal/signextend.py b/test/formal/signextend.py new file mode 100644 index 000000000..32d374261 --- /dev/null +++ b/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) +) + diff --git a/test/formal/signextend_and.py b/test/formal/signextend_and.py new file mode 100644 index 000000000..ae2b4bd2c --- /dev/null +++ b/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) +) diff --git a/test/formal/signextend_shl.py b/test/formal/signextend_shl.py new file mode 100644 index 000000000..608b10eec --- /dev/null +++ b/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)) +) diff --git a/test/formal/signextend_shr.py b/test/formal/signextend_shr.py new file mode 100644 index 000000000..4364e6a23 --- /dev/null +++ b/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) +) + From 59db0f1537038cb355587b12be994b2187e7e8a8 Mon Sep 17 00:00:00 2001 From: hrkrshnn Date: Tue, 10 Aug 2021 12:55:34 +0200 Subject: [PATCH 3/4] An equivalence check for SIGNEXTEND opcode Checking the implementation of SIGNEXTEND using Z3's native SignExt and Extract --- test/formal/signextend_equivalence.py | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test/formal/signextend_equivalence.py diff --git a/test/formal/signextend_equivalence.py b/test/formal/signextend_equivalence.py new file mode 100644 index 000000000..1199fff47 --- /dev/null +++ b/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) From 4480662a582609bdae54ae8d9303aefa1c0311ec Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 12 Aug 2021 15:29:53 +0200 Subject: [PATCH 4/4] Test. --- .../fullSuite/shift_signextend.yul | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 test/libyul/yulOptimizerTests/fullSuite/shift_signextend.yul diff --git a/test/libyul/yulOptimizerTests/fullSuite/shift_signextend.yul b/test/libyul/yulOptimizerTests/fullSuite/shift_signextend.yul new file mode 100644 index 000000000..6e86edb8d --- /dev/null +++ b/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))) +// } +// }