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.

Author: blishko

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 cryptographic functions.
  * 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.
 

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), ""),

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, "b", "c");
+		address e2 = ecrecover("a", 1, "b", "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.