Merge pull request #14344 from pgebal/pgebal/fix-ice-internal-type

Fix error in SMTChecker: Use rich indentifier instead of external identifier to encode member access to functions

Changelog.md

@@ -20,6 +20,7 @@ Bugfixes:
  * Commandline Interface: It is no longer possible to specify both ``--optimize-yul`` and ``--no-optimize-yul`` at the same time.
  * SMTChecker: Fix encoding of side-effects inside ``if`` and ``ternary conditional``statements in the BMC engine.
  * SMTChecker: Fix false negative when a verification target can be violated only by trusted external call from another public function.
+ * SMTChecker: Fix internal error caused by using external identifier to encode member access to functions that take an internal function as a parameter.
  * Standard JSON Interface: Fix an incomplete AST being returned when analysis is interrupted by certain kinds of fatal errors.
  * Yul Optimizer: Ensure that the assignment of memory slots for variables moved to memory does not depend on AST IDs that may depend on whether additional files are included during compilation.
  * Yul Optimizer: Fix optimized IR being unnecessarily passed through the Yul optimizer again before bytecode generation.

libsolidity/formal/SMTEncoder.cpp

@@ -33,6 +33,7 @@
 #include <liblangutil/CharStreamProvider.h>
 
 #include <libsolutil/Algorithms.h>
+#include <libsolutil/FunctionSelector.h>
 
 #include <range/v3/view.hpp>
 
@@ -1358,7 +1359,10 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 	{
 		auto const* functionType = dynamic_cast<FunctionType const*>(_memberAccess.annotation().type);
 		if (functionType && functionType->hasDeclaration())
-			defineExpr(_memberAccess, functionType->externalIdentifier());
+			defineExpr(
+				_memberAccess,
+				util::selectorFromSignatureU32(functionType->richIdentifier())
+			);
 
 		return true;
 	}

test/libsolidity/smtCheckerTests/functions/functions_library_internal.sol

@@ -0,0 +1,14 @@
+library L {
+	function value(function()internal a, uint256 b) internal {}
+}
+contract C {
+	using L for function()internal;
+
+	function f() public {
+		function()internal x;
+		x.value(42);
+ 	}
+}
+// ====
+// SMTEngine: all
+// ----