From 57342666ca9b03499d8299b3ff269494647b6787 Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@ethereum.org>
Date: Fri, 10 Jan 2025 21:20:56 +0100
Subject: [PATCH] SMTChecker: Fix crash in BMC engine regarding state variables

Previously, analyzing a call to a getter to a contract then has not been
analyzed yet with BMC would result in a crash because BMC would not know
about the state variable being accessed.

To fix this, we let BMC know about all state variables in all contracts
during initialization.
---
 Changelog.md                                  |  1 +
 libsolidity/formal/BMC.cpp                    |  4 +++-
 libsolidity/formal/SMTEncoder.cpp             |  8 +++++++
 libsolidity/formal/SMTEncoder.h               |  3 +++
 .../cross_contract_getter_call.sol            | 22 +++++++++++++++++++
 5 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 test/libsolidity/smtCheckerTests/bmc_coverage/cross_contract_getter_call.sol

diff --git a/Changelog.md b/Changelog.md
index c00adf0fd977..35f9b83bedda 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -11,6 +11,7 @@ Compiler Features:
 
 Bugfixes:
  * General: Fix internal compiler error when requesting IR AST outputs for interfaces and abstract contracts.
+ * SMTChecker: Fix SMT logic error when analyzing cross-contract getter call with BMC.
  * SMTChecker: Fix SMT logic error when initializing a fixed-sized-bytes array using string literals.
  * SMTChecker: Fix SMT logic error when translating invariants involving array store and select operations.
  * SMTChecker: Fix wrong encoding of string literals as arguments of ``ecrecover`` precompile.
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 679309766c36..d7bad10e7b35 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -93,7 +93,9 @@ void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<V
 	m_context.reset();
 	m_context.setAssertionAccumulation(true);
 	m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
-	createFreeConstants(sourceDependencies(_source));
+	auto const& sources = sourceDependencies(_source);
+	createFreeConstants(sources);
+	createStateVariables(sources);
 	m_unprovedAmt = 0;
 
 	_source.accept(*this);
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 6db9420b802b..d7b23156383e 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -3271,6 +3271,14 @@ void SMTEncoder::createFreeConstants(std::set<SourceUnit const*, ASTNode::Compar
 				}
 }
 
+void SMTEncoder::createStateVariables(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
+{
+	for (auto const& source: _sources)
+		for (auto const& node: source->nodes())
+			if (auto contract = dynamic_cast<ContractDefinition const*>(node.get()))
+				createStateVariables(*contract);
+}
+
 smt::SymbolicState& SMTEncoder::state()
 {
 	return m_context.state();
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 3248f1390f64..f01f6802c337 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -439,6 +439,9 @@ class SMTEncoder: public ASTConstVisitor
 	/// Create symbolic variables for the free constants in all @param _sources.
 	void createFreeConstants(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources);
 
+	/// Create symbolic variables for all state variables for all contracts in all @param _sources.
+	void createStateVariables(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources);
+
 	/// @returns a note to be added to warnings.
 	std::string extraComment();
 
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/cross_contract_getter_call.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/cross_contract_getter_call.sol
new file mode 100644
index 000000000000..f36647ed2b04
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/cross_contract_getter_call.sol
@@ -0,0 +1,22 @@
+contract C {
+	D internal d;
+	constructor() {
+		d = new D();
+	}
+	function invokeAndCheck() public {
+		d.set();
+		assert(d.n() <= 1);
+	}
+}
+
+contract D {
+	uint public n;
+	function set() external {
+		n = 1;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 8729: (51-58): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
+// Warning 4661: (112-130): BMC: Assertion violation happens here.