Merge pull request #6994 from ethereum/smt_refactor_targets

[SMTChecker] Delay all checks

libsolidity/formal/SMTChecker.cpp

@@ -111,11 +111,11 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 	{
 		m_interface->reset();
 		m_context.reset();
+		m_context.pushSolver();
 		m_pathConditions.clear();
-		m_callStack.clear();
 		pushCallStack({&_function, nullptr});
 		m_uninterpretedTerms.clear();
-		m_overflowTargets.clear();
+		m_verificationTargets.clear();
 		resetStateVariables();
 		initializeLocalVariables(_function);
 		m_loopExecutionHappened = false;
@@ -186,18 +186,14 @@ bool SMTChecker::visit(PlaceholderStatement const&)
 
 void SMTChecker::endVisit(FunctionDefinition const&)
 {
-	m_callStack.pop_back();
+	popCallStack();
 	solAssert(m_modifierDepthStack.back() == -1, "");
 	m_modifierDepthStack.pop_back();
-	// If _function was visited from a function call we don't remove
-	// the local variables just yet, since we might need them for
-	// future calls.
-	// Otherwise we remove any local variables from the context and
-	// keep the state variables.
 	if (m_callStack.empty())
 	{
-		checkUnderOverflow();
+		checkVerificationTargets(m_context.assertions());
-		solAssert(m_callStack.empty(), "");
+		m_verificationTargets.clear();
+		m_context.popSolver();
 	}
 }
 
@@ -217,7 +213,11 @@ bool SMTChecker::visit(IfStatement const& _node)
 	// We ignore called functions here because they have
 	// specific input values.
 	if (isRootFunction())
-		checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
+		addVerificationTarget(
+			VerificationTarget::Type::ConstantCondition,
+			expr(_node.condition()),
+			&_node.condition()
+		);
 
 	auto indicesEndTrue = visitBranch(&_node.trueStatement(), expr(_node.condition()));
 	auto touchedVars = touchedVariables(_node.trueStatement());
@@ -256,13 +256,21 @@ bool SMTChecker::visit(WhileStatement const& _node)
 		// TODO the assertions generated in the body should still be active in the condition
 		_node.condition().accept(*this);
 		if (isRootFunction())
-			checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
+			addVerificationTarget(
+				VerificationTarget::Type::ConstantCondition,
+				expr(_node.condition()),
+				&_node.condition()
+			);
 	}
 	else
 	{
 		_node.condition().accept(*this);
 		if (isRootFunction())
-			checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
+			addVerificationTarget(
+				VerificationTarget::Type::ConstantCondition,
+				expr(_node.condition()),
+				&_node.condition()
+			);
 
 		indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition()));
 	}
@@ -302,16 +310,20 @@ bool SMTChecker::visit(ForStatement const& _node)
 	{
 		_node.condition()->accept(*this);
 		if (isRootFunction())
-			checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
+			addVerificationTarget(
+				VerificationTarget::Type::ConstantCondition,
+				expr(*_node.condition()),
+				_node.condition()
+			);
 	}
 
-	m_interface->push();
+	m_context.pushSolver();
 	if (_node.condition())
-		m_interface->addAssertion(expr(*_node.condition()));
+		m_context.addAssertion(expr(*_node.condition()));
 	_node.body().accept(*this);
 	if (_node.loopExpression())
 		_node.loopExpression()->accept(*this);
-	m_interface->pop();
+	m_context.popSolver();
 
 	auto indicesAfterLoop = copyVariableIndices();
 	// We reset the execution to before the loop
@@ -458,62 +470,6 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
 	}
 }
 
-void SMTChecker::addOverflowTarget(
-	OverflowTarget::Type _type,
-	TypePointer _intType,
-	smt::Expression _value,
-	SourceLocation const& _location
-)
-{
-	m_overflowTargets.emplace_back(
-		_type,
-		std::move(_intType),
-		std::move(_value),
-		currentPathConditions(),
-		_location,
-		m_callStack
-	);
-}
-
-void SMTChecker::checkUnderOverflow()
-{
-	for (auto& target: m_overflowTargets)
-	{
-		swap(m_callStack, target.callStack);
-		if (target.type != OverflowTarget::Type::Overflow)
-			checkUnderflow(target);
-		if (target.type != OverflowTarget::Type::Underflow)
-			checkOverflow(target);
-		swap(m_callStack, target.callStack);
-	}
-}
-
-void SMTChecker::checkUnderflow(OverflowTarget& _target)
-{
-	solAssert(_target.type != OverflowTarget::Type::Overflow, "");
-	auto intType = dynamic_cast<IntegerType const*>(_target.intType);
-	checkCondition(
-		_target.path && _target.value < smt::minValue(*intType),
-		_target.location,
-		"Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")",
-		"<result>",
-		&_target.value
-	);
-}
-
-void SMTChecker::checkOverflow(OverflowTarget& _target)
-{
-	solAssert(_target.type != OverflowTarget::Type::Underflow, "");
-	auto intType = dynamic_cast<IntegerType const*>(_target.intType);
-	checkCondition(
-		_target.path && _target.value > smt::maxValue(*intType),
-		_target.location,
-		"Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")",
-		"<result>",
-		&_target.value
-	);
-}
-
 void SMTChecker::endVisit(UnaryOperation const& _op)
 {
 	if (_op.annotation().type->category() == Type::Category::RationalNumber)
@@ -555,11 +511,10 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 				"Assertion checker does not yet implement such increments / decrements."
 			);
 
-		addOverflowTarget(
+		addVerificationTarget(
-			_op.getOperator() == Token::Inc ? OverflowTarget::Type::Overflow : OverflowTarget::Type::Underflow,
+			_op.getOperator() == Token::Inc ? VerificationTarget::Type::Overflow : VerificationTarget::Type::Underflow,
-			_op.annotation().type,
 			expr(_op),
-			_op.location()
+			&_op
 		);
 
 		break;
@@ -568,11 +523,10 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 	{
 		defineExpr(_op, 0 - expr(_op.subExpression()));
 		if (_op.annotation().type->category() == Type::Category::Integer)
-			addOverflowTarget(
+			addVerificationTarget(
-				OverflowTarget::Type::All,
+				VerificationTarget::Type::UnderOverflow,
-				_op.annotation().type,
 				expr(_op),
-				_op.location()
+				&_op
 			);
 		break;
 	}
@@ -705,7 +659,12 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 
 		smt::Expression thisBalance = m_context.balance();
 		setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_interface);
-		checkCondition(thisBalance < expr(*value), _funCall.location(), "Insufficient funds", "address(this).balance", &thisBalance);
+
+		addVerificationTarget(
+			VerificationTarget::Type::Balance,
+			thisBalance < expr(*value),
+			&_funCall
+		);
 
 		m_context.transfer(m_context.thisAddress(), expr(address), expr(*value));
 		break;
@@ -723,7 +682,11 @@ void SMTChecker::visitAssert(FunctionCall const& _funCall)
 	auto const& args = _funCall.arguments();
 	solAssert(args.size() == 1, "");
 	solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
-	checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
+	addVerificationTarget(
+		VerificationTarget::Type::Assert,
+		m_context.expression(*args.front())->currentValue(),
+		&_funCall
+	);
 	addPathImpliedExpression(expr(*args[0]));
 }
 
@@ -733,7 +696,11 @@ void SMTChecker::visitRequire(FunctionCall const& _funCall)
 	solAssert(args.size() == 1, "");
 	solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
 	if (isRootFunction())
-		checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
+		addVerificationTarget(
+			VerificationTarget::Type::ConstantCondition,
+			m_context.expression(*args.front())->currentValue(),
+			args.front().get()
+		);
 	addPathImpliedExpression(expr(*args[0]));
 }
 
@@ -748,7 +715,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 	// We set the current value to unknown anyway to add type constraints.
 	m_context.setUnknownValue(*symbolicVar);
 	if (index > 0)
-		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
+		m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
 void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
@@ -947,10 +914,10 @@ void SMTChecker::endVisit(Return const& _return)
 			solAssert(components.size() == returnParams.size(), "");
 			for (unsigned i = 0; i < returnParams.size(); ++i)
 				if (components.at(i))
-					m_interface->addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i)));
+					m_context.addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i)));
 		}
 		else if (returnParams.size() == 1)
-			m_interface->addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
+			m_context.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
 	}
 }
 
@@ -1091,7 +1058,7 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 			expr(*indexAccess.indexExpression()),
 			_rightHandSide
 		);
-		m_interface->addAssertion(m_context.newValue(*varDecl) == store);
+		m_context.addAssertion(m_context.newValue(*varDecl) == store);
 		// Update the SMT select value after the assignment,
 		// necessary for sound models.
 		defineExpr(indexAccess, smt::Expression::select(
@@ -1173,7 +1140,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 				expr(_op.leftExpression()),
 				expr(_op.rightExpression()),
 				_op.annotation().commonType,
-				_op.location()
+				_op
 			));
 			break;
 		}
@@ -1196,7 +1163,7 @@ smt::Expression SMTChecker::arithmeticOperation(
 	smt::Expression const& _left,
 	smt::Expression const& _right,
 	TypePointer const& _commonType,
-	langutil::SourceLocation const& _location
+	Expression const& _expression
 )
 {
 	static set<Token> validOperators{
@@ -1221,15 +1188,18 @@ smt::Expression SMTChecker::arithmeticOperation(
 
 	if (_op == Token::Div || _op == Token::Mod)
 	{
-		checkCondition(_right == 0, _location, "Division by zero", "<result>", &_right);
+		addVerificationTarget(
-		m_interface->addAssertion(_right != 0);
+			VerificationTarget::Type::DivByZero,
+			_right,
+			&_expression
+		);
+		m_context.addAssertion(_right != 0);
 	}
 
-	addOverflowTarget(
+	addVerificationTarget(
-		OverflowTarget::Type::All,
+		VerificationTarget::Type::UnderOverflow,
-		_commonType,
 		value,
-		_location
+		&_expression
 	);
 
 	smt::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
@@ -1386,7 +1356,7 @@ smt::Expression SMTChecker::compoundAssignment(Assignment const& _assignment)
 		decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
 		expr(_assignment.rightHandSide()),
 		_assignment.annotation().type,
-		_assignment.location()
+		_assignment
 	);
 }
 
@@ -1400,7 +1370,7 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio
 	TypePointer type = _variable.type();
 	if (type->category() == Type::Category::Mapping)
 		arrayAssignment();
-	m_interface->addAssertion(m_context.newValue(_variable) == _value);
+	m_context.addAssertion(m_context.newValue(_variable) == _value);
 }
 
 SMTChecker::VariableIndices SMTChecker::visitBranch(ASTNode const* _statement, smt::Expression _condition)
@@ -1421,32 +1391,164 @@ SMTChecker::VariableIndices SMTChecker::visitBranch(ASTNode const* _statement, s
 	return indicesAfterBranch;
 }
 
-void SMTChecker::checkCondition(
+/// Verification targets.
-	smt::Expression _condition,
+
-	SourceLocation const& _location,
+void SMTChecker::checkVerificationTargets(smt::Expression const& _constraints)
-	string const& _description,
+{
-	string const& _additionalValueName,
+	for (auto& target: m_verificationTargets)
-	smt::Expression const* _additionalValue
+		checkVerificationTarget(target, _constraints);
+}
+
+void SMTChecker::checkVerificationTarget(VerificationTarget& _target, smt::Expression const& _constraints)
+{
+	switch (_target.type)
+	{
+		case VerificationTarget::Type::ConstantCondition:
+			checkConstantCondition(_target);
+			break;
+		case VerificationTarget::Type::Underflow:
+			checkUnderflow(_target, _constraints);
+			break;
+		case VerificationTarget::Type::Overflow:
+			checkOverflow(_target, _constraints);
+			break;
+		case VerificationTarget::Type::UnderOverflow:
+			checkUnderflow(_target, _constraints);
+			checkOverflow(_target, _constraints);
+			break;
+		case VerificationTarget::Type::DivByZero:
+			checkDivByZero(_target);
+			break;
+		case VerificationTarget::Type::Balance:
+			checkBalance(_target);
+			break;
+		case VerificationTarget::Type::Assert:
+			checkAssert(_target);
+			break;
+		default:
+			solAssert(false, "");
+	}
+}
+
+void SMTChecker::checkConstantCondition(VerificationTarget& _target)
+{
+	checkBooleanNotConstant(
+		*_target.expression,
+		_target.constraints,
+		_target.value,
+		_target.callStack,
+		"Condition is always $VALUE."
+	);
+}
+
+void SMTChecker::checkUnderflow(VerificationTarget& _target, smt::Expression const& _constraints)
+{
+	solAssert(
+		_target.type == VerificationTarget::Type::Underflow ||
+			_target.type == VerificationTarget::Type::UnderOverflow,
+		""
+	);
+	auto intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
+	solAssert(intType, "");
+	checkCondition(
+		_target.constraints && _constraints && _target.value < smt::minValue(*intType),
+		_target.callStack,
+		_target.modelExpressions,
+		_target.expression->location(),
+		"Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")",
+		"<result>",
+		&_target.value
+	);
+}
+
+void SMTChecker::checkOverflow(VerificationTarget& _target, smt::Expression const& _constraints)
+{
+	solAssert(
+		_target.type == VerificationTarget::Type::Overflow ||
+			_target.type == VerificationTarget::Type::UnderOverflow,
+		""
+	);
+	auto intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
+	solAssert(intType, "");
+	checkCondition(
+		_target.constraints && _constraints && _target.value > smt::maxValue(*intType),
+		_target.callStack,
+		_target.modelExpressions,
+		_target.expression->location(),
+		"Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")",
+		"<result>",
+		&_target.value
+	);
+}
+
+void SMTChecker::checkDivByZero(VerificationTarget& _target)
+{
+	solAssert(_target.type == VerificationTarget::Type::DivByZero, "");
+	checkCondition(
+		_target.constraints && (_target.value == 0),
+		_target.callStack,
+		_target.modelExpressions,
+		_target.expression->location(),
+		"Division by zero",
+		"<result>",
+		&_target.value
+	);
+}
+
+void SMTChecker::checkBalance(VerificationTarget& _target)
+{
+	solAssert(_target.type == VerificationTarget::Type::Balance, "");
+	checkCondition(
+		_target.constraints && _target.value,
+		_target.callStack,
+		_target.modelExpressions,
+		_target.expression->location(),
+		"Insufficient funds",
+		"address(this).balance"
+	);
+}
+
+void SMTChecker::checkAssert(VerificationTarget& _target)
+{
+	solAssert(_target.type == VerificationTarget::Type::Assert, "");
+	checkCondition(
+		_target.constraints && !_target.value,
+		_target.callStack,
+		_target.modelExpressions,
+		_target.expression->location(),
+		"Assertion violation"
+	);
+}
+
+void SMTChecker::addVerificationTarget(
+	VerificationTarget::Type _type,
+	smt::Expression const& _value,
+	Expression const* _expression
 )
 {
-	m_interface->push();
+	VerificationTarget target{
-	addPathConjoinedExpression(_condition);
+		_type,
+		_value,
+		currentPathConditions() && m_context.assertions(),
+		_expression,
+		m_callStack,
+		modelExpressions()
+	};
+	if (_type == VerificationTarget::Type::ConstantCondition)
+		checkVerificationTarget(target);
+	else
+		m_verificationTargets.emplace_back(move(target));
+}
 
+pair<vector<smt::Expression>, vector<string>> SMTChecker::modelExpressions()
+{
 	vector<smt::Expression> expressionsToEvaluate;
 	vector<string> expressionNames;
-	if (m_callStack.size())
-	{
-		solAssert(m_scanner, "");
-		if (_additionalValue)
-		{
-			expressionsToEvaluate.emplace_back(*_additionalValue);
-			expressionNames.push_back(_additionalValueName);
-		}
 	for (auto const& var: m_context.variables())
 	{
 		if (var.first->type()->isValueType())
 		{
-				expressionsToEvaluate.emplace_back(currentValue(*var.first));
+			expressionsToEvaluate.emplace_back(m_context.variable(*var.first)->currentValue());
 			expressionNames.push_back(var.first->name());
 		}
 	}
@@ -1462,6 +1564,7 @@ void SMTChecker::checkCondition(
 			expressionNames.push_back(var.first);
 		}
 	}
+	solAssert(m_scanner, "");
 	for (auto const& uf: m_uninterpretedTerms)
 	{
 		if (uf->annotation().type->isValueType())
@@ -1470,6 +1573,31 @@ void SMTChecker::checkCondition(
 			expressionNames.push_back(m_scanner->sourceAt(uf->location()));
 		}
 	}
+
+	return {expressionsToEvaluate, expressionNames};
+}
+
+void SMTChecker::checkCondition(
+	smt::Expression const& _condition,
+	vector<CallStackEntry> const& callStack,
+	pair<vector<smt::Expression>, vector<string>> const& _modelExpressions,
+	SourceLocation const& _location,
+	string const& _description,
+	string const& _additionalValueName,
+	smt::Expression const* _additionalValue
+)
+{
+	m_interface->push();
+	m_interface->addAssertion(_condition);
+
+	vector<smt::Expression> expressionsToEvaluate;
+	vector<string> expressionNames;
+	tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
+	if (callStack.size())
+		if (_additionalValue)
+		{
+			expressionsToEvaluate.emplace_back(*_additionalValue);
+			expressionNames.push_back(_additionalValueName);
 		}
 	smt::CheckResult result;
 	vector<string> values;
@@ -1502,7 +1630,7 @@ void SMTChecker::checkCondition(
 	{
 		std::ostringstream message;
 		message << _description << " happens here";
-		if (m_callStack.size())
+		if (callStack.size())
 		{
 			std::ostringstream modelMessage;
 			modelMessage << "  for:\n";
@@ -1518,7 +1646,7 @@ void SMTChecker::checkCondition(
 				_location,
 				message.str(),
 				SecondarySourceLocation().append(modelMessage.str(), SourceLocation{})
-				.append(currentCallStack())
+				.append(callStackMessage(callStack))
 				.append(move(secondaryLocation))
 			);
 		}
@@ -1541,22 +1669,29 @@ void SMTChecker::checkCondition(
 		m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
 		break;
 	}
+
 	m_interface->pop();
 }
 
-void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description)
+void SMTChecker::checkBooleanNotConstant(
+	Expression const& _condition,
+	smt::Expression const& _constraints,
+	smt::Expression const& _value,
+	vector<CallStackEntry> const& _callStack,
+	string const& _description
+)
 {
 	// Do not check for const-ness if this is a constant.
 	if (dynamic_cast<Literal const*>(&_condition))
 		return;
 
 	m_interface->push();
-	addPathConjoinedExpression(expr(_condition));
+	m_interface->addAssertion(_constraints && _value);
 	auto positiveResult = checkSatisfiable();
 	m_interface->pop();
 
 	m_interface->push();
-	addPathConjoinedExpression(!expr(_condition));
+	m_interface->addAssertion(_constraints && !_value);
 	auto negatedResult = checkSatisfiable();
 	m_interface->pop();
 
@@ -1573,7 +1708,7 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 		// can't do anything.
 	}
 	else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
-		m_errorReporter.warning(_condition.location(), "Condition unreachable.", currentCallStack());
+		m_errorReporter.warning(_condition.location(), "Condition unreachable.", callStackMessage(_callStack));
 	else
 	{
 		string value;
@@ -1591,7 +1726,7 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 		m_errorReporter.warning(
 			_condition.location(),
 			boost::algorithm::replace_all_copy(_description, "$VALUE", value),
-			currentCallStack()
+			callStackMessage(_callStack)
 		);
 	}
 }
@@ -1639,7 +1774,7 @@ void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _fu
 	for (unsigned i = 0; i < funParams.size(); ++i)
 		if (createVariable(*funParams[i]))
 		{
-			m_interface->addAssertion(_callArgs[i] == m_context.newValue(*funParams[i]));
+			m_context.addAssertion(_callArgs[i] == m_context.newValue(*funParams[i]));
 			if (funParams[i]->annotation().type->category() == Type::Category::Mapping)
 				m_arrayAssignmentHappened = true;
 		}
@@ -1705,7 +1840,7 @@ void SMTChecker::mergeVariables(set<VariableDeclaration const*> const& _variable
 		int trueIndex = _indicesEndTrue.at(decl);
 		int falseIndex = _indicesEndFalse.at(decl);
 		solAssert(trueIndex != falseIndex, "");
-		m_interface->addAssertion(m_context.newValue(*decl) == smt::Expression::ite(
+		m_context.addAssertion(m_context.newValue(*decl) == smt::Expression::ite(
 			_condition,
 			valueAtIndex(*decl, trueIndex),
 			valueAtIndex(*decl, falseIndex))
@@ -1765,7 +1900,7 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
 {
 	createExpr(_e);
 	solAssert(smt::smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
-	m_interface->addAssertion(expr(_e) == _value);
+	m_context.addAssertion(expr(_e) == _value);
 }
 
 void SMTChecker::popPathCondition()
@@ -1786,16 +1921,16 @@ smt::Expression SMTChecker::currentPathConditions()
 	return m_pathConditions.back();
 }
 
-SecondarySourceLocation SMTChecker::currentCallStack()
+SecondarySourceLocation SMTChecker::callStackMessage(vector<CallStackEntry> const& _callStack)
 {
 	SecondarySourceLocation callStackLocation;
-	solAssert(!m_callStack.empty(), "");
+	solAssert(!_callStack.empty(), "");
 	callStackLocation.append("Callstack: ", SourceLocation());
-	for (auto const& call: m_callStack | boost::adaptors::reversed)
+	for (auto const& call: _callStack | boost::adaptors::reversed)
 		if (call.second)
 			callStackLocation.append("", call.second->location());
 	// The first function in the tx has no FunctionCall.
-	solAssert(m_callStack.front().second == nullptr, "");
+	solAssert(_callStack.front().second == nullptr, "");
 	return callStackLocation;
 }
 
@@ -1814,12 +1949,12 @@ void SMTChecker::pushCallStack(CallStackEntry _entry)
 
 void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
 {
-	m_interface->addAssertion(currentPathConditions() && _e);
+	m_context.addAssertion(currentPathConditions() && _e);
 }
 
 void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
 {
-	m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
+	m_context.addAssertion(smt::Expression::implies(currentPathConditions(), _e));
 }
 
 bool SMTChecker::isRootFunction()

libsolidity/formal/SMTChecker.h

@@ -103,7 +103,7 @@ private:
 		smt::Expression const& _left,
 		smt::Expression const& _right,
 		TypePointer const& _commonType,
-		langutil::SourceLocation const& _location
+		Expression const& _expression
 	);
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
@@ -163,57 +163,68 @@ private:
 	VariableIndices visitBranch(ASTNode const* _statement, smt::Expression const* _condition = nullptr);
 	VariableIndices visitBranch(ASTNode const* _statement, smt::Expression _condition);
 
+	using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
+
+	/// Verification targets.
+	//@{
+	struct VerificationTarget
+	{
+		enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type;
+		smt::Expression value;
+		smt::Expression constraints;
+		Expression const* expression;
+		std::vector<CallStackEntry> callStack;
+		std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions;
+	};
+
+	void checkVerificationTargets(smt::Expression const& _constraints);
+	void checkVerificationTarget(VerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true));
+	void checkConstantCondition(VerificationTarget& _target);
+	void checkUnderflow(VerificationTarget& _target, smt::Expression const& _constraints);
+	void checkOverflow(VerificationTarget& _target, smt::Expression const& _constraints);
+	void checkDivByZero(VerificationTarget& _target);
+	void checkBalance(VerificationTarget& _target);
+	void checkAssert(VerificationTarget& _target);
+	void addVerificationTarget(
+		VerificationTarget::Type _type,
+		smt::Expression const& _value,
+		Expression const* _expression
+	);
+	//@}
+
+	/// Solver related.
+	//@{
+
+	std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions();
 	/// Check that a condition can be satisfied.
 	void checkCondition(
-		smt::Expression _condition,
+		smt::Expression const& _condition,
+		std::vector<CallStackEntry> const& callStack,
+		std::pair<std::vector<smt::Expression>, std::vector<std::string>> const& _modelExpressions,
 		langutil::SourceLocation const& _location,
 		std::string const& _description,
 		std::string const& _additionalValueName = "",
 		smt::Expression const* _additionalValue = nullptr
 	);
-	/// Checks that a boolean condition is not constant. Do not warn if the expression
+	/// Checks whether a Boolean condition is constant.
-	/// is a literal constant.
+	/// Do not warn if the expression is a literal constant.
+	/// @param _condition the Solidity expression, used to check whether it is a Literal and for location.
+	/// @param _constraints the program constraints, including control-flow.
+	/// @param _value the Boolean term to be checked.
+	/// @param _callStack the callStack to be shown with the model if applicable.
 	/// @param _description the warning string, $VALUE will be replaced by the constant value.
 	void checkBooleanNotConstant(
 		Expression const& _condition,
+		smt::Expression const& _constraints,
+		smt::Expression const& _value,
+		std::vector<CallStackEntry> const& _callStack,
 		std::string const& _description
 	);
-
-	using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
-
-	struct OverflowTarget
-	{
-		enum class Type { Underflow, Overflow, All } type;
-		TypePointer intType;
-		smt::Expression value;
-		smt::Expression path;
-		langutil::SourceLocation const& location;
-		std::vector<CallStackEntry> callStack;
-
-		OverflowTarget(Type _type, TypePointer _intType, smt::Expression _value, smt::Expression _path, langutil::SourceLocation const& _location, std::vector<CallStackEntry> _callStack):
-			type(_type),
-			intType(_intType),
-			value(_value),
-			path(_path),
-			location(_location),
-			callStack(move(_callStack))
-		{
-			solAssert(dynamic_cast<IntegerType const*>(intType), "");
-		}
-	};
-
-	/// Checks that the value is in the range given by the type.
-	void checkUnderflow(OverflowTarget& _target);
-	void checkOverflow(OverflowTarget& _target);
-	/// Calls the functions above for all elements in m_overflowTargets accordingly.
-	void checkUnderOverflow();
-	/// Adds an overflow target for lazy check at the end of the function.
-	void addOverflowTarget(OverflowTarget::Type _type, TypePointer _intType, smt::Expression _value, langutil::SourceLocation const& _location);
-
 	std::pair<smt::CheckResult, std::vector<std::string>>
 	checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
 
 	smt::CheckResult checkSatisfiable();
+	//@}
 
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smt::Expression> const& _callArgs);
@@ -248,8 +259,8 @@ private:
 	void popPathCondition();
 	/// Returns the conjunction of all path conditions or True if empty
 	smt::Expression currentPathConditions();
-	/// Returns the current callstack. Used for models.
+	/// @returns a human-readable call stack. Used for models.
-	langutil::SecondarySourceLocation currentCallStack();
+	langutil::SecondarySourceLocation callStackMessage(std::vector<CallStackEntry> const& _callStack);
 	/// Copies and pops the last called node.
 	CallStackEntry popCallStack();
 	/// Adds (_definition, _node) to the callstack.
@@ -300,7 +311,7 @@ private:
 	/// Returns true if _funDef was already visited.
 	bool visitedFunction(FunctionDefinition const* _funDef);
 
-	std::vector<OverflowTarget> m_overflowTargets;
+	std::vector<VerificationTarget> m_verificationTargets;
 
 	/// Depth of visit to modifiers.
 	/// When m_modifierDepth == #modifiers the function can be visited

test/libsolidity/smtCheckerTests/complex/MerkleProof.sol

@@ -38,4 +38,3 @@ library MerkleProof {
 // Warning: (988-1032): Assertion checker does not yet implement this type of function call.
 // Warning: (1175-1219): Assertion checker does not yet implement this type of function call.
 // Warning: (755-767): Assertion checker does not yet support this expression.
-// Warning: (769-772): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol

@@ -5,4 +5,4 @@ contract C
 	function f(bool x) public pure { require(x); for (;x;) {} }
 }
 // ----
-// Warning: (98-99): For loop condition is always true.
+// Warning: (98-99): Condition is always true.

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol

@@ -5,4 +5,4 @@ contract C
 	function f(bool x) public pure { require(x); while (x) {} }
 }
 // ----
-// Warning: (99-100): While loop condition is always true.
+// Warning: (99-100): Condition is always true.

test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol

@@ -12,5 +12,5 @@ contract C
 	}
 }
 // ----
-// Warning: (179-193): Assertion violation happens here
 // Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (179-193): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol

@@ -14,5 +14,5 @@ contract C
 	}
 }
 // ----
-// Warning: (269-282): Assertion violation happens here
 // 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_fail.sol

@@ -12,7 +12,5 @@ contract C
 	}
 }
 // ----
-// Warning: (189-203): Assertion violation happens here
-// Warning: (176-181): Underflow (resulting value less than 0) happens here
 // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (126-129): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (189-203): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -13,7 +13,5 @@ contract C
 	}
 }
 // ----
-// Warning: (244-257): Assertion violation happens here
-// Warning: (176-181): Underflow (resulting value less than 0) happens here
 // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (126-129): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (244-257): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol

@@ -7,4 +7,4 @@ contract C {
     }
 }
 // ----
-// Warning: (122-128): For loop condition is always true.
+// Warning: (122-128): Condition is always true.

test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol

@@ -10,4 +10,4 @@ contract C {
     }
 }
 // ----
-// Warning: (138-144): For loop condition is always true.
+// Warning: (138-144): Condition is always true.

test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol

@@ -7,4 +7,4 @@ contract C {
     }
 }
 // ----
-// Warning: (122-127): For loop condition is always false.
+// Warning: (122-127): Condition is always false.

test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol

@@ -19,8 +19,8 @@ contract C
 }
 // ----
 // Warning: (186-195): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (280-303): Assertion violation happens here
 // Warning: (317-333): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (414-431): Assertion violation happens here
 // Warning: (451-460): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (280-303): Assertion violation happens here
+// Warning: (414-431): Assertion violation happens here
 // Warning: (542-559): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_balance.sol

@@ -9,5 +9,5 @@ contract C
 }
 // ----
 // Warning: (96-102): Unused local variable.
-// Warning: (131-160): Assertion violation happens here
 // Warning: (105-127): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (131-160): Assertion violation happens here

test/libsolidity/smtCheckerTestsJSON/multi.json

@@ -3,9 +3,9 @@
 	{
 		"smtlib2responses":
 		{
-			"0x0a0e9583fd983e7ce82e96bd95f7c0eb831e2dd3ce3364035e30bf1d22823b34": "sat\n((|EVALEXPR_0| 1))\n",
+			"0x5c4a8addfb72cd6eedbd143f0d402faa2833363b9c8c3f4ed5d9b01ff8fdeee0": "unsat\n",
-			"0x15353582486fb1dac47801edbb366ae40a59ef0191ebe7c09ca32bdabecc2f1a": "unsat\n",
+			"0xf04f3df4fcb1dcab2a20ff50621679f88608a48addeedfd3792fd652e7115d2f": "sat\n((|EVALEXPR_0| 0))\n",
-			"0xa66d08de30c873ca7d0e7e9e426f278640e0ee463a1aed2e4e80baee916b6869": "sat\n((|EVALEXPR_0| 0))\n"
+			"0xf7f1fe2ee1dced3b4ee90b7f1babcfb9ca520344b39c592f4a378761775705bd": "sat\n((|EVALEXPR_0| 1))\n"
 		}
 	}
 }

test/libsolidity/smtCheckerTestsJSON/simple.json

@@ -3,7 +3,7 @@
 	{
 		"smtlib2responses":
 		{
-			"0xa66d08de30c873ca7d0e7e9e426f278640e0ee463a1aed2e4e80baee916b6869": "sat\n((|EVALEXPR_0| 0))\n"
+			"0xf38a3b8e5fd03ea30ca7df1b566b1f76a5d6e0b8c46f58ff7bf576f537a4c366": "sat\n((|EVALEXPR_0| 0))\n"
 		}
 	}
 }