5 files changed, 70 insertions, 33 deletions
diff --git a/libsolidity/interface/AssemblyStack.cpp b/libsolidity/interface/AssemblyStack.cpp
index 5b6b1113..31959d93 100644
--- a/libsolidity/interface/AssemblyStack.cpp
+++ b/libsolidity/interface/AssemblyStack.cpp
@@ -23,17 +23,16 @@
 #include <libsolidity/interface/AssemblyStack.h>
 
 #include <liblangutil/Scanner.h>
-#include <libsolidity/inlineasm/AsmPrinter.h>
-#include <libsolidity/inlineasm/AsmParser.h>
-#include <libsolidity/inlineasm/AsmAnalysis.h>
-#include <libsolidity/inlineasm/AsmAnalysisInfo.h>
-#include <libsolidity/inlineasm/AsmCodeGen.h>
-
-#include <libevmasm/Assembly.h>
-
+#include <libyul/AsmPrinter.h>
+#include <libyul/AsmParser.h>
+#include <libyul/AsmAnalysis.h>
+#include <libyul/AsmAnalysisInfo.h>
+#include <libyul/AsmCodeGen.h>
 #include <libyul/backends/evm/EVMCodeTransform.h>
 #include <libyul/backends/evm/EVMAssembly.h>
 
+#include <libevmasm/Assembly.h>
+
 using namespace std;
 using namespace dev;
 using namespace langutil;
@@ -41,19 +40,19 @@ using namespace dev::solidity;
 
 namespace
 {
-assembly::AsmFlavour languageToAsmFlavour(AssemblyStack::Language _language)
+yul::AsmFlavour languageToAsmFlavour(AssemblyStack::Language _language)
 {
 	switch (_language)
 	{
 	case AssemblyStack::Language::Assembly:
-		return assembly::AsmFlavour::Loose;
+		return yul::AsmFlavour::Loose;
 	case AssemblyStack::Language::StrictAssembly:
-		return assembly::AsmFlavour::Strict;
+		return yul::AsmFlavour::Strict;
 	case AssemblyStack::Language::Yul:
-		return assembly::AsmFlavour::Yul;
+		return yul::AsmFlavour::Yul;
 	}
 	solAssert(false, "");
-	return assembly::AsmFlavour::Yul;
+	return yul::AsmFlavour::Yul;
 }
 
 }
@@ -70,7 +69,7 @@ bool AssemblyStack::parseAndAnalyze(std::string const& _sourceName, std::string
 	m_errors.clear();
 	m_analysisSuccessful = false;
 	m_scanner = make_shared<Scanner>(CharStream(_source), _sourceName);
-	m_parserResult = assembly::Parser(m_errorReporter, languageToAsmFlavour(m_language)).parse(m_scanner, false);
+	m_parserResult = yul::Parser(m_errorReporter, languageToAsmFlavour(m_language)).parse(m_scanner, false);
 	if (!m_errorReporter.errors().empty())
 		return false;
 	solAssert(m_parserResult, "");
@@ -78,21 +77,21 @@ bool AssemblyStack::parseAndAnalyze(std::string const& _sourceName, std::string
 	return analyzeParsed();
 }
 
-bool AssemblyStack::analyze(assembly::Block const& _block, Scanner const* _scanner)
+bool AssemblyStack::analyze(yul::Block const& _block, Scanner const* _scanner)
 {
 	m_errors.clear();
 	m_analysisSuccessful = false;
 	if (_scanner)
 		m_scanner = make_shared<Scanner>(*_scanner);
-	m_parserResult = make_shared<assembly::Block>(_block);
+	m_parserResult = make_shared<yul::Block>(_block);
 
 	return analyzeParsed();
 }
 
 bool AssemblyStack::analyzeParsed()
 {
-	m_analysisInfo = make_shared<assembly::AsmAnalysisInfo>();
-	assembly::AsmAnalyzer analyzer(*m_analysisInfo, m_errorReporter, m_evmVersion, boost::none, languageToAsmFlavour(m_language));
+	m_analysisInfo = make_shared<yul::AsmAnalysisInfo>();
+	yul::AsmAnalyzer analyzer(*m_analysisInfo, m_errorReporter, m_evmVersion, boost::none, languageToAsmFlavour(m_language));
 	m_analysisSuccessful = analyzer.analyze(*m_parserResult);
 	return m_analysisSuccessful;
 }
@@ -109,7 +108,7 @@ MachineAssemblyObject AssemblyStack::assemble(Machine _machine) const
 	{
 		MachineAssemblyObject object;
 		eth::Assembly assembly;
-		assembly::CodeGenerator::assemble(*m_parserResult, *m_analysisInfo, assembly);
+		yul::CodeGenerator::assemble(*m_parserResult, *m_analysisInfo, assembly);
 		object.bytecode = make_shared<eth::LinkerObject>(assembly.assemble());
 		object.assembly = assembly.assemblyString();
 		return object;
@@ -133,5 +132,5 @@ MachineAssemblyObject AssemblyStack::assemble(Machine _machine) const
 string AssemblyStack::print() const
 {
 	solAssert(m_parserResult, "");
-	return assembly::AsmPrinter(m_language == Language::Yul)(*m_parserResult);
+	return yul::AsmPrinter(m_language == Language::Yul)(*m_parserResult);
 }
diff --git a/libsolidity/interface/AssemblyStack.h b/libsolidity/interface/AssemblyStack.h
index d6ee33cf..03b811db 100644
--- a/libsolidity/interface/AssemblyStack.h
+++ b/libsolidity/interface/AssemblyStack.h
@@ -34,16 +34,17 @@ namespace langutil
 class Scanner;
 }
 
-namespace dev
-{
-namespace solidity
-{
-namespace assembly
+namespace yul
 {
 struct AsmAnalysisInfo;
 struct Block;
 }
 
+namespace dev
+{
+namespace solidity
+{
+
 struct MachineAssemblyObject
 {
 	std::shared_ptr<eth::LinkerObject> bytecode;
@@ -73,7 +74,7 @@ public:
 
 	/// Runs analysis step on the supplied block, returns false if input cannot be assembled.
 	/// Multiple calls overwrite the previous state.
-	bool analyze(assembly::Block const& _block, langutil::Scanner const* _scanner = nullptr);
+	bool analyze(yul::Block const& _block, langutil::Scanner const* _scanner = nullptr);
 
 	/// Run the assembly step (should only be called after parseAndAnalyze).
 	MachineAssemblyObject assemble(Machine _machine) const;
@@ -93,8 +94,8 @@ private:
 	std::shared_ptr<langutil::Scanner> m_scanner;
 
 	bool m_analysisSuccessful = false;
-	std::shared_ptr<assembly::Block> m_parserResult;
-	std::shared_ptr<assembly::AsmAnalysisInfo> m_analysisInfo;
+	std::shared_ptr<yul::Block> m_parserResult;
+	std::shared_ptr<yul::AsmAnalysisInfo> m_analysisInfo;
 	langutil::ErrorList m_errors;
 	langutil::ErrorReporter m_errorReporter;
 };
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index a5674705..de4a7ec2 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -27,7 +27,6 @@
 #include <libsolidity/interface/Version.h>
 #include <libsolidity/analysis/SemVerHandler.h>
 #include <libsolidity/ast/AST.h>
-#include <liblangutil/Scanner.h>
 #include <libsolidity/parsing/Parser.h>
 #include <libsolidity/analysis/ControlFlowAnalyzer.h>
 #include <libsolidity/analysis/ControlFlowGraph.h>
@@ -45,10 +44,12 @@
 #include <libsolidity/interface/Natspec.h>
 #include <libsolidity/interface/GasEstimator.h>
 
-#include <libevmasm/Exceptions.h>
-
 #include <libyul/YulString.h>
 
+#include <liblangutil/Scanner.h>
+
+#include <libevmasm/Exceptions.h>
+
 #include <libdevcore/SwarmHash.h>
 #include <libdevcore/JSON.h>
 
@@ -107,6 +108,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 +286,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..2c7add3b 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -153,6 +153,9 @@ 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; }
+
 	/// Parses all source units that were added
 	/// @returns false on error.
 	bool parse();
@@ -188,6 +191,10 @@ public:
 	/// start line, start column, end line, end column
 	std::tuple<int, int, int, int> positionFromSourceLocation(langutil::SourceLocation const& _sourceLocation) const;
 
+	/// @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& unhandledSMTLib2Queries() const { return m_unhandledSMTLib2Queries; }
+
 	/// @returns a list of the contract names in the sources.
 	std::vector<std::string> contractNames() const;
 
@@ -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..bf33b789 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["smtlib2responses"];
+		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.unhandledSMTLib2Queries().empty())
+		for (string const& query: m_compilerStack.unhandledSMTLib2Queries())
+			output["auxiliaryInputRequested"]["smtlib2queries"]["0x" + keccak256(query).hex()] = query;
+
 	output["sources"] = Json::objectValue;
 	unsigned sourceIndex = 0;
 	for (string const& sourceName: analysisSuccess ? m_compilerStack.sourceNames() : vector<string>())