diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp index 3ad4c8b01..3e186b7c2 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.cpp +++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp @@ -18,7 +18,6 @@ #include #include -#include #include #include #include @@ -41,8 +40,7 @@ using namespace solidity::smtutil; void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _ast) { - set ssaVars = SSAValueTracker::ssaVariables(_ast); - ReasoningBasedSimplifier simpl{_context.dialect, ssaVars}; + ReasoningBasedSimplifier simpl{_context.dialect}; // Hack to inject the boolean lp solver. simpl.m_solver = make_unique(); simpl(_ast); @@ -58,14 +56,120 @@ void ReasoningBasedSimplifier::operator()(VariableDeclaration& _varDecl) SMTSolver::encodeVariableDeclaration(_varDecl); } +void ReasoningBasedSimplifier::operator()(Assignment& _assignment) +{ + SMTSolver::encodeVariableAssignment(_assignment); +} + void ReasoningBasedSimplifier::operator()(If& _if) +{ + checkIfConditionRedundant(_if); + + decltype(m_variableSequenceCounter) oldCounters(m_variableSequenceCounter); + optional oldPathCondition = m_pathCondition; + + // TODO do not call encode again - assert it is a variable + smtutil::Expression ifCondition = encodeExpression(*_if.condition); + smtutil::Expression branchCondition = (ifCondition >= 1); + if (m_pathCondition) + m_pathCondition = *m_pathCondition && branchCondition; + else + m_pathCondition = branchCondition; + ASTModifier::operator()(_if.body); + + // join control flow + for (auto& var: oldCounters) + if (m_variableSequenceCounter.at(var.first) != var.second) + { + YulString const& name = var.first; + size_t oldCounter = var.second; + size_t branchCounter = m_variableSequenceCounter.at(name); + size_t newCounter = branchCounter + 1; + m_solver->newVariable(variableNameAtIndex(name, newCounter), defaultSort()); + + // TODO full path condition? + m_solver->addAssertion( + ifCondition == 0 || + variableExpressionAtIndex(name, newCounter) == variableExpressionAtIndex(name, branchCounter) + ); + m_solver->addAssertion( + ifCondition >= 1 || + variableExpressionAtIndex(name, newCounter) == variableExpressionAtIndex(name, oldCounter) + ); + var.second = newCounter; + } + + m_variableSequenceCounter = move(oldCounters); + m_pathCondition = move(oldPathCondition); +} + +void ReasoningBasedSimplifier::operator()(ForLoop& _for) +{ + // TODO handle break / continue + + decltype(m_variableSequenceCounter) oldCounters(m_variableSequenceCounter); + optional oldPathCondition = m_pathCondition; + + // TODO do not call encode again - assert it is a variable + smtutil::Expression forCondition = encodeExpression(*_for.condition); + smtutil::Expression branchCondition = (forCondition >= 1); + if (m_pathCondition) + m_pathCondition = *m_pathCondition && branchCondition; + else + m_pathCondition = branchCondition; + yulAssert(_for.pre.statements.empty()); + ASTModifier::operator()(_for.body); + // TODO clear modified variables! + ASTModifier::operator()(_for.post); + + // join control flow + for (auto& var: oldCounters) + if (m_variableSequenceCounter.at(var.first) != var.second) + { + var.second++; + m_solver->newVariable(variableNameAtIndex(var.first, var.second), defaultSort()); + restrictToEVMWord(currentVariableExpression(var.first)); + } + + m_variableSequenceCounter = move(oldCounters); + m_pathCondition = move(oldPathCondition); +} + +void ReasoningBasedSimplifier::operator()(FunctionCall& _fun) +{ + ASTModifier::operator()(_fun); + // TODO do not forget to add path condition! + // TODO and(x, 0xfff) -> x if x <= 0xfff + // TODO if _fun is not returning, assert that the path condition is aflse +} + +void ReasoningBasedSimplifier::operator()(FunctionDefinition& _fun) +{ + ScopedSaveAndRestore counters(m_variableSequenceCounter, {}); + ScopedSaveAndRestore pathCond(m_pathCondition, true); + ASTModifier::operator()(_fun); +} + +ReasoningBasedSimplifier::ReasoningBasedSimplifier( + Dialect const& _dialect +): + SMTSolver(_dialect) +{ +} + +void ReasoningBasedSimplifier::checkIfConditionRedundant(If& _if) { if (!SideEffectsCollector{m_dialect, *_if.condition}.movable()) return; cout << "Checking if condition can be false" << endl; + // TODO should not call encode, but instead check if it is + // a variable and use its name / value smtutil::Expression condition = encodeExpression(*_if.condition); m_solver->push(); + // TODO find a way so that we do not have to do that all the time. + if (m_pathCondition) + m_solver->addAssertion(*m_pathCondition); m_solver->addAssertion(condition == constantValue(0)); cout << " running check" << endl; CheckResult result = m_solver->check({}).first; @@ -81,7 +185,9 @@ void ReasoningBasedSimplifier::operator()(If& _if) { cout << "Checking if condition can be true" << endl; m_solver->push(); - // TODO change this to >= 1 for simplicity? + // TODO find a way so that we do not have to do that all the time. + if (m_pathCondition) + m_solver->addAssertion(*m_pathCondition); m_solver->addAssertion(condition >= 1); cout << " running check" << endl; CheckResult result2 = m_solver->check({}).first; @@ -93,83 +199,9 @@ void ReasoningBasedSimplifier::operator()(If& _if) falseCondition.debugData = debugDataOf(*_if.condition); _if.condition = make_unique(move(falseCondition)); _if.body = yul::Block{}; - // Nothing left to be done. - return; } cout << " unknown :(" << endl; } - - m_solver->push(); - cout << "Setting condition true inside body" << endl; - m_solver->addAssertion(condition >= constantValue(1)); - - ASTModifier::operator()(_if.body); - - m_solver->pop(); - - // TODO if the body is non-continuing, we could assert that the condition is false - // but this might not be true anymore once we join with another control-flow. - // maybe it is best to let the conditional simplifier and the data flow analyzer do this for us. -} - -void ReasoningBasedSimplifier::operator()(ForLoop& _for) -{ - // TODO handle break / continue - - if (!SideEffectsCollector{m_dialect, *_for.condition}.movable()) - return; - - cout << "Checking if condition can be false" << endl; - smtutil::Expression condition = encodeExpression(*_for.condition); - m_solver->push(); - m_solver->addAssertion(condition <= constantValue(0)); - cout << " running check" << endl; - CheckResult result = m_solver->check({}).first; - m_solver->pop(); - if (result == CheckResult::UNSATISFIABLE) - { - cout << " unsat => cannot be false!" << endl; - Literal trueCondition = m_dialect.trueLiteral(); - trueCondition.debugData = debugDataOf(*_for.condition); - _for.condition = make_unique(move(trueCondition)); - } - else - { - cout << "Checking if condition can be true" << endl; - m_solver->push(); - m_solver->addAssertion(condition >= constantValue(1)); - cout << " running check" << endl; - CheckResult result2 = m_solver->check({}).first; - m_solver->pop(); - if (result2 == CheckResult::UNSATISFIABLE) - { - cout << " unsat => cannot be true!" << endl; - Literal falseCondition = m_dialect.zeroLiteralForType(m_dialect.boolType); - falseCondition.debugData = debugDataOf(*_for.condition); - _for.condition = make_unique(move(falseCondition)); - _for.body = yul::Block{}; - // Nothing left to be done. - return; - } - } - - m_solver->push(); - cout << "Setting condition true inside body" << endl; - m_solver->addAssertion(condition >= constantValue(1)); - - ASTModifier::operator()(_for.body); - ASTModifier::operator()(_for.post); - - m_solver->pop(); -} - -ReasoningBasedSimplifier::ReasoningBasedSimplifier( - Dialect const& _dialect, - set const& _ssaVariables -): - SMTSolver(_ssaVariables, _dialect), - m_dialect(_dialect) -{ } diff --git a/libyul/optimiser/ReasoningBasedSimplifier.h b/libyul/optimiser/ReasoningBasedSimplifier.h index c645483e8..f28be17c0 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.h +++ b/libyul/optimiser/ReasoningBasedSimplifier.h @@ -58,14 +58,16 @@ public: using ASTModifier::operator(); void operator()(VariableDeclaration& _varDecl) override; + void operator()(Assignment& _assignment) override; void operator()(If& _if) override; void operator()(ForLoop& _for) override; + void operator()(FunctionCall& _fun) override; + void operator()(FunctionDefinition& _fun) override; private: - explicit ReasoningBasedSimplifier( - Dialect const& _dialect, - std::set const& _ssaVariables - ); + explicit ReasoningBasedSimplifier(Dialect const& _dialect); + + void checkIfConditionRedundant(If& _if); smtutil::Expression encodeEVMBuiltin( evmasm::Instruction _instruction, @@ -74,8 +76,6 @@ private: smtutil::Expression newZeroOneVariable(); void restrictToEVMWord(smtutil::Expression _value); - - Dialect const& m_dialect; }; } diff --git a/libyul/optimiser/SMTSolver.cpp b/libyul/optimiser/SMTSolver.cpp index 033597a13..9c8ffacb5 100644 --- a/libyul/optimiser/SMTSolver.cpp +++ b/libyul/optimiser/SMTSolver.cpp @@ -33,8 +33,7 @@ using namespace solidity::smtutil; using namespace solidity; using namespace std; -SMTSolver::SMTSolver(set const& _ssaVariables, Dialect const& _dialect): - m_ssaVariables(_ssaVariables), +SMTSolver::SMTSolver(Dialect const& _dialect): m_solver(make_unique()), m_dialect(_dialect) { } @@ -51,13 +50,7 @@ smtutil::Expression SMTSolver::encodeExpression(Expression const& _expression) }, [&](Identifier const& _identifier) { - if ( - m_ssaVariables.count(_identifier.name) && - m_variables.count(_identifier.name) - ) - return m_variables.at(_identifier.name); - else - return newRestrictedVariable(); + return currentVariableExpression(_identifier.name); }, [&](Literal const& _literal) { @@ -76,6 +69,21 @@ smtutil::Expression SMTSolver::bv2int(smtutil::Expression _arg) return smtutil::Expression::bv2int(std::move(_arg)); } +string SMTSolver::variableNameAtIndex(YulString const& _name, size_t _index) const +{ + return "yul_" + to_string(_index) + "_"s + _name.str(); +} + +smtutil::Expression SMTSolver::variableExpressionAtIndex(YulString const& _name, size_t _index) const +{ + return smtutil::Expression(variableNameAtIndex(_name, _index), {}, defaultSort()); +} + +smtutil::Expression SMTSolver::currentVariableExpression(YulString const& _name) const +{ + return variableExpressionAtIndex(_name, m_variableSequenceCounter.at(_name)); +} + smtutil::Expression SMTSolver::newVariable() { return m_solver->newVariable(uniqueName(), defaultSort()); @@ -149,18 +157,25 @@ void SMTSolver::encodeVariableDeclaration(VariableDeclaration const& _varDecl) { if ( _varDecl.variables.size() == 1 && - _varDecl.value && - m_ssaVariables.count(_varDecl.variables.front().name) + _varDecl.value ) - { - 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) - ); - } + encodeVariableUpdate(_varDecl.variables.front().name, *_varDecl.value); +} + +void SMTSolver::encodeVariableAssignment(Assignment const& _assignment) +{ + if (_assignment.variableNames.size() == 1) + encodeVariableUpdate(_assignment.variableNames.front().name, *_assignment.value); +} + +void SMTSolver::encodeVariableUpdate(YulString const& _name, Expression const& _value) +{ + smtutil::Expression value = encodeExpression(_value); + if (m_variableSequenceCounter.count(_name)) + ++m_variableSequenceCounter[_name]; + else + m_variableSequenceCounter[_name] = 1; + + m_solver->newVariable(variableNameAtIndex(_name, m_variableSequenceCounter[_name]), defaultSort()); + m_solver->addAssertion(currentVariableExpression(_name) == value); } diff --git a/libyul/optimiser/SMTSolver.h b/libyul/optimiser/SMTSolver.h index 3541a74d7..bb37a1023 100644 --- a/libyul/optimiser/SMTSolver.h +++ b/libyul/optimiser/SMTSolver.h @@ -47,13 +47,12 @@ namespace solidity::yul class SMTSolver { protected: - SMTSolver( - std::set const& _ssaVariables, - Dialect const& _dialect - ); + SMTSolver(Dialect const& _dialect); /// Helper function that encodes VariableDeclaration void encodeVariableDeclaration(VariableDeclaration const& _varDecl); + void encodeVariableAssignment(Assignment const& _assignment); + void encodeVariableUpdate(YulString const& _name, Expression const& _value); /// The encoding for a builtin. The type of encoding determines what we are /// solving for. @@ -67,6 +66,10 @@ protected: static smtutil::Expression int2bv(smtutil::Expression _arg); static smtutil::Expression bv2int(smtutil::Expression _arg); + std::string variableNameAtIndex(YulString const& _name, size_t _index) const; + smtutil::Expression variableExpressionAtIndex(YulString const& _name, size_t _index) const; + smtutil::Expression currentVariableExpression(YulString const& _name) const; + smtutil::Expression newVariable(); smtutil::Expression newBooleanVariable(); virtual smtutil::Expression newRestrictedVariable(bigint _maxValue = (bigint(1) << 256) - 1); @@ -81,9 +84,9 @@ protected: static smtutil::Expression signedToTwosComplement(smtutil::Expression _value); smtutil::Expression wrap(smtutil::Expression _value); - std::set const& m_ssaVariables; std::unique_ptr m_solver; - std::map m_variables; + std::map m_variableSequenceCounter; + std::optional m_pathCondition; Dialect const& m_dialect; diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul index 6e4b3f5ed..2680fc684 100644 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul @@ -11,6 +11,6 @@ // { // let x := sub(0, 7) // let y := 2 -// if 1 { } -// if 0 { } +// if iszero(add(sdiv(x, y), 3)) { } +// if iszero(add(sdiv(x, y), 4)) { } // }