Merge pull request #15191 from pgebal/smtchecker/fix-invalid-number-of-verified-checks

SMTChecker: Fix error that reports invalid number of verified checks

Author: blishko

Changelog.md

@@ -11,6 +11,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix error that reports invalid number of verified checks for BMC engine.
  * TypeChecker: Fix segfault when assigning nested tuple to tuple.
  * Yul Optimizer: Name simplification could lead to forbidden identifiers with a leading and/or trailing dot, e.g., ``x._`` would get simplified into ``x.``.
 

libsolidity/formal/BMC.cpp

@@ -118,13 +118,18 @@ void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<V
 		);
 
 	if (!m_settings.showProvedSafe && !m_safeTargets.empty())
+	{
+		std::size_t provedSafeNum = 0;
+		for (auto&& [_, targets]: m_safeTargets)
+			provedSafeNum += targets.size();
 		m_errorReporter.info(
 			6002_error,
 			"BMC: " +
-			std::to_string(m_safeTargets.size()) +
+			std::to_string(provedSafeNum) +
 			" verification condition(s) proved safe!" +
 			" Enable the model checker option \"show proved safe\" to see all of them."
 		);
+	}
 	else if (m_settings.showProvedSafe)
 		for (auto const& [node, targets]: m_safeTargets)
 			for (auto const& target: targets)

libsolidity/formal/BMC.h

@@ -149,7 +149,10 @@ class BMC: public SMTEncoder
 
 		friend bool operator<(BMCVerificationTarget const& _a, BMCVerificationTarget const& _b)
 		{
-			return _a.expression->id() < _b.expression->id();
+			if (_a.expression->id() == _b.expression->id())
+				return _a.type < _b.type;
+			else
+				return _a.expression->id() < _b.expression->id();
 		}
 	};
 

test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol

@@ -39,4 +39,4 @@ contract C is B {
 // Warning 4661: (389-412): BMC: Assertion violation happens here.
 // Warning 4661: (489-513): BMC: Assertion violation happens here.
 // Warning 4661: (533-546): BMC: Assertion violation happens here.
-// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/operators/unary_minus_bmc.sol

@@ -8,4 +8,4 @@ contract C
 // SMTEngine: bmc
 // ----
 // Warning 4661: (48-63): BMC: Assertion violation happens here.
-// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol

@@ -77,4 +77,4 @@ contract C {
 // Warning 4144: (953-982): BMC: Underflow (resulting value less than -32768) happens here.
 // Warning 3046: (1149-1178): BMC: Division by zero happens here.
 // Warning 7812: (2245-2271): BMC: Assertion violation might happen here.
-// Info 6002: BMC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 6002: BMC: 10 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/overflow/overflow_and_underflow_bmc.sol

@@ -0,0 +1,11 @@
+contract C {
+	function f(int x, int y) public pure returns (int) {
+		require(x == 0);
+		require(y == 0);
+		return x + y;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.