Inject SMTLIB2 queries and responses via standard-json-io.

1 files changed, 25 insertions, 0 deletions

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>())