cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Removing SMT portfolio

Browse Source
This commit is contained in:
Martin Blicha 2023-06-26 10:31:02 +02:00
parent 1e190abf6e
commit cabec89872
8 changed files with 17 additions and 241 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -43,7 +43,7 @@ CHCSmtLib2Interface::CHCSmtLib2Interface(
std::optional<unsigned> _queryTimeout
):
CHCSolverInterface(_queryTimeout),
m_smtlib2(std::make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),
m_smtlib2(std::make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, _enabledSolvers, m_queryTimeout)),
m_queryResponses(std::move(_queryResponses)),
m_smtCallback(_smtCallback),
m_enabledSolvers(_enabledSolvers)

2
libsmtutil/CMakeLists.txt
View File

@ -4,8 +4,6 @@ set(sources
Exceptions.h
SMTLib2Interface.cpp
SMTLib2Interface.h
SMTPortfolio.cpp
SMTPortfolio.h
SolverInterface.h
Sorts.cpp
Sorts.h

8
libsmtutil/SMTLib2Interface.cpp
View File

@ -41,11 +41,15 @@ using namespace solidity::smtutil;
SMTLib2Interface::SMTLib2Interface(
std::map<h256, std::string> _queryResponses,
ReadCallback::Callback _smtCallback,
std::optional<unsigned> _queryTimeout
SMTSolverChoice _enabledSolvers,
std::optional<unsigned> _queryTimeout,
bool _dumpQuery
):
SolverInterface(_queryTimeout),
m_queryResponses(std::move(_queryResponses)),
m_smtCallback(std::move(_smtCallback))
m_smtCallback(std::move(_smtCallback)),
m_enabledSolvers(_enabledSolvers),
m_dumpQuery(_dumpQuery)
{
reset();
}

6
libsmtutil/SMTLib2Interface.h
View File

@ -44,7 +44,9 @@ public:
explicit SMTLib2Interface(
std::map<util::h256, std::string> _queryResponses = {},
frontend::ReadCallback::Callback _smtCallback = {},
std::optional<unsigned> _queryTimeout = {}
SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(),
std::optional<unsigned> _queryTimeout = {},
bool _printQuery = false
);
void reset() override;
@ -94,6 +96,8 @@ private:
std::vector<std::string> m_unhandledQueries;
frontend::ReadCallback::Callback m_smtCallback;
SMTSolverChoice m_enabledSolvers;
bool m_dumpQuery;
};
}

153
libsmtutil/SMTPortfolio.cpp
View File

@ -1,153 +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/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsmtutil/SMTPortfolio.h>
#include <libsmtutil/SMTLib2Interface.h>
using namespace solidity;
using namespace solidity::util;
using namespace solidity::frontend;
using namespace solidity::smtutil;
SMTPortfolio::SMTPortfolio(
std::map<h256, std::string> _smtlib2Responses,
frontend::ReadCallback::Callback _smtCallback,
[[maybe_unused]] SMTSolverChoice _enabledSolvers,
std::optional<unsigned> _queryTimeout,
bool _printQuery
):
SolverInterface(_queryTimeout)
{
solAssert(!_printQuery || _enabledSolvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");
if (_enabledSolvers.smtlib2)
m_solvers.emplace_back(std::make_unique<SMTLib2Interface>(std::move(_smtlib2Responses), std::move(_smtCallback), m_queryTimeout));
}
void SMTPortfolio::reset()
{
for (auto const& s: m_solvers)
s->reset();
}
void SMTPortfolio::push()
{
for (auto const& s: m_solvers)
s->push();
}
void SMTPortfolio::pop()
{
for (auto const& s: m_solvers)
s->pop();
}
void SMTPortfolio::declareVariable(std::string const& _name, SortPointer const& _sort)
{
smtAssert(_sort, "");
for (auto const& s: m_solvers)
s->declareVariable(_name, _sort);
}
void SMTPortfolio::addAssertion(Expression const& _expr)
{
for (auto const& s: m_solvers)
s->addAssertion(_expr);
}
/*
* Broadcasts the SMT query to all solvers and returns a single result.
* This comment explains how this result is decided.
*
* When a solver is queried, there are four possible answers:
* SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, CONFLICTING, ERROR
* We say that a solver _answered_ the query if it returns either:
* SAT or UNSAT
* A solver did not answer the query if it returns either:
* UNKNOWN (it tried but couldn't solve it) or ERROR (crash, internal error, API error, etc).
*
* Ideally all solvers answer the query and agree on what the answer is
* (all say SAT or all say UNSAT).
*
* The actual logic as as follows:
* 1) If at least one solver answers the query, all the non-answer results are ignored.
* Here SAT/UNSAT is preferred over UNKNOWN since it's an actual answer, and over ERROR
* because one buggy solver/integration shouldn't break the portfolio.
*
* 2) If at least one solver answers SAT and at least one answers UNSAT, at least one of them is buggy
* and the result is CONFLICTING.
* In the future if we have more than 2 solvers enabled we could go with the majority.
*
* 3) If NO solver answers the query:
* If at least one solver returned UNKNOWN (where the rest returned ERROR), the result is UNKNOWN.
* This is preferred over ERROR since the SMTChecker might decide to abstract the query
* when it is told that this is a hard query to solve.
*
* If all solvers return ERROR, the result is ERROR.
*/
std::pair<CheckResult, std::vector<std::string>> SMTPortfolio::check(std::vector<Expression> const& _expressionsToEvaluate)
{
CheckResult lastResult = CheckResult::ERROR;
std::vector<std::string> finalValues;
for (auto const& s: m_solvers)
{
CheckResult result;
std::vector<std::string> values;
tie(result, values) = s->check(_expressionsToEvaluate);
if (solverAnswered(result))
{
if (!solverAnswered(lastResult))
{
lastResult = result;
finalValues = std::move(values);
}
else if (lastResult != result)
{
lastResult = CheckResult::CONFLICTING;
break;
}
}
else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR)
lastResult = result;
}
return std::make_pair(lastResult, finalValues);
}
std::vector<std::string> SMTPortfolio::unhandledQueries()
{
// This code assumes that the constructor guarantees that
// SmtLib2Interface is in position 0, if enabled.
if (!m_solvers.empty())
if (auto smtlib2 = dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()))
return smtlib2->unhandledQueries();
return {};
}
bool SMTPortfolio::solverAnswered(CheckResult result)
{
return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE;
}
std::string SMTPortfolio::dumpQuery(std::vector<Expression> const& _expressionsToEvaluate)
{
// This code assumes that the constructor guarantees that
// SmtLib2Interface is in position 0, if enabled.
auto smtlib2 = dynamic_cast<SMTLib2Interface*>(m_solvers.front().get());
solAssert(smtlib2, "Must use SMTLib2 solver to dump queries");
return smtlib2->dumpQuery(_expressionsToEvaluate);
}

77
libsmtutil/SMTPortfolio.h
View File

@ -1,77 +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/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
#include <libsmtutil/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <libsolutil/FixedHash.h>
#include <map>
#include <vector>
namespace solidity::smtutil
{
/**
* The SMTPortfolio wraps all available solvers within a single interface,
* propagating the functionalities to all solvers.
* It also checks whether different solvers give conflicting answers
* to SMT queries.
*/
class SMTPortfolio: public SolverInterface
{
public:
/// Noncopyable.
SMTPortfolio(SMTPortfolio const&) = delete;
SMTPortfolio& operator=(SMTPortfolio const&) = delete;
SMTPortfolio(
std::map<util::h256, std::string> _smtlib2Responses = {},
frontend::ReadCallback::Callback _smtCallback = {},
SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(),
std::optional<unsigned> _queryTimeout = {},
bool _printQuery = false
);
void reset() override;
void push() override;
void pop() override;
void declareVariable(std::string const&, SortPointer const&) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override;
size_t solvers() override { return m_solvers.size(); }
std::string dumpQuery(std::vector<Expression> const& _expressionsToEvaluate);
private:
static bool solverAnswered(CheckResult result);
std::vector<std::unique_ptr<SolverInterface>> m_solvers;
std::vector<Expression> m_assertions;
};
}

9
libsolidity/formal/BMC.cpp
View File

@ -20,7 +20,7 @@
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsmtutil/SMTPortfolio.h>
#include <libsmtutil/SMTLib2Interface.h>
#include <liblangutil/CharStream.h>
#include <liblangutil/CharStreamProvider.h>
@ -43,7 +43,7 @@ BMC::BMC(
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider),
m_interface(std::make_unique<smtutil::SMTPortfolio>(
m_interface(std::make_unique<smtutil::SMTLib2Interface>(
_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout, _settings.printQuery
))
{
@ -1219,8 +1219,9 @@ BMC::checkSatisfiableAndGenerateModel(std::vector<smtutil::Expression> const& _e
{
if (m_settings.printQuery)
{
auto portfolio = dynamic_cast<smtutil::SMTPortfolio*>(m_interface.get());
std::string smtlibCode = portfolio->dumpQuery(_expressionsToEvaluate);
auto smtlibInterface = dynamic_cast<smtutil::SMTLib2Interface*>(m_interface.get());
solAssert(smtlibInterface, "Must use SMTLib2 solver to dump queries");
std::string smtlibCode = smtlibInterface->dumpQuery(_expressionsToEvaluate);
m_errorReporter.info(
6240_error,
"BMC: Requested query:\n" + smtlibCode

1
libsolidity/formal/SMTEncoder.cpp
View File

@ -27,7 +27,6 @@
#include <libyul/AST.h>
#include <libyul/optimiser/Semantics.h>
#include <libsmtutil/SMTPortfolio.h>
#include <libsmtutil/Helpers.h>
#include <liblangutil/CharStreamProvider.h>