Skip to content

SMTChecker: Fix encoding of arguments of cryptographic functions #15749

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jan 22, 2025
Merged

SMTChecker: Fix encoding of arguments of cryptographic functions #15749

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Changelog.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
10 changes: 5 additions & 5 deletions libsolidity/formal/SMTEncoder.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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), ""),
Expand Down
12 changes: 9 additions & 3 deletions test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_string_literal.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.