Merge pull request #7442 from ethereum/develop

Merge develop into develop_060

.clang-format

@@ -25,6 +25,7 @@ PenaltyBreakBeforeFirstCallParameter: 2000
 SpaceAfterCStyleCast: true
 SpaceBeforeParens: ControlStatements
 TabWidth: 4
+UseTab: ForIndentation
 
 # Local Variables:
 # mode: yaml

Changelog.md

@@ -34,11 +34,13 @@ Language Features:
 Compiler Features:
  * ABI Output: Change sorting order of functions from selector to kind, name.
  * Optimizer: Add rule that replaces the BYTE opcode by 0 if the first argument is larger than 31.
+ * SMTChecker: Add loop support to the CHC engine.
  * Yul Optimizer: Take side-effect-freeness of user-defined functions into account.
  * Yul Optimizer: Remove redundant mload/sload operations.
 
 
 Bugfixes:
+ * Fix internal error when popping a dynamic storage array of mappings.
 
 
 ### 0.5.11 (2019-08-12)

docs/types/value-types.rst

@@ -110,7 +110,7 @@ Modulo
 
 The modulo operation ``a % n`` yields the remainder ``r`` after the division of the operand ``a``
 by the operand ``n``, where ``q = int(a / n)`` and ``r = a - (n * q)``. This means that modulo
-results in the same sign as its left operand (or zero) and ``a % n == -(abs(a) % n)`` holds for negative ``a``:
+results in the same sign as its left operand (or zero) and ``a % n == -(-a % n)`` holds for negative ``a``:
 
  * ``int256(5) % int256(2) == int256(1)``
  * ``int256(5) % int256(-2) == int256(1)``

libsolidity/codegen/ArrayUtils.cpp

@@ -896,11 +896,16 @@ void ArrayUtils::popStorageArrayElement(ArrayType const& _type) const
 		// Stack: ArrayReference oldLength
 		m_context << u256(1) << Instruction::SWAP1 << Instruction::SUB;
 		// Stack ArrayReference newLength
-		m_context << Instruction::DUP2 << Instruction::DUP2;
+
-		// Stack ArrayReference newLength ArrayReference newLength;
+		if (_type.baseType()->category() != Type::Category::Mapping)
-		accessIndex(_type, false);
+		{
-		// Stack: ArrayReference newLength storage_slot byte_offset
+			m_context << Instruction::DUP2 << Instruction::DUP2;
-		StorageItem(m_context, *_type.baseType()).setToZero(SourceLocation(), true);
+			// Stack ArrayReference newLength ArrayReference newLength;
+			accessIndex(_type, false);
+			// Stack: ArrayReference newLength storage_slot byte_offset
+			StorageItem(m_context, *_type.baseType()).setToZero(SourceLocation(), true);
+		}
+
 		// Stack: ArrayReference newLength
 		m_context << Instruction::SWAP1 << Instruction::SSTORE;
 	}

libsolidity/formal/CHC.cpp

@@ -74,8 +74,10 @@ bool CHC::visit(ContractDefinition const& _contract)
 		else
 			m_stateSorts.push_back(smt::smtSort(*var->type()));
 
+	clearIndices();
+
 	string interfaceName = "interface_" + _contract.name() + "_" + to_string(_contract.id());
-	m_interfacePredicate = createBlock(interfaceSort(),	interfaceName);
+	m_interfacePredicate = createSymbolicBlock(interfaceSort(), interfaceName);
 
 	// TODO create static instances for Bool/Int sorts in SolverInterface.
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
@@ -83,7 +85,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 		vector<smt::SortPointer>(),
 		boolSort
 	);
-	m_errorPredicate = createBlock(errorFunctionSort, "error");
+	m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error");
 
 	// If the contract has a constructor it is handled as a function.
 	// Otherwise we zero-initialize all state vars.
@@ -91,7 +93,9 @@ bool CHC::visit(ContractDefinition const& _contract)
 	if (!_contract.constructor())
 	{
 		string constructorName = "constructor_" + _contract.name() + "_" + to_string(_contract.id());
-		m_constructorPredicate = createBlock(constructorSort(), constructorName);
+		m_constructorPredicate = createSymbolicBlock(constructorSort(), constructorName);
+		smt::Expression constructorPred = (*m_constructorPredicate)({});
+		addRule(constructorPred, constructorName);
 
 		for (auto const& var: m_stateVariables)
 		{
@@ -101,14 +105,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 			m_context.setZeroValue(*symbVar);
 		}
 
-		smt::Expression constructorAppl = (*m_constructorPredicate)({});
+		connectBlocks(constructorPred, interface());
-		m_interface->addRule(constructorAppl, constructorName);
-
-		smt::Expression constructorInterface = smt::Expression::implies(
-			constructorAppl && m_context.assertions(),
-			interface()
-		);
-		m_interface->addRule(constructorInterface, constructorName + "_to_" + interfaceName);
 	}
 
 	return true;
@@ -119,10 +116,13 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	if (!shouldVisit(_contract))
 		return;
 
-	auto errorAppl = (*m_errorPredicate)({});
+	for (unsigned i = 0; i < m_verificationTargets.size(); ++i)
-	for (auto const& target: m_verificationTargets)
+	{
+		auto const& target = m_verificationTargets.at(i);
+		auto errorAppl = error(i + 1);
 		if (query(errorAppl, target->location()))
 			m_safeAssertions.insert(target);
+	}
 
 	SMTEncoder::endVisit(_contract);
 }
@@ -139,39 +139,25 @@ bool CHC::visit(FunctionDefinition const& _function)
 
 	// Store the constraints related to variable initialization.
 	smt::Expression const& initAssertions = m_context.assertions();
-
+	m_context.pushSolver();
-	createFunctionBlock(*m_currentFunction);
-
-	// Rule Interface -> FunctionEntry, uses no constraints.
-	smt::Expression interfaceFunction = smt::Expression::implies(
-		interface(),
-		predicateCurrent(m_currentFunction)
-	);
-	m_interface->addRule(
-		interfaceFunction,
-		m_interfacePredicate->currentName() + "_to_" + m_predicates.at(m_currentFunction)->currentName()
-	);
-
-	pushBlock(predicateCurrent(m_currentFunction));
-
-	createFunctionBlock(m_currentFunction->body());
-
-	// Rule FunctionEntry -> FunctionBody, also no constraints.
-	smt::Expression functionBody = smt::Expression::implies(
-		predicateEntry(m_currentFunction),
-		predicateBodyCurrent(&m_currentFunction->body())
-	);
-	m_interface->addRule(
-		functionBody,
-		m_predicates.at(m_currentFunction)->currentName() + "_to_" + m_predicates.at(&m_currentFunction->body())->currentName()
-	);
-
-	pushBlock(predicateBodyCurrent(&m_currentFunction->body()));
-	// We need to re-add the constraints that were created for initialization of variables.
-	m_context.addAssertion(initAssertions);
 
 	solAssert(m_functionBlocks == 0, "");
-	m_functionBlocks = 2;
+
+	createBlock(m_currentFunction);
+	createBlock(&m_currentFunction->body(), "block_");
+
+	auto functionPred = predicate(m_currentFunction);
+	auto bodyPred = predicate(&m_currentFunction->body());
+
+	connectBlocks(interface(), functionPred);
+	connectBlocks(functionPred, bodyPred);
+
+	m_context.popSolver();
+
+	pushBlock(&m_currentFunction->body());
+
+	// We need to re-add the constraints that were created for initialization of variables.
+	m_context.addAssertion(initAssertions);
 
 	SMTEncoder::visit(*m_currentFunction);
 
@@ -185,35 +171,22 @@ void CHC::endVisit(FunctionDefinition const& _function)
 
 	solAssert(m_currentFunction == &_function, "Inlining internal function calls not yet implemented");
 
-	// Create Function Exit block.
+	// Function Exit block.
-	createFunctionBlock(*m_currentFunction);
+	createBlock(m_currentFunction);
-
+	connectBlocks(m_path.back(), predicate(&_function));
-	// Rule FunctionBody -> FunctionExit.
-	smt::Expression bodyFunction = smt::Expression::implies(
-		predicateEntry(&_function.body()) && m_context.assertions(),
-		predicateCurrent(&_function)
-	);
-	m_interface->addRule(
-		bodyFunction,
-		m_predicates.at(&_function.body())->currentName() + "_to_" + m_predicates.at(&_function.body())->currentName()
-	);
 
 	// Rule FunctionExit -> Interface, uses no constraints.
-	smt::Expression functionInterface = smt::Expression::implies(
+	clearIndices();
-		predicateCurrent(&_function),
+	m_context.pushSolver();
-		interface()
+	connectBlocks(predicate(&_function), interface());
-	);
+	m_context.popSolver();
-	m_interface->addRule(
-		functionInterface,
-		m_predicates.at(&_function)->currentName() + "_to_" + m_interfacePredicate->currentName()
-	);
 
 	m_currentFunction = nullptr;
 	solAssert(m_path.size() == m_functionBlocks, "");
-	for (unsigned i = 0; i < m_path.size(); ++i)
+	while (m_functionBlocks > 0)
-		m_context.popSolver();
+		popBlock();
-	m_functionBlocks = 0;
+
-	m_path.clear();
+	solAssert(m_path.empty(), "");
 
 	SMTEncoder::endVisit(_function);
 }
@@ -237,15 +210,51 @@ bool CHC::visit(IfStatement const& _if)
 
 bool CHC::visit(WhileStatement const& _while)
 {
-	eraseKnowledge();
+	bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
-	m_context.resetVariables(touchedVariables(_while));
+	m_unknownFunctionCallSeen = false;
+
+	solAssert(m_currentFunction, "");
+
+	if (_while.isDoWhile())
+		_while.body().accept(*this);
+
+	visitLoop(
+		_while,
+		&_while.condition(),
+		_while.body(),
+		nullptr
+	);
+
+	if (m_unknownFunctionCallSeen)
+		eraseKnowledge();
+
+	m_unknownFunctionCallSeen = unknownFunctionCallWasSeen;
+
 	return false;
 }
 
 bool CHC::visit(ForStatement const& _for)
 {
-	eraseKnowledge();
+	bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
-	m_context.resetVariables(touchedVariables(_for));
+	m_unknownFunctionCallSeen = false;
+
+	solAssert(m_currentFunction, "");
+
+	if (auto init = _for.initializationExpression())
+		init->accept(*this);
+
+	visitLoop(
+		_for,
+		_for.condition(),
+		_for.body(),
+		_for.loopExpression()
+	);
+
+	if (m_unknownFunctionCallSeen)
+		eraseKnowledge();
+
+	m_unknownFunctionCallSeen = unknownFunctionCallWasSeen;
+
 	return false;
 }
 
@@ -292,6 +301,18 @@ void CHC::endVisit(FunctionCall const& _funCall)
 	createReturnedExpressions(_funCall);
 }
 
+void CHC::endVisit(Break const&)
+{
+	solAssert(m_breakDest, "");
+	m_breakSeen = true;
+}
+
+void CHC::endVisit(Continue const&)
+{
+	solAssert(m_continueDest, "");
+	m_continueSeen = true;
+}
+
 void CHC::visitAssert(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();
@@ -300,13 +321,10 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 
 	solAssert(!m_path.empty(), "");
 
+	createErrorBlock();
+
 	smt::Expression assertNeg = !(m_context.expression(*args.front())->currentValue());
-	smt::Expression assertionError = smt::Expression::implies(
+	connectBlocks(m_path.back(), error(), currentPathConditions() && assertNeg);
-		m_path.back() && m_context.assertions() && currentPathConditions() && assertNeg,
-		error()
-	);
-	string predicateName = "assert_" + to_string(_funCall.id());
-	m_interface->addRule(assertionError, predicateName + "_to_error");
 
 	m_verificationTargets.push_back(&_funCall);
 }
@@ -323,6 +341,85 @@ void CHC::unknownFunctionCall(FunctionCall const&)
 	m_unknownFunctionCallSeen = true;
 }
 
+void CHC::visitLoop(
+	BreakableStatement const& _loop,
+	Expression const* _condition,
+	Statement const& _body,
+	ASTNode const* _postLoop
+)
+{
+	bool breakWasSeen = m_breakSeen;
+	bool continueWasSeen = m_continueSeen;
+	m_breakSeen = false;
+	m_continueSeen = false;
+
+	solAssert(m_currentFunction, "");
+	auto const& functionBody = m_currentFunction->body();
+
+	createBlock(&_loop, "loop_header_");
+	createBlock(&_body, "loop_body_");
+	createBlock(&functionBody, "block_");
+
+	connectBlocks(m_path.back(), predicate(&_loop));
+
+	// We need to save the next block here because new blocks
+	// might be created inside the loop body.
+	// This will be m_path.back() in the end of this function.
+	pushBlock(&functionBody);
+
+	smt::Expression loopHeader = predicate(&_loop);
+	pushBlock(&_loop);
+
+	if (_condition)
+		_condition->accept(*this);
+	auto condition = _condition ? expr(*_condition) : smt::Expression(true);
+
+	connectBlocks(loopHeader, predicate(&_body), condition);
+	connectBlocks(loopHeader, predicate(&functionBody), !condition);
+
+	// Loop body visit.
+	pushBlock(&_body);
+
+	m_breakDest = &functionBody;
+	m_continueDest = _postLoop ? _postLoop : &_loop;
+
+	auto functionBlocks = m_functionBlocks;
+	_body.accept(*this);
+	if (_postLoop)
+	{
+		createBlock(_postLoop, "loop_post_");
+		connectBlocks(m_path.back(), predicate(_postLoop));
+		pushBlock(_postLoop);
+		_postLoop->accept(*this);
+	}
+
+	// Back edge.
+	connectBlocks(m_path.back(), predicate(&_loop));
+
+	// Pop all function blocks created by nested inner loops
+	// to adjust the assertion context.
+	for (unsigned i = m_functionBlocks; i > functionBlocks; --i)
+		popBlock();
+	m_functionBlocks = functionBlocks;
+
+	// Loop body
+	popBlock();
+	// Loop header
+	popBlock();
+
+	// New function block starts with indices = 0
+	clearIndices();
+
+	if (m_breakSeen || m_continueSeen)
+	{
+		eraseKnowledge();
+		m_context.resetVariables([](VariableDeclaration const&) { return true; });
+	}
+
+	m_breakSeen = breakWasSeen;
+	m_continueSeen = continueWasSeen;
+}
+
 void CHC::reset()
 {
 	m_stateSorts.clear();
@@ -330,6 +427,8 @@ void CHC::reset()
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
 	m_unknownFunctionCallSeen = false;
+	m_breakSeen = false;
+	m_continueSeen = false;
 }
 
 void CHC::eraseKnowledge()
@@ -352,22 +451,26 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
 {
 	if (
 		_function.isPublic() &&
-		_function.isImplemented()
+		_function.isImplemented() &&
+		!_function.isConstructor()
 	)
 		return true;
 	return false;
 }
 
-void CHC::pushBlock(smt::Expression const& _block)
+void CHC::pushBlock(ASTNode const* _node)
 {
+	clearIndices();
 	m_context.pushSolver();
-	m_path.push_back(_block);
+	m_path.push_back(predicate(_node));
+	++m_functionBlocks;
 }
 
 void CHC::popBlock()
 {
 	m_context.popSolver();
 	m_path.pop_back();
+	--m_functionBlocks;
 }
 
 smt::SortPointer CHC::constructorSort()
@@ -404,12 +507,13 @@ smt::SortPointer CHC::sort(FunctionDefinition const& _function)
 	return m_nodeSorts[&_function] = move(sort);
 }
 
-smt::SortPointer CHC::sort(Block const& _block)
+smt::SortPointer CHC::sort(ASTNode const* _node)
 {
-	if (m_nodeSorts.count(&_block))
+	if (m_nodeSorts.count(_node))
-		return m_nodeSorts.at(&_block);
+		return m_nodeSorts.at(_node);
 
-	solAssert(_block.scope() == m_currentFunction, "");
+	if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
+		return sort(*funDef);
 
 	auto fSort = dynamic_pointer_cast<smt::FunctionSort>(sort(*m_currentFunction));
 	solAssert(fSort, "");
@@ -422,10 +526,10 @@ smt::SortPointer CHC::sort(Block const& _block)
 		fSort->domain + varSorts,
 		boolSort
 	);
-	return m_nodeSorts[&_block] = move(functionBodySort);
+	return m_nodeSorts[_node] = move(functionBodySort);
 }
 
-unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(smt::SortPointer _sort, string const& _name)
+unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name)
 {
 	auto block = make_unique<smt::SymbolicFunctionVariable>(
 		_sort,
@@ -462,33 +566,36 @@ smt::Expression CHC::error()
 	return (*m_errorPredicate)({});
 }
 
-void CHC::createFunctionBlock(FunctionDefinition const& _function)
+smt::Expression CHC::error(unsigned _idx)
 {
-	if (m_predicates.count(&_function))
+	return m_errorPredicate->valueAtIndex(_idx)({});
-	{
-		m_predicates.at(&_function)->increaseIndex();
-		m_interface->registerRelation(m_predicates.at(&_function)->currentValue());
-	}
-	else
-		m_predicates[&_function] = createBlock(
-			sort(_function),
-			predicateName(_function)
-		);
 }
 
-void CHC::createFunctionBlock(Block const& _block)
+void CHC::createBlock(ASTNode const* _node, string const& _prefix)
 {
-	solAssert(_block.scope() == m_currentFunction, "");
+	if (m_predicates.count(_node))
-	if (m_predicates.count(&_block))
 	{
-		m_predicates.at(&_block)->increaseIndex();
+		m_predicates.at(_node)->increaseIndex();
-		m_interface->registerRelation(m_predicates.at(&_block)->currentValue());
+		m_interface->registerRelation(m_predicates.at(_node)->currentValue());
 	}
 	else
-		m_predicates[&_block] = createBlock(
+		m_predicates[_node] = createSymbolicBlock(sort(_node), _prefix + predicateName(_node));
-			sort(_block),
+}
-			predicateName(*m_currentFunction) + "_body"
+
-		);
+void CHC::createErrorBlock()
+{
+	solAssert(m_errorPredicate, "");
+	m_errorPredicate->increaseIndex();
+	m_interface->registerRelation(m_errorPredicate->currentValue());
+}
+
+void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints)
+{
+	smt::Expression edge = smt::Expression::implies(
+		_from && m_context.assertions() && _constraints,
+		_to
+	);
+	addRule(edge, _from.name + "_to_" + _to.name);
 }
 
 vector<smt::Expression> CHC::currentFunctionVariables()
@@ -511,30 +618,44 @@ vector<smt::Expression> CHC::currentBlockVariables()
 	return currentFunctionVariables() + paramExprs;
 }
 
-string CHC::predicateName(FunctionDefinition const& _function)
+void CHC::clearIndices()
 {
-	string functionName = _function.isConstructor() ?
+	for (auto const& var: m_stateVariables)
-		"constructor" :
+		m_context.variable(*var)->resetIndex();
-		_function.isFallback() ?
+	if (m_currentFunction)
-			"fallback" :
+	{
-			"function_" + _function.name();
+		for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
-	return functionName + "_" + to_string(_function.id());
+			m_context.variable(*var)->resetIndex();
+		for (auto const& var: m_currentFunction->localVariables())
+			m_context.variable(*var)->resetIndex();
+	}
 }
 
-smt::Expression CHC::predicateCurrent(ASTNode const* _node)
+string CHC::predicateName(ASTNode const* _node)
 {
-	return (*m_predicates.at(_node))(currentFunctionVariables());
+	string prefix;
+	if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
+	{
+		prefix = funDef->isConstructor() ?
+			"constructor" :
+			funDef->isFallback() ?
+				"fallback" :
+				"function_" + funDef->name();
+		prefix += "_";
+	}
+	return prefix + to_string(_node->id());
 }
 
-smt::Expression CHC::predicateBodyCurrent(ASTNode const* _node)
+smt::Expression CHC::predicate(ASTNode const* _node)
 {
+	if (dynamic_cast<FunctionDefinition const*>(_node))
+		return (*m_predicates.at(_node))(currentFunctionVariables());
 	return (*m_predicates.at(_node))(currentBlockVariables());
 }
 
-smt::Expression CHC::predicateEntry(ASTNode const* _node)
+void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
 {
-	solAssert(!m_path.empty(), "");
+	m_interface->addRule(_rule, _ruleName);
-	return (*m_predicates.at(_node))(m_path.back().arguments);
 }
 
 bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)

libsolidity/formal/CHC.h

@@ -61,9 +61,17 @@ private:
 	bool visit(WhileStatement const&) override;
 	bool visit(ForStatement const&) override;
 	void endVisit(FunctionCall const& _node) override;
+	void endVisit(Break const& _node) override;
+	void endVisit(Continue const& _node) override;
 
 	void visitAssert(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
+	void visitLoop(
+		BreakableStatement const& _loop,
+		Expression const* _condition,
+		Statement const& _body,
+		ASTNode const* _postLoop
+	);
 	//@}
 
 	/// Helpers.
@@ -72,7 +80,7 @@ private:
 	void eraseKnowledge();
 	bool shouldVisit(ContractDefinition const& _contract) const;
 	bool shouldVisit(FunctionDefinition const& _function) const;
-	void pushBlock(smt::Expression const& _block);
+	void pushBlock(ASTNode const* _node);
 	void popBlock();
 	//@}
 
@@ -81,13 +89,13 @@ private:
 	smt::SortPointer constructorSort();
 	smt::SortPointer interfaceSort();
 	smt::SortPointer sort(FunctionDefinition const& _function);
-	smt::SortPointer sort(Block const& _block);
+	smt::SortPointer sort(ASTNode const* _block);
 	//@}
 
 	/// Predicate helpers.
 	//@{
 	/// @returns a new block of given _sort and _name.
-	std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(smt::SortPointer _sort, std::string const& _name);
+	std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smt::SortPointer _sort, std::string const& _name);
 
 	/// Constructor predicate over current variables.
 	smt::Expression constructor();
@@ -95,16 +103,17 @@ private:
 	smt::Expression interface();
 	/// Error predicate over current variables.
 	smt::Expression error();
+	smt::Expression error(unsigned _idx);
 
-	/// Creates a block for the given _function or increases its SSA index
+	/// Creates a block for the given _node or increases its SSA index
 	/// if the block already exists which in practice creates a new function.
-	/// The predicate parameters are _function input and output parameters.
+	void createBlock(ASTNode const* _node, std::string const& _prefix = "");
-	void createFunctionBlock(FunctionDefinition const& _function);
+
-	/// Creates a block for the given _function or increases its SSA index
+	/// Creates a new error block to be used by an assertion.
-	/// if the block already exists which in practice creates a new function.
+	/// Also registers the predicate.
-	/// The predicate parameters are m_currentFunction input, output
+	void createErrorBlock();
-	/// and local variables.
+
-	void createFunctionBlock(Block const& _block);
+	void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true));
 
 	/// @returns the current symbolic values of the current function's
 	/// input and output parameters.
@@ -113,19 +122,20 @@ private:
 	/// local variables.
 	std::vector<smt::Expression> currentBlockVariables();
 
-	/// @returns the predicate name for a given function.
+	/// Sets the SSA indices of the variables in scope to 0.
-	std::string predicateName(FunctionDefinition const& _function);
+	/// Used when starting a new block.
-	/// @returns a predicate application over the current function's parameters.
+	void clearIndices();
-	smt::Expression predicateCurrent(ASTNode const* _node);
+
-	/// @returns a predicate application over the current function's parameters plus local variables.
+	/// @returns the predicate name for a given node.
-	smt::Expression predicateBodyCurrent(ASTNode const* _node);
+	std::string predicateName(ASTNode const* _node);
-	/// Predicate for block _node over the variables at the latest
+	/// @returns a predicate application over the current scoped variables.
-	/// block entry.
+	smt::Expression predicate(ASTNode const* _node);
-	smt::Expression predicateEntry(ASTNode const* _node);
 	//@}
 
 	/// Solver related.
 	//@{
+	/// Adds Horn rule to the solver.
+	void addRule(smt::Expression const& _rule, std::string const& _ruleName);
 	/// @returns true if query is unsatisfiable (safe).
 	bool query(smt::Expression const& _query, langutil::SourceLocation const& _location);
 	//@}
@@ -179,6 +189,15 @@ private:
 	std::vector<smt::Expression> m_path;
 	/// Whether a function call was seen in the current scope.
 	bool m_unknownFunctionCallSeen = false;
+	/// Whether a break statement was seen in the current scope.
+	bool m_breakSeen = false;
+	/// Whether a continue statement was seen in the current scope.
+	bool m_continueSeen = false;
+
+	/// Block where a loop break should go to.
+	ASTNode const* m_breakDest;
+	/// Block where a loop continue should go to.
+	ASTNode const* m_continueDest;
 	//@}
 
 	/// CHC solver.

libsolidity/formal/SMTEncoder.cpp

@@ -962,18 +962,21 @@ pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
 
 	smt::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
 	auto value = smt::Expression::ite(
-		valueNoMod > smt::maxValue(intType) || valueNoMod < smt::minValue(intType),
+		valueNoMod > smt::maxValue(intType),
 		valueNoMod % intValueRange,
-		valueNoMod
+		smt::Expression::ite(
+			valueNoMod < smt::minValue(intType),
+			valueNoMod % intValueRange,
+			valueNoMod
+		)
 	);
+
 	if (intType.isSigned())
-	{
 		value = smt::Expression::ite(
 			value > smt::maxValue(intType),
 			value - intValueRange,
 			value
 		);
-	}
 
 	return {value, valueNoMod};
 }

libsolidity/formal/SMTEncoder.h

@@ -88,6 +88,8 @@ protected:
 	void endVisit(IndexAccess const& _node) override;
 	void endVisit(IndexRangeAccess const& _node) override;
 	bool visit(InlineAssembly const& _node) override;
+	void endVisit(Break const&) override {}
+	void endVisit(Continue const&) override {}
 
 	/// Do not visit subtree if node is a RationalNumber.
 	/// Symbolic _expr is the rational literal.

libsolidity/formal/SymbolicTypes.cpp

@@ -295,7 +295,6 @@ Expression zeroValue(solidity::TypePointer const& _type)
 			auto mappingType = dynamic_cast<MappingType const*>(_type);
 			solAssert(mappingType, "");
 			return Expression::const_array(Expression(mappingType), zeroValue(mappingType->valueType()));
-
 		}
 		solAssert(false, "");
 	}

libsolidity/formal/Z3CHCInterface.cpp

@@ -41,6 +41,7 @@ Z3CHCInterface::Z3CHCInterface():
 	// These are useful for solving problems with arrays and loops.
 	// Use quantified lemma generalizer.
 	p.set("fp.spacer.q3.use_qgen", true);
+	p.set("fp.spacer.mbqi", false);
 	// Ground pobs by using values from a model.
 	p.set("fp.spacer.ground_pobs", false);
 	m_solver.set(p);
@@ -100,7 +101,7 @@ pair<CheckResult, vector<string>> Z3CHCInterface::query(Expression const& _expr)
 		}
 		// TODO retrieve model / invariants
 	}
-	catch (z3::exception const& _e)
+	catch (z3::exception const&)
 	{
 		result = CheckResult::ERROR;
 		values.clear();

libyul/optimiser/SSATransform.cpp

@@ -32,45 +32,32 @@ using namespace dev;
 using namespace langutil;
 using namespace yul;
 
-void SSATransform::operator()(Identifier& _identifier)
+namespace
 {
-	if (m_currentVariableValues.count(_identifier.name))
-		_identifier.name = m_currentVariableValues[_identifier.name];
-}
 
-void SSATransform::operator()(ForLoop& _for)
+/**
+ * First step of SSA transform: Introduces new SSA variables for each assignment or
+ * declaration of a variable to be replaced.
+ */
+class IntroduceSSA: public ASTModifier
 {
-	// This will clear the current value in case of a reassignment inside the
+public:
-	// init part, although the new variable would still be in scope inside the whole loop.
+	explicit IntroduceSSA(NameDispenser& _nameDispenser, set<YulString> const& _variablesToReplace):
-	// This small inefficiency is fine if we move the pre part of all for loops out
+		m_nameDispenser(_nameDispenser), m_variablesToReplace(_variablesToReplace)
-	// of the for loop.
+	{ }
-	(*this)(_for.pre);
 
-	Assignments assignments;
+	void operator()(Block& _block) override;
-	assignments(_for.body);
-	assignments(_for.post);
-	for (auto const& var: assignments.names())
-		m_currentVariableValues.erase(var);
 
-	visit(*_for.condition);
+private:
-	(*this)(_for.body);
+	NameDispenser& m_nameDispenser;
-	(*this)(_for.post);
+	/// This is a set of all variables that are assigned to anywhere in the code.
-}
+	/// Variables that are only declared but never re-assigned are not touched.
+	set<YulString> const& m_variablesToReplace;
+};
 
 
-void SSATransform::operator()(Block& _block)
+void IntroduceSSA::operator()(Block& _block)
 {
-	set<YulString> variablesToClearAtEnd;
-
-	// Creates a new variable and stores it in the current variable value map.
-	auto newVariable = [&](YulString _varName) -> YulString
-	{
-		YulString newName = m_nameDispenser.newName(_varName);
-		m_currentVariableValues[_varName] = newName;
-		variablesToClearAtEnd.emplace(_varName);
-		return newName;
-	};
-
 	iterateReplacing(
 		_block.statements,
 		[&](Statement& _s) -> boost::optional<vector<Statement>>
@@ -96,8 +83,8 @@ void SSATransform::operator()(Block& _block)
 				TypedNameList newVariables;
 				for (auto const& var: varDecl.variables)
 				{
-					YulString newName = newVariable(var.name);
 					YulString oldName = var.name;
+					YulString newName = m_nameDispenser.newName(oldName);
 					newVariables.emplace_back(TypedName{loc, newName, {}});
 					statements.emplace_back(VariableDeclaration{
 						loc,
@@ -123,8 +110,8 @@ void SSATransform::operator()(Block& _block)
 				TypedNameList newVariables;
 				for (auto const& var: assignment.variableNames)
 				{
-					YulString newName = newVariable(var.name);
 					YulString oldName = var.name;
+					YulString newName = m_nameDispenser.newName(oldName);
 					newVariables.emplace_back(TypedName{loc, newName, {}});
 					statements.emplace_back(Assignment{
 						loc,
@@ -140,14 +127,111 @@ void SSATransform::operator()(Block& _block)
 			return {};
 		}
 	);
-	for (auto const& var: variablesToClearAtEnd)
+}
+
+/**
+ * Second step of SSA transform: Replace the references to variables-to-be-replaced
+ * by their current values.
+ */
+class PropagateValues: public ASTModifier
+{
+public:
+	explicit PropagateValues(set<YulString> const& _variablesToReplace):
+		m_variablesToReplace(_variablesToReplace)
+	{ }
+
+	void operator()(Identifier& _identifier) override;
+	void operator()(VariableDeclaration& _varDecl) override;
+	void operator()(Assignment& _assignment) override;
+	void operator()(ForLoop& _for) override;
+	void operator()(Block& _block) override;
+
+private:
+	/// This is a set of all variables that are assigned to anywhere in the code.
+	/// Variables that are only declared but never re-assigned are not touched.
+	set<YulString> const& m_variablesToReplace;
+	map<YulString, YulString> m_currentVariableValues;
+	set<YulString> m_clearAtEndOfBlock;
+};
+
+void PropagateValues::operator()(Identifier& _identifier)
+{
+	if (m_currentVariableValues.count(_identifier.name))
+		_identifier.name = m_currentVariableValues[_identifier.name];
+}
+
+void PropagateValues::operator()(VariableDeclaration& _varDecl)
+{
+	ASTModifier::operator()(_varDecl);
+
+	if (_varDecl.variables.size() != 1)
+		return;
+	YulString name = _varDecl.variables.front().name;
+	if (!m_variablesToReplace.count(name))
+		return;
+
+	yulAssert(_varDecl.value->type() == typeid(Identifier), "");
+	m_currentVariableValues[name] = boost::get<Identifier>(*_varDecl.value).name;
+	m_clearAtEndOfBlock.insert(name);
+}
+
+
+void PropagateValues::operator()(Assignment& _assignment)
+{
+	visit(*_assignment.value);
+
+	if (_assignment.variableNames.size() != 1)
+		return;
+	YulString name = _assignment.variableNames.front().name;
+	if (!m_variablesToReplace.count(name))
+		return;
+
+	yulAssert(_assignment.value->type() == typeid(Identifier), "");
+	m_currentVariableValues[name] = boost::get<Identifier>(*_assignment.value).name;
+	m_clearAtEndOfBlock.insert(name);
+}
+
+void PropagateValues::operator()(ForLoop& _for)
+{
+	// This will clear the current value in case of a reassignment inside the
+	// init part, although the new variable would still be in scope inside the whole loop.
+	// This small inefficiency is fine if we move the pre part of all for loops out
+	// of the for loop.
+	(*this)(_for.pre);
+
+	Assignments assignments;
+	assignments(_for.body);
+	assignments(_for.post);
+
+	for (auto const& var: assignments.names())
 		m_currentVariableValues.erase(var);
+
+	visit(*_for.condition);
+	(*this)(_for.body);
+	(*this)(_for.post);
+}
+
+void PropagateValues::operator()(Block& _block)
+{
+	set<YulString> clearAtParentBlock = std::move(m_clearAtEndOfBlock);
+	m_clearAtEndOfBlock.clear();
+
+	ASTModifier::operator()(_block);
+
+	for (auto const& var: m_clearAtEndOfBlock)
+		m_currentVariableValues.erase(var);
+
+	m_clearAtEndOfBlock = std::move(clearAtParentBlock);
+}
+
 }
 
 void SSATransform::run(Block& _ast, NameDispenser& _nameDispenser)
 {
 	Assignments assignments;
 	assignments(_ast);
-	SSATransform{_nameDispenser, assignments.names()}(_ast);
+	IntroduceSSA{_nameDispenser, assignments.names()}(_ast);
+	PropagateValues{assignments.names()}(_ast);
 }
 
+

libyul/optimiser/SSATransform.h

@@ -75,22 +75,7 @@ class NameDispenser;
 class SSATransform: public ASTModifier
 {
 public:
-	void operator()(Identifier&) override;
-	void operator()(ForLoop&) override;
-	void operator()(Block& _block) override;
-
 	static void run(Block& _ast, NameDispenser& _nameDispenser);
-
-private:
-	explicit SSATransform(NameDispenser& _nameDispenser, std::set<YulString> const& _variablesToReplace):
-		m_nameDispenser(_nameDispenser), m_variablesToReplace(_variablesToReplace)
-	{ }
-
-	NameDispenser& m_nameDispenser;
-	/// This is a set of all variables that are assigned to anywhere in the code.
-	/// Variables that are only declared but never re-assigned are not touched.
-	std::set<YulString> const& m_variablesToReplace;
-	std::map<YulString, YulString> m_currentVariableValues;
 };
 
 }

test/libsolidity/semanticTests/storage/mappings_array2d_pop_delete.sol

@@ -0,0 +1,39 @@
+contract C {
+	mapping (uint => uint)[][] a;
+
+	function n1(uint key, uint value) public {
+		a.length++;
+		mapping (uint => uint)[] storage b = a[a.length - 1];
+		b.length++;
+		b[b.length - 1][key] = value;
+	}
+
+	function n2() public {
+		a.length++;
+		mapping (uint => uint)[] storage b = a[a.length - 1];
+		b.length++;
+	}
+
+	function map(uint key) public view returns (uint) {
+		mapping (uint => uint)[] storage b = a[a.length - 1];
+		return b[b.length - 1][key];
+	}
+
+	function p() public {
+		a.pop();
+	}
+
+	function d() public returns (uint) {
+		delete a;
+		return a.length;
+	}
+}
+// ----
+// n1(uint256,uint256): 42, 64 ->
+// map(uint256): 42 -> 64
+// p() ->
+// n2() ->
+// map(uint256): 42 -> 64
+// d() -> 0
+// n2() ->
+// map(uint256): 42 -> 64

test/libsolidity/semanticTests/storage/mappings_array_pop_delete.sol

@@ -0,0 +1,34 @@
+contract C {
+	mapping (uint => uint)[] a;
+
+	function n1(uint key, uint value) public {
+		a.length++;
+		a[a.length - 1][key] = value;
+	}
+
+	function n2() public {
+		a.length++;
+	}
+
+	function map(uint key) public view returns (uint) {
+		return a[a.length - 1][key];
+	}
+
+	function p() public {
+		a.pop();
+	}
+
+	function d() public returns (uint) {
+		delete a;
+		return a.length;
+	}
+}
+// ----
+// n1(uint256,uint256): 42, 64 ->
+// map(uint256): 42 -> 64
+// p() ->
+// n2() ->
+// map(uint256): 42 -> 64
+// d() -> 0
+// n2() ->
+// map(uint256): 42 -> 64

test/libsolidity/smtCheckerTests/invariants/loop_array.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	uint[] a;
+	function f(uint n) public {
+		uint i;
+		while (i < n)
+		{
+			a[i] = i;
+			++i;
+		}
+		require(n > 1);
+		// Assertion is safe but current solver version cannot solve it.
+		// Keep test for next solver release.
+		assert(a[n-1] > a[n-2]);
+	}
+}
+// ----
+// Warning: (273-296): Assertion violation happens here

test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	uint[] a;
+	function f(uint n) public {
+		uint i;
+		for (i = 0; i < n; ++i)
+			a[i] = i;
+		require(n > 1);
+		// Assertion is safe but current solver version cannot solve it.
+		// Keep test for next solver release.
+		assert(a[n-1] > a[n-2]);
+	}
+}
+// ----
+// Warning: (267-290): Assertion violation happens here

test/libsolidity/smtCheckerTests/invariants/loop_basic.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	function f(uint x) public pure {
+		uint y;
+		require(x > 0);
+		while (y < x)
+			++y;
+		assert(y == x);
+	}
+}

test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	function f(uint x) public pure {
+		uint y;
+		for (y = 0; y < x; ++y) {}
+		assert(y == x);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/invariants/loop_nested.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	function f() public pure {
+		uint x = 10;
+		uint y;
+		while (y < x)
+		{
+			++y;
+			x = 0;
+			while (x < 10)
+				++x;
+			assert(x == 10);
+		}
+		assert(y == x);
+	}
+}

test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	function f() public pure {
+		uint x;
+		uint y;
+		for (x = 10; y < x; ++y)
+		{
+			for (x = 0; x < 10; ++x) {}
+			assert(x == 10);
+		}
+		assert(y == x);
+	}
+}

test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol

@@ -15,4 +15,3 @@ contract C
 }
 // ----
 // Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (269-282): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -8,10 +8,12 @@ contract C
 			// Overflows due to resetting x.
 			x = x + 1;
 		}
-		// The assertion is true but x is touched and reset.
+		// Assertion is safe but current solver version cannot solve it.
+		// Keep test for next solver release.
 		assert(x > 0);
 	}
 }
 // ----
+// Warning: (296-309): Error trying to invoke SMT solver.
 // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (244-257): Assertion violation happens here
+// Warning: (296-309): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_6.sol

@@ -10,4 +10,3 @@ contract C {
     }
 }
 // ----
-// Warning: (213-226): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol

@@ -18,5 +18,4 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (265-285): Assertion violation happens here
 // Warning: (312-331): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol

@@ -18,6 +18,5 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (266-286): Assertion violation happens here
 // Warning: (290-309): Assertion violation happens here
 // Warning: (313-332): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol

@@ -15,4 +15,3 @@ contract C {
 }
 // ----
 // Warning: (115-121): Unused local variable.
-// Warning: (356-370): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1.sol

@@ -14,4 +14,3 @@ contract C
 	}
 }
 // ----
-// Warning: (177-190): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_break.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 10);
+		while (x < 10) {
+			if (b)
+				++x;
+			else {
+				x = 20;
+				break;
+			}
+		}
+		// Assertion is safe but break is unsupported for now
+		// so knowledge is erased.
+		assert(x >= 10);
+	}
+}
+// ----
+// Warning: (274-289): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 10);
+		while (x < 10) {
+			if (b)
+				++x;
+			else {
+				break;
+			}
+		}
+		// Fails because the loop might break.
+		assert(x >= 10);
+	}
+}
+// ----
+// Warning: (218-233): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_continue.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 100);
+		while (x < 10) {
+			if (b) {
+				x = 15;
+				continue;
+			}
+			else
+				x = 20;
+
+		}
+		// Should be safe, but fails due to continue being unsupported
+		// and erasing all knowledge.
+		assert(x >= 15);
+	}
+}
+// ----
+// Warning: (294-309): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 100);
+		while (x < 10) {
+			if (b) {
+				x = 15;
+				continue;
+			}
+			else
+				x = 20;
+
+		}
+		// Fails due to the if.
+		assert(x >= 17);
+	}
+}
+// ----
+// Warning: (223-238): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 100);
+		while (x < 10) {
+			if (b)
+				x = x + 1;
+			else
+				x = 0;
+		}
+		// CHC proves it safe because
+		// 1- if it doesn't go in the loop in the first place, x >= 10
+		// 2- if it goes in the loop and b == true, x increases until >= 10
+		// 3- if it goes in the loop and b == false, it's an infinite loop, therefore
+		//    the assertion and the error are unreachable.
+		assert(x > 0);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/loops/while_2.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x) public pure {
+		x = 2;
+		while (x > 1) {
+			if (x > 10)
+				x = 2;
+			else
+				--x;
+		}
+		assert(x < 2);
+	}
+}

test/libsolidity/smtCheckerTests/loops/while_2_break.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint x = 0;
+		while (x == 0) {
+			++x;
+			break;
+			++x;
+		}
+		// Assertion is safe but break is unsupported for now
+		// so knowledge is erased.
+		assert(x == 1);
+	}
+}
+// ----
+// Warning: (128-131): Unreachable code.
+// Warning: (224-238): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		while (x == 0) {
+			++x;
+			break;
+			++x;
+		}
+		assert(x == 2);
+	}
+}
+// ----
+// Warning: (120-123): Unreachable code.
+// Warning: (131-145): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_2_fail.sol

@@ -12,4 +12,3 @@ contract C {
 	}
 }
 // ----
-// Warning: (158-172): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol

@@ -13,11 +13,13 @@ contract LoopFor2 {
 			c[i] = b[i];
 			++i;
 		}
+		// Fails due to aliasing, since both b and c are
+		// memory references of same type.
 		assert(b[0] == c[0]);
 		assert(a[0] == 900);
 		assert(b[0] == 900);
 	}
 }
 // ----
-// Warning: (274-294): Assertion violation happens here
+// Warning: (362-382): Assertion violation happens here
-// Warning: (321-340): Assertion violation happens here
+// Warning: (409-428): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol

@@ -20,5 +20,4 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (265-285): Assertion violation happens here
 // Warning: (312-331): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol

@@ -20,6 +20,5 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (266-286): Assertion violation happens here
 // Warning: (290-309): Assertion violation happens here
 // Warning: (313-332): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol

@@ -8,4 +8,3 @@ contract C {
     }
 }
 // ----
-// Warning: (199-213): Assertion violation happens here

test/libsolidity/smtCheckerTestsJSON/multi.json

@@ -4,7 +4,6 @@
 		"smtlib2responses":
 		{
 			"0x047d0c67d7e03c5ac96ca227d1e19ba63257f4ab19cef30029413219ec8963af": "sat\n((|EVALEXPR_0| 0))\n",
-			"0x21d5b49d1416d788fe34b1d2a10a99ea92b007e17a977604afd7b2ff01a055cd": "unsat\n",
 			"0xada7569fb01a9b3e2823517ed40dcc99b11fb1e433e6e3ec8a8713f6f95753d3": "sat\n((|EVALEXPR_0| 1))\n"
 		}
 	}

test/libyul/yulOptimizerTests/ssaAndBack/for_loop.yul

@@ -23,8 +23,8 @@
 //     let b := mload(1)
 //     for { } lt(mload(a), mload(b)) { a := mload(b) }
 //     {
-//         let b_3 := mload(a)
+//         let b_4 := mload(a)
-//         let a_6 := mload(b_3)
+//         let a_7 := mload(b_4)
-//         b := mload(a_6)
+//         b := mload(a_7)
 //     }
 // }

test/libyul/yulOptimizerTests/ssaTransform/for_simple.yul

@@ -36,12 +36,12 @@
 //     }
 //     a
 //     {
-//         let a_7 := add(a, 6)
+//         let a_6 := add(a, 6)
-//         a := a_7
+//         a := a_6
 //     }
 //     {
-//         let a_6 := add(a, 12)
+//         let a_7 := add(a, 12)
-//         a := a_6
+//         a := a_7
 //     }
 //     let a_8 := add(a, 8)
 //     a := a_8

test/tools/ossfuzz/protoToAbiV2.cpp

@@ -653,28 +653,36 @@ void ProtoConverter::visit(ArrayType const& _x)
 	if (_x.info_size() == 0 || _x.info_size() > (int)s_maxArrayDimensions)
 		return;
 
+	// Array type is dynamically encoded if one of the following is true
+	//   - array base type is "bytes" or "string"
+	//   - at least one array dimension is dynamically sized.
+	if (_x.base_type_oneof_case() == ArrayType::kDynbytesty)
+		m_isLastDynParamRightPadded = true;
+	else
+		for (auto const& dim: _x.info())
+			if (!dim.is_static())
+			{
+				m_isLastDynParamRightPadded = true;
+				break;
+			}
+
 	string baseType = {};
 	switch (_x.base_type_oneof_case())
 	{
 	case ArrayType::kInty:
 		baseType = getIntTypeAsString(_x.inty());
-		m_isLastDynParamRightPadded = false;
 		break;
 	case ArrayType::kByty:
 		baseType = getFixedByteTypeAsString(_x.byty());
-		m_isLastDynParamRightPadded = false;
 		break;
 	case ArrayType::kAdty:
 		baseType = getAddressTypeAsString(_x.adty());
-		m_isLastDynParamRightPadded = false;
 		break;
 	case ArrayType::kBoolty:
 		baseType = getBoolTypeAsString();
-		m_isLastDynParamRightPadded = false;
 		break;
 	case ArrayType::kDynbytesty:
 		baseType = bytesArrayTypeAsString(_x.dynbytesty());
-		m_isLastDynParamRightPadded = true;
 		break;
 	case ArrayType::kStty:
 	case ArrayType::BASE_TYPE_ONEOF_NOT_SET: