Merge pull request #15782 from ethereum/smt-bmc-getters

SMTChecker: Fix crash in BMC engine regarding state variables

Author: blishko

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.

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);

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();

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();
 

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.