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

Add CallbackKind and use it for the SMT solver

Browse Source
This commit is contained in:
Leonardo Alt
2019-11-21 22:10:21 +00:00
committed by Alex Beregszaszi
parent 0201ff5a02
commit ddc478e3e4
24 changed files with 132 additions and 42 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+6 -2
View File
@@ -27,10 +27,14 @@ using namespace dev;
using namespace langutil;
using namespace dev::solidity;
BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
BMC::BMC(
smt::EncodingContext& _context,
ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback
):
SMTEncoder(_context),
m_outerErrorReporter(_errorReporter),
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses))
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses, _smtCallback))
{
#if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (!_smtlib2Responses.empty())
libsolidity/formal/BMC.h
+6 -1
View File
@@ -53,7 +53,12 @@ namespace solidity
class BMC: public SMTEncoder
{
public:
BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
BMC(
smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback
);
void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions);
libsolidity/formal/CHC.cpp
+4 -2
View File
@@ -35,17 +35,19 @@ using namespace dev::solidity;
CHC::CHC(
smt::EncodingContext& _context,
ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback
):
SMTEncoder(_context),
#ifdef HAVE_Z3
m_interface(make_shared<smt::Z3CHCInterface>()),
#else
m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses)),
m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback)),
#endif
m_outerErrorReporter(_errorReporter)
{
(void)_smtlib2Responses;
(void)_smtCallback;
}
void CHC::analyze(SourceUnit const& _source)
libsolidity/formal/CHC.h
+4 -1
View File
@@ -34,6 +34,8 @@
#include <libsolidity/formal/CHCSolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <set>
namespace dev
@@ -47,7 +49,8 @@ public:
CHC(
smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback
);
void analyze(SourceUnit const& _sources);
libsolidity/formal/CHCSmtLib2Interface.cpp
+13 -6
View File
@@ -34,9 +34,13 @@ using namespace dev;
using namespace dev::solidity;
using namespace dev::solidity::smt;
CHCSmtLib2Interface::CHCSmtLib2Interface(map<h256, string> const& _queryResponses):
m_smtlib2(make_shared<SMTLib2Interface>(_queryResponses)),
m_queryResponses(_queryResponses)
CHCSmtLib2Interface::CHCSmtLib2Interface(
map<h256, string> const& _queryResponses,
ReadCallback::Callback const& _smtCallback
):
m_smtlib2(make_shared<SMTLib2Interface>(_queryResponses, _smtCallback)),
m_queryResponses(_queryResponses),
m_smtCallback(_smtCallback)
{
reset();
}
@@ -152,9 +156,12 @@ string CHCSmtLib2Interface::querySolver(string const& _input)
h256 inputHash = dev::keccak256(_input);
if (m_queryResponses.count(inputHash))
return m_queryResponses.at(inputHash);
else
if (m_smtCallback)
{
m_unhandledQueries.push_back(_input);
return "unknown\n";
auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
if (result.success)
return result.responseOrErrorMessage;
}
m_unhandledQueries.push_back(_input);
return "unknown\n";
}
libsolidity/formal/CHCSmtLib2Interface.h
+6 -1
View File
@@ -35,7 +35,10 @@ namespace smt
class CHCSmtLib2Interface: public CHCSolverInterface
{
public:
explicit CHCSmtLib2Interface(std::map<h256, std::string> const& _queryResponses);
explicit CHCSmtLib2Interface(
std::map<h256, std::string> const& _queryResponses,
ReadCallback::Callback const& _smtCallback
);
void reset();
@@ -68,6 +71,8 @@ private:
std::map<h256, std::string> const& m_queryResponses;
std::vector<std::string> m_unhandledQueries;
ReadCallback::Callback m_smtCallback;
};
}
libsolidity/formal/ModelChecker.cpp
+7 -3
View File
@@ -22,9 +22,13 @@ using namespace dev;
using namespace langutil;
using namespace dev::solidity;
ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
m_bmc(m_context, _errorReporter, _smtlib2Responses),
m_chc(m_context, _errorReporter, _smtlib2Responses),
ModelChecker::ModelChecker(
ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback
):
m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback),
m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback),
m_context()
{
}
libsolidity/formal/ModelChecker.h
+5 -1
View File
@@ -43,7 +43,11 @@ namespace solidity
class ModelChecker
{
public:
ModelChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
ModelChecker(
langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback = ReadCallback::Callback()
);
void analyze(SourceUnit const& _sources);
libsolidity/formal/SMTLib2Interface.cpp
+12 -5
View File
@@ -34,8 +34,12 @@ using namespace dev;
using namespace dev::solidity;
using namespace dev::solidity::smt;
SMTLib2Interface::SMTLib2Interface(map<h256, string> const& _queryResponses):
m_queryResponses(_queryResponses)
SMTLib2Interface::SMTLib2Interface(
map<h256, string> const& _queryResponses,
ReadCallback::Callback const& _smtCallback
):
m_queryResponses(_queryResponses),
m_smtCallback(_smtCallback)
{
reset();
}
@@ -230,9 +234,12 @@ string SMTLib2Interface::querySolver(string const& _input)
h256 inputHash = dev::keccak256(_input);
if (m_queryResponses.count(inputHash))
return m_queryResponses.at(inputHash);
else
if (m_smtCallback)
{
m_unhandledQueries.push_back(_input);
return "unknown\n";
auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
if (result.success)
return result.responseOrErrorMessage;
}
m_unhandledQueries.push_back(_input);
return "unknown\n";
}
libsolidity/formal/SMTLib2Interface.h
+6 -1
View File
@@ -41,7 +41,10 @@ namespace smt
class SMTLib2Interface: public SolverInterface, public boost::noncopyable
{
public:
explicit SMTLib2Interface(std::map<h256, std::string> const& _queryResponses);
explicit SMTLib2Interface(
std::map<h256, std::string> const& _queryResponses,
ReadCallback::Callback const& _smtCallback
);
void reset() override;
@@ -78,6 +81,8 @@ private:
std::map<h256, std::string> const& m_queryResponses;
std::vector<std::string> m_unhandledQueries;
ReadCallback::Callback m_smtCallback;
};
}
libsolidity/formal/SMTPortfolio.cpp
+5 -2
View File
@@ -30,9 +30,12 @@ using namespace dev;
using namespace dev::solidity;
using namespace dev::solidity::smt;
SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
SMTPortfolio::SMTPortfolio(
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback
)
{
m_solvers.emplace_back(make_unique<smt::SMTLib2Interface>(_smtlib2Responses));
m_solvers.emplace_back(make_unique<smt::SMTLib2Interface>(_smtlib2Responses, _smtCallback));
#ifdef HAVE_Z3
m_solvers.emplace_back(make_unique<smt::Z3Interface>());
#endif
libsolidity/formal/SMTPortfolio.h
+4 -1
View File
@@ -42,7 +42,10 @@ namespace smt
class SMTPortfolio: public SolverInterface, public boost::noncopyable
{
public:
SMTPortfolio(std::map<h256, std::string> const& _smtlib2Responses);
SMTPortfolio(
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback
);
void reset() override;
libsolidity/interface/CompilerStack.cpp
+2 -2
View File
@@ -389,7 +389,7 @@ bool CompilerStack::analyze()
if (noErrors)
{
ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses);
ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_readFile);
for (Source const* source: m_sourceOrder)
modelChecker.analyze(*source->ast);
m_unhandledSMTLib2Queries += modelChecker.unhandledQueries();
@@ -886,7 +886,7 @@ StringMap CompilerStack::loadMissingSources(SourceUnit const& _ast, std::string
ReadCallback::Result result{false, string("File not supplied initially.")};
if (m_readFile)
result = m_readFile(importPath);
result = m_readFile(ReadCallback::kindString(ReadCallback::Kind::ReadFile), importPath);
if (result.success)
newSources[importPath] = result.responseOrErrorMessage;
libsolidity/interface/CompilerStack.h
+1 -1
View File
@@ -107,7 +107,7 @@ public:
};
/// Creates a new compiler stack.
/// @param _readFile callback to used to read files for import statements. Must return
/// @param _readFile callback used to read files for import statements. Must return
/// and must not emit exceptions.
explicit CompilerStack(ReadCallback::Callback const& _readFile = ReadCallback::Callback());
libsolidity/interface/ReadFile.h
+22 -1
View File
@@ -17,6 +17,8 @@
#pragma once
#include <liblangutil/Exceptions.h>
#include <boost/noncopyable.hpp>
#include <functional>
#include <string>
@@ -37,8 +39,27 @@ public:
std::string responseOrErrorMessage;
};
enum class Kind
{
ReadFile,
SMTQuery
};
static std::string kindString(Kind _kind)
{
switch (_kind)
{
case Kind::ReadFile:
return "source";
case Kind::SMTQuery:
return "smt-query";
default:
solAssert(false, "");
}
}
/// File reading or generic query callback.
using Callback = std::function<Result(std::string const&)>;
using Callback = std::function<Result(std::string const&, std::string const&)>;
};
}
libsolidity/interface/StandardCompiler.cpp
+1 -1
View File
@@ -555,7 +555,7 @@ boost::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompile
{
if (!url.isString())
return formatFatalError("JSONError", "URL must be a string.");
ReadCallback::Result result = m_readFile(url.asString());
ReadCallback::Result result = m_readFile(ReadCallback::kindString(ReadCallback::Kind::ReadFile), url.asString());
if (result.success)
{
if (!hash.empty() && !hashMatchesContent(hash, result.responseOrErrorMessage))
libsolidity/interface/StandardCompiler.h
+1 -1
View File
@@ -41,7 +41,7 @@ class StandardCompiler: boost::noncopyable
{
public:
/// Creates a new StandardCompiler.
/// @param _readFile callback to used to read files for import statements. Must return
/// @param _readFile callback used to read files for import statements. Must return
/// and must not emit exceptions.
explicit StandardCompiler(ReadCallback::Callback const& _readFile = ReadCallback::Callback()):
m_readFile(_readFile)