mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Inject SMTLIB2 queries and responses via standard-json-io.
This commit is contained in:
parent
9217fbb58d
commit
bb10be789c
@ -6,6 +6,7 @@ Language Features:
|
|||||||
Compiler Features:
|
Compiler Features:
|
||||||
* Build System: LLL is not built anymore by default. Must configure it with CMake as `-DLLL=ON`.
|
* Build System: LLL is not built anymore by default. Must configure it with CMake as `-DLLL=ON`.
|
||||||
* Code generator: Do not perform redundant double cleanup on unsigned integers when loading from calldata.
|
* Code generator: Do not perform redundant double cleanup on unsigned integers when loading from calldata.
|
||||||
|
* SMTChecker: SMTLib2 queries and responses passed via standard JSON compiler interface.
|
||||||
* SMTChecker: Support ``msg``, ``tx`` and ``block`` member variables.
|
* SMTChecker: Support ``msg``, ``tx`` and ``block`` member variables.
|
||||||
* SMTChecker: Support ``gasleft()`` and ``blockhash()`` functions.
|
* SMTChecker: Support ``gasleft()`` and ``blockhash()`` functions.
|
||||||
* SMTChecker: Support internal bound function calls.
|
* SMTChecker: Support internal bound function calls.
|
||||||
|
@ -32,8 +32,8 @@ using namespace dev;
|
|||||||
using namespace langutil;
|
using namespace langutil;
|
||||||
using namespace dev::solidity;
|
using namespace dev::solidity;
|
||||||
|
|
||||||
SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
|
SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
|
||||||
m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)),
|
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
|
||||||
m_errorReporter(_errorReporter)
|
m_errorReporter(_errorReporter)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
@ -47,10 +47,15 @@ class VariableUsage;
|
|||||||
class SMTChecker: private ASTConstVisitor
|
class SMTChecker: private ASTConstVisitor
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
SMTChecker(langutil::ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
|
SMTChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
|
||||||
|
|
||||||
void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
|
void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
|
||||||
|
|
||||||
|
/// This is used if the SMT solver is not directly linked into this binary.
|
||||||
|
/// @returns a list of inputs to the SMT solver that were not part of the argument to
|
||||||
|
/// the constructor.
|
||||||
|
std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
|
||||||
|
|
||||||
private:
|
private:
|
||||||
// TODO: Check that we do not have concurrent reads and writes to a variable,
|
// TODO: Check that we do not have concurrent reads and writes to a variable,
|
||||||
// because the order of expression evaluation is undefined
|
// because the order of expression evaluation is undefined
|
||||||
|
@ -20,6 +20,8 @@
|
|||||||
#include <liblangutil/Exceptions.h>
|
#include <liblangutil/Exceptions.h>
|
||||||
#include <libsolidity/interface/ReadFile.h>
|
#include <libsolidity/interface/ReadFile.h>
|
||||||
|
|
||||||
|
#include <libdevcore/Keccak256.h>
|
||||||
|
|
||||||
#include <boost/algorithm/string/predicate.hpp>
|
#include <boost/algorithm/string/predicate.hpp>
|
||||||
#include <boost/algorithm/string/join.hpp>
|
#include <boost/algorithm/string/join.hpp>
|
||||||
#include <boost/filesystem/operations.hpp>
|
#include <boost/filesystem/operations.hpp>
|
||||||
@ -37,8 +39,8 @@ using namespace dev;
|
|||||||
using namespace dev::solidity;
|
using namespace dev::solidity;
|
||||||
using namespace dev::solidity::smt;
|
using namespace dev::solidity::smt;
|
||||||
|
|
||||||
SMTLib2Interface::SMTLib2Interface(ReadCallback::Callback const& _queryCallback):
|
SMTLib2Interface::SMTLib2Interface(map<h256, string> const& _smtlib2Responses):
|
||||||
m_queryCallback(_queryCallback)
|
m_smtlib2Responses(_smtlib2Responses)
|
||||||
{
|
{
|
||||||
reset();
|
reset();
|
||||||
}
|
}
|
||||||
@ -212,11 +214,12 @@ vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, stri
|
|||||||
|
|
||||||
string SMTLib2Interface::querySolver(string const& _input)
|
string SMTLib2Interface::querySolver(string const& _input)
|
||||||
{
|
{
|
||||||
if (!m_queryCallback)
|
h256 inputHash = dev::keccak256(_input);
|
||||||
BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available."));
|
if (m_smtlib2Responses.count(inputHash))
|
||||||
|
return m_smtlib2Responses.at(inputHash);
|
||||||
ReadCallback::Result queryResult = m_queryCallback(_input);
|
else
|
||||||
if (!queryResult.success)
|
{
|
||||||
BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage));
|
m_unhandledQueries.push_back(_input);
|
||||||
return queryResult.responseOrErrorMessage;
|
return "unknown\n";
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -22,6 +22,8 @@
|
|||||||
#include <liblangutil/Exceptions.h>
|
#include <liblangutil/Exceptions.h>
|
||||||
#include <libsolidity/interface/ReadFile.h>
|
#include <libsolidity/interface/ReadFile.h>
|
||||||
|
|
||||||
|
#include <libdevcore/FixedHash.h>
|
||||||
|
|
||||||
#include <libdevcore/Common.h>
|
#include <libdevcore/Common.h>
|
||||||
|
|
||||||
#include <boost/noncopyable.hpp>
|
#include <boost/noncopyable.hpp>
|
||||||
@ -42,7 +44,7 @@ namespace smt
|
|||||||
class SMTLib2Interface: public SolverInterface, public boost::noncopyable
|
class SMTLib2Interface: public SolverInterface, public boost::noncopyable
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
explicit SMTLib2Interface(ReadCallback::Callback const& _queryCallback);
|
explicit SMTLib2Interface(std::map<h256, std::string> const& _smtlib2Responses);
|
||||||
|
|
||||||
void reset() override;
|
void reset() override;
|
||||||
|
|
||||||
@ -54,6 +56,8 @@ public:
|
|||||||
void addAssertion(Expression const& _expr) override;
|
void addAssertion(Expression const& _expr) override;
|
||||||
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
|
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
|
||||||
|
|
||||||
|
std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; }
|
||||||
|
|
||||||
private:
|
private:
|
||||||
void declareFunction(std::string const&, Sort const&);
|
void declareFunction(std::string const&, Sort const&);
|
||||||
|
|
||||||
@ -69,9 +73,11 @@ private:
|
|||||||
/// Communicates with the solver via the callback. Throws SMTSolverError on error.
|
/// Communicates with the solver via the callback. Throws SMTSolverError on error.
|
||||||
std::string querySolver(std::string const& _input);
|
std::string querySolver(std::string const& _input);
|
||||||
|
|
||||||
ReadCallback::Callback m_queryCallback;
|
std::map<h256, std::string> const& m_smtlib2Responses;
|
||||||
std::vector<std::string> m_accumulatedOutput;
|
std::vector<std::string> m_accumulatedOutput;
|
||||||
std::set<std::string> m_variables;
|
std::set<std::string> m_variables;
|
||||||
|
|
||||||
|
std::vector<std::string> m_unhandledQueries;
|
||||||
};
|
};
|
||||||
|
|
||||||
}
|
}
|
||||||
|
@ -32,7 +32,7 @@ using namespace dev;
|
|||||||
using namespace dev::solidity;
|
using namespace dev::solidity;
|
||||||
using namespace dev::solidity::smt;
|
using namespace dev::solidity::smt;
|
||||||
|
|
||||||
SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback)
|
SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
|
||||||
{
|
{
|
||||||
#ifdef HAVE_Z3
|
#ifdef HAVE_Z3
|
||||||
m_solvers.emplace_back(make_shared<smt::Z3Interface>());
|
m_solvers.emplace_back(make_shared<smt::Z3Interface>());
|
||||||
@ -41,9 +41,9 @@ SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback)
|
|||||||
m_solvers.emplace_back(make_shared<smt::CVC4Interface>());
|
m_solvers.emplace_back(make_shared<smt::CVC4Interface>());
|
||||||
#endif
|
#endif
|
||||||
#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
|
#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
|
||||||
m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_readCallback)),
|
m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses)),
|
||||||
#endif
|
#endif
|
||||||
(void)_readCallback;
|
(void)_smtlib2Responses;
|
||||||
}
|
}
|
||||||
|
|
||||||
void SMTPortfolio::reset()
|
void SMTPortfolio::reset()
|
||||||
|
@ -22,8 +22,11 @@
|
|||||||
|
|
||||||
#include <libsolidity/interface/ReadFile.h>
|
#include <libsolidity/interface/ReadFile.h>
|
||||||
|
|
||||||
|
#include <libdevcore/FixedHash.h>
|
||||||
|
|
||||||
#include <boost/noncopyable.hpp>
|
#include <boost/noncopyable.hpp>
|
||||||
|
|
||||||
|
#include <map>
|
||||||
#include <vector>
|
#include <vector>
|
||||||
|
|
||||||
namespace dev
|
namespace dev
|
||||||
@ -42,7 +45,7 @@ namespace smt
|
|||||||
class SMTPortfolio: public SolverInterface, public boost::noncopyable
|
class SMTPortfolio: public SolverInterface, public boost::noncopyable
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
SMTPortfolio(ReadCallback::Callback const& _readCallback);
|
SMTPortfolio(std::map<h256, std::string> const& _smtlib2Responses);
|
||||||
|
|
||||||
void reset() override;
|
void reset() override;
|
||||||
|
|
||||||
@ -54,6 +57,7 @@ public:
|
|||||||
void addAssertion(Expression const& _expr) override;
|
void addAssertion(Expression const& _expr) override;
|
||||||
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
|
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
|
||||||
|
|
||||||
|
std::vector<std::string> unhandledQueries() override { return m_solvers.at(0)->unhandledQueries(); }
|
||||||
private:
|
private:
|
||||||
static bool solverAnswered(CheckResult result);
|
static bool solverAnswered(CheckResult result);
|
||||||
|
|
||||||
|
@ -284,6 +284,9 @@ public:
|
|||||||
virtual std::pair<CheckResult, std::vector<std::string>>
|
virtual std::pair<CheckResult, std::vector<std::string>>
|
||||||
check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
|
check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
|
||||||
|
|
||||||
|
/// @returns a list of queries that the system was not able to respond to.
|
||||||
|
virtual std::vector<std::string> unhandledQueries() { return {}; }
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
// SMT query timeout in milliseconds.
|
// SMT query timeout in milliseconds.
|
||||||
static int const queryTimeout = 10000;
|
static int const queryTimeout = 10000;
|
||||||
|
@ -107,6 +107,8 @@ void CompilerStack::reset(bool _keepSources)
|
|||||||
m_stackState = Empty;
|
m_stackState = Empty;
|
||||||
m_sources.clear();
|
m_sources.clear();
|
||||||
}
|
}
|
||||||
|
m_smtlib2Responses.clear();
|
||||||
|
m_unhandledSMTLib2Queries.clear();
|
||||||
m_libraries.clear();
|
m_libraries.clear();
|
||||||
m_evmVersion = EVMVersion();
|
m_evmVersion = EVMVersion();
|
||||||
m_optimize = false;
|
m_optimize = false;
|
||||||
@ -283,9 +285,10 @@ bool CompilerStack::analyze()
|
|||||||
|
|
||||||
if (noErrors)
|
if (noErrors)
|
||||||
{
|
{
|
||||||
SMTChecker smtChecker(m_errorReporter, m_smtQuery);
|
SMTChecker smtChecker(m_errorReporter, m_smtlib2Responses);
|
||||||
for (Source const* source: m_sourceOrder)
|
for (Source const* source: m_sourceOrder)
|
||||||
smtChecker.analyze(*source->ast, source->scanner);
|
smtChecker.analyze(*source->ast, source->scanner);
|
||||||
|
m_unhandledSMTLib2Queries += smtChecker.unhandledQueries();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
catch(FatalError const&)
|
catch(FatalError const&)
|
||||||
|
@ -153,6 +153,13 @@ public:
|
|||||||
/// @returns true if a source object by the name already existed and was replaced.
|
/// @returns true if a source object by the name already existed and was replaced.
|
||||||
bool addSource(std::string const& _name, std::string const& _content, bool _isLibrary = false);
|
bool addSource(std::string const& _name, std::string const& _content, bool _isLibrary = false);
|
||||||
|
|
||||||
|
/// Adds a response to an SMTLib2 query (identified by the hash of the query input).
|
||||||
|
void addSMTLib2Response(h256 const& _hash, std::string const& _response) { m_smtlib2Responses[_hash] = _response; }
|
||||||
|
|
||||||
|
/// @returns a list of unhandled queries to the SMT solver (has to be supplied in a second run
|
||||||
|
/// by calling @a addSMTLib2Response.
|
||||||
|
std::vector<std::string> const& unhandledSMTQueries() const { return m_unhandledSMTLib2Queries; }
|
||||||
|
|
||||||
/// Parses all source units that were added
|
/// Parses all source units that were added
|
||||||
/// @returns false on error.
|
/// @returns false on error.
|
||||||
bool parse();
|
bool parse();
|
||||||
@ -334,7 +341,6 @@ private:
|
|||||||
) const;
|
) const;
|
||||||
|
|
||||||
ReadCallback::Callback m_readFile;
|
ReadCallback::Callback m_readFile;
|
||||||
ReadCallback::Callback m_smtQuery;
|
|
||||||
bool m_optimize = false;
|
bool m_optimize = false;
|
||||||
unsigned m_optimizeRuns = 200;
|
unsigned m_optimizeRuns = 200;
|
||||||
EVMVersion m_evmVersion;
|
EVMVersion m_evmVersion;
|
||||||
@ -344,6 +350,8 @@ private:
|
|||||||
/// "context:prefix=target"
|
/// "context:prefix=target"
|
||||||
std::vector<Remapping> m_remappings;
|
std::vector<Remapping> m_remappings;
|
||||||
std::map<std::string const, Source> m_sources;
|
std::map<std::string const, Source> m_sources;
|
||||||
|
std::vector<std::string> m_unhandledSMTLib2Queries;
|
||||||
|
std::map<h256, std::string> m_smtlib2Responses;
|
||||||
std::shared_ptr<GlobalContext> m_globalContext;
|
std::shared_ptr<GlobalContext> m_globalContext;
|
||||||
std::vector<Source const*> m_sourceOrder;
|
std::vector<Source const*> m_sourceOrder;
|
||||||
/// This is updated during compilation.
|
/// This is updated during compilation.
|
||||||
|
@ -319,6 +319,27 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
|
|||||||
return formatFatalError("JSONError", "Invalid input source specified.");
|
return formatFatalError("JSONError", "Invalid input source specified.");
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Json::Value const& auxInputs = _input["auxiliaryInput"];
|
||||||
|
if (!!auxInputs)
|
||||||
|
{
|
||||||
|
Json::Value const& smtlib2Responses = auxInputs["smtlib2"];
|
||||||
|
if (!!smtlib2Responses)
|
||||||
|
for (auto const& hashString: smtlib2Responses.getMemberNames())
|
||||||
|
{
|
||||||
|
h256 hash;
|
||||||
|
try
|
||||||
|
{
|
||||||
|
hash = h256(hashString);
|
||||||
|
}
|
||||||
|
catch (dev::BadHexCharacter const&)
|
||||||
|
{
|
||||||
|
return formatFatalError("JSONError", "Invalid hex encoding of SMTLib2 auxiliary input.");
|
||||||
|
}
|
||||||
|
|
||||||
|
m_compilerStack.addSMTLib2Response(hash, smtlib2Responses[hashString].asString());
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
Json::Value const& settings = _input.get("settings", Json::Value());
|
Json::Value const& settings = _input.get("settings", Json::Value());
|
||||||
|
|
||||||
if (settings.isMember("evmVersion"))
|
if (settings.isMember("evmVersion"))
|
||||||
@ -518,6 +539,10 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
|
|||||||
if (errors.size() > 0)
|
if (errors.size() > 0)
|
||||||
output["errors"] = errors;
|
output["errors"] = errors;
|
||||||
|
|
||||||
|
if (!m_compilerStack.unhandledSMTQueries().empty())
|
||||||
|
for (string const& query: m_compilerStack.unhandledSMTQueries())
|
||||||
|
output["auxiliaryInputRequested"]["smtlib2"]["0x" + keccak256(query).hex()] = query;
|
||||||
|
|
||||||
output["sources"] = Json::objectValue;
|
output["sources"] = Json::objectValue;
|
||||||
unsigned sourceIndex = 0;
|
unsigned sourceIndex = 0;
|
||||||
for (string const& sourceName: analysisSuccess ? m_compilerStack.sourceNames() : vector<string>())
|
for (string const& sourceName: analysisSuccess ? m_compilerStack.sourceNames() : vector<string>())
|
||||||
|
Loading…
Reference in New Issue
Block a user