Merge remote-tracking branch 'origin/develop' into HEAD

CMakeLists.txt

@@ -51,8 +51,26 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
 include(EthOptions)
 configure_project(TESTS)
 
+find_package(Z3 4.6.0)
+if (${Z3_FOUND})
+  add_definitions(-DHAVE_Z3)
+  message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
+endif()
+
+find_package(CVC4 QUIET)
+if (${CVC4_FOUND})
+  add_definitions(-DHAVE_CVC4)
+  message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.")
+endif()
+
+if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
+  message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\
+  \nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
+endif()
+
 add_subdirectory(libsolutil)
 add_subdirectory(liblangutil)
+add_subdirectory(libsmtutil)
 add_subdirectory(libevmasm)
 add_subdirectory(libyul)
 add_subdirectory(libsolidity)

Changelog.md

@@ -25,7 +25,7 @@ Compiler Features:
  * Build system: Update the soljson.js build to emscripten 1.39.15 and boost 1.73.0 and include Z3 for integrated SMTChecker support without the callback mechanism.
  * SMTChecker: Support array ``length``.
  * SMTChecker: Support array ``push`` and ``pop``.
-
+ * Add support for natspec comments on state variables.
 
 Bugfixes:
  * Optimizer: Fixed a bug in BlockDeDuplicator.

docs/control-structures.rst

@@ -255,9 +255,9 @@ which only need to be created if there is a dispute.
 
     contract C {
         function createDSalted(bytes32 salt, uint arg) public {
-            /// This complicated expression just tells you how the address
+            // This complicated expression just tells you how the address
-            /// can be pre-computed. It is just there for illustration.
+            // can be pre-computed. It is just there for illustration.
-            /// You actually only need ``new D{salt: salt}(arg)``.
+            // You actually only need ``new D{salt: salt}(arg)``.
             address predictedAddress = address(uint(keccak256(abi.encodePacked(
                 byte(0xff),
                 address(this),

docs/natspec-format.rst

@@ -28,6 +28,9 @@ Documentation Example
 Documentation is inserted above each ``class``, ``interface`` and
 ``function`` using the doxygen notation format.
 
+Note: a ``public`` state variable is equivalent to a ``function``
+for the purposes of NatSpec.
+
 -  For Solidity you may choose ``///`` for single or multi-line
    comments, or ``/**`` and ending with ``*/``.
 
@@ -82,10 +85,10 @@ Tag
 =========== =============================================================================== =============================
 ``@title``  A title that should describe the contract/interface                             contract, interface
 ``@author`` The name of the author                                                          contract, interface, function
-``@notice`` Explain to an end user what this does                                           contract, interface, function
+``@notice`` Explain to an end user what this does                                           contract, interface, function, public state variable
-``@dev``    Explain to a developer any extra details                                        contract, interface, function
+``@dev``    Explain to a developer any extra details                                        contract, interface, function, state variable
 ``@param``  Documents a parameter just like in doxygen (must be followed by parameter name) function
-``@return`` Documents the return variables of a contract's function                         function
+``@return`` Documents the return variables of a contract's function                         function, public state variable
 =========== =============================================================================== =============================
 
 If your function returns multiple values, like ``(int quotient, int remainder)``

docs/security-considerations.rst

@@ -63,7 +63,7 @@ complete contract):
 
     // THIS CONTRACT CONTAINS A BUG - DO NOT USE
     contract Fund {
-        /// Mapping of ether shares of the contract.
+        /// @dev Mapping of ether shares of the contract.
         mapping(address => uint) shares;
         /// Withdraw your share.
         function withdraw() public {
@@ -87,7 +87,7 @@ as it uses ``call`` which forwards all remaining gas by default:
 
     // THIS CONTRACT CONTAINS A BUG - DO NOT USE
     contract Fund {
-        /// Mapping of ether shares of the contract.
+        /// @dev Mapping of ether shares of the contract.
         mapping(address => uint) shares;
         /// Withdraw your share.
         function withdraw() public {
@@ -106,7 +106,7 @@ outlined further below:
     pragma solidity >=0.4.11 <0.8.0;
 
     contract Fund {
-        /// Mapping of ether shares of the contract.
+        /// @dev Mapping of ether shares of the contract.
         mapping(address => uint) shares;
         /// Withdraw your share.
         function withdraw() public {

docs/types/reference-types.rst

@@ -415,7 +415,7 @@ Array slices are useful to ABI-decode secondary data passed in function paramete
     pragma solidity >=0.6.0 <0.8.0;
 
     contract Proxy {
-        /// Address of the client contract managed by proxy i.e., this contract
+        /// @dev Address of the client contract managed by proxy i.e., this contract
         address client;
 
         constructor(address _client) public {

libsmtutil/CHCSmtLib2Interface.cpp

@@ -15,7 +15,7 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/CHCSmtLib2Interface.h>
+#include <libsmtutil/CHCSmtLib2Interface.h>
 
 #include <libsolutil/Keccak256.h>
 
@@ -32,7 +32,7 @@ using namespace std;
 using namespace solidity;
 using namespace solidity::util;
 using namespace solidity::frontend;
-using namespace solidity::frontend::smt;
+using namespace solidity::smtutil;
 
 CHCSmtLib2Interface::CHCSmtLib2Interface(
 	map<h256, string> const& _queryResponses,
@@ -51,10 +51,10 @@ void CHCSmtLib2Interface::reset()
 	m_variables.clear();
 }
 
-void CHCSmtLib2Interface::registerRelation(smt::Expression const& _expr)
+void CHCSmtLib2Interface::registerRelation(Expression const& _expr)
 {
-	solAssert(_expr.sort, "");
+	smtAssert(_expr.sort, "");
-	solAssert(_expr.sort->kind == smt::Kind::Function, "");
+	smtAssert(_expr.sort->kind == Kind::Function, "");
 	if (!m_variables.count(_expr.name))
 	{
 		auto fSort = dynamic_pointer_cast<FunctionSort>(_expr.sort);
@@ -71,7 +71,7 @@ void CHCSmtLib2Interface::registerRelation(smt::Expression const& _expr)
 	}
 }
 
-void CHCSmtLib2Interface::addRule(smt::Expression const& _expr, std::string const& _name)
+void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& _name)
 {
 	write(
 		"(rule (! " +
@@ -82,7 +82,7 @@ void CHCSmtLib2Interface::addRule(smt::Expression const& _expr, std::string cons
 	);
 }
 
-pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(smt::Expression const& _block)
+pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(Expression const& _block)
 {
 	string accumulated{};
 	swap(m_accumulatedOutput, accumulated);
@@ -112,7 +112,7 @@ pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(smt::Expression con
 
 void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	solAssert(_sort, "");
+	smtAssert(_sort, "");
 	if (_sort->kind == Kind::Function)
 		declareFunction(_name, _sort);
 	else if (!m_variables.count(_name))
@@ -124,13 +124,13 @@ void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const
 
 void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
 {
-	solAssert(_sort, "");
+	smtAssert(_sort, "");
-	solAssert(_sort->kind == smt::Kind::Function, "");
+	smtAssert(_sort->kind == Kind::Function, "");
 	// TODO Use domain and codomain as key as well
 	if (!m_variables.count(_name))
 	{
 		auto fSort = dynamic_pointer_cast<FunctionSort>(_sort);
-		solAssert(fSort->codomain, "");
+		smtAssert(fSort->codomain, "");
 		string domain = m_smtlib2->toSmtLibSort(fSort->domain);
 		string codomain = m_smtlib2->toSmtLibSort(*fSort->codomain);
 		m_variables.insert(_name);

libsmtutil/CHCSmtLib2Interface.h

@@ -21,11 +21,11 @@
 
 #pragma once
 
-#include <libsolidity/formal/CHCSolverInterface.h>
+#include <libsmtutil/CHCSolverInterface.h>
 
-#include <libsolidity/formal/SMTLib2Interface.h>
+#include <libsmtutil/SMTLib2Interface.h>
 
-namespace solidity::frontend::smt
+namespace solidity::smtutil
 {
 
 class CHCSmtLib2Interface: public CHCSolverInterface
@@ -33,7 +33,7 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 public:
 	explicit CHCSmtLib2Interface(
 		std::map<util::h256, std::string> const& _queryResponses,
-		ReadCallback::Callback const& _smtCallback
+		frontend::ReadCallback::Callback const& _smtCallback
 	);
 
 	void reset();
@@ -67,7 +67,7 @@ private:
 	std::map<util::h256, std::string> const& m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;
 
-	ReadCallback::Callback m_smtCallback;
+	frontend::ReadCallback::Callback m_smtCallback;
 };
 
 }

libsmtutil/CHCSolverInterface.h

@@ -21,9 +21,9 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 
-namespace solidity::frontend::smt
+namespace solidity::smtutil
 {
 
 class CHCSolverInterface

libsmtutil/CMakeLists.txt

@@ -0,0 +1,35 @@
+set(sources
+	CHCSmtLib2Interface.cpp
+	CHCSmtLib2Interface.h
+	Exceptions.h
+	SMTLib2Interface.cpp
+	SMTLib2Interface.h
+	SMTPortfolio.cpp
+	SMTPortfolio.h
+	SolverInterface.h
+	Sorts.cpp
+	Sorts.h
+)
+
+if (${Z3_FOUND})
+  set(z3_SRCS Z3Interface.cpp Z3Interface.h Z3CHCInterface.cpp Z3CHCInterface.h)
+else()
+  set(z3_SRCS)
+endif()
+
+if (${CVC4_FOUND})
+  set(cvc4_SRCS CVC4Interface.cpp CVC4Interface.h)
+else()
+  set(cvc4_SRCS)
+endif()
+
+add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS})
+target_link_libraries(smtutil PUBLIC solutil Boost::boost)
+
+if (${Z3_FOUND})
+  target_link_libraries(smtutil PUBLIC z3::libz3)
+endif()
+
+if (${CVC4_FOUND})
+  target_link_libraries(smtutil PUBLIC CVC4::CVC4)
+endif()

libsmtutil/CVC4Interface.cpp

@@ -15,15 +15,14 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/CVC4Interface.h>
+#include <libsmtutil/CVC4Interface.h>
 
-#include <liblangutil/Exceptions.h>
 #include <libsolutil/CommonIO.h>
 
 using namespace std;
 using namespace solidity;
 using namespace solidity::util;
-using namespace solidity::frontend::smt;
+using namespace solidity::smtutil;
 
 CVC4Interface::CVC4Interface():
 	m_solver(&m_context)
@@ -51,7 +50,7 @@ void CVC4Interface::pop()
 
 void CVC4Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	solAssert(_sort, "");
+	smtAssert(_sort, "");
 	m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort));
 }
 
@@ -63,19 +62,19 @@ void CVC4Interface::addAssertion(Expression const& _expr)
 	}
 	catch (CVC4::TypeCheckingException const& _e)
 	{
-		solAssert(false, _e.what());
+		smtAssert(false, _e.what());
 	}
 	catch (CVC4::LogicException const& _e)
 	{
-		solAssert(false, _e.what());
+		smtAssert(false, _e.what());
 	}
 	catch (CVC4::UnsafeInterruptException const& _e)
 	{
-		solAssert(false, _e.what());
+		smtAssert(false, _e.what());
 	}
 	catch (CVC4::Exception const& _e)
 	{
-		solAssert(false, _e.what());
+		smtAssert(false, _e.what());
 	}
 }
 
@@ -97,7 +96,7 @@ pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const&
 			result = CheckResult::UNKNOWN;
 			break;
 		default:
-			solAssert(false, "");
+			smtAssert(false, "");
 		}
 
 		if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
@@ -147,15 +146,15 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 				}
 				catch (CVC4::TypeCheckingException const& _e)
 				{
-					solAssert(false, _e.what());
+					smtAssert(false, _e.what());
 				}
 				catch (CVC4::Exception const& _e)
 				{
-					solAssert(false, _e.what());
+					smtAssert(false, _e.what());
 				}
 		}
 
-		solAssert(_expr.hasCorrectArity(), "");
+		smtAssert(_expr.hasCorrectArity(), "");
 		if (n == "ite")
 			return arguments[0].iteExpr(arguments[1], arguments[2]);
 		else if (n == "not")
@@ -193,13 +192,13 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 		else if (n == "const_array")
 		{
 			shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
-			solAssert(sortSort, "");
+			smtAssert(sortSort, "");
 			return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1]));
 		}
 		else if (n == "tuple_get")
 		{
 			shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.arguments[0].sort);
-			solAssert(tupleSort, "");
+			smtAssert(tupleSort, "");
 			CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
 			CVC4::Datatype const& dt = tt.getDatatype();
 			size_t index = std::stoi(_expr.arguments[1].name);
@@ -209,25 +208,25 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 		else if (n == "tuple_constructor")
 		{
 			shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.sort);
-			solAssert(tupleSort, "");
+			smtAssert(tupleSort, "");
 			CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
 			CVC4::Datatype const& dt = tt.getDatatype();
 			CVC4::Expr c = dt[0].getConstructor();
 			return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments);
 		}
 
-		solAssert(false, "");
+		smtAssert(false, "");
 	}
 	catch (CVC4::TypeCheckingException const& _e)
 	{
-		solAssert(false, _e.what());
+		smtAssert(false, _e.what());
 	}
 	catch (CVC4::Exception const& _e)
 	{
-		solAssert(false, _e.what());
+		smtAssert(false, _e.what());
 	}
 
-	solAssert(false, "");
+	smtAssert(false, "");
 }
 
 CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
@@ -256,7 +255,7 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
 	default:
 		break;
 	}
-	solAssert(false, "");
+	smtAssert(false, "");
 	// Cannot be reached.
 	return m_context.integerType();
 }

libsmtutil/CVC4Interface.h

@@ -17,7 +17,7 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 #include <boost/noncopyable.hpp>
 
 #if defined(__GLIBC__)
@@ -33,7 +33,7 @@
 #undef _GLIBCXX_PERMIT_BACKWARD_HASH
 #endif
 
-namespace solidity::frontend::smt
+namespace solidity::smtutil
 {
 
 class CVC4Interface: public SolverInterface, public boost::noncopyable
@@ -53,8 +53,8 @@ public:
 
 private:
 	CVC4::Expr toCVC4Expr(Expression const& _expr);
-	CVC4::Type cvc4Sort(smt::Sort const& _sort);
+	CVC4::Type cvc4Sort(Sort const& _sort);
-	std::vector<CVC4::Type> cvc4Sort(std::vector<smt::SortPointer> const& _sorts);
+	std::vector<CVC4::Type> cvc4Sort(std::vector<SortPointer> const& _sorts);
 
 	CVC4::ExprManager m_context;
 	CVC4::SmtEngine m_solver;

libsmtutil/Exceptions.h

@@ -0,0 +1,31 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolutil/Assertions.h>
+#include <libsolutil/Exceptions.h>
+
+namespace solidity::smtutil
+{
+
+struct SMTLogicError: virtual util::Exception {};
+
+#define smtAssert(CONDITION, DESCRIPTION) \
+	assertThrow(CONDITION, SMTLogicError, DESCRIPTION)
+
+}

libsmtutil/SMTLib2Interface.cpp

@@ -15,7 +15,7 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/SMTLib2Interface.h>
+#include <libsmtutil/SMTLib2Interface.h>
 
 #include <libsolutil/Keccak256.h>
 
@@ -34,7 +34,7 @@ using namespace std;
 using namespace solidity;
 using namespace solidity::util;
 using namespace solidity::frontend;
-using namespace solidity::frontend::smt;
+using namespace solidity::smtutil;
 
 SMTLib2Interface::SMTLib2Interface(
 	map<h256, string> const& _queryResponses,
@@ -63,13 +63,13 @@ void SMTLib2Interface::push()
 
 void SMTLib2Interface::pop()
 {
-	solAssert(!m_accumulatedOutput.empty(), "");
+	smtAssert(!m_accumulatedOutput.empty(), "");
 	m_accumulatedOutput.pop_back();
 }
 
 void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	solAssert(_sort, "");
+	smtAssert(_sort, "");
 	if (_sort->kind == Kind::Function)
 		declareFunction(_name, _sort);
 	else if (!m_variables.count(_name))
@@ -81,8 +81,8 @@ void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _
 
 void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
 {
-	solAssert(_sort, "");
+	smtAssert(_sort, "");
-	solAssert(_sort->kind == smt::Kind::Function, "");
+	smtAssert(_sort->kind == Kind::Function, "");
 	// TODO Use domain and codomain as key as well
 	if (!m_variables.count(_name))
 	{
@@ -102,12 +102,12 @@ void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _
 	}
 }
 
-void SMTLib2Interface::addAssertion(smt::Expression const& _expr)
+void SMTLib2Interface::addAssertion(Expression const& _expr)
 {
 	write("(assert " + toSExpr(_expr) + ")");
 }
 
-pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<smt::Expression> const& _expressionsToEvaluate)
+pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
 {
 	string response = querySolver(
 		boost::algorithm::join(m_accumulatedOutput, "\n") +
@@ -131,7 +131,7 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<smt::Expression
 	return make_pair(result, values);
 }
 
-string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
+string SMTLib2Interface::toSExpr(Expression const& _expr)
 {
 	if (_expr.arguments.empty())
 		return _expr.name;
@@ -139,26 +139,26 @@ string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
 	std::string sexpr = "(";
 	if (_expr.name == "const_array")
 	{
-		solAssert(_expr.arguments.size() == 2, "");
+		smtAssert(_expr.arguments.size() == 2, "");
 		auto sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments.at(0).sort);
-		solAssert(sortSort, "");
+		smtAssert(sortSort, "");
 		auto arraySort = dynamic_pointer_cast<ArraySort>(sortSort->inner);
-		solAssert(arraySort, "");
+		smtAssert(arraySort, "");
 		sexpr += "(as const " + toSmtLibSort(*arraySort) + ") ";
 		sexpr += toSExpr(_expr.arguments.at(1));
 	}
 	else if (_expr.name == "tuple_get")
 	{
-		solAssert(_expr.arguments.size() == 2, "");
+		smtAssert(_expr.arguments.size() == 2, "");
 		auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.arguments.at(0).sort);
 		unsigned index = std::stoi(_expr.arguments.at(1).name);
-		solAssert(index < tupleSort->members.size(), "");
+		smtAssert(index < tupleSort->members.size(), "");
 		sexpr += "|" + tupleSort->members.at(index) + "| " + toSExpr(_expr.arguments.at(0));
 	}
 	else if (_expr.name == "tuple_constructor")
 	{
 		auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.sort);
-		solAssert(tupleSort, "");
+		smtAssert(tupleSort, "");
 		sexpr += "|" + tupleSort->name + "|";
 		for (auto const& arg: _expr.arguments)
 			sexpr += " " + toSExpr(arg);
@@ -184,7 +184,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 	case Kind::Array:
 	{
 		auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
-		solAssert(arraySort.domain && arraySort.range, "");
+		smtAssert(arraySort.domain && arraySort.range, "");
 		return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
 	}
 	case Kind::Tuple:
@@ -195,7 +195,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 		{
 			m_userSorts.insert(tupleName);
 			string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName);
-			solAssert(tupleSort.members.size() == tupleSort.components.size(), "");
+			smtAssert(tupleSort.members.size() == tupleSort.components.size(), "");
 			for (unsigned i = 0; i < tupleSort.members.size(); ++i)
 				decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")";
 			decl += "))))";
@@ -205,7 +205,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 		return tupleName;
 	}
 	default:
-		solAssert(false, "Invalid SMT sort");
+		smtAssert(false, "Invalid SMT sort");
 	}
 }
 
@@ -220,11 +220,11 @@ string SMTLib2Interface::toSmtLibSort(vector<SortPointer> const& _sorts)
 
 void SMTLib2Interface::write(string _data)
 {
-	solAssert(!m_accumulatedOutput.empty(), "");
+	smtAssert(!m_accumulatedOutput.empty(), "");
 	m_accumulatedOutput.back() += move(_data) + "\n";
 }
 
-string SMTLib2Interface::checkSatAndGetValuesCommand(vector<smt::Expression> const& _expressionsToEvaluate)
+string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate)
 {
 	string command;
 	if (_expressionsToEvaluate.empty())
@@ -235,7 +235,7 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<smt::Expression> con
 		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
 		{
 			auto const& e = _expressionsToEvaluate.at(i);
-			solAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate.");
+			smtAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate.");
 			command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n";
 			command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
 		}

libsmtutil/SMTLib2Interface.h

@@ -17,10 +17,10 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 
 #include <libsolidity/interface/ReadFile.h>
-#include <liblangutil/Exceptions.h>
+
 #include <libsolutil/Common.h>
 #include <libsolutil/FixedHash.h>
 
@@ -31,7 +31,7 @@
 #include <string>
 #include <vector>
 
-namespace solidity::frontend::smt
+namespace solidity::smtutil
 {
 
 class SMTLib2Interface: public SolverInterface, public boost::noncopyable
@@ -39,7 +39,7 @@ class SMTLib2Interface: public SolverInterface, public boost::noncopyable
 public:
 	explicit SMTLib2Interface(
 		std::map<util::h256, std::string> const& _queryResponses,
-		ReadCallback::Callback _smtCallback
+		frontend::ReadCallback::Callback _smtCallback
 	);
 
 	void reset() override;
@@ -49,13 +49,13 @@ public:
 
 	void declareVariable(std::string const&, SortPointer const&) override;
 
-	void addAssertion(smt::Expression const& _expr) override;
+	void addAssertion(Expression const& _expr) override;
-	std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::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; }
 
 	// Used by CHCSmtLib2Interface
-	std::string toSExpr(smt::Expression const& _expr);
+	std::string toSExpr(Expression const& _expr);
 	std::string toSmtLibSort(Sort const& _sort);
 	std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
 
@@ -66,7 +66,7 @@ private:
 
 	void write(std::string _data);
 
-	std::string checkSatAndGetValuesCommand(std::vector<smt::Expression> const& _expressionsToEvaluate);
+	std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
 	std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
 
 	/// Communicates with the solver via the callback. Throws SMTSolverError on error.
@@ -79,7 +79,7 @@ private:
 	std::map<util::h256, std::string> const& m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;
 
-	ReadCallback::Callback m_smtCallback;
+	frontend::ReadCallback::Callback m_smtCallback;
 };
 
 }

libsmtutil/SMTPortfolio.cpp

@@ -15,36 +15,36 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/SMTPortfolio.h>
+#include <libsmtutil/SMTPortfolio.h>
 
 #ifdef HAVE_Z3
-#include <libsolidity/formal/Z3Interface.h>
+#include <libsmtutil/Z3Interface.h>
 #endif
 #ifdef HAVE_CVC4
-#include <libsolidity/formal/CVC4Interface.h>
+#include <libsmtutil/CVC4Interface.h>
 #endif
-#include <libsolidity/formal/SMTLib2Interface.h>
+#include <libsmtutil/SMTLib2Interface.h>
 
 using namespace std;
 using namespace solidity;
 using namespace solidity::util;
 using namespace solidity::frontend;
-using namespace solidity::frontend::smt;
+using namespace solidity::smtutil;
 
 SMTPortfolio::SMTPortfolio(
 	map<h256, string> const& _smtlib2Responses,
-	ReadCallback::Callback const& _smtCallback,
+	frontend::ReadCallback::Callback const& _smtCallback,
 	[[maybe_unused]] SMTSolverChoice _enabledSolvers
 )
 {
-	m_solvers.emplace_back(make_unique<smt::SMTLib2Interface>(_smtlib2Responses, _smtCallback));
+	m_solvers.emplace_back(make_unique<SMTLib2Interface>(_smtlib2Responses, _smtCallback));
 #ifdef HAVE_Z3
 	if (_enabledSolvers.z3)
-		m_solvers.emplace_back(make_unique<smt::Z3Interface>());
+		m_solvers.emplace_back(make_unique<Z3Interface>());
 #endif
 #ifdef HAVE_CVC4
 	if (_enabledSolvers.cvc4)
-		m_solvers.emplace_back(make_unique<smt::CVC4Interface>());
+		m_solvers.emplace_back(make_unique<CVC4Interface>());
 #endif
 }
 
@@ -68,12 +68,12 @@ void SMTPortfolio::pop()
 
 void SMTPortfolio::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	solAssert(_sort, "");
+	smtAssert(_sort, "");
 	for (auto const& s: m_solvers)
 		s->declareVariable(_name, _sort);
 }
 
-void SMTPortfolio::addAssertion(smt::Expression const& _expr)
+void SMTPortfolio::addAssertion(Expression const& _expr)
 {
 	for (auto const& s: m_solvers)
 		s->addAssertion(_expr);
@@ -109,7 +109,7 @@ void SMTPortfolio::addAssertion(smt::Expression const& _expr)
  *
  *   If all solvers return ERROR, the result is ERROR.
 */
-pair<CheckResult, vector<string>> SMTPortfolio::check(vector<smt::Expression> const& _expressionsToEvaluate)
+pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const& _expressionsToEvaluate)
 {
 	CheckResult lastResult = CheckResult::ERROR;
 	vector<string> finalValues;
@@ -141,8 +141,8 @@ vector<string> SMTPortfolio::unhandledQueries()
 {
 	// This code assumes that the constructor guarantees that
 	// SmtLib2Interface is in position 0.
-	solAssert(!m_solvers.empty(), "");
+	smtAssert(!m_solvers.empty(), "");
-	solAssert(dynamic_cast<smt::SMTLib2Interface*>(m_solvers.front().get()), "");
+	smtAssert(dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()), "");
 	return m_solvers.front()->unhandledQueries();
 }
 

libsmtutil/SMTPortfolio.h

@@ -18,7 +18,7 @@
 #pragma once
 
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 #include <libsolidity/interface/ReadFile.h>
 #include <libsolutil/FixedHash.h>
 
@@ -26,7 +26,7 @@
 #include <map>
 #include <vector>
 
-namespace solidity::frontend::smt
+namespace solidity::smtutil
 {
 
 /**
@@ -40,7 +40,7 @@ class SMTPortfolio: public SolverInterface, public boost::noncopyable
 public:
 	SMTPortfolio(
 		std::map<util::h256, std::string> const& _smtlib2Responses,
-		ReadCallback::Callback const& _smtCallback,
+		frontend::ReadCallback::Callback const& _smtCallback,
 		SMTSolverChoice _enabledSolvers
 	);
 
@@ -51,18 +51,18 @@ public:
 
 	void declareVariable(std::string const&, SortPointer const&) override;
 
-	void addAssertion(smt::Expression const& _expr) override;
+	void addAssertion(Expression const& _expr) override;
 
-	std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::Expression> const& _expressionsToEvaluate) override;
+	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
 
 	std::vector<std::string> unhandledQueries() override;
 	unsigned solvers() override { return m_solvers.size(); }
 private:
 	static bool solverAnswered(CheckResult result);
 
-	std::vector<std::unique_ptr<smt::SolverInterface>> m_solvers;
+	std::vector<std::unique_ptr<SolverInterface>> m_solvers;
 
-	std::vector<smt::Expression> m_assertions;
+	std::vector<Expression> m_assertions;
 };
 
 }

libsmtutil/SolverInterface.h

@@ -17,13 +17,10 @@
 
 #pragma once
 
-#include <libsolidity/formal/Sorts.h>
+#include <libsmtutil/Exceptions.h>
+#include <libsmtutil/Sorts.h>
 
-#include <libsolidity/ast/Types.h>
-#include <libsolidity/interface/ReadFile.h>
-#include <liblangutil/Exceptions.h>
 #include <libsolutil/Common.h>
-#include <libsolutil/Exceptions.h>
 
 #include <boost/noncopyable.hpp>
 #include <cstdio>
@@ -32,7 +29,7 @@
 #include <string>
 #include <vector>
 
-namespace solidity::frontend::smt
+namespace solidity::smtutil
 {
 
 struct SMTSolverChoice
@@ -55,17 +52,13 @@ enum class CheckResult
 	SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR
 };
 
-// Forward declaration.
-SortPointer smtSort(Type const& _type);
-
 /// C++ representation of an SMTLIB2 expression.
 class Expression
 {
 	friend class SolverInterface;
 public:
 	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
-	explicit Expression(frontend::TypePointer _type): Expression(_type->toString(true), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
+	explicit Expression(std::shared_ptr<SortSort> _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {}
-	explicit Expression(std::shared_ptr<SortSort> _sort): Expression("", {}, _sort) {}
 	Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
 	Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
 	Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {}
@@ -81,7 +74,7 @@ public:
 		if (name == "tuple_constructor")
 		{
 			auto tupleSort = std::dynamic_pointer_cast<TupleSort>(sort);
-			solAssert(tupleSort, "");
+			smtAssert(tupleSort, "");
 			return arguments.size() == tupleSort->components.size();
 		}
 
@@ -111,7 +104,7 @@ public:
 
 	static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
 	{
-		solAssert(*_trueValue.sort == *_falseValue.sort, "");
+		smtAssert(*_trueValue.sort == *_falseValue.sort, "");
 		SortPointer sort = _trueValue.sort;
 		return Expression("ite", std::vector<Expression>{
 			std::move(_condition), std::move(_trueValue), std::move(_falseValue)
@@ -131,11 +124,11 @@ public:
 	/// select is the SMT representation of an array index access.
 	static Expression select(Expression _array, Expression _index)
 	{
-		solAssert(_array.sort->kind == Kind::Array, "");
+		smtAssert(_array.sort->kind == Kind::Array, "");
 		std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
-		solAssert(arraySort, "");
+		smtAssert(arraySort, "");
-		solAssert(_index.sort, "");
+		smtAssert(_index.sort, "");
-		solAssert(*arraySort->domain == *_index.sort, "");
+		smtAssert(*arraySort->domain == *_index.sort, "");
 		return Expression(
 			"select",
 			std::vector<Expression>{std::move(_array), std::move(_index)},
@@ -148,11 +141,11 @@ public:
 	static Expression store(Expression _array, Expression _index, Expression _element)
 	{
 		auto arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
-		solAssert(arraySort, "");
+		smtAssert(arraySort, "");
-		solAssert(_index.sort, "");
+		smtAssert(_index.sort, "");
-		solAssert(_element.sort, "");
+		smtAssert(_element.sort, "");
-		solAssert(*arraySort->domain == *_index.sort, "");
+		smtAssert(*arraySort->domain == *_index.sort, "");
-		solAssert(*arraySort->range == *_element.sort, "");
+		smtAssert(*arraySort->range == *_element.sort, "");
 		return Expression(
 			"store",
 			std::vector<Expression>{std::move(_array), std::move(_index), std::move(_element)},
@@ -162,12 +155,12 @@ public:
 
 	static Expression const_array(Expression _sort, Expression _value)
 	{
-		solAssert(_sort.sort->kind == Kind::Sort, "");
+		smtAssert(_sort.sort->kind == Kind::Sort, "");
 		auto sortSort = std::dynamic_pointer_cast<SortSort>(_sort.sort);
 		auto arraySort = std::dynamic_pointer_cast<ArraySort>(sortSort->inner);
-		solAssert(sortSort && arraySort, "");
+		smtAssert(sortSort && arraySort, "");
-		solAssert(_value.sort, "");
+		smtAssert(_value.sort, "");
-		solAssert(*arraySort->range == *_value.sort, "");
+		smtAssert(*arraySort->range == *_value.sort, "");
 		return Expression(
 			"const_array",
 			std::vector<Expression>{std::move(_sort), std::move(_value)},
@@ -177,10 +170,10 @@ public:
 
 	static Expression tuple_get(Expression _tuple, size_t _index)
 	{
-		solAssert(_tuple.sort->kind == Kind::Tuple, "");
+		smtAssert(_tuple.sort->kind == Kind::Tuple, "");
 		std::shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_tuple.sort);
-		solAssert(tupleSort, "");
+		smtAssert(tupleSort, "");
-		solAssert(_index < tupleSort->components.size(), "");
+		smtAssert(_index < tupleSort->components.size(), "");
 		return Expression(
 			"tuple_get",
 			std::vector<Expression>{std::move(_tuple), Expression(_index)},
@@ -190,11 +183,11 @@ public:
 
 	static Expression tuple_constructor(Expression _tuple, std::vector<Expression> _arguments)
 	{
-		solAssert(_tuple.sort->kind == Kind::Sort, "");
+		smtAssert(_tuple.sort->kind == Kind::Sort, "");
 		auto sortSort = std::dynamic_pointer_cast<SortSort>(_tuple.sort);
 		auto tupleSort = std::dynamic_pointer_cast<TupleSort>(sortSort->inner);
-		solAssert(tupleSort, "");
+		smtAssert(tupleSort, "");
-		solAssert(_arguments.size() == tupleSort->components.size(), "");
+		smtAssert(_arguments.size() == tupleSort->components.size(), "");
 		return Expression(
 			"tuple_constructor",
 			std::move(_arguments),
@@ -260,12 +253,12 @@ public:
 	}
 	Expression operator()(std::vector<Expression> _arguments) const
 	{
-		solAssert(
+		smtAssert(
 			sort->kind == Kind::Function,
 			"Attempted function application to non-function."
 		);
 		auto fSort = dynamic_cast<FunctionSort const*>(sort.get());
-		solAssert(fSort, "");
+		smtAssert(fSort, "");
 		return Expression(name, std::move(_arguments), fSort->codomain);
 	}
 
@@ -303,7 +296,7 @@ public:
 	Expression newVariable(std::string _name, SortPointer const& _sort)
 	{
 		// Subclasses should do something here
-		solAssert(_sort, "");
+		smtAssert(_sort, "");
 		declareVariable(_name, _sort);
 		return Expression(std::move(_name), {}, _sort);
 	}

libsmtutil/Sorts.cpp

@@ -16,11 +16,11 @@
 */
 
 
-#include <libsolidity/formal/Sorts.h>
+#include <libsmtutil/Sorts.h>
 
 using namespace std;
 
-namespace solidity::frontend::smt
+namespace solidity::smtutil
 {
 
 shared_ptr<Sort> const SortProvider::boolSort{make_shared<Sort>(Kind::Bool)};

libsmtutil/Sorts.h

@@ -17,14 +17,14 @@
 
 #pragma once
 
-#include <liblangutil/Exceptions.h>
+#include <libsmtutil/Exceptions.h>
+
 #include <libsolutil/Common.h>
-#include <libsolutil/Exceptions.h>
 
 #include <memory>
 #include <vector>
 
-namespace solidity::frontend::smt
+namespace solidity::smtutil
 {
 
 enum class Kind
@@ -57,7 +57,7 @@ struct FunctionSort: public Sort
 		if (!Sort::operator==(_other))
 			return false;
 		auto _otherFunction = dynamic_cast<FunctionSort const*>(&_other);
-		solAssert(_otherFunction, "");
+		smtAssert(_otherFunction, "");
 		if (domain.size() != _otherFunction->domain.size())
 			return false;
 		if (!std::equal(
@@ -67,8 +67,8 @@ struct FunctionSort: public Sort
 			[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
 		))
 			return false;
-		solAssert(codomain, "");
+		smtAssert(codomain, "");
-		solAssert(_otherFunction->codomain, "");
+		smtAssert(_otherFunction->codomain, "");
 		return *codomain == *_otherFunction->codomain;
 	}
 
@@ -87,11 +87,11 @@ struct ArraySort: public Sort
 		if (!Sort::operator==(_other))
 			return false;
 		auto _otherArray = dynamic_cast<ArraySort const*>(&_other);
-		solAssert(_otherArray, "");
+		smtAssert(_otherArray, "");
-		solAssert(_otherArray->domain, "");
+		smtAssert(_otherArray->domain, "");
-		solAssert(_otherArray->range, "");
+		smtAssert(_otherArray->range, "");
-		solAssert(domain, "");
+		smtAssert(domain, "");
-		solAssert(range, "");
+		smtAssert(range, "");
 		return *domain == *_otherArray->domain && *range == *_otherArray->range;
 	}
 
@@ -107,9 +107,9 @@ struct SortSort: public Sort
 		if (!Sort::operator==(_other))
 			return false;
 		auto _otherSort = dynamic_cast<SortSort const*>(&_other);
-		solAssert(_otherSort, "");
+		smtAssert(_otherSort, "");
-		solAssert(_otherSort->inner, "");
+		smtAssert(_otherSort->inner, "");
-		solAssert(inner, "");
+		smtAssert(inner, "");
 		return *inner == *_otherSort->inner;
 	}
 
@@ -134,7 +134,7 @@ struct TupleSort: public Sort
 		if (!Sort::operator==(_other))
 			return false;
 		auto _otherTuple = dynamic_cast<TupleSort const*>(&_other);
-		solAssert(_otherTuple, "");
+		smtAssert(_otherTuple, "");
 		if (name != _otherTuple->name)
 			return false;
 		if (members != _otherTuple->members)

libsmtutil/Z3CHCInterface.cpp

@@ -15,14 +15,13 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/Z3CHCInterface.h>
+#include <libsmtutil/Z3CHCInterface.h>
 
-#include <liblangutil/Exceptions.h>
 #include <libsolutil/CommonIO.h>
 
 using namespace std;
 using namespace solidity;
-using namespace solidity::frontend::smt;
+using namespace solidity::smtutil;
 
 Z3CHCInterface::Z3CHCInterface():
 	m_z3Interface(make_unique<Z3Interface>()),
@@ -48,7 +47,7 @@ Z3CHCInterface::Z3CHCInterface():
 
 void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	solAssert(_sort, "");
+	smtAssert(_sort, "");
 	m_z3Interface->declareVariable(_name, _sort);
 }
 

libsmtutil/Z3CHCInterface.h

@@ -21,10 +21,10 @@
 
 #pragma once
 
-#include <libsolidity/formal/CHCSolverInterface.h>
+#include <libsmtutil/CHCSolverInterface.h>
-#include <libsolidity/formal/Z3Interface.h>
+#include <libsmtutil/Z3Interface.h>
 
-namespace solidity::frontend::smt
+namespace solidity::smtutil
 {
 
 class Z3CHCInterface: public CHCSolverInterface

libsmtutil/Z3Interface.cpp

@@ -15,13 +15,12 @@
 	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 */
 
-#include <libsolidity/formal/Z3Interface.h>
+#include <libsmtutil/Z3Interface.h>
 
-#include <liblangutil/Exceptions.h>
 #include <libsolutil/CommonIO.h>
 
 using namespace std;
-using namespace solidity::frontend::smt;
+using namespace solidity::smtutil;
 
 Z3Interface::Z3Interface():
 	m_solver(m_context)
@@ -50,7 +49,7 @@ void Z3Interface::pop()
 
 void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	solAssert(_sort, "");
+	smtAssert(_sort, "");
 	if (_sort->kind == Kind::Function)
 		declareFunction(_name, *_sort);
 	else if (m_constants.count(_name))
@@ -61,7 +60,7 @@ void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort)
 
 void Z3Interface::declareFunction(string const& _name, Sort const& _sort)
 {
-	solAssert(_sort.kind == smt::Kind::Function, "");
+	smtAssert(_sort.kind == Kind::Function, "");
 	FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
 	if (m_functions.count(_name))
 		m_functions.at(_name) = m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain));
@@ -124,7 +123,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			return m_functions.at(n)(arguments);
 		else if (m_constants.count(n))
 		{
-			solAssert(arguments.empty(), "");
+			smtAssert(arguments.empty(), "");
 			return m_constants.at(n);
 		}
 		else if (arguments.empty())
@@ -136,7 +135,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			else if (_expr.sort->kind == Kind::Sort)
 			{
 				auto sortSort = dynamic_pointer_cast<SortSort>(_expr.sort);
-				solAssert(sortSort, "");
+				smtAssert(sortSort, "");
 				return m_context.constant(n.c_str(), z3Sort(*sortSort->inner));
 			}
 			else
@@ -146,11 +145,11 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 				}
 				catch (z3::exception const& _e)
 				{
-					solAssert(false, _e.msg());
+					smtAssert(false, _e.msg());
 				}
 		}
 
-		solAssert(_expr.hasCorrectArity(), "");
+		smtAssert(_expr.hasCorrectArity(), "");
 		if (n == "ite")
 			return z3::ite(arguments[0], arguments[1], arguments[2]);
 		else if (n == "not")
@@ -188,9 +187,9 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		else if (n == "const_array")
 		{
 			shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
-			solAssert(sortSort, "");
+			smtAssert(sortSort, "");
 			auto arraySort = dynamic_pointer_cast<ArraySort>(sortSort->inner);
-			solAssert(arraySort && arraySort->domain, "");
+			smtAssert(arraySort && arraySort->domain, "");
 			return z3::const_array(z3Sort(*arraySort->domain), arguments[1]);
 		}
 		else if (n == "tuple_get")
@@ -201,21 +200,21 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		else if (n == "tuple_constructor")
 		{
 			auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort)));
-			solAssert(constructor.arity() == arguments.size(), "");
+			smtAssert(constructor.arity() == arguments.size(), "");
 			z3::expr_vector args(m_context);
 			for (auto const& arg: arguments)
 				args.push_back(arg);
 			return constructor(args);
 		}
 
-		solAssert(false, "");
+		smtAssert(false, "");
 	}
 	catch (z3::exception const& _e)
 	{
-		solAssert(false, _e.msg());
+		smtAssert(false, _e.msg());
 	}
 
-	solAssert(false, "");
+	smtAssert(false, "");
 }
 
 z3::sort Z3Interface::z3Sort(Sort const& _sort)
@@ -256,7 +255,7 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
 	default:
 		break;
 	}
-	solAssert(false, "");
+	smtAssert(false, "");
 	// Cannot be reached.
 	return m_context.int_sort();
 }

libsmtutil/Z3Interface.h

@@ -17,11 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 #include <boost/noncopyable.hpp>
 #include <z3++.h>
 
-namespace solidity::frontend::smt
+namespace solidity::smtutil
 {
 
 class Z3Interface: public SolverInterface, public boost::noncopyable
@@ -55,8 +55,8 @@ public:
 private:
 	void declareFunction(std::string const& _name, Sort const& _sort);
 
-	z3::sort z3Sort(smt::Sort const& _sort);
+	z3::sort z3Sort(Sort const& _sort);
-	z3::sort_vector z3Sort(std::vector<smt::SortPointer> const& _sorts);
+	z3::sort_vector z3Sort(std::vector<SortPointer> const& _sorts);
 
 	z3::context m_context;
 	z3::solver m_solver;

libsolidity/CMakeLists.txt

@@ -94,22 +94,12 @@ set(sources
 	formal/BMC.h
 	formal/CHC.cpp
 	formal/CHC.h
-	formal/CHCSmtLib2Interface.cpp
-	formal/CHCSmtLib2Interface.h
-	formal/CHCSolverInterface.h
 	formal/EncodingContext.cpp
 	formal/EncodingContext.h
 	formal/ModelChecker.cpp
 	formal/ModelChecker.h
 	formal/SMTEncoder.cpp
 	formal/SMTEncoder.h
-	formal/SMTLib2Interface.cpp
-	formal/SMTLib2Interface.h
-	formal/SMTPortfolio.cpp
-	formal/SMTPortfolio.h
-	formal/SolverInterface.h
-	formal/Sorts.cpp
-	formal/Sorts.h
 	formal/SSAVariable.cpp
 	formal/SSAVariable.h
 	formal/SymbolicState.cpp
@@ -144,36 +134,6 @@ set(sources
 	parsing/Token.h
 )
 
-find_package(Z3 4.6.0)
+add_library(solidity ${sources})
-if (${Z3_FOUND})
+target_link_libraries(solidity PUBLIC yul evmasm langutil smtutil solutil Boost::boost)
-  add_definitions(-DHAVE_Z3)
-  message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
-  set(z3_SRCS formal/Z3Interface.cpp formal/Z3Interface.h formal/Z3CHCInterface.cpp formal/Z3CHCInterface.h)
-else()
-  set(z3_SRCS)
-endif()
 
-find_package(CVC4 QUIET)
-if (${CVC4_FOUND})
-  add_definitions(-DHAVE_CVC4)
-  message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.")
-  set(cvc4_SRCS formal/CVC4Interface.cpp formal/CVC4Interface.h)
-else()
-  set(cvc4_SRCS)
-endif()
-
-if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
-  message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\
-  \nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
-endif()
-
-add_library(solidity ${sources} ${z3_SRCS} ${cvc4_SRCS})
-target_link_libraries(solidity PUBLIC yul evmasm langutil solutil Boost::boost)
-
-if (${Z3_FOUND})
-  target_link_libraries(solidity PUBLIC z3::libz3)
-endif()
-
-if (${CVC4_FOUND})
-  target_link_libraries(solidity PUBLIC CVC4::CVC4)
-endif()

libsolidity/analysis/DocStringAnalyser.cpp

@@ -34,10 +34,9 @@ using namespace solidity::frontend;
 
 bool DocStringAnalyser::analyseDocStrings(SourceUnit const& _sourceUnit)
 {
-	m_errorOccured = false;
+	auto errorWatcher = m_errorReporter.errorWatcher();
 	_sourceUnit.accept(*this);
-
+	return errorWatcher.ok();
-	return !m_errorOccured;
 }
 
 bool DocStringAnalyser::visit(ContractDefinition const& _contract)
@@ -57,6 +56,31 @@ bool DocStringAnalyser::visit(FunctionDefinition const& _function)
 	return true;
 }
 
+bool DocStringAnalyser::visit(VariableDeclaration const& _variable)
+{
+	if (_variable.isStateVariable())
+	{
+		static set<string> const validPublicTags = set<string>{"dev", "notice", "return", "title", "author"};
+		if (_variable.isPublic())
+			parseDocStrings(_variable, _variable.annotation(), validPublicTags, "public state variables");
+		else
+		{
+			parseDocStrings(_variable, _variable.annotation(), validPublicTags, "non-public state variables");
+			if (_variable.annotation().docTags.count("notice") > 0)
+				m_errorReporter.warning(
+					9098_error, _variable.documentation()->location(),
+					"Documentation tag on non-public state variables will be disallowed in 0.7.0. You will need to use the @dev tag explicitly."
+				);
+		}
+		if (_variable.annotation().docTags.count("title") > 0 || _variable.annotation().docTags.count("author") > 0)
+			m_errorReporter.warning(
+				4822_error, _variable.documentation()->location(),
+				"Documentation tag @title and @author is only allowed on contract definitions. It will be disallowed in 0.7.0."
+			);
+	}
+	return false;
+}
+
 bool DocStringAnalyser::visit(ModifierDefinition const& _modifier)
 {
 	handleCallable(_modifier, _modifier, _modifier.annotation());
@@ -127,8 +151,7 @@ void DocStringAnalyser::parseDocStrings(
 	DocStringParser parser;
 	if (_node.documentation() && !_node.documentation()->text()->empty())
 	{
-		if (!parser.parse(*_node.documentation()->text(), m_errorReporter))
+		parser.parse(*_node.documentation()->text(), m_errorReporter);
-			m_errorOccured = true;
 		_annotation.docTags = parser.tags();
 	}
 
@@ -144,7 +167,20 @@ void DocStringAnalyser::parseDocStrings(
 			if (docTag.first == "return")
 			{
 				returnTagsVisited++;
-				if (auto* function = dynamic_cast<FunctionDefinition const*>(&_node))
+				if (auto* varDecl = dynamic_cast<VariableDeclaration const*>(&_node))
+				{
+					if (!varDecl->isPublic())
+						appendError(
+							_node.documentation()->location(),
+							"Documentation tag \"@" + docTag.first + "\" is only allowed on public state-variables."
+						);
+					if (returnTagsVisited > 1)
+						appendError(
+							_node.documentation()->location(),
+							"Documentation tag \"@" + docTag.first + "\" is only allowed once on state-variables."
+						);
+				}
+				else if (auto* function = dynamic_cast<FunctionDefinition const*>(&_node))
 				{
 					string content = docTag.second.content;
 					string firstWord = content.substr(0, content.find_first_of(" \t"));
@@ -172,6 +208,5 @@ void DocStringAnalyser::parseDocStrings(
 
 void DocStringAnalyser::appendError(SourceLocation const& _location, string const& _description)
 {
-	m_errorOccured = true;
 	m_errorReporter.docstringParsingError(7816_error, _location, _description);
 }

libsolidity/analysis/DocStringAnalyser.h

@@ -46,6 +46,7 @@ public:
 private:
 	bool visit(ContractDefinition const& _contract) override;
 	bool visit(FunctionDefinition const& _function) override;
+	bool visit(VariableDeclaration const& _variable) override;
 	bool visit(ModifierDefinition const& _modifier) override;
 	bool visit(EventDefinition const& _event) override;
 
@@ -67,6 +68,12 @@ private:
 		StructurallyDocumentedAnnotation& _annotation
 	);
 
+	void handleDeclaration(
+		Declaration const& _declaration,
+		StructurallyDocumented const& _node,
+		StructurallyDocumentedAnnotation& _annotation
+	);
+
 	void parseDocStrings(
 		StructurallyDocumented const& _node,
 		StructurallyDocumentedAnnotation& _annotation,
@@ -76,7 +83,6 @@ private:
 
 	void appendError(langutil::SourceLocation const& _location, std::string const& _description);
 
-	bool m_errorOccured = false;
 	langutil::ErrorReporter& m_errorReporter;
 };
 

libsolidity/analysis/ReferencesResolver.cpp

@@ -44,8 +44,9 @@ namespace solidity::frontend
 
 bool ReferencesResolver::resolve(ASTNode const& _root)
 {
+	auto errorWatcher = m_errorReporter.errorWatcher();
 	_root.accept(*this);
-	return !m_errorOccurred;
+	return errorWatcher.ok();
 }
 
 bool ReferencesResolver::visit(Block const& _block)
@@ -267,19 +268,16 @@ void ReferencesResolver::operator()(yul::VariableDeclaration const& _varDecl)
 
 void ReferencesResolver::declarationError(SourceLocation const& _location, string const& _description)
 {
-	m_errorOccurred = true;
 	m_errorReporter.declarationError(8532_error, _location, _description);
 }
 
 void ReferencesResolver::declarationError(SourceLocation const& _location, SecondarySourceLocation const& _ssl, string const& _description)
 {
-	m_errorOccurred = true;
 	m_errorReporter.declarationError(3881_error, _location, _ssl, _description);
 }
 
 void ReferencesResolver::fatalDeclarationError(SourceLocation const& _location, string const& _description)
 {
-	m_errorOccurred = true;
 	m_errorReporter.fatalDeclarationError(6546_error, _location, _description);
 }
 

libsolidity/analysis/ReferencesResolver.h

@@ -103,7 +103,6 @@ private:
 	/// Stack of return parameters.
 	std::vector<ParameterList const*> m_returnParameters;
 	bool const m_resolveInsideCode;
-	bool m_errorOccurred = false;
 
 	InlineAssemblyAnnotation* m_yulAnnotation = nullptr;
 	bool m_yulInsideFunction = false;

libsolidity/ast/AST.h

@@ -859,7 +859,7 @@ private:
  * Declaration of a variable. This can be used in various places, e.g. in function parameter
  * lists, struct definitions and even function bodies.
  */
-class VariableDeclaration: public Declaration
+class VariableDeclaration: public Declaration, public StructurallyDocumented
 {
 public:
 	enum Location { Unspecified, Storage, Memory, CallData };
@@ -882,6 +882,7 @@ public:
 		ASTPointer<ASTString> const& _name,
 		ASTPointer<Expression> _value,
 		Visibility _visibility,
+		ASTPointer<StructuredDocumentation> const _documentation = nullptr,
 		bool _isStateVar = false,
 		bool _isIndexed = false,
 		Mutability _mutability = Mutability::Mutable,
@@ -889,6 +890,7 @@ public:
 		Location _referenceLocation = Location::Unspecified
 	):
 		Declaration(_id, _location, _name, _visibility),
+		StructurallyDocumented(std::move(_documentation)),
 		m_typeName(std::move(_type)),
 		m_value(std::move(_value)),
 		m_isStateVariable(_isStateVar),

libsolidity/ast/ASTAnnotations.h

@@ -171,7 +171,7 @@ struct ModifierDefinitionAnnotation: CallableDeclarationAnnotation, Structurally
 {
 };
 
-struct VariableDeclarationAnnotation: DeclarationAnnotation
+struct VariableDeclarationAnnotation: DeclarationAnnotation, StructurallyDocumentedAnnotation
 {
 	/// Type of variable (type of identifier referencing this variable).
 	TypePointer type = nullptr;

libsolidity/ast/ASTJsonConverter.cpp

@@ -391,6 +391,8 @@ bool ASTJsonConverter::visit(VariableDeclaration const& _node)
 	};
 	if (_node.isStateVariable() && _node.isPublic())
 		attributes.emplace_back("functionSelector", _node.externalIdentifierHex());
+	if (_node.isStateVariable() && _node.documentation())
+		attributes.emplace_back("documentation", toJson(*_node.documentation()));
 	if (m_inEvent)
 		attributes.emplace_back("indexed", _node.isIndexed());
 	if (!_node.annotation().baseFunctions.empty())

libsolidity/ast/ASTJsonImporter.cpp

@@ -441,6 +441,7 @@ ASTPointer<VariableDeclaration> ASTJsonImporter::createVariableDeclaration(Json:
 		make_shared<ASTString>(member(_node, "name").asString()),
 		nullOrCast<Expression>(member(_node, "value")),
 		visibility(_node),
+		_node["documentation"].isNull() ? nullptr : createDocumentation(member(_node, "documentation")),
 		memberAsBool(_node, "stateVariable"),
 		_node.isMember("indexed") ? memberAsBool(_node, "indexed") : false,
 		mutability,

libsolidity/codegen/ir/Common.cpp

@@ -16,6 +16,7 @@
 */
 
 #include <libsolidity/codegen/ir/Common.h>
+#include <libsolidity/ast/TypeProvider.h>
 
 #include <libsolutil/CommonIO.h>
 
@@ -23,6 +24,13 @@ using namespace std;
 using namespace solidity::util;
 using namespace solidity::frontend;
 
+YulArity YulArity::fromType(FunctionType const& _functionType)
+{
+	return YulArity{
+		TupleType(_functionType.parameterTypes()).sizeOnStack(),
+		TupleType(_functionType.returnParameterTypes()).sizeOnStack()
+	};
+}
 string IRNames::function(FunctionDefinition const& _function)
 {
 	// @TODO previously, we had to distinguish creation context and runtime context,
@@ -45,6 +53,13 @@ string IRNames::runtimeObject(ContractDefinition const& _contract)
 	return _contract.name() + "_" + toString(_contract.id()) + "_deployed";
 }
 
+string IRNames::internalDispatch(YulArity const& _arity)
+{
+	return "dispatch_internal"
+		"_in_" + to_string(_arity.in) +
+		"_out_" + to_string(_arity.out);
+}
+
 string IRNames::implicitConstructor(ContractDefinition const& _contract)
 {
 	return "constructor_" + _contract.name() + "_" + to_string(_contract.id());

libsolidity/codegen/ir/Common.h

@@ -22,17 +22,35 @@
 
 #include <libsolidity/ast/AST.h>
 
+#include <algorithm>
 #include <string>
 
 namespace solidity::frontend
 {
 
+/**
+ * Structure that describes arity and co-arity of a Yul function, i.e. the number of its inputs and outputs.
+ */
+struct YulArity
+{
+	explicit YulArity(size_t _in, size_t _out): in(_in), out(_out) {}
+
+	static YulArity fromType(FunctionType const& _functionType);
+
+	bool operator==(YulArity const& _other) const { return in == _other.in && out == _other.out; }
+	bool operator!=(YulArity const& _other) const { return !(*this == _other); }
+
+	size_t in;  /// Number of input parameters
+	size_t out; /// Number of output parameters
+};
+
 struct IRNames
 {
 	static std::string function(FunctionDefinition const& _function);
 	static std::string function(VariableDeclaration const& _varDecl);
 	static std::string creationObject(ContractDefinition const& _contract);
 	static std::string runtimeObject(ContractDefinition const& _contract);
+	static std::string internalDispatch(YulArity const& _arity);
 	static std::string implicitConstructor(ContractDefinition const& _contract);
 	static std::string constantValueFunction(VariableDeclaration const& _constant);
 	static std::string localVariable(VariableDeclaration const& _declaration);
@@ -45,3 +63,15 @@ struct IRNames
 };
 
 }
+
+// Overloading std::less() makes it possible to use YulArity as a map key. We could define operator<
+// instead but such an operator would be a bit ambiguous (e.g. YulArity{2, 2} would be be greater than
+// YulArity{1, 10} in lexicographical order but the latter has greater total number of inputs and outputs).
+template<>
+struct std::less<solidity::frontend::YulArity>
+{
+	bool operator() (solidity::frontend::YulArity const& _lhs, solidity::frontend::YulArity const& _rhs) const
+	{
+		return _lhs.in < _rhs.in || (_lhs.in == _rhs.in && _lhs.out < _rhs.out);
+	}
+};

libsolidity/codegen/ir/IRGenerationContext.cpp

@@ -121,9 +121,9 @@ string IRGenerationContext::newYulVariable()
 	return "_" + to_string(++m_varCounter);
 }
 
-string IRGenerationContext::internalDispatch(size_t _in, size_t _out)
+string IRGenerationContext::generateInternalDispatchFunction(YulArity const& _arity)
 {
-	string funName = "dispatch_internal_in_" + to_string(_in) + "_out_" + to_string(_out);
+	string funName = IRNames::internalDispatch(_arity);
 	return m_functions.createFunction(funName, [&]() {
 		Whiskers templ(R"(
 			function <functionName>(fun <comma> <in>) <arrow> <out> {
@@ -138,38 +138,33 @@ string IRGenerationContext::internalDispatch(size_t _in, size_t _out)
 			}
 		)");
 		templ("functionName", funName);
-		templ("comma", _in > 0 ? "," : "");
+		templ("comma", _arity.in > 0 ? "," : "");
-		YulUtilFunctions utils(m_evmVersion, m_revertStrings, m_functions);
+		templ("in", suffixedVariableNameList("in_", 0, _arity.in));
-		templ("in", suffixedVariableNameList("in_", 0, _in));
+		templ("arrow", _arity.out > 0 ? "->" : "");
-		templ("arrow", _out > 0 ? "->" : "");
+		templ("assignment_op", _arity.out > 0 ? ":=" : "");
-		templ("assignment_op", _out > 0 ? ":=" : "");
+		templ("out", suffixedVariableNameList("out_", 0, _arity.out));
-		templ("out", suffixedVariableNameList("out_", 0, _out));
 
-		// UNIMPLEMENTED: Internal library calls via pointers are not implemented yet.
+		vector<map<string, string>> cases;
-		// We're not generating code for internal library functions here even though it's possible
+		for (FunctionDefinition const* function: collectFunctionsOfArity(_arity))
-		// to call them via pointers. Right now such calls end up triggering the `default` case in
+		{
-		// the switch above.
+			solAssert(function, "");
-		vector<map<string, string>> functions;
+			solAssert(
-		for (auto const& contract: mostDerivedContract().annotation().linearizedBaseContracts)
+				YulArity::fromType(*TypeProvider::function(*function, FunctionType::Kind::Internal)) == _arity,
-			for (FunctionDefinition const* function: contract->definedFunctions())
+				"A single dispatch function can only handle functions of one arity"
-				if (
+			);
-					FunctionType const* functionType = TypeProvider::function(*function)->asCallableFunction(false);
+			solAssert(!function->isConstructor(), "");
-					!function->isConstructor() &&
+			// 0 is reserved for uninitialized function pointers
-					TupleType(functionType->parameterTypes()).sizeOnStack() == _in &&
+			solAssert(function->id() != 0, "Unexpected function ID: 0");
-					TupleType(functionType->returnParameterTypes()).sizeOnStack() == _out
-				)
-				{
-					// 0 is reserved for uninitialized function pointers
-					solAssert(function->id() != 0, "Unexpected function ID: 0");
 
-					functions.emplace_back(map<string, string> {
+			cases.emplace_back(map<string, string>{
-						{ "funID", to_string(function->id()) },
+				{"funID", to_string(function->id())},
-						{ "name", IRNames::function(*function)}
+				{"name", IRNames::function(*function)}
-					});
+			});
 
-					enqueueFunctionForCodeGeneration(*function);
+			enqueueFunctionForCodeGeneration(*function);
-				}
+		}
-		templ("cases", move(functions));
+
+		templ("cases", move(cases));
 		return templ.render();
 	});
 }
@@ -189,3 +184,20 @@ std::string IRGenerationContext::revertReasonIfDebug(std::string const& _message
 	return YulUtilFunctions::revertReasonIfDebug(m_revertStrings, _message);
 }
 
+set<FunctionDefinition const*> IRGenerationContext::collectFunctionsOfArity(YulArity const& _arity)
+{
+	// UNIMPLEMENTED: Internal library calls via pointers are not implemented yet.
+	// We're not returning any internal library functions here even though it's possible
+	// to call them via pointers. Right now such calls end will up triggering the `default` case in
+	// the switch in the generated dispatch function.
+	set<FunctionDefinition const*> functions;
+	for (auto const& contract: mostDerivedContract().annotation().linearizedBaseContracts)
+		for (FunctionDefinition const* function: contract->definedFunctions())
+			if (
+				!function->isConstructor() &&
+				YulArity::fromType(*TypeProvider::function(*function, FunctionType::Kind::Internal)) == _arity
+			)
+				functions.insert(function);
+
+	return functions;
+}

libsolidity/codegen/ir/IRGenerationContext.h

@@ -102,7 +102,7 @@ public:
 
 	std::string newYulVariable();
 
-	std::string internalDispatch(size_t _in, size_t _out);
+	std::string generateInternalDispatchFunction(YulArity const& _arity);
 
 	/// @returns a new copy of the utility function generator (but using the same function set).
 	YulUtilFunctions utils();
@@ -120,6 +120,8 @@ public:
 	std::set<ContractDefinition const*, ASTNode::CompareByID>& subObjectsCreated() { return m_subObjects; }
 
 private:
+	std::set<FunctionDefinition const*> collectFunctionsOfArity(YulArity const& _arity);
+
 	langutil::EVMVersion m_evmVersion;
 	RevertStrings m_revertStrings;
 	OptimiserSettings m_optimiserSettings;

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -692,16 +692,16 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 				joinHumanReadable(args) <<
 				")\n";
 		else
+		{
+			YulArity arity = YulArity::fromType(*functionType);
 			define(_functionCall) <<
-				// NOTE: internalDispatch() takes care of adding the function to function generation queue
+				// NOTE: generateInternalDispatchFunction() takes care of adding the function to function generation queue
-				m_context.internalDispatch(
+				m_context.generateInternalDispatchFunction(arity) <<
-					TupleType(functionType->parameterTypes()).sizeOnStack(),
-					TupleType(functionType->returnParameterTypes()).sizeOnStack()
-				) <<
 				"(" <<
 				IRVariable(_functionCall.expression()).part("functionIdentifier").name() <<
 				joinHumanReadablePrefixed(args) <<
 				")\n";
+		}
 		break;
 	}
 	case FunctionType::Kind::External:

libsolidity/formal/BMC.cpp

@@ -17,10 +17,11 @@
 
 #include <libsolidity/formal/BMC.h>
 
-#include <libsolidity/formal/SMTPortfolio.h>
 #include <libsolidity/formal/SymbolicState.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
+#include <libsmtutil/SMTPortfolio.h>
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::util;
@@ -32,10 +33,10 @@ BMC::BMC(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
-	smt::SMTSolverChoice _enabledSolvers
+	smtutil::SMTSolverChoice _enabledSolvers
 ):
 	SMTEncoder(_context),
-	m_interface(make_unique<smt::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers)),
+	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers)),
 	m_outerErrorReporter(_errorReporter)
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
@@ -132,7 +133,7 @@ void BMC::endVisit(ContractDefinition const& _contract)
 	{
 		inlineConstructorHierarchy(_contract);
 		/// Check targets created by state variable initialization.
-		smt::Expression constraints = m_context.assertions();
+		smtutil::Expression constraints = m_context.assertions();
 		checkVerificationTargets(constraints);
 		m_verificationTargets.clear();
 	}
@@ -166,7 +167,7 @@ void BMC::endVisit(FunctionDefinition const& _function)
 {
 	if (isRootFunction())
 	{
-		smt::Expression constraints = m_context.assertions();
+		smtutil::Expression constraints = m_context.assertions();
 		checkVerificationTargets(constraints);
 		m_verificationTargets.clear();
 	}
@@ -293,7 +294,7 @@ bool BMC::visit(ForStatement const& _node)
 	if (_node.condition())
 		_node.condition()->accept(*this);
 
-	auto forCondition = _node.condition() ? expr(*_node.condition()) : smt::Expression(true);
+	auto forCondition = _node.condition() ? expr(*_node.condition()) : smtutil::Expression(true);
 	mergeVariables(touchedVars, forCondition, indicesAfterLoop, copyVariableIndices());
 
 	m_loopExecutionHappened = true;
@@ -380,7 +381,7 @@ void BMC::endVisit(FunctionCall const& _funCall)
 		SMTEncoder::endVisit(_funCall);
 		auto value = _funCall.arguments().front();
 		solAssert(value, "");
-		smt::Expression thisBalance = m_context.state().balance();
+		smtutil::Expression thisBalance = m_context.state().balance();
 
 		addVerificationTarget(
 			VerificationTarget::Type::Balance,
@@ -452,7 +453,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 
 void BMC::abstractFunctionCall(FunctionCall const& _funCall)
 {
-	vector<smt::Expression> smtArguments;
+	vector<smtutil::Expression> smtArguments;
 	for (auto const& arg: _funCall.arguments())
 		smtArguments.push_back(expr(*arg));
 	defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments));
@@ -479,10 +480,10 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 	}
 }
 
-pair<smt::Expression, smt::Expression> BMC::arithmeticOperation(
+pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
 	Token _op,
-	smt::Expression const& _left,
+	smtutil::Expression const& _left,
-	smt::Expression const& _right,
+	smtutil::Expression const& _right,
 	TypePointer const& _commonType,
 	Expression const& _expression
 )
@@ -515,9 +516,9 @@ void BMC::reset()
 	m_loopExecutionHappened = false;
 }
 
-pair<vector<smt::Expression>, vector<string>> BMC::modelExpressions()
+pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
 {
-	vector<smt::Expression> expressionsToEvaluate;
+	vector<smtutil::Expression> expressionsToEvaluate;
 	vector<string> expressionNames;
 	for (auto const& var: m_context.variables())
 		if (var.first->type()->isValueType())
@@ -530,7 +531,7 @@ pair<vector<smt::Expression>, vector<string>> BMC::modelExpressions()
 		auto const& type = var.second->type();
 		if (
 			type->isValueType() &&
-			smt::smtKind(type->category()) != smt::Kind::Function
+			smt::smtKind(type->category()) != smtutil::Kind::Function
 		)
 		{
 			expressionsToEvaluate.emplace_back(var.second->currentValue());
@@ -549,13 +550,13 @@ pair<vector<smt::Expression>, vector<string>> BMC::modelExpressions()
 
 /// Verification targets.
 
-void BMC::checkVerificationTargets(smt::Expression const& _constraints)
+void BMC::checkVerificationTargets(smtutil::Expression const& _constraints)
 {
 	for (auto& target: m_verificationTargets)
 		checkVerificationTarget(target, _constraints);
 }
 
-void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints)
+void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
 {
 	switch (_target.type)
 	{
@@ -596,7 +597,7 @@ void BMC::checkConstantCondition(BMCVerificationTarget& _target)
 	);
 }
 
-void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints)
+void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
 {
 	solAssert(
 		_target.type == VerificationTarget::Type::Underflow ||
@@ -618,7 +619,7 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const&
 	);
 }
 
-void BMC::checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints)
+void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
 {
 	solAssert(
 		_target.type == VerificationTarget::Type::Overflow ||
@@ -688,7 +689,7 @@ void BMC::checkAssert(BMCVerificationTarget& _target)
 
 void BMC::addVerificationTarget(
 	VerificationTarget::Type _type,
-	smt::Expression const& _value,
+	smtutil::Expression const& _value,
 	Expression const* _expression
 )
 {
@@ -711,21 +712,21 @@ void BMC::addVerificationTarget(
 /// Solving.
 
 void BMC::checkCondition(
-	smt::Expression _condition,
+	smtutil::Expression _condition,
 	vector<SMTEncoder::CallStackEntry> const& _callStack,
-	pair<vector<smt::Expression>, vector<string>> const& _modelExpressions,
+	pair<vector<smtutil::Expression>, vector<string>> const& _modelExpressions,
 	SourceLocation const& _location,
 	ErrorId _errorHappens,
 	ErrorId _errorMightHappen,
 	string const& _description,
 	string const& _additionalValueName,
-	smt::Expression const* _additionalValue
+	smtutil::Expression const* _additionalValue
 )
 {
 	m_interface->push();
 	m_interface->addAssertion(_condition);
 
-	vector<smt::Expression> expressionsToEvaluate;
+	vector<smtutil::Expression> expressionsToEvaluate;
 	vector<string> expressionNames;
 	tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
 	if (_callStack.size())
@@ -734,7 +735,7 @@ void BMC::checkCondition(
 			expressionsToEvaluate.emplace_back(*_additionalValue);
 			expressionNames.push_back(_additionalValueName);
 		}
-	smt::CheckResult result;
+	smtutil::CheckResult result;
 	vector<string> values;
 	tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);
 
@@ -755,7 +756,7 @@ void BMC::checkCondition(
 
 	switch (result)
 	{
-	case smt::CheckResult::SATISFIABLE:
+	case smtutil::CheckResult::SATISFIABLE:
 	{
 		std::ostringstream message;
 		message << _description << " happens here";
@@ -787,15 +788,15 @@ void BMC::checkCondition(
 		}
 		break;
 	}
-	case smt::CheckResult::UNSATISFIABLE:
+	case smtutil::CheckResult::UNSATISFIABLE:
 		break;
-	case smt::CheckResult::UNKNOWN:
+	case smtutil::CheckResult::UNKNOWN:
 		m_errorReporter.warning(_errorMightHappen, _location, _description + " might happen here.", secondaryLocation);
 		break;
-	case smt::CheckResult::CONFLICTING:
+	case smtutil::CheckResult::CONFLICTING:
 		m_errorReporter.warning(1584_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
 		break;
-	case smt::CheckResult::ERROR:
+	case smtutil::CheckResult::ERROR:
 		m_errorReporter.warning(1823_error, _location, "Error trying to invoke SMT solver.");
 		break;
 	}
@@ -805,8 +806,8 @@ void BMC::checkCondition(
 
 void BMC::checkBooleanNotConstant(
 	Expression const& _condition,
-	smt::Expression const& _constraints,
+	smtutil::Expression const& _constraints,
-	smt::Expression const& _value,
+	smtutil::Expression const& _value,
 	vector<SMTEncoder::CallStackEntry> const& _callStack
 )
 {
@@ -824,32 +825,32 @@ void BMC::checkBooleanNotConstant(
 	auto negatedResult = checkSatisfiable();
 	m_interface->pop();
 
-	if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
+	if (positiveResult == smtutil::CheckResult::ERROR || negatedResult == smtutil::CheckResult::ERROR)
 		m_errorReporter.warning(8592_error, _condition.location(), "Error trying to invoke SMT solver.");
-	else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING)
+	else if (positiveResult == smtutil::CheckResult::CONFLICTING || negatedResult == smtutil::CheckResult::CONFLICTING)
 		m_errorReporter.warning(3356_error, _condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound.");
-	else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE)
+	else if (positiveResult == smtutil::CheckResult::SATISFIABLE && negatedResult == smtutil::CheckResult::SATISFIABLE)
 	{
 		// everything fine.
 	}
-	else if (positiveResult == smt::CheckResult::UNKNOWN || negatedResult == smt::CheckResult::UNKNOWN)
+	else if (positiveResult == smtutil::CheckResult::UNKNOWN || negatedResult == smtutil::CheckResult::UNKNOWN)
 	{
 		// can't do anything.
 	}
-	else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
+	else if (positiveResult == smtutil::CheckResult::UNSATISFIABLE && negatedResult == smtutil::CheckResult::UNSATISFIABLE)
 		m_errorReporter.warning(2512_error, _condition.location(), "Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
 	else
 	{
 		string description;
-		if (positiveResult == smt::CheckResult::SATISFIABLE)
+		if (positiveResult == smtutil::CheckResult::SATISFIABLE)
 		{
-			solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, "");
+			solAssert(negatedResult == smtutil::CheckResult::UNSATISFIABLE, "");
 			description = "Condition is always true.";
 		}
 		else
 		{
-			solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, "");
+			solAssert(positiveResult == smtutil::CheckResult::UNSATISFIABLE, "");
-			solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
+			solAssert(negatedResult == smtutil::CheckResult::SATISFIABLE, "");
 			description = "Condition is always false.";
 		}
 		m_errorReporter.warning(
@@ -861,22 +862,22 @@ void BMC::checkBooleanNotConstant(
 	}
 }
 
-pair<smt::CheckResult, vector<string>>
+pair<smtutil::CheckResult, vector<string>>
-BMC::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
+BMC::checkSatisfiableAndGenerateModel(vector<smtutil::Expression> const& _expressionsToEvaluate)
 {
-	smt::CheckResult result;
+	smtutil::CheckResult result;
 	vector<string> values;
 	try
 	{
 		tie(result, values) = m_interface->check(_expressionsToEvaluate);
 	}
-	catch (smt::SolverError const& _e)
+	catch (smtutil::SolverError const& _e)
 	{
 		string description("Error querying SMT solver");
 		if (_e.comment())
 			description += ": " + *_e.comment();
 		m_errorReporter.warning(8140_error, description);
-		result = smt::CheckResult::ERROR;
+		result = smtutil::CheckResult::ERROR;
 	}
 
 	for (string& value: values)
@@ -892,7 +893,7 @@ BMC::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _expression
 	return make_pair(result, values);
 }
 
-smt::CheckResult BMC::checkSatisfiable()
+smtutil::CheckResult BMC::checkSatisfiable()
 {
 	return checkSatisfiableAndGenerateModel({}).first;
 }

libsolidity/formal/BMC.h

@@ -30,9 +30,10 @@
 
 #include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SMTEncoder.h>
-#include <libsolidity/formal/SolverInterface.h>
 
 #include <libsolidity/interface/ReadFile.h>
+
+#include <libsmtutil/SolverInterface.h>
 #include <liblangutil/ErrorReporter.h>
 
 #include <set>
@@ -59,7 +60,7 @@ public:
 		langutil::ErrorReporter& _errorReporter,
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		smt::SMTSolverChoice _enabledSolvers
+		smtutil::SMTSolverChoice _enabledSolvers
 	);
 
 	void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions);
@@ -102,10 +103,10 @@ private:
 	void internalOrExternalFunctionCall(FunctionCall const& _funCall);
 
 	/// Creates underflow/overflow verification targets.
-	std::pair<smt::Expression, smt::Expression> arithmeticOperation(
+	std::pair<smtutil::Expression, smtutil::Expression> arithmeticOperation(
 		Token _op,
-		smt::Expression const& _left,
+		smtutil::Expression const& _left,
-		smt::Expression const& _right,
+		smtutil::Expression const& _right,
 		TypePointer const& _commonType,
 		Expression const& _expression
 	) override;
@@ -113,7 +114,7 @@ private:
 	void resetStorageReferences();
 	void reset();
 
-	std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions();
+	std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> modelExpressions();
 	//@}
 
 	/// Verification targets.
@@ -122,20 +123,20 @@ private:
 	{
 		Expression const* expression;
 		std::vector<CallStackEntry> callStack;
-		std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions;
+		std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> modelExpressions;
 	};
 
-	void checkVerificationTargets(smt::Expression const& _constraints);
+	void checkVerificationTargets(smtutil::Expression const& _constraints);
-	void checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true));
+	void checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expression const& _constraints = smtutil::Expression(true));
 	void checkConstantCondition(BMCVerificationTarget& _target);
-	void checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints);
+	void checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints);
-	void checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints);
+	void checkOverflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints);
 	void checkDivByZero(BMCVerificationTarget& _target);
 	void checkBalance(BMCVerificationTarget& _target);
 	void checkAssert(BMCVerificationTarget& _target);
 	void addVerificationTarget(
 		VerificationTarget::Type _type,
-		smt::Expression const& _value,
+		smtutil::Expression const& _value,
 		Expression const* _expression
 	);
 	//@}
@@ -144,31 +145,31 @@ private:
 	//@{
 	/// Check that a condition can be satisfied.
 	void checkCondition(
-		smt::Expression _condition,
+		smtutil::Expression _condition,
 		std::vector<CallStackEntry> const& _callStack,
-		std::pair<std::vector<smt::Expression>, std::vector<std::string>> const& _modelExpressions,
+		std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> const& _modelExpressions,
 		langutil::SourceLocation const& _location,
 		langutil::ErrorId _errorHappens,
 		langutil::ErrorId _errorMightHappen,
 		std::string const& _description,
 		std::string const& _additionalValueName = "",
-		smt::Expression const* _additionalValue = nullptr
+		smtutil::Expression const* _additionalValue = nullptr
 	);
 	/// Checks that a boolean condition is not constant. Do not warn if the expression
 	/// is a literal constant.
 	void checkBooleanNotConstant(
 		Expression const& _condition,
-		smt::Expression const& _constraints,
+		smtutil::Expression const& _constraints,
-		smt::Expression const& _value,
+		smtutil::Expression const& _value,
 		std::vector<CallStackEntry> const& _callStack
 	);
-	std::pair<smt::CheckResult, std::vector<std::string>>
+	std::pair<smtutil::CheckResult, std::vector<std::string>>
-	checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
+	checkSatisfiableAndGenerateModel(std::vector<smtutil::Expression> const& _expressionsToEvaluate);
 
-	smt::CheckResult checkSatisfiable();
+	smtutil::CheckResult checkSatisfiable();
 	//@}
 
-	std::unique_ptr<smt::SolverInterface> m_interface;
+	std::unique_ptr<smtutil::SolverInterface> m_interface;
 
 	/// Flags used for better warning messages.
 	bool m_loopExecutionHappened = false;

libsolidity/formal/CHC.cpp

@@ -17,22 +17,22 @@
 
 #include <libsolidity/formal/CHC.h>
 
-#include <libsolidity/formal/CHCSmtLib2Interface.h>
-
 #ifdef HAVE_Z3
-#include <libsolidity/formal/Z3CHCInterface.h>
+#include <libsmtutil/Z3CHCInterface.h>
 #endif
 
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <libsolidity/ast/TypeProvider.h>
 
+#include <libsmtutil/CHCSmtLib2Interface.h>
 #include <libsolutil/Algorithms.h>
 
 using namespace std;
 using namespace solidity;
 using namespace solidity::util;
 using namespace solidity::langutil;
+using namespace solidity::smtutil;
 using namespace solidity::frontend;
 
 CHC::CHC(
@@ -40,7 +40,7 @@ CHC::CHC(
 	ErrorReporter& _errorReporter,
 	map<util::h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
-	[[maybe_unused]] smt::SMTSolverChoice _enabledSolvers
+	[[maybe_unused]] smtutil::SMTSolverChoice _enabledSolvers
 ):
 	SMTEncoder(_context),
 	m_outerErrorReporter(_errorReporter),
@@ -48,10 +48,10 @@ CHC::CHC(
 {
 #ifdef HAVE_Z3
 	if (_enabledSolvers.z3)
-		m_interface = make_unique<smt::Z3CHCInterface>();
+		m_interface = make_unique<smtutil::Z3CHCInterface>();
 #endif
 	if (!m_interface)
-		m_interface = make_unique<smt::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback);
+		m_interface = make_unique<smtutil::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback);
 }
 
 void CHC::analyze(SourceUnit const& _source)
@@ -63,14 +63,14 @@ void CHC::analyze(SourceUnit const& _source)
 	usesZ3 = m_enabledSolvers.z3;
 	if (usesZ3)
 	{
-		auto z3Interface = dynamic_cast<smt::Z3CHCInterface const*>(m_interface.get());
+		auto z3Interface = dynamic_cast<smtutil::Z3CHCInterface const*>(m_interface.get());
 		solAssert(z3Interface, "");
 		m_context.setSolver(z3Interface->z3Interface());
 	}
 #endif
 	if (!usesZ3)
 	{
-		auto smtlib2Interface = dynamic_cast<smt::CHCSmtLib2Interface const*>(m_interface.get());
+		auto smtlib2Interface = dynamic_cast<smtutil::CHCSmtLib2Interface const*>(m_interface.get());
 		solAssert(smtlib2Interface, "");
 		m_context.setSolver(smtlib2Interface->smtlib2Interface());
 	}
@@ -80,9 +80,9 @@ void CHC::analyze(SourceUnit const& _source)
 
 	resetSourceAnalysis();
 
-	auto genesisSort = make_shared<smt::FunctionSort>(
+	auto genesisSort = make_shared<smtutil::FunctionSort>(
-		vector<smt::SortPointer>(),
+		vector<smtutil::SortPointer>(),
-		smt::SortProvider::boolSort
+		smtutil::SortProvider::boolSort
 	);
 	m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis");
 	addRule(genesis(), "genesis");
@@ -108,7 +108,7 @@ void CHC::analyze(SourceUnit const& _source)
 				auto [result, model] = query(error(), assertion->location());
 				// This should be fine but it's a bug in the old compiler
 				(void)model;
-				if (result == smt::CheckResult::UNSATISFIABLE)
+				if (result == smtutil::CheckResult::UNSATISFIABLE)
 					m_safeAssertions.insert(assertion);
 			}
 		}
@@ -120,10 +120,10 @@ void CHC::analyze(SourceUnit const& _source)
 			auto [result, model] = query(error(), scope->location());
 			// This should be fine but it's a bug in the old compiler
 			(void)model;
-			if (result != smt::CheckResult::UNSATISFIABLE)
+			if (result != smtutil::CheckResult::UNSATISFIABLE)
 			{
 				string msg = "Empty array \"pop\" ";
-				if (result == smt::CheckResult::SATISFIABLE)
+				if (result == smtutil::CheckResult::SATISFIABLE)
 					msg += "detected here.";
 				else
 					msg += "might happen here.";
@@ -142,7 +142,7 @@ void CHC::analyze(SourceUnit const& _source)
 
 vector<string> CHC::unhandledQueries() const
 {
-	if (auto smtlib2 = dynamic_cast<smt::CHCSmtLib2Interface const*>(m_interface.get()))
+	if (auto smtlib2 = dynamic_cast<smtutil::CHCSmtLib2Interface const*>(m_interface.get()))
 		return smtlib2->unhandledQueries();
 
 	return {};
@@ -182,14 +182,14 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	else
 		inlineConstructorHierarchy(_contract);
 
-	auto summary = predicate(*m_constructorSummaryPredicate, vector<smt::Expression>{m_error.currentValue()} + currentStateVariables());
+	auto summary = predicate(*m_constructorSummaryPredicate, vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables());
 	connectBlocks(m_currentBlock, summary);
 
 	clearIndices(m_currentContract, nullptr);
-	auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
+	auto stateExprs = vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
 	setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs);
 
-	addAssertVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue());
+	addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), m_error.currentValue());
 	connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0);
 
 	SMTEncoder::endVisit(_contract);
@@ -265,10 +265,10 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		{
 			string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
 			auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix);
-			connectBlocks(m_currentBlock, predicate(*constructorExit, vector<smt::Expression>{m_error.currentValue()} + currentStateVariables()));
+			connectBlocks(m_currentBlock, predicate(*constructorExit, vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables()));
 
 			clearIndices(m_currentContract, m_currentFunction);
-			auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
+			auto stateExprs = vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
 			setCurrentBlock(*constructorExit, &stateExprs);
 		}
 		else
@@ -417,7 +417,7 @@ bool CHC::visit(ForStatement const& _for)
 	connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
 	setCurrentBlock(*loopHeaderBlock);
 
-	auto condition = smt::Expression(true);
+	auto condition = smtutil::Expression(true);
 	if (auto forCondition = _for.condition())
 	{
 		forCondition->accept(*this);
@@ -656,7 +656,7 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
 
 void CHC::setCurrentBlock(
 	smt::SymbolicFunctionVariable const& _block,
-	vector<smt::Expression> const* _arguments
+	vector<smtutil::Expression> const* _arguments
 )
 {
 	if (m_context.solverStackHeigh() > 0)
@@ -670,7 +670,7 @@ void CHC::setCurrentBlock(
 		m_currentBlock = predicate(_block);
 }
 
-set<Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTNode const* _txRoot)
+set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTNode const* _txRoot)
 {
 	set<Expression const*, IdCompare> assertions;
 	solidity::util::BreadthFirstSearch<ASTNode const*>{{_txRoot}}.run([&](auto const* function, auto&& _addChild) {
@@ -690,7 +690,7 @@ vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPriva
 	);
 }
 
-vector<smt::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
+vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
 {
 	return applyMap(
 		stateVariablesIncludingInheritedAndPrivate(_contract),
@@ -698,35 +698,35 @@ vector<smt::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
 	);
 }
 
-smt::SortPointer CHC::constructorSort()
+smtutil::SortPointer CHC::constructorSort()
 {
-	return make_shared<smt::FunctionSort>(
+	return make_shared<smtutil::FunctionSort>(
-		vector<smt::SortPointer>{smt::SortProvider::intSort} + m_stateSorts,
+		vector<smtutil::SortPointer>{smtutil::SortProvider::intSort} + m_stateSorts,
-		smt::SortProvider::boolSort
+		smtutil::SortProvider::boolSort
 	);
 }
 
-smt::SortPointer CHC::interfaceSort()
+smtutil::SortPointer CHC::interfaceSort()
 {
-	return make_shared<smt::FunctionSort>(
+	return make_shared<smtutil::FunctionSort>(
 		m_stateSorts,
-		smt::SortProvider::boolSort
+		smtutil::SortProvider::boolSort
 	);
 }
 
-smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
+smtutil::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
 {
-	return make_shared<smt::FunctionSort>(
+	return make_shared<smtutil::FunctionSort>(
 		stateSorts(_contract),
-		smt::SortProvider::boolSort
+		smtutil::SortProvider::boolSort
 	);
 }
 
-smt::SortPointer CHC::arity0FunctionSort()
+smtutil::SortPointer CHC::arity0FunctionSort()
 {
-	return make_shared<smt::FunctionSort>(
+	return make_shared<smtutil::FunctionSort>(
-		vector<smt::SortPointer>(),
+		vector<smtutil::SortPointer>(),
-		smt::SortProvider::boolSort
+		smtutil::SortProvider::boolSort
 	);
 }
 
@@ -741,33 +741,33 @@ smt::SortPointer CHC::arity0FunctionSort()
 ///   - Current input variables
 ///    At the beginning of the function these must equal set 1
 /// - 1 set of output variables
-smt::SortPointer CHC::sort(FunctionDefinition const& _function)
+smtutil::SortPointer CHC::sort(FunctionDefinition const& _function)
 {
 	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
 	auto inputSorts = applyMap(_function.parameters(), smtSort);
 	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
-	return make_shared<smt::FunctionSort>(
+	return make_shared<smtutil::FunctionSort>(
-		vector<smt::SortPointer>{smt::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
+		vector<smtutil::SortPointer>{smtutil::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
-		smt::SortProvider::boolSort
+		smtutil::SortProvider::boolSort
 	);
 }
 
-smt::SortPointer CHC::sort(ASTNode const* _node)
+smtutil::SortPointer CHC::sort(ASTNode const* _node)
 {
 	if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
 		return sort(*funDef);
 
-	auto fSort = dynamic_pointer_cast<smt::FunctionSort>(sort(*m_currentFunction));
+	auto fSort = dynamic_pointer_cast<smtutil::FunctionSort>(sort(*m_currentFunction));
 	solAssert(fSort, "");
 
 	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
-	return make_shared<smt::FunctionSort>(
+	return make_shared<smtutil::FunctionSort>(
 		fSort->domain + applyMap(m_currentFunction->localVariables(), smtSort),
-		smt::SortProvider::boolSort
+		smtutil::SortProvider::boolSort
 	);
 }
 
-smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
+smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
 	auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
 	auto sorts = stateSorts(_contract);
@@ -775,13 +775,13 @@ smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractD
 	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
 	auto inputSorts = applyMap(_function.parameters(), smtSort);
 	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
-	return make_shared<smt::FunctionSort>(
+	return make_shared<smtutil::FunctionSort>(
-		vector<smt::SortPointer>{smt::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts,
+		vector<smtutil::SortPointer>{smtutil::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts,
-		smt::SortProvider::boolSort
+		smtutil::SortProvider::boolSort
 	);
 }
 
-unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name)
+unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smtutil::SortPointer _sort, string const& _name)
 {
 	auto block = make_unique<smt::SymbolicFunctionVariable>(
 		_sort,
@@ -808,7 +808,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 			}
 }
 
-smt::Expression CHC::interface()
+smtutil::Expression CHC::interface()
 {
 	auto paramExprs = applyMap(
 		m_stateVariables,
@@ -817,32 +817,32 @@ smt::Expression CHC::interface()
 	return (*m_interfaces.at(m_currentContract))(paramExprs);
 }
 
-smt::Expression CHC::interface(ContractDefinition const& _contract)
+smtutil::Expression CHC::interface(ContractDefinition const& _contract)
 {
 	return (*m_interfaces.at(&_contract))(stateVariablesAtIndex(0, _contract));
 }
 
-smt::Expression CHC::error()
+smtutil::Expression CHC::error()
 {
 	return (*m_errorPredicate)({});
 }
 
-smt::Expression CHC::error(unsigned _idx)
+smtutil::Expression CHC::error(unsigned _idx)
 {
 	return m_errorPredicate->functionValueAtIndex(_idx)({});
 }
 
-smt::Expression CHC::summary(ContractDefinition const&)
+smtutil::Expression CHC::summary(ContractDefinition const&)
 {
 	return (*m_constructorSummaryPredicate)(
-		vector<smt::Expression>{m_error.currentValue()} +
+		vector<smtutil::Expression>{m_error.currentValue()} +
 		currentStateVariables()
 	);
 }
 
-smt::Expression CHC::summary(FunctionDefinition const& _function)
+smtutil::Expression CHC::summary(FunctionDefinition const& _function)
 {
-	vector<smt::Expression> args{m_error.currentValue()};
+	vector<smtutil::Expression> args{m_error.currentValue()};
 	auto contract = _function.annotation().contract;
 	args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables();
 	args += applyMap(_function.parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); });
@@ -877,27 +877,27 @@ void CHC::createErrorBlock()
 	m_interface->registerRelation(m_errorPredicate->currentFunctionValue());
 }
 
-void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints)
+void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints)
 {
-	smt::Expression edge = smt::Expression::implies(
+	smtutil::Expression edge = smtutil::Expression::implies(
 		_from && m_context.assertions() && _constraints,
 		_to
 	);
 	addRule(edge, _from.name + "_to_" + _to.name);
 }
 
-vector<smt::Expression> CHC::initialStateVariables()
+vector<smtutil::Expression> CHC::initialStateVariables()
 {
 	return stateVariablesAtIndex(0);
 }
 
-vector<smt::Expression> CHC::stateVariablesAtIndex(int _index)
+vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index)
 {
 	solAssert(m_currentContract, "");
 	return applyMap(m_stateVariables, [&](auto _var) { return valueAtIndex(*_var, _index); });
 }
 
-vector<smt::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract)
+vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract)
 {
 	return applyMap(
 		stateVariablesIncludingInheritedAndPrivate(_contract),
@@ -905,23 +905,23 @@ vector<smt::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinitio
 	);
 }
 
-vector<smt::Expression> CHC::currentStateVariables()
+vector<smtutil::Expression> CHC::currentStateVariables()
 {
 	solAssert(m_currentContract, "");
 	return applyMap(m_stateVariables, [this](auto _var) { return currentValue(*_var); });
 }
 
-vector<smt::Expression> CHC::currentFunctionVariables()
+vector<smtutil::Expression> CHC::currentFunctionVariables()
 {
-	vector<smt::Expression> initInputExprs;
+	vector<smtutil::Expression> initInputExprs;
-	vector<smt::Expression> mutableInputExprs;
+	vector<smtutil::Expression> mutableInputExprs;
 	for (auto const& var: m_currentFunction->parameters())
 	{
 		initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0));
 		mutableInputExprs.push_back(m_context.variable(*var)->currentValue());
 	}
 	auto returnExprs = applyMap(m_currentFunction->returnParameters(), [this](auto _var) { return currentValue(*_var); });
-	return vector<smt::Expression>{m_error.currentValue()} +
+	return vector<smtutil::Expression>{m_error.currentValue()} +
 		initialStateVariables() +
 		initInputExprs +
 		currentStateVariables() +
@@ -929,7 +929,7 @@ vector<smt::Expression> CHC::currentFunctionVariables()
 		returnExprs;
 }
 
-vector<smt::Expression> CHC::currentBlockVariables()
+vector<smtutil::Expression> CHC::currentBlockVariables()
 {
 	if (m_currentFunction)
 		return currentFunctionVariables() + applyMap(m_currentFunction->localVariables(), [this](auto _var) { return currentValue(*_var); });
@@ -954,27 +954,27 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr
 	return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id());
 }
 
-smt::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block)
+smtutil::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block)
 {
 	return _block(currentBlockVariables());
 }
 
-smt::Expression CHC::predicate(
+smtutil::Expression CHC::predicate(
 	smt::SymbolicFunctionVariable const& _block,
-	vector<smt::Expression> const& _arguments
+	vector<smtutil::Expression> const& _arguments
 )
 {
 	return _block(_arguments);
 }
 
-smt::Expression CHC::predicate(FunctionCall const& _funCall)
+smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 {
 	auto const* function = functionCallToDefinition(_funCall);
 	if (!function)
-		return smt::Expression(true);
+		return smtutil::Expression(true);
 
 	m_error.increaseIndex();
-	vector<smt::Expression> args{m_error.currentValue()};
+	vector<smtutil::Expression> args{m_error.currentValue()};
 	auto const* contract = function->annotation().contract;
 
 	args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : currentStateVariables();
@@ -998,28 +998,28 @@ smt::Expression CHC::predicate(FunctionCall const& _funCall)
 	return (*m_summaries.at(m_currentContract).at(function))(args);
 }
 
-void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
+void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName)
 {
 	m_interface->addRule(_rule, _ruleName);
 }
 
-pair<smt::CheckResult, vector<string>> CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)
+pair<smtutil::CheckResult, vector<string>> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location)
 {
-	smt::CheckResult result;
+	smtutil::CheckResult result;
 	vector<string> values;
 	tie(result, values) = m_interface->query(_query);
 	switch (result)
 	{
-	case smt::CheckResult::SATISFIABLE:
+	case smtutil::CheckResult::SATISFIABLE:
 		break;
-	case smt::CheckResult::UNSATISFIABLE:
+	case smtutil::CheckResult::UNSATISFIABLE:
 		break;
-	case smt::CheckResult::UNKNOWN:
+	case smtutil::CheckResult::UNKNOWN:
 		break;
-	case smt::CheckResult::CONFLICTING:
+	case smtutil::CheckResult::CONFLICTING:
 		m_outerErrorReporter.warning(1988_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
 		break;
-	case smt::CheckResult::ERROR:
+	case smtutil::CheckResult::ERROR:
 		m_outerErrorReporter.warning(1218_error, _location, "Error trying to invoke SMT solver.");
 		break;
 	}
@@ -1029,26 +1029,26 @@ pair<smt::CheckResult, vector<string>> CHC::query(smt::Expression const& _query,
 void CHC::addVerificationTarget(
 	ASTNode const* _scope,
 	VerificationTarget::Type _type,
-	smt::Expression _from,
+	smtutil::Expression _from,
-	smt::Expression _constraints,
+	smtutil::Expression _constraints,
-	smt::Expression _errorId
+	smtutil::Expression _errorId
 )
 {
 	m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
 }
 
-void CHC::addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId)
+void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId)
 {
 	addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId);
 }
 
-void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId)
+void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expression _errorId)
 {
 	solAssert(m_currentContract, "");
 	solAssert(m_currentFunction, "");
 
 	if (m_currentFunction->isConstructor())
-		addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smt::Expression(true), _errorId);
+		addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smtutil::Expression(true), _errorId);
 	else
 	{
 		auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables());

libsolidity/formal/CHC.h

@@ -32,10 +32,10 @@
 
 #include <libsolidity/formal/SMTEncoder.h>
 
-#include <libsolidity/formal/CHCSolverInterface.h>
-
 #include <libsolidity/interface/ReadFile.h>
 
+#include <libsmtutil/CHCSolverInterface.h>
+
 #include <set>
 
 namespace solidity::frontend
@@ -49,7 +49,7 @@ public:
 		langutil::ErrorReporter& _errorReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		smt::SMTSolverChoice _enabledSolvers
+		smtutil::SMTSolverChoice _enabledSolvers
 	);
 
 	void analyze(SourceUnit const& _sources);
@@ -96,43 +96,43 @@ private:
 	void eraseKnowledge();
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
 	bool shouldVisit(FunctionDefinition const& _function) const;
-	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const* _arguments = nullptr);
+	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
 	std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
 	//@}
 
 	/// Sort helpers.
 	//@{
-	static std::vector<smt::SortPointer> stateSorts(ContractDefinition const& _contract);
+	static std::vector<smtutil::SortPointer> stateSorts(ContractDefinition const& _contract);
-	smt::SortPointer constructorSort();
+	smtutil::SortPointer constructorSort();
-	smt::SortPointer interfaceSort();
+	smtutil::SortPointer interfaceSort();
-	static smt::SortPointer interfaceSort(ContractDefinition const& _const);
+	static smtutil::SortPointer interfaceSort(ContractDefinition const& _const);
-	smt::SortPointer arity0FunctionSort();
+	smtutil::SortPointer arity0FunctionSort();
-	smt::SortPointer sort(FunctionDefinition const& _function);
+	smtutil::SortPointer sort(FunctionDefinition const& _function);
-	smt::SortPointer sort(ASTNode const* _block);
+	smtutil::SortPointer sort(ASTNode const* _block);
 	/// @returns the sort of a predicate that represents the summary of _function in the scope of _contract.
 	/// The _contract is also needed because the same function might be in many contracts due to inheritance,
 	/// where the sort changes because the set of state variables might change.
-	static smt::SortPointer summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract);
+	static smtutil::SortPointer summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract);
 	//@}
 
 	/// Predicate helpers.
 	//@{
 	/// @returns a new block of given _sort and _name.
-	std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smt::SortPointer _sort, std::string const& _name);
+	std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name);
 
 	/// Creates summary predicates for all functions of all contracts
 	/// in a given _source.
 	void defineInterfacesAndSummaries(SourceUnit const& _source);
 
 	/// Genesis predicate.
-	smt::Expression genesis() { return (*m_genesisPredicate)({}); }
+	smtutil::Expression genesis() { return (*m_genesisPredicate)({}); }
 	/// Interface predicate over current variables.
-	smt::Expression interface();
+	smtutil::Expression interface();
-	smt::Expression interface(ContractDefinition const& _contract);
+	smtutil::Expression interface(ContractDefinition const& _contract);
 	/// Error predicate over current variables.
-	smt::Expression error();
+	smtutil::Expression error();
-	smt::Expression error(unsigned _idx);
+	smtutil::Expression error(unsigned _idx);
 
 	/// Creates a block for the given _node.
 	std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(ASTNode const* _node, std::string const& _prefix = "");
@@ -144,48 +144,48 @@ private:
 	/// Also registers the predicate.
 	void createErrorBlock();
 
-	void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true));
+	void connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints = smtutil::Expression(true));
 
 	/// @returns the symbolic values of the state variables at the beginning
 	/// of the current transaction.
-	std::vector<smt::Expression> initialStateVariables();
+	std::vector<smtutil::Expression> initialStateVariables();
-	std::vector<smt::Expression> stateVariablesAtIndex(int _index);
+	std::vector<smtutil::Expression> stateVariablesAtIndex(int _index);
-	std::vector<smt::Expression> stateVariablesAtIndex(int _index, ContractDefinition const& _contract);
+	std::vector<smtutil::Expression> stateVariablesAtIndex(int _index, ContractDefinition const& _contract);
 	/// @returns the current symbolic values of the current state variables.
-	std::vector<smt::Expression> currentStateVariables();
+	std::vector<smtutil::Expression> currentStateVariables();
 
 	/// @returns the current symbolic values of the current function's
 	/// input and output parameters.
-	std::vector<smt::Expression> currentFunctionVariables();
+	std::vector<smtutil::Expression> currentFunctionVariables();
 	/// @returns the same as currentFunctionVariables plus
 	/// local variables.
-	std::vector<smt::Expression> currentBlockVariables();
+	std::vector<smtutil::Expression> currentBlockVariables();
 
 	/// @returns the predicate name for a given node.
 	std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
 	/// @returns a predicate application over the current scoped variables.
-	smt::Expression predicate(smt::SymbolicFunctionVariable const& _block);
+	smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block);
 	/// @returns a predicate application over @param _arguments.
-	smt::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const& _arguments);
+	smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const& _arguments);
 	/// @returns the summary predicate for the called function.
-	smt::Expression predicate(FunctionCall const& _funCall);
+	smtutil::Expression predicate(FunctionCall const& _funCall);
 	/// @returns a predicate that defines a constructor summary.
-	smt::Expression summary(ContractDefinition const& _contract);
+	smtutil::Expression summary(ContractDefinition const& _contract);
 	/// @returns a predicate that defines a function summary.
-	smt::Expression summary(FunctionDefinition const& _function);
+	smtutil::Expression summary(FunctionDefinition const& _function);
 	//@}
 
 	/// Solver related.
 	//@{
 	/// Adds Horn rule to the solver.
-	void addRule(smt::Expression const& _rule, std::string const& _ruleName);
+	void addRule(smtutil::Expression const& _rule, std::string const& _ruleName);
 	/// @returns <true, empty> if query is unsatisfiable (safe).
 	/// @returns <false, model> otherwise.
-	std::pair<smt::CheckResult, std::vector<std::string>> query(smt::Expression const& _query, langutil::SourceLocation const& _location);
+	std::pair<smtutil::CheckResult, std::vector<std::string>> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location);
 
-	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
+	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
-	void addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
+	void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
-	void addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId);
+	void addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expression _errorId);
 	//@}
 
 	/// Misc.
@@ -231,7 +231,7 @@ private:
 	//@{
 	/// State variables sorts.
 	/// Used by all predicates.
-	std::vector<smt::SortPointer> m_stateSorts;
+	std::vector<smtutil::SortPointer> m_stateSorts;
 	/// State variables.
 	/// Used to create all predicates.
 	std::vector<VariableDeclaration const*> m_stateVariables;
@@ -241,7 +241,7 @@ private:
 	//@{
 	struct CHCVerificationTarget: VerificationTarget
 	{
-		smt::Expression errorId;
+		smtutil::Expression errorId;
 	};
 
 	std::map<ASTNode const*, CHCVerificationTarget, IdCompare> m_verificationTargets;
@@ -261,7 +261,7 @@ private:
 	std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions;
 
 	/// The current block.
-	smt::Expression m_currentBlock = smt::Expression(true);
+	smtutil::Expression m_currentBlock = smtutil::Expression(true);
 
 	/// Counter to generate unique block names.
 	unsigned m_blockCounter = 0;
@@ -276,13 +276,13 @@ private:
 	//@}
 
 	/// CHC solver.
-	std::unique_ptr<smt::CHCSolverInterface> m_interface;
+	std::unique_ptr<smtutil::CHCSolverInterface> m_interface;
 
 	/// ErrorReporter that comes from CompilerStack.
 	langutil::ErrorReporter& m_outerErrorReporter;
 
 	/// SMT solvers that are chosen at runtime.
-	smt::SMTSolverChoice m_enabledSolvers;
+	smtutil::SMTSolverChoice m_enabledSolvers;
 };
 
 }

libsolidity/formal/EncodingContext.cpp

@@ -92,7 +92,7 @@ void EncodingContext::resetAllVariables()
 	resetVariables([&](frontend::VariableDeclaration const&) { return true; });
 }
 
-Expression EncodingContext::newValue(frontend::VariableDeclaration const& _decl)
+smtutil::Expression EncodingContext::newValue(frontend::VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
 	return m_variables.at(&_decl)->increaseIndex();
@@ -179,10 +179,10 @@ bool EncodingContext::knownGlobalSymbol(string const& _var) const
 
 /// Solver.
 
-Expression EncodingContext::assertions()
+smtutil::Expression EncodingContext::assertions()
 {
 	if (m_assertions.empty())
-		return Expression(true);
+		return smtutil::Expression(true);
 
 	return m_assertions.back();
 }
@@ -201,7 +201,7 @@ void EncodingContext::popSolver()
 	m_assertions.pop_back();
 }
 
-void EncodingContext::addAssertion(Expression const& _expr)
+void EncodingContext::addAssertion(smtutil::Expression const& _expr)
 {
 	if (m_assertions.empty())
 		m_assertions.push_back(_expr);

libsolidity/formal/EncodingContext.h

@@ -17,10 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/formal/SymbolicState.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 
+#include <libsmtutil/SolverInterface.h>
+
 #include <unordered_map>
 #include <set>
 
@@ -45,7 +46,7 @@ public:
 
 	/// Sets the current solver used by the current engine for
 	/// SMT variable declaration.
-	void setSolver(SolverInterface* _solver)
+	void setSolver(smtutil::SolverInterface* _solver)
 	{
 		solAssert(_solver, "");
 		m_solver = _solver;
@@ -55,7 +56,7 @@ public:
 	void setAssertionAccumulation(bool _acc) { m_accumulateAssertions = _acc; }
 
 	/// Forwards variable creation to the solver.
-	Expression newVariable(std::string _name, SortPointer _sort)
+	smtutil::Expression newVariable(std::string _name, smtutil::SortPointer _sort)
 	{
 		solAssert(m_solver, "");
 		return m_solver->newVariable(move(_name), move(_sort));
@@ -85,7 +86,7 @@ public:
 
 	/// Allocates a new index for the declaration, updates the current
 	/// index to this value and returns the expression.
-	Expression newValue(frontend::VariableDeclaration const& _decl);
+	smtutil::Expression newValue(frontend::VariableDeclaration const& _decl);
 	/// Sets the value of the declaration to zero.
 	void setZeroValue(frontend::VariableDeclaration const& _decl);
 	void setZeroValue(SymbolicVariable& _variable);
@@ -125,12 +126,12 @@ public:
 	/// Solver.
 	//@{
 	/// @returns conjunction of all added assertions.
-	Expression assertions();
+	smtutil::Expression assertions();
 	void pushSolver();
 	void popSolver();
-	void addAssertion(Expression const& _e);
+	void addAssertion(smtutil::Expression const& _e);
 	unsigned solverStackHeigh() { return m_assertions.size(); } const
-	SolverInterface* solver()
+	smtutil::SolverInterface* solver()
 	{
 		solAssert(m_solver, "");
 		return m_solver;
@@ -159,10 +160,10 @@ private:
 	/// Solver related.
 	//@{
 	/// Solver can be SMT solver or Horn solver in the future.
-	SolverInterface* m_solver = nullptr;
+	smtutil::SolverInterface* m_solver = nullptr;
 
 	/// Assertion stack.
-	std::vector<Expression> m_assertions;
+	std::vector<smtutil::Expression> m_assertions;
 
 	/// Whether to conjoin assertions in the assertion stack.
 	bool m_accumulateAssertions = true;

libsolidity/formal/ModelChecker.cpp

@@ -27,7 +27,7 @@ ModelChecker::ModelChecker(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
-	smt::SMTSolverChoice _enabledSolvers
+	smtutil::SMTSolverChoice _enabledSolvers
 ):
 	m_context(),
 	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
@@ -49,9 +49,9 @@ vector<string> ModelChecker::unhandledQueries()
 	return m_bmc.unhandledQueries() + m_chc.unhandledQueries();
 }
 
-smt::SMTSolverChoice ModelChecker::availableSolvers()
+solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
 {
-	smt::SMTSolverChoice available = smt::SMTSolverChoice::None();
+	smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None();
 #ifdef HAVE_Z3
 	available.z3 = true;
 #endif

libsolidity/formal/ModelChecker.h

@@ -25,9 +25,10 @@
 #include <libsolidity/formal/BMC.h>
 #include <libsolidity/formal/CHC.h>
 #include <libsolidity/formal/EncodingContext.h>
-#include <libsolidity/formal/SolverInterface.h>
 
 #include <libsolidity/interface/ReadFile.h>
+
+#include <libsmtutil/SolverInterface.h>
 #include <liblangutil/ErrorReporter.h>
 
 namespace solidity::langutil
@@ -48,7 +49,7 @@ public:
 		langutil::ErrorReporter& _errorReporter,
 		std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
-		smt::SMTSolverChoice _enabledSolvers = smt::SMTSolverChoice::All()
+		smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All()
 	);
 
 	void analyze(SourceUnit const& _sources);
@@ -59,7 +60,7 @@ public:
 	std::vector<std::string> unhandledQueries();
 
 	/// @returns SMT solvers that are available via the C++ API.
-	static smt::SMTSolverChoice availableSolvers();
+	static smtutil::SMTSolverChoice availableSolvers();
 
 private:
 	/// Stores the context of the encoding.

libsolidity/formal/SMTEncoder.cpp

@@ -18,10 +18,11 @@
 #include <libsolidity/formal/SMTEncoder.h>
 
 #include <libsolidity/ast/TypeProvider.h>
-#include <libsolidity/formal/SMTPortfolio.h>
 #include <libsolidity/formal/SymbolicState.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
+#include <libsmtutil/SMTPortfolio.h>
+
 #include <boost/range/adaptors.hpp>
 #include <boost/range/adaptor/reversed.hpp>
 
@@ -180,7 +181,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
 	solAssert(_invocation, "");
 	_invocation->accept(*this);
 
-	vector<smt::Expression> args;
+	vector<smtutil::Expression> args;
 	if (auto const* arguments = _invocation->arguments())
 	{
 		auto const& modifierParams = _definition->parameters();
@@ -366,7 +367,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 	else
 	{
 		auto const& type = _assignment.annotation().type;
-		vector<smt::Expression> rightArguments;
+		vector<smtutil::Expression> rightArguments;
 		if (auto const* tupleTypeRight = dynamic_cast<TupleType const*>(_assignment.rightHandSide().annotation().type))
 		{
 			auto symbTupleLeft = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_assignment.leftHandSide()));
@@ -640,7 +641,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		auto const& value = args.front();
 		solAssert(value, "");
 
-		smt::Expression thisBalance = m_context.state().balance();
+		smtutil::Expression thisBalance = m_context.state().balance();
 		setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context);
 
 		m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value));
@@ -778,7 +779,7 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 			else
 			{
 				auto const& intType = dynamic_cast<IntegerType const&>(*m_context.expression(_funCall)->type());
-				defineExpr(_funCall, smt::Expression::ite(
+				defineExpr(_funCall, smtutil::Expression::ite(
 					expr(*argument) >= smt::minValue(intType) && expr(*argument) <= smt::maxValue(intType),
 					expr(*argument),
 					expr(_funCall)
@@ -809,9 +810,9 @@ void SMTEncoder::endVisit(Literal const& _literal)
 	solAssert(_literal.annotation().type, "Expected type for AST node");
 	Type const& type = *_literal.annotation().type;
 	if (smt::isNumber(type.category()))
-		defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
+		defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal)));
 	else if (smt::isBool(type.category()))
-		defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
+		defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
 	else if (smt::isStringLiteral(type.category()))
 		createExpr(_literal);
 	else
@@ -964,7 +965,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 
 	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
 	solAssert(arrayVar, "");
-	defineExpr(_indexAccess, smt::Expression::select(
+	defineExpr(_indexAccess, smtutil::Expression::select(
 		arrayVar->elements(),
 		expr(*_indexAccess.indexExpression())
 	));
@@ -991,7 +992,7 @@ void SMTEncoder::arrayAssignment()
 	m_arrayAssignmentHappened = true;
 }
 
-void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide)
+void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
 {
 	auto toStore = _rightHandSide;
 	auto indexAccess = dynamic_cast<IndexAccess const*>(&_expr);
@@ -1038,7 +1039,7 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 				});
 
 			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.variable(*varDecl));
-			smt::Expression store = smt::Expression::store(
+			smtutil::Expression store = smtutil::Expression::store(
 				symbArray->elements(),
 				expr(*indexAccess->indexExpression()),
 				toStore
@@ -1049,7 +1050,7 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 			m_context.addAssertion(symbArray->length() == oldLength);
 			// Update the SMT select value after the assignment,
 			// necessary for sound models.
-			defineExpr(*indexAccess, smt::Expression::select(
+			defineExpr(*indexAccess, smtutil::Expression::select(
 				symbArray->elements(),
 				expr(*indexAccess->indexExpression())
 			));
@@ -1060,9 +1061,10 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 		{
 			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*base));
 			solAssert(symbArray, "");
-			toStore = smt::Expression::tuple_constructor(
+			auto baseType = base->annotation().type;
-				smt::Expression(base->annotation().type),
+			toStore = smtutil::Expression::tuple_constructor(
-				{smt::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
+				smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
+				{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
 			);
 			indexAccess = base;
 		}
@@ -1091,10 +1093,10 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall)
 	m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1));
 
 	auto const& arguments = _funCall.arguments();
-	smt::Expression element = arguments.empty() ?
+	smtutil::Expression element = arguments.empty() ?
 		smt::zeroValue(_funCall.annotation().type) :
 		expr(*arguments.front());
-	smt::Expression store = smt::Expression::store(
+	smtutil::Expression store = smtutil::Expression::store(
 		symbArray->elements(),
 		oldLength,
 		element
@@ -1124,7 +1126,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
 
 	symbArray->increaseIndex();
 	m_context.addAssertion(symbArray->elements() == oldElements);
-	auto newLength = smt::Expression::ite(
+	auto newLength = smtutil::Expression::ite(
 		oldLength == 0,
 		smt::maxValue(*TypeProvider::uint256()),
 		oldLength - 1
@@ -1134,7 +1136,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
 	arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
 }
 
-void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array)
+void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array)
 {
 	if (auto const* id = dynamic_cast<Identifier const*>(&_expr))
 	{
@@ -1175,9 +1177,9 @@ bool SMTEncoder::shortcutRationalNumber(Expression const& _expr)
 		auto rationalType = dynamic_cast<RationalNumberType const*>(_expr.annotation().type);
 		solAssert(rationalType, "");
 		if (rationalType->isNegative())
-			defineExpr(_expr, smt::Expression(u2s(rationalType->literalValue(nullptr))));
+			defineExpr(_expr, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
 		else
-			defineExpr(_expr, smt::Expression(rationalType->literalValue(nullptr)));
+			defineExpr(_expr, smtutil::Expression(rationalType->literalValue(nullptr)));
 		return true;
 	}
 	return false;
@@ -1223,10 +1225,10 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
 		);
 }
 
-pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
+pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	Token _op,
-	smt::Expression const& _left,
+	smtutil::Expression const& _left,
-	smt::Expression const& _right,
+	smtutil::Expression const& _right,
 	TypePointer const& _commonType,
 	Expression const&
 )
@@ -1243,7 +1245,7 @@ pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
 	solAssert(_commonType->category() == Type::Category::Integer, "");
 
 	auto const& intType = dynamic_cast<IntegerType const&>(*_commonType);
-	smt::Expression valueNoMod(
+	smtutil::Expression valueNoMod(
 		_op == Token::Add ? _left + _right :
 		_op == Token::Sub ? _left - _right :
 		_op == Token::Div ? division(_left, _right, intType) :
@@ -1254,11 +1256,11 @@ pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
 	if (_op == Token::Div || _op == Token::Mod)
 		m_context.addAssertion(_right != 0);
 
-	smt::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
+	smtutil::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
-	auto value = smt::Expression::ite(
+	auto value = smtutil::Expression::ite(
 		valueNoMod > smt::maxValue(intType),
 		valueNoMod % intValueRange,
-		smt::Expression::ite(
+		smtutil::Expression::ite(
 			valueNoMod < smt::minValue(intType),
 			valueNoMod % intValueRange,
 			valueNoMod
@@ -1266,7 +1268,7 @@ pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
 	);
 
 	if (intType.isSigned())
-		value = smt::Expression::ite(
+		value = smtutil::Expression::ite(
 			value > smt::maxValue(intType),
 			value - intValueRange,
 			value
@@ -1281,13 +1283,13 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
 	solAssert(commonType, "");
 	if (smt::isSupportedType(commonType->category()))
 	{
-		smt::Expression left(expr(_op.leftExpression(), commonType));
+		smtutil::Expression left(expr(_op.leftExpression(), commonType));
-		smt::Expression right(expr(_op.rightExpression(), commonType));
+		smtutil::Expression right(expr(_op.rightExpression(), commonType));
 		Token op = _op.getOperator();
-		shared_ptr<smt::Expression> value;
+		shared_ptr<smtutil::Expression> value;
 		if (smt::isNumber(commonType->category()))
 		{
-			value = make_shared<smt::Expression>(
+			value = make_shared<smtutil::Expression>(
 				op == Token::Equal ? (left == right) :
 				op == Token::NotEqual ? (left != right) :
 				op == Token::LessThan ? (left < right) :
@@ -1299,7 +1301,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
 		else // Bool
 		{
 			solUnimplementedAssert(smt::isBool(commonType->category()), "Operation not yet supported");
-			value = make_shared<smt::Expression>(
+			value = make_shared<smtutil::Expression>(
 				op == Token::Equal ? (left == right) :
 				/*op == Token::NotEqual*/ (left != right)
 			);
@@ -1344,14 +1346,14 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
 		);
 }
 
-smt::Expression SMTEncoder::division(smt::Expression _left, smt::Expression _right, IntegerType const& _type)
+smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type)
 {
 	// Signed division in SMTLIB2 rounds differently for negative division.
 	if (_type.isSigned())
-		return (smt::Expression::ite(
+		return (smtutil::Expression::ite(
 			_left >= 0,
-			smt::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))),
+			smtutil::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))),
-			smt::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right))
+			smtutil::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right))
 		));
 	else
 		return _left / _right;
@@ -1359,7 +1361,7 @@ smt::Expression SMTEncoder::division(smt::Expression _left, smt::Expression _rig
 
 void SMTEncoder::assignment(
 	Expression const& _left,
-	vector<smt::Expression> const& _right,
+	vector<smtutil::Expression> const& _right,
 	TypePointer const& _type,
 	langutil::SourceLocation const& _location
 )
@@ -1405,7 +1407,7 @@ void SMTEncoder::assignment(
 		);
 }
 
-smt::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
+smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
 {
 	static map<Token, Token> const compoundToArithmetic{
 		{Token::AssignAdd, Token::Add},
@@ -1439,7 +1441,7 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression con
 	// TODO else { store each string literal byte into the array }
 }
 
-void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expression const& _value)
+void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value)
 {
 	TypePointer type = _variable.type();
 	if (type->category() == Type::Category::Mapping)
@@ -1447,12 +1449,12 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expressio
 	m_context.addAssertion(m_context.newValue(_variable) == _value);
 }
 
-SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smt::Expression _condition)
+SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression _condition)
 {
 	return visitBranch(_statement, &_condition);
 }
 
-SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smt::Expression const* _condition)
+SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition)
 {
 	auto indicesBeforeBranch = copyVariableIndices();
 	if (_condition)
@@ -1465,7 +1467,7 @@ SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, s
 	return indicesAfterBranch;
 }
 
-void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smt::Expression> const& _callArgs)
+void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smtutil::Expression> const& _callArgs)
 {
 	auto const& funParams = _function.parameters();
 	solAssert(funParams.size() == _callArgs.size(), "");
@@ -1562,7 +1564,7 @@ TypePointer SMTEncoder::typeWithoutPointer(TypePointer const& _type)
 	return _type;
 }
 
-void SMTEncoder::mergeVariables(set<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
+void SMTEncoder::mergeVariables(set<VariableDeclaration const*> const& _variables, smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
 {
 	auto cmp = [] (VariableDeclaration const* var1, VariableDeclaration const* var2) {
 		return var1->id() < var2->id();
@@ -1589,7 +1591,7 @@ void SMTEncoder::mergeVariables(set<VariableDeclaration const*> const& _variable
 		int trueIndex = _indicesEndTrue.at(decl);
 		int falseIndex = _indicesEndFalse.at(decl);
 		solAssert(trueIndex != falseIndex, "");
-		m_context.addAssertion(m_context.newValue(*decl) == smt::Expression::ite(
+		m_context.addAssertion(m_context.newValue(*decl) == smtutil::Expression::ite(
 			_condition,
 			valueAtIndex(*decl, trueIndex),
 			valueAtIndex(*decl, falseIndex))
@@ -1597,13 +1599,13 @@ void SMTEncoder::mergeVariables(set<VariableDeclaration const*> const& _variable
 	}
 }
 
-smt::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl)
+smtutil::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl)
 {
 	solAssert(m_context.knownVariable(_decl), "");
 	return m_context.variable(_decl)->currentValue();
 }
 
-smt::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, int _index)
+smtutil::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, int _index)
 {
 	solAssert(m_context.knownVariable(_decl), "");
 	return m_context.variable(_decl)->valueAtIndex(_index);
@@ -1626,7 +1628,7 @@ bool SMTEncoder::createVariable(VariableDeclaration const& _varDecl)
 	return true;
 }
 
-smt::Expression SMTEncoder::expr(Expression const& _e, TypePointer _targetType)
+smtutil::Expression SMTEncoder::expr(Expression const& _e, TypePointer _targetType)
 {
 	if (!m_context.knownExpression(_e))
 	{
@@ -1648,10 +1650,10 @@ void SMTEncoder::createExpr(Expression const& _e)
 		);
 }
 
-void SMTEncoder::defineExpr(Expression const& _e, smt::Expression _value)
+void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value)
 {
 	createExpr(_e);
-	solAssert(_value.sort->kind != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
+	solAssert(_value.sort->kind != smtutil::Kind::Function, "Equality operator applied to type that is not fully supported");
 	m_context.addAssertion(expr(_e) == _value);
 }
 
@@ -1661,15 +1663,15 @@ void SMTEncoder::popPathCondition()
 	m_pathConditions.pop_back();
 }
 
-void SMTEncoder::pushPathCondition(smt::Expression const& _e)
+void SMTEncoder::pushPathCondition(smtutil::Expression const& _e)
 {
 	m_pathConditions.push_back(currentPathConditions() && _e);
 }
 
-smt::Expression SMTEncoder::currentPathConditions()
+smtutil::Expression SMTEncoder::currentPathConditions()
 {
 	if (m_pathConditions.empty())
-		return smt::Expression(true);
+		return smtutil::Expression(true);
 	return m_pathConditions.back();
 }
 
@@ -1697,9 +1699,9 @@ void SMTEncoder::pushCallStack(CallStackEntry _entry)
 	m_callStack.push_back(_entry);
 }
 
-void SMTEncoder::addPathImpliedExpression(smt::Expression const& _e)
+void SMTEncoder::addPathImpliedExpression(smtutil::Expression const& _e)
 {
-	m_context.addAssertion(smt::Expression::implies(currentPathConditions(), _e));
+	m_context.addAssertion(smtutil::Expression::implies(currentPathConditions(), _e));
 }
 
 bool SMTEncoder::isRootFunction()
@@ -1835,12 +1837,12 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 		defineExpr(_funCall, currentValue(*returnParams.front()));
 }
 
-vector<smt::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall)
+vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall)
 {
 	auto const* function = functionCallToDefinition(_funCall);
 	solAssert(function, "");
 
-	vector<smt::Expression> args;
+	vector<smtutil::Expression> args;
 	Expression const* calledExpr = &_funCall.expression();
 	auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
 	solAssert(funType, "");

libsolidity/formal/SMTEncoder.h

@@ -99,10 +99,10 @@ protected:
 	/// @returns _op(_left, _right) with and without modular arithmetic.
 	/// Used by the function above, compound assignments and
 	/// unary increment/decrement.
-	virtual std::pair<smt::Expression, smt::Expression> arithmeticOperation(
+	virtual std::pair<smtutil::Expression, smtutil::Expression> arithmeticOperation(
 		Token _op,
-		smt::Expression const& _left,
+		smtutil::Expression const& _left,
-		smt::Expression const& _right,
+		smtutil::Expression const& _right,
 		TypePointer const& _commonType,
 		Expression const& _expression
 	);
@@ -135,32 +135,32 @@ protected:
 	/// while aliasing is not supported.
 	void arrayAssignment();
 	/// Handles assignment to SMT array index.
-	void arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide);
+	void arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide);
 
 	void arrayPush(FunctionCall const& _funCall);
 	void arrayPop(FunctionCall const& _funCall);
-	void arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array);
+	void arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array);
 	/// Allows BMC and CHC to create verification targets for popping
 	/// an empty array.
 	virtual void makeArrayPopVerificationTarget(FunctionCall const&) {}
 
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
-	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
+	smtutil::Expression division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type);
 
 	void assignment(VariableDeclaration const& _variable, Expression const& _value);
 	/// Handles assignments to variables of different types.
-	void assignment(VariableDeclaration const& _variable, smt::Expression const& _value);
+	void assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value);
 	/// Handles assignments between generic expressions.
 	/// Will also be used for assignments of tuple components.
 	void assignment(
 		Expression const& _left,
-		std::vector<smt::Expression> const& _right,
+		std::vector<smtutil::Expression> const& _right,
 		TypePointer const& _type,
 		langutil::SourceLocation const& _location
 	);
 	/// Computes the right hand side of a compound assignment.
-	smt::Expression compoundAssignment(Assignment const& _assignment);
+	smtutil::Expression compoundAssignment(Assignment const& _assignment);
 
 	/// Maps a variable to an SSA index.
 	using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;
@@ -168,8 +168,8 @@ protected:
 	/// Visits the branch given by the statement, pushes and pops the current path conditions.
 	/// @param _condition if present, asserts that this condition is true within the branch.
 	/// @returns the variable indices after visiting the branch.
-	VariableIndices visitBranch(ASTNode const* _statement, smt::Expression const* _condition = nullptr);
+	VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr);
-	VariableIndices visitBranch(ASTNode const* _statement, smt::Expression _condition);
+	VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression _condition);
 
 	using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
 
@@ -177,7 +177,7 @@ protected:
 	void initializeStateVariables(ContractDefinition const& _contract);
 	void createLocalVariables(FunctionDefinition const& _function);
 	void initializeLocalVariables(FunctionDefinition const& _function);
-	void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smt::Expression> const& _callArgs);
+	void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smtutil::Expression> const& _callArgs);
 	void resetStateVariables();
 	/// @returns the type without storage pointer information if it has it.
 	TypePointer typeWithoutPointer(TypePointer const& _type);
@@ -185,31 +185,31 @@ protected:
 	/// Given two different branches and the touched variables,
 	/// merge the touched variables into after-branch ite variables
 	/// using the branch condition as guard.
-	void mergeVariables(std::set<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
+	void mergeVariables(std::set<VariableDeclaration const*> const& _variables, smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
 	/// Tries to create an uninitialized variable and returns true on success.
 	bool createVariable(VariableDeclaration const& _varDecl);
 
 	/// @returns an expression denoting the value of the variable declared in @a _decl
 	/// at the current point.
-	smt::Expression currentValue(VariableDeclaration const& _decl);
+	smtutil::Expression currentValue(VariableDeclaration const& _decl);
 	/// @returns an expression denoting the value of the variable declared in @a _decl
 	/// at the given index. Does not ensure that this index exists.
-	smt::Expression valueAtIndex(VariableDeclaration const& _decl, int _index);
+	smtutil::Expression valueAtIndex(VariableDeclaration const& _decl, int _index);
 	/// Returns the expression corresponding to the AST node.
 	/// If _targetType is not null apply conversion.
 	/// Throws if the expression does not exist.
-	smt::Expression expr(Expression const& _e, TypePointer _targetType = nullptr);
+	smtutil::Expression expr(Expression const& _e, TypePointer _targetType = nullptr);
 	/// Creates the expression (value can be arbitrary)
 	void createExpr(Expression const& _e);
 	/// Creates the expression and sets its value.
-	void defineExpr(Expression const& _e, smt::Expression _value);
+	void defineExpr(Expression const& _e, smtutil::Expression _value);
 
 	/// Adds a new path condition
-	void pushPathCondition(smt::Expression const& _e);
+	void pushPathCondition(smtutil::Expression const& _e);
 	/// Remove the last path condition
 	void popPathCondition();
 	/// Returns the conjunction of all path conditions or True if empty
-	smt::Expression currentPathConditions();
+	smtutil::Expression currentPathConditions();
 	/// @returns a human-readable call stack. Used for models.
 	langutil::SecondarySourceLocation callStackMessage(std::vector<CallStackEntry> const& _callStack);
 	/// Copies and pops the last called node.
@@ -217,7 +217,7 @@ protected:
 	/// Adds (_definition, _node) to the callstack.
 	void pushCallStack(CallStackEntry _entry);
 	/// Add to the solver: the given expression implied by the current path conditions
-	void addPathImpliedExpression(smt::Expression const& _e);
+	void addPathImpliedExpression(smtutil::Expression const& _e);
 
 	/// Copy the SSA indices of m_variables.
 	VariableIndices copyVariableIndices();
@@ -240,7 +240,7 @@ protected:
 	/// @returns the symbolic arguments for a function call,
 	/// taking into account bound functions and
 	/// type conversion.
-	std::vector<smt::Expression> symbolicArguments(FunctionCall const& _funCall);
+	std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall);
 
 	/// @returns a note to be added to warnings.
 	std::string extraComment();
@@ -248,8 +248,8 @@ protected:
 	struct VerificationTarget
 	{
 		enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray } type;
-		smt::Expression value;
+		smtutil::Expression value;
-		smt::Expression constraints;
+		smtutil::Expression constraints;
 	};
 
 	smt::VariableUsage m_variableUsage;
@@ -261,7 +261,7 @@ protected:
 	/// These may be direct application of UFs or Array index access.
 	/// Used to retrieve models.
 	std::set<Expression const*> m_uninterpretedTerms;
-	std::vector<smt::Expression> m_pathConditions;
+	std::vector<smtutil::Expression> m_pathConditions;
 	/// Local SMTEncoder ErrorReporter.
 	/// This is necessary to show the "No SMT solver available"
 	/// warning before the others in case it's needed.

libsolidity/formal/SymbolicState.cpp

@@ -20,6 +20,7 @@
 #include <libsolidity/formal/EncodingContext.h>
 
 using namespace std;
+using namespace solidity;
 using namespace solidity::frontend::smt;
 
 SymbolicState::SymbolicState(EncodingContext& _context):
@@ -35,22 +36,22 @@ void SymbolicState::reset()
 
 // Blockchain
 
-Expression SymbolicState::thisAddress()
+smtutil::Expression SymbolicState::thisAddress()
 {
 	return m_thisAddress.currentValue();
 }
 
-Expression SymbolicState::balance()
+smtutil::Expression SymbolicState::balance()
 {
 	return balance(m_thisAddress.currentValue());
 }
 
-Expression SymbolicState::balance(Expression _address)
+smtutil::Expression SymbolicState::balance(smtutil::Expression _address)
 {
-	return Expression::select(m_balances.elements(), move(_address));
+	return smtutil::Expression::select(m_balances.elements(), move(_address));
 }
 
-void SymbolicState::transfer(Expression _from, Expression _to, Expression _value)
+void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
 {
 	unsigned indexBefore = m_balances.index();
 	addBalance(_from, 0 - _value);
@@ -59,7 +60,7 @@ void SymbolicState::transfer(Expression _from, Expression _to, Expression _value
 	solAssert(indexAfter > indexBefore, "");
 	m_balances.increaseIndex();
 	/// Do not apply the transfer operation if _from == _to.
-	auto newBalances = Expression::ite(
+	auto newBalances = smtutil::Expression::ite(
 		move(_from) == move(_to),
 		m_balances.valueAtIndex(indexBefore),
 		m_balances.valueAtIndex(indexAfter)
@@ -69,9 +70,9 @@ void SymbolicState::transfer(Expression _from, Expression _to, Expression _value
 
 /// Private helpers.
 
-void SymbolicState::addBalance(Expression _address, Expression _value)
+void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
 {
-	auto newBalances = Expression::store(
+	auto newBalances = smtutil::Expression::store(
 		m_balances.elements(),
 		_address,
 		balance(_address) + move(_value)

libsolidity/formal/SymbolicState.h

@@ -17,10 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/formal/Sorts.h>
-#include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 
+#include <libsmtutil/Sorts.h>
+#include <libsmtutil/SolverInterface.h>
+
 namespace solidity::frontend::smt
 {
 
@@ -39,18 +40,18 @@ public:
 	/// Blockchain.
 	//@{
 	/// Value of `this` address.
-	Expression thisAddress();
+	smtutil::Expression thisAddress();
 	/// @returns the symbolic balance of address `this`.
-	Expression balance();
+	smtutil::Expression balance();
 	/// @returns the symbolic balance of an address.
-	Expression balance(Expression _address);
+	smtutil::Expression balance(smtutil::Expression _address);
 	/// Transfer _value from _from to _to.
-	void transfer(Expression _from, Expression _to, Expression _value);
+	void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
 	//@}
 
 private:
 	/// Adds _value to _account's balance.
-	void addBalance(Expression _account, Expression _value);
+	void addBalance(smtutil::Expression _account, smtutil::Expression _value);
 
 	EncodingContext& m_context;
 
@@ -62,7 +63,7 @@ private:
 
 	/// Symbolic balances.
 	SymbolicArrayVariable m_balances{
-		std::make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort),
+		std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::intSort, smtutil::SortProvider::intSort),
 		"balances",
 		m_context
 	};

libsolidity/formal/SymbolicTypes.cpp

@@ -24,6 +24,7 @@
 #include <vector>
 
 using namespace std;
+using namespace solidity::smtutil;
 
 namespace solidity::frontend::smt
 {
@@ -334,14 +335,14 @@ bool isStringLiteral(frontend::Type::Category _category)
 	return _category == frontend::Type::Category::StringLiteral;
 }
 
-Expression minValue(frontend::IntegerType const& _type)
+smtutil::Expression minValue(frontend::IntegerType const& _type)
 {
-	return Expression(_type.minValue());
+	return smtutil::Expression(_type.minValue());
 }
 
-Expression maxValue(frontend::IntegerType const& _type)
+smtutil::Expression maxValue(frontend::IntegerType const& _type)
 {
-	return Expression(_type.maxValue());
+	return smtutil::Expression(_type.maxValue());
 }
 
 void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context)
@@ -349,13 +350,13 @@ void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _c
 	setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context);
 }
 
-void setSymbolicZeroValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
+void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
 {
 	solAssert(_type, "");
 	_context.addAssertion(_expr == zeroValue(_type));
 }
 
-Expression zeroValue(frontend::TypePointer const& _type)
+smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 {
 	solAssert(_type, "");
 	if (isSupportedType(_type->category()))
@@ -363,28 +364,31 @@ Expression zeroValue(frontend::TypePointer const& _type)
 		if (isNumber(_type->category()))
 			return 0;
 		if (isBool(_type->category()))
-			return Expression(false);
+			return smtutil::Expression(false);
 		if (isArray(_type->category()) || isMapping(_type->category()))
 		{
 			auto tupleSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
 			solAssert(tupleSort, "");
 			auto sortSort = make_shared<SortSort>(tupleSort->components.front());
 
-			std::optional<Expression> zeroArray;
+			std::optional<smtutil::Expression> zeroArray;
 			auto length = bigint(0);
 			if (auto arrayType = dynamic_cast<ArrayType const*>(_type))
 			{
-				zeroArray = Expression::const_array(Expression(sortSort), zeroValue(arrayType->baseType()));
+				zeroArray = smtutil::Expression::const_array(smtutil::Expression(sortSort), zeroValue(arrayType->baseType()));
 				if (!arrayType->isDynamicallySized())
 					length = bigint(arrayType->length());
 			}
 			else if (auto mappingType = dynamic_cast<MappingType const*>(_type))
-				zeroArray = Expression::const_array(Expression(sortSort), zeroValue(mappingType->valueType()));
+				zeroArray = smtutil::Expression::const_array(smtutil::Expression(sortSort), zeroValue(mappingType->valueType()));
 			else
 				solAssert(false, "");
 
 			solAssert(zeroArray, "");
-			return Expression::tuple_constructor(Expression(_type), vector<Expression>{*zeroArray, length});
+			return smtutil::Expression::tuple_constructor(
+				smtutil::Expression(std::make_shared<SortSort>(smtSort(*_type)), _type->toString(true)),
+				vector<smtutil::Expression>{*zeroArray, length}
+			);
 
 		}
 		solAssert(false, "");
@@ -398,7 +402,7 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
 	setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _context);
 }
 
-void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
+void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
 {
 	solAssert(_type, "");
 	if (isEnum(_type->category()))
@@ -417,7 +421,7 @@ void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _typ
 	}
 }
 
-optional<Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)
+optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)
 {
 	if (_to && _from)
 		// StringLiterals are encoded as SMT arrays in the generic case,
@@ -425,7 +429,7 @@ optional<Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)
 		// case they'd need to be encoded as numbers.
 		if (auto strType = dynamic_cast<StringLiteralType const*>(_from))
 			if (_to->category() == frontend::Type::Category::FixedBytes)
-				return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
+				return smtutil::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
 
 	return std::nullopt;
 }

libsolidity/formal/SymbolicTypes.h

@@ -26,14 +26,14 @@ namespace solidity::frontend::smt
 {
 
 /// Returns the SMT sort that models the Solidity type _type.
-SortPointer smtSort(frontend::Type const& _type);
+smtutil::SortPointer smtSort(frontend::Type const& _type);
-std::vector<SortPointer> smtSort(std::vector<frontend::TypePointer> const& _types);
+std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> const& _types);
 /// If _type has type Function, abstract it to Integer.
 /// Otherwise return smtSort(_type).
-SortPointer smtSortAbstractFunction(frontend::Type const& _type);
+smtutil::SortPointer smtSortAbstractFunction(frontend::Type const& _type);
-std::vector<SortPointer> smtSortAbstractFunction(std::vector<frontend::TypePointer> const& _types);
+std::vector<smtutil::SortPointer> smtSortAbstractFunction(std::vector<frontend::TypePointer> const& _types);
 /// Returns the SMT kind that models the Solidity type type category _category.
-Kind smtKind(frontend::Type::Category _category);
+smtutil::Kind smtKind(frontend::Type::Category _category);
 
 /// Returns true if type is fully supported (declaration and operations).
 bool isSupportedType(frontend::Type::Category _category);
@@ -61,14 +61,14 @@ bool isStringLiteral(frontend::Type::Category _category);
 /// which is true for unsupported types.
 std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(frontend::Type const& _type, std::string const& _uniqueName, EncodingContext& _context);
 
-Expression minValue(frontend::IntegerType const& _type);
+smtutil::Expression minValue(frontend::IntegerType const& _type);
-Expression maxValue(frontend::IntegerType const& _type);
+smtutil::Expression maxValue(frontend::IntegerType const& _type);
-Expression zeroValue(frontend::TypePointer const& _type);
+smtutil::Expression zeroValue(frontend::TypePointer const& _type);
 
 void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context);
-void setSymbolicZeroValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
+void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
 void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context);
-void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
+void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
 
-std::optional<Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to);
+std::optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to);
 }

libsolidity/formal/SymbolicVariables.cpp

@@ -22,6 +22,7 @@
 
 using namespace std;
 using namespace solidity;
+using namespace solidity::smtutil;
 using namespace solidity::frontend;
 using namespace solidity::frontend::smt;
 
@@ -55,7 +56,7 @@ SymbolicVariable::SymbolicVariable(
 	solAssert(m_sort, "");
 }
 
-smt::Expression SymbolicVariable::currentValue(frontend::TypePointer const&) const
+smtutil::Expression SymbolicVariable::currentValue(frontend::TypePointer const&) const
 {
 	return valueAtIndex(m_ssa->index());
 }
@@ -65,7 +66,7 @@ string SymbolicVariable::currentName() const
 	return uniqueSymbol(m_ssa->index());
 }
 
-smt::Expression SymbolicVariable::valueAtIndex(int _index) const
+smtutil::Expression SymbolicVariable::valueAtIndex(int _index) const
 {
 	return m_context.newVariable(uniqueSymbol(_index), m_sort);
 }
@@ -80,19 +81,19 @@ string SymbolicVariable::uniqueSymbol(unsigned _index) const
 	return m_uniqueName + "_" + to_string(_index);
 }
 
-smt::Expression SymbolicVariable::resetIndex()
+smtutil::Expression SymbolicVariable::resetIndex()
 {
 	m_ssa->resetIndex();
 	return currentValue();
 }
 
-smt::Expression SymbolicVariable::setIndex(unsigned _index)
+smtutil::Expression SymbolicVariable::setIndex(unsigned _index)
 {
 	m_ssa->setIndex(_index);
 	return currentValue();
 }
 
-smt::Expression SymbolicVariable::increaseIndex()
+smtutil::Expression SymbolicVariable::increaseIndex()
 {
 	++(*m_ssa);
 	return currentValue();
@@ -159,39 +160,39 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
 	solAssert(m_sort->kind == Kind::Function, "");
 }
 
-smt::Expression SymbolicFunctionVariable::currentValue(frontend::TypePointer const& _targetType) const
+smtutil::Expression SymbolicFunctionVariable::currentValue(frontend::TypePointer const& _targetType) const
 {
 	return m_abstract.currentValue(_targetType);
 }
 
-smt::Expression SymbolicFunctionVariable::currentFunctionValue() const
+smtutil::Expression SymbolicFunctionVariable::currentFunctionValue() const
 {
 	return m_declaration;
 }
 
-smt::Expression SymbolicFunctionVariable::valueAtIndex(int _index) const
+smtutil::Expression SymbolicFunctionVariable::valueAtIndex(int _index) const
 {
 	return m_abstract.valueAtIndex(_index);
 }
 
-smt::Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const
+smtutil::Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const
 {
 	return SymbolicVariable::valueAtIndex(_index);
 }
 
-smt::Expression SymbolicFunctionVariable::resetIndex()
+smtutil::Expression SymbolicFunctionVariable::resetIndex()
 {
 	SymbolicVariable::resetIndex();
 	return m_abstract.resetIndex();
 }
 
-smt::Expression SymbolicFunctionVariable::setIndex(unsigned _index)
+smtutil::Expression SymbolicFunctionVariable::setIndex(unsigned _index)
 {
 	SymbolicVariable::setIndex(_index);
 	return m_abstract.setIndex(_index);
 }
 
-smt::Expression SymbolicFunctionVariable::increaseIndex()
+smtutil::Expression SymbolicFunctionVariable::increaseIndex()
 {
 	++(*m_ssa);
 	resetDeclaration();
@@ -199,7 +200,7 @@ smt::Expression SymbolicFunctionVariable::increaseIndex()
 	return m_abstract.currentValue();
 }
 
-smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _arguments) const
+smtutil::Expression SymbolicFunctionVariable::operator()(vector<smtutil::Expression> _arguments) const
 {
 	return m_declaration(_arguments);
 }
@@ -246,17 +247,17 @@ vector<SortPointer> const& SymbolicTupleVariable::components()
 	return tupleSort->components;
 }
 
-smt::Expression SymbolicTupleVariable::component(
+smtutil::Expression SymbolicTupleVariable::component(
 	size_t _index,
 	TypePointer _fromType,
 	TypePointer _toType
 )
 {
-	optional<smt::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
+	optional<smtutil::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
 	if (conversion)
 		return *conversion;
 
-	return smt::Expression::tuple_get(currentValue(), _index);
+	return smtutil::Expression::tuple_get(currentValue(), _index);
 }
 
 SymbolicArrayVariable::SymbolicArrayVariable(
@@ -294,26 +295,26 @@ SymbolicArrayVariable::SymbolicArrayVariable(
 	solAssert(m_sort->kind == Kind::Array, "");
 }
 
-smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
+smtutil::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
 {
-	optional<smt::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
+	optional<smtutil::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
 	if (conversion)
 		return *conversion;
 
 	return m_pair.currentValue();
 }
 
-smt::Expression SymbolicArrayVariable::valueAtIndex(int _index) const
+smtutil::Expression SymbolicArrayVariable::valueAtIndex(int _index) const
 {
 	return m_pair.valueAtIndex(_index);
 }
 
-smt::Expression SymbolicArrayVariable::elements()
+smtutil::Expression SymbolicArrayVariable::elements()
 {
 	return m_pair.component(0);
 }
 
-smt::Expression SymbolicArrayVariable::length()
+smtutil::Expression SymbolicArrayVariable::length()
 {
 	return m_pair.component(1);
 }

libsolidity/formal/SymbolicVariables.h

@@ -17,10 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/formal/SSAVariable.h>
 #include <libsolidity/ast/Types.h>
 #include <libsolidity/ast/TypeProvider.h>
+
+#include <libsmtutil/SolverInterface.h>
 #include <memory>
 
 namespace solidity::frontend::smt
@@ -42,7 +43,7 @@ public:
 		EncodingContext& _context
 	);
 	SymbolicVariable(
-		SortPointer _sort,
+		smtutil::SortPointer _sort,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -51,14 +52,14 @@ public:
 
 	virtual ~SymbolicVariable() = default;
 
-	virtual Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const;
+	virtual smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const;
 	std::string currentName() const;
-	virtual Expression valueAtIndex(int _index) const;
+	virtual smtutil::Expression valueAtIndex(int _index) const;
 	virtual std::string nameAtIndex(int _index) const;
-	virtual Expression resetIndex();
+	virtual smtutil::Expression resetIndex();
-	virtual Expression setIndex(unsigned _index);
+	virtual smtutil::Expression setIndex(unsigned _index);
-	virtual Expression increaseIndex();
+	virtual smtutil::Expression increaseIndex();
-	virtual Expression operator()(std::vector<Expression> /*_arguments*/) const
+	virtual smtutil::Expression operator()(std::vector<smtutil::Expression> /*_arguments*/) const
 	{
 		solAssert(false, "Function application to non-function.");
 	}
@@ -66,7 +67,7 @@ public:
 	unsigned index() const { return m_ssa->index(); }
 	unsigned& index() { return m_ssa->index(); }
 
-	SortPointer const& sort() const { return m_sort; }
+	smtutil::SortPointer const& sort() const { return m_sort; }
 	frontend::TypePointer const& type() const { return m_type; }
 	frontend::TypePointer const& originalType() const { return m_originalType; }
 
@@ -74,7 +75,7 @@ protected:
 	std::string uniqueSymbol(unsigned _index) const;
 
 	/// SMT sort.
-	SortPointer m_sort;
+	smtutil::SortPointer m_sort;
 	/// Solidity type, used for size and range in number types.
 	frontend::TypePointer m_type;
 	/// Solidity original type, used for type conversion if necessary.
@@ -154,33 +155,33 @@ public:
 		EncodingContext& _context
 	);
 	SymbolicFunctionVariable(
-		SortPointer _sort,
+		smtutil::SortPointer _sort,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
 
-	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+	smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
 
 	// Explicit request the function declaration.
-	Expression currentFunctionValue() const;
+	smtutil::Expression currentFunctionValue() const;
 
-	Expression valueAtIndex(int _index) const override;
+	smtutil::Expression valueAtIndex(int _index) const override;
 
 	// Explicit request the function declaration.
-	Expression functionValueAtIndex(int _index) const;
+	smtutil::Expression functionValueAtIndex(int _index) const;
 
-	Expression resetIndex() override;
+	smtutil::Expression resetIndex() override;
-	Expression setIndex(unsigned _index) override;
+	smtutil::Expression setIndex(unsigned _index) override;
-	Expression increaseIndex() override;
+	smtutil::Expression increaseIndex() override;
 
-	Expression operator()(std::vector<Expression> _arguments) const override;
+	smtutil::Expression operator()(std::vector<smtutil::Expression> _arguments) const override;
 
 private:
 	/// Creates a new function declaration.
 	void resetDeclaration();
 
 	/// Stores the current function declaration.
-	Expression m_declaration;
+	smtutil::Expression m_declaration;
 
 	/// Abstract representation.
 	SymbolicIntVariable m_abstract{
@@ -216,13 +217,13 @@ public:
 		EncodingContext& _context
 	);
 	SymbolicTupleVariable(
-		SortPointer _sort,
+		smtutil::SortPointer _sort,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
 
-	std::vector<SortPointer> const& components();
+	std::vector<smtutil::SortPointer> const& components();
-	Expression component(
+	smtutil::Expression component(
 		size_t _index,
 		TypePointer _fromType = nullptr,
 		TypePointer _toType = nullptr
@@ -242,22 +243,22 @@ public:
 		EncodingContext& _context
 	);
 	SymbolicArrayVariable(
-		SortPointer _sort,
+		smtutil::SortPointer _sort,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
 
 	SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
 
-	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+	smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
-	Expression valueAtIndex(int _index) const override;
+	smtutil::Expression valueAtIndex(int _index) const override;
-	Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); }
+	smtutil::Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); }
-	Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); }
+	smtutil::Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); }
-	Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); }
+	smtutil::Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); }
-	Expression elements();
+	smtutil::Expression elements();
-	Expression length();
+	smtutil::Expression length();
 
-	SortPointer tupleSort() { return m_pair.sort(); }
+	smtutil::SortPointer tupleSort() { return m_pair.sort(); }
 
 private:
 	SymbolicTupleVariable m_pair;

libsolidity/interface/CompilerStack.cpp

@@ -82,7 +82,7 @@ static int g_compilerStackCounts = 0;
 
 CompilerStack::CompilerStack(ReadCallback::Callback _readFile):
 	m_readFile{std::move(_readFile)},
-	m_enabledSMTSolvers{smt::SMTSolverChoice::All()},
+	m_enabledSMTSolvers{smtutil::SMTSolverChoice::All()},
 	m_generateIR{false},
 	m_generateEwasm{false},
 	m_errorList{},
@@ -136,7 +136,7 @@ void CompilerStack::setEVMVersion(langutil::EVMVersion _version)
 	m_evmVersion = _version;
 }
 
-void CompilerStack::setSMTSolverChoice(smt::SMTSolverChoice _enabledSMTSolvers)
+void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers)
 {
 	if (m_stackState >= ParsingPerformed)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled SMT solvers before parsing."));
@@ -205,7 +205,7 @@ void CompilerStack::reset(bool _keepSettings)
 		m_remappings.clear();
 		m_libraries.clear();
 		m_evmVersion = langutil::EVMVersion();
-		m_enabledSMTSolvers = smt::SMTSolverChoice::All();
+		m_enabledSMTSolvers = smtutil::SMTSolverChoice::All();
 		m_generateIR = false;
 		m_generateEwasm = false;
 		m_revertStrings = RevertStrings::Default;
@@ -582,9 +582,9 @@ string const* CompilerStack::sourceMapping(string const& _contractName) const
 	if (!c.sourceMapping)
 	{
 		if (auto items = assemblyItems(_contractName))
-			c.sourceMapping = make_unique<string>(evmasm::AssemblyItem::computeSourceMapping(*items, sourceIndices()));
+			c.sourceMapping.emplace(evmasm::AssemblyItem::computeSourceMapping(*items, sourceIndices()));
 	}
-	return c.sourceMapping.get();
+	return c.sourceMapping ? &*c.sourceMapping : nullptr;
 }
 
 string const* CompilerStack::runtimeSourceMapping(string const& _contractName) const
@@ -596,11 +596,11 @@ string const* CompilerStack::runtimeSourceMapping(string const& _contractName) c
 	if (!c.runtimeSourceMapping)
 	{
 		if (auto items = runtimeAssemblyItems(_contractName))
-			c.runtimeSourceMapping = make_unique<string>(
+			c.runtimeSourceMapping.emplace(
 				evmasm::AssemblyItem::computeSourceMapping(*items, sourceIndices())
 			);
 	}
-	return c.runtimeSourceMapping.get();
+	return c.runtimeSourceMapping ? &*c.runtimeSourceMapping : nullptr;
 }
 
 std::string const CompilerStack::filesystemFriendlyName(string const& _contractName) const

libsolidity/interface/CompilerStack.h

@@ -27,7 +27,8 @@
 #include <libsolidity/interface/OptimiserSettings.h>
 #include <libsolidity/interface/Version.h>
 #include <libsolidity/interface/DebugSettings.h>
-#include <libsolidity/formal/SolverInterface.h>
+
+#include <libsmtutil/SolverInterface.h>
 
 #include <liblangutil/ErrorReporter.h>
 #include <liblangutil/EVMVersion.h>
@@ -163,7 +164,7 @@ public:
 	void setEVMVersion(langutil::EVMVersion _version = langutil::EVMVersion{});
 
 	/// Set which SMT solvers should be enabled.
-	void setSMTSolverChoice(smt::SMTSolverChoice _enabledSolvers);
+	void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers);
 
 	/// Sets the requested contract names by source.
 	/// If empty, no filtering is performed and every contract
@@ -348,8 +349,8 @@ private:
 		util::LazyInit<Json::Value const> storageLayout;
 		util::LazyInit<Json::Value const> userDocumentation;
 		util::LazyInit<Json::Value const> devDocumentation;
-		mutable std::unique_ptr<std::string const> sourceMapping;
+		mutable std::optional<std::string const> sourceMapping;
-		mutable std::unique_ptr<std::string const> runtimeSourceMapping;
+		mutable std::optional<std::string const> runtimeSourceMapping;
 	};
 
 	/// Loads the missing sources from @a _ast (named @a _path) using the callback
@@ -433,7 +434,7 @@ private:
 	OptimiserSettings m_optimiserSettings;
 	RevertStrings m_revertStrings = RevertStrings::Default;
 	langutil::EVMVersion m_evmVersion;
-	smt::SMTSolverChoice m_enabledSMTSolvers;
+	smtutil::SMTSolverChoice m_enabledSMTSolvers;
 	std::map<std::string, std::set<std::string>> m_requestedContractNames;
 	bool m_generateIR;
 	bool m_generateEwasm;

libsolidity/interface/Natspec.cpp

@@ -40,7 +40,7 @@ Json::Value Natspec::userDocumentation(ContractDefinition const& _contractDef)
 	auto constructorDefinition(_contractDef.constructor());
 	if (constructorDefinition)
 	{
-		string value = extractDoc(constructorDefinition->annotation().docTags, "notice");
+		string const value = extractDoc(constructorDefinition->annotation().docTags, "notice");
 		if (!value.empty())
 		{
 			// add the constructor, only if we have any documentation to add
@@ -56,6 +56,7 @@ Json::Value Natspec::userDocumentation(ContractDefinition const& _contractDef)
 
 	for (auto const& it: _contractDef.interfaceFunctions())
 		if (it.second->hasDeclaration())
+		{
 			if (auto const* f = dynamic_cast<FunctionDefinition const*>(&it.second->declaration()))
 			{
 				string value = extractDoc(f->annotation().docTags, "notice");
@@ -67,6 +68,19 @@ Json::Value Natspec::userDocumentation(ContractDefinition const& _contractDef)
 					methods[it.second->externalSignature()] = user;
 				}
 			}
+			else if (auto var = dynamic_cast<VariableDeclaration const*>(&it.second->declaration()))
+			{
+				solAssert(var->isStateVariable() && var->isPublic(), "");
+				string value = extractDoc(var->annotation().docTags, "notice");
+				if (!value.empty())
+				{
+					Json::Value user;
+					// since @notice is the only user tag if missing function should not appear
+					user["notice"] = Json::Value(value);
+					methods[it.second->externalSignature()] = user;
+				}
+			}
+		}
 	doc["methods"] = methods;
 
 	return doc;
@@ -114,7 +128,20 @@ Json::Value Natspec::devDocumentation(ContractDefinition const& _contractDef)
 		}
 	}
 
+	Json::Value stateVariables(Json::objectValue);
+	for (VariableDeclaration const* varDecl: _contractDef.stateVariables())
+	{
+		if (auto devDoc = devDocumentation(varDecl->annotation().docTags); !devDoc.empty())
+			stateVariables[varDecl->name()] = devDoc;
+
+		solAssert(varDecl->annotation().docTags.count("return") <= 1, "");
+		if (varDecl->annotation().docTags.count("return") == 1)
+			stateVariables[varDecl->name()]["return"] = extractDoc(varDecl->annotation().docTags, "return");
+	}
+
 	doc["methods"] = methods;
+	if (!stateVariables.empty())
+		doc["stateVariables"] = stateVariables;
 
 	return doc;
 }

libsolidity/interface/StandardCompiler.cpp

@@ -28,6 +28,7 @@
 #include <libyul/optimiser/Suite.h>
 #include <liblangutil/SourceReferenceFormatter.h>
 #include <libevmasm/Instruction.h>
+#include <libsmtutil/Exceptions.h>
 #include <libsolutil/JSON.h>
 #include <libsolutil/Keccak256.h>
 #include <libsolutil/CommonData.h>
@@ -921,6 +922,16 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 			"Yul exception"
 		));
 	}
+	catch (smtutil::SMTLogicError const& _exception)
+	{
+		errors.append(formatErrorWithException(
+			_exception,
+			false,
+			"SMTLogicException",
+			"general",
+			"SMT logic exception"
+		));
+	}
 	catch (util::Exception const& _exception)
 	{
 		errors.append(formatError(

libsolidity/parsing/DocStringParser.cpp

@@ -77,10 +77,9 @@ string::const_iterator skipWhitespace(
 
 }
 
-bool DocStringParser::parse(string const& _docString, ErrorReporter& _errorReporter)
+void DocStringParser::parse(string const& _docString, ErrorReporter& _errorReporter)
 {
 	m_errorReporter = &_errorReporter;
-	m_errorsOccurred = false;
 	m_lastTag = nullptr;
 
 	auto currPos = _docString.begin();
@@ -119,7 +118,6 @@ bool DocStringParser::parse(string const& _docString, ErrorReporter& _errorRepor
 			currPos = nlPos + 1;
 		}
 	}
-	return !m_errorsOccurred;
 }
 
 DocStringParser::iter DocStringParser::parseDocTagLine(iter _pos, iter _end, bool _appending)
@@ -194,6 +192,5 @@ void DocStringParser::newTag(string const& _tagName)
 
 void DocStringParser::appendError(string const& _description)
 {
-	m_errorsOccurred = true;
 	m_errorReporter->docstringParsingError(9440_error, _description);
 }

libsolidity/parsing/DocStringParser.h

@@ -37,8 +37,7 @@ class DocStringParser
 {
 public:
 	/// Parse the given @a _docString and stores the parsed components internally.
-	/// @returns false on error and appends the error to @a _errors.
+	void parse(std::string const& _docString, langutil::ErrorReporter& _errorReporter);
-	bool parse(std::string const& _docString, langutil::ErrorReporter& _errorReporter);
 
 	std::multimap<std::string, DocTag> const& tags() const { return m_docTags; }
 
@@ -65,7 +64,6 @@ private:
 	std::multimap<std::string, DocTag> m_docTags;
 	DocTag* m_lastTag = nullptr;
 	langutil::ErrorReporter* m_errorReporter = nullptr;
-	bool m_errorsOccurred = false;
 };
 
 }

libsolidity/parsing/Parser.cpp

@@ -686,6 +686,7 @@ ASTPointer<VariableDeclaration> Parser::parseVariableDeclaration(
 	ASTNodeFactory nodeFactory = _lookAheadArrayType ?
 		ASTNodeFactory(*this, _lookAheadArrayType) : ASTNodeFactory(*this);
 	ASTPointer<TypeName> type;
+	ASTPointer<StructuredDocumentation> const documentation = parseStructuredDocumentation();
 	if (_lookAheadArrayType)
 		type = _lookAheadArrayType;
 	else
@@ -695,6 +696,9 @@ ASTPointer<VariableDeclaration> Parser::parseVariableDeclaration(
 			nodeFactory.setEndPositionFromNode(type);
 	}
 
+	if (!_options.isStateVariable && documentation != nullptr)
+		parserWarning(2837_error, "Only state variables can have a docstring. This will be disallowed in 0.7.0.");
+
 	if (dynamic_cast<FunctionTypeName*>(type.get()) && _options.isStateVariable && m_scanner->currentToken() == Token::LBrace)
 		fatalParserError(
 			2915_error,
@@ -809,6 +813,7 @@ ASTPointer<VariableDeclaration> Parser::parseVariableDeclaration(
 		identifier,
 		value,
 		visibility,
+		documentation,
 		_options.isStateVariable,
 		isIndexed,
 		mutability,

libyul/backends/wasm/WasmAST.h

@@ -25,6 +25,7 @@
 #include <vector>
 #include <map>
 #include <memory>
+#include <optional>
 
 namespace solidity::yul::wasm
 {
@@ -76,7 +77,7 @@ struct FunctionImport {
 	std::string externalName;
 	std::string internalName;
 	std::vector<std::string> paramTypes;
-	std::unique_ptr<std::string> returnType;
+	std::optional<std::string> returnType;
 };
 
 struct FunctionDefinition

libyul/backends/wasm/WasmCodeTransform.cpp

@@ -29,6 +29,8 @@
 
 #include <liblangutil/Exceptions.h>
 
+#include <optional>
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::yul;
@@ -125,7 +127,7 @@ wasm::Expression WasmCodeTransform::operator()(FunctionCall const& _call)
 					builtin->name.str().substr(4),
 					builtin->name.str(),
 					{},
-					builtin->returns.empty() ? nullptr : make_unique<string>(builtin->returns.front().str())
+					builtin->returns.empty() ? nullopt : make_optional<string>(builtin->returns.front().str())
 				};
 				for (auto const& param: builtin->parameters)
 					imp.paramTypes.emplace_back(param.str());
@@ -252,6 +254,7 @@ wasm::Expression WasmCodeTransform::operator()(ForLoop const& _for)
 	m_breakContinueLabelNames.push({breakLabel, continueLabel});
 
 	wasm::Loop loop;
+	loop.labelName = newLabel();
 	loop.statements = visit(_for.pre.statements);
 	loop.statements.emplace_back(wasm::BreakIf{wasm::Label{breakLabel}, make_unique<wasm::Expression>(
 		wasm::BuiltinCall{"i64.eqz", make_vector<wasm::Expression>(
@@ -260,6 +263,7 @@ wasm::Expression WasmCodeTransform::operator()(ForLoop const& _for)
 	)});
 	loop.statements.emplace_back(wasm::Block{continueLabel, visit(_for.body.statements)});
 	loop.statements += visit(_for.post.statements);
+	loop.statements.emplace_back(wasm::Break{wasm::Label{loop.labelName}});
 
 	return { wasm::Block{breakLabel, make_vector<wasm::Expression>(move(loop))} };
 }

libyul/optimiser/Metrics.cpp

@@ -36,30 +36,71 @@ using namespace solidity;
 using namespace solidity::yul;
 using namespace solidity::util;
 
-size_t CodeSize::codeSize(Statement const& _statement)
+size_t CodeWeights::costOf(Statement const& _statement) const
 {
-	CodeSize cs;
+	if (holds_alternative<ExpressionStatement>(_statement))
+		return expressionStatementCost;
+	else if (holds_alternative<Assignment>(_statement))
+		return assignmentCost;
+	else if (holds_alternative<VariableDeclaration>(_statement))
+		return variableDeclarationCost;
+	else if (holds_alternative<FunctionDefinition>(_statement))
+		return functionDefinitionCost;
+	else if (holds_alternative<If>(_statement))
+		return ifCost;
+	else if (holds_alternative<Switch>(_statement))
+		return switchCost + caseCost * std::get<Switch>(_statement).cases.size();
+	else if (holds_alternative<ForLoop>(_statement))
+		return forLoopCost;
+	else if (holds_alternative<Break>(_statement))
+		return breakCost;
+	else if (holds_alternative<Continue>(_statement))
+		return continueCost;
+	else if (holds_alternative<Leave>(_statement))
+		return leaveCost;
+	else if (holds_alternative<Block>(_statement))
+		return blockCost;
+	else
+		yulAssert(false, "If you add a new statement type, you must update CodeWeights.");
+}
+
+size_t CodeWeights::costOf(Expression const& _expression) const
+{
+	if (holds_alternative<FunctionCall>(_expression))
+		return functionCallCost;
+	else if (holds_alternative<Identifier>(_expression))
+		return identifierCost;
+	else if (holds_alternative<Literal>(_expression))
+		return literalCost;
+	else
+		yulAssert(false, "If you add a new expression type, you must update CodeWeights.");
+}
+
+
+size_t CodeSize::codeSize(Statement const& _statement, CodeWeights const& _weights)
+{
+	CodeSize cs(true, _weights);
 	cs.visit(_statement);
 	return cs.m_size;
 }
 
-size_t CodeSize::codeSize(Expression const& _expression)
+size_t CodeSize::codeSize(Expression const& _expression, CodeWeights const& _weights)
 {
-	CodeSize cs;
+	CodeSize cs(true, _weights);
 	cs.visit(_expression);
 	return cs.m_size;
 }
 
-size_t CodeSize::codeSize(Block const& _block)
+size_t CodeSize::codeSize(Block const& _block, CodeWeights const& _weights)
 {
-	CodeSize cs;
+	CodeSize cs(true, _weights);
 	cs(_block);
 	return cs.m_size;
 }
 
-size_t CodeSize::codeSizeIncludingFunctions(Block const& _block)
+size_t CodeSize::codeSizeIncludingFunctions(Block const& _block, CodeWeights const& _weights)
 {
-	CodeSize cs(false);
+	CodeSize cs(false, _weights);
 	cs(_block);
 	return cs.m_size;
 }
@@ -68,32 +109,14 @@ void CodeSize::visit(Statement const& _statement)
 {
 	if (holds_alternative<FunctionDefinition>(_statement) && m_ignoreFunctions)
 		return;
-	else if (
-		holds_alternative<If>(_statement) ||
-		holds_alternative<Break>(_statement) ||
-		holds_alternative<Continue>(_statement) ||
-		holds_alternative<Leave>(_statement)
-	)
-		m_size += 2;
-	else if (holds_alternative<ForLoop>(_statement))
-		m_size += 3;
-	else if (holds_alternative<Switch>(_statement))
-		m_size += 1 + 2 * std::get<Switch>(_statement).cases.size();
-	else if (!(
-		holds_alternative<Block>(_statement) ||
-		holds_alternative<ExpressionStatement>(_statement) ||
-		holds_alternative<Assignment>(_statement) ||
-		holds_alternative<VariableDeclaration>(_statement)
-	))
-		++m_size;
 
+	m_size += m_weights.costOf(_statement);
 	ASTWalker::visit(_statement);
 }
 
 void CodeSize::visit(Expression const& _expression)
 {
-	if (!holds_alternative<Identifier>(_expression))
+	m_size += m_weights.costOf(_expression);
-		++m_size;
 	ASTWalker::visit(_expression);
 }
 

libyul/optimiser/Metrics.h

@@ -30,33 +30,67 @@ struct Dialect;
 struct EVMDialect;
 
 /**
- * Metric for the size of code.
+ * Weights to be assigned to specific yul statements and expressions by a metric.
- * More specifically, the number of AST nodes.
- * Ignores function definitions while traversing the AST by default.
- * If you want to know the size of a function, you have to invoke this on its body.
  *
- * As an exception, the following AST elements have a cost of zero:
+ * The default values are meant to reflect specifically the number of AST nodes.
+ *
+ * The following AST elements have a default cost of zero (because the cleanup phase would
+ * remove them anyway or they are just wrappers around something else will be counted instead):
  *  - expression statement (only the expression inside has a cost)
  *  - block (only the statements inside have a cost)
  *  - variable references
  *  - variable declarations (only the right hand side has a cost)
  *  - assignments (only the value has a cost)
  *
- * As another exception, each statement incurs and additional cost of one
+ * Each statement incurs and additional cost of one
  * per jump/branch. This means if, break and continue statements have a cost of 2,
  * switch statements have a cost of 1 plus the number of cases times two,
  * and for loops cost 3.
+*/
+struct CodeWeights
+{
+	// Statements
+	size_t expressionStatementCost = 0;
+	size_t assignmentCost = 0;
+	size_t variableDeclarationCost = 0;
+	size_t functionDefinitionCost = 1;
+	size_t ifCost = 2;
+	size_t switchCost = 1;
+	size_t caseCost = 2;
+	size_t forLoopCost = 3;
+	size_t breakCost = 2;
+	size_t continueCost = 2;
+	size_t leaveCost = 2;
+	size_t blockCost = 0;
+
+	// Expressions
+	size_t functionCallCost = 1;
+	size_t identifierCost = 0;
+	size_t literalCost = 1;
+
+	size_t costOf(Statement const& _statement) const;
+	size_t costOf(Expression const& _expression) const;
+};
+
+/**
+ * Metric for the size of code.
+ * Ignores function definitions while traversing the AST by default.
+ * If you want to know the size of a function, you have to invoke this on its body.
+ *
+ * The cost of each statement and expression type is configurable via CodeWeights.
  */
 class CodeSize: public ASTWalker
 {
 public:
-	static size_t codeSize(Statement const& _statement);
+	static size_t codeSize(Statement const& _statement, CodeWeights const& _weights = {});
-	static size_t codeSize(Expression const& _expression);
+	static size_t codeSize(Expression const& _expression, CodeWeights const& _weights = {});
-	static size_t codeSize(Block const& _block);
+	static size_t codeSize(Block const& _block, CodeWeights const& _weights = {});
-	static size_t codeSizeIncludingFunctions(Block const& _block);
+	static size_t codeSizeIncludingFunctions(Block const& _block, CodeWeights const& _weights = {});
 
 private:
-	CodeSize(bool _ignoreFunctions = true): m_ignoreFunctions(_ignoreFunctions) {}
+	CodeSize(bool _ignoreFunctions = true, CodeWeights const& _weights = {}):
+		m_ignoreFunctions(_ignoreFunctions),
+		m_weights(_weights) {}
 
 	void visit(Statement const& _statement) override;
 	void visit(Expression const& _expression) override;
@@ -64,6 +98,7 @@ private:
 private:
 	bool m_ignoreFunctions;
 	size_t m_size = 0;
+	CodeWeights m_weights;
 };
 
 /**

solc/CommandLineInterface.cpp

@@ -47,6 +47,8 @@
 #include <liblangutil/SourceReferenceFormatter.h>
 #include <liblangutil/SourceReferenceFormatterHuman.h>
 
+#include <libsmtutil/Exceptions.h>
+
 #include <libsolutil/Common.h>
 #include <libsolutil/CommonData.h>
 #include <libsolutil/CommonIO.h>
@@ -1297,6 +1299,14 @@ bool CommandLineInterface::processInput()
 			boost::diagnostic_information(_exception);
 		return false;
 	}
+	catch (smtutil::SMTLogicError const& _exception)
+	{
+		serr() <<
+			"SMT logic error during analysis:" <<
+			endl <<
+			boost::diagnostic_information(_exception);
+		return false;
+	}
 	catch (Error const& _error)
 	{
 		if (_error.type() == Error::Type::DocstringParsingError)

test/CMakeLists.txt

@@ -188,7 +188,7 @@ add_executable(soltest ${sources}
     ${libsolidity_util_sources}
     ${yul_phaser_sources}
 )
-target_link_libraries(soltest PRIVATE libsolc yul solidity yulInterpreter evmasm solutil Boost::boost Boost::filesystem Boost::program_options Boost::unit_test_framework evmc)
+target_link_libraries(soltest PRIVATE libsolc yul solidity smtutil solutil Boost::boost yulInterpreter evmasm Boost::filesystem Boost::program_options Boost::unit_test_framework evmc)
 
 
 # Special compilation flag for Visual Studio (version 2019 at least affected)

test/boostTest.cpp

@@ -89,7 +89,10 @@ int registerTests(
 	}
 	else
 	{
-		static vector<unique_ptr<string>> filenames;
+		// This must be a vector of unique_ptrs because Boost.Test keeps the equivalent of a string_view to the filename
+		// that is passed in. If the strings were stored directly in the vector, pointers/references to them would be
+		// invalidated on reallocation.
+		static vector<unique_ptr<string const>> filenames;
 
 		filenames.emplace_back(make_unique<string>(_path.string()));
 		_suite.add(make_test_case(

test/cmdlineTests/evm_to_wasm_break/output

@@ -154,7 +154,7 @@ object "object" {
 
 
 Binary representation:
-0061736d0100000001480a60000060017e017e60027e7e017e60037e7e7e017e60047e7e7e7e017e60057e7e7e7e7e0060087e7e7e7e7e7e7e7e0060087e7e7e7e7e7e7e7e017e60027f7f0060037f7f7f0002310208657468657265756d0c73746f7261676553746f7265000808657468657265756d0c63616c6c44617461436f70790009030e0d0003070407020704010101050605030100010610037e0142000b7e0142000b7e0142000b071102066d656d6f72790200046d61696e00020a80090dee02011f7e4200210002402000200020002000100921012300210223012103230221040b2001210520022106200321072004210842012109200020008420002009848450ada745ada745ad210a02400340200aa745ad500d01024002402005200620072008200020002000420a1008210b2300210c2301210d2302210e0b0240200b200c200d200e1005210f2300211023012111230221120b200f20108420112012848450ada745ad42005204400c030b024020052006200720082000200020004202100621132300211423012115230221160b201320148420152016848450ada745ad42005204400c030b0240200520062007200820002000200042041006211723002118230121192302211a0b20172018842019201a848450ada745ad42005204400c010b0b0240200520062007200820002000200020091004211b2300211c2301211d2302211e0b201b2105201c2106201d2107201e21080b0b20002000200020002005200620072008100e0b2c01037e200020017c2105200520027c21032005200054ada72003200554ada772ada7ad21042004240020030b6f010b7e200320077c210c200c42007c210b024020022006200c200354ada7200b200c54ada772ada7ad1003210d2300210e0b200d210a024020012005200e1003210f230021100b200f2109024020002004201010032111230021120b2011210820092400200a2401200b240220080b2301047e200020018420022003848450ada7ad210720052400200624012007240220040b4601047e2000200451ad42005204402001200551ad42005204402002200651ad42005204402003200751ad42005204404201210b0b0b0b0b20092400200a2401200b240220080b2a01027e02402000200154ad21032003420151044042ffffffff0f2102052000200152ad21020b0b20020b930101087e4200210c0240200020041007210d200d42005104400240200120051007210e200e42005104400240200220061007210f200f42005104402003200754ad210c05200f42015104404200210c054201210c0b0b0b05200e42015104404200210c054201210c0b0b0b05200d42015104404200210c054201210c0b0b0b200ca7ad210b20092400200a2401200b240220080b8c0101087e4200200020018420028452ad4200520440000b4200200342208852ad4200520440000b4200a72003a7ada74220a710014200a7290300100c21084200a74208a76aada7290300100c21094200a74210a76aada7290300100c210a4200a74218a76aada7290300100c210b2008210420092105200a2106200b210720052400200624012007240220040b1c01017e20004208864280fe0383200042088842ff018384210120010b1b01027e2000100a421086210220022000421088100a84210120010b1b01027e2000100b422086210220022000422088100b84210120010b3e01007e2000a72001100c3703002000a74208a76aada72002100c3703002000a74210a76aada72003100c3703002000a74218a76aada72004100c3703000b2401007e42002000200120022003100d42202004200520062007100d4200a74220a710000b
+0061736d0100000001480a60000060017e017e60027e7e017e60037e7e7e017e60047e7e7e7e017e60057e7e7e7e7e0060087e7e7e7e7e7e7e7e0060087e7e7e7e7e7e7e7e017e60027f7f0060037f7f7f0002310208657468657265756d0c73746f7261676553746f7265000808657468657265756d0c63616c6c44617461436f70790009030e0d0003070407020704010101050605030100010610037e0142000b7e0142000b7e0142000b071102066d656d6f72790200046d61696e00020a82090df002011f7e4200210002402000200020002000100921012300210223012103230221040b2001210520022106200321072004210842012109200020008420002009848450ada745ada745ad210a02400340200aa745ad500d01024002402005200620072008200020002000420a1008210b2300210c2301210d2302210e0b0240200b200c200d200e1005210f2300211023012111230221120b200f20108420112012848450ada745ad42005204400c030b024020052006200720082000200020004202100621132300211423012115230221160b201320148420152016848450ada745ad42005204400c030b0240200520062007200820002000200042041006211723002118230121192302211a0b20172018842019201a848450ada745ad42005204400c010b0b0240200520062007200820002000200020091004211b2300211c2301211d2302211e0b201b2105201c2106201d2107201e21080c000b0b20002000200020002005200620072008100e0b2c01037e200020017c2105200520027c21032005200054ada72003200554ada772ada7ad21042004240020030b6f010b7e200320077c210c200c42007c210b024020022006200c200354ada7200b200c54ada772ada7ad1003210d2300210e0b200d210a024020012005200e1003210f230021100b200f2109024020002004201010032111230021120b2011210820092400200a2401200b240220080b2301047e200020018420022003848450ada7ad210720052400200624012007240220040b4601047e2000200451ad42005204402001200551ad42005204402002200651ad42005204402003200751ad42005204404201210b0b0b0b0b20092400200a2401200b240220080b2a01027e02402000200154ad21032003420151044042ffffffff0f2102052000200152ad21020b0b20020b930101087e4200210c0240200020041007210d200d42005104400240200120051007210e200e42005104400240200220061007210f200f42005104402003200754ad210c05200f42015104404200210c054201210c0b0b0b05200e42015104404200210c054201210c0b0b0b05200d42015104404200210c054201210c0b0b0b200ca7ad210b20092400200a2401200b240220080b8c0101087e4200200020018420028452ad4200520440000b4200200342208852ad4200520440000b4200a72003a7ada74220a710014200a7290300100c21084200a74208a76aada7290300100c21094200a74210a76aada7290300100c210a4200a74218a76aada7290300100c210b2008210420092105200a2106200b210720052400200624012007240220040b1c01017e20004208864280fe0383200042088842ff018384210120010b1b01027e2000100a421086210220022000421088100a84210120010b1b01027e2000100b422086210220022000422088100b84210120010b3e01007e2000a72001100c3703002000a74208a76aada72002100c3703002000a74210a76aada72003100c3703002000a74218a76aada72004100c3703000b2401007e42002000200120022003100d42202004200520062007100d4200a74220a710000b
 
 Text representation:
 (module
@@ -213,7 +213,7 @@ Text representation:
     (local.set $_2 (i64.const 1))
     (local.set $_3 (i64.extend_i32_u (i32.eqz (i32.wrap_i64 (i64.extend_i32_u (i32.eqz (i32.wrap_i64 (i64.extend_i32_u (i64.eqz (i64.or (i64.or (local.get $_1) (local.get $_1)) (i64.or (local.get $_1) (local.get $_2))))))))))))
     (block $label_
-        (loop
+        (loop $label__4
             (br_if $label_ (i64.eqz (i64.extend_i32_u (i32.eqz (i32.wrap_i64 (local.get $_3))))))
             (block $label__3
                 (block
@@ -266,6 +266,7 @@ Text representation:
             (local.set $x_5 (local.get $x_9))
             (local.set $x_6 (local.get $x_10))
             (local.set $x_7 (local.get $x_11))
+            (br $label__4)
         )
 
     )
@@ -413,22 +414,22 @@ Text representation:
     (local $z3 i64)
     (local $z4 i64)
     (local $z i64)
-    (local $condition_4 i64)
     (local $condition_5 i64)
     (local $condition_6 i64)
+    (local $condition_7 i64)
     (local.set $z (i64.const 0))
     (block
-        (local.set $condition_4 (call $cmp (local.get $x1) (local.get $y1)))
+        (local.set $condition_5 (call $cmp (local.get $x1) (local.get $y1)))
-        (if (i64.eq (local.get $condition_4) (i64.const 0)) (then
+        (if (i64.eq (local.get $condition_5) (i64.const 0)) (then
             (block
-                (local.set $condition_5 (call $cmp (local.get $x2) (local.get $y2)))
+                (local.set $condition_6 (call $cmp (local.get $x2) (local.get $y2)))
-                (if (i64.eq (local.get $condition_5) (i64.const 0)) (then
+                (if (i64.eq (local.get $condition_6) (i64.const 0)) (then
                     (block
-                        (local.set $condition_6 (call $cmp (local.get $x3) (local.get $y3)))
+                        (local.set $condition_7 (call $cmp (local.get $x3) (local.get $y3)))
-                        (if (i64.eq (local.get $condition_6) (i64.const 0)) (then
+                        (if (i64.eq (local.get $condition_7) (i64.const 0)) (then
                             (local.set $z (i64.extend_i32_u (i64.lt_u (local.get $x4) (local.get $y4))))
                         )(else
-                            (if (i64.eq (local.get $condition_6) (i64.const 1)) (then
+                            (if (i64.eq (local.get $condition_7) (i64.const 1)) (then
                                 (local.set $z (i64.const 0))
                             )(else
                                 (local.set $z (i64.const 1))
@@ -437,7 +438,7 @@ Text representation:
 
                     )
                 )(else
-                    (if (i64.eq (local.get $condition_5) (i64.const 1)) (then
+                    (if (i64.eq (local.get $condition_6) (i64.const 1)) (then
                         (local.set $z (i64.const 0))
                     )(else
                         (local.set $z (i64.const 1))
@@ -446,7 +447,7 @@ Text representation:
 
             )
         )(else
-            (if (i64.eq (local.get $condition_4) (i64.const 1)) (then
+            (if (i64.eq (local.get $condition_5) (i64.const 1)) (then
                 (local.set $z (i64.const 0))
             )(else
                 (local.set $z (i64.const 1))

test/libsolidity/ASTJSON/documentation.json

@@ -85,10 +85,10 @@
   {
     "C":
     [
-      20
+      23
     ]
   },
-  "id": 21,
+  "id": 24,
   "nodeType": "SourceUnit",
   "nodes":
   [
@@ -98,89 +98,126 @@
       "contractDependencies": [],
       "contractKind": "contract",
       "fullyImplemented": true,
-      "id": 20,
+      "id": 23,
       "linearizedBaseContracts":
       [
-        20
+        23
       ],
       "name": "C",
       "nodeType": "ContractDefinition",
       "nodes":
       [
         {
-          "anonymous": false,
+          "constant": false,
           "documentation":
           {
             "id": 7,
             "nodeType": "StructuredDocumentation",
-            "src": "15:26:3",
+            "src": "15:32:3",
-            "text": "Some comment on Evt."
+            "text": "Some comment on state var."
           },
+          "functionSelector": "c19d93fb",
           "id": 9,
-          "name": "Evt",
+          "mutability": "mutable",
-          "nodeType": "EventDefinition",
+          "name": "state",
-          "parameters":
+          "nodeType": "VariableDeclaration",
+          "scope": 23,
+          "src": "48:17:3",
+          "stateVariable": true,
+          "storageLocation": "default",
+          "typeDescriptions":
+          {
+            "typeIdentifier": "t_uint256",
+            "typeString": "uint256"
+          },
+          "typeName":
           {
             "id": 8,
-            "nodeType": "ParameterList",
+            "name": "uint",
-            "parameters": [],
+            "nodeType": "ElementaryTypeName",
-            "src": "51:2:3"
+            "src": "48:4:3",
+            "typeDescriptions":
+            {
+              "typeIdentifier": "t_uint256",
+              "typeString": "uint256"
+            }
           },
-          "src": "42:12:3"
+          "visibility": "public"
         },
         {
-          "body":
+          "anonymous": false,
-          {
-            "id": 13,
-            "nodeType": "Block",
-            "src": "99:6:3",
-            "statements":
-            [
-              {
-                "id": 12,
-                "nodeType": "PlaceholderStatement",
-                "src": "101:1:3"
-              }
-            ]
-          },
           "documentation":
           {
             "id": 10,
             "nodeType": "StructuredDocumentation",
-            "src": "57:26:3",
+            "src": "69:26:3",
-            "text": "Some comment on mod."
+            "text": "Some comment on Evt."
           },
-          "id": 14,
+          "id": 12,
-          "name": "mod",
+          "name": "Evt",
-          "nodeType": "ModifierDefinition",
+          "nodeType": "EventDefinition",
           "parameters":
           {
             "id": 11,
             "nodeType": "ParameterList",
             "parameters": [],
-            "src": "96:2:3"
+            "src": "105:2:3"
           },
-          "src": "84:21:3",
+          "src": "96:12:3"
+        },
+        {
+          "body":
+          {
+            "id": 16,
+            "nodeType": "Block",
+            "src": "153:6:3",
+            "statements":
+            [
+              {
+                "id": 15,
+                "nodeType": "PlaceholderStatement",
+                "src": "155:1:3"
+              }
+            ]
+          },
+          "documentation":
+          {
+            "id": 13,
+            "nodeType": "StructuredDocumentation",
+            "src": "111:26:3",
+            "text": "Some comment on mod."
+          },
+          "id": 17,
+          "name": "mod",
+          "nodeType": "ModifierDefinition",
+          "parameters":
+          {
+            "id": 14,
+            "nodeType": "ParameterList",
+            "parameters": [],
+            "src": "150:2:3"
+          },
+          "src": "138:21:3",
           "virtual": false,
           "visibility": "internal"
         },
         {
           "body":
           {
-            "id": 18,
+            "id": 21,
             "nodeType": "Block",
-            "src": "155:2:3",
+            "src": "209:2:3",
             "statements": []
           },
           "documentation":
           {
-            "id": 15,
+            "id": 18,
             "nodeType": "StructuredDocumentation",
-            "src": "108:25:3",
+            "src": "162:25:3",
             "text": "Some comment on fn."
           },
           "functionSelector": "a4a2c40b",
-          "id": 19,
+          "id": 22,
           "implemented": true,
           "kind": "function",
           "modifiers": [],
@@ -188,29 +225,29 @@
           "nodeType": "FunctionDefinition",
           "parameters":
           {
-            "id": 16,
+            "id": 19,
             "nodeType": "ParameterList",
             "parameters": [],
-            "src": "145:2:3"
+            "src": "199:2:3"
           },
           "returnParameters":
           {
-            "id": 17,
+            "id": 20,
             "nodeType": "ParameterList",
             "parameters": [],
-            "src": "155:0:3"
+            "src": "209:0:3"
           },
-          "scope": 20,
+          "scope": 23,
-          "src": "134:23:3",
+          "src": "188:23:3",
           "stateMutability": "nonpayable",
           "virtual": false,
           "visibility": "public"
         }
       ],
-      "scope": 21,
+      "scope": 24,
-      "src": "0:159:3"
+      "src": "0:213:3"
     }
   ],
-  "src": "0:160:3"
+  "src": "0:214:3"
 }
 ]

test/libsolidity/ASTJSON/documentation.sol

@@ -11,6 +11,7 @@ contract C {}
 // ---- SOURCE: c
 
 contract C {
+  /** Some comment on state var.*/ uint public state;
   /** Some comment on Evt.*/ event Evt();
   /** Some comment on mod.*/ modifier mod() { _; }
   /** Some comment on fn.*/ function fn() public {}

test/libsolidity/ASTJSON/documentation_legacy.json

@@ -6,7 +6,7 @@
     {
       "C":
       [
-        20
+        23
       ]
     }
   },
@@ -28,13 +28,52 @@
         "fullyImplemented": true,
         "linearizedBaseContracts":
         [
-          20
+          23
         ],
         "name": "C",
-        "scope": 21
+        "scope": 24
       },
       "children":
       [
+        {
+          "attributes":
+          {
+            "constant": false,
+            "functionSelector": "c19d93fb",
+            "mutability": "mutable",
+            "name": "state",
+            "scope": 23,
+            "stateVariable": true,
+            "storageLocation": "default",
+            "type": "uint256",
+            "visibility": "public"
+          },
+          "children":
+          [
+            {
+              "attributes":
+              {
+                "name": "uint",
+                "type": "uint256"
+              },
+              "id": 8,
+              "name": "ElementaryTypeName",
+              "src": "48:4:3"
+            },
+            {
+              "attributes":
+              {
+                "text": "Some comment on state var."
+              },
+              "id": 7,
+              "name": "StructuredDocumentation",
+              "src": "15:32:3"
+            }
+          ],
+          "id": 9,
+          "name": "VariableDeclaration",
+          "src": "48:17:3"
+        },
         {
           "attributes":
           {
@@ -48,9 +87,9 @@
               {
                 "text": "Some comment on Evt."
               },
-              "id": 7,
+              "id": 10,
               "name": "StructuredDocumentation",
-              "src": "15:26:3"
+              "src": "69:26:3"
             },
             {
               "attributes":
@@ -61,14 +100,14 @@
                 ]
               },
               "children": [],
-              "id": 8,
+              "id": 11,
               "name": "ParameterList",
-              "src": "51:2:3"
+              "src": "105:2:3"
             }
           ],
-          "id": 9,
+          "id": 12,
           "name": "EventDefinition",
-          "src": "42:12:3"
+          "src": "96:12:3"
         },
         {
           "attributes":
@@ -84,9 +123,9 @@
               {
                 "text": "Some comment on mod."
               },
-              "id": 10,
+              "id": 13,
               "name": "StructuredDocumentation",
-              "src": "57:26:3"
+              "src": "111:26:3"
             },
             {
               "attributes":
@@ -97,27 +136,27 @@
                 ]
               },
               "children": [],
-              "id": 11,
+              "id": 14,
               "name": "ParameterList",
-              "src": "96:2:3"
+              "src": "150:2:3"
             },
             {
               "children":
               [
                 {
-                  "id": 12,
+                  "id": 15,
                   "name": "PlaceholderStatement",
-                  "src": "101:1:3"
+                  "src": "155:1:3"
                 }
               ],
-              "id": 13,
+              "id": 16,
               "name": "Block",
-              "src": "99:6:3"
+              "src": "153:6:3"
             }
           ],
-          "id": 14,
+          "id": 17,
           "name": "ModifierDefinition",
-          "src": "84:21:3"
+          "src": "138:21:3"
         },
         {
           "attributes":
@@ -131,7 +170,7 @@
               null
             ],
             "name": "fn",
-            "scope": 20,
+            "scope": 23,
             "stateMutability": "nonpayable",
             "virtual": false,
             "visibility": "public"
@@ -143,9 +182,9 @@
               {
                 "text": "Some comment on fn."
               },
-              "id": 15,
+              "id": 18,
               "name": "StructuredDocumentation",
-              "src": "108:25:3"
+              "src": "162:25:3"
             },
             {
               "attributes":
@@ -156,9 +195,9 @@
                 ]
               },
               "children": [],
-              "id": 16,
+              "id": 19,
               "name": "ParameterList",
-              "src": "145:2:3"
+              "src": "199:2:3"
             },
             {
               "attributes":
@@ -169,9 +208,9 @@
                 ]
               },
               "children": [],
-              "id": 17,
+              "id": 20,
               "name": "ParameterList",
-              "src": "155:0:3"
+              "src": "209:0:3"
             },
             {
               "attributes":
@@ -182,22 +221,22 @@
                 ]
               },
               "children": [],
-              "id": 18,
+              "id": 21,
               "name": "Block",
-              "src": "155:2:3"
+              "src": "209:2:3"
             }
           ],
-          "id": 19,
+          "id": 22,
           "name": "FunctionDefinition",
-          "src": "134:23:3"
+          "src": "188:23:3"
         }
       ],
-      "id": 20,
+      "id": 23,
       "name": "ContractDefinition",
-      "src": "0:159:3"
+      "src": "0:213:3"
     }
   ],
-  "id": 21,
+  "id": 24,
   "name": "SourceUnit",
-  "src": "0:160:3"
+  "src": "0:214:3"
 }

test/libsolidity/SMTCheckerTest.cpp

@@ -30,13 +30,13 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _ev
 {
 	auto const& choice = m_reader.stringSetting("SMTSolvers", "any");
 	if (choice == "any")
-		m_enabledSolvers = smt::SMTSolverChoice::All();
+		m_enabledSolvers = smtutil::SMTSolverChoice::All();
 	else if (choice == "z3")
-		m_enabledSolvers = smt::SMTSolverChoice::Z3();
+		m_enabledSolvers = smtutil::SMTSolverChoice::Z3();
 	else if (choice == "cvc4")
-		m_enabledSolvers = smt::SMTSolverChoice::CVC4();
+		m_enabledSolvers = smtutil::SMTSolverChoice::CVC4();
 	else if (choice == "none")
-		m_enabledSolvers = smt::SMTSolverChoice::None();
+		m_enabledSolvers = smtutil::SMTSolverChoice::None();
 	else
 		BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT solver choice."));
 

test/libsolidity/SMTCheckerTest.h

@@ -19,7 +19,7 @@
 
 #include <test/libsolidity/SyntaxTest.h>
 
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsmtutil/SolverInterface.h>
 
 #include <string>
 
@@ -41,7 +41,7 @@ protected:
 	/// This is set via option SMTSolvers in the test.
 	/// The possible options are `all`, `z3`, `cvc4`, `none`,
 	/// where if none is given the default used option is `all`.
-	smt::SMTSolverChoice m_enabledSolvers;
+	smtutil::SMTSolverChoice m_enabledSolvers;
 };
 
 }

test/libsolidity/SolidityNatspecJSON.cpp

@@ -204,6 +204,77 @@ BOOST_AUTO_TEST_CASE(dev_and_user_no_doc)
 	checkNatspec(sourceCode, "test", userNatspec, true);
 }
 
+BOOST_AUTO_TEST_CASE(public_state_variable)
+{
+	char const* sourceCode = R"(
+		contract test {
+			/// @notice example of notice
+			/// @dev example of dev
+			/// @return returns state
+			uint public state;
+		}
+	)";
+
+	char const* devDoc = R"R(
+	{
+		"methods" : {},
+		"stateVariables" :
+		{
+			"state" :
+			{
+				"details" : "example of dev",
+				"return" : "returns state"
+			}
+		}
+	}
+	)R";
+	checkNatspec(sourceCode, "test", devDoc, false);
+
+	char const* userDoc = R"R(
+	{
+		"methods" :
+		{
+			"state()" :
+			{
+				"notice": "example of notice"
+			}
+		}
+	}
+	)R";
+	checkNatspec(sourceCode, "test", userDoc, true);
+}
+
+BOOST_AUTO_TEST_CASE(private_state_variable)
+{
+	char const* sourceCode = R"(
+		contract test {
+			/// @dev example of dev
+			uint private state;
+		}
+	)";
+
+	char const* devDoc = R"(
+	{
+		"methods" : {},
+		"stateVariables" :
+		{
+			"state" :
+			{
+				"details" : "example of dev"
+			}
+		}
+	}
+	)";
+	checkNatspec(sourceCode, "test", devDoc, false);
+
+	char const* userDoc = R"(
+	{
+		"methods":{}
+	}
+	)";
+	checkNatspec(sourceCode, "test", userDoc, true);
+}
+
 BOOST_AUTO_TEST_CASE(dev_desc_after_nl)
 {
 	char const* sourceCode = R"(

test/libsolidity/semanticTests/functionCall/call_internal_function_with_multislot_arguments_via_pointer.sol

@@ -0,0 +1,31 @@
+contract C {
+    function m(
+        function() external returns (uint) a,
+        function() external returns (uint) b
+    ) internal returns (function() external returns (uint)) {
+        return a;
+    }
+
+    function s(uint a, uint b) internal returns (uint) {
+        return a + b;
+    }
+
+    function foo() external returns (uint) {
+        return 6;
+    }
+
+    function test() public returns (uint) {
+        function(uint, uint) internal returns (uint) single_slot_function = s;
+
+        function(
+            function() external returns (uint),
+            function() external returns (uint)
+        ) internal returns (function() external returns (uint)) multi_slot_function = m;
+
+        return multi_slot_function(this.foo, this.foo)() + single_slot_function(5, 1);
+    }
+}
+// ====
+// compileViaYul: also
+// ----
+// test() -> 12

test/libsolidity/semanticTests/isoltestFormatting.sol

@@ -0,0 +1,13 @@
+contract C {
+    function f() public returns (uint[5] memory) {
+        uint[5] memory a = [4, 11, 0x111, uint(3355443), 2222222222222222222];
+        return a;
+    }
+    function g() public returns (uint[5] memory) {
+        uint[5] memory a = [16, 256, 257, uint(0x333333), 0x1ed6eb565788e38e];
+        return a;
+    }
+}
+// ----
+// f() -> 4, 11, 0x0111, 0x333333, 2222222222222222222
+// g() -> 0x10, 0x0100, 0x0101, 0x333333, 2222222222222222222

test/libsolidity/syntaxTests/natspec/docstring_author_title_state_variable.sol

@@ -0,0 +1,7 @@
+contract C {
+    /// @title title
+    /// @author author
+    uint private state;
+}
+// ----
+// Warning: (17-56): Documentation tag @title and @author is only allowed on contract definitions. It will be disallowed in 0.7.0.

test/libsolidity/syntaxTests/natspec/docstring_non_public_state_variable_with_return.sol

@@ -0,0 +1,6 @@
+contract test {
+  /// @return returns something
+  uint private state;
+}
+// ----
+// DocstringParsingError: (18-47): Documentation tag "@return" is only allowed on public state-variables.

test/libsolidity/syntaxTests/natspec/docstring_private_state_variable.sol

@@ -0,0 +1,7 @@
+contract C {
+    /// @notice example of notice
+    /// @dev example of dev
+    uint private state;
+}
+// ----
+// Warning: (17-74): Documentation tag on non-public state variables will be disallowed in 0.7.0. You will need to use the @dev tag explicitly.

test/libsolidity/syntaxTests/natspec/docstring_state_variable.sol

@@ -0,0 +1,5 @@
+contract C {
+    /// @notice example of notice
+    /// @dev example of dev
+    uint public state;
+}

test/libsolidity/syntaxTests/natspec/docstring_state_variable_too_many_return_tags.sol

@@ -0,0 +1,9 @@
+contract test {
+  /// @notice example of notice
+  /// @dev example of dev
+  /// @return returns something
+  /// @return returns something
+  uint public state;
+}
+// ----
+// DocstringParsingError: (18-137): Documentation tag "@return" is only allowed once on state-variables.

test/libsolidity/syntaxTests/natspec/docstring_variable.sol

@@ -0,0 +1,14 @@
+contract C {
+    function f() public pure returns (uint) {
+        /// @title example of title
+        /// @author example of author
+        /// @notice example of notice
+        /// @dev example of dev
+        /// @param example of param
+        /// @return example of return
+        uint state = 42;
+        return state;
+    }
+}
+// ----
+// Warning: (290-295): Only state variables can have a docstring. This will be disallowed in 0.7.0.

test/libsolidity/util/BytesUtils.cpp

@@ -252,7 +252,35 @@ string BytesUtils::formatBytes(
 		if (*_bytes.begin() & 0x80)
 			os << formatSigned(_bytes);
 		else
-			os << formatUnsigned(_bytes);
+		{
+			std::string decimal(formatUnsigned(_bytes));
+			std::string hexadecimal(formatHex(_bytes));
+			unsigned int value = u256(_bytes).convert_to<unsigned int>();
+			if (value < 0x10)
+				os << decimal;
+			else if (value >= 0x10 && value <= 0xff) {
+				os << hexadecimal;
+			}
+			else
+			{
+				auto entropy = [](std::string const& str) -> double {
+					double result = 0;
+					map<char, int> frequencies;
+					for (char c: str)
+						frequencies[c]++;
+					for (auto p: frequencies)
+					{
+						double freq = static_cast<double>(p.second) / str.length();
+						result -= freq * (log(freq) / log(2));
+					}
+					return result;
+				};
+				if (entropy(decimal) < entropy(hexadecimal.substr(2, hexadecimal.length())))
+					os << decimal;
+				else
+					os << hexadecimal;
+			}
+		}
 		break;
 	case ABIType::SignedDec:
 		os << formatSigned(_bytes);

test/libyul/Metrics.cpp

@@ -36,15 +36,38 @@ namespace solidity::yul::test
 namespace
 {
 
-size_t codeSize(string const& _source)
+size_t codeSize(string const& _source, CodeWeights const _weights = {})
 {
 	shared_ptr<Block> ast = parse(_source, false).first;
 	BOOST_REQUIRE(ast);
-	return CodeSize::codeSize(*ast);
+	return CodeSize::codeSize(*ast, _weights);
 }
 
 }
 
+class CustomWeightFixture
+{
+protected:
+	CodeWeights m_weights{
+		/* expressionStatementCost = */ 1,
+		/* assignmentCost = */ 2,
+		/* variableDeclarationCost = */ 3,
+		/* functionDefinitionCost = */ 4,
+		/* ifCost = */ 5,
+		/* switchCost = */ 6,
+		/* caseCost = */ 7,
+		/* forLoopCost = */ 8,
+		/* breakCost = */ 9,
+		/* continueCost = */ 10,
+		/* leaveCost = */ 11,
+		/* blockCost = */ 12,
+
+		/* functionCallCost = */ 13,
+		/* identifierCost = */ 14,
+		/* literalCost = */ 15,
+	};
+};
+
 BOOST_AUTO_TEST_SUITE(YulCodeSize)
 
 BOOST_AUTO_TEST_CASE(empty_code)
@@ -52,41 +75,103 @@ BOOST_AUTO_TEST_CASE(empty_code)
 	BOOST_CHECK_EQUAL(codeSize("{}"), 0);
 }
 
+BOOST_FIXTURE_TEST_CASE(empty_code_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(codeSize("{}", m_weights), 0);
+}
+
 BOOST_AUTO_TEST_CASE(nested_blocks)
 {
 	BOOST_CHECK_EQUAL(codeSize("{ {} {} {{ }} }"), 0);
 }
 
+BOOST_FIXTURE_TEST_CASE(nested_blocks_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(codeSize("{ {} {} {{ }} }", m_weights), 4 * m_weights.blockCost);
+}
+
 BOOST_AUTO_TEST_CASE(instruction)
 {
 	BOOST_CHECK_EQUAL(codeSize("{ pop(calldatasize()) }"), 2);
 }
 
+BOOST_FIXTURE_TEST_CASE(instruction_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ pop(calldatasize()) }", m_weights),
+		2 * m_weights.functionCallCost +
+		1 * m_weights.expressionStatementCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(variables_are_free)
 {
 	BOOST_CHECK_EQUAL(codeSize("{ let x let y let a, b, c }"), 0);
 }
 
+BOOST_FIXTURE_TEST_CASE(variables_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ let x let y let a, b, c }", m_weights),
+		3 * m_weights.variableDeclarationCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(constants_cost_one)
 {
 	BOOST_CHECK_EQUAL(codeSize("{ let x := 3 }"), 1);
 }
 
+BOOST_FIXTURE_TEST_CASE(constants_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ let x := 3 }", m_weights),
+		1 * m_weights.variableDeclarationCost +
+		1 * m_weights.literalCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(functions_are_skipped)
 {
 	BOOST_CHECK_EQUAL(codeSize("{ function f(x) -> r { r := mload(x) } }"), 0);
 }
 
+BOOST_FIXTURE_TEST_CASE(functions_are_skipped_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(codeSize("{ function f(x) -> r { r := mload(x) } }", m_weights), 0);
+}
+
 BOOST_AUTO_TEST_CASE(function_with_arguments)
 {
 	BOOST_CHECK_EQUAL(codeSize("{ function f(x) { sstore(x, 2) } f(2) }"), 2);
 }
 
+BOOST_FIXTURE_TEST_CASE(function_with_arguments_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ function f(x) { sstore(x, 2) } f(2) }", m_weights),
+		1 * m_weights.expressionStatementCost +
+		1 * m_weights.functionCallCost +
+		1 * m_weights.literalCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(function_with_variables_as_arguments)
 {
 	BOOST_CHECK_EQUAL(codeSize("{ function f(x) { sstore(x, 2) } let y f(y) }"), 1);
 }
 
+BOOST_FIXTURE_TEST_CASE(function_with_variables_as_arguments_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ function f(x) { sstore(x, 2) } let y f(y) }", m_weights),
+		1 * m_weights.variableDeclarationCost +
+		1 * m_weights.expressionStatementCost +
+		1 * m_weights.functionCallCost +
+		1 * m_weights.identifierCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(function_with_variables_and_constants_as_arguments)
 {
 	BOOST_CHECK_EQUAL(codeSize(
@@ -94,21 +179,69 @@ BOOST_AUTO_TEST_CASE(function_with_variables_and_constants_as_arguments)
 	), 2);
 }
 
+BOOST_FIXTURE_TEST_CASE(
+	function_with_variables_and_constants_as_arguments_custom_weights,
+	CustomWeightFixture
+)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize(
+			"{ function f(x, r) -> z { sstore(x, r) z := r } let y let t := f(y, 2) }",
+			m_weights
+		),
+		2 * m_weights.variableDeclarationCost +
+		1 * m_weights.functionCallCost +
+		1 * m_weights.identifierCost +
+		1 * m_weights.literalCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(assignment)
 {
 	BOOST_CHECK_EQUAL(codeSize("{ let a a := 3 }"), 1);
 }
 
+BOOST_FIXTURE_TEST_CASE(assignment_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ let a a := 3 }", m_weights),
+		1 * m_weights.variableDeclarationCost +
+		1 * m_weights.assignmentCost +
+		1 * m_weights.literalCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(assignments_between_vars_are_free)
 {
 	BOOST_CHECK_EQUAL(codeSize("{ let a let b := a a := b }"), 0);
 }
 
+BOOST_FIXTURE_TEST_CASE(assignments_between_vars_are_free_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ let a let b := a a := b }", m_weights),
+		2 * m_weights.variableDeclarationCost +
+		1 * m_weights.assignmentCost +
+		2 * m_weights.identifierCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(assignment_complex)
 {
 	BOOST_CHECK_EQUAL(codeSize("{ let a let x := mload(a) a := sload(x) }"), 2);
 }
 
+BOOST_FIXTURE_TEST_CASE(assignment_complex_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ let a let x := mload(a) a := sload(x) }", m_weights),
+		2 * m_weights.variableDeclarationCost +
+		1 * m_weights.assignmentCost +
+		2 * m_weights.identifierCost +
+		2 * m_weights.functionCallCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(empty_for_loop)
 {
 	BOOST_CHECK_EQUAL(codeSize(
@@ -116,6 +249,15 @@ BOOST_AUTO_TEST_CASE(empty_for_loop)
 	), 4);
 }
 
+BOOST_FIXTURE_TEST_CASE(empty_for_loop_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ for {} 1 {} {} }", m_weights),
+		1 * m_weights.forLoopCost +
+		1 * m_weights.literalCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(break_statement)
 {
 	BOOST_CHECK_EQUAL(codeSize(
@@ -123,6 +265,16 @@ BOOST_AUTO_TEST_CASE(break_statement)
 	), 6);
 }
 
+BOOST_FIXTURE_TEST_CASE(break_statement_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ for {} 1 {} { break } }", m_weights),
+		1 * m_weights.forLoopCost +
+		1 * m_weights.literalCost +
+		1 * m_weights.breakCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(continue_statement)
 {
 	BOOST_CHECK_EQUAL(codeSize(
@@ -130,6 +282,16 @@ BOOST_AUTO_TEST_CASE(continue_statement)
 	), 6);
 }
 
+BOOST_FIXTURE_TEST_CASE(continue_statement_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ for {} 1 {} { continue } }", m_weights),
+		1 * m_weights.forLoopCost +
+		1 * m_weights.literalCost +
+		1 * m_weights.continueCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(regular_for_loop)
 {
 	BOOST_CHECK_EQUAL(codeSize(
@@ -137,6 +299,20 @@ BOOST_AUTO_TEST_CASE(regular_for_loop)
 	), 10);
 }
 
+BOOST_FIXTURE_TEST_CASE(regular_for_loop_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ for { let x := 0 } lt(x, 10) { x := add(x, 1) } { mstore(x, 1) } }", m_weights),
+		1 * m_weights.forLoopCost +
+		1 * m_weights.variableDeclarationCost +
+		1 * m_weights.assignmentCost +
+		3 * m_weights.functionCallCost +
+		4 * m_weights.literalCost +
+		3 * m_weights.identifierCost +
+		1 * m_weights.expressionStatementCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(if_statement)
 {
 	BOOST_CHECK_EQUAL(codeSize(
@@ -144,6 +320,15 @@ BOOST_AUTO_TEST_CASE(if_statement)
 	), 3);
 }
 
+BOOST_FIXTURE_TEST_CASE(if_statement_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ if 1 {} }", m_weights),
+		1 * m_weights.ifCost +
+		1 * m_weights.literalCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(switch_statement_tiny)
 {
 	BOOST_CHECK_EQUAL(codeSize(
@@ -158,6 +343,16 @@ BOOST_AUTO_TEST_CASE(switch_statement_small)
 	), 6);
 }
 
+BOOST_FIXTURE_TEST_CASE(switch_statement_small_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ switch calldatasize() case 0 {} default {} }", m_weights),
+		1 * m_weights.functionCallCost +
+		1 * m_weights.switchCost +
+		2 * m_weights.caseCost
+	);
+}
+
 BOOST_AUTO_TEST_CASE(switch_statement_medium)
 {
 	BOOST_CHECK_EQUAL(codeSize(
@@ -172,6 +367,16 @@ BOOST_AUTO_TEST_CASE(switch_statement_large)
 	), 10);
 }
 
+BOOST_FIXTURE_TEST_CASE(switch_statement_large_custom_weights, CustomWeightFixture)
+{
+	BOOST_CHECK_EQUAL(
+		codeSize("{ switch calldatasize() case 0 {} case 1 {} case 2 {} default {} }", m_weights),
+		1 * m_weights.functionCallCost +
+		1 * m_weights.switchCost +
+		4 * m_weights.caseCost
+	);
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }

test/yulPhaser/AlgorithmRunner.cpp

@@ -37,6 +37,7 @@ using namespace boost::unit_test::framework;
 using namespace boost::test_tools;
 using namespace solidity::langutil;
 using namespace solidity::util;
+using namespace solidity::yul;
 
 namespace fs = boost::filesystem;
 
@@ -299,8 +300,8 @@ BOOST_FIXTURE_TEST_CASE(run_should_print_cache_stats_if_requested, AlgorithmRunn
 		make_shared<ProgramCache>(programs[1]),
 	};
 	shared_ptr<FitnessMetric> fitnessMetric = make_shared<FitnessMetricAverage>(vector<shared_ptr<FitnessMetric>>{
-		make_shared<ProgramSize>(nullopt, caches[0]),
+		make_shared<ProgramSize>(nullopt, caches[0], CodeWeights{}),
-		make_shared<ProgramSize>(nullopt, caches[1]),
+		make_shared<ProgramSize>(nullopt, caches[1], CodeWeights{}),
 	});
 	Population population = Population::makeRandom(fitnessMetric, 2, 0, 5);
 

test/yulPhaser/FitnessMetrics.cpp

@@ -62,12 +62,12 @@ protected:
 
 	Program optimisedProgram(Program _program) const
 	{
-		[[maybe_unused]] size_t originalSize = _program.codeSize();
+		[[maybe_unused]] size_t originalSize = _program.codeSize(m_weights);
 		Program result = move(_program);
 		result.optimise(m_chromosome.optimisationSteps());
 
 		// Make sure that the program and the chromosome we have chosen are suitable for the test
-		assert(result.codeSize() != originalSize);
+		assert(result.codeSize(m_weights) != originalSize);
 
 		return result;
 	}
@@ -77,15 +77,16 @@ protected:
 	Program m_program = get<Program>(Program::load(m_sourceStream));
 	Program m_optimisedProgram = optimisedProgram(m_program);
 	shared_ptr<ProgramCache> m_programCache = make_shared<ProgramCache>(m_program);
+	static constexpr CodeWeights m_weights{};
 };
 
 class FitnessMetricCombinationFixture: public ProgramBasedMetricFixture
 {
 protected:
 	vector<shared_ptr<FitnessMetric>> m_simpleMetrics = {
-		make_shared<ProgramSize>(m_program, nullptr, 1),
+		make_shared<ProgramSize>(m_program, nullptr, m_weights, 1),
-		make_shared<ProgramSize>(m_program, nullptr, 2),
+		make_shared<ProgramSize>(m_program, nullptr, m_weights, 2),
-		make_shared<ProgramSize>(m_program, nullptr, 3),
+		make_shared<ProgramSize>(m_program, nullptr, m_weights, 3),
 	};
 	vector<size_t> m_fitness = {
 		m_simpleMetrics[0]->evaluate(m_chromosome),
@@ -100,7 +101,7 @@ BOOST_AUTO_TEST_SUITE(ProgramBasedMetricTest)
 
 BOOST_FIXTURE_TEST_CASE(optimisedProgram_should_return_optimised_program_even_if_cache_not_available, ProgramBasedMetricFixture)
 {
-	string code = toString(DummyProgramBasedMetric(m_program, nullptr).optimisedProgram(m_chromosome));
+	string code = toString(DummyProgramBasedMetric(m_program, nullptr, m_weights).optimisedProgram(m_chromosome));
 
 	BOOST_TEST(code != toString(m_program));
 	BOOST_TEST(code == toString(m_optimisedProgram));
@@ -108,7 +109,7 @@ BOOST_FIXTURE_TEST_CASE(optimisedProgram_should_return_optimised_program_even_if
 
 BOOST_FIXTURE_TEST_CASE(optimisedProgram_should_use_cache_if_available, ProgramBasedMetricFixture)
 {
-	string code = toString(DummyProgramBasedMetric(nullopt, m_programCache).optimisedProgram(m_chromosome));
+	string code = toString(DummyProgramBasedMetric(nullopt, m_programCache, m_weights).optimisedProgram(m_chromosome));
 
 	BOOST_TEST(code != toString(m_program));
 	BOOST_TEST(code == toString(m_optimisedProgram));
@@ -117,7 +118,7 @@ BOOST_FIXTURE_TEST_CASE(optimisedProgram_should_use_cache_if_available, ProgramB
 
 BOOST_FIXTURE_TEST_CASE(optimisedProgramNoCache_should_return_optimised_program_even_if_cache_not_available, ProgramBasedMetricFixture)
 {
-	string code = toString(DummyProgramBasedMetric(m_program, nullptr).optimisedProgramNoCache(m_chromosome));
+	string code = toString(DummyProgramBasedMetric(m_program, nullptr, m_weights).optimisedProgramNoCache(m_chromosome));
 
 	BOOST_TEST(code != toString(m_program));
 	BOOST_TEST(code == toString(m_optimisedProgram));
@@ -125,7 +126,7 @@ BOOST_FIXTURE_TEST_CASE(optimisedProgramNoCache_should_return_optimised_program_
 
 BOOST_FIXTURE_TEST_CASE(optimisedProgramNoCache_should_not_use_cache_even_if_available, ProgramBasedMetricFixture)
 {
-	string code = toString(DummyProgramBasedMetric(nullopt, m_programCache).optimisedProgramNoCache(m_chromosome));
+	string code = toString(DummyProgramBasedMetric(nullopt, m_programCache, m_weights).optimisedProgramNoCache(m_chromosome));
 
 	BOOST_TEST(code != toString(m_program));
 	BOOST_TEST(code == toString(m_optimisedProgram));
@@ -137,18 +138,18 @@ BOOST_AUTO_TEST_SUITE(ProgramSizeTest)
 
 BOOST_FIXTURE_TEST_CASE(evaluate_should_compute_size_of_the_optimised_program, ProgramBasedMetricFixture)
 {
-	size_t fitness = ProgramSize(m_program, nullptr).evaluate(m_chromosome);
+	size_t fitness = ProgramSize(m_program, nullptr, m_weights).evaluate(m_chromosome);
 
-	BOOST_TEST(fitness != m_program.codeSize());
+	BOOST_TEST(fitness != m_program.codeSize(m_weights));
-	BOOST_TEST(fitness == m_optimisedProgram.codeSize());
+	BOOST_TEST(fitness == m_optimisedProgram.codeSize(m_weights));
 }
 
 BOOST_FIXTURE_TEST_CASE(evaluate_should_be_able_to_use_program_cache_if_available, ProgramBasedMetricFixture)
 {
-	size_t fitness = ProgramSize(nullopt, m_programCache).evaluate(m_chromosome);
+	size_t fitness = ProgramSize(nullopt, m_programCache, m_weights).evaluate(m_chromosome);
 
-	BOOST_TEST(fitness != m_program.codeSize());
+	BOOST_TEST(fitness != m_program.codeSize(m_weights));
-	BOOST_TEST(fitness == m_optimisedProgram.codeSize());
+	BOOST_TEST(fitness == m_optimisedProgram.codeSize(m_weights));
 	BOOST_TEST(m_programCache->size() == m_chromosome.length());
 }
 
@@ -157,21 +158,21 @@ BOOST_FIXTURE_TEST_CASE(evaluate_should_repeat_the_optimisation_specified_number
 	Program const& programOptimisedOnce = m_optimisedProgram;
 	Program programOptimisedTwice = optimisedProgram(programOptimisedOnce);
 
-	ProgramSize metric(m_program, nullptr, 2);
+	ProgramSize metric(m_program, nullptr, m_weights, 2);
 	size_t fitness = metric.evaluate(m_chromosome);
 
-	BOOST_TEST(fitness != m_program.codeSize());
+	BOOST_TEST(fitness != m_program.codeSize(m_weights));
-	BOOST_TEST(fitness != programOptimisedOnce.codeSize());
+	BOOST_TEST(fitness != programOptimisedOnce.codeSize(m_weights));
-	BOOST_TEST(fitness == programOptimisedTwice.codeSize());
+	BOOST_TEST(fitness == programOptimisedTwice.codeSize(m_weights));
 }
 
 BOOST_FIXTURE_TEST_CASE(evaluate_should_not_optimise_if_number_of_repetitions_is_zero, ProgramBasedMetricFixture)
 {
-	ProgramSize metric(m_program, nullptr, 0);
+	ProgramSize metric(m_program, nullptr, m_weights, 0);
 	size_t fitness = metric.evaluate(m_chromosome);
 
-	BOOST_TEST(fitness == m_program.codeSize());
+	BOOST_TEST(fitness == m_program.codeSize(m_weights));
-	BOOST_TEST(fitness != m_optimisedProgram.codeSize());
+	BOOST_TEST(fitness != m_optimisedProgram.codeSize(m_weights));
 }
 
 BOOST_AUTO_TEST_SUITE_END()
@@ -179,12 +180,18 @@ BOOST_AUTO_TEST_SUITE(RelativeProgramSizeTest)
 
 BOOST_FIXTURE_TEST_CASE(evaluate_should_compute_the_size_ratio_between_optimised_program_and_original_program, ProgramBasedMetricFixture)
 {
-	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 3).evaluate(m_chromosome) == round(1000.0 * m_optimisedProgram.codeSize() / m_program.codeSize()));
+	BOOST_TEST(
+		RelativeProgramSize(m_program, nullptr, 3, m_weights).evaluate(m_chromosome) ==
+		round(1000.0 * m_optimisedProgram.codeSize(m_weights) / m_program.codeSize(m_weights))
+	);
 }
 
 BOOST_FIXTURE_TEST_CASE(evaluate_should_be_able_to_use_program_cache_if_available, ProgramBasedMetricFixture)
 {
-	BOOST_TEST(RelativeProgramSize(nullopt, m_programCache, 3).evaluate(m_chromosome) == round(1000.0 * m_optimisedProgram.codeSize() / m_program.codeSize()));
+	BOOST_TEST(
+		RelativeProgramSize(nullopt, m_programCache, 3, m_weights).evaluate(m_chromosome) ==
+		round(1000.0 * m_optimisedProgram.codeSize(m_weights) / m_program.codeSize(m_weights))
+	);
 	BOOST_TEST(m_programCache->size() == m_chromosome.length());
 }
 
@@ -193,17 +200,17 @@ BOOST_FIXTURE_TEST_CASE(evaluate_should_repeat_the_optimisation_specified_number
 	Program const& programOptimisedOnce = m_optimisedProgram;
 	Program programOptimisedTwice = optimisedProgram(programOptimisedOnce);
 
-	RelativeProgramSize metric(m_program, nullptr, 3, 2);
+	RelativeProgramSize metric(m_program, nullptr, 3, m_weights, 2);
 	size_t fitness = metric.evaluate(m_chromosome);
 
 	BOOST_TEST(fitness != 1000);
-	BOOST_TEST(fitness != RelativeProgramSize(programOptimisedTwice, nullptr, 3, 1).evaluate(m_chromosome));
+	BOOST_TEST(fitness != RelativeProgramSize(programOptimisedTwice, nullptr, 3, m_weights, 1).evaluate(m_chromosome));
-	BOOST_TEST(fitness == round(1000.0 * programOptimisedTwice.codeSize() / m_program.codeSize()));
+	BOOST_TEST(fitness == round(1000.0 * programOptimisedTwice.codeSize(m_weights) / m_program.codeSize(m_weights)));
 }
 
 BOOST_FIXTURE_TEST_CASE(evaluate_should_return_one_if_number_of_repetitions_is_zero, ProgramBasedMetricFixture)
 {
-	RelativeProgramSize metric(m_program, nullptr, 3, 0);
+	RelativeProgramSize metric(m_program, nullptr, 3, m_weights, 0);
 
 	BOOST_TEST(metric.evaluate(m_chromosome) == 1000);
 }
@@ -213,7 +220,7 @@ BOOST_FIXTURE_TEST_CASE(evaluate_should_return_one_if_the_original_program_size_
 	CharStream sourceStream = CharStream("{}", "");
 	Program program = get<Program>(Program::load(sourceStream));
 
-	RelativeProgramSize metric(program, nullptr, 3);
+	RelativeProgramSize metric(program, nullptr, 3, m_weights);
 
 	BOOST_TEST(metric.evaluate(m_chromosome) == 1000);
 	BOOST_TEST(metric.evaluate(Chromosome("")) == 1000);
@@ -222,12 +229,12 @@ BOOST_FIXTURE_TEST_CASE(evaluate_should_return_one_if_the_original_program_size_
 
 BOOST_FIXTURE_TEST_CASE(evaluate_should_multiply_the_result_by_scaling_factor, ProgramBasedMetricFixture)
 {
-	double sizeRatio = static_cast<double>(m_optimisedProgram.codeSize()) / m_program.codeSize();
+	double sizeRatio = static_cast<double>(m_optimisedProgram.codeSize(m_weights)) / m_program.codeSize(m_weights);
-	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 0).evaluate(m_chromosome) == round(1.0 * sizeRatio));
+	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 0, m_weights).evaluate(m_chromosome) == round(1.0 * sizeRatio));
-	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 1).evaluate(m_chromosome) == round(10.0 * sizeRatio));
+	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 1, m_weights).evaluate(m_chromosome) == round(10.0 * sizeRatio));
-	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 2).evaluate(m_chromosome) == round(100.0 * sizeRatio));
+	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 2, m_weights).evaluate(m_chromosome) == round(100.0 * sizeRatio));
-	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 3).evaluate(m_chromosome) == round(1000.0 * sizeRatio));
+	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 3, m_weights).evaluate(m_chromosome) == round(1000.0 * sizeRatio));
-	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 4).evaluate(m_chromosome) == round(10000.0 * sizeRatio));
+	BOOST_TEST(RelativeProgramSize(m_program, nullptr, 4, m_weights).evaluate(m_chromosome) == round(10000.0 * sizeRatio));
 }
 
 BOOST_AUTO_TEST_SUITE_END()

test/yulPhaser/Phaser.cpp

@@ -32,6 +32,7 @@
 using namespace std;
 using namespace solidity::util;
 using namespace solidity::langutil;
+using namespace solidity::yul;
 
 namespace fs = boost::filesystem;
 
@@ -86,6 +87,7 @@ protected:
 		/* relativeMetricScale = */ 5,
 		/* chromosomeRepetitions = */ 1,
 	};
+	CodeWeights const m_weights{};
 };
 
 class PoulationFactoryFixture
@@ -183,7 +185,7 @@ BOOST_FIXTURE_TEST_CASE(build_should_create_metric_of_the_right_type, FitnessMet
 {
 	m_options.metric = MetricChoice::RelativeCodeSize;
 	m_options.metricAggregator = MetricAggregatorChoice::Sum;
-	unique_ptr<FitnessMetric> metric = FitnessMetricFactory::build(m_options, {m_programs[0]}, {nullptr});
+	unique_ptr<FitnessMetric> metric = FitnessMetricFactory::build(m_options, {m_programs[0]}, {nullptr}, m_weights);
 	BOOST_REQUIRE(metric != nullptr);
 
 	auto sumMetric = dynamic_cast<FitnessMetricSum*>(metric.get());
@@ -201,7 +203,7 @@ BOOST_FIXTURE_TEST_CASE(build_should_respect_chromosome_repetitions_option, Fitn
 	m_options.metric = MetricChoice::CodeSize;
 	m_options.metricAggregator = MetricAggregatorChoice::Average;
 	m_options.chromosomeRepetitions = 5;
-	unique_ptr<FitnessMetric> metric = FitnessMetricFactory::build(m_options, {m_programs[0]}, {nullptr});
+	unique_ptr<FitnessMetric> metric = FitnessMetricFactory::build(m_options, {m_programs[0]}, {nullptr}, m_weights);
 	BOOST_REQUIRE(metric != nullptr);
 
 	auto averageMetric = dynamic_cast<FitnessMetricAverage*>(metric.get());
@@ -219,7 +221,7 @@ BOOST_FIXTURE_TEST_CASE(build_should_set_relative_metric_scale, FitnessMetricFac
 	m_options.metric = MetricChoice::RelativeCodeSize;
 	m_options.metricAggregator = MetricAggregatorChoice::Average;
 	m_options.relativeMetricScale = 10;
-	unique_ptr<FitnessMetric> metric = FitnessMetricFactory::build(m_options, {m_programs[0]}, {nullptr});
+	unique_ptr<FitnessMetric> metric = FitnessMetricFactory::build(m_options, {m_programs[0]}, {nullptr}, m_weights);
 	BOOST_REQUIRE(metric != nullptr);
 
 	auto averageMetric = dynamic_cast<FitnessMetricAverage*>(metric.get());
@@ -237,7 +239,8 @@ BOOST_FIXTURE_TEST_CASE(build_should_create_metric_for_each_input_program, Fitne
 	unique_ptr<FitnessMetric> metric = FitnessMetricFactory::build(
 		m_options,
 		m_programs,
-		vector<shared_ptr<ProgramCache>>(m_programs.size(), nullptr)
+		vector<shared_ptr<ProgramCache>>(m_programs.size(), nullptr),
+		m_weights
 	);
 	BOOST_REQUIRE(metric != nullptr);
 
@@ -256,7 +259,7 @@ BOOST_FIXTURE_TEST_CASE(build_should_pass_program_caches_to_metrics, FitnessMetr
 	};
 
 	m_options.metric = MetricChoice::RelativeCodeSize;
-	unique_ptr<FitnessMetric> metric = FitnessMetricFactory::build(m_options, m_programs, caches);
+	unique_ptr<FitnessMetric> metric = FitnessMetricFactory::build(m_options, m_programs, caches, m_weights);
 	BOOST_REQUIRE(metric != nullptr);
 
 	auto combinedMetric = dynamic_cast<FitnessMetricCombination*>(metric.get());

test/yulPhaser/Program.cpp

@@ -398,7 +398,7 @@ BOOST_AUTO_TEST_CASE(codeSize)
 	CharStream sourceStream(sourceCode, current_test_case().p_name);
 	Program program = get<Program>(Program::load(sourceStream));
 
-	BOOST_TEST(program.codeSize() == CodeSize::codeSizeIncludingFunctions(program.ast()));
+	BOOST_TEST(program.codeSize(CodeWeights{}) == CodeSize::codeSizeIncludingFunctions(program.ast()));
 }
 
 BOOST_AUTO_TEST_SUITE_END()

test/yulPhaser/ProgramCache.cpp

@@ -18,6 +18,8 @@
 #include <tools/yulPhaser/ProgramCache.h>
 #include <tools/yulPhaser/Chromosome.h>
 
+#include <libyul/optimiser/Metrics.h>
+
 #include <liblangutil/CharStream.h>
 
 #include <libsolutil/CommonIO.h>
@@ -212,11 +214,11 @@ BOOST_FIXTURE_TEST_CASE(startRound_should_remove_entries_older_than_two_rounds,
 
 BOOST_FIXTURE_TEST_CASE(gatherStats_should_return_cache_statistics, ProgramCacheFixture)
 {
-	size_t sizeI = optimisedProgram(m_program, "I").codeSize();
+	size_t sizeI = optimisedProgram(m_program, "I").codeSize(CacheStats::StorageWeights);
-	size_t sizeIu = optimisedProgram(m_program, "Iu").codeSize();
+	size_t sizeIu = optimisedProgram(m_program, "Iu").codeSize(CacheStats::StorageWeights);
-	size_t sizeIuO = optimisedProgram(m_program, "IuO").codeSize();
+	size_t sizeIuO = optimisedProgram(m_program, "IuO").codeSize(CacheStats::StorageWeights);
-	size_t sizeL = optimisedProgram(m_program, "L").codeSize();
+	size_t sizeL = optimisedProgram(m_program, "L").codeSize(CacheStats::StorageWeights);
-	size_t sizeLT = optimisedProgram(m_program, "LT").codeSize();
+	size_t sizeLT = optimisedProgram(m_program, "LT").codeSize(CacheStats::StorageWeights);
 
 	m_programCache.optimiseProgram("L");
 	m_programCache.optimiseProgram("Iu");

tools/yulPhaser/FitnessMetrics.cpp

@@ -23,6 +23,7 @@
 
 using namespace std;
 using namespace solidity::util;
+using namespace solidity::yul;
 using namespace solidity::phaser;
 
 Program const& ProgramBasedMetric::program() const
@@ -55,18 +56,18 @@ Program ProgramBasedMetric::optimisedProgramNoCache(Chromosome const& _chromosom
 
 size_t ProgramSize::evaluate(Chromosome const& _chromosome)
 {
-	return optimisedProgram(_chromosome).codeSize();
+	return optimisedProgram(_chromosome).codeSize(codeWeights());
 }
 
 size_t RelativeProgramSize::evaluate(Chromosome const& _chromosome)
 {
 	size_t const scalingFactor = pow(10, m_fixedPointPrecision);
 
-	size_t unoptimisedSize = optimisedProgram(Chromosome("")).codeSize();
+	size_t unoptimisedSize = optimisedProgram(Chromosome("")).codeSize(codeWeights());
 	if (unoptimisedSize == 0)
 		return scalingFactor;
 
-	size_t optimisedSize = optimisedProgram(_chromosome).codeSize();
+	size_t optimisedSize = optimisedProgram(_chromosome).codeSize(codeWeights());
 
 	return static_cast<size_t>(round(
 		static_cast<double>(optimisedSize) / unoptimisedSize * scalingFactor

tools/yulPhaser/FitnessMetrics.h

@@ -24,6 +24,8 @@
 #include <tools/yulPhaser/Program.h>
 #include <tools/yulPhaser/ProgramCache.h>
 
+#include <libyul/optimiser/Metrics.h>
+
 #include <cstddef>
 #include <optional>
 
@@ -64,10 +66,12 @@ public:
 	explicit ProgramBasedMetric(
 		std::optional<Program> _program,
 		std::shared_ptr<ProgramCache> _programCache,
+		yul::CodeWeights const& _codeWeights,
 		size_t _repetitionCount = 1
 	):
 		m_program(std::move(_program)),
 		m_programCache(std::move(_programCache)),
+		m_codeWeights(_codeWeights),
 		m_repetitionCount(_repetitionCount)
 	{
 		assert(m_program.has_value() == (m_programCache == nullptr));
@@ -75,6 +79,7 @@ public:
 
 	Program const& program() const;
 	ProgramCache const* programCache() const { return m_programCache.get(); }
+	yul::CodeWeights const& codeWeights() const { return m_codeWeights; }
 	size_t repetitionCount() const { return m_repetitionCount; }
 
 	Program optimisedProgram(Chromosome const& _chromosome);
@@ -83,6 +88,7 @@ public:
 private:
 	std::optional<Program> m_program;
 	std::shared_ptr<ProgramCache> m_programCache;
+	yul::CodeWeights m_codeWeights;
 	size_t m_repetitionCount;
 };
 
@@ -111,9 +117,10 @@ public:
 		std::optional<Program> _program,
 		std::shared_ptr<ProgramCache> _programCache,
 		size_t _fixedPointPrecision,
+		yul::CodeWeights const& _weights,
 		size_t _repetitionCount = 1
 	):
-		ProgramBasedMetric(std::move(_program), std::move(_programCache), _repetitionCount),
+		ProgramBasedMetric(std::move(_program), std::move(_programCache), _weights, _repetitionCount),
 		m_fixedPointPrecision(_fixedPointPrecision) {}
 
 	size_t fixedPointPrecision() const { return m_fixedPointPrecision; }

tools/yulPhaser/Phaser.cpp

@@ -39,6 +39,7 @@ using namespace std;
 using namespace solidity;
 using namespace solidity::langutil;
 using namespace solidity::util;
+using namespace solidity::yul;
 using namespace solidity::phaser;
 
 namespace po = boost::program_options;
@@ -188,6 +189,27 @@ unique_ptr<GeneticAlgorithm> GeneticAlgorithmFactory::build(
 	}
 }
 
+CodeWeights CodeWeightFactory::buildFromCommandLine(po::variables_map const& _arguments)
+{
+	return {
+		_arguments["expression-statement-cost"].as<size_t>(),
+		_arguments["assignment-cost"].as<size_t>(),
+		_arguments["variable-declaration-cost"].as<size_t>(),
+		_arguments["function-definition-cost"].as<size_t>(),
+		_arguments["if-cost"].as<size_t>(),
+		_arguments["switch-cost"].as<size_t>(),
+		_arguments["case-cost"].as<size_t>(),
+		_arguments["for-loop-cost"].as<size_t>(),
+		_arguments["break-cost"].as<size_t>(),
+		_arguments["continue-cost"].as<size_t>(),
+		_arguments["leave-cost"].as<size_t>(),
+		_arguments["block-cost"].as<size_t>(),
+		_arguments["function-call-cost"].as<size_t>(),
+		_arguments["identifier-cost"].as<size_t>(),
+		_arguments["literal-cost"].as<size_t>(),
+	};
+}
+
 FitnessMetricFactory::Options FitnessMetricFactory::Options::fromCommandLine(po::variables_map const& _arguments)
 {
 	return {
@@ -201,7 +223,8 @@ FitnessMetricFactory::Options FitnessMetricFactory::Options::fromCommandLine(po:
 unique_ptr<FitnessMetric> FitnessMetricFactory::build(
 	Options const& _options,
 	vector<Program> _programs,
-	vector<shared_ptr<ProgramCache>> _programCaches
+	vector<shared_ptr<ProgramCache>> _programCaches,
+	CodeWeights const& _weights
 )
 {
 	assert(_programCaches.size() == _programs.size());
@@ -216,6 +239,7 @@ unique_ptr<FitnessMetric> FitnessMetricFactory::build(
 				metrics.push_back(make_unique<ProgramSize>(
 					_programCaches[i] != nullptr ? optional<Program>{} : move(_programs[i]),
 					move(_programCaches[i]),
+					_weights,
 					_options.chromosomeRepetitions
 				));
 
@@ -228,6 +252,7 @@ unique_ptr<FitnessMetric> FitnessMetricFactory::build(
 					_programCaches[i] != nullptr ? optional<Program>{} : move(_programs[i]),
 					move(_programCaches[i]),
 					_options.relativeMetricScale,
+					_weights,
 					_options.chromosomeRepetitions
 				));
 			break;
@@ -653,6 +678,28 @@ Phaser::CommandLineDescription Phaser::buildCommandLineDescription()
 	;
 	keywordDescription.add(metricsDescription);
 
+	po::options_description metricWeightDescription("METRIC WEIGHTS", lineLength, minDescriptionLength);
+	metricWeightDescription.add_options()
+		// TODO: We need to figure out the best set of weights for the phaser.
+		// This one is just a stopgap to make sure no statement or expression has zero cost.
+		("expression-statement-cost", po::value<size_t>()->value_name("<COST>")->default_value(1))
+		("assignment-cost",           po::value<size_t>()->value_name("<COST>")->default_value(1))
+		("variable-declaration-cost", po::value<size_t>()->value_name("<COST>")->default_value(1))
+		("function-definition-cost",  po::value<size_t>()->value_name("<COST>")->default_value(1))
+		("if-cost",                   po::value<size_t>()->value_name("<COST>")->default_value(2))
+		("switch-cost",               po::value<size_t>()->value_name("<COST>")->default_value(1))
+		("case-cost",                 po::value<size_t>()->value_name("<COST>")->default_value(2))
+		("for-loop-cost",             po::value<size_t>()->value_name("<COST>")->default_value(3))
+		("break-cost",                po::value<size_t>()->value_name("<COST>")->default_value(2))
+		("continue-cost",             po::value<size_t>()->value_name("<COST>")->default_value(2))
+		("leave-cost",                po::value<size_t>()->value_name("<COST>")->default_value(2))
+		("block-cost",                po::value<size_t>()->value_name("<COST>")->default_value(1))
+		("function-call-cost",        po::value<size_t>()->value_name("<COST>")->default_value(1))
+		("identifier-cost",           po::value<size_t>()->value_name("<COST>")->default_value(1))
+		("literal-cost",              po::value<size_t>()->value_name("<COST>")->default_value(1))
+	;
+	keywordDescription.add(metricWeightDescription);
+
 	po::options_description cacheDescription("CACHE", lineLength, minDescriptionLength);
 	cacheDescription.add_options()
 		(
@@ -762,8 +809,13 @@ void Phaser::runPhaser(po::variables_map const& _arguments)
 
 	vector<Program> programs = ProgramFactory::build(programOptions);
 	vector<shared_ptr<ProgramCache>> programCaches = ProgramCacheFactory::build(cacheOptions, programs);
-
+	CodeWeights codeWeights = CodeWeightFactory::buildFromCommandLine(_arguments);
-	unique_ptr<FitnessMetric> fitnessMetric = FitnessMetricFactory::build(metricOptions, programs, programCaches);
+	unique_ptr<FitnessMetric> fitnessMetric = FitnessMetricFactory::build(
+		metricOptions,
+		programs,
+		programCaches,
+		codeWeights
+	);
 	Population population = PopulationFactory::build(populationOptions, move(fitnessMetric));
 
 	if (_arguments["mode"].as<PhaserMode>() == PhaserMode::RunAlgorithm)

tools/yulPhaser/Phaser.h

@@ -39,6 +39,13 @@ class CharStream;
 
 }
 
+namespace solidity::yul
+{
+
+struct CodeWeights;
+
+}
+
 namespace solidity::phaser
 {
 
@@ -125,6 +132,17 @@ public:
 	);
 };
 
+/**
+ * Builds and validates instances of @a CodeWeights.
+ */
+class CodeWeightFactory
+{
+public:
+	static yul::CodeWeights buildFromCommandLine(
+		boost::program_options::variables_map const& _arguments
+	);
+};
+
 /**
  * Builds and validates instances of @a FitnessMetric and its derived classes.
  */
@@ -144,7 +162,8 @@ public:
 	static std::unique_ptr<FitnessMetric> build(
 		Options const& _options,
 		std::vector<Program> _programs,
-		std::vector<std::shared_ptr<ProgramCache>> _programCaches
+		std::vector<std::shared_ptr<ProgramCache>> _programCaches,
+		yul::CodeWeights const& _weights
 	);
 };
 

tools/yulPhaser/Program.cpp

@@ -207,7 +207,7 @@ unique_ptr<Block> Program::applyOptimisationSteps(
 	return _ast;
 }
 
-size_t Program::computeCodeSize(Block const& _ast)
+size_t Program::computeCodeSize(Block const& _ast, CodeWeights const& _weights)
 {
-	return CodeSize::codeSizeIncludingFunctions(_ast);
+	return CodeSize::codeSizeIncludingFunctions(_ast, _weights);
 }

tools/yulPhaser/Program.h

@@ -41,6 +41,7 @@ namespace solidity::yul
 
 struct AsmAnalysisInfo;
 struct Dialect;
+struct CodeWeights;
 
 }
 
@@ -78,7 +79,7 @@ public:
 	static std::variant<Program, langutil::ErrorList> load(langutil::CharStream& _sourceCode);
 	void optimise(std::vector<std::string> const& _optimisationSteps);
 
-	size_t codeSize() const { return computeCodeSize(*m_ast); }
+	size_t codeSize(yul::CodeWeights const& _weights) const { return computeCodeSize(*m_ast, _weights); }
 	yul::Block const& ast() const { return *m_ast; }
 
 	friend std::ostream& operator<<(std::ostream& _stream, Program const& _program);
@@ -113,7 +114,7 @@ private:
 		std::unique_ptr<yul::Block> _ast,
 		std::vector<std::string> const& _optimisationSteps
 	);
-	static size_t computeCodeSize(yul::Block const& _ast);
+	static size_t computeCodeSize(yul::Block const& _ast, yul::CodeWeights const& _weights);
 
 	std::unique_ptr<yul::Block> m_ast;
 	yul::Dialect const& m_dialect;

tools/yulPhaser/ProgramCache.cpp

@@ -17,6 +17,8 @@
 
 #include <tools/yulPhaser/ProgramCache.h>
 
+#include <libyul/optimiser/Metrics.h>
+
 #include <libyul/optimiser/Suite.h>
 
 using namespace std;
@@ -133,7 +135,7 @@ size_t ProgramCache::calculateTotalCachedCodeSize() const
 {
 	size_t size = 0;
 	for (auto const& pair: m_entries)
-		size += pair.second.program.codeSize();
+		size += pair.second.program.codeSize(CacheStats::StorageWeights);
 
 	return size;
 }

tools/yulPhaser/ProgramCache.h

@@ -19,6 +19,8 @@
 
 #include <tools/yulPhaser/Program.h>
 
+#include <libyul/optimiser/Metrics.h>
+
 #include <map>
 #include <string>
 
@@ -44,6 +46,29 @@ struct CacheEntry
  */
 struct CacheStats
 {
+	/// Weights used to compute totalCodeSize.
+	/// The goal here is to get a result proportional to the amount of memory taken by the AST.
+	/// Each statement/expression gets 1 just for existing. We add more if it contains any extra
+	/// data that won't be visited separately by ASTWalker.
+	static yul::CodeWeights constexpr StorageWeights = {
+		/* expressionStatementCost = */ 1,
+		/* assignmentCost = */ 1,
+		/* variableDeclarationCost = */ 1,
+		/* functionDefinitionCost = */ 1,
+		/* ifCost = */ 1,
+		/* switchCost = */ 1,
+		/* caseCost = */ 1,
+		/* forLoopCost = */ 1,
+		/* breakCost = */ 1,
+		/* continueCost = */ 1,
+		/* leaveCost = */ 1,
+		/* blockCost = */ 1,
+
+		/* functionCallCost = */ 1,
+		/* identifierCost = */ 1,
+		/* literalCost = */ 1,
+	};
+
 	size_t hits;
 	size_t misses;
 	size_t totalCodeSize;