Merge pull request #10097 from ethereum/develop

Merge develop into breaking.

libsolidity/formal/BMC.cpp

@@ -716,6 +716,13 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression cons
 void BMC::checkDivByZero(BMCVerificationTarget& _target)
 {
 	solAssert(_target.type == VerificationTarget::Type::DivByZero, "");
+
+	if (
+		m_solvedTargets.count(_target.expression) &&
+		m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::DivByZero)
+	)
+		return;
+
 	checkCondition(
 		_target.constraints && (_target.value == 0),
 		_target.callStack,

libsolidity/formal/CHC.cpp

@@ -533,18 +533,9 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 
 void CHC::visitAddMulMod(FunctionCall const& _funCall)
 {
-	auto previousError = errorFlag().currentValue();
-	errorFlag().increaseIndex();
-
-	addVerificationTarget(
-		&_funCall,
-		VerificationTarget::Type::DivByZero,
-		errorFlag().currentValue()
-	);
-
 	solAssert(_funCall.arguments().at(2), "");
-	smtutil::Expression target = expr(*_funCall.arguments().at(2)) == 0 && errorFlag().currentValue() == newErrorId(_funCall);
-	m_context.addAssertion((errorFlag().currentValue() == previousError) || target);
+
+	addVerificationTarget(_funCall, VerificationTarget::Type::DivByZero, expr(*_funCall.arguments().at(2)) == 0);
 
 	SMTEncoder::visitAddMulMod(_funCall);
 }
@@ -643,13 +634,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 	auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
 
-	auto previousError = errorFlag().currentValue();
-	errorFlag().increaseIndex();
-
-	addVerificationTarget(&_arrayPop, VerificationTarget::Type::PopEmptyArray, errorFlag().currentValue());
-
-	smtutil::Expression target = (symbArray->length() <= 0) && (errorFlag().currentValue() == newErrorId(_arrayPop));
-	m_context.addAssertion((errorFlag().currentValue() == previousError) || target);
+	addVerificationTarget(_arrayPop, VerificationTarget::Type::PopEmptyArray, symbArray->length() <= 0);
 }
 
 pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
@@ -660,6 +645,9 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 	frontend::Expression const& _expression
 )
 {
+	if (_op == Token::Mod || _op == Token::Div)
+		addVerificationTarget(_expression, VerificationTarget::Type::DivByZero, _right == 0);
+
 	auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
 
 	IntegerType const* intType = nullptr;
@@ -673,46 +661,19 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 	if (_op == Token::Mod || (_op == Token::Div && !intType->isSigned()))
 		return values;
 
-	auto previousError = errorFlag().currentValue();
-	errorFlag().increaseIndex();
-
-	VerificationTarget::Type targetType;
-	unsigned errorId = newErrorId(_expression);
-
-	optional<smtutil::Expression> target;
 	if (_op == Token::Div)
-	{
-		targetType = VerificationTarget::Type::Overflow;
-		target = values.second > intType->maxValue() && errorFlag().currentValue() == errorId;
-	}
+		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	else if (intType->isSigned())
 	{
-		unsigned secondErrorId = newErrorId(_expression);
-		targetType = VerificationTarget::Type::UnderOverflow;
-		target = (values.second < intType->minValue() && errorFlag().currentValue() == errorId) ||
-			(values.second > intType->maxValue() && errorFlag().currentValue() == secondErrorId);
+		addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
+		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	}
 	else if (_op == Token::Sub)
-	{
-		targetType = VerificationTarget::Type::Underflow;
-		target = values.second < intType->minValue() && errorFlag().currentValue() == errorId;
-	}
+		addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
 	else if (_op == Token::Add || _op == Token::Mul)
-	{
-		targetType = VerificationTarget::Type::Overflow;
-		target = values.second > intType->maxValue() && errorFlag().currentValue() == errorId;
-	}
+		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	else
 		solAssert(false, "");
-
-	addVerificationTarget(
-		&_expression,
-		targetType,
-		errorFlag().currentValue()
-	);
-
-	m_context.addAssertion((errorFlag().currentValue() == previousError) || *target);
-
 	return values;
 }
 
@@ -1158,7 +1119,7 @@ void CHC::addVerificationTarget(
 	if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		return;
 
-	m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
+	m_verificationTargets[_scope].push_back(CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
 }
 
 void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId)
@@ -1175,6 +1136,18 @@ void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type
 	}
 }
 
+void CHC::addVerificationTarget(frontend::Expression const& _scope, VerificationTarget::Type _type, smtutil::Expression const& _target)
+{
+	auto previousError = errorFlag().currentValue();
+	errorFlag().increaseIndex();
+	addVerificationTarget(&_scope, _type, errorFlag().currentValue());
+
+	m_context.addAssertion(
+		errorFlag().currentValue() == previousError ||
+		(_target && errorFlag().currentValue() == newErrorId(_scope))
+	);
+}
+
 void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId)
 {
 	addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId);
@@ -1182,76 +1155,72 @@ void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression
 
 void CHC::checkVerificationTargets()
 {
-	for (auto const& [scope, target]: m_verificationTargets)
+	for (auto const& [scope, targets]: m_verificationTargets)
 	{
-		if (target.type == VerificationTarget::Type::Assert)
-			checkAssertTarget(scope, target);
-		else
+		for (size_t i = 0; i < targets.size(); ++i)
 		{
-			string satMsg;
-			string satMsgUnderflow;
-			string satMsgOverflow;
-			string unknownMsg;
-			ErrorId errorReporterId;
-			ErrorId underflowErrorId = 3944_error;
-			ErrorId overflowErrorId = 4984_error;
+			auto const& target = targets[i];
 
-			if (target.type == VerificationTarget::Type::PopEmptyArray)
-			{
-				solAssert(dynamic_cast<FunctionCall const*>(scope), "");
-				satMsg = "Empty array \"pop\" detected here.";
-				unknownMsg = "Empty array \"pop\" might happen here.";
-				errorReporterId = 2529_error;
-			}
-			else if (
-				target.type == VerificationTarget::Type::Underflow ||
-				target.type == VerificationTarget::Type::Overflow ||
-				target.type == VerificationTarget::Type::UnderOverflow
-			)
-			{
-				auto const* expr = dynamic_cast<Expression const*>(scope);
-				solAssert(expr, "");
-				auto const* intType = dynamic_cast<IntegerType const*>(expr->annotation().type);
-				if (!intType)
-					intType = TypeProvider::uint256();
-
-				satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ") happens here.";
-				satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ") happens here.";
-				if (target.type == VerificationTarget::Type::Underflow)
-				{
-					satMsg = satMsgUnderflow;
-					errorReporterId = underflowErrorId;
-				}
-				else if (target.type == VerificationTarget::Type::Overflow)
-				{
-					satMsg = satMsgOverflow;
-					errorReporterId = overflowErrorId;
-				}
-			}
-			else if (target.type == VerificationTarget::Type::DivByZero)
-			{
-				satMsg = "Division by zero happens here.";
-				errorReporterId = 4281_error;
-			}
-			else
-				solAssert(false, "");
-
-			auto it = m_errorIds.find(scope->id());
-			solAssert(it != m_errorIds.end(), "");
-			unsigned errorId = it->second;
-
-			if (target.type != VerificationTarget::Type::UnderOverflow)
-				checkAndReportTarget(scope, target, errorId, errorReporterId, satMsg, unknownMsg);
+			if (target.type == VerificationTarget::Type::Assert)
+				checkAssertTarget(scope, target);
 			else
 			{
-				auto specificTarget = target;
-				specificTarget.type = VerificationTarget::Type::Underflow;
-				checkAndReportTarget(scope, specificTarget, errorId, underflowErrorId, satMsgUnderflow, unknownMsg);
+				string satMsg;
+				string satMsgUnderflow;
+				string satMsgOverflow;
+				string unknownMsg;
+				ErrorId errorReporterId;
+				ErrorId underflowErrorId = 3944_error;
+				ErrorId overflowErrorId = 4984_error;
 
-				++it;
+				if (target.type == VerificationTarget::Type::PopEmptyArray)
+				{
+					solAssert(dynamic_cast<FunctionCall const*>(scope), "");
+					satMsg = "Empty array \"pop\" detected here.";
+					unknownMsg = "Empty array \"pop\" might happen here.";
+					errorReporterId = 2529_error;
+				}
+				else if (
+					target.type == VerificationTarget::Type::Underflow ||
+					target.type == VerificationTarget::Type::Overflow
+				)
+				{
+					auto const* expr = dynamic_cast<Expression const*>(scope);
+					solAssert(expr, "");
+					auto const* intType = dynamic_cast<IntegerType const*>(expr->annotation().type);
+					if (!intType)
+						intType = TypeProvider::uint256();
+
+					satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
+					satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
+					if (target.type == VerificationTarget::Type::Underflow)
+					{
+						satMsg = satMsgUnderflow + " happens here.";
+						unknownMsg = satMsgUnderflow + " might happen here.";
+						errorReporterId = underflowErrorId;
+					}
+					else if (target.type == VerificationTarget::Type::Overflow)
+					{
+						satMsg = satMsgOverflow + " happens here.";
+						unknownMsg = satMsgOverflow + " might happen here.";
+						errorReporterId = overflowErrorId;
+					}
+				}
+				else if (target.type == VerificationTarget::Type::DivByZero)
+				{
+					satMsg = "Division by zero happens here.";
+					unknownMsg = "Division by zero might happen here.";
+					errorReporterId = 4281_error;
+				}
+				else
+					solAssert(false, "");
+
+				auto it = m_errorIds.find(scope->id());
 				solAssert(it != m_errorIds.end(), "");
-				specificTarget.type = VerificationTarget::Type::Overflow;
-				checkAndReportTarget(scope, specificTarget, it->second, overflowErrorId, satMsgOverflow, unknownMsg);
+				solAssert(i < it->second.size(), "");
+				unsigned errorId = it->second[i];
+
+				checkAndReportTarget(scope, target, errorId, errorReporterId, satMsg, unknownMsg);
 			}
 		}
 	}
@@ -1265,9 +1234,10 @@ void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const&
 	{
 		auto it = m_errorIds.find(assertion->id());
 		solAssert(it != m_errorIds.end(), "");
-		unsigned errorId = it->second;
+		solAssert(!it->second.empty(), "");
+		unsigned errorId = it->second[0];
 
-		checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.");
+		checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.", "Assertion violation might happen here.");
 	}
 }
 
@@ -1461,7 +1431,7 @@ unsigned CHC::newErrorId(frontend::Expression const& _expr)
 	// because error id zero actually means no error in the CHC encoding.
 	if (errorId == 0)
 		errorId = m_context.newUniqueId();
-	m_errorIds.emplace(_expr.id(), errorId);
+	m_errorIds[_expr.id()].push_back(errorId);
 	return errorId;
 }
 

libsolidity/formal/CHC.h

@@ -183,6 +183,7 @@ private:
 
 	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
 	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId);
+	void addVerificationTarget(frontend::Expression const& _scope, VerificationTarget::Type _type, smtutil::Expression const& _target);
 	void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
 
 	void checkVerificationTargets();
@@ -277,7 +278,9 @@ private:
 		smtutil::Expression errorId;
 	};
 
-	std::map<ASTNode const*, CHCVerificationTarget, IdCompare> m_verificationTargets;
+	/// Verification targets corresponding to ASTNodes. There can be multiple targets for a single ASTNode,
+	/// e.g., divByZero and Overflow for signed division.
+	std::map<ASTNode const*, std::vector<CHCVerificationTarget>, IdCompare> m_verificationTargets;
 
 	/// Targets proven safe.
 	std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_safeTargets;
@@ -294,9 +297,8 @@ private:
 	std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions;
 
 	/// Maps ASTNode ids to error ids.
-	/// A multimap is used instead of map anticipating the UnderOverflow
-	/// target which has 2 error ids.
-	std::multimap<unsigned, unsigned> m_errorIds;
+	/// There can be multiple errorIds associated with a single ASTNode.
+	std::map<unsigned, std::vector<unsigned>> m_errorIds;
 
 	/// The current block.
 	smtutil::Expression m_currentBlock = smtutil::Expression(true);

libsolidity/formal/SMTEncoder.cpp

@@ -782,7 +782,6 @@ void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
 	auto x = expr(*args.at(0));
 	auto y = expr(*args.at(1));
 	auto k = expr(*args.at(2));
-	m_context.addAssertion(k != 0);
 	auto const& intType = dynamic_cast<IntegerType const&>(*_funCall.annotation().type);
 
 	if (kind == FunctionType::Kind::AddMod)
@@ -874,10 +873,8 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 	if (argSize == castSize)
 	{
 		// If sizes are the same, it's possible that the signs are different.
-		if (smt::isNumber(*funCallType))
+		if (smt::isNumber(*funCallType) && smt::isNumber(*argType))
 		{
-			solAssert(smt::isNumber(*argType), "");
-
 			// castIsSigned && !argIsSigned => might overflow if arg > castType.max
 			// !castIsSigned && argIsSigned => might underflow if arg < castType.min
 			// !castIsSigned && !argIsSigned => ok
@@ -1143,6 +1140,16 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		}
 		return false;
 	}
+	else if (
+		auto const* functionType = dynamic_cast<FunctionType const*>(exprType);
+		functionType &&
+		_memberAccess.memberName() == "selector" &&
+		functionType->hasDeclaration()
+	)
+	{
+		defineExpr(_memberAccess, functionType->externalIdentifier());
+		return false;
+	}
 	else
 		m_errorReporter.warning(
 			7650_error,
@@ -1207,9 +1214,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 
 	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
 	solAssert(arrayVar, "");
+	TypePointer baseType = _indexAccess.baseExpression().annotation().type;
 	defineExpr(_indexAccess, smtutil::Expression::select(
 		arrayVar->elements(),
-		expr(*_indexAccess.indexExpression())
+		expr(*_indexAccess.indexExpression(), keyType(baseType))
 	));
 	setSymbolicUnknownValue(
 		expr(_indexAccess),
@@ -1241,17 +1249,19 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
 			auto const& base = indexAccess->baseExpression();
 			if (dynamic_cast<Identifier const*>(&base))
 				base.accept(*this);
+
+			TypePointer baseType = base.annotation().type;
+			auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType));
 			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
 			solAssert(symbArray, "");
-			auto baseType = symbArray->type();
 			toStore = smtutil::Expression::tuple_constructor(
 				smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
-				{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
+				{smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()}
 			);
 			m_context.expression(*indexAccess)->increaseIndex();
 			defineExpr(*indexAccess, smtutil::Expression::select(
 				symbArray->elements(),
-				expr(*indexAccess->indexExpression())
+				indexExpr
 			));
 			lastExpr = &indexAccess->baseExpression();
 		}
@@ -1527,8 +1537,6 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 
 	if (_op == Token::Div || _op == Token::Mod)
 	{
-		m_context.addAssertion(_right != 0);
-
 		// mod and unsigned division never underflow/overflow
 		if (_op == Token::Mod || !intType->isSigned())
 			return {valueUnbounded, valueUnbounded};
@@ -1739,13 +1747,15 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
 	m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left);
 	if (_type.isSigned())
 		m_context.addAssertion(
-			(_left >= 0 && 0 <= r.currentValue() && r.currentValue() < smtutil::abs(_right)) ||
-			(_left < 0 && (0 - smtutil::abs(_right)) < r.currentValue() && r.currentValue() <= 0)
+			(_left >= 0 && 0 <= r.currentValue() && (_right == 0 || r.currentValue() < smtutil::abs(_right))) ||
+			(_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r.currentValue()) && r.currentValue() <= 0))
 		);
 	else // unsigned version
-		m_context.addAssertion(0 <= r.currentValue() && r.currentValue() < _right);
+		m_context.addAssertion(0 <= r.currentValue() && (_right == 0 || r.currentValue() < _right));
 
-	return {d.currentValue(), r.currentValue()};
+	auto divResult = smtutil::Expression::ite(_right == 0, 0, d.currentValue());
+	auto modResult = smtutil::Expression::ite(_right == 0, 0, r.currentValue());
+	return {divResult, modResult};
 }
 
 void SMTEncoder::assignment(
@@ -2235,6 +2245,19 @@ Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
 	return base;
 }
 
+TypePointer SMTEncoder::keyType(TypePointer _type)
+{
+	if (auto const* mappingType = dynamic_cast<MappingType const*>(_type))
+		return mappingType->keyType();
+	if (
+		dynamic_cast<ArrayType const*>(_type) ||
+		dynamic_cast<ArraySliceType const*>(_type)
+	)
+		return TypeProvider::uint256();
+	else
+		solAssert(false, "");
+}
+
 Expression const* SMTEncoder::innermostTuple(Expression const& _expr)
 {
 	auto const* tuple = dynamic_cast<TupleExpression const*>(&_expr);

libsolidity/formal/SMTEncoder.h

@@ -55,6 +55,11 @@ public:
 	/// @returns the leftmost identifier in a multi-d IndexAccess.
 	static Expression const* leftmostBase(IndexAccess const& _indexAccess);
 
+	/// @returns the key type in _type.
+	/// _type must allow IndexAccess, that is,
+	/// it must be either ArrayType or MappingType
+	static TypePointer keyType(TypePointer _type);
+
 	/// @returns the innermost element in a chain of 1-tuples if applicable,
 	/// otherwise _expr.
 	static Expression const* innermostTuple(Expression const& _expr);