From 1682f7f8b12562663263e12951100b1561b08ada Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@ethereum.org>
Date: Tue, 21 Jan 2025 17:45:21 +0100
Subject: [PATCH] SMTChecker: Fix encoding of arguments of cryptographic
 functions

For example, the function ecrecover expect an argument of type fixed
bytes, but due to implicit conversion, you can also pass a string
literal. We previously did not take this into account in the encoding
into SMT, which could let to SMT expressions having wrong sorts.
---
 Changelog.md                                         |  1 +
 libsolidity/formal/SMTEncoder.cpp                    | 10 +++++-----
 .../crypto/crypto_functions_same_string_literal.sol  | 12 +++++++++---
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index b0539c403a3d..03a3f7e9b426 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -12,6 +12,7 @@ Bugfixes:
  * General: Fix internal compiler error when requesting IR AST outputs for interfaces and abstract contracts.
  * 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.
  * Standard JSON Interface: Fix ``generatedSources`` and ``sourceMap`` being generated internally even when not requested.
  * Yul: Fix internal compiler error when a code generation error should be reported instead.
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 01627007f03e..6db9420b802b 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -851,7 +851,7 @@ void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
 {
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	auto kind = funType.kind();
-	auto arg0 = expr(*_funCall.arguments().at(0));
+	auto arg0 = expr(*_funCall.arguments().at(0), TypeProvider::bytesStorage());
 	std::optional<smtutil::Expression> result;
 	if (kind == FunctionType::Kind::KECCAK256)
 		result = smtutil::Expression::select(state().cryptoFunction("keccak256"), arg0);
@@ -862,10 +862,10 @@ void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
 	else if (kind == FunctionType::Kind::ECRecover)
 	{
 		auto e = state().cryptoFunction("ecrecover");
-		auto arg0 = expr(*_funCall.arguments().at(0));
-		auto arg1 = expr(*_funCall.arguments().at(1));
-		auto arg2 = expr(*_funCall.arguments().at(2));
-		auto arg3 = expr(*_funCall.arguments().at(3));
+		auto arg0 = expr(*_funCall.arguments().at(0), TypeProvider::fixedBytes(32));
+		auto arg1 = expr(*_funCall.arguments().at(1), TypeProvider::uint(8));
+		auto arg2 = expr(*_funCall.arguments().at(2), TypeProvider::fixedBytes(32));
+		auto arg3 = expr(*_funCall.arguments().at(3), TypeProvider::fixedBytes(32));
 		auto inputSort = dynamic_cast<smtutil::ArraySort&>(*e.sort).domain;
 		auto ecrecoverInput = smtutil::Expression::tuple_constructor(
 			smtutil::Expression(std::make_shared<smtutil::SortSort>(inputSort), ""),
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_string_literal.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_string_literal.sol
index 9e5123ab5bd5..67e7899db3f2 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_string_literal.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_string_literal.sol
@@ -5,19 +5,25 @@ contract C {
 		assert(k1 == k2);
 	}
 
-        function c2() public pure {
+	function c2() public pure {
 		bytes32 s1 = sha256("10");
 		bytes32 s2 = sha256("10");
 		assert(s1 == s2);
 	}
 
-        function c3() public pure {
+	function c3() public pure {
 		bytes32 r1 = ripemd160("100");
 		bytes32 r2 = ripemd160("100");
 		assert(r1 == r2);
 	}
+
+	function c4() public pure {
+		address e1 = ecrecover("a", 1, hex"bb", unicode"c");
+		address e2 = ecrecover("a", 1, hex"bb", unicode"c");
+		assert(e1 == e2);
+	}
 }
 // ====
 // SMTEngine: chc
 // ----
-// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.