Remove UnderOverflow verification target for BMC engine

ethereum · May 9, 2024 · 3c5aa3b · 3c5aa3b
1 parent 7c94f53
commit 3c5aa3b
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 55 deletions.
diff --git a/Changelog.md b/Changelog.md
@@ -5,7 +5,7 @@ Language Features:
 
 
 Compiler Features:
-* SMTChecker: Create balance check verification target for CHC engine.
+* SMTChecker: Add balance check verification target for CHC engine.
 
 Bugfixes:
  * Commandline Interface: Fix ICE when the optimizer is disabled and an empty/blank string is used for ``--yul-optimizations`` sequence.

diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
@@ -569,11 +569,18 @@ void BMC::endVisit(UnaryOperation const& _op)
 		return;
 
 	if (_op.getOperator() == Token::Sub && smt::isInteger(*_op.annotation().type))
+	{
+		addVerificationTarget(
+			VerificationTargetType::Underflow,
+			expr(_op),
+			&_op
+		);
 		addVerificationTarget(
-			VerificationTargetType::UnderOverflow,
+			VerificationTargetType::Overflow,
 			expr(_op),
 			&_op
 		);
+	}
 }
 
 void BMC::endVisit(BinaryOperation const& _op)
@@ -813,32 +820,29 @@ std::pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
 	if (_op == Token::Mod)
 		return values;
 
-	VerificationTargetType type;
 	// The order matters here:
 	// If _op is Div and intType is signed, we only care about overflow.
 	if (_op == Token::Div)
 	{
 		if (intType->isSigned())
 			// Signed division can only overflow.
-			type = VerificationTargetType::Overflow;
+			addVerificationTarget(VerificationTargetType::Overflow, values.second, &_expression);
 		else
 			// Unsigned division cannot underflow/overflow.
 			return values;
 	}
 	else if (intType->isSigned())
-		type = VerificationTargetType::UnderOverflow;
+	{
+		addVerificationTarget(VerificationTargetType::Overflow, values.second, &_expression);
+		addVerificationTarget(VerificationTargetType::Underflow, values.second, &_expression);
+	}
 	else if (_op == Token::Sub)
-		type = VerificationTargetType::Underflow;
+		addVerificationTarget(VerificationTargetType::Underflow, values.second, &_expression);
 	else if (_op == Token::Add || _op == Token::Mul)
-		type = VerificationTargetType::Overflow;
+		addVerificationTarget(VerificationTargetType::Overflow, values.second, &_expression);
 	else
 		solAssert(false, "");
 
-	addVerificationTarget(
-		type,
-		values.second,
-		&_expression
-	);
 	return values;
 }
 
@@ -919,6 +923,12 @@ void BMC::checkVerificationTargets()
 
 void BMC::checkVerificationTarget(BMCVerificationTarget& _target)
 {
+	if (
+		m_solvedTargets.count(_target.expression) &&
+		m_solvedTargets.at(_target.expression).count(_target.type)
+	)
+		return;
+
 	switch (_target.type)
 	{
 		case VerificationTargetType::ConstantCondition:
@@ -930,10 +940,6 @@ void BMC::checkVerificationTarget(BMCVerificationTarget& _target)
 		case VerificationTargetType::Overflow:
 			checkOverflow(_target);
 			break;
-		case VerificationTargetType::UnderOverflow:
-			checkUnderflow(_target);
-			checkOverflow(_target);
-			break;
 		case VerificationTargetType::DivByZero:
 			checkDivByZero(_target);
 			break;
@@ -961,19 +967,10 @@ void BMC::checkConstantCondition(BMCVerificationTarget& _target)
 void BMC::checkUnderflow(BMCVerificationTarget& _target)
 {
 	solAssert(
-		_target.type == VerificationTargetType::Underflow ||
-			_target.type == VerificationTargetType::UnderOverflow,
+		_target.type == VerificationTargetType::Underflow,
 		""
 	);
 
-	if (
-		m_solvedTargets.count(_target.expression) && (
-			m_solvedTargets.at(_target.expression).count(VerificationTargetType::Underflow) ||
-			m_solvedTargets.at(_target.expression).count(VerificationTargetType::UnderOverflow)
-		)
-	)
-		return;
-
 	auto const* intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
 	if (!intType)
 		intType = TypeProvider::uint256();
@@ -994,19 +991,10 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target)
 void BMC::checkOverflow(BMCVerificationTarget& _target)
 {
 	solAssert(
-		_target.type == VerificationTargetType::Overflow ||
-			_target.type == VerificationTargetType::UnderOverflow,
+		_target.type == VerificationTargetType::Overflow,
 		""
 	);
 
-	if (
-		m_solvedTargets.count(_target.expression) && (
-			m_solvedTargets.at(_target.expression).count(VerificationTargetType::Overflow) ||
-			m_solvedTargets.at(_target.expression).count(VerificationTargetType::UnderOverflow)
-		)
-	)
-		return;
-
 	auto const* intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
 	if (!intType)
 		intType = TypeProvider::uint256();
@@ -1028,12 +1016,6 @@ void BMC::checkDivByZero(BMCVerificationTarget& _target)
 {
 	solAssert(_target.type == VerificationTargetType::DivByZero, "");
 
-	if (
-		m_solvedTargets.count(_target.expression) &&
-		m_solvedTargets.at(_target.expression).count(VerificationTargetType::DivByZero)
-	)
-		return;
-
 	checkCondition(
 		_target,
 		_target.constraints && (_target.value == 0),
@@ -1051,11 +1033,6 @@ void BMC::checkBalance(BMCVerificationTarget& _target)
 {
 	solAssert(_target.type == VerificationTargetType::Balance, "");
 
-	if (
-		m_solvedTargets.count(_target.expression) &&
-		m_solvedTargets.at(_target.expression).count(VerificationTargetType::Balance)
-	)
-		return;
 	checkCondition(
 		_target,
 		_target.constraints && _target.value,
@@ -1072,12 +1049,6 @@ void BMC::checkAssert(BMCVerificationTarget& _target)
 {
 	solAssert(_target.type == VerificationTargetType::Assert, "");
 
-	if (
-		m_solvedTargets.count(_target.expression) &&
-		m_solvedTargets.at(_target.expression).count(_target.type)
-	)
-		return;
-
 	checkCondition(
 		_target,
 		_target.constraints && !_target.value,

diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h
@@ -113,7 +113,7 @@ struct ModelCheckerInvariants
 	std::set<InvariantType> invariants;
 };
 
-enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray, OutOfBounds };
+enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, DivByZero, Balance, Assert, PopEmptyArray, OutOfBounds };
 
 struct ModelCheckerTargets
 {

diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_1.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_1.sol
@@ -12,4 +12,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (166-201): CHC: Assertion violation happens here.
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.