From 8ca453f82ec2a37f808129501fbe0edee30b2431 Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@gmail.com>
Date: Fri, 26 May 2023 14:10:33 +0200
Subject: [PATCH] SMTChecker: External function call with struct member is not
 getter

if a struct has a member that is a function pointer with `external`
attribute, and such a member is called, it is currently incorrectly
treated as a public getter in SMTEncoder.

The proposed fix is to make SMTEncoder::publicGetter more strict in
deciding whether an expression is a public getter.
The added condition, that the access happens on a state variable, is
exactly what is checked later with an assertion that is currently
failing.
---
 libsolidity/formal/SMTEncoder.cpp             |  3 +-
 .../struct_external_function_pointer.sol      | 33 +++++++++++++++++++
 2 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 test/libsolidity/smtCheckerTests/types/struct/struct_external_function_pointer.sol

diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 8f22ab824..818efac5c 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -2839,7 +2839,8 @@ smtutil::Expression SMTEncoder::contractAddressValue(FunctionCall const& _f)
 
 VariableDeclaration const* SMTEncoder::publicGetter(Expression const& _expr) const {
 	if (auto memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
-		return dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration);
+		if (auto variableDeclaration = dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration))
+			return variableDeclaration->isStateVariable() ? variableDeclaration : nullptr;
 	return nullptr;
 }
 
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_external_function_pointer.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_external_function_pointer.sol
new file mode 100644
index 000000000..494d2dcf2
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_external_function_pointer.sol
@@ -0,0 +1,33 @@
+struct S {
+    function() external returns (uint) x;
+}
+contract C {
+
+    function X() public pure returns (uint) {
+        return 1;
+    }
+
+    uint y;
+    uint z;
+
+    function setZ(uint _z) public {
+        z = _z;
+    }
+
+
+    function f() public returns (uint) {
+        S memory s;
+        s.x = this.X;
+        require(y == 0);
+        require(z == 0);
+        uint ret = s.x();
+        assert(y == 0); // should hold
+        assert(z == 0); // can report violation due to overapproximation after externall call s.x()
+        return ret;
+    }
+}
+
+
+// ----
+// Warning 6328: (431-445): 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.