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

.circleci/config.yml

@@ -1046,7 +1046,7 @@ jobs:
 
   b_bytecode_ems:
     docker:
-      - image: circleci/node:10
+      - image: circleci/node:14
     environment:
       SOLC_EMSCRIPTEN: "On"
     steps:

Changelog.md

@@ -51,6 +51,8 @@ Compiler Features:
 Bugfixes:
  * Code generator: Do not pad empty string literals with a single 32-byte zero field in the ABI coder v1.
  * SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals.
+ * SMTChecker: Fix internal error when trying to generate counterexamples with old z3.
+ * SMTChecker: Fix segmentation fault that could occur on certain SMT-enabled sources when no SMT solver was available.
  * Yul Optimizer: Fix a bug in NameSimplifier where a new name created by NameSimplifier could also be created by NameDispenser.
  * Yul Optimizer: Removed NameSimplifier from optimization steps available to users.
 

docs/ir/ir-breaking-changes.rst

@@ -33,3 +33,39 @@ Consequently, if the padding space within a struct is used to store data (e.g. i
     }
 
 We have the same behavior for implicit delete, for example when array of structs is shortened.
+
+ * The order of contract initialization has changed in case of inheritance.
+
+The order used to be:
+ - All state variables are zero-initialized at the beginning.
+ - Evaluate base constructor arguments from most derived to most base contract.
+ - Initialize all state variables in the whole inheritance hierarchy from most base to most derived.
+ - Run the constructor, if present, for all contracts in the linearized hierarchy from most base to most derived.
+
+New order:
+ - All state variables are zero-initialized at the beginning.
+ - Evaluate base constructor arguments from most derived to most base contract.
+ - For every contract in order from most base to most derived in the linearized hierarchy execute:
+     1. If present at declaration, initial values are assigned to state variables.
+     2. Constructor, if present.
+
+This causes differences in some contracts, for example:
+::
+    // SPDX-License-Identifier: GPL-3.0
+    pragma solidity >0.7.0;
+
+    contract A {
+        uint x;
+        constructor() {
+            x = 42;
+        }
+        function f() public view returns(uint256) {
+            return x;
+        }
+    }
+    contract B is A {
+        uint public y = f();
+    }
+
+Previously, ``y`` would be set to 0. This is due to the fact that we would first initialize state variables: First, ``x`` is set to 0, and when initializing ``y``, ``f()`` would return 0 causing ``y`` to be 0 as well.
+With the new rules, ``y`` will be set to 42. We first initialize ``x`` to 0, then call A's constructor which sets ``x`` to 42. Finally, when initializing ``y``, ``f()`` returns 42 causing ``y`` to be 42.

docs/yul.rst

@@ -896,12 +896,11 @@ the ``dup`` and ``swap`` instructions as well as ``jump`` instructions, labels a
 
 .. note::
   The ``call*`` instructions use the ``out`` and ``outsize`` parameters to define an area in memory where
-  the return data is placed. This area is written to depending on how many bytes the called contract returns.
+  the return or failure data is placed. This area is written to depending on how many bytes the called contract returns.
   If it returns more data, only the first ``outsize`` bytes are written. You can access the rest of the data
   using the ``returndatacopy`` opcode. If it returns less data, then the remaining bytes are not touched at all.
   You need to use the ``returndatasize`` opcode to check which part of this memory area contains the return data.
-  The remaining bytes will retain their values as of before the call. If the call fails (it returns ``0``),
+  The remaining bytes will retain their values as of before the call.
-  nothing is written to that area, but you can still retrieve the failure data using ``returndatacopy``.
 
 
 In some internal dialects, there are additional functions:

libsmtutil/CHCSmtLib2Interface.cpp

@@ -36,7 +36,7 @@ using namespace solidity::frontend;
 using namespace solidity::smtutil;
 
 CHCSmtLib2Interface::CHCSmtLib2Interface(
-	map<h256, string> _queryResponses,
+	map<h256, string> const& _queryResponses,
 	ReadCallback::Callback _smtCallback,
 	optional<unsigned> _queryTimeout
 ):

libsmtutil/CHCSmtLib2Interface.h

@@ -33,7 +33,7 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 {
 public:
 	explicit CHCSmtLib2Interface(
-		std::map<util::h256, std::string> _queryResponses = {},
+		std::map<util::h256, std::string> const& _queryResponses = {},
 		frontend::ReadCallback::Callback _smtCallback = {},
 		std::optional<unsigned> _queryTimeout = {}
 	);

libsmtutil/Z3CHCInterface.cpp

@@ -33,6 +33,13 @@ Z3CHCInterface::Z3CHCInterface(optional<unsigned> _queryTimeout):
 	m_context(m_z3Interface->context()),
 	m_solver(*m_context)
 {
+	Z3_get_version(
+		&get<0>(m_version),
+		&get<1>(m_version),
+		&get<2>(m_version),
+		&get<3>(m_version)
+	);
+
 	// These need to be set globally.
 	z3::set_param("rewriter.pull_cheap_ite", true);
 
@@ -73,7 +80,6 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
 pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
 {
 	CheckResult result;
-	CHCSolverInterface::CexGraph cex;
 	try
 	{
 		z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr);
@@ -82,9 +88,14 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
 		case z3::check_result::sat:
 		{
 			result = CheckResult::SATISFIABLE;
-			auto proof = m_solver.get_answer();
+			// z3 version 4.8.8 modified Spacer to also return
-			auto cex = cexGraph(proof);
+			// proofs containing nonlinear clauses.
-			return {result, cex};
+			if (m_version >= tuple(4, 8, 8, 0))
+			{
+				auto proof = m_solver.get_answer();
+				return {result, cexGraph(proof)};
+			}
+			break;
 		}
 		case z3::check_result::unsat:
 		{
@@ -112,10 +123,9 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
 			result = CheckResult::UNKNOWN;
 		else
 			result = CheckResult::ERROR;
-		cex = {};
 	}
 
-	return {result, cex};
+	return {result, {}};
 }
 
 void Z3CHCInterface::setSpacerOptions(bool _preProcessing)

libsmtutil/Z3CHCInterface.h

@@ -25,6 +25,7 @@
 #include <libsmtutil/CHCSolverInterface.h>
 #include <libsmtutil/Z3Interface.h>
 
+#include <tuple>
 #include <vector>
 
 namespace solidity::smtutil
@@ -64,6 +65,8 @@ private:
 	z3::context* m_context;
 	// Horn solver.
 	z3::fixedpoint m_solver;
+
+	std::tuple<unsigned, unsigned, unsigned, unsigned> m_version = std::tuple(0, 0, 0, 0);
 };
 
 }

libsolidity/formal/BMC.cpp

@@ -149,6 +149,9 @@ bool BMC::visit(FunctionDefinition const& _function)
 		resetStateVariables();
 	}
 
+	if (_function.isConstructor())
+		inlineConstructorHierarchy(dynamic_cast<ContractDefinition const&>(*_function.scope()));
+
 	/// Already visits the children.
 	SMTEncoder::visit(_function);
 

libsolidity/formal/CHC.cpp

@@ -112,20 +112,11 @@ vector<string> CHC::unhandledQueries() const
 bool CHC::visit(ContractDefinition const& _contract)
 {
 	resetContractAnalysis();
-
 	initContract(_contract);
-
-	m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
-
 	clearIndices(&_contract);
 
+	m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
 	solAssert(m_currentContract, "");
-	m_constructorSummaryPredicate = createSymbolicBlock(
-		constructorSort(*m_currentContract, state()),
-		"summary_constructor_" + contractSuffix(_contract),
-		PredicateType::ConstructorSummary,
-		&_contract
-	);
 
 	SMTEncoder::visit(_contract);
 	return false;
@@ -133,27 +124,64 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 void CHC::endVisit(ContractDefinition const& _contract)
 {
-	auto implicitConstructorPredicate = createSymbolicBlock(
-		implicitConstructorSort(state()),
-		"implicit_constructor_" + contractSuffix(_contract),
-		PredicateType::ImplicitConstructor,
-		&_contract
-	);
-	addRule(
-		(*implicitConstructorPredicate)({0, state().thisAddress(), state().crypto(), state().tx(), state().state()}),
-		implicitConstructorPredicate->functor().name
-	);
-	setCurrentBlock(*implicitConstructorPredicate);
-
 	if (auto constructor = _contract.constructor())
 		constructor->accept(*this);
-	else
+
-		inlineConstructorHierarchy(_contract);
+	defineContractInitializer(_contract);
+
+	auto const& entry = *createConstructorBlock(_contract, "implicit_constructor_entry");
+
+	// In case constructors use uninitialized state variables,
+	// they need to be zeroed.
+	// This is not part of `initialConstraints` because it's only true here,
+	// at the beginning of the deployment routine.
+	smtutil::Expression zeroes(true);
+	for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
+		zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type());
+	addRule(smtutil::Expression::implies(initialConstraints(_contract) && zeroes, predicate(entry)), entry.functor().name);
+	setCurrentBlock(entry);
+
+	solAssert(!m_errorDest, "");
+	m_errorDest = m_constructorSummaries.at(&_contract);
+	// We need to evaluate the base constructor calls (arguments) from derived -> base
+	auto baseArgs = baseArguments(_contract);
+	for (auto base: _contract.annotation().linearizedBaseContracts)
+	{
+		if (base != &_contract)
+		{
+			m_callGraph[&_contract].insert(base);
+			vector<ASTPointer<Expression>> const& args = baseArgs.count(base) ? baseArgs.at(base) : decltype(args){};
+
+			auto baseConstructor = base->constructor();
+			if (baseConstructor && !args.empty())
+			{
+				auto const& params = baseConstructor->parameters();
+				solAssert(params.size() == args.size(), "");
+				for (unsigned i = 0; i < params.size(); ++i)
+				{
+					args.at(i)->accept(*this);
+					if (params.at(i))
+					{
+						solAssert(m_context.knownVariable(*params.at(i)), "");
+						m_context.addAssertion(currentValue(*params.at(i)) == expr(*args.at(i), params.at(i)->type()));
+					}
+				}
+			}
+		}
+	}
+	m_errorDest = nullptr;
+	// Then call initializer_Base from base -> derived
+	for (auto base: _contract.annotation().linearizedBaseContracts | boost::adaptors::reversed)
+	{
+		errorFlag().increaseIndex();
+		m_context.addAssertion(smt::constructorCall(*m_contractInitializers.at(base), m_context));
+		connectBlocks(m_currentBlock, summary(_contract), errorFlag().currentValue() > 0);
+		m_context.addAssertion(errorFlag().currentValue() == 0);
+	}
 
 	connectBlocks(m_currentBlock, summary(_contract));
 
-	setCurrentBlock(*m_constructorSummaryPredicate);
+	setCurrentBlock(*m_constructorSummaries.at(&_contract));
-
 	m_queryPlaceholders[&_contract].push_back({smtutil::Expression(true), errorFlag().currentValue(), m_currentBlock});
 	connectBlocks(m_currentBlock, interface(), errorFlag().currentValue() == 0);
 
@@ -168,16 +196,7 @@ bool CHC::visit(FunctionDefinition const& _function)
 		return false;
 	}
 
-	// This is the case for base constructor inlining.
+	// No inlining.
-	if (m_currentFunction)
-	{
-		solAssert(m_currentFunction->isConstructor(), "");
-		solAssert(_function.isConstructor(), "");
-		solAssert(_function.scope() != m_currentContract, "");
-		SMTEncoder::visit(_function);
-		return false;
-	}
-
 	solAssert(!m_currentFunction, "Function inlining should not happen in CHC.");
 	m_currentFunction = &_function;
 
@@ -189,23 +208,19 @@ bool CHC::visit(FunctionDefinition const& _function)
 	auto functionPred = predicate(*functionEntryBlock);
 	auto bodyPred = predicate(*bodyBlock);
 
-	if (_function.isConstructor())
+	addRule(functionPred, functionPred.name);
-		connectBlocks(m_currentBlock, functionPred);
-	else
-		addRule(functionPred, functionPred.name);
 
-	m_context.addAssertion(errorFlag().currentValue() == 0);
+	solAssert(m_currentContract, "");
-	for (auto const* var: m_stateVariables)
+	m_context.addAssertion(initialConstraints(*m_currentContract, &_function));
-		m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
-	for (auto const& var: _function.parameters())
-		m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
-	m_context.addAssertion(state().state(0) == state().state());
 
 	connectBlocks(functionPred, bodyPred);
 
 	setCurrentBlock(*bodyBlock);
 
+	solAssert(!m_errorDest, "");
+	m_errorDest = m_summaries.at(m_currentContract).at(&_function);
 	SMTEncoder::visit(*m_currentFunction);
+	m_errorDest = nullptr;
 
 	return false;
 }
@@ -216,55 +231,29 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		return;
 
 	solAssert(m_currentFunction && m_currentContract, "");
+	// No inlining.
+	solAssert(m_currentFunction == &_function, "");
 
-	// This is the case for base constructor inlining.
+	connectBlocks(m_currentBlock, summary(_function));
-	if (m_currentFunction != &_function)
+	setCurrentBlock(*m_summaries.at(m_currentContract).at(&_function));
+
+	// Query placeholders for constructors are not created here because
+	// of contracts without constructors.
+	// Instead, those are created in endVisit(ContractDefinition).
+	if (!_function.isConstructor())
 	{
-		solAssert(m_currentFunction && m_currentFunction->isConstructor(), "");
+		auto sum = summary(_function);
-		solAssert(_function.isConstructor(), "");
+		auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
-		solAssert(_function.scope() != m_currentContract, "");
+		if (_function.isPublic())
-	}
-	else
-	{
-		// We create an extra exit block for constructors that simply
-		// connects to the interface in case an explicit constructor
-		// exists in the hierarchy.
-		// It is not connected directly here, as normal functions are,
-		// because of the case where there are only implicit constructors.
-		// This is done in endVisit(ContractDefinition).
-		if (_function.isConstructor())
 		{
-			string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
+			auto txConstraints = m_context.state().txConstraints(_function);
-			solAssert(m_currentContract, "");
+			m_queryPlaceholders[&_function].push_back({txConstraints && sum, errorFlag().currentValue(), ifacePre});
-			auto constructorExit = createSymbolicBlock(
+			connectBlocks(ifacePre, interface(), txConstraints && sum && errorFlag().currentValue() == 0);
-				constructorSort(*m_currentContract, state()),
-				"constructor_exit_" + suffix,
-				PredicateType::ConstructorSummary,
-				m_currentContract
-			);
-			connectBlocks(m_currentBlock, predicate(*constructorExit));
-
-			setCurrentBlock(*constructorExit);
 		}
-		else
-		{
-			auto assertionError = errorFlag().currentValue();
-			auto sum = summary(_function);
-			connectBlocks(m_currentBlock, sum);
-			auto iface = interface();
-			setCurrentBlock(*m_interfaces.at(m_currentContract));
-
-			auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
-			if (_function.isPublic())
-			{
-				auto txConstraints = m_context.state().txConstraints(_function);
-				m_queryPlaceholders[&_function].push_back({txConstraints && sum, assertionError, ifacePre});
-				connectBlocks(ifacePre, iface, txConstraints && sum && (assertionError == 0));
-			}
-		}
-		m_currentFunction = nullptr;
 	}
 
+	m_currentFunction = nullptr;
+
 	SMTEncoder::endVisit(_function);
 }
 
@@ -564,10 +553,11 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 
 	m_context.addAssertion(predicate(_funCall));
 
+	solAssert(m_errorDest, "");
 	connectBlocks(
 		m_currentBlock,
-		(m_currentFunction && !m_currentFunction->isConstructor()) ? summary(*m_currentFunction) : summary(*m_currentContract),
+		predicate(*m_errorDest),
-		(errorFlag().currentValue() > 0)
+		errorFlag().currentValue() > 0
 	);
 	m_context.addAssertion(errorFlag().currentValue() == 0);
 }
@@ -644,9 +634,10 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 	state().newTx();
 	m_context.addAssertion(originalTx == state().tx());
 
+	solAssert(m_errorDest, "");
 	connectBlocks(
 		m_currentBlock,
-		(m_currentFunction && !m_currentFunction->isConstructor()) ? summary(*m_currentFunction) : summary(*m_currentContract),
+		predicate(*m_errorDest),
 		(errorFlag().currentValue() > 0)
 	);
 	m_context.addAssertion(errorFlag().currentValue() == 0);
@@ -728,6 +719,8 @@ void CHC::resetSourceAnalysis()
 	m_summaries.clear();
 	m_interfaces.clear();
 	m_nondetInterfaces.clear();
+	m_constructorSummaries.clear();
+	m_contractInitializers.clear();
 	Predicate::reset();
 	ArraySlicePredicate::reset();
 	m_blockCounter = 0;
@@ -840,6 +833,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 			string suffix = contract->name() + "_" + to_string(contract->id());
 			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + suffix, PredicateType::Interface, contract);
 			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract);
+			m_constructorSummaries[contract] = createConstructorBlock(*contract, "summary_constructor");
+			m_contractInitializers[contract] = createConstructorBlock(*contract, "contract_initializer");
 
 			for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract))
 				if (!m_context.knownVariable(*var))
@@ -890,6 +885,39 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 		}
 }
 
+void CHC::defineContractInitializer(ContractDefinition const& _contract)
+{
+	auto const& implicitConstructorPredicate = *createConstructorBlock(_contract, "contract_initializer_entry");
+
+	auto implicitFact = smt::constructor(implicitConstructorPredicate, m_context);
+	addRule(smtutil::Expression::implies(initialConstraints(_contract), implicitFact), implicitFact.name);
+	setCurrentBlock(implicitConstructorPredicate);
+
+	solAssert(!m_errorDest, "");
+	m_errorDest = m_contractInitializers.at(&_contract);
+	for (auto var: _contract.stateVariables())
+		if (var->value())
+		{
+			var->value()->accept(*this);
+			assignment(*var, *var->value());
+		}
+	m_errorDest = nullptr;
+
+	auto const& afterInit = *createConstructorBlock(_contract, "contract_initializer_after_init");
+	connectBlocks(m_currentBlock, predicate(afterInit));
+	setCurrentBlock(afterInit);
+
+	if (auto constructor = _contract.constructor())
+	{
+		errorFlag().increaseIndex();
+		m_context.addAssertion(smt::functionCall(*m_summaries.at(&_contract).at(constructor), &_contract, m_context));
+		connectBlocks(m_currentBlock, initializer(_contract), errorFlag().currentValue() > 0);
+		m_context.addAssertion(errorFlag().currentValue() == 0);
+	}
+
+	connectBlocks(m_currentBlock, initializer(_contract));
+}
+
 smtutil::Expression CHC::interface()
 {
 	solAssert(m_currentContract, "");
@@ -911,14 +939,19 @@ smtutil::Expression CHC::error(unsigned _idx)
 	return m_errorPredicate->functor(_idx)({});
 }
 
+smtutil::Expression CHC::initializer(ContractDefinition const& _contract)
+{
+	return predicate(*m_contractInitializers.at(&_contract));
+}
+
 smtutil::Expression CHC::summary(ContractDefinition const& _contract)
 {
-	return constructor(*m_constructorSummaryPredicate, _contract, m_context);
+	return predicate(*m_constructorSummaries.at(&_contract));
 }
 
 smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
-	return smt::function(*m_summaries.at(&_contract).at(&_function), _function, &_contract, m_context);
+	return smt::function(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
 }
 
 smtutil::Expression CHC::summary(FunctionDefinition const& _function)
@@ -942,14 +975,22 @@ Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType,
 
 Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
-	auto block = createSymbolicBlock(
+	return createSymbolicBlock(
 		functionSort(_function, &_contract, state()),
 		"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
 		PredicateType::FunctionSummary,
 		&_function
 	);
+}
 
-	return block;
+Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract, string const& _prefix)
+{
+	return createSymbolicBlock(
+		constructorSort(_contract, state()),
+		_prefix + "_" + contractSuffix(_contract) + "_" + uniquePrefix(),
+		PredicateType::ConstructorSummary,
+		&_contract
+	);
 }
 
 void CHC::createErrorBlock()
@@ -967,6 +1008,21 @@ void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression co
 	addRule(edge, _from.name + "_to_" + _to.name);
 }
 
+smtutil::Expression CHC::initialConstraints(ContractDefinition const& _contract, FunctionDefinition const* _function)
+{
+	smtutil::Expression conj = state().state() == state().state(0);
+	conj = conj && errorFlag().currentValue() == 0;
+	for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
+		conj = conj && m_context.variable(*var)->valueAtIndex(0) == currentValue(*var);
+
+	FunctionDefinition const* function = _function ? _function : _contract.constructor();
+	if (function)
+		for (auto var: function->parameters())
+			conj = conj && m_context.variable(*var)->valueAtIndex(0) == currentValue(*var);
+
+	return conj;
+}
+
 vector<smtutil::Expression> CHC::initialStateVariables()
 {
 	return stateVariablesAtIndex(0);
@@ -1021,16 +1077,11 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
 	case PredicateType::Interface:
 		solAssert(m_currentContract, "");
 		return ::interface(_block, *m_currentContract, m_context);
-	case PredicateType::ImplicitConstructor:
-		solAssert(m_currentContract, "");
-		return implicitConstructor(_block, *m_currentContract, m_context);
 	case PredicateType::ConstructorSummary:
-		solAssert(m_currentContract, "");
+		return constructor(_block, m_context);
-		return constructor(_block, *m_currentContract, m_context);
 	case PredicateType::FunctionEntry:
 	case PredicateType::FunctionSummary:
-		solAssert(m_currentFunction, "");
+		return smt::function(_block, m_currentContract, m_context);
-		return smt::function(_block, *m_currentFunction, m_currentContract, m_context);
 	case PredicateType::FunctionBlock:
 		solAssert(m_currentFunction, "");
 		return functionBlock(_block, *m_currentFunction, m_currentContract, m_context);
@@ -1173,9 +1224,10 @@ void CHC::verificationTargetEncountered(
 	errorFlag().increaseIndex();
 
 	// create an error edge to the summary
+	solAssert(m_errorDest, "");
 	connectBlocks(
 		m_currentBlock,
-		scopeIsFunction ? summary(*m_currentFunction) : summary(*m_currentContract),
+		predicate(*m_errorDest),
 		currentPathConditions() && _errorCondition && errorFlag().currentValue() == errorId
 	);
 
@@ -1416,16 +1468,12 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
 		path.emplace_back(txCex);
 
-		/// Recurse on the next interface node which represents the previous transaction
+		/// Stop when we reach the summary of the analyzed constructor.
-		/// or stop.
+		if (summaryPredicate->type() == PredicateType::ConstructorSummary)
-		if (interfaceId)
-		{
-			Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).name);
-			solAssert(interfacePredicate && interfacePredicate->isInterface(), "");
-			node = *interfaceId;
-		}
-		else
 			break;
+
+		/// Recurse on the next interface node which represents the previous transaction.
+		node = *interfaceId;
 	}
 
 	return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");

libsolidity/formal/CHC.h

@@ -126,6 +126,11 @@ private:
 	/// in a given _source.
 	void defineInterfacesAndSummaries(SourceUnit const& _source);
 
+	/// Creates a CHC system that, for a given contract,
+	/// - initializes its state variables (as 0 or given value, if any).
+	/// - "calls" the explicit constructor function of the contract, if any.
+	void defineContractInitializer(ContractDefinition const& _contract);
+
 	/// Interface predicate over current variables.
 	smtutil::Expression interface();
 	smtutil::Expression interface(ContractDefinition const& _contract);
@@ -139,12 +144,18 @@ private:
 	/// The contract is needed here because of inheritance.
 	Predicate const* createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract);
 
+	/// @returns a block related to @a _contract's constructor.
+	Predicate const* createConstructorBlock(ContractDefinition const& _contract, std::string const& _prefix);
+
 	/// Creates a new error block to be used by an assertion.
 	/// Also registers the predicate.
 	void createErrorBlock();
 
 	void connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints = smtutil::Expression(true));
 
+	/// @returns The initial constraints that set up the beginning of a function.
+	smtutil::Expression initialConstraints(ContractDefinition const& _contract, FunctionDefinition const* _function = nullptr);
+
 	/// @returns the symbolic values of the state variables at the beginning
 	/// of the current transaction.
 	std::vector<smtutil::Expression> initialStateVariables();
@@ -160,6 +171,8 @@ private:
 	smtutil::Expression predicate(Predicate const& _block);
 	/// @returns the summary predicate for the called function.
 	smtutil::Expression predicate(FunctionCall const& _funCall);
+	/// @returns a predicate that defines a contract initializer.
+	smtutil::Expression initializer(ContractDefinition const& _contract);
 	/// @returns a predicate that defines a constructor summary.
 	smtutil::Expression summary(ContractDefinition const& _contract);
 	/// @returns a predicate that defines a function summary.
@@ -231,10 +244,6 @@ private:
 
 	/// Predicates.
 	//@{
-	/// Constructor summary predicate, exists after the constructor
-	/// (implicit or explicit) and before the interface.
-	Predicate const* m_constructorSummaryPredicate = nullptr;
-
 	/// Artificial Interface predicate.
 	/// Single entry block for all functions.
 	std::map<ContractDefinition const*, Predicate const*> m_interfaces;
@@ -245,6 +254,9 @@ private:
 	/// nondeterministically.
 	std::map<ContractDefinition const*, Predicate const*> m_nondetInterfaces;
 
+	std::map<ContractDefinition const*, Predicate const*> m_constructorSummaries;
+	std::map<ContractDefinition const*, Predicate const*> m_contractInitializers;
+
 	/// Artificial Error predicate.
 	/// Single error block for all assertions.
 	Predicate const* m_errorPredicate = nullptr;
@@ -311,9 +323,16 @@ private:
 	bool m_unknownFunctionCallSeen = false;
 
 	/// Block where a loop break should go to.
-	Predicate const* m_breakDest;
+	Predicate const* m_breakDest = nullptr;
 	/// Block where a loop continue should go to.
-	Predicate const* m_continueDest;
+	Predicate const* m_continueDest = nullptr;
+
+	/// Block where an error condition should go to.
+	/// This can be:
+	/// 1) Constructor initializer summary, if error happens while evaluating initial values of state variables.
+	/// 2) Constructor summary, if error happens while evaluating base constructor arguments.
+	/// 3) Function summary, if error happens inside a function.
+	Predicate const* m_errorDest = nullptr;
 	//@}
 
 	/// CHC solver.

libsolidity/formal/Predicate.cpp

@@ -141,12 +141,12 @@ optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
 
 bool Predicate::isSummary() const
 {
-	return functor().name.rfind("summary", 0) == 0;
+	return m_type == PredicateType::ConstructorSummary || m_type == PredicateType::FunctionSummary;
 }
 
 bool Predicate::isInterface() const
 {
-	return functor().name.rfind("interface", 0) == 0;
+	return m_type == PredicateType::Interface;
 }
 
 string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) const
@@ -190,7 +190,7 @@ string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) co
 vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expression> const& _args) const
 {
 	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
-	/// The signature of an implicit constructor summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, postStateVars).
+	/// The signature of the summary predicate of a contract without constructor is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars).
 	/// Here we are interested in postStateVars.
 	auto stateVars = stateVariables();
 	solAssert(stateVars.has_value(), "");
@@ -204,7 +204,7 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
 	}
 	else if (programContract())
 	{
-		stateFirst = _args.begin() + 6;
+		stateFirst = _args.begin() + 6 + static_cast<int>(stateVars->size());
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else

libsolidity/formal/Predicate.h

@@ -34,7 +34,6 @@ enum class PredicateType
 {
 	Interface,
 	NondetInterface,
-	ImplicitConstructor,
 	ConstructorSummary,
 	FunctionEntry,
 	FunctionSummary,

libsolidity/formal/PredicateInstance.cpp

@@ -51,31 +51,50 @@ smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition c
 	);
 }
 
-smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context)
+smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context)
 {
-	auto& state = _context.state();
+	auto const& contract = dynamic_cast<ContractDefinition const&>(*_pred.programNode());
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)};
+	if (auto const* constructor = contract.constructor())
-	return _pred(stateExprs);
+		return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context));
-}
-
-smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
-{
-	if (auto const* constructor = _contract.constructor())
-		return _pred(currentFunctionVariables(*constructor, &_contract, _context));
 
 	auto& state = _context.state();
 	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
-	return _pred(stateExprs + currentStateVariables(_contract, _context));
+	return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context));
+}
+
+smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context)
+{
+	auto const& contract = dynamic_cast<ContractDefinition const&>(*_pred.programNode());
+	if (auto const* constructor = contract.constructor())
+		return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context));
+
+	auto& state = _context.state();
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state()};
+	state.newState();
+	stateExprs += vector<smtutil::Expression>{state.state()};
+	stateExprs += currentStateVariables(contract, _context);
+	stateExprs += newStateVariables(contract, _context);
+	return _pred(stateExprs);
 }
 
 smtutil::Expression function(
 	Predicate const& _pred,
-	FunctionDefinition const& _function,
 	ContractDefinition const* _contract,
 	EncodingContext& _context
 )
 {
-	return _pred(currentFunctionVariables(_function, _contract, _context));
+	auto const& function = dynamic_cast<FunctionDefinition const&>(*_pred.programNode());
+	return _pred(currentFunctionVariablesForDefinition(function, _contract, _context));
+}
+
+smtutil::Expression functionCall(
+	Predicate const& _pred,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+)
+{
+	auto const& function = dynamic_cast<FunctionDefinition const&>(*_pred.programNode());
+	return _pred(currentFunctionVariablesForCall(function, _contract, _context));
 }
 
 smtutil::Expression functionBlock(
@@ -111,14 +130,22 @@ vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _con
 	);
 }
 
-vector<smtutil::Expression> currentFunctionVariables(
+vector<smtutil::Expression> newStateVariables(ContractDefinition const& _contract, EncodingContext& _context)
+{
+	return applyMap(
+		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
+		[&](auto _var) { return _context.variable(*_var)->increaseIndex(); }
+	);
+}
+
+vector<smtutil::Expression> currentFunctionVariablesForDefinition(
 	FunctionDefinition const& _function,
 	ContractDefinition const* _contract,
 	EncodingContext& _context
 )
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)};
+	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)};
 	exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
 	exprs += vector<smtutil::Expression>{state.state()};
@@ -128,9 +155,29 @@ vector<smtutil::Expression> currentFunctionVariables(
 	return exprs;
 }
 
+vector<smtutil::Expression> currentFunctionVariablesForCall(
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+)
+{
+	auto& state = _context.state();
+	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state()};
+	exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
+	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
+
+	state.newState();
+
+	exprs += vector<smtutil::Expression>{state.state()};
+	exprs += _contract ? newStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
+	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->increaseIndex(); });
+	exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
+	return exprs;
+}
+
 vector<smtutil::Expression> currentBlockVariables(FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context)
 {
-	return currentFunctionVariables(_function, _contract, _context) +
+	return currentFunctionVariablesForDefinition(_function, _contract, _context) +
 		applyMap(
 			SMTEncoder::localVariablesIncludingModifiers(_function),
 			[&](auto _var) { return _context.variable(*_var)->currentValue(); }

libsolidity/formal/PredicateInstance.h

@@ -36,13 +36,17 @@ smtutil::Expression interface(Predicate const& _pred, ContractDefinition const&
 
 smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx);
 
-smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
+smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context);
-
+smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context);
-smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
 
 smtutil::Expression function(
 	Predicate const& _pred,
-	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+);
+
+smtutil::Expression functionCall(
+	Predicate const& _pred,
 	ContractDefinition const* _contract,
 	EncodingContext& _context
 );
@@ -62,7 +66,15 @@ std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, Contract
 
 std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context);
 
-std::vector<smtutil::Expression> currentFunctionVariables(
+std::vector<smtutil::Expression> newStateVariables(ContractDefinition const& _contract, EncodingContext& _context);
+
+std::vector<smtutil::Expression> currentFunctionVariablesForDefinition(
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+);
+
+std::vector<smtutil::Expression> currentFunctionVariablesForCall(
 	FunctionDefinition const& _function,
 	ContractDefinition const* _contract,
 	EncodingContext& _context

libsolidity/formal/PredicateSort.cpp

@@ -46,21 +46,15 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta
 	);
 }
 
-SortPointer implicitConstructorSort(SymbolicState& _state)
-{
-	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()},
-		SortProvider::boolSort
-	);
-}
-
 SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state)
 {
 	if (auto const* constructor = _contract.constructor())
 		return functionSort(*constructor, &_contract, _state);
 
+	auto varSorts = stateSorts(_contract);
+	vector<SortPointer> stateSort{_state.stateSort()};
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract),
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
 		SortProvider::boolSort
 	);
 }

libsolidity/formal/PredicateSort.h

@@ -39,19 +39,17 @@ namespace solidity::frontend::smt
  * The nondeterminism behavior of a contract. Signature:
  * nondet_interface(blockchainState, stateVariables, blockchainState', stateVariables').
  *
- * 3. Implicit constructor
+ * 3. Constructor entry/summary
- * The implicit constructor of a contract, that is, without input parameters. Signature:
+ * The summary of a contract's deployment procedure.
- * implicit_constructor(error, this, cryptoFunctions, txData, blockchainState).
+ * Signature:
+ * If the contract has a constructor function, this is the same as the summary of that function. Otherwise:
+ * constructor_summary(error, this, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables').
  *
- * 4. Constructor entry/summary
+ * 4. Function entry/summary
- * The summary of an implicit constructor. Signature:
- * constructor_summary(error, this, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables').
- *
- * 5. Function entry/summary
  * The entry point of a function definition. Signature:
  * function_entry(error, this, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
  *
- * 6. Function body
+ * 5. Function body
  * Use for any predicate within a function. Signature:
  * function_body(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables).
  */
@@ -62,9 +60,6 @@ smtutil::SortPointer interfaceSort(ContractDefinition const& _contract, Symbolic
 /// @returns the nondeterminisc interface predicate sort for _contract.
 smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state);
 
-/// @returns the implicit constructor predicate sort.
-smtutil::SortPointer implicitConstructorSort(SymbolicState& _state);
-
 /// @returns the constructor entry/summary predicate sort for _contract.
 smtutil::SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state);
 

libsolidity/formal/SMTEncoder.cpp

@@ -131,9 +131,6 @@ bool SMTEncoder::visit(FunctionDefinition const& _function)
 {
 	m_modifierDepthStack.push_back(-1);
 
-	if (_function.isConstructor())
-		inlineConstructorHierarchy(dynamic_cast<ContractDefinition const&>(*_function.scope()));
-
 	initializeLocalVariables(_function);
 
 	_function.parameterList().accept(*this);
@@ -2558,6 +2555,37 @@ SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
 	solAssert(false, "");
 }
 
+map<ContractDefinition const*, vector<ASTPointer<frontend::Expression>>> SMTEncoder::baseArguments(ContractDefinition const& _contract)
+{
+	map<ContractDefinition const*, vector<ASTPointer<Expression>>> baseArgs;
+
+	for (auto contract: _contract.annotation().linearizedBaseContracts)
+	{
+		/// Collect base contracts and potential constructor arguments.
+		for (auto specifier: contract->baseContracts())
+		{
+			solAssert(specifier, "");
+			auto const& base = dynamic_cast<ContractDefinition const&>(*specifier->name().annotation().referencedDeclaration);
+			if (auto args = specifier->arguments())
+				baseArgs[&base] = *args;
+		}
+		/// Collect base constructor arguments given as constructor modifiers.
+		if (auto constructor = contract->constructor())
+			for (auto mod: constructor->modifiers())
+			{
+				auto decl = mod->name()->annotation().referencedDeclaration;
+				if (auto base = dynamic_cast<ContractDefinition const*>(decl))
+				{
+					solAssert(!baseArgs.count(base), "");
+					if (auto args = mod->arguments())
+						baseArgs[base] = *args;
+				}
+			}
+	}
+
+	return baseArgs;
+}
+
 void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 {
 	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);

libsolidity/formal/SMTEncoder.h

@@ -77,6 +77,9 @@ public:
 	/// @returns the SourceUnit that contains _scopable.
 	static SourceUnit const* sourceUnitContaining(Scopable const& _scopable);
 
+	/// @returns the arguments for each base constructor call in the hierarchy of @a _contract.
+	std::map<ContractDefinition const*, std::vector<ASTPointer<frontend::Expression>>> baseArguments(ContractDefinition const& _contract);
+
 protected:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined

libyul/Dialect.h

@@ -74,6 +74,8 @@ struct Dialect: boost::noncopyable
 
 	virtual BuiltinFunction const* memoryStoreFunction(YulString /* _type */) const { return nullptr; }
 	virtual BuiltinFunction const* memoryLoadFunction(YulString /* _type */) const { return nullptr; }
+	virtual BuiltinFunction const* storageStoreFunction(YulString /* _type */) const { return nullptr; }
+	virtual BuiltinFunction const* storageLoadFunction(YulString /* _type */) const { return nullptr; }
 
 	/// Check whether the given type is legal for the given literal value.
 	/// Should only be called if the type exists in the dialect at all.

libyul/backends/evm/EVMDialect.h

@@ -75,6 +75,8 @@ struct EVMDialect: public Dialect
 	BuiltinFunctionForEVM const* booleanNegationFunction() const override { return builtin("iszero"_yulstring); }
 	BuiltinFunctionForEVM const* memoryStoreFunction(YulString /*_type*/) const override { return builtin("mstore"_yulstring); }
 	BuiltinFunctionForEVM const* memoryLoadFunction(YulString /*_type*/) const override { return builtin("mload"_yulstring); }
+	BuiltinFunctionForEVM const* storageStoreFunction(YulString /*_type*/) const override { return builtin("sstore"_yulstring); }
+	BuiltinFunctionForEVM const* storageLoadFunction(YulString /*_type*/) const override { return builtin("sload"_yulstring); }
 
 	static EVMDialect const& strictAssemblyForEVM(langutil::EVMVersion _version);
 	static EVMDialect const& strictAssemblyForEVMObjects(langutil::EVMVersion _version);

libyul/optimiser/DataFlowAnalyzer.cpp

@@ -25,8 +25,8 @@
 #include <libyul/optimiser/NameCollector.h>
 #include <libyul/optimiser/Semantics.h>
 #include <libyul/AST.h>
+#include <libyul/Dialect.h>
 #include <libyul/Exceptions.h>
-#include <libyul/backends/evm/EVMDialect.h>
 
 #include <libsolutil/CommonData.h>
 
@@ -39,9 +39,27 @@ using namespace solidity;
 using namespace solidity::util;
 using namespace solidity::yul;
 
+DataFlowAnalyzer::DataFlowAnalyzer(
+	Dialect const& _dialect,
+	map<YulString, SideEffects> _functionSideEffects
+):
+m_dialect(_dialect),
+m_functionSideEffects(std::move(_functionSideEffects)),
+m_knowledgeBase(_dialect, m_value)
+{
+	if (auto const* builtin = _dialect.memoryStoreFunction(YulString{}))
+		m_storeFunctionName[static_cast<unsigned>(StoreLoadLocation::Memory)] = builtin->name;
+	if (auto const* builtin = _dialect.memoryLoadFunction(YulString{}))
+		m_loadFunctionName[static_cast<unsigned>(StoreLoadLocation::Memory)] = builtin->name;
+	if (auto const* builtin = _dialect.storageStoreFunction(YulString{}))
+		m_storeFunctionName[static_cast<unsigned>(StoreLoadLocation::Storage)] = builtin->name;
+	if (auto const* builtin = _dialect.storageLoadFunction(YulString{}))
+		m_loadFunctionName[static_cast<unsigned>(StoreLoadLocation::Storage)] = builtin->name;
+}
+
 void DataFlowAnalyzer::operator()(ExpressionStatement& _statement)
 {
-	if (auto vars = isSimpleStore(evmasm::Instruction::SSTORE, _statement))
+	if (auto vars = isSimpleStore(StoreLoadLocation::Storage, _statement))
 	{
 		ASTModifier::operator()(_statement);
 		set<YulString> keysToErase;
@@ -55,7 +73,7 @@ void DataFlowAnalyzer::operator()(ExpressionStatement& _statement)
 			m_storage.eraseKey(key);
 		m_storage.set(vars->first, vars->second);
 	}
-	else if (auto vars = isSimpleStore(evmasm::Instruction::MSTORE, _statement))
+	else if (auto vars = isSimpleStore(StoreLoadLocation::Memory, _statement))
 	{
 		ASTModifier::operator()(_statement);
 		set<YulString> keysToErase;
@@ -265,9 +283,9 @@ void DataFlowAnalyzer::handleAssignment(set<YulString> const& _variables, Expres
 			// This might erase additional knowledge about the slot.
 			// On the other hand, if we knew the value in the slot
 			// already, then the sload() / mload() would have been replaced by a variable anyway.
-			if (auto key = isSimpleLoad(evmasm::Instruction::MLOAD, *_value))
+			if (auto key = isSimpleLoad(StoreLoadLocation::Memory, *_value))
 				m_memory.set(*key, variable);
-			else if (auto key = isSimpleLoad(evmasm::Instruction::SLOAD, *_value))
+			else if (auto key = isSimpleLoad(StoreLoadLocation::Storage, *_value))
 				m_storage.set(*key, variable);
 		}
 	}
@@ -391,53 +409,27 @@ bool DataFlowAnalyzer::inScope(YulString _variableName) const
 }
 
 std::optional<pair<YulString, YulString>> DataFlowAnalyzer::isSimpleStore(
-	evmasm::Instruction _store,
+	StoreLoadLocation _location,
 	ExpressionStatement const& _statement
 ) const
 {
-	yulAssert(
+	if (FunctionCall const* funCall = get_if<FunctionCall>(&_statement.expression))
-		_store == evmasm::Instruction::MSTORE ||
+		if (funCall->functionName.name == m_storeFunctionName[static_cast<unsigned>(_location)])
-		_store == evmasm::Instruction::SSTORE,
+			if (Identifier const* key = std::get_if<Identifier>(&funCall->arguments.front()))
-		""
+				if (Identifier const* value = std::get_if<Identifier>(&funCall->arguments.back()))
-	);
+					return make_pair(key->name, value->name);
-	if (holds_alternative<FunctionCall>(_statement.expression))
-	{
-		FunctionCall const& funCall = std::get<FunctionCall>(_statement.expression);
-		if (EVMDialect const* dialect = dynamic_cast<EVMDialect const*>(&m_dialect))
-			if (auto const* builtin = dialect->builtin(funCall.functionName.name))
-				if (builtin->instruction == _store)
-					if (
-						holds_alternative<Identifier>(funCall.arguments.at(0)) &&
-						holds_alternative<Identifier>(funCall.arguments.at(1))
-					)
-					{
-						YulString key = std::get<Identifier>(funCall.arguments.at(0)).name;
-						YulString value = std::get<Identifier>(funCall.arguments.at(1)).name;
-						return make_pair(key, value);
-					}
-	}
 	return {};
 }
 
 std::optional<YulString> DataFlowAnalyzer::isSimpleLoad(
-	evmasm::Instruction _load,
+	StoreLoadLocation _location,
 	Expression const& _expression
 ) const
 {
-	yulAssert(
+	if (FunctionCall const* funCall = get_if<FunctionCall>(&_expression))
-		_load == evmasm::Instruction::MLOAD ||
+		if (funCall->functionName.name == m_loadFunctionName[static_cast<unsigned>(_location)])
-		_load == evmasm::Instruction::SLOAD,
+			if (Identifier const* key = std::get_if<Identifier>(&funCall->arguments.front()))
-		""
+				return key->name;
-	);
-	if (holds_alternative<FunctionCall>(_expression))
-	{
-		FunctionCall const& funCall = std::get<FunctionCall>(_expression);
-		if (EVMDialect const* dialect = dynamic_cast<EVMDialect const*>(&m_dialect))
-			if (auto const* builtin = dialect->builtin(funCall.functionName.name))
-				if (builtin->instruction == _load)
-					if (holds_alternative<Identifier>(funCall.arguments.at(0)))
-						return std::get<Identifier>(funCall.arguments.at(0)).name;
-	}
 	return {};
 }
 

libyul/optimiser/DataFlowAnalyzer.h

@@ -29,9 +29,6 @@
 #include <libyul/AST.h> // Needed for m_zero below.
 #include <libyul/SideEffects.h>
 
-// TODO avoid
-#include <libevmasm/Instruction.h>
-
 #include <libsolutil/InvertibleMap.h>
 
 #include <map>
@@ -89,11 +86,7 @@ public:
 	explicit DataFlowAnalyzer(
 		Dialect const& _dialect,
 		std::map<YulString, SideEffects> _functionSideEffects = {}
-	):
+	);
-		m_dialect(_dialect),
-		m_functionSideEffects(std::move(_functionSideEffects)),
-		m_knowledgeBase(_dialect, m_value)
-	{}
 
 	using ASTModifier::operator();
 	void operator()(ExpressionStatement& _statement) override;
@@ -143,17 +136,23 @@ protected:
 	/// Returns true iff the variable is in scope.
 	bool inScope(YulString _variableName) const;
 
+	enum class StoreLoadLocation {
+		Memory = 0,
+		Storage = 1,
+		Last = Storage
+	};
+
 	/// Checks if the statement is sstore(a, b) / mstore(a, b)
 	/// where a and b are variables and returns these variables in that case.
 	std::optional<std::pair<YulString, YulString>> isSimpleStore(
-		evmasm::Instruction _store,
+		StoreLoadLocation _location,
 		ExpressionStatement const& _statement
 	) const;
 
 	/// Checks if the expression is sload(a) / mload(a)
 	/// where a is a variable and returns the variable in that case.
 	std::optional<YulString> isSimpleLoad(
-		evmasm::Instruction _load,
+		StoreLoadLocation _location,
 		Expression const& _expression
 	) const;
 
@@ -173,6 +172,9 @@ protected:
 
 	KnowledgeBase m_knowledgeBase;
 
+	YulString m_storeFunctionName[static_cast<unsigned>(StoreLoadLocation::Last) + 1];
+	YulString m_loadFunctionName[static_cast<unsigned>(StoreLoadLocation::Last) + 1];
+
 	/// Current nesting depth of loops.
 	size_t m_loopDepth{0};
 

libyul/optimiser/LoadResolver.cpp

@@ -46,21 +46,18 @@ void LoadResolver::visit(Expression& _e)
 {
 	DataFlowAnalyzer::visit(_e);
 
-	if (!dynamic_cast<EVMDialect const*>(&m_dialect))
+	if (FunctionCall const* funCall = std::get_if<FunctionCall>(&_e))
-		return;
+		for (auto location: { StoreLoadLocation::Memory, StoreLoadLocation::Storage })
-
+			if (funCall->functionName.name == m_loadFunctionName[static_cast<unsigned>(location)])
-	if (holds_alternative<FunctionCall>(_e))
+			{
-	{
+				tryResolve(_e, location, funCall->arguments);
-		FunctionCall const& funCall = std::get<FunctionCall>(_e);
+				break;
-		if (auto const* builtin = dynamic_cast<EVMDialect const&>(m_dialect).builtin(funCall.functionName.name))
+			}
-			if (builtin->instruction)
-				tryResolve(_e, *builtin->instruction, funCall.arguments);
-	}
 }
 
 void LoadResolver::tryResolve(
 	Expression& _e,
-	evmasm::Instruction _instruction,
+	StoreLoadLocation _location,
 	vector<Expression> const& _arguments
 )
 {
@@ -69,13 +66,13 @@ void LoadResolver::tryResolve(
 
 	YulString key = std::get<Identifier>(_arguments.at(0)).name;
 	if (
-		_instruction == evmasm::Instruction::SLOAD &&
+		_location == StoreLoadLocation::Storage &&
 		m_storage.values.count(key)
 	)
 		_e = Identifier{locationOf(_e), m_storage.values[key]};
 	else if (
 		m_optimizeMLoad &&
-		_instruction == evmasm::Instruction::MLOAD &&
+		_location == StoreLoadLocation::Memory &&
 		m_memory.values.count(key)
 	)
 		_e = Identifier{locationOf(_e), m_memory.values[key]};

libyul/optimiser/LoadResolver.h

@@ -24,14 +24,10 @@
 
 #include <libyul/optimiser/DataFlowAnalyzer.h>
 #include <libyul/optimiser/OptimiserStep.h>
-#include <libevmasm/Instruction.h>
 
 namespace solidity::yul
 {
 
-struct EVMDialect;
-struct BuiltinFunctionForEVM;
-
 /**
  * Optimisation stage that replaces expressions of type ``sload(x)`` and ``mload(x)`` by the value
  * currently stored in storage resp. memory, if known.
@@ -63,7 +59,7 @@ protected:
 
 	void tryResolve(
 		Expression& _e,
-		evmasm::Instruction _instruction,
+		StoreLoadLocation _location,
 		std::vector<Expression> const& _arguments
 	);
 

scripts/chk_shellscripts/ignore.txt

@@ -1,12 +1,5 @@
 ./test/docsCodeStyle.sh
 ./test/cmdlineTests.sh
-./test/externalTests.sh
-./test/externalTests/common.sh
-./test/externalTests/gnosis.sh
-./test/externalTests/zeppelin.sh
-./test/externalTests/colony.sh
-./test/externalTests/solc-js/solc-js.sh
-./scripts/common.sh
 ./scripts/isoltest.sh
 ./scripts/get_version.sh
 ./scripts/soltest.sh

scripts/common.sh

@@ -1,3 +1,4 @@
+#!/usr/bin/env bash
 # ------------------------------------------------------------------------------
 # vim:ts=4:et
 # This file is part of solidity.
@@ -37,21 +38,21 @@ safe_kill()
     local n=1
 
     # only proceed if $PID does exist
-    kill -0 $PID 2>/dev/null || return
+    kill -0 "$PID" 2>/dev/null || return
 
     echo "Sending SIGTERM to ${NAME} (${PID}) ..."
-    kill $PID
+    kill "$PID"
 
     # wait until process terminated gracefully
-    while kill -0 $PID 2>/dev/null && [[ $n -le 4 ]]; do
+    while kill -0 "$PID" 2>/dev/null && [[ $n -le 4 ]]; do
         echo "Waiting ($n) ..."
         sleep 1
-        n=$[n + 1]
+        n=$((n + 1))
     done
 
     # process still alive? then hard-kill
-    if kill -0 $PID 2>/dev/null; then
+    if kill -0 "$PID" 2>/dev/null; then
         echo "Sending SIGKILL to ${NAME} (${PID}) ..."
-        kill -9 $PID
+        kill -9 "$PID"
     fi
 }

test/externalTests.sh

@@ -42,10 +42,10 @@ source test/externalTests/common.sh
 
 printTask "Running external tests..."
 
-$REPO_ROOT/externalTests/zeppelin.sh "$SOLJSON"
+"$REPO_ROOT/externalTests/zeppelin.sh" "$SOLJSON"
-$REPO_ROOT/externalTests/gnosis.sh "$SOLJSON"
+"$REPO_ROOT/externalTests/gnosis.sh" "$SOLJSON"
-$REPO_ROOT/externalTests/colony.sh "$SOLJSON"
+"$REPO_ROOT/externalTests/colony.sh" "$SOLJSON"
-$REPO_ROOT/externalTests/ens.sh "$SOLJSON"
+"$REPO_ROOT/externalTests/ens.sh" "$SOLJSON"
 
 # Disabled temporarily as it needs to be updated to latest Truffle first.
 #test_truffle Gnosis https://github.com/axic/pm-contracts.git solidity-050

test/externalTests/colony.sh

@@ -31,18 +31,17 @@ function test_fn { yarn run test:contracts; }
 function colony_test
 {
     OPTIMIZER_LEVEL=3
-    FORCE_ABIv2=false
     CONFIG="truffle.js"
 
-    truffle_setup https://github.com/solidity-external-tests/colonyNetwork.git develop_080
+    truffle_setup "$SOLJSON" https://github.com/solidity-external-tests/colonyNetwork.git develop_080
-    run_install install_fn
+    run_install "$SOLJSON" install_fn
 
     cd lib
     rm -Rf dappsys
     git clone https://github.com/solidity-external-tests/dappsys-monolithic.git -b master_080 dappsys
     cd ..
 
-    truffle_run_test compile_fn test_fn
+    truffle_run_test "$SOLJSON" compile_fn test_fn "NO-FORCE-ABI-V2"
 }
 
 external_test ColonyNetworks colony_test

test/externalTests/common.sh

@@ -40,9 +40,10 @@ function verify_version_input
 
 function setup
 {
-    local branch="$1"
+    local soljson="$1"
+    local branch="$2"
 
-    setup_solcjs "$DIR" "$SOLJSON" "$branch" "solc"
+    setup_solcjs "$DIR" "$soljson" "$branch" "solc"
     cd solc
 }
 
@@ -80,7 +81,7 @@ function download_project
     printLog "Cloning $branch of $repo..."
     git clone --depth 1 "$repo" -b "$branch" "$dir/ext"
     cd ext
-    echo "Current commit hash: `git rev-parse HEAD`"
+    echo "Current commit hash: $(git rev-parse HEAD)"
 }
 
 function force_truffle_version
@@ -92,10 +93,11 @@ function force_truffle_version
 
 function truffle_setup
 {
-    local repo="$1"
+    local soljson="$1"
-    local branch="$2"
+    local repo="$2"
+    local branch="$3"
 
-    setup_solcjs "$DIR" "$SOLJSON" "master" "solc"
+    setup_solcjs "$DIR" "$soljson" "master" "solc"
     download_project "$repo" "$branch" "$DIR"
 }
 
@@ -207,11 +209,12 @@ function clean
 
 function run_install
 {
-    local init_fn="$1"
+    local soljson="$1"
+    local init_fn="$2"
     printLog "Running install function..."
 
     replace_version_pragmas
-    force_solc "$CONFIG" "$DIR" "$SOLJSON"
+    force_solc "$CONFIG" "$DIR" "$soljson"
 
     $init_fn
 }
@@ -232,11 +235,15 @@ function run_test
 
 function truffle_run_test
 {
-    local compile_fn="$1"
+    local soljson="$1"
-    local test_fn="$2"
+    local compile_fn="$2"
+    local test_fn="$3"
+    local force_abi_v2_flag="$4"
+
+    test "$force_abi_v2_flag" = "FORCE-ABI-V2" || test "$force_abi_v2_flag" = "NO-FORCE-ABI-V2"
 
     replace_version_pragmas
-    force_solc "$CONFIG" "$DIR" "$SOLJSON"
+    force_solc "$CONFIG" "$DIR" "$soljson"
 
     printLog "Checking optimizer level..."
     if [ -z "$OPTIMIZER_LEVEL" ]; then
@@ -258,7 +265,7 @@ function truffle_run_test
         clean
         force_solc_settings "$CONFIG" "$optimize" "istanbul"
         # Force abi coder v2 in the last step. Has to be the last because code is modified.
-        if [ "$FORCE_ABIv2" = true ]; then
+        if [ "$force_abi_v2_flag" = "FORCE-ABI-V2" ]; then
             [[ "$optimize" =~ yul ]] && force_abi_v2
         fi
 

test/externalTests/ens.sh

@@ -18,9 +18,7 @@
 #
 # (c) 2019 solidity contributors.
 #------------------------------------------------------------------------------
-# shellcheck disable=SC1091
 source scripts/common.sh
-# shellcheck disable=SC1091
 source test/externalTests/common.sh
 
 verify_input "$1"
@@ -35,14 +33,14 @@ function ens_test
     export OPTIMIZER_LEVEL=1
     export CONFIG="truffle-config.js"
 
-    truffle_setup https://github.com/solidity-external-tests/ens.git upgrade-0.8.0
+    truffle_setup "$SOLJSON" https://github.com/solidity-external-tests/ens.git upgrade-0.8.0
 
     # Use latest Truffle. Older versions crash on the output from 0.8.0.
     force_truffle_version ^5.1.55
 
-    run_install install_fn
+    run_install "$SOLJSON" install_fn
 
-    truffle_run_test compile_fn test_fn
+    truffle_run_test "$SOLJSON" compile_fn test_fn "NO-FORCE-ABI-V2"
 }
 
 external_test Ens ens_test

test/externalTests/gnosis.sh

@@ -33,17 +33,17 @@ function gnosis_safe_test
     OPTIMIZER_LEVEL=1
     CONFIG="truffle.js"
 
-    truffle_setup https://github.com/solidity-external-tests/safe-contracts.git development_080
+    truffle_setup "$SOLJSON" https://github.com/solidity-external-tests/safe-contracts.git development_080
 
     force_truffle_version ^5.0.42
     sed -i 's|github:gnosis/mock-contract#sol_0_5_0|github:solidity-external-tests/mock-contract#master_080|g' package.json
     rm -f package-lock.json
     rm -rf node_modules/
 
-    run_install install_fn
+    run_install "$SOLJSON" install_fn
     replace_libsolc_call
 
-    truffle_run_test compile_fn test_fn
+    truffle_run_test "$SOLJSON" compile_fn test_fn "NO-FORCE-ABI-V2"
 }
 
 external_test Gnosis-Safe gnosis_safe_test

test/externalTests/solc-js/solc-js.sh

@@ -35,16 +35,16 @@ function solcjs_test
     SOLCJS_INPUT_DIR="$TEST_DIR"/test/externalTests/solc-js
 
     # set up solc-js on the branch specified
-    setup master
+    setup "$SOLJSON" master
 
     printLog "Updating index.js file..."
     echo "require('./determinism.js');" >> test/index.js
 
     printLog "Copying determinism.js..."
-    cp -f $SOLCJS_INPUT_DIR/determinism.js test/
+    cp -f "$SOLCJS_INPUT_DIR/determinism.js" test/
 
     printLog "Copying contracts..."
-    cp -Rf $SOLCJS_INPUT_DIR/DAO test/
+    cp -Rf "$SOLCJS_INPUT_DIR/DAO" test/
 
     printLog "Copying SMTChecker tests..."
     cp -Rf "$TEST_DIR"/test/libsolidity/smtCheckerTests test/
@@ -52,7 +52,7 @@ function solcjs_test
 
     # Update version (needed for some tests)
     echo "Updating package.json to version $VERSION"
-    npm version --allow-same-version --no-git-tag-version $VERSION
+    npm version --allow-same-version --no-git-tag-version "$VERSION"
 
     run_test compile_fn test_fn
 }

test/externalTests/zeppelin.sh

@@ -33,10 +33,10 @@ function zeppelin_test
     OPTIMIZER_LEVEL=1
     CONFIG="truffle-config.js"
 
-    truffle_setup https://github.com/solidity-external-tests/openzeppelin-contracts.git upgrade-0.8.0
+    truffle_setup "$SOLJSON" https://github.com/solidity-external-tests/openzeppelin-contracts.git upgrade-0.8.0
-    run_install install_fn
+    run_install "$SOLJSON" install_fn
 
-    truffle_run_test compile_fn test_fn
+    truffle_run_test "$SOLJSON" compile_fn test_fn "NO-FORCE-ABI-V2"
 }
 
 external_test Zeppelin zeppelin_test

test/libsolidity/constructor_inheritance_init_order_3.sol

@@ -0,0 +1,12 @@
+contract A {
+    uint public x;
+    constructor(uint) {}
+    function f() public { x = 4; }
+}
+contract B is A {
+    constructor() A(f()) {}
+}
+// ====
+// compileViaYul: also
+// ----
+// x() -> 4

test/libsolidity/semanticTests/reverts/revert_return_area.sol

@@ -0,0 +1,20 @@
+contract C {
+    fallback() external {
+        revert("abc");
+    }
+
+    function f() public returns (uint s, uint r) {
+        address x = address(this);
+        assembly {
+            mstore(0, 7)
+            s := call(sub(0, 1), x, 0, 0, 0, 0, 32)
+            r := mload(0)
+        }
+    }
+}
+
+// ====
+// compileViaYul: also
+// EVMVersion: >=byzantium
+// ----
+// f() -> 0x00, 0x08c379a000000000000000000000000000000000000000000000000000000000

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol

@@ -19,6 +19,6 @@ contract A is B {
 	}
 }
 // ----
-// Warning 4984: (203-208): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (232-250): CHC: Assertion violation happens here.
+// Warning 4984: (203-208): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol

@@ -18,6 +18,6 @@ contract A is B {
 	}
 }
 // ----
+// Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (207-212): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol

@@ -28,6 +28,6 @@ contract A is B2, B1 {
 }
 // ----
 // Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (334-350): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol

@@ -19,8 +19,8 @@ contract C {
 	function f() public view {
 		uint y = this.m(0,1,2,3);
 		assert(y == m[0][1][2][3]); // should hold
-		assert(y == 1); // should fail
+		// Disabled because of Spacer seg fault
+		//assert(y == 1); // should fail
 	}
 }
 // ----
-// Warning 6328: (401-415): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol

@@ -14,8 +14,8 @@ contract C {
 	function f() public view {
 		uint y = this.m(0,1,2,3);
 		assert(y == m[0][1][2][3]); // should hold
-		assert(y == 1); // should fail
+		// Disabled because Spacer seg faults
+		//assert(y == 1); // should fail
 	}
 }
 // ----
-// Warning 6328: (349-363): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol

@@ -0,0 +1,36 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x;
+	constructor(uint a) { x = a; }
+}
+
+contract B is A {
+	constructor(uint b) A(b) {
+	}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+
+	function g() internal returns (uint) {
+		x = 42;
+		return x;
+	}
+}
+
+contract Z is B {
+	constructor(uint z) B(z + f()) {
+	}
+}
+
+contract C is Z(5) {
+	constructor() {
+		assert(x == 6);
+		assert(x > 9); // should fail
+	}
+}
+// ----
+// Warning 4984: (325-332): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (400-413): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol

@@ -0,0 +1,38 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x;
+	constructor(uint a) { x = a; }
+}
+
+contract B is A(9) {
+	constructor(uint b) {
+		x += b;
+	}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+
+	function g() internal returns (uint) {
+		x = 42;
+		return x;
+	}
+}
+
+contract Z is B {
+	constructor(uint z) B(z + f()) {
+	}
+}
+
+contract C is Z(5) {
+	constructor() {
+		assert(x == 15);
+		assert(x > 90); // should fail
+	}
+}
+// ----
+// Warning 4984: (143-149): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (333-340): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (409-423): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_1.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x;
+	constructor(uint a) { x = a; }
+}
+
+contract B is A {
+	constructor(uint b) A(b + f()) {
+	}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+}
+
+abstract contract Z is A {
+	uint k;
+	constructor(uint z) {
+		k = z;
+	}
+}
+
+contract C is Z, B {
+	constructor() B(x) Z(x) {
+		assert(x == 1);
+		assert(k == 0);
+		assert(x == k); // should fail
+	}
+}
+// ----
+// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (384-398): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_2.sol

@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x;
+	constructor(uint a) { x = a; }
+}
+
+contract B is A {
+	constructor(uint b) A(b) {
+	}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+}
+
+abstract contract Z is A {
+	uint k;
+	constructor(uint z) {
+		k = z;
+	}
+}
+
+contract C is Z, B {
+	constructor() B(f()) Z(f()) {
+		assert(x == 1);
+		assert(k == 2);
+		assert(x == k); // should fail
+	}
+}
+// ----
+// Warning 6328: (382-396): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_3.sol

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x;
+	constructor(uint a) { x = a; }
+}
+
+contract B is A {
+	constructor(uint b) A(b + f()) {
+	}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+}
+
+abstract contract Z is A {
+	uint k;
+	constructor(uint z) {
+		k = z;
+	}
+}
+
+contract C is Z, B {
+	constructor(uint c) B(c) Z(x) {
+		assert(x == c + 1);
+		assert(k == 0);
+		assert(x == k); // should fail
+	}
+}
+// ----
+// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (366-371): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (394-408): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_4.sol

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x;
+	constructor(uint a) { x = a; }
+}
+
+contract B is A {
+	constructor(uint b) A(b + f()) {
+	}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+}
+
+abstract contract Z is A {
+	uint k;
+	constructor(uint z) {
+		k = z;
+	}
+}
+
+contract C is Z, B {
+	constructor(uint c) Z(x) B(c) {
+		assert(x == c + 1);
+		assert(k == 0);
+		assert(x == k); // should fail
+	}
+}
+// ----
+// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (366-371): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (394-408): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol

@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x;
+	constructor(uint a) { x = a; }
+}
+
+contract B is A {
+	constructor(uint b) A(b + f()) {
+	}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+
+	function g() internal returns (uint) {
+		x = 42;
+		return x;
+	}
+}
+
+abstract contract Z is A {
+	uint k;
+	constructor(uint z) {
+		k = z;
+	}
+}
+
+contract C is Z, B {
+	constructor() Z(g()) B(f()) {
+		assert(x == 44);
+		assert(k == 42);
+		assert(x == k); // should fail
+	}
+}
+// ----
+// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (456-470): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_6.sol

@@ -0,0 +1,38 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x;
+	constructor(uint a) { x = a; }
+}
+
+contract B is A {
+	constructor(uint b) A(b) {
+	}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+
+	function g() internal returns (uint) {
+		x = 42;
+		return x;
+	}
+}
+
+abstract contract Z is A {
+	uint k;
+	constructor(uint z) {
+		k = z;
+	}
+}
+
+contract C is Z, B {
+	constructor() Z(g()) B(f()) {
+		assert(x == 1);
+		assert(k == 42);
+		assert(x == k); // should fail
+	}
+}
+// ----
+// Warning 6328: (449-463): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_7.sol

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x;
+	constructor(uint a) { x = a; }
+}
+
+contract B is A {
+	constructor(uint b) A(b) {
+	}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+
+	function g() internal returns (uint) {
+		x = 42;
+		return x;
+	}
+}
+
+contract Z is B {
+	constructor() B(f()) {
+	}
+}
+
+contract C is Z {
+	constructor() {
+		assert(x == 1);
+		assert(x > 2); // should fail
+	}
+}
+// ----
+// Warning 6328: (387-400): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_8.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x;
+	constructor(uint) {}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+}
+
+contract C is A {
+	constructor() A(f()) {
+		assert(x == 1);
+		assert(x == 0); // should fail
+		assert(x > 2000); // should fail
+	}
+}
+// ----
+// Warning 6328: (218-232): CHC: Assertion violation happens here.
+// Warning 6328: (251-267): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_9.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint public x = 42;
+	constructor(uint) {}
+
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+}
+
+contract C is A {
+	constructor() A(f()) {
+		assert(x == 42);
+		assert(x == 0); // should fail
+		assert(x == 1); // should fail
+		assert(x > 2000); // should fail
+	}
+}
+// ----
+// Warning 6328: (224-238): CHC: Assertion violation happens here.
+// Warning 6328: (257-271): CHC: Assertion violation happens here.
+// Warning 6328: (290-306): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_asserts.sol

@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract A {
+	int x;
+	constructor (int a) { x = a;}
+}
+
+contract B is A {
+	int y;
+	constructor(int a) A(-a) {
+		if (a > 0) {
+			y = 2;
+		}
+		else {
+			y = 4;
+		}
+	}
+}
+
+contract C is B {
+	constructor(int a) B(a) {
+		assert(y != 3); // should hold
+		assert(y == 4); // should fail
+		if (a > 0) {
+			assert(x < 0 && y == 2); // should hold
+			assert(x < 0 && y == 4); // should fail
+		}
+		else {
+			assert(x >= 0 && y == 4); // should hold
+			assert(x >= 0 && y == 2); // should fail
+			assert(x > 0); // should fail
+		}
+	}
+}
+// ----
+// Warning 6328: (280-294): CHC: Assertion violation happens here.
+// Warning 6328: (372-395): CHC: Assertion violation happens here.
+// Warning 6328: (472-496): CHC: Assertion violation happens here.
+// Warning 6328: (516-529): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol

@@ -23,9 +23,9 @@ contract A is B {
 
 // ----
 // Warning 4984: (157-162): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (216-221): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (239-244): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (261-266): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (261-270): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (287-292): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (275-293): CHC: Assertion violation happens here.
+// Warning 4984: (216-221): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol

@@ -23,8 +23,8 @@ contract A is B {
 
 // ----
 // Warning 4984: (157-163): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4984: (217-222): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (240-245): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (262-268): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (285-290): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (273-291): CHC: Assertion violation happens here.
+// Warning 4984: (217-222): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_tree.sol

@@ -0,0 +1,43 @@
+pragma experimental SMTChecker;
+
+contract A {
+	int x;
+	constructor (int a) { x = a; }
+}
+
+contract Z {
+	int z;
+	constructor(int _z) {
+		z = _z;
+	}
+}
+
+contract B is A, Z {
+	constructor(int b) A(b) Z(x) {
+		assert(x == b);
+		assert(z == 0);
+	}
+}
+
+contract F is Z, A {
+	constructor(int b) Z(x) A(b) {
+		assert(x == b);
+		assert(z == 0);
+	}
+}
+
+contract C is B {
+	constructor(int c) B(-c) {
+		if (x > 0) {
+			assert(c < 0); // should hold
+			assert(c >= 0); // should fail
+		}
+		else {
+			assert(c < 0); // should fail
+			assert(c >= 0); // should hold
+		}
+	}
+}
+// ----
+// Warning 6328: (436-450): CHC: Assertion violation happens here.
+// Warning 6328: (483-496): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol

@@ -5,11 +5,17 @@ contract A {
 }
 
 contract B is A {
-	constructor() { x = 2; }
+	constructor() {
+		assert(x == 1);
+		x = 2;
+	}
 }
 
 contract C is A {
-	constructor() { x = 3; }
+	constructor() {
+		assert(x == 1);
+		x = 3;
+	}
 }
 
 contract D is B, C {
@@ -19,4 +25,5 @@ contract D is B, C {
 	}
 }
 // ----
-// Warning 6328: (214-228): CHC: Assertion violation happens here.
+// Warning 6328: (167-181): CHC: Assertion violation happens here.
+// Warning 6328: (256-270): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	constructor() {
+		x = 42;
+	}
+	function f() public view returns(uint256) {
+		return x;
+	}
+}
+contract B is A {
+	uint y = f();
+}
+contract C is B {
+	function g() public view {
+		assert(y == 42);
+	}
+}

test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol

@@ -15,10 +15,10 @@ contract C
 		// Erasing knowledge about memory references should not
 		// erase knowledge about storage references.
 		assert(c[0] == 42);
-		assert(a[0] == 2);
+		// Removed because current Spacer seg faults in cex generation.
+		//assert(a[0] == 2);
 		// Removed because current Spacer seg faults in cex generation.
 		//assert(b[0] == 1);
 	}
 }
 // ----
-// Warning 6328: (476-493): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol

@@ -21,7 +21,8 @@ contract C {
 		// Removed because current Spacer seg faults in cex generation.
 		//assert(s1.t.y == s2.t.y);
 		s1.a[2] = 4;
-		assert(s1.a[2] == s2.a[2]);
+		// Removed because current Spacer seg faults in cex generation.
+		//assert(s1.a[2] == s2.a[2]);
 		s1.ts[3].y = 5;
 		// Removed because current Spacer seg faults in cex generation.
 		//assert(s1.ts[3].y == s2.ts[3].y);
@@ -30,5 +31,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (456-482): CHC: Assertion violation happens here.
+// Warning 6328: (697-735): CHC: Assertion violation happens here.
-// Warning 6328: (629-667): CHC: Assertion violation happens here.

test/libyul/EwasmTranslationTest.cpp

@@ -102,6 +102,7 @@ string EwasmTranslationTest::interpret()
 	InterpreterState state;
 	state.maxTraceSize = 10000;
 	state.maxSteps = 1000000;
+	state.maxExprNesting = 64;
 	try
 	{
 		Interpreter::run(state, WasmDialect{}, *m_object->code);

test/libyul/YulInterpreterTest.cpp

@@ -89,6 +89,7 @@ string YulInterpreterTest::interpret()
 	InterpreterState state;
 	state.maxTraceSize = 32;
 	state.maxSteps = 512;
+	state.maxExprNesting = 64;
 	try
 	{
 		Interpreter::run(state, EVMDialect::strictAssemblyForEVMObjects(langutil::EVMVersion{}), *m_ast);

test/libyul/yulInterpreterTests/expr_nesting_depth_exceeded.yul

@@ -0,0 +1,14 @@
+{
+  function f(x) -> y
+  {
+    // 32 nested additions are computed in
+    // exactly 66 expression evaluation steps
+    y := add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,x))))))))))))))))))))))))))))))))
+  }
+  mstore(0,f(0))
+}
+// ----
+// Trace:
+//   Maximum expression nesting level reached.
+// Memory dump:
+// Storage dump:

test/libyul/yulInterpreterTests/expr_nesting_depth_not_exceeded.yul

@@ -0,0 +1,14 @@
+{
+  function f(x) -> y
+  {
+    // 31 nested additions are computed in
+    // exactly 64 expression evaluation steps
+    y := add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,add(0x1,x)))))))))))))))))))))))))))))))
+  }
+  mstore(0,f(0))
+}
+// ----
+// Trace:
+// Memory dump:
+//      0: 000000000000000000000000000000000000000000000000000000000000001f
+// Storage dump:

test/tools/ossfuzz/abiV2FuzzerCommon.cpp

@@ -40,3 +40,46 @@ solidity::bytes SolidityCompilationFramework::compileContract(
 	);
 	return obj.bytecode;
 }
+
+bool AbiV2Utility::isOutputExpected(
+	uint8_t const* _result,
+	size_t _length,
+	std::vector<uint8_t> const& _expectedOutput
+)
+{
+	if (_length != _expectedOutput.size())
+		return false;
+
+	return (memcmp(_result, _expectedOutput.data(), _length) == 0);
+}
+
+evmc_message AbiV2Utility::initializeMessage(bytes const& _input)
+{
+	// Zero initialize all message fields
+	evmc_message msg = {};
+	// Gas available (value of type int64_t) is set to its maximum
+	// value.
+	msg.gas = std::numeric_limits<int64_t>::max();
+	msg.input_data = _input.data();
+	msg.input_size = _input.size();
+	return msg;
+}
+
+evmc::result AbiV2Utility::executeContract(
+	EVMHost& _hostContext,
+	bytes const& _functionHash,
+	evmc_address _deployedAddress
+)
+{
+	evmc_message message = initializeMessage(_functionHash);
+	message.destination = _deployedAddress;
+	message.kind = EVMC_CALL;
+	return _hostContext.call(message);
+}
+
+evmc::result AbiV2Utility::deployContract(EVMHost& _hostContext, bytes const& _code)
+{
+	evmc_message message = initializeMessage(_code);
+	message.kind = EVMC_CREATE;
+	return _hostContext.call(message);
+}

test/tools/ossfuzz/abiV2FuzzerCommon.h

@@ -1,14 +1,17 @@
 #pragma once
 
+#include <test/EVMHost.h>
+
 #include <libsolidity/interface/CompilerStack.h>
 
 #include <libyul/AssemblyStack.h>
 
 #include <libsolutil/Keccak256.h>
 
+#include <evmone/evmone.h>
+
 namespace solidity::test::abiv2fuzzer
 {
-
 class SolidityCompilationFramework
 {
 public:
@@ -29,4 +32,36 @@ protected:
 	langutil::EVMVersion m_evmVersion;
 };
 
+struct AbiV2Utility
+{
+	/// Compares the contents of the memory address pointed to
+	/// by `_result` of `_length` bytes to the expected output.
+	/// Returns true if `_result` matches expected output, false
+	/// otherwise.
+	static bool isOutputExpected(
+		uint8_t const* _result,
+		size_t _length,
+		std::vector<uint8_t> const& _expectedOutput
+	);
+	/// Accepts a reference to a user-specified input and returns an
+	/// evmc_message with all of its fields zero initialized except
+	/// gas and input fields.
+	/// The gas field is set to the maximum permissible value so that we
+	/// don't run into out of gas errors. The input field is copied from
+	/// user input.
+	static evmc_message initializeMessage(bytes const& _input);
+	/// Accepts host context implementation, and keccak256 hash of the function
+	/// to be called at a specified address in the simulated blockchain as
+	/// input and returns the result of the execution of the called function.
+	static evmc::result executeContract(
+		EVMHost& _hostContext,
+		bytes const& _functionHash,
+		evmc_address _deployedAddress
+	);
+	/// Accepts a reference to host context implementation and byte code
+	/// as input and deploys it on the simulated blockchain. Returns the
+	/// result of deployment.
+	static evmc::result deployContract(EVMHost& _hostContext, bytes const& _code);
+};
+
 }

test/tools/ossfuzz/abiV2ProtoFuzzer.cpp

@@ -16,89 +16,26 @@
 */
 // SPDX-License-Identifier: GPL-3.0
 
-#include <test/EVMHost.h>
 #include <test/tools/ossfuzz/abiV2FuzzerCommon.h>
 #include <test/tools/ossfuzz/protoToAbiV2.h>
 
-#include <evmone/evmone.h>
 #include <src/libfuzzer/libfuzzer_macro.h>
 
 #include <fstream>
 
-static evmc::VM evmone = evmc::VM{evmc_create_evmone()};
-
 using namespace solidity::test::abiv2fuzzer;
 using namespace solidity::test;
 using namespace solidity::util;
 using namespace solidity;
 using namespace std;
 
-namespace
+static evmc::VM evmone = evmc::VM{evmc_create_evmone()};
-{
-/// Test function returns a uint256 value
-static size_t const expectedOutputLength = 32;
 /// Expected output value is decimal 0
-static uint8_t const expectedOutput[expectedOutputLength] = {
+static vector<uint8_t> const expectedOutput = {
 	0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
 	0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
 };
 
-/// Compares the contents of the memory address pointed to
-/// by `_result` of `_length` bytes to the expected output.
-/// Returns true if `_result` matches expected output, false
-/// otherwise.
-bool isOutputExpected(uint8_t const* _result, size_t _length)
-{
-	if (_length != expectedOutputLength)
-		return false;
-
-	return (memcmp(_result, expectedOutput, expectedOutputLength) == 0);
-}
-
-/// Accepts a reference to a user-specified input and returns an
-/// evmc_message with all of its fields zero initialized except
-/// gas and input fields.
-/// The gas field is set to the maximum permissible value so that we
-/// don't run into out of gas errors. The input field is copied from
-/// user input.
-evmc_message initializeMessage(bytes const& _input)
-{
-	// Zero initialize all message fields
-	evmc_message msg = {};
-	// Gas available (value of type int64_t) is set to its maximum
-	// value.
-	msg.gas = std::numeric_limits<int64_t>::max();
-	msg.input_data = _input.data();
-	msg.input_size = _input.size();
-	return msg;
-}
-
-/// Accepts host context implementation, and keccak256 hash of the function
-/// to be called at a specified address in the simulated blockchain as
-/// input and returns the result of the execution of the called function.
-evmc::result executeContract(
-	EVMHost& _hostContext,
-	bytes const& _functionHash,
-	evmc_address _deployedAddress
-)
-{
-	evmc_message message = initializeMessage(_functionHash);
-	message.destination = _deployedAddress;
-	message.kind = EVMC_CALL;
-	return _hostContext.call(message);
-}
-
-/// Accepts a reference to host context implementation and byte code
-/// as input and deploys it on the simulated blockchain. Returns the
-/// result of deployment.
-evmc::result deployContract(EVMHost& _hostContext, bytes const& _code)
-{
-	evmc_message message = initializeMessage(_code);
-	message.kind = EVMC_CREATE;
-	return _hostContext.call(message);
-}
-}
-
 DEFINE_PROTO_FUZZER(Contract const& _input)
 {
 	string contract_source = ProtoConverter{}.contractToString(_input);
@@ -147,7 +84,7 @@ DEFINE_PROTO_FUZZER(Contract const& _input)
 	EVMHost hostContext(version, evmone);
 
 	// Deploy contract and signal failure if deploy failed
-	evmc::result createResult = deployContract(hostContext, byteCode);
+	evmc::result createResult = AbiV2Utility::deployContract(hostContext, byteCode);
 	solAssert(
 		createResult.status_code == EVMC_SUCCESS,
 		"Proto ABIv2 Fuzzer: Contract creation failed"
@@ -155,7 +92,7 @@ DEFINE_PROTO_FUZZER(Contract const& _input)
 
 	// Execute test function and signal failure if EVM reverted or
 	// did not return expected output on successful execution.
-	evmc::result callResult = executeContract(
+	evmc::result callResult = AbiV2Utility::executeContract(
 		hostContext,
 		fromHex(hexEncodedInput),
 		createResult.create_address
@@ -165,7 +102,7 @@ DEFINE_PROTO_FUZZER(Contract const& _input)
 	solAssert(callResult.status_code != EVMC_REVERT, "Proto ABIv2 fuzzer: EVM One reverted");
 	if (callResult.status_code == EVMC_SUCCESS)
 		solAssert(
-			isOutputExpected(callResult.output_data, callResult.output_size),
+			AbiV2Utility::isOutputExpected(callResult.output_data, callResult.output_size, expectedOutput),
 			"Proto ABIv2 fuzzer: ABIv2 coding failure found"
 		);
 }

test/tools/ossfuzz/yulFuzzerCommon.cpp

@@ -27,12 +27,14 @@ yulFuzzerUtil::TerminationReason yulFuzzerUtil::interpret(
 	shared_ptr<yul::Block> _ast,
 	Dialect const& _dialect,
 	size_t _maxSteps,
-	size_t _maxTraceSize
+	size_t _maxTraceSize,
+	size_t _maxExprNesting
 )
 {
 	InterpreterState state;
 	state.maxTraceSize = _maxTraceSize;
 	state.maxSteps = _maxSteps;
+	state.maxExprNesting = _maxExprNesting;
 	// Add 64 bytes of pseudo-randomly generated calldata so that
 	// calldata opcodes perform non trivial work.
 	state.calldata = {
@@ -59,6 +61,10 @@ yulFuzzerUtil::TerminationReason yulFuzzerUtil::interpret(
 	{
 		reason = TerminationReason::TraceLimitReached;
 	}
+	catch (ExpressionNestingLimitReached const&)
+	{
+		reason = TerminationReason::ExpresionNestingLimitReached;
+	}
 	catch (ExplicitlyTerminated const&)
 	{
 		reason = TerminationReason::ExplicitlyTerminated;

test/tools/ossfuzz/yulFuzzerCommon.h

@@ -28,6 +28,7 @@ struct yulFuzzerUtil
 		ExplicitlyTerminated,
 		StepLimitReached,
 		TraceLimitReached,
+		ExpresionNestingLimitReached,
 		None
 	};
 
@@ -36,10 +37,12 @@ struct yulFuzzerUtil
 		std::shared_ptr<yul::Block> _ast,
 		Dialect const& _dialect,
 		size_t _maxSteps = maxSteps,
-		size_t _maxTraceSize = maxTraceSize
+		size_t _maxTraceSize = maxTraceSize,
+		size_t _maxExprNesting = maxExprNesting
 	);
 	static size_t constexpr maxSteps = 100;
 	static size_t constexpr maxTraceSize = 75;
+	static size_t constexpr maxExprNesting = 64;
 };
 
 }

test/tools/ossfuzz/yulProto_diff_ossfuzz.cpp

@@ -99,7 +99,8 @@ DEFINE_PROTO_FUZZER(Program const& _input)
 
 	if (
 		termReason == yulFuzzerUtil::TerminationReason::StepLimitReached ||
-		termReason == yulFuzzerUtil::TerminationReason::TraceLimitReached
+		termReason == yulFuzzerUtil::TerminationReason::TraceLimitReached ||
+		termReason == yulFuzzerUtil::TerminationReason::ExpresionNestingLimitReached
 	)
 		return;
 
@@ -109,10 +110,10 @@ DEFINE_PROTO_FUZZER(Program const& _input)
 		stack.parserResult()->code,
 		EVMDialect::strictAssemblyForEVMObjects(version)
 	);
-
 	if (
 		termReason == yulFuzzerUtil::TerminationReason::StepLimitReached ||
-		termReason == yulFuzzerUtil::TerminationReason::TraceLimitReached
+		termReason == yulFuzzerUtil::TerminationReason::TraceLimitReached ||
+		termReason == yulFuzzerUtil::TerminationReason::ExpresionNestingLimitReached
 	)
 		return;
 

test/tools/yulInterpreter/Interpreter.cpp

@@ -247,6 +247,7 @@ void Interpreter::incrementStep()
 
 void ExpressionEvaluator::operator()(Literal const& _literal)
 {
+	incrementStep();
 	static YulString const trueString("true");
 	static YulString const falseString("false");
 
@@ -256,6 +257,7 @@ void ExpressionEvaluator::operator()(Literal const& _literal)
 void ExpressionEvaluator::operator()(Identifier const& _identifier)
 {
 	solAssert(m_variables.count(_identifier.name), "");
+	incrementStep();
 	setValue(m_variables.at(_identifier.name));
 }
 
@@ -326,6 +328,7 @@ void ExpressionEvaluator::evaluateArgs(
 	vector<optional<LiteralKind>> const* _literalArguments
 )
 {
+	incrementStep();
 	vector<u256> values;
 	size_t i = 0;
 	/// Function arguments are evaluated in reverse.
@@ -341,3 +344,13 @@ void ExpressionEvaluator::evaluateArgs(
 	m_values = std::move(values);
 	std::reverse(m_values.begin(), m_values.end());
 }
+
+void ExpressionEvaluator::incrementStep()
+{
+	m_nestingLevel++;
+	if (m_state.maxExprNesting > 0 && m_nestingLevel > m_state.maxExprNesting)
+	{
+		m_state.trace.emplace_back("Maximum expression nesting level reached.");
+		throw ExpressionNestingLimitReached();
+	}
+}

test/tools/yulInterpreter/Interpreter.h

@@ -55,6 +55,10 @@ class TraceLimitReached: public InterpreterTerminatedGeneric
 {
 };
 
+class ExpressionNestingLimitReached: public InterpreterTerminatedGeneric
+{
+};
+
 enum class ControlFlowState
 {
 	Default,
@@ -92,6 +96,7 @@ struct InterpreterState
 	size_t maxTraceSize = 0;
 	size_t maxSteps = 0;
 	size_t numSteps = 0;
+	size_t maxExprNesting = 0;
 	ControlFlowState controlFlowState = ControlFlowState::Default;
 
 	void dumpTraceAndState(std::ostream& _out) const;
@@ -202,6 +207,11 @@ private:
 		std::vector<std::optional<LiteralKind>> const* _literalArguments
 	);
 
+	/// Increment evaluation count, throwing exception if the
+	/// nesting level is beyond the upper bound configured in
+	/// the interpreter state.
+	void incrementStep();
+
 	InterpreterState& m_state;
 	Dialect const& m_dialect;
 	/// Values of variables.
@@ -209,6 +219,8 @@ private:
 	Scope& m_scope;
 	/// Current value of the expression
 	std::vector<u256> m_values;
+	/// Current expression nesting level
+	unsigned m_nestingLevel = 0;
 };
 
 }