Merge pull request #9736 from ethereum/yul_smt

Reasoning based optimizer using integers only

docs/yul.rst

@@ -1110,6 +1110,7 @@ Abbreviation Full name
 ``L``        ``LoadResolver``
 ``M``        ``LoopInvariantCodeMotion``
 ``r``        ``RedundantAssignEliminator``
+``R``        ``ReasoningBasedSimplifier`` - highly experimental
 ``m``        ``Rematerialiser``
 ``V``        ``SSAReverser``
 ``a``        ``SSATransform``
@@ -1121,6 +1122,10 @@ Abbreviation Full name
 Some steps depend on properties ensured by ``BlockFlattener``, ``FunctionGrouper``, ``ForLoopInitRewriter``.
 For this reason the Yul optimizer always applies them before applying any steps supplied by the user.
 
+The ReasoningBasedSimplifier is an optimizer step that is currently not enabled
+in the default set of steps. It uses an SMT solver to simplify arithmetic expressions
+and boolean conditions. It has not received thorough testing or validation yet and can produce
+non-reproducible results, so please use with care!
 
 .. _erc20yul:
 

libsmtutil/CMakeLists.txt

@@ -9,6 +9,7 @@ set(sources
 	SolverInterface.h
 	Sorts.cpp
 	Sorts.h
+	Helpers.h
 )
 
 if (${Z3_FOUND})

libsmtutil/Helpers.h

@@ -0,0 +1,58 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libsmtutil/SolverInterface.h>
+
+namespace solidity::smtutil
+{
+
+/// Signed division in SMTLIB2 rounds differently than EVM.
+/// This does not check for division by zero!
+inline Expression signedDivision(Expression _left, Expression _right)
+{
+	return Expression::ite(
+		_left >= 0,
+		Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))),
+		Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right))
+	);
+}
+
+inline Expression abs(Expression _value)
+{
+	return Expression::ite(_value >= 0, _value, 0 - _value);
+}
+
+/// Signed modulo in SMTLIB2 behaves differently with regards
+/// to the sign than EVM.
+/// This does not check for modulo by zero!
+inline Expression signedModulo(Expression _left, Expression _right)
+{
+	return Expression::ite(
+		_left >= 0,
+		_left % _right,
+		Expression::ite(
+			(_left % _right) == 0,
+			0,
+			(_left % _right) - abs(_right)
+		)
+	);
+}
+
+}

libsolidity/formal/SMTEncoder.cpp

@@ -23,6 +23,7 @@
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <libsmtutil/SMTPortfolio.h>
+#include <libsmtutil/Helpers.h>
 
 #include <boost/range/adaptors.hpp>
 #include <boost/range/adaptor/reversed.hpp>
@@ -1497,11 +1498,7 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp
 {
 	// Signed division in SMTLIB2 rounds differently for negative division.
 	if (_type.isSigned())
-		return (smtutil::Expression::ite(
-			_left >= 0,
-			smtutil::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))),
-			smtutil::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right))
-		));
+		return signedDivision(_left, _right);
 	else
 		return _left / _right;
 }

libyul/CMakeLists.txt

@@ -132,6 +132,8 @@ add_library(yul
 	optimiser/OptimiserStep.h
 	optimiser/OptimizerUtilities.cpp
 	optimiser/OptimizerUtilities.h
+	optimiser/ReasoningBasedSimplifier.cpp
+	optimiser/ReasoningBasedSimplifier.h
 	optimiser/RedundantAssignEliminator.cpp
 	optimiser/RedundantAssignEliminator.h
 	optimiser/Rematerialiser.cpp
@@ -168,4 +170,5 @@ add_library(yul
 	optimiser/VarNameCleaner.cpp
 	optimiser/VarNameCleaner.h
 )
-target_link_libraries(yul PUBLIC evmasm solutil langutil)
+
+target_link_libraries(yul PUBLIC evmasm solutil langutil smtutil)

libyul/Dialect.cpp

@@ -33,6 +33,15 @@ Literal Dialect::zeroLiteralForType(solidity::yul::YulString _type) const
 	return {SourceLocation{}, LiteralKind::Number, "0"_yulstring, _type};
 }
 
+
+Literal Dialect::trueLiteral() const
+{
+	if (boolType != defaultType)
+		return {SourceLocation{}, LiteralKind::Boolean, "true"_yulstring, boolType};
+	else
+		return {SourceLocation{}, LiteralKind::Number, "1"_yulstring, defaultType};
+}
+
 bool Dialect::validTypeForLiteral(LiteralKind _kind, YulString, YulString _type) const
 {
 	if (_kind == LiteralKind::Boolean)

libyul/Dialect.h

@@ -77,6 +77,7 @@ struct Dialect: boost::noncopyable
 	virtual bool validTypeForLiteral(LiteralKind _kind, YulString _value, YulString _type) const;
 
 	virtual Literal zeroLiteralForType(YulString _type) const;
+	virtual Literal trueLiteral() const;
 
 	virtual std::set<YulString> fixedFunctionNames() const { return {}; }
 

libyul/optimiser/OptimiserStep.h

@@ -20,6 +20,7 @@
 
 #include <libyul/Exceptions.h>
 
+#include <optional>
 #include <string>
 #include <set>
 
@@ -49,17 +50,41 @@ struct OptimiserStep
 	virtual ~OptimiserStep() = default;
 
 	virtual void run(OptimiserStepContext&, Block&) const = 0;
+	/// @returns non-nullopt if the step cannot be run, for example because it requires
+	/// an SMT solver to be loaded, but none is available. In that case, the string
+	/// contains a human-readable reason.
+	virtual std::optional<std::string> invalidInCurrentEnvironment() const = 0;
 	std::string name;
 };
 
 template <class Step>
 struct OptimiserStepInstance: public OptimiserStep
 {
+private:
+	template<typename T>
+	struct HasInvalidInCurrentEnvironmentMethod
+	{
+	private:
+		template<typename U> static auto test(int) -> decltype(U::invalidInCurrentEnvironment(), std::true_type());
+		template<typename> static std::false_type test(...);
+
+	public:
+		static constexpr bool value = decltype(test<T>(0))::value;
+	};
+
+public:
 	OptimiserStepInstance(): OptimiserStep{Step::name} {}
 	void run(OptimiserStepContext& _context, Block& _ast) const override
 	{
 		Step::run(_context, _ast);
 	}
+	std::optional<std::string> invalidInCurrentEnvironment() const override
+	{
+		if constexpr (HasInvalidInCurrentEnvironmentMethod<Step>::value)
+			return Step::invalidInCurrentEnvironment();
+		else
+			return std::nullopt;
+	};
 };
 
 

libyul/optimiser/ReasoningBasedSimplifier.cpp

@@ -0,0 +1,339 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libyul/optimiser/ReasoningBasedSimplifier.h>
+
+#include <libyul/optimiser/SSAValueTracker.h>
+#include <libyul/optimiser/Semantics.h>
+#include <libyul/AsmData.h>
+#include <libyul/Utilities.h>
+#include <libyul/Dialect.h>
+
+#include <libyul/backends/evm/EVMDialect.h>
+
+#include <libsmtutil/SMTPortfolio.h>
+#include <libsmtutil/Helpers.h>
+
+#include <libsolutil/Visitor.h>
+#include <libsolutil/CommonData.h>
+
+#include <utility>
+#include <memory>
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::yul;
+using namespace solidity::smtutil;
+
+void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _ast)
+{
+	set<YulString> ssaVars = SSAValueTracker::ssaVariables(_ast);
+	ReasoningBasedSimplifier{_context.dialect, ssaVars}(_ast);
+}
+
+std::optional<string> ReasoningBasedSimplifier::invalidInCurrentEnvironment()
+{
+	// SMTLib2 interface is always available, but we would like to have synchronous answers.
+	if (smtutil::SMTPortfolio{}.solvers() <= 1)
+		return string{"No SMT solvers available."};
+	else
+		return nullopt;
+}
+
+void ReasoningBasedSimplifier::operator()(VariableDeclaration& _varDecl)
+{
+	if (_varDecl.variables.size() != 1 || !_varDecl.value)
+		return;
+	YulString varName = _varDecl.variables.front().name;
+	if (!m_ssaVariables.count(varName))
+		return;
+	bool const inserted = m_variables.insert({varName, m_solver->newVariable("yul_" + varName.str(), defaultSort())}).second;
+	yulAssert(inserted, "");
+	m_solver->addAssertion(m_variables.at(varName) == encodeExpression(*_varDecl.value));
+}
+
+void ReasoningBasedSimplifier::operator()(If& _if)
+{
+	if (!SideEffectsCollector{m_dialect, *_if.condition}.movable())
+		return;
+
+	smtutil::Expression condition = encodeExpression(*_if.condition);
+	m_solver->push();
+	m_solver->addAssertion(condition == constantValue(0));
+	CheckResult result = m_solver->check({}).first;
+	m_solver->pop();
+	if (result == CheckResult::UNSATISFIABLE)
+	{
+		Literal trueCondition = m_dialect.trueLiteral();
+		trueCondition.location = locationOf(*_if.condition);
+		_if.condition = make_unique<yul::Expression>(move(trueCondition));
+	}
+	else
+	{
+		m_solver->push();
+		m_solver->addAssertion(condition != constantValue(0));
+		CheckResult result2 = m_solver->check({}).first;
+		m_solver->pop();
+		if (result2 == CheckResult::UNSATISFIABLE)
+		{
+			Literal falseCondition = m_dialect.zeroLiteralForType(m_dialect.boolType);
+			falseCondition.location = locationOf(*_if.condition);
+			_if.condition = make_unique<yul::Expression>(move(falseCondition));
+			_if.body = yul::Block{};
+			// Nothing left to be done.
+			return;
+		}
+	}
+
+	m_solver->push();
+	m_solver->addAssertion(condition != constantValue(0));
+
+	ASTModifier::operator()(_if.body);
+
+	m_solver->pop();
+}
+
+ReasoningBasedSimplifier::ReasoningBasedSimplifier(
+	Dialect const& _dialect,
+	set<YulString> const& _ssaVariables
+):
+	m_dialect(_dialect),
+	m_ssaVariables(_ssaVariables),
+	m_solver(make_unique<smtutil::SMTPortfolio>())
+{
+}
+
+smtutil::Expression ReasoningBasedSimplifier::encodeExpression(yul::Expression const& _expression)
+{
+	return std::visit(GenericVisitor{
+		[&](FunctionCall const& _functionCall)
+		{
+			if (auto const* dialect = dynamic_cast<EVMDialect const*>(&m_dialect))
+				if (auto const* builtin = dialect->builtin(_functionCall.functionName.name))
+					if (builtin->instruction)
+						return encodeEVMBuiltin(*builtin->instruction, _functionCall.arguments);
+			return newRestrictedVariable();
+		},
+		[&](Identifier const& _identifier)
+		{
+			if (
+				m_ssaVariables.count(_identifier.name) &&
+				m_variables.count(_identifier.name)
+			)
+				return m_variables.at(_identifier.name);
+			else
+				return newRestrictedVariable();
+		},
+		[&](Literal const& _literal)
+		{
+			return literalValue(_literal);
+		}
+	}, _expression);
+}
+
+smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
+	evmasm::Instruction _instruction,
+	vector<yul::Expression> const& _arguments
+)
+{
+	vector<smtutil::Expression> arguments = applyMap(
+		_arguments,
+		[this](yul::Expression const& _expr) { return encodeExpression(_expr); }
+	);
+	switch (_instruction)
+	{
+	case evmasm::Instruction::ADD:
+		return wrap(arguments.at(0) + arguments.at(1));
+	case evmasm::Instruction::MUL:
+		return wrap(arguments.at(0) * arguments.at(1));
+	case evmasm::Instruction::SUB:
+		return wrap(arguments.at(0) - arguments.at(1));
+	case evmasm::Instruction::DIV:
+		return smtutil::Expression::ite(
+			arguments.at(1) == constantValue(0),
+			constantValue(0),
+			arguments.at(0) / arguments.at(1)
+		);
+	case evmasm::Instruction::SDIV:
+		return smtutil::Expression::ite(
+			arguments.at(1) == constantValue(0),
+			constantValue(0),
+			// No `wrap()` needed here, because -2**255 / -1 results
+			// in 2**255 which is "converted" to its two's complement
+			// representation 2**255 in `signedToUnsigned`
+			signedToUnsigned(smtutil::signedDivision(
+				unsignedToSigned(arguments.at(0)),
+				unsignedToSigned(arguments.at(1))
+			))
+		);
+		break;
+	case evmasm::Instruction::MOD:
+		return smtutil::Expression::ite(
+			arguments.at(1) == constantValue(0),
+			constantValue(0),
+			arguments.at(0) % arguments.at(1)
+		);
+	case evmasm::Instruction::SMOD:
+		return smtutil::Expression::ite(
+			arguments.at(1) == constantValue(0),
+			constantValue(0),
+			signedToUnsigned(signedModulo(
+				unsignedToSigned(arguments.at(0)),
+				unsignedToSigned(arguments.at(1))
+			))
+		);
+		break;
+	case evmasm::Instruction::LT:
+		return booleanValue(arguments.at(0) < arguments.at(1));
+	case evmasm::Instruction::SLT:
+		return booleanValue(unsignedToSigned(arguments.at(0)) < unsignedToSigned(arguments.at(1)));
+	case evmasm::Instruction::GT:
+		return booleanValue(arguments.at(0) > arguments.at(1));
+	case evmasm::Instruction::SGT:
+		return booleanValue(unsignedToSigned(arguments.at(0)) > unsignedToSigned(arguments.at(1)));
+	case evmasm::Instruction::EQ:
+		return booleanValue(arguments.at(0) == arguments.at(1));
+	case evmasm::Instruction::ISZERO:
+		return booleanValue(arguments.at(0) == constantValue(0));
+	case evmasm::Instruction::AND:
+		return smtutil::Expression::ite(
+			(arguments.at(0) == 0 || arguments.at(0) == 1) &&
+			(arguments.at(1) == 0 || arguments.at(1) == 1),
+			booleanValue(arguments.at(0) == 1 && arguments.at(1) == 1),
+			bv2int(int2bv(arguments.at(0)) & int2bv(arguments.at(1)))
+		);
+	case evmasm::Instruction::OR:
+		return smtutil::Expression::ite(
+			(arguments.at(0) == 0 || arguments.at(0) == 1) &&
+			(arguments.at(1) == 0 || arguments.at(1) == 1),
+			booleanValue(arguments.at(0) == 1 || arguments.at(1) == 1),
+			bv2int(int2bv(arguments.at(0)) | int2bv(arguments.at(1)))
+		);
+	case evmasm::Instruction::XOR:
+		return bv2int(int2bv(arguments.at(0)) ^ int2bv(arguments.at(1)));
+	case evmasm::Instruction::NOT:
+		return smtutil::Expression(u256(-1)) - arguments.at(0);
+	case evmasm::Instruction::SHL:
+		return smtutil::Expression::ite(
+			arguments.at(0) > 255,
+			constantValue(0),
+			bv2int(int2bv(arguments.at(1)) << int2bv(arguments.at(0)))
+		);
+	case evmasm::Instruction::SHR:
+		return smtutil::Expression::ite(
+			arguments.at(0) > 255,
+			constantValue(0),
+			bv2int(int2bv(arguments.at(1)) >> int2bv(arguments.at(0)))
+		);
+	case evmasm::Instruction::SAR:
+		return smtutil::Expression::ite(
+			arguments.at(0) > 255,
+			constantValue(0),
+			bv2int(smtutil::Expression::ashr(int2bv(arguments.at(1)), int2bv(arguments.at(0))))
+		);
+	case evmasm::Instruction::ADDMOD:
+		return smtutil::Expression::ite(
+			arguments.at(2) == constantValue(0),
+			constantValue(0),
+			(arguments.at(0) + arguments.at(1)) % arguments.at(2)
+		);
+	case evmasm::Instruction::MULMOD:
+		return smtutil::Expression::ite(
+			arguments.at(2) == constantValue(0),
+			constantValue(0),
+			(arguments.at(0) * arguments.at(1)) % arguments.at(2)
+		);
+	// TODO SIGNEXTEND
+	default:
+		break;
+	}
+	return newRestrictedVariable();
+}
+
+smtutil::Expression ReasoningBasedSimplifier::int2bv(smtutil::Expression _arg) const
+{
+	return smtutil::Expression::int2bv(std::move(_arg), 256);
+}
+
+smtutil::Expression ReasoningBasedSimplifier::bv2int(smtutil::Expression _arg) const
+{
+	return smtutil::Expression::bv2int(std::move(_arg));
+}
+
+smtutil::Expression ReasoningBasedSimplifier::newVariable()
+{
+	return m_solver->newVariable(uniqueName(), defaultSort());
+}
+
+smtutil::Expression ReasoningBasedSimplifier::newRestrictedVariable()
+{
+	smtutil::Expression var = newVariable();
+	m_solver->addAssertion(0 <= var && var < smtutil::Expression(bigint(1) << 256));
+	return var;
+}
+
+string ReasoningBasedSimplifier::uniqueName()
+{
+	return "expr_" + to_string(m_varCounter++);
+}
+
+shared_ptr<Sort> ReasoningBasedSimplifier::defaultSort() const
+{
+	return SortProvider::intSort();
+}
+
+smtutil::Expression ReasoningBasedSimplifier::booleanValue(smtutil::Expression _value) const
+{
+	return smtutil::Expression::ite(_value, constantValue(1), constantValue(0));
+}
+
+smtutil::Expression ReasoningBasedSimplifier::constantValue(size_t _value) const
+{
+	return _value;
+}
+
+smtutil::Expression ReasoningBasedSimplifier::literalValue(Literal const& _literal) const
+{
+	return smtutil::Expression(valueOfLiteral(_literal));
+}
+
+smtutil::Expression ReasoningBasedSimplifier::unsignedToSigned(smtutil::Expression _value)
+{
+	return smtutil::Expression::ite(
+		_value < smtutil::Expression(bigint(1) << 255),
+		_value,
+		_value - smtutil::Expression(bigint(1) << 256)
+	);
+}
+
+smtutil::Expression ReasoningBasedSimplifier::signedToUnsigned(smtutil::Expression _value)
+{
+	return smtutil::Expression::ite(
+		_value >= 0,
+		_value,
+		_value + smtutil::Expression(bigint(1) << 256)
+	);
+}
+
+smtutil::Expression ReasoningBasedSimplifier::wrap(smtutil::Expression _value)
+{
+	smtutil::Expression rest = newRestrictedVariable();
+	smtutil::Expression multiplier = newVariable();
+	m_solver->addAssertion(_value == multiplier * smtutil::Expression(bigint(1) << 256) + rest);
+	return rest;
+}

libyul/optimiser/ReasoningBasedSimplifier.h

@@ -0,0 +1,98 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+#pragma once
+
+#include <libyul/optimiser/ASTWalker.h>
+#include <libyul/optimiser/OptimiserStep.h>
+#include <libyul/Dialect.h>
+
+// because of instruction
+#include <libyul/backends/evm/EVMDialect.h>
+
+#include <map>
+
+namespace solidity::smtutil
+{
+class SolverInterface;
+class Expression;
+struct Sort;
+}
+
+namespace solidity::yul
+{
+
+/**
+ * Reasoning-based simplifier.
+ * This optimizer uses SMT solvers to check whether `if` conditions are constant.
+ * - If `constraints AND condition` is UNSAT, the condition is never true and the whole body can be removed.
+ * - If `constraints AND NOT condition` is UNSAT, the condition is always true and can be replaced by `1`.
+ * The simplifications above can only be applied if the condition is movable.
+ *
+ * It is only effective on the EVM dialect, but safe to use on other dialects.
+ *
+ * Prerequisite: Disambiguator, SSATransform.
+ */
+class ReasoningBasedSimplifier: public ASTModifier
+{
+public:
+	static constexpr char const* name{"ReasoningBasedSimplifier"};
+	static void run(OptimiserStepContext& _context, Block& _ast);
+	static std::optional<std::string> invalidInCurrentEnvironment();
+
+	using ASTModifier::operator();
+	void operator()(VariableDeclaration& _varDecl) override;
+	void operator()(If& _if) override;
+
+private:
+	explicit ReasoningBasedSimplifier(
+		Dialect const& _dialect,
+		std::set<YulString> const& _ssaVariables
+	);
+
+	smtutil::Expression encodeExpression(
+		Expression const& _expression
+	);
+
+	virtual smtutil::Expression encodeEVMBuiltin(
+		evmasm::Instruction _instruction,
+		std::vector<Expression> const& _arguments
+	);
+
+	smtutil::Expression int2bv(smtutil::Expression _arg) const;
+	smtutil::Expression bv2int(smtutil::Expression _arg) const;
+
+	smtutil::Expression newVariable();
+	virtual smtutil::Expression newRestrictedVariable();
+	std::string uniqueName();
+
+	virtual std::shared_ptr<smtutil::Sort> defaultSort() const;
+	virtual smtutil::Expression booleanValue(smtutil::Expression _value) const;
+	virtual smtutil::Expression constantValue(size_t _value) const;
+	virtual smtutil::Expression literalValue(Literal const& _literal) const;
+	virtual smtutil::Expression unsignedToSigned(smtutil::Expression _value);
+	virtual smtutil::Expression signedToUnsigned(smtutil::Expression _value);
+	virtual smtutil::Expression wrap(smtutil::Expression _value);
+
+	Dialect const& m_dialect;
+	std::set<YulString> const& m_ssaVariables;
+	std::unique_ptr<smtutil::SolverInterface> m_solver;
+	std::map<YulString, smtutil::Expression> m_variables;
+
+	size_t m_varCounter = 0;
+};
+
+}

libyul/optimiser/Suite.cpp

@@ -41,6 +41,7 @@
 #include <libyul/optimiser/ForLoopConditionOutOfBody.h>
 #include <libyul/optimiser/ForLoopInitRewriter.h>
 #include <libyul/optimiser/ForLoopConditionIntoBody.h>
+#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/optimiser/Rematerialiser.h>
 #include <libyul/optimiser/UnusedFunctionParameterPruner.h>
 #include <libyul/optimiser/UnusedPruner.h>
@@ -184,6 +185,7 @@ map<string, unique_ptr<OptimiserStep>> const& OptimiserSuite::allSteps()
 			LoopInvariantCodeMotion,
 			NameSimplifier,
 			RedundantAssignEliminator,
+			ReasoningBasedSimplifier,
 			Rematerialiser,
 			SSAReverser,
 			SSATransform,
@@ -221,6 +223,7 @@ map<string, char> const& OptimiserSuite::stepNameToAbbreviationMap()
 		{LoadResolver::name,                  'L'},
 		{LoopInvariantCodeMotion::name,       'M'},
 		{NameSimplifier::name,                'N'},
+		{ReasoningBasedSimplifier::name,      'R'},
 		{RedundantAssignEliminator::name,     'r'},
 		{Rematerialiser::name,                'm'},
 		{SSAReverser::name,                   'V'},
@@ -266,6 +269,7 @@ void OptimiserSuite::validateSequence(string const& _stepAbbreviations)
 			insideLoop = false;
 			break;
 		default:
+		{
 			yulAssert(
 				string(NonStepAbbreviations).find(abbreviation) == string::npos,
 				"Unhandled syntactic element in the abbreviation sequence"
@@ -275,6 +279,14 @@ void OptimiserSuite::validateSequence(string const& _stepAbbreviations)
 				OptimizerException,
 				"'"s + abbreviation + "' is not a valid step abbreviation"
 			);
+			optional<string> invalid = allSteps().at(stepAbbreviationToNameMap().at(abbreviation))->invalidInCurrentEnvironment();
+			assertThrow(
+				!invalid.has_value(),
+				OptimizerException,
+				"'"s + abbreviation + "' is invalid in the current environment: " + *invalid
+			);
+
+		}
 		}
 	assertThrow(!insideLoop, OptimizerException, "Unbalanced brackets");
 }

test/libsolidity/semanticTests/arithmetics/signed_mod.sol

@@ -0,0 +1,14 @@
+contract C {
+    function f(int a, int b) public pure returns (int) {
+        return a % b;
+    }
+}
+
+// ====
+// compileViaYul: also
+// ----
+// f(int256,int256): 7, 5 -> 2
+// f(int256,int256): 7, -5 -> 2
+// f(int256,int256): -7, 5 -> -2
+// f(int256,int256): -7, 5 -> -2
+// f(int256,int256): -5, -5 -> 0

test/libyul/YulOptimizerTest.cpp

@@ -53,6 +53,7 @@
 #include <libyul/optimiser/UnusedPruner.h>
 #include <libyul/optimiser/ExpressionJoiner.h>
 #include <libyul/optimiser/OptimiserStep.h>
+#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/optimiser/SSAReverser.h>
 #include <libyul/optimiser/SSATransform.h>
 #include <libyul/optimiser/Semantics.h>
@@ -102,6 +103,9 @@ YulOptimizerTest::YulOptimizerTest(string const& _filename):
 		BOOST_THROW_EXCEPTION(runtime_error("Filename path has to contain a directory: \"" + _filename + "\"."));
 	m_optimizerStep = std::prev(std::prev(path.end()))->string();
 
+	if (m_optimizerStep == "reasoningBasedSimplifier" && solidity::test::CommonOptions::get().disableSMT)
+		m_shouldRun = false;
+
 	m_source = m_reader.source();
 
 	auto dialectName = m_reader.stringSetting("dialect", "evm");
@@ -320,6 +324,11 @@ TestCase::TestResult YulOptimizerTest::run(ostream& _stream, string const& _line
 		LiteralRematerialiser::run(*m_context, *m_object->code);
 		StructuralSimplifier::run(*m_context, *m_object->code);
 	}
+	else if (m_optimizerStep == "reasoningBasedSimplifier")
+	{
+		disambiguate();
+		ReasoningBasedSimplifier::run(*m_context, *m_object->code);
+	}
 	else if (m_optimizerStep == "equivalentFunctionCombiner")
 	{
 		disambiguate();

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul

@@ -0,0 +1,31 @@
+{
+    let x := calldataload(0)
+    let y := calldataload(32)
+    let z := calldataload(64)
+    let result := addmod(x, y, z)
+
+    // should be zero
+    if gt(result, z) { sstore(0, 1) }
+
+    // addmod is equal to mod of sum for small numbers
+    if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) {
+        if eq(result, mod(add(x, y), z)) { sstore(0, 9) }
+    }
+
+    // but not in general
+    if and(and(gt(x, sub(0, 5)), gt(y, sub(0, 2))), eq(z, 3)) {
+        if eq(result, mod(add(x, y), z)) { sstore(0, 5) }
+    }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := calldataload(0)
+//     let y := calldataload(32)
+//     let z := calldataload(64)
+//     let result := addmod(x, y, z)
+//     if 0 { }
+//     if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { if 1 { sstore(0, 9) } }
+//     if and(and(gt(x, sub(0, 5)), gt(y, sub(0, 2))), eq(z, 3)) { if 0 { } }
+// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul

@@ -0,0 +1,13 @@
+{
+    let x := 7
+    let y := 8
+    if eq(add(x, y), 15) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := 7
+//     let y := 8
+//     if 1 { }
+// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul

@@ -0,0 +1,19 @@
+{
+	function f() -> z
+	{
+		z := 15
+	}
+	let x := 7
+	let y := 8
+	if eq(add(x, y), f()) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     function f() -> z
+//     { z := 15 }
+//     let x := 7
+//     let y := 8
+//     if eq(add(x, y), f()) { }
+// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul

@@ -0,0 +1,23 @@
+{
+	function f() -> z
+	{
+		sstore(1, 15)
+		z := 15
+	}
+	let x := 7
+	let y := 8
+	if eq(add(x, y), f()) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     function f() -> z
+//     {
+//         sstore(1, 15)
+//         z := 15
+//     }
+//     let x := 7
+//     let y := 8
+//     if eq(add(x, y), f()) { }
+// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul

@@ -0,0 +1,32 @@
+{
+    let vloc_x := calldataload(0)
+    let vloc_y := calldataload(1)
+    if lt(vloc_x, shl(100, 1)) {
+        if lt(vloc_y, shl(100, 1)) {
+            if iszero(and(iszero(iszero(vloc_x)), gt(vloc_y, div(not(0), vloc_x)))) {
+                let vloc := mul(vloc_x, vloc_y)
+                sstore(0, vloc)
+            }
+        }
+    }
+}
+// ====
+// EVMVersion: >=constantinople
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let vloc_x := calldataload(0)
+//     let vloc_y := calldataload(1)
+//     if lt(vloc_x, shl(100, 1))
+//     {
+//         if lt(vloc_y, shl(100, 1))
+//         {
+//             if 1
+//             {
+//                 let vloc := mul(vloc_x, vloc_y)
+//                 sstore(0, vloc)
+//             }
+//         }
+//     }
+// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul

@@ -0,0 +1,31 @@
+{
+    let x := calldataload(0)
+    let y := calldataload(32)
+    let z := calldataload(64)
+    let result := mulmod(x, y, z)
+
+    // should be zero
+    if gt(result, z) { sstore(0, 1) }
+
+    // mulmod is equal to mod of product for small numbers
+    if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) {
+        if eq(result, mod(mul(x, y), z)) { sstore(0, 9) }
+    }
+
+    // but not in general
+    if and(and(gt(x, sub(0, 5)), eq(y, 2)), eq(z, 3)) {
+        if eq(result, mod(mul(x, y), z)) { sstore(0, 5) }
+    }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := calldataload(0)
+//     let y := calldataload(32)
+//     let z := calldataload(64)
+//     let result := mulmod(x, y, z)
+//     if 0 { }
+//     if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { if 1 { sstore(0, 9) } }
+//     if and(and(gt(x, sub(0, 5)), eq(y, 2)), eq(z, 3)) { if 0 { } }
+// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul

@@ -0,0 +1,16 @@
+{
+    let x := sub(0, 7)
+    let y := 2
+    // (-7)/2 == -3 on the evm
+    if iszero(add(sdiv(x, y), 3)) { }
+    if iszero(add(sdiv(x, y), 4)) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := sub(0, 7)
+//     let y := 2
+//     if 1 { }
+//     if 0 { }
+// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul

@@ -0,0 +1,26 @@
+{
+    let x := calldataload(2)
+    let t := lt(x, 20)
+    if t {
+        if lt(x, 21) { }
+        if lt(x, 20) { }
+        if lt(x, 19) { }
+        if gt(x, 20) { }
+        if iszero(gt(x, 20)) { }
+    }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := calldataload(2)
+//     let t := lt(x, 20)
+//     if t
+//     {
+//         if 1 { }
+//         if 1 { }
+//         if lt(x, 19) { }
+//         if 0 { }
+//         if 1 { }
+//     }
+// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul

@@ -0,0 +1,31 @@
+{
+    let y := calldataload(0)
+    let t := calldataload(32)
+
+    if sgt(sub(y, 1), y) {
+        // y - 1 > y, i.e. y is the most negative value
+        if eq(sdiv(y, sub(0, 1)), y) {
+            // should be true: y / -1 == y
+            sstore(0, 7)
+        }
+        if iszero(eq(y, t)) {
+            // t is not the most negative value
+            if eq(sdiv(t, sub(0, 1)), sub(0, t)) {
+                // should be true: t / -1 = 0 - t
+                sstore(1, 7)
+            }
+        }
+    }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let y := calldataload(0)
+//     let t := calldataload(32)
+//     if sgt(sub(y, 1), y)
+//     {
+//         if 1 { sstore(0, 7) }
+//         if iszero(eq(y, t)) { if 1 { sstore(1, 7) } }
+//     }
+// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul

@@ -0,0 +1,53 @@
+{
+    // 7 % 5 == 2
+    // 7 % -5 == 2
+    // -7 % 5 == -2
+    // -7 % -5 == -2
+    // -5 % -5 == 0
+    let x := calldataload(0)
+    let y := calldataload(32)
+    let result := smod(x, y)
+    if eq(x, 7) {
+        if eq(y, 5) {
+            if eq(result, 2) { sstore(0, 7)}
+        }
+        if eq(y, sub(0, 5)) {
+            if eq(result, 2) { sstore(0, 7)}
+        }
+    }
+    if eq(x, sub(0, 7)) {
+        if eq(y, 5) {
+            if eq(result, sub(0, 2)) { sstore(0, 7)}
+        }
+        if eq(y, sub(0, 5)) {
+            if eq(result, sub(0, 2)) { sstore(0, 7)}
+        }
+    }
+    if eq(x, sub(0, 5)) {
+        if eq(y, sub(0, 5)) {
+            if eq(result, 0) { sstore(0, 7)}
+        }
+    }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := calldataload(0)
+//     let y := calldataload(32)
+//     let result := smod(x, y)
+//     if eq(x, 7)
+//     {
+//         if eq(y, 5) { if 1 { sstore(0, 7) } }
+//         if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } }
+//     }
+//     if eq(x, sub(0, 7))
+//     {
+//         if eq(y, 5) { if 1 { sstore(0, 7) } }
+//         if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } }
+//     }
+//     if eq(x, sub(0, 5))
+//     {
+//         if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } }
+//     }
+// }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul

@@ -0,0 +1,5 @@
+{ }
+// ----
+// step: reasoningBasedSimplifier
+//
+// { }

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul

@@ -0,0 +1,15 @@
+{
+    let x := 7
+    let y := 8
+    if gt(sub(x, y), 20) { }
+    if eq(sub(x, y), 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) {}
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := 7
+//     let y := 8
+//     if 1 { }
+//     if 1 { }
+// }

test/tools/yulopti.cpp

@@ -36,6 +36,7 @@
 #include <libyul/optimiser/StackCompressor.h>
 #include <libyul/optimiser/VarNameCleaner.h>
 #include <libyul/optimiser/Suite.h>
+#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 
 #include <libyul/backends/evm/EVMDialect.h>
 
@@ -157,7 +158,7 @@ public:
 			map<char, string> const& extraOptions = {
 				{'#', "quit"},
 				{',', "VarNameCleaner"},
-				{';', "StackCompressor"},
+				{';', "StackCompressor"}
 			};
 
 			printUsageBanner(abbreviationMap, extraOptions, 4);

test/yulPhaser/Chromosome.cpp

@@ -138,7 +138,7 @@ BOOST_AUTO_TEST_CASE(output_operator_should_create_concise_and_unambiguous_strin
 
 	BOOST_TEST(chromosome.length() == allSteps.size());
 	BOOST_TEST(chromosome.optimisationSteps() == allSteps);
-	BOOST_TEST(toString(chromosome) == "flcCUnDvejsxIOoighTLMNrmVatpud");
+	BOOST_TEST(toString(chromosome) == "flcCUnDvejsxIOoighTLMNRrmVatpud");
 }
 
 BOOST_AUTO_TEST_CASE(optimisationSteps_should_translate_chromosomes_genes_to_optimisation_step_names)