aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Changelog.md1
-rw-r--r--libsolidity/formal/SMTChecker.cpp4
-rw-r--r--libsolidity/formal/SMTChecker.h7
-rw-r--r--libsolidity/formal/SMTLib2Interface.cpp21
-rw-r--r--libsolidity/formal/SMTLib2Interface.h10
-rw-r--r--libsolidity/formal/SMTPortfolio.cpp6
-rw-r--r--libsolidity/formal/SMTPortfolio.h6
-rw-r--r--libsolidity/formal/SolverInterface.h3
-rw-r--r--libsolidity/interface/CompilerStack.cpp5
-rw-r--r--libsolidity/interface/CompilerStack.h10
-rw-r--r--libsolidity/interface/StandardCompiler.cpp25
11 files changed, 78 insertions, 20 deletions
diff --git a/Changelog.md b/Changelog.md
index 449798a4..ca904ffc 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -6,6 +6,7 @@ Language Features:
Compiler Features:
* 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.
+ * SMTChecker: SMTLib2 queries and responses passed via standard JSON compiler interface.
* SMTChecker: Support ``msg``, ``tx`` and ``block`` member variables.
* SMTChecker: Support ``gasleft()`` and ``blockhash()`` functions.
* SMTChecker: Support internal bound function calls.
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index bb9b498f..0af171a7 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -32,8 +32,8 @@ using namespace dev;
using namespace langutil;
using namespace dev::solidity;
-SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
- m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)),
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
+ m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
m_errorReporter(_errorReporter)
{
}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 5f51beb7..34724848 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -47,10 +47,15 @@ class VariableUsage;
class SMTChecker: private ASTConstVisitor
{
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);
+ /// 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:
// TODO: Check that we do not have concurrent reads and writes to a variable,
// because the order of expression evaluation is undefined
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 55c72cfc..80ecc715 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -20,6 +20,8 @@
#include <liblangutil/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
+#include <libdevcore/Keccak256.h>
+
#include <boost/algorithm/string/predicate.hpp>
#include <boost/algorithm/string/join.hpp>
#include <boost/filesystem/operations.hpp>
@@ -37,8 +39,8 @@ using namespace dev;
using namespace dev::solidity;
using namespace dev::solidity::smt;
-SMTLib2Interface::SMTLib2Interface(ReadCallback::Callback const& _queryCallback):
- m_queryCallback(_queryCallback)
+SMTLib2Interface::SMTLib2Interface(map<h256, string> const& _smtlib2Responses):
+ m_smtlib2Responses(_smtlib2Responses)
{
reset();
}
@@ -212,11 +214,12 @@ vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, stri
string SMTLib2Interface::querySolver(string const& _input)
{
- if (!m_queryCallback)
- BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available."));
-
- ReadCallback::Result queryResult = m_queryCallback(_input);
- if (!queryResult.success)
- BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage));
- return queryResult.responseOrErrorMessage;
+ h256 inputHash = dev::keccak256(_input);
+ if (m_smtlib2Responses.count(inputHash))
+ return m_smtlib2Responses.at(inputHash);
+ else
+ {
+ m_unhandledQueries.push_back(_input);
+ return "unknown\n";
+ }
}
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 4f72d27c..c67101ae 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -22,6 +22,8 @@
#include <liblangutil/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
+#include <libdevcore/FixedHash.h>
+
#include <libdevcore/Common.h>
#include <boost/noncopyable.hpp>
@@ -42,7 +44,7 @@ namespace smt
class SMTLib2Interface: public SolverInterface, public boost::noncopyable
{
public:
- explicit SMTLib2Interface(ReadCallback::Callback const& _queryCallback);
+ explicit SMTLib2Interface(std::map<h256, std::string> const& _smtlib2Responses);
void reset() override;
@@ -54,6 +56,8 @@ public:
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 { return m_unhandledQueries; }
+
private:
void declareFunction(std::string const&, Sort const&);
@@ -69,9 +73,11 @@ private:
/// Communicates with the solver via the callback. Throws SMTSolverError on error.
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::set<std::string> m_variables;
+
+ std::vector<std::string> m_unhandledQueries;
};
}
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
index 224e5cd6..4c591380 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -32,7 +32,7 @@ using namespace dev;
using namespace dev::solidity;
using namespace dev::solidity::smt;
-SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback)
+SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
{
#ifdef HAVE_Z3
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>());
#endif
#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
- (void)_readCallback;
+ (void)_smtlib2Responses;
}
void SMTPortfolio::reset()
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h
index 12e2be66..7f5ba37e 100644
--- a/libsolidity/formal/SMTPortfolio.h
+++ b/libsolidity/formal/SMTPortfolio.h
@@ -22,8 +22,11 @@
#include <libsolidity/interface/ReadFile.h>
+#include <libdevcore/FixedHash.h>
+
#include <boost/noncopyable.hpp>
+#include <map>
#include <vector>
namespace dev
@@ -42,7 +45,7 @@ namespace smt
class SMTPortfolio: public SolverInterface, public boost::noncopyable
{
public:
- SMTPortfolio(ReadCallback::Callback const& _readCallback);
+ SMTPortfolio(std::map<h256, std::string> const& _smtlib2Responses);
void reset() override;
@@ -54,6 +57,7 @@ public:
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 { return m_solvers.at(0)->unhandledQueries(); }
private:
static bool solverAnswered(CheckResult result);
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index fd1abd61..cc8214de 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -284,6 +284,9 @@ public:
virtual std::pair<CheckResult, std::vector<std::string>>
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:
// SMT query timeout in milliseconds.
static int const queryTimeout = 10000;
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index a5674705..ae85276e 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -107,6 +107,8 @@ void CompilerStack::reset(bool _keepSources)
m_stackState = Empty;
m_sources.clear();
}
+ m_smtlib2Responses.clear();
+ m_unhandledSMTLib2Queries.clear();
m_libraries.clear();
m_evmVersion = EVMVersion();
m_optimize = false;
@@ -283,9 +285,10 @@ bool CompilerStack::analyze()
if (noErrors)
{
- SMTChecker smtChecker(m_errorReporter, m_smtQuery);
+ SMTChecker smtChecker(m_errorReporter, m_smtlib2Responses);
for (Source const* source: m_sourceOrder)
smtChecker.analyze(*source->ast, source->scanner);
+ m_unhandledSMTLib2Queries += smtChecker.unhandledQueries();
}
}
catch(FatalError const&)
diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h
index 8c50266e..3fceed24 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -153,6 +153,13 @@ public:
/// @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);
+ /// 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
/// @returns false on error.
bool parse();
@@ -334,7 +341,6 @@ private:
) const;
ReadCallback::Callback m_readFile;
- ReadCallback::Callback m_smtQuery;
bool m_optimize = false;
unsigned m_optimizeRuns = 200;
EVMVersion m_evmVersion;
@@ -344,6 +350,8 @@ private:
/// "context:prefix=target"
std::vector<Remapping> m_remappings;
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::vector<Source const*> m_sourceOrder;
/// This is updated during compilation.
diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 291a1071..59c28cd9 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -319,6 +319,27 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
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());
if (settings.isMember("evmVersion"))
@@ -518,6 +539,10 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
if (errors.size() > 0)
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;
unsigned sourceIndex = 0;
for (string const& sourceName: analysisSuccess ? m_compilerStack.sourceNames() : vector<string>())
generated by cgit (git 2.34.1) at 2024-10-01 06:31:49 +0800