From bb10be789c269927e593b41d37aa0637db68bbe1 Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 13 Oct 2017 15:19:53 +0200 Subject: Inject SMTLIB2 queries and responses via standard-json-io. --- libsolidity/interface/StandardCompiler.cpp | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'libsolidity/interface/StandardCompiler.cpp') 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()) -- cgit v1.2.3 From 54bed454f6e7a53f51ec7e9bda7805900a2c8472 Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 13 Oct 2017 17:57:58 +0200 Subject: Rename function and warn if responses are supplied for Z3. --- libsolidity/interface/StandardCompiler.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'libsolidity/interface/StandardCompiler.cpp') diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 59c28cd9..a3cb90b1 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -539,8 +539,8 @@ 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()) + if (!m_compilerStack.unhandledSMTLib2Queries().empty()) + for (string const& query: m_compilerStack.unhandledSMTLib2Queries()) output["auxiliaryInputRequested"]["smtlib2"]["0x" + keccak256(query).hex()] = query; output["sources"] = Json::objectValue; -- cgit v1.2.3 From f44be616c96159fca18ad2f9ca4a1c0cb4218490 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 3 Aug 2018 16:48:20 +0200 Subject: Renaming json fields smtlib2queries and smtlib2responses --- libsolidity/interface/StandardCompiler.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'libsolidity/interface/StandardCompiler.cpp') diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index a3cb90b1..bf33b789 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -322,7 +322,7 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input) Json::Value const& auxInputs = _input["auxiliaryInput"]; if (!!auxInputs) { - Json::Value const& smtlib2Responses = auxInputs["smtlib2"]; + Json::Value const& smtlib2Responses = auxInputs["smtlib2responses"]; if (!!smtlib2Responses) for (auto const& hashString: smtlib2Responses.getMemberNames()) { @@ -541,7 +541,7 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input) if (!m_compilerStack.unhandledSMTLib2Queries().empty()) for (string const& query: m_compilerStack.unhandledSMTLib2Queries()) - output["auxiliaryInputRequested"]["smtlib2"]["0x" + keccak256(query).hex()] = query; + output["auxiliaryInputRequested"]["smtlib2queries"]["0x" + keccak256(query).hex()] = query; output["sources"] = Json::objectValue; unsigned sourceIndex = 0; -- cgit v1.2.3