Merge pull request #6935 from ethereum/subMaxValueXNotXRule

Add optimization rule SUB(~0, X) -> NOT(X).

Changelog.md

@@ -5,6 +5,7 @@ Language Features:
 
 
 Compiler Features:
+ * Optimizer: Add rule to simplify SUB(~0, X) to NOT(X).
 
 
 

libevmasm/RuleList.h

@@ -123,6 +123,7 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart2(
 		{{Instruction::ADD, {X, 0}}, [=]{ return X; }, false},
 		{{Instruction::ADD, {0, X}}, [=]{ return X; }, false},
 		{{Instruction::SUB, {X, 0}}, [=]{ return X; }, false},
+		{{Instruction::SUB, {~u256(0), X}}, [=]() -> Pattern { return {Instruction::NOT, {X}}; }, false},
 		{{Instruction::MUL, {X, 0}}, [=]{ return u256(0); }, true},
 		{{Instruction::MUL, {0, X}}, [=]{ return u256(0); }, true},
 		{{Instruction::MUL, {X, 1}}, [=]{ return X; }, false},

test/formal/sub_not_zero_x_to_not_x_256.py

@@ -0,0 +1,26 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+SUB(~0, X) -> NOT(X)
+Requirements:
+"""
+
+rule = Rule()
+
+n_bits = 256
+
+# Input vars
+X = BitVec('X', n_bits)
+
+# Constants
+ZERO = BitVecVal(0, n_bits)
+
+# Non optimized result
+nonopt = SUB(~ZERO, X)
+
+# Optimized result
+opt = NOT(X)
+
+rule.check(nonopt, opt)