cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #11854 from ethereum/smt_fix_push_lvalue

Browse Source 
[SMTChecker] Fix false negative after `push` on storage references
This commit is contained in:
Leonardo 2021-08-30 14:57:34 +02:00 committed by GitHub
commit d1a79214d5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 46 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -13,6 +13,7 @@ Compiler Features:
Bugfixes: Bugfixes:
* SMTChecker: Fix false positive in external calls from constructors. * SMTChecker: Fix false positive in external calls from constructors.
* SMTChecker: Fix internal error on some multi-source uses of ``abi.*``, cryptographic functions and constants. * SMTChecker: Fix internal error on some multi-source uses of ``abi.*``, cryptographic functions and constants.
* SMTChecker: Fix false negative caused by ``push`` on storage array references returned by internal functions.

42
libsolidity/formal/SMTEncoder.cpp
View File

@ -1977,26 +1977,32 @@ void SMTEncoder::assignment(
indexOrMemberAssignment(*left, _right); indexOrMemberAssignment(*left, _right);
else if (auto const* funCall = dynamic_cast<FunctionCall const*>(left)) else if (auto const* funCall = dynamic_cast<FunctionCall const*>(left))
{ {
if ( if (auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type))
auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type);
funType && funType->kind() == FunctionType::Kind::ArrayPush
)
{ {
auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression()); if (funType->kind() == FunctionType::Kind::ArrayPush)
solAssert(memberAccess, ""); {
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression())); auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
solAssert(symbArray, ""); solAssert(memberAccess, "");
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, "");
auto oldLength = symbArray->length(); auto oldLength = symbArray->length();
auto store = smtutil::Expression::store( auto store = smtutil::Expression::store(
symbArray->elements(), symbArray->elements(),
symbArray->length() - 1, symbArray->length() - 1,
_right _right
); );
symbArray->increaseIndex(); symbArray->increaseIndex();
m_context.addAssertion(symbArray->elements() == store); m_context.addAssertion(symbArray->elements() == store);
m_context.addAssertion(symbArray->length() == oldLength); m_context.addAssertion(symbArray->length() == oldLength);
assignment(memberAccess->expression(), symbArray->currentValue()); assignment(memberAccess->expression(), symbArray->currentValue());
}
else if (funType->kind() == FunctionType::Kind::Internal)
{
for (auto type: funType->returnParameterTypes())
if (type->category() == Type::Category::Mapping || dynamic_cast<ReferenceType const*>(type))
resetReferences(type);
}
} }
} }
else else

20
test/libsolidity/smtCheckerTests/array_members/push_function_return_value.sol Normal file
View File

@ -0,0 +1,20 @@
contract C {
bytes x;
function getX() internal view returns (bytes storage) {
return x;
}
function s() public {
require(x.length == 0);
getX().push("a");
assert(x.length == 1); // should hold but knowledge is erased due to pushing a reference
assert(x.length == 0); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (168-189): CHC: Assertion violation happens here.
// Warning 6328: (259-280): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol
View File

@ -17,4 +17,5 @@ contract C {
// SMTEngine: all // SMTEngine: all
// SMTIgnoreCex: yes // SMTIgnoreCex: yes
// ---- // ----
// Warning 6368: (159-169): CHC: Out of bounds access happens here.
// Warning 6328: (152-181): CHC: Assertion violation happens here. // Warning 6328: (152-181): CHC: Assertion violation happens here.