SMTChecker: Fix analysis for selected contracts

blishko · blishko · commit 25463c564dc1 · 2025-03-19T13:14:48.000+01:00
Previously, when a contract was selected for analysis, the analysis was
incorrect.
There were two issues. First, the contracts in the same file were
considered as entry points even though they were not selected for
analysis.
Second, the contracts in a different file were mostly ignored, resulting
in unsoundness when an external call was made to such a contract in
trusted mode.

The solution to the above problems is to always create representation of all
contracts (in case they are called from the selected contract), but
create verification targets only for the 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`	`\|`