Merge pull request #14370 from ethereum/smt-cleanup

Remove ReasoningBasedSimplifier from libyul

Changelog.md

@@ -12,6 +12,7 @@ Compiler Features:
  * SMTChecker: Add ``--model-checker-print-query`` CLI option and ``settings.modelChecker.printQuery`` JSON option to output the SMTChecker queries in the SMTLIB2 format. This requires using `smtlib2` solver only.
  * Standard JSON Interface: Add ``ast`` file-level output for Yul input.
  * Standard JSON Interface: Add ``irAst`` and ``irOptimizedAst`` contract-level outputs for Solidity input, providing AST in compact JSON format for IR and optimized IR.
+ * Yul Optimizer: Remove experimental `ReasoningBasedSimplifier` optimization step.
  * Yul Optimizer: Stack-to-memory mover is now enabled by default whenever possible for via IR code generation and pure Yul compilation.
 
 

docs/internals/optimizer.rst

@@ -316,7 +316,6 @@ Abbreviation Full name
 ``L``        :ref:`load-resolver`
 ``M``        :ref:`loop-invariant-code-motion`
 ``r``        :ref:`redundant-assign-eliminator`
-``R``        :ref:`reasoning-based-simplifier` - highly experimental
 ``m``        :ref:`rematerialiser`
 ``V``        :ref:`SSA-reverser`
 ``a``        :ref:`SSA-transform`
@@ -330,10 +329,6 @@ 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!
 
 Selecting Optimizations
 -----------------------
@@ -863,22 +858,6 @@ Works best if the code is in SSA form.
 
 Prerequisite: Disambiguator, ForLoopInitRewriter.
 
-.. _reasoning-based-simplifier:
-
-ReasoningBasedSimplifier
-^^^^^^^^^^^^^^^^^^^^^^^^
-
-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.
-
 Statement-Scale Simplifications
 -------------------------------
 

libyul/CMakeLists.txt

@@ -143,8 +143,6 @@ add_library(yul
 	optimiser/OptimiserStep.h
 	optimiser/OptimizerUtilities.cpp
 	optimiser/OptimizerUtilities.h
-	optimiser/ReasoningBasedSimplifier.cpp
-	optimiser/ReasoningBasedSimplifier.h
 	optimiser/UnusedAssignEliminator.cpp
 	optimiser/UnusedAssignEliminator.h
 	optimiser/UnusedStoreBase.cpp
@@ -153,8 +151,6 @@ add_library(yul
 	optimiser/UnusedStoreEliminator.h
 	optimiser/Rematerialiser.cpp
 	optimiser/Rematerialiser.h
-	optimiser/SMTSolver.cpp
-	optimiser/SMTSolver.h
 	optimiser/SSAReverser.cpp
 	optimiser/SSAReverser.h
 	optimiser/SSATransform.cpp

libyul/optimiser/ReasoningBasedSimplifier.cpp

@@ -1,228 +0,0 @@
-/*
-	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/SMTSolver.h>
-
-#include <libyul/optimiser/SSAValueTracker.h>
-#include <libyul/optimiser/Semantics.h>
-#include <libyul/AST.h>
-#include <libyul/Dialect.h>
-
-#include <libsmtutil/SMTPortfolio.h>
-#include <libsmtutil/Helpers.h>
-
-#include <libsolutil/CommonData.h>
-
-#include <libevmasm/Instruction.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)
-{
-	SMTSolver::encodeVariableDeclaration(_varDecl);
-}
-
-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.debugData = debugDataOf(*_if.condition);
-		_if.condition = make_unique<yul::Expression>(std::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.debugData = debugDataOf(*_if.condition);
-			_if.condition = make_unique<yul::Expression>(std::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
-):
-	SMTSolver(_ssaVariables, _dialect),
-	m_dialect(_dialect)
-{
-}
-
-
-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 `signedToTwosComplement`
-			signedToTwosComplement(smtutil::signedDivisionEVM(
-				twosComplementToSigned(arguments.at(0)),
-				twosComplementToSigned(arguments.at(1))
-			))
-		);
-	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),
-			signedToTwosComplement(signedModuloEVM(
-				twosComplementToSigned(arguments.at(0)),
-				twosComplementToSigned(arguments.at(1))
-			))
-		);
-	case evmasm::Instruction::LT:
-		return booleanValue(arguments.at(0) < arguments.at(1));
-	case evmasm::Instruction::SLT:
-		return booleanValue(twosComplementToSigned(arguments.at(0)) < twosComplementToSigned(arguments.at(1)));
-	case evmasm::Instruction::GT:
-		return booleanValue(arguments.at(0) > arguments.at(1));
-	case evmasm::Instruction::SGT:
-		return booleanValue(twosComplementToSigned(arguments.at(0)) > twosComplementToSigned(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();
-}

libyul/optimiser/ReasoningBasedSimplifier.h

@@ -1,75 +0,0 @@
-/*
-	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/SMTSolver.h>
-#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, SMTSolver
-{
-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 encodeEVMBuiltin(
-		evmasm::Instruction _instruction,
-		std::vector<Expression> const& _arguments
-	) override;
-
-	Dialect const& m_dialect;
-};
-
-}

libyul/optimiser/SMTSolver.cpp

@@ -1,160 +0,0 @@
-/*
-	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/SMTSolver.h>
-#include <libyul/optimiser/OptimizerUtilities.h>
-
-#include <libyul/AST.h>
-#include <libyul/Utilities.h>
-
-#include <libsolutil/Visitor.h>
-#include <libsolutil/CommonData.h>
-
-#include <libsmtutil/SMTPortfolio.h>
-#include <libsmtutil/Helpers.h>
-
-using namespace solidity::yul;
-using namespace solidity::util;
-using namespace solidity::smtutil;
-using namespace solidity;
-using namespace std;
-
-SMTSolver::SMTSolver(set<YulString> const& _ssaVariables, Dialect const& _dialect):
-	m_ssaVariables(_ssaVariables),
-	m_solver(make_unique<smtutil::SMTPortfolio>()),
-	m_dialect(_dialect)
-{ }
-
-smtutil::Expression SMTSolver::encodeExpression(Expression const& _expression)
-{
-	return std::visit(GenericVisitor{
-		[&](FunctionCall const& _functionCall)
-		{
-			if (auto instruction = toEVMInstruction(m_dialect, _functionCall.functionName.name))
-				return encodeEVMBuiltin(*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 SMTSolver::int2bv(smtutil::Expression _arg)
-{
-	return smtutil::Expression::int2bv(std::move(_arg), 256);
-}
-
-smtutil::Expression SMTSolver::bv2int(smtutil::Expression _arg)
-{
-	return smtutil::Expression::bv2int(std::move(_arg));
-}
-
-smtutil::Expression SMTSolver::newVariable()
-{
-	return m_solver->newVariable(uniqueName(), defaultSort());
-}
-
-smtutil::Expression SMTSolver::newRestrictedVariable(bigint _maxValue)
-{
-	smtutil::Expression var = newVariable();
-	m_solver->addAssertion(0 <= var && var <= smtutil::Expression(_maxValue));
-	return var;
-}
-
-string SMTSolver::uniqueName()
-{
-	return "expr_" + to_string(m_varCounter++);
-}
-
-shared_ptr<Sort> SMTSolver::defaultSort() const
-{
-	return SortProvider::intSort();
-}
-
-smtutil::Expression SMTSolver::booleanValue(smtutil::Expression _value)
-{
-	return smtutil::Expression::ite(_value, constantValue(1), constantValue(0));
-}
-
-smtutil::Expression SMTSolver::constantValue(bigint _value)
-{
-	return _value;
-}
-
-smtutil::Expression SMTSolver::literalValue(Literal const& _literal)
-{
-	return smtutil::Expression(valueOfLiteral(_literal));
-}
-
-smtutil::Expression SMTSolver::twosComplementToSigned(smtutil::Expression _value)
-{
-	return smtutil::Expression::ite(
-		_value < smtutil::Expression(bigint(1) << 255),
-		_value,
-		_value - smtutil::Expression(bigint(1) << 256)
-	);
-}
-
-smtutil::Expression SMTSolver::signedToTwosComplement(smtutil::Expression _value)
-{
-	return smtutil::Expression::ite(
-		_value >= 0,
-		_value,
-		_value + smtutil::Expression(bigint(1) << 256)
-	);
-}
-
-smtutil::Expression SMTSolver::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;
-}
-
-void SMTSolver::encodeVariableDeclaration(VariableDeclaration const& _varDecl)
-{
-	if (
-		_varDecl.variables.size() == 1 &&
-		_varDecl.value &&
-		m_ssaVariables.count(_varDecl.variables.front().name)
-	)
-	{
-		YulString const& variableName = _varDecl.variables.front().name;
-		bool const inserted = m_variables.insert({
-			variableName,
-			m_solver->newVariable("yul_" + variableName.str(), defaultSort())
-		}).second;
-		yulAssert(inserted, "");
-		m_solver->addAssertion(
-			m_variables.at(variableName) == encodeExpression(*_varDecl.value)
-		);
-	}
-}

libyul/optimiser/SMTSolver.h

@@ -1,92 +0,0 @@
-/*
-	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/AST.h>
-#include <libyul/Dialect.h>
-#include <libyul/Exceptions.h>
-
-// because of instruction
-#include <libyul/backends/evm/EVMDialect.h>
-
-#include <libsmtutil/SolverInterface.h>
-
-#include <memory>
-
-namespace solidity::smtutil
-{
-
-class SolverInterface;
-class Expression;
-struct Sort;
-
-}
-
-namespace solidity::yul
-{
-
-/**
- * Base class for SMT based optimization steps.
- *
- * Works best when used with AST in SSA form.
- */
-class SMTSolver
-{
-protected:
-	SMTSolver(
-		std::set<YulString> const& _ssaVariables,
-		Dialect const& _dialect
-	);
-
-	/// Helper function that encodes VariableDeclaration
-	void encodeVariableDeclaration(VariableDeclaration const& _varDecl);
-
-	/// The encoding for a builtin. The type of encoding determines what we are
-	/// solving for.
-	virtual smtutil::Expression encodeEVMBuiltin(
-		evmasm::Instruction _instruction,
-		std::vector<Expression> const& _arguments
-	) = 0;
-
-	smtutil::Expression encodeExpression(Expression const& _expression);
-
-	static smtutil::Expression int2bv(smtutil::Expression _arg);
-	static smtutil::Expression bv2int(smtutil::Expression _arg);
-
-	smtutil::Expression newVariable();
-	virtual smtutil::Expression newRestrictedVariable(bigint _maxValue = (bigint(1) << 256) - 1);
-	std::string uniqueName();
-
-	virtual std::shared_ptr<smtutil::Sort> defaultSort() const;
-	static smtutil::Expression booleanValue(smtutil::Expression _value);
-	static smtutil::Expression constantValue(bigint _value);
-	static smtutil::Expression literalValue(Literal const& _literal);
-	static smtutil::Expression twosComplementToSigned(smtutil::Expression _value);
-	static smtutil::Expression signedToTwosComplement(smtutil::Expression _value);
-	smtutil::Expression wrap(smtutil::Expression _value);
-
-	std::set<YulString> const& m_ssaVariables;
-	std::unique_ptr<smtutil::SolverInterface> m_solver;
-	std::map<YulString, smtutil::Expression> m_variables;
-
-	Dialect const& m_dialect;
-
-private:
-	size_t m_varCounter = 0;
-};
-
-}

libyul/optimiser/Suite.cpp

@@ -43,7 +43,6 @@
 #include <libyul/optimiser/ForLoopInitRewriter.h>
 #include <libyul/optimiser/ForLoopConditionIntoBody.h>
 #include <libyul/optimiser/FunctionSpecializer.h>
-#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/optimiser/Rematerialiser.h>
 #include <libyul/optimiser/UnusedFunctionParameterPruner.h>
 #include <libyul/optimiser/UnusedPruner.h>
@@ -272,7 +271,6 @@ map<string, unique_ptr<OptimiserStep>> const& OptimiserSuite::allSteps()
 			LoopInvariantCodeMotion,
 			UnusedAssignEliminator,
 			UnusedStoreEliminator,
-			ReasoningBasedSimplifier,
 			Rematerialiser,
 			SSAReverser,
 			SSATransform,
@@ -312,7 +310,6 @@ map<string, char> const& OptimiserSuite::stepNameToAbbreviationMap()
 		{LiteralRematerialiser::name,         'T'},
 		{LoadResolver::name,                  'L'},
 		{LoopInvariantCodeMotion::name,       'M'},
-		{ReasoningBasedSimplifier::name,      'R'},
 		{UnusedAssignEliminator::name,        'r'},
 		{UnusedStoreEliminator::name,         'S'},
 		{Rematerialiser::name,                'm'},

test/libyul/YulOptimizerTest.cpp

@@ -24,7 +24,6 @@
 #include <test/Common.h>
 
 #include <libyul/Object.h>
-#include <libyul/optimiser/ReasoningBasedSimplifier.h>
 #include <libyul/AsmPrinter.h>
 
 #include <liblangutil/CharStreamProvider.h>
@@ -53,12 +52,6 @@ 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 ||
-		ReasoningBasedSimplifier::invalidInCurrentEnvironment()
-	))
-		m_shouldRun = false;
-
 	m_source = m_reader.source();
 
 	auto dialectName = m_reader.stringSetting("dialect", "evm");

test/libyul/YulOptimizerTestCommon.cpp

@@ -49,7 +49,6 @@
 #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>
@@ -289,10 +288,6 @@ YulOptimizerTestCommon::YulOptimizerTestCommon(
 			LiteralRematerialiser::run(*m_context, *m_ast);
 			StructuralSimplifier::run(*m_context, *m_ast);
 		}},
-		{"reasoningBasedSimplifier", [&]() {
-			disambiguate();
-			ReasoningBasedSimplifier::run(*m_context, *m_object->code);
-		}},
 		{"equivalentFunctionCombiner", [&]() {
 			disambiguate();
 			ForLoopInitRewriter::run(*m_context, *m_ast);
@@ -424,8 +419,7 @@ string YulOptimizerTestCommon::randomOptimiserStep(unsigned _seed)
 			// it can sometimes drain memory.
 			if (
 				optimiserStep == "mainFunction"	||
-				optimiserStep == "wordSizeTransform" ||
+				optimiserStep == "wordSizeTransform"
-				optimiserStep == "reasoningBasedSimplifier"
 			)
 				// "Fullsuite" is fuzzed roughly four times more frequently than
 				// other steps because of the filtering in place above.

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul

@@ -1,13 +0,0 @@
-{
-    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

@@ -1,19 +0,0 @@
-{
-	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

@@ -1,23 +0,0 @@
-{
-	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

@@ -1,32 +0,0 @@
-{
-    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

@@ -1,31 +0,0 @@
-{
-    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

@@ -1,16 +0,0 @@
-{
-    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

@@ -1,26 +0,0 @@
-{
-    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

@@ -1,31 +0,0 @@
-{
-    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

@@ -1,53 +0,0 @@
-{
-    // 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

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

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul

@@ -1,15 +0,0 @@
-{
-    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

@@ -37,7 +37,6 @@
 #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>
 

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) == "flcCUnDEvejsxIOoighFTLMRmVatrpuSd");
+	BOOST_TEST(toString(chromosome) == "flcCUnDEvejsxIOoighFTLMmVatrpuSd");
 }
 
 BOOST_AUTO_TEST_CASE(optimisationSteps_should_translate_chromosomes_genes_to_optimisation_step_names)