Merge pull request #15880 from ethereum/smt-fix-contract-selection

blishko · web-flow · commit b53eba3c3a3e · 2025-03-19T14:04:03.000+01:00
SMTChecker: Fix analysis for selected contracts
diff --git a/Changelog.md b/Changelog.md
@@ -7,6 +7,7 @@ Compiler Features:
 
 
 Bugfixes:
+* SMTChecker: Fix incorrect analysis when only a subset of contracts is selected with `--model-checker-contracts`.
 
 
 ### 0.8.29 (2025-03-12)
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
@@ -1068,7 +1068,7 @@ void BMC::addVerificationTarget(
 	Expression const* _expression
 )
 {
-	if (!m_settings.targets.has(_type) || (m_currentContract && !shouldAnalyze(*m_currentContract)))
+	if (!m_settings.targets.has(_type) || (m_currentContract && !shouldAnalyzeVerificationTargetsFor(*m_currentContract)))
 		return;
 
 	BMCVerificationTarget target{
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
@@ -89,7 +89,7 @@ void CHC::analyze(SourceUnit const& _source)
 			" If you wish to use Eldarica, please enable Eldarica only."
 		);
 
-	if (!shouldAnalyze(_source))
+	if (!shouldAnalyzeVerificationTargetsFor(_source))
 		return;
 
 	resetSourceAnalysis();
@@ -131,7 +131,7 @@ std::vector<std::string> CHC::unhandledQueries() const
 
 bool CHC::visit(ContractDefinition const& _contract)
 {
-	if (!shouldAnalyze(_contract))
+	if (!shouldEncode(_contract))
 		return false;
 
 	// Raises UnimplementedFeatureError in the presence of transient storage variables
@@ -152,7 +152,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 void CHC::endVisit(ContractDefinition const& _contract)
 {
-	if (!shouldAnalyze(_contract))
+	if (!shouldEncode(_contract))
 		return;
 
 	for (auto base: _contract.annotation().linearizedBaseContracts)
@@ -239,15 +239,14 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	setCurrentBlock(*m_constructorSummaries.at(&_contract));
 
 	solAssert(&_contract == m_currentContract, "");
-	if (shouldAnalyze(_contract))
-	{
-		auto constructor = _contract.constructor();
-		auto txConstraints = state().txTypeConstraints();
-		if (!constructor || !constructor->isPayable())
-			txConstraints = txConstraints && state().txNonPayableConstraint();
+	smtAssert(shouldEncode(_contract));
+	auto constructor = _contract.constructor();
+	auto txConstraints = state().txTypeConstraints();
+	if (!constructor || !constructor->isPayable())
+		txConstraints = txConstraints && state().txNonPayableConstraint();
+	connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0);
+	if (shouldAnalyzeVerificationTargetsFor(_contract))
 		m_queryPlaceholders[&_contract].push_back({txConstraints, errorFlag().currentValue(), m_currentBlock});
-		connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0);
-	}
 
 	solAssert(m_scopes.back() == &_contract, "");
 	m_scopes.pop_back();
@@ -338,7 +337,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		!_function.isConstructor() &&
 		_function.isPublic() &&
 		contractFunctions(*m_currentContract).count(&_function) &&
-		shouldAnalyze(*m_currentContract)
+		shouldEncode(*m_currentContract)
 	)
 	{
 		defineExternalFunctionInterface(_function, *m_currentContract);
@@ -349,8 +348,9 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
 		auto sum = externalSummary(_function);
 
-		m_queryPlaceholders[&_function].push_back({sum, errorFlag().currentValue(), ifacePre});
 		connectBlocks(ifacePre, interface(), sum && errorFlag().currentValue() == 0);
+		if (shouldAnalyzeVerificationTargetsFor(*m_currentContract))
+			m_queryPlaceholders[&_function].push_back({sum, errorFlag().currentValue(), ifacePre});
 	}
 
 	m_currentFunction = nullptr;
diff --git a/libsolidity/formal/ModelCheckerSettings.cpp b/libsolidity/formal/ModelCheckerSettings.cpp
@@ -123,7 +123,7 @@ std::optional<ModelCheckerContracts> ModelCheckerContracts::fromString(std::stri
 	{
 		auto&& names = sourceContract | ranges::views::split(':') | ranges::to<std::vector<std::string>>();
 		if (names.size() != 2 || names.at(0).empty() || names.at(1).empty())
-			return {};
+			return std::nullopt;
 		chosen[names.at(0)].insert(names.at(1));
 	}
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
@@ -1092,19 +1092,24 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
 	}
 }
 
-bool SMTEncoder::shouldAnalyze(SourceUnit const& _source) const
+bool SMTEncoder::shouldEncode(ContractDefinition const& _contract) const
+{
+	return _contract.canBeDeployed();
+}
+
+bool SMTEncoder::shouldAnalyzeVerificationTargetsFor(SourceUnit const& _source) const
 {
 	return m_settings.contracts.isDefault() ||
 		m_settings.contracts.has(*_source.annotation().path);
 }
 
-bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const
+bool SMTEncoder::shouldAnalyzeVerificationTargetsFor(ContractDefinition const& _contract) const
 {
-	if (!_contract.canBeDeployed())
+	if (!shouldEncode(_contract))
 		return false;
 
 	return m_settings.contracts.isDefault() ||
-		m_settings.contracts.has(_contract.sourceUnitName());
+		m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());
 }
 
 void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
@@ -238,11 +238,12 @@ class SMTEncoder: public ASTConstVisitor
 	void visitFunctionIdentifier(Identifier const& _identifier);
 	virtual void visitPublicGetter(FunctionCall const& _funCall);
 
-	/// @returns true if @param _contract is set for analysis in the settings
-	/// and it is not abstract.
-	bool shouldAnalyze(ContractDefinition const& _contract) const;
-	/// @returns true if @param _source is set for analysis in the settings.
-	bool shouldAnalyze(SourceUnit const& _source) const;
+	/// @returns true if symbolic representation of @param _contract is required for verification
+	bool shouldEncode(ContractDefinition const& _contract) const;
+	/// @returns true if the verification targets of @param _contract are actually selected for verification
+	bool shouldAnalyzeVerificationTargetsFor(ContractDefinition const& _contract) const;
+	/// @returns true if we should descend into @param _source to look for contracts that should be verified
+	bool shouldAnalyzeVerificationTargetsFor(SourceUnit const& _source) const;
 
 	/// @returns the state variable returned by a public getter if
 	/// @a _expr is a call to a public getter,
diff --git a/test/cmdlineTests/model_checker_contracts_inexistent_contract/err b/test/cmdlineTests/model_checker_contracts_inexistent_contract/err
@@ -1,27 +1 @@
 Warning: Requested contract "C" does not exist in source "model_checker_contracts_inexistent_contract/input.sol".
-
-Warning: CHC: Assertion violation happens here.
-Counterexample:
-
-x = 0
-
-Transaction trace:
-B.constructor()
-B.f(0)
- --> model_checker_contracts_inexistent_contract/input.sol:5:3:
-  |
-5 | 		assert(x > 0);
-  | 		^^^^^^^^^^^^^
-
-Warning: CHC: Assertion violation happens here.
-Counterexample:
-
-y = 0
-
-Transaction trace:
-A.constructor()
-A.g(0)
-  --> model_checker_contracts_inexistent_contract/input.sol:10:3:
-   |
-10 | 		assert(y > 0);
-   | 		^^^^^^^^^^^^^
diff --git a/test/cmdlineTests/model_checker_contracts_only_one/err b/test/cmdlineTests/model_checker_contracts_only_one/err
@@ -4,7 +4,7 @@ Counterexample:
 x = 0
 
 Transaction trace:
-B.constructor()
+A.constructor()
 B.f(0)
  --> model_checker_contracts_only_one/input.sol:5:3:
   |
diff --git a/test/cmdlineTests/standard_model_checker_contracts_inexistent_contract/output.json b/test/cmdlineTests/standard_model_checker_contracts_inexistent_contract/output.json
@@ -9,72 +9,6 @@
             "message": "Requested contract \"C\" does not exist in source \"Source\".",
             "severity": "warning",
             "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "6328",
-            "formattedMessage": "Warning: CHC: Assertion violation happens here.
-Counterexample:
-
-y = 0
-
-Transaction trace:
-B.constructor()
-B.g(0)
- --> Source:5:7:
-  |
-5 | \t\t\t\t\t\tassert(y > 0);
-  | \t\t\t\t\t\t^^^^^^^^^^^^^
-
-",
-            "message": "CHC: Assertion violation happens here.
-Counterexample:
-
-y = 0
-
-Transaction trace:
-B.constructor()
-B.g(0)",
-            "severity": "warning",
-            "sourceLocation": {
-                "end": 137,
-                "file": "Source",
-                "start": 124
-            },
-            "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "6328",
-            "formattedMessage": "Warning: CHC: Assertion violation happens here.
-Counterexample:
-
-x = 0
-
-Transaction trace:
-A.constructor()
-A.f(0)
-  --> Source:10:7:
-   |
-10 | \t\t\t\t\t\tassert(x > 0);
-   | \t\t\t\t\t\t^^^^^^^^^^^^^
-
-",
-            "message": "CHC: Assertion violation happens here.
-Counterexample:
-
-x = 0
-
-Transaction trace:
-A.constructor()
-A.f(0)",
-            "severity": "warning",
-            "sourceLocation": {
-                "end": 231,
-                "file": "Source",
-                "start": 218
-            },
-            "type": "Warning"
         }
     ],
     "sources": {
diff --git a/test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json b/test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json
@@ -9,7 +9,7 @@ Counterexample:
 y = 0
 
 Transaction trace:
-B.constructor()
+A.constructor()
 B.g(0)
  --> Source:5:7:
   |
@@ -23,7 +23,7 @@ Counterexample:
 y = 0
 
 Transaction trace:
-B.constructor()
+A.constructor()
 B.g(0)",
             "severity": "warning",
             "sourceLocation": {
diff --git a/test/cmdlineTests/standard_model_checker_contracts_only_one/output.json b/test/cmdlineTests/standard_model_checker_contracts_only_one/output.json
@@ -9,7 +9,7 @@ Counterexample:
 y = 0
 
 Transaction trace:
-B.constructor()
+A.constructor()
 B.g(0)
  --> Source:5:7:
   |
@@ -23,7 +23,7 @@ Counterexample:
 y = 0
 
 Transaction trace:
-B.constructor()
+A.constructor()
 B.g(0)",
             "severity": "warning",
             "sourceLocation": {
diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp
@@ -32,8 +32,17 @@ SMTCheckerTest::SMTCheckerTest(std::string const& _filename):
 	universalCallback(nullptr, smtCommand)
 {
 	auto contract = m_reader.stringSetting("SMTContract", "");
-	if (!contract.empty())
+	auto maybeContracts = ModelCheckerContracts::fromString(contract);
+	auto isValidContractName = [](std::string const& _name)
+	{
+		return !_name.empty() && _name.find_first_of(" \t\n\r:,") == std::string::npos;
+	};
+	if (maybeContracts)
+		m_modelCheckerSettings.contracts = *maybeContracts;
+	else if (isValidContractName(contract))
 		m_modelCheckerSettings.contracts.contracts[""] = {contract};
+	else
+		BOOST_THROW_EXCEPTION(std::runtime_error("Invalid contract specified in SMTContract setting."));
 
 	auto extCallsMode = ModelCheckerExtCalls::fromString(m_reader.stringSetting("SMTExtCalls", "untrusted"));
 	if (extCallsMode)
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol
@@ -1,6 +1,6 @@
 contract State {
 	function f(uint _x) public pure returns (uint) {
-		assert(_x < 100); // should fail
+		assert(_x < 100); // should hold when analyzing only contract C (can fail only when analyzing State as standalone contract)
 		return _x;
 	}
 }
@@ -18,5 +18,4 @@ contract C {
 // SMTExtCalls: trusted
 // SMTIgnoreInv: yes
 // ----
-// Warning 6328: (69-85): CHC: Assertion violation happens here.
-// Info 1391: CHC: 1 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.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol
@@ -1,6 +1,6 @@
 contract State {
 	function f(uint _x) public pure returns (uint) {
-		assert(_x < 100); // should fail
+		assert(_x < 100); // should hold when analyzing only contract C (can fail only when analyzing State as standalone contract)
 		return _x;
 	}
 }
@@ -21,5 +21,4 @@ contract C {
 // SMTEngine: all
 // SMTExtCalls: trusted
 // ----
-// Warning 6328: (69-85): CHC: Assertion violation happens here.
-// Info 1391: CHC: 1 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.
diff --git a/test/libsolidity/smtCheckerTests/imports/target_in_imported_contract_analyzed_when_called_from_selection_with_trusted_calls.sol b/test/libsolidity/smtCheckerTests/imports/target_in_imported_contract_analyzed_when_called_from_selection_with_trusted_calls.sol
@@ -0,0 +1,11 @@
+==== Source: A.sol ====
+contract A { function a() pure public { assert(false); } }
+==== Source: B.sol ====
+import "A.sol";
+contract B { function b(A a) pure public { a.a(); } }
+// ====
+// SMTContract: B.sol:B
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (A.sol:40-53): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\nTransaction trace:\nB.constructor()\nB.b(0)\n    A.a() -- trusted external call
diff --git a/test/libsolidity/smtCheckerTests/imports/target_in_imported_contract_not_analyzed_when_not_selected_and_not_called_from_selection.sol b/test/libsolidity/smtCheckerTests/imports/target_in_imported_contract_not_analyzed_when_not_selected_and_not_called_from_selection.sol
@@ -0,0 +1,9 @@
+==== Source: A.sol ====
+contract A { function a() pure public { assert(false); } }
+==== Source: B.sol ====
+import "A.sol";
+contract B { function b() pure public { } }
+// ====
+// SMTContract: B.sol:B
+// SMTEngine: chc
+// ----
diff --git a/test/libsolidity/smtCheckerTests/verification_target/target_in_constructor_of_same_source_contract_not_analyzed_when_not_selected_and_not_called_from_selection.sol b/test/libsolidity/smtCheckerTests/verification_target/target_in_constructor_of_same_source_contract_not_analyzed_when_not_selected_and_not_called_from_selection.sol
@@ -0,0 +1,13 @@
+contract B {
+    constructor() { fail(); }
+
+    function fail() pure internal { assert(false); }
+}
+
+contract A {
+    function safe() pure public { }
+}
+// ====
+// SMTContract: A
+// SMTEngine: chc
+// ----
diff --git a/test/libsolidity/smtCheckerTests/verification_target/target_in_same_source_contract_not_analyzed_when_not_selected_and_not_called_from_selection.sol b/test/libsolidity/smtCheckerTests/verification_target/target_in_same_source_contract_not_analyzed_when_not_selected_and_not_called_from_selection.sol
@@ -0,0 +1,11 @@
+contract B {
+    function fail() pure public { assert(false); }
+}
+
+contract A {
+    function safe() pure public { }
+}
+// ====
+// SMTContract: A
+// SMTEngine: chc
+// ----

Original file line number	Diff line number	Diff line change
`@@ -7,6 +7,7 @@ Compiler Features:`
`7`	`7`
`8`	`8`
`9`	`9`	`Bugfixes:`
	`10`	+* SMTChecker: Fix incorrect analysis when only a subset of contracts is selected with `--model-checker-contracts`.
`10`	`11`
`11`	`12`
`12`	`13`	`### 0.8.29 (2025-03-12)`
Original file line number	Diff line number	Diff line change
`@@ -1068,7 +1068,7 @@ void BMC::addVerificationTarget(`
`1068`	`1068`	`Expression const* _expression`
`1069`	`1069`	`)`
`1070`	`1070`	`{`
`1071`		`- if (!m_settings.targets.has(_type) \|\| (m_currentContract && !shouldAnalyze(*m_currentContract)))`
	`1071`	`+ if (!m_settings.targets.has(_type) \|\| (m_currentContract && !shouldAnalyzeVerificationTargetsFor(*m_currentContract)))`
`1072`	`1072`	`return;`
`1073`	`1073`
`1074`	`1074`	`BMCVerificationTarget target{`
Original file line number	Diff line number	Diff line change
`@@ -123,7 +123,7 @@ std::optional<ModelCheckerContracts> ModelCheckerContracts::fromString(std::stri`
`123`	`123`	`{`
`124`	`124`	`auto&& names = sourceContract \| ranges::views::split(':') \| ranges::to<std::vector<std::string>>();`
`125`	`125`	`if (names.size() != 2 \|\| names.at(0).empty() \|\| names.at(1).empty())`
`126`		`- return {};`
	`126`	`+ return std::nullopt;`
`127`	`127`	`chosen[names.at(0)].insert(names.at(1));`
`128`	`128`	`}`
`129`	`129`
Original file line number	Diff line number	Diff line change
`@@ -1092,19 +1092,24 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)`
`1092`	`1092`	`}`
`1093`	`1093`	`}`
`1094`	`1094`
`1095`		`-bool SMTEncoder::shouldAnalyze(SourceUnit const& _source) const`
	`1095`	`+bool SMTEncoder::shouldEncode(ContractDefinition const& _contract) const`
	`1096`	`+{`
	`1097`	`+ return _contract.canBeDeployed();`
	`1098`	`+}`
	`1099`	`+`
	`1100`	`+bool SMTEncoder::shouldAnalyzeVerificationTargetsFor(SourceUnit const& _source) const`
`1096`	`1101`	`{`
`1097`	`1102`	`return m_settings.contracts.isDefault() \|\|`
`1098`	`1103`	`m_settings.contracts.has(*_source.annotation().path);`
`1099`	`1104`	`}`
`1100`	`1105`
`1101`		`-bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const`
	`1106`	`+bool SMTEncoder::shouldAnalyzeVerificationTargetsFor(ContractDefinition const& _contract) const`
`1102`	`1107`	`{`
`1103`		`- if (!_contract.canBeDeployed())`
	`1108`	`+ if (!shouldEncode(_contract))`
`1104`	`1109`	`return false;`
`1105`	`1110`
`1106`	`1111`	`return m_settings.contracts.isDefault() \|\|`
`1107`		`- m_settings.contracts.has(_contract.sourceUnitName());`
	`1112`	`+ m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());`
`1108`	`1113`	`}`
`1109`	`1114`
`1110`	`1115`	`void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)`
Original file line number	Diff line number	Diff line change
`@@ -4,7 +4,7 @@ Counterexample:`
`4`	`4`	`x = 0`
`5`	`5`
`6`	`6`	`Transaction trace:`
`7`		`-B.constructor()`
	`7`	`+A.constructor()`
`8`	`8`	`B.f(0)`
`9`	`9`	`--> model_checker_contracts_only_one/input.sol:5:3:`
`10`	`10`	`\|`