From b4dd0420ca09a7ccad49e72da93a0edaf59078a0 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 1 Mar 2022 23:49:03 +0100 Subject: [PATCH] encoding --- libsolutil/BooleanLP.cpp | 127 +++++++++++++----- libsolutil/BooleanLP.h | 10 +- libyul/optimiser/ReasoningBasedSimplifier.cpp | 32 ++++- libyul/optimiser/ReasoningBasedSimplifier.h | 3 + libyul/optimiser/SMTSolver.cpp | 8 ++ libyul/optimiser/SMTSolver.h | 1 + test/libyul/YulOptimizerTest.cpp | 3 +- 7 files changed, 141 insertions(+), 43 deletions(-) diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index 3f9d5ed94..efc731915 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -97,31 +97,53 @@ void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _s void BooleanLPSolver::addAssertion(Expression const& _expr) { + solAssert(_expr.sort->kind == Kind::Bool); if (_expr.arguments.empty()) - state().clauses.emplace_back(Clause{vector{*parseLiteral(_expr)}}); + { + solAssert(isBooleanVariable(_expr.name)); + state().clauses.emplace_back(Clause{Literal{ + true, + state().variables.at(_expr.name) + }}); + } else if (_expr.name == "=") { - // Try to see if both sides are linear. - optional left = parseLinearSum(_expr.arguments.at(0)); - optional right = parseLinearSum(_expr.arguments.at(1)); - if (left && right) + solAssert(_expr.arguments.at(0).sort->kind == _expr.arguments.at(1).sort->kind); + if (_expr.arguments.at(0).sort->kind == Kind::Bool) { - LinearExpression data = *left - *right; - data[0] *= -1; - Constraint c{move(data), _expr.name == "=", {}}; - if (!tryAddDirectBounds(c)) - state().fixedConstraints.emplace_back(move(c)); + if (_expr.arguments.at(0).arguments.empty() && isBooleanVariable(_expr.arguments.at(0).name)) + addBooleanEquality(*parseLiteral(_expr.arguments.at(0)), _expr.arguments.at(1)); + else if (_expr.arguments.at(1).arguments.empty() && isBooleanVariable(_expr.arguments.at(1).name)) + addBooleanEquality(*parseLiteral(_expr.arguments.at(1)), _expr.arguments.at(0)); + else + { + Literal newBoolean = *parseLiteral(declareInternalVariable(true)); + addBooleanEquality(newBoolean, _expr.arguments.at(0)); + addBooleanEquality(newBoolean, _expr.arguments.at(1)); + } + } + else if (_expr.arguments.at(0).sort->kind == Kind::Int) + { + // Try to see if both sides are linear. + optional left = parseLinearSum(_expr.arguments.at(0)); + optional right = parseLinearSum(_expr.arguments.at(1)); + if (left && right) + { + LinearExpression data = *left - *right; + data[0] *= -1; + Constraint c{move(data), _expr.name == "=", {}}; + if (!tryAddDirectBounds(c)) + state().fixedConstraints.emplace_back(move(c)); + } + else + { + Expression left = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(0)); + Expression right = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(1)); + addAssertion(left == right); + } } - else if (_expr.arguments.at(0).arguments.empty() && isBooleanVariable(_expr.arguments.at(0).name)) - addBooleanEquality(*parseLiteral(_expr.arguments.at(0)), _expr.arguments.at(1)); - else if (_expr.arguments.at(1).arguments.empty() && isBooleanVariable(_expr.arguments.at(1).name)) - addBooleanEquality(*parseLiteral(_expr.arguments.at(1)), _expr.arguments.at(0)); else - { - Literal newBoolean = *parseLiteral(declareInternalBoolean()); - addBooleanEquality(newBoolean, _expr.arguments.at(0)); - addBooleanEquality(newBoolean, _expr.arguments.at(1)); - } + solAssert(false); } else if (_expr.name == "and") { @@ -137,7 +159,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr) { // We cannot have more than one constraint per clause. // TODO Why? - right = *parseLiteral(declareInternalBoolean()); + right = *parseLiteral(declareInternalVariable(true)); addBooleanEquality(right, _expr.arguments.at(1)); } state().clauses.emplace_back(Clause{vector{left, right}}); @@ -152,18 +174,20 @@ void BooleanLPSolver::addAssertion(Expression const& _expr) { optional left = parseLinearSum(_expr.arguments.at(0)); optional right = parseLinearSum(_expr.arguments.at(1)); - if (!left || !right) + if (left && right) { - cout << "Unable to parse expression" << endl; - // TODO fail in some way - return; + LinearExpression data = *left - *right; + data[0] *= -1; + Constraint c{move(data), _expr.name == "=", {}}; + if (!tryAddDirectBounds(c)) + state().fixedConstraints.emplace_back(move(c)); + } + else + { + Expression left = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(0)); + Expression right = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(1)); + addAssertion(left <= right); } - - LinearExpression data = *left - *right; - data[0] *= -1; - Constraint c{move(data), _expr.name == "=", {}}; - if (!tryAddDirectBounds(c)) - state().fixedConstraints.emplace_back(move(c)); } else if (_expr.name == ">=") addAssertion(_expr.arguments.at(1) <= _expr.arguments.at(0)); @@ -275,11 +299,11 @@ string BooleanLPSolver::toString() const return result; } -Expression BooleanLPSolver::declareInternalBoolean() +Expression BooleanLPSolver::declareInternalVariable(bool _boolean) { string name = "$" + to_string(state().variables.size() + 1); - declareVariable(name, true); - return smtutil::Expression(name, {}, SortProvider::boolSort); + declareVariable(name, _boolean); + return smtutil::Expression(name, {}, _boolean ? SortProvider::boolSort : SortProvider::uintSort); } void BooleanLPSolver::declareVariable(string const& _name, bool _boolean) @@ -350,17 +374,42 @@ Literal BooleanLPSolver::negate(Literal const& _lit) Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr) { - // TODO hen can this fail? + solAssert(_expr.sort->kind == Kind::Bool); + // TODO when can this fail? if (optional literal = parseLiteral(_expr)) return *literal; else { - Literal newBoolean = *parseLiteral(declareInternalBoolean()); + Literal newBoolean = *parseLiteral(declareInternalVariable(true)); addBooleanEquality(newBoolean, _expr); return newBoolean; } } +Expression BooleanLPSolver::parseLinearSumOrReturnEqualVariable(Expression const& _expr) +{ + solAssert(_expr.sort->kind == Kind::Int); + if (_expr.name == "ite") + { + Literal condition = parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0)); + // TODO this adds too many variables + Expression conditionBoolean = declareInternalVariable(true); + addBooleanEquality(condition, conditionBoolean); + Expression trueValue = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(1)); + Expression falseValue = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(2)); + Expression result = declareInternalVariable(false); + addAssertion(conditionBoolean || (result == trueValue)); + addAssertion(!conditionBoolean || (result == falseValue)); + return result; + } + if (_expr.arguments.empty()) + return _expr; + solAssert(parseLinearSum(_expr)); + Expression result = declareInternalVariable(false); + addAssertion(result == _expr); + return result; +} + optional BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr) const { if (_expr.arguments.empty() || _expr.name == "*") @@ -374,7 +423,12 @@ optional BooleanLPSolver::parseLinearSum(smtutil::Expression c return _expr.name == "+" ? *left + *right : *left - *right; } else + { + // TOOD This should just resort to parseLinearSumOrReturn... + // and then use that variable + cout << "Invalid operator " << _expr.name << endl; return std::nullopt; + } } optional BooleanLPSolver::parseProduct(smtutil::Expression const& _expr) const @@ -477,6 +531,7 @@ size_t BooleanLPSolver::addConditionalConstraint(Constraint _constraint) void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expression const& _right) { + solAssert(_right.sort->kind == Kind::Bool); if (optional right = parseLiteral(_right)) { // includes: not, <=, <, >=, >, boolean variables. @@ -501,7 +556,7 @@ void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expressi { // We cannot have more than one constraint per clause. // TODO Why? - b = *parseLiteral(declareInternalBoolean()); + b = *parseLiteral(declareInternalVariable(true)); addBooleanEquality(b, _right.arguments.at(1)); } diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h index 46c0dfe34..6d1fc8b05 100644 --- a/libsolutil/BooleanLP.h +++ b/libsolutil/BooleanLP.h @@ -47,12 +47,14 @@ struct State }; /** - * Component that satisfies the SMT SolverInterface and uses an LP solver plus the DPLL + * Component that satisfies the SMT SolverInterface and uses an LP solver plus the CDCL * algorithm internally. * It uses a rational relaxation of the integer program and thus will not be able to answer * "satisfiable", but its answers are still correct. * - * TODO are integers always non-negative? + * Contrary to the usual SMT type system, it adds an implicit constraint for all variables + * and sub-expressions to be non-negative. + * TODO this does not apply to e.g. `x + y - something` * * Integers are unbounded. */ @@ -77,13 +79,15 @@ public: private: using rational = boost::rational; - smtutil::Expression declareInternalBoolean(); + smtutil::Expression declareInternalVariable(bool _boolean); void declareVariable(std::string const& _name, bool _boolean); + /// Parses an expression of sort bool and returns a literal. std::optional parseLiteral(smtutil::Expression const& _expr); Literal negate(Literal const& _lit); Literal parseLiteralOrReturnEqualBoolean(smtutil::Expression const& _expr); + smtutil::Expression parseLinearSumOrReturnEqualVariable(smtutil::Expression const& _expr); /// Parses the expression and expects a linear sum of variables. /// Returns a vector with the first element being the constant and the diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp index 94c7102bd..62e9a1bb2 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.cpp +++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp @@ -28,6 +28,8 @@ #include +#include + #include #include @@ -40,7 +42,10 @@ using namespace solidity::smtutil; void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _ast) { set ssaVars = SSAValueTracker::ssaVariables(_ast); - ReasoningBasedSimplifier{_context.dialect, ssaVars}(_ast); + ReasoningBasedSimplifier simpl{_context.dialect, ssaVars}; + // Hack to inject the boolean lp solver. + simpl.m_solver = make_unique(); + simpl(_ast); } std::optional ReasoningBasedSimplifier::invalidInCurrentEnvironment() @@ -120,12 +125,21 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin( switch (_instruction) { case evmasm::Instruction::ADD: - return wrap(arguments.at(0) + arguments.at(1)); + { + auto result = arguments.at(0) + arguments.at(1) - (bigint(1) << 256) * newZeroOneVariable(); + restrictToEVMWord(result); + return result; + } case evmasm::Instruction::MUL: return wrap(arguments.at(0) * arguments.at(1)); case evmasm::Instruction::SUB: - return wrap(arguments.at(0) - arguments.at(1)); + { + auto result = arguments.at(0) - arguments.at(1) + (bigint(1) << 256) * newZeroOneVariable(); + restrictToEVMWord(result); + return result; + } case evmasm::Instruction::DIV: + // TODO add assertion that result is <= input return smtutil::Expression::ite( arguments.at(1) == constantValue(0), constantValue(0), @@ -224,3 +238,15 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin( } return newRestrictedVariable(); } + +smtutil::Expression ReasoningBasedSimplifier::newZeroOneVariable() +{ + smtutil::Expression var = newVariable(); + m_solver->addAssertion(var == 0 || var == 1); + return var; +} + +void ReasoningBasedSimplifier::restrictToEVMWord(smtutil::Expression _value) +{ + m_solver->addAssertion(0 <= _value && _value < bigint(1) << 256); +} diff --git a/libyul/optimiser/ReasoningBasedSimplifier.h b/libyul/optimiser/ReasoningBasedSimplifier.h index c458a36d0..c08488dbd 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.h +++ b/libyul/optimiser/ReasoningBasedSimplifier.h @@ -69,6 +69,9 @@ private: std::vector const& _arguments ) override; + 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 c0c6bcb5e..2cd662063 100644 --- a/libyul/optimiser/SMTSolver.cpp +++ b/libyul/optimiser/SMTSolver.cpp @@ -81,6 +81,11 @@ smtutil::Expression SMTSolver::newVariable() return m_solver->newVariable(uniqueName(), defaultSort()); } +smtutil::Expression SMTSolver::newBooleanVariable() +{ + return m_solver->newVariable(uniqueName(), SortProvider::boolSort); +} + smtutil::Expression SMTSolver::newRestrictedVariable(bigint _maxValue) { smtutil::Expression var = newVariable(); @@ -100,6 +105,7 @@ shared_ptr SMTSolver::defaultSort() const smtutil::Expression SMTSolver::booleanValue(smtutil::Expression _value) { + // TODO should not use ite return smtutil::Expression::ite(_value, constantValue(1), constantValue(0)); } @@ -115,6 +121,7 @@ smtutil::Expression SMTSolver::literalValue(Literal const& _literal) smtutil::Expression SMTSolver::twosComplementToSigned(smtutil::Expression _value) { + // TODO will that work for LP? return smtutil::Expression::ite( _value < smtutil::Expression(bigint(1) << 255), _value, @@ -136,6 +143,7 @@ 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); + m_solver->addAssertion(0 <= rest && rest < bigint(1) << 256); return rest; } diff --git a/libyul/optimiser/SMTSolver.h b/libyul/optimiser/SMTSolver.h index d92a84c1d..dfc54687e 100644 --- a/libyul/optimiser/SMTSolver.h +++ b/libyul/optimiser/SMTSolver.h @@ -68,6 +68,7 @@ protected: static smtutil::Expression bv2int(smtutil::Expression _arg); smtutil::Expression newVariable(); + smtutil::Expression newBooleanVariable(); virtual smtutil::Expression newRestrictedVariable(bigint _maxValue = (bigint(1) << 256) - 1); std::string uniqueName(); diff --git a/test/libyul/YulOptimizerTest.cpp b/test/libyul/YulOptimizerTest.cpp index 6404fa7c6..01db4ca7c 100644 --- a/test/libyul/YulOptimizerTest.cpp +++ b/test/libyul/YulOptimizerTest.cpp @@ -53,12 +53,13 @@ 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");