[SMTChecker] Refactor CHC loops and add if blocks

Changelog.md

@@ -5,6 +5,7 @@ Language Features:
 
 Compiler Features:
  * Code Generator: Use SELFBALANCE for ``address(this).balance`` if using Istanbul EVM
+ * SMTChecker: Add break/continue support to the CHC engine.
  * SMTChecker: Support assignments to multi-dimensional arrays and mappings.
 
 

libsolidity/formal/CHC.cpp

@@ -137,24 +137,22 @@ bool CHC::visit(FunctionDefinition const& _function)
 
 	initFunction(_function);
 
+	auto functionEntryBlock = createBlock(m_currentFunction);
+	auto bodyBlock = createBlock(&m_currentFunction->body());
+
+	auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables());
+	auto bodyPred = predicate(*bodyBlock);
+
 	// Store the constraints related to variable initialization.
 	smt::Expression const& initAssertions = m_context.assertions();
 	m_context.pushSolver();
 
-	solAssert(m_functionBlocks == 0, "");
-
-	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());
+	setCurrentBlock(*bodyBlock);
 
 	// We need to re-add the constraints that were created for initialization of variables.
 	m_context.addAssertion(initAssertions);
@@ -169,25 +167,10 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	if (!shouldVisit(_function))
 		return;
 
-	solAssert(m_currentFunction == &_function, "Inlining internal function calls not yet implemented");
-
-	// Function Exit block.
-	createBlock(m_currentFunction);
-	connectBlocks(m_path.back(), predicate(&_function));
-
-	// Rule FunctionExit -> Interface, uses no constraints.
-	clearIndices();
-	m_context.pushSolver();
-	connectBlocks(predicate(&_function), interface());
-	m_context.popSolver();
+	connectBlocks(m_currentBlock, interface());
 
+	solAssert(&_function == m_currentFunction, "");
 	m_currentFunction = nullptr;
-	solAssert(m_path.size() == m_functionBlocks, "");
-	while (m_functionBlocks > 0)
-		popBlock();
-
-	solAssert(m_path.empty(), "");
-
 	SMTEncoder::endVisit(_function);
 }
 
@@ -198,7 +181,38 @@ bool CHC::visit(IfStatement const& _if)
 	bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
 	m_unknownFunctionCallSeen = false;
 
-	SMTEncoder::visit(_if);
+	solAssert(m_currentFunction, "");
+	auto const& functionBody = m_currentFunction->body();
+
+	auto ifHeaderBlock = createBlock(&_if, "if_header_");
+	auto trueBlock = createBlock(&_if.trueStatement(), "if_true_");
+	auto falseBlock = _if.falseStatement() ? createBlock(_if.falseStatement(), "if_false_") : nullptr;
+	auto afterIfBlock = createBlock(&functionBody);
+
+	connectBlocks(m_currentBlock, predicate(*ifHeaderBlock));
+
+	setCurrentBlock(*ifHeaderBlock);
+	_if.condition().accept(*this);
+	auto condition = expr(_if.condition());
+
+	connectBlocks(m_currentBlock, predicate(*trueBlock), condition);
+	if (_if.falseStatement())
+		connectBlocks(m_currentBlock, predicate(*falseBlock), !condition);
+	else
+		connectBlocks(m_currentBlock, predicate(*afterIfBlock), !condition);
+
+	setCurrentBlock(*trueBlock);
+	_if.trueStatement().accept(*this);
+	connectBlocks(m_currentBlock, predicate(*afterIfBlock));
+
+	if (_if.falseStatement())
+	{
+		setCurrentBlock(*falseBlock);
+		_if.falseStatement()->accept(*this);
+		connectBlocks(m_currentBlock, predicate(*afterIfBlock));
+	}
+
+	setCurrentBlock(*afterIfBlock);
 
 	if (m_unknownFunctionCallSeen)
 		eraseKnowledge();
@@ -214,16 +228,41 @@ bool CHC::visit(WhileStatement const& _while)
 	m_unknownFunctionCallSeen = false;
 
 	solAssert(m_currentFunction, "");
+	auto const& functionBody = m_currentFunction->body();
+
+	auto namePrefix = string(_while.isDoWhile() ? "do_" : "") + "while";
+	auto loopHeaderBlock = createBlock(&_while, namePrefix + "_header_");
+	auto loopBodyBlock = createBlock(&_while.body(), namePrefix + "_body_");
+	auto afterLoopBlock = createBlock(&functionBody);
+
+	auto outerBreakDest = m_breakDest;
+	auto outerContinueDest = m_continueDest;
+	m_breakDest = afterLoopBlock.get();
+	m_continueDest = loopHeaderBlock.get();
 
 	if (_while.isDoWhile())
 		_while.body().accept(*this);
 
-	visitLoop(
-		_while,
-		&_while.condition(),
-		_while.body(),
-		nullptr
-	);
+	connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
+
+	setCurrentBlock(*loopHeaderBlock);
+
+	_while.condition().accept(*this);
+	auto condition = expr(_while.condition());
+
+	connectBlocks(m_currentBlock, predicate(*loopBodyBlock), condition);
+	connectBlocks(m_currentBlock, predicate(*afterLoopBlock), !condition);
+
+	// Loop body visit.
+	setCurrentBlock(*loopBodyBlock);
+	_while.body().accept(*this);
+
+	m_breakDest = outerBreakDest;
+	m_continueDest = outerContinueDest;
+
+	// Back edge.
+	connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
+	setCurrentBlock(*afterLoopBlock);
 
 	if (m_unknownFunctionCallSeen)
 		eraseKnowledge();
@@ -239,16 +278,52 @@ bool CHC::visit(ForStatement const& _for)
 	m_unknownFunctionCallSeen = false;
 
 	solAssert(m_currentFunction, "");
+	auto const& functionBody = m_currentFunction->body();
+
+	auto loopHeaderBlock = createBlock(&_for, "for_header_");
+	auto loopBodyBlock = createBlock(&_for.body(), "for_body_");
+	auto afterLoopBlock = createBlock(&functionBody);
+	auto postLoop = _for.loopExpression();
+	auto postLoopBlock = postLoop ? createBlock(postLoop, "for_post_") : nullptr;
+
+	auto outerBreakDest = m_breakDest;
+	auto outerContinueDest = m_continueDest;
+	m_breakDest = afterLoopBlock.get();
+	m_continueDest = postLoop ? postLoopBlock.get() : loopHeaderBlock.get();
 
 	if (auto init = _for.initializationExpression())
 		init->accept(*this);
 
-	visitLoop(
-		_for,
-		_for.condition(),
-		_for.body(),
-		_for.loopExpression()
-	);
+	connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
+	setCurrentBlock(*loopHeaderBlock);
+
+	auto condition = smt::Expression(true);
+	if (auto forCondition = _for.condition())
+	{
+		forCondition->accept(*this);
+		condition = expr(*forCondition);
+	}
+
+	connectBlocks(m_currentBlock, predicate(*loopBodyBlock), condition);
+	connectBlocks(m_currentBlock, predicate(*afterLoopBlock), !condition);
+
+	// Loop body visit.
+	setCurrentBlock(*loopBodyBlock);
+	_for.body().accept(*this);
+
+	if (postLoop)
+	{
+		connectBlocks(m_currentBlock, predicate(*postLoopBlock));
+		setCurrentBlock(*postLoopBlock);
+		postLoop->accept(*this);
+	}
+
+	m_breakDest = outerBreakDest;
+	m_continueDest = outerContinueDest;
+
+	// Back edge.
+	connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
+	setCurrentBlock(*afterLoopBlock);
 
 	if (m_unknownFunctionCallSeen)
 		eraseKnowledge();
@@ -301,16 +376,20 @@ void CHC::endVisit(FunctionCall const& _funCall)
 	createReturnedExpressions(_funCall);
 }
 
-void CHC::endVisit(Break const&)
+void CHC::endVisit(Break const& _break)
 {
 	solAssert(m_breakDest, "");
-	m_breakSeen = true;
+	connectBlocks(m_currentBlock, predicate(*m_breakDest));
+	auto breakGhost = createBlock(&_break, "break_ghost_");
+	m_currentBlock = predicate(*breakGhost);
 }
 
-void CHC::endVisit(Continue const&)
+void CHC::endVisit(Continue const& _continue)
 {
 	solAssert(m_continueDest, "");
-	m_continueSeen = true;
+	connectBlocks(m_currentBlock, predicate(*m_continueDest));
+	auto continueGhost = createBlock(&_continue, "continue_ghost_");
+	m_currentBlock = predicate(*continueGhost);
 }
 
 void CHC::visitAssert(FunctionCall const& _funCall)
@@ -319,12 +398,10 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 	solAssert(args.size() == 1, "");
 	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
 
-	solAssert(!m_path.empty(), "");
-
 	createErrorBlock();
 
 	smt::Expression assertNeg = !(m_context.expression(*args.front())->currentValue());
-	connectBlocks(m_path.back(), error(), currentPathConditions() && assertNeg);
+	connectBlocks(m_currentBlock, error(), currentPathConditions() && assertNeg);
 
 	m_verificationTargets.push_back(&_funCall);
 }
@@ -341,85 +418,6 @@ 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();
@@ -427,8 +425,9 @@ void CHC::reset()
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
 	m_unknownFunctionCallSeen = false;
-	m_breakSeen = false;
-	m_continueSeen = false;
+	m_blockCounter = 0;
+	m_breakDest = nullptr;
+	m_continueDest = nullptr;
 }
 
 void CHC::eraseKnowledge()
@@ -458,19 +457,12 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
 	return false;
 }
 
-void CHC::pushBlock(ASTNode const* _node)
-{
-	clearIndices();
-	m_context.pushSolver();
-	m_path.push_back(predicate(_node));
-	++m_functionBlocks;
-}
-
-void CHC::popBlock()
+void CHC::setCurrentBlock(smt::SymbolicFunctionVariable const& _block)
 {
 	m_context.popSolver();
-	m_path.pop_back();
-	--m_functionBlocks;
+	clearIndices();
+	m_context.pushSolver();
+	m_currentBlock = predicate(_block);
 }
 
 smt::SortPointer CHC::constructorSort()
@@ -493,25 +485,18 @@ smt::SortPointer CHC::interfaceSort()
 
 smt::SortPointer CHC::sort(FunctionDefinition const& _function)
 {
-	if (m_nodeSorts.count(&_function))
-		return m_nodeSorts.at(&_function);
-
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
 	vector<smt::SortPointer> varSorts;
 	for (auto const& var: _function.parameters() + _function.returnParameters())
 		varSorts.push_back(smt::smtSort(*var->type()));
-	auto sort = make_shared<smt::FunctionSort>(
+	return make_shared<smt::FunctionSort>(
 		m_stateSorts + varSorts,
 		boolSort
 	);
-	return m_nodeSorts[&_function] = move(sort);
 }
 
 smt::SortPointer CHC::sort(ASTNode const* _node)
 {
-	if (m_nodeSorts.count(_node))
-		return m_nodeSorts.at(_node);
-
 	if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
 		return sort(*funDef);
 
@@ -522,11 +507,10 @@ smt::SortPointer CHC::sort(ASTNode const* _node)
 	vector<smt::SortPointer> varSorts;
 	for (auto const& var: m_currentFunction->localVariables())
 		varSorts.push_back(smt::smtSort(*var->type()));
-	auto functionBodySort = make_shared<smt::FunctionSort>(
+	return make_shared<smt::FunctionSort>(
 		fSort->domain + varSorts,
 		boolSort
 	);
-	return m_nodeSorts[_node] = move(functionBodySort);
 }
 
 unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name)
@@ -571,15 +555,14 @@ smt::Expression CHC::error(unsigned _idx)
 	return m_errorPredicate->valueAtIndex(_idx)({});
 }
 
-void CHC::createBlock(ASTNode const* _node, string const& _prefix)
+unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node, string const& _prefix)
 {
-	if (m_predicates.count(_node))
-	{
-		m_predicates.at(_node)->increaseIndex();
-		m_interface->registerRelation(m_predicates.at(_node)->currentValue());
-	}
-	else
-		m_predicates[_node] = createSymbolicBlock(sort(_node), _prefix + predicateName(_node));
+	return createSymbolicBlock(sort(_node),
+		"block_" +
+		uniquePrefix() +
+		"_" +
+		_prefix +
+		predicateName(_node));
 }
 
 void CHC::createErrorBlock()
@@ -646,13 +629,20 @@ string CHC::predicateName(ASTNode const* _node)
 	return prefix + to_string(_node->id());
 }
 
-smt::Expression CHC::predicate(ASTNode const* _node)
+smt::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block)
 {
-	if (dynamic_cast<FunctionDefinition const*>(_node))
-		return (*m_predicates.at(_node))(currentFunctionVariables());
-	return (*m_predicates.at(_node))(currentBlockVariables());
+	return _block(currentBlockVariables());
 }
 
+smt::Expression CHC::predicate(
+	smt::SymbolicFunctionVariable const& _block,
+	vector<smt::Expression> const& _arguments
+)
+{
+	return _block(_arguments);
+}
+
+
 void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
 {
 	m_interface->addRule(_rule, _ruleName);
@@ -680,3 +670,8 @@ bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _
 	}
 	return false;
 }
+
+string CHC::uniquePrefix()
+{
+	return to_string(m_blockCounter++);
+}

libsolidity/formal/CHC.h

@@ -66,12 +66,6 @@ private:
 
 	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.
@@ -80,8 +74,7 @@ private:
 	void eraseKnowledge();
 	bool shouldVisit(ContractDefinition const& _contract) const;
 	bool shouldVisit(FunctionDefinition const& _function) const;
-	void pushBlock(ASTNode const* _node);
-	void popBlock();
+	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block);
 	//@}
 
 	/// Sort helpers.
@@ -105,9 +98,8 @@ private:
 	smt::Expression error();
 	smt::Expression error(unsigned _idx);
 
-	/// Creates a block for the given _node or increases its SSA index
-	/// if the block already exists which in practice creates a new function.
-	void createBlock(ASTNode const* _node, std::string const& _prefix = "");
+	/// Creates a block for the given _node.
+	std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(ASTNode const* _node, std::string const& _prefix = "");
 
 	/// Creates a new error block to be used by an assertion.
 	/// Also registers the predicate.
@@ -129,7 +121,9 @@ private:
 	/// @returns the predicate name for a given node.
 	std::string predicateName(ASTNode const* _node);
 	/// @returns a predicate application over the current scoped variables.
-	smt::Expression predicate(ASTNode const* _node);
+	smt::Expression predicate(smt::SymbolicFunctionVariable const& _block);
+	/// @returns a predicate application over @param _arguments.
+	smt::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const& _arguments);
 	//@}
 
 	/// Solver related.
@@ -140,6 +134,13 @@ private:
 	bool query(smt::Expression const& _query, langutil::SourceLocation const& _location);
 	//@}
 
+	/// Misc.
+	//@{
+	/// Returns a prefix to be used in a new unique block name
+	/// and increases the block counter.
+	std::string uniquePrefix();
+	//@}
+
 	/// Predicates.
 	//@{
 	/// Constructor predicate.
@@ -153,9 +154,6 @@ private:
 	/// Artificial Error predicate.
 	/// Single error block for all assertions.
 	std::unique_ptr<smt::SymbolicVariable> m_errorPredicate;
-
-	/// Maps AST nodes to their predicates.
-	std::unordered_map<ASTNode const*, std::shared_ptr<smt::SymbolicVariable>> m_predicates;
 	//@}
 
 	/// Variables.
@@ -166,9 +164,6 @@ private:
 	/// State variables.
 	/// Used to create all predicates.
 	std::vector<VariableDeclaration const*> m_stateVariables;
-
-	/// Input sorts for AST nodes.
-	std::map<ASTNode const*, smt::SortPointer> m_nodeSorts;
 	//@}
 
 	/// Verification targets.
@@ -183,21 +178,19 @@ private:
 	//@{
 	FunctionDefinition const* m_currentFunction = nullptr;
 
-	/// Number of basic blocks created for the body of the current function.
-	unsigned m_functionBlocks = 0;
-	/// The current control flow path.
-	std::vector<smt::Expression> m_path;
+	/// The current block.
+	smt::Expression m_currentBlock = smt::Expression(true);
+
+	/// Counter to generate unique block names.
+	unsigned m_blockCounter = 0;
+
 	/// 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;
+	smt::SymbolicFunctionVariable const* m_breakDest = nullptr;
 	/// Block where a loop continue should go to.
-	ASTNode const* m_continueDest;
+	smt::SymbolicFunctionVariable const* m_continueDest = nullptr;
 	//@}
 
 	/// CHC solver.

test/libsolidity/smtCheckerTests/loops/do_while_break.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint x;
+		do {
+			break;
+			x = 1;
+		} while (x == 0);
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (104-109): Unreachable code.
+// Warning: (122-128): Unreachable code.

test/libsolidity/smtCheckerTests/loops/do_while_break_2.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint a = 0;
+		while (true) {
+			do {
+				break;
+				a = 2;
+			} while (true);
+			a = 1;
+			break;
+		}
+		assert(a == 1);
+	}
+}
+// ----
+// Warning: (128-133): Unreachable code.
+// Warning: (147-151): Unreachable code.

test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint a = 0;
+		while (true) {
+			do {
+				break;
+				a = 2;
+			} while (true);
+			a = 1;
+			break;
+		}
+		assert(a == 2);
+	}
+}
+// ----
+// Warning: (128-133): Unreachable code.
+// Warning: (147-151): Unreachable code.
+// Warning: (180-194): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint x;
+		do {
+			break;
+			x = 1;
+		} while (x == 0);
+		assert(x == 1);
+	}
+}
+// ----
+// Warning: (104-109): Unreachable code.
+// Warning: (122-128): Unreachable code.
+// Warning: (133-147): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/do_while_continue.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint x;
+		do {
+			continue;
+			x = 1;
+		} while (x == 0);
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (107-112): Unreachable code.

test/libsolidity/smtCheckerTests/loops/for_1_break.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 10);
+		for (; x < 10; ) {
+			if (b)
+				++x;
+			else {
+				x = 20;
+				break;
+			}
+		}
+		assert(x >= 10);
+	}
+}

test/libsolidity/smtCheckerTests/loops/for_1_break_fail.sol

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

test/libsolidity/smtCheckerTests/loops/for_1_continue.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 10);
+		for (; x < 10; ++x) {
+			if (b) {
+				x = 20;
+				continue;
+			}
+		}
+		assert(x > 0);
+	}
+}

test/libsolidity/smtCheckerTests/loops/for_1_continue_fail.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 10);
+		for (; x < 10; ) {
+			if (b) {
+				x = 20;
+				continue;
+			}
+			++x;
+		}
+		assert(x > 15);
+	}
+}
+// ----
+// Warning: (185-199): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_break_direct.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		for (x = 0; x < 10; ++x)
+			break;
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (102-105): Unreachable code.

test/libsolidity/smtCheckerTests/loops/while_1_break.sol

@@ -12,10 +12,6 @@ contract C
 				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_continue.sol

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

test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol

@@ -8,9 +8,9 @@ contract C
 			if (b) {
 				x = 15;
 				continue;
+				x = 200;
 			}
-			else
-				x = 20;
+			x = 20;
 
 		}
 		// Fails due to the if.
@@ -18,4 +18,5 @@ contract C
 	}
 }
 // ----
-// Warning: (223-238): Assertion violation happens here
+// Warning: (169-176): Unreachable code.
+// Warning: (227-242): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_2_break.sol

@@ -9,11 +9,8 @@ contract C
 			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_break_direct.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		x = 0;
+		while (x < 10)
+			break;
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (98-104): Condition is always true.

test/libsolidity/smtCheckerTests/loops/while_nested_break.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, uint y, bool b, bool c) public pure {
+		require(x < 10);
+		while (x < 10) {
+			if (b) {
+				++x;
+				if (x == 10)
+					x = 15;
+			}
+			else {
+				require(y < 10);
+				while (y < 10) {
+					if (c)
+						++y;
+					else {
+						y = 20;
+						break;
+					}
+				}
+				assert(y >= 10);
+				x = 15;
+				break;
+			}
+		}
+		assert(x >= 15);
+	}
+}

test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol

@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, uint y, bool b, bool c) public pure {
+		require(x < 10);
+		while (x < 10) {
+			if (b) {
+				++x;
+				if (x == 10)
+					x = 15;
+			}
+			else {
+				require(y < 10);
+				while (y < 10) {
+					if (c)
+						++y;
+					else {
+						y = 20;
+						break;
+					}
+				}
+				assert(y >= 15);
+				x = 15;
+				break;
+			}
+		}
+		assert(x >= 20);
+	}
+}
+// ----
+// Warning: (329-344): Assertion violation happens here
+// Warning: (380-395): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_nested_continue.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, uint y, bool b, bool c) public pure {
+		require(x < 10);
+		while (x < 10) {
+			if (b) {
+				x = 20;
+				continue;
+			}
+			else {
+				require(y < 10);
+				while (y < 10) {
+					if (c) {
+						y = 20;
+						continue;
+					}
+					y = 15;
+					break;
+				}
+				assert(y >= 15);
+				x = y;
+			}
+		}
+		assert(x >= 15);
+	}
+}

test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, uint y, bool b, bool c) public pure {
+		require(x < 10);
+		while (x < 10) {
+			if (b) {
+				x = 15;
+				continue;
+			}
+			else {
+				require(y < 10);
+				while (y < 10) {
+					if (c) {
+						y = 20;
+						continue;
+					}
+					y = 15;
+					break;
+				}
+				assert(y >= 20);
+				x = y;
+			}
+		}
+		assert(x >= 20);
+	}
+}
+// ----
+// Warning: (323-338): Assertion violation happens here
+// Warning: (362-377): Assertion violation happens here