cerc-io/solidity
11
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

Do not show redundant unsupported errors in SMTChecker

Browse Source
This commit is contained in:
Leo Alt
2021-08-27 16:25:09 +02:00
parent 327571db88
commit 8e81df1bd3
11 changed files with 132 additions and 40 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+5 -10
View File
@@ -37,15 +37,14 @@ using namespace solidity::frontend;
BMC::BMC(
smt::EncodingContext& _context,
ErrorReporter& _errorReporter,
UniqueErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings, _charStreamProvider),
m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout)),
m_outerErrorReporter(_errorReporter)
SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout))
{
#if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (m_settings.solvers.cvc4 || m_settings.solvers.z3)
@@ -67,7 +66,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
m_errorReporter.warning(
7710_error,
SourceLocation(),
"BMC analysis was not possible since no SMT solver was found and enabled."
@@ -113,7 +112,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
m_errorReporter.warning(
8084_error,
SourceLocation(),
"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available."
@@ -124,10 +123,6 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
);
}
}
else
m_outerErrorReporter.append(m_errorReporter.errors());
m_errorReporter.clear();
}
bool BMC::shouldInlineFunctionCall(
libsolidity/formal/BMC.h
+2 -5
View File
@@ -36,7 +36,7 @@
#include <libsolidity/interface/ReadFile.h>
#include <libsmtutil/SolverInterface.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/UniqueErrorReporter.h>
#include <set>
#include <string>
@@ -59,7 +59,7 @@ class BMC: public SMTEncoder
public:
BMC(
smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter,
langutil::UniqueErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
@@ -186,9 +186,6 @@ private:
bool m_loopExecutionHappened = false;
bool m_externalFunctionCallHappened = false;
/// ErrorReporter that comes from CompilerStack.
langutil::ErrorReporter& m_outerErrorReporter;
std::vector<BMCVerificationTarget> m_verificationTargets;
/// Targets that were already proven.
libsolidity/formal/CHC.cpp
+4 -9
View File
@@ -53,14 +53,13 @@ using namespace solidity::frontend::smt;
CHC::CHC(
EncodingContext& _context,
ErrorReporter& _errorReporter,
UniqueErrorReporter& _errorReporter,
[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings, _charStreamProvider),
m_outerErrorReporter(_errorReporter)
SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider)
{
bool usesZ3 = m_settings.solvers.z3;
#ifdef HAVE_Z3
@@ -79,7 +78,7 @@ void CHC::analyze(SourceUnit const& _source)
if (!m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
m_errorReporter.warning(
7649_error,
SourceLocation(),
"CHC analysis was not possible since no Horn solver was enabled."
@@ -111,7 +110,7 @@ void CHC::analyze(SourceUnit const& _source)
if (!ranSolver && !m_noSolverWarning)
{
m_noSolverWarning = true;
m_outerErrorReporter.warning(
m_errorReporter.warning(
3996_error,
SourceLocation(),
#ifdef HAVE_Z3_DLOPEN
@@ -122,10 +121,6 @@ void CHC::analyze(SourceUnit const& _source)
#endif
);
}
else
m_outerErrorReporter.append(m_errorReporter.errors());
m_errorReporter.clear();
}
vector<string> CHC::unhandledQueries() const
libsolidity/formal/CHC.h
+2 -4
View File
@@ -40,6 +40,7 @@
#include <libsmtutil/CHCSolverInterface.h>
#include <liblangutil/SourceLocation.h>
#include <liblangutil/UniqueErrorReporter.h>
#include <boost/algorithm/string/join.hpp>
@@ -55,7 +56,7 @@ class CHC: public SMTEncoder
public:
CHC(
smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter,
langutil::UniqueErrorReporter& _errorReporter,
std::map<util::h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings const& _settings,
@@ -415,9 +416,6 @@ private:
/// CHC solver.
std::unique_ptr<smtutil::CHCSolverInterface> m_interface;
/// ErrorReporter that comes from CompilerStack.
langutil::ErrorReporter& m_outerErrorReporter;
};
}
libsolidity/formal/ModelChecker.cpp
+8 -5
View File
@@ -40,8 +40,8 @@ ModelChecker::ModelChecker(
m_errorReporter(_errorReporter),
m_settings(move(_settings)),
m_context(),
m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
m_bmc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
m_chc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
{
}
@@ -68,7 +68,7 @@ void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUni
{
if (!exist.count(sourceName))
{
m_errorReporter.warning(
m_uniqueErrorReporter.warning(
9134_error,
SourceLocation(),
"Requested source \"" + sourceName + "\" does not exist."
@@ -79,7 +79,7 @@ void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUni
// Requested contracts in source `s`.
for (auto const& contract: m_settings.contracts.contracts.at(sourceName))
if (!source.count(contract))
m_errorReporter.warning(
m_uniqueErrorReporter.warning(
7400_error,
SourceLocation(),
"Requested contract \"" + contract + "\" does not exist in source \"" + sourceName + "\"."
@@ -104,7 +104,7 @@ void ModelChecker::analyze(SourceUnit const& _source)
break;
}
solAssert(smtPragma, "");
m_errorReporter.warning(
m_uniqueErrorReporter.warning(
5523_error,
smtPragma->location(),
"The SMTChecker pragma has been deprecated and will be removed in the future. "
@@ -125,6 +125,9 @@ void ModelChecker::analyze(SourceUnit const& _source)
if (m_settings.engine.bmc)
m_bmc.analyze(_source, solvedTargets);
m_errorReporter.append(m_uniqueErrorReporter.errors());
m_uniqueErrorReporter.clear();
}
vector<string> ModelChecker::unhandledQueries()
libsolidity/formal/ModelChecker.h
+10
View File
@@ -31,7 +31,9 @@
#include <libsolidity/interface/ReadFile.h>
#include <libsmtutil/SolverInterface.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/UniqueErrorReporter.h>
namespace solidity::langutil
{
@@ -73,8 +75,16 @@ public:
static smtutil::SMTSolverChoice availableSolvers();
private:
/// Error reporter from CompilerStack.
/// We need to append m_uniqueErrorReporter
/// to this one when the analysis is done.
langutil::ErrorReporter& m_errorReporter;
/// Used by ModelChecker, SMTEncoder, BMC and CHC to avoid duplicates.
/// This is local to ModelChecker, so needs to be appended
/// to m_errorReporter at the end of the analysis.
langutil::UniqueErrorReporter m_uniqueErrorReporter;
ModelCheckerSettings m_settings;
/// Stores the context of the encoding.
libsolidity/formal/SMTEncoder.cpp
+2 -1
View File
@@ -46,9 +46,10 @@ using namespace solidity::frontend;
SMTEncoder::SMTEncoder(
smt::EncodingContext& _context,
ModelCheckerSettings const& _settings,
UniqueErrorReporter& _errorReporter,
langutil::CharStreamProvider const& _charStreamProvider
):
m_errorReporter(m_smtErrors),
m_errorReporter(_errorReporter),
m_context(_context),
m_settings(_settings),
m_charStreamProvider(_charStreamProvider)
libsolidity/formal/SMTEncoder.h
+3 -6
View File
@@ -32,7 +32,7 @@
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/ASTVisitor.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/UniqueErrorReporter.h>
#include <string>
#include <unordered_map>
@@ -55,6 +55,7 @@ public:
SMTEncoder(
smt::EncodingContext& _context,
ModelCheckerSettings const& _settings,
langutil::UniqueErrorReporter& _errorReporter,
langutil::CharStreamProvider const& _charStreamProvider
);
@@ -420,11 +421,7 @@ protected:
/// or unchecked arithmetic.
bool m_checked = true;
/// Local SMTEncoder ErrorReporter.
/// This is necessary to show the "No SMT solver available"
/// warning before the others in case it's needed.
langutil::ErrorReporter m_errorReporter;
langutil::ErrorList m_smtErrors;
langutil::UniqueErrorReporter& m_errorReporter;
/// Stores the current function/modifier call/invocation path.
std::vector<CallStackEntry> m_callStack;