cerc-io/solidity
16
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

Fix false negative on storage array references returned by internal functions

Browse Source
This commit is contained in:
Leo Alt 2021-08-27 18:53:15 +02:00
parent a3d8da2530
commit 16bc15acac
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:
* 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 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);
else if (auto const* funCall = dynamic_cast<FunctionCall const*>(left))
{
if (
auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type);
funType && funType->kind() == FunctionType::Kind::ArrayPush
)
if (auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type))
{
auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
solAssert(memberAccess, "");
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, "");
if (funType->kind() == FunctionType::Kind::ArrayPush)
{
auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
solAssert(memberAccess, "");
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, "");
auto oldLength = symbArray->length();
auto store = smtutil::Expression::store(
symbArray->elements(),
symbArray->length() - 1,
_right
);
symbArray->increaseIndex();
m_context.addAssertion(symbArray->elements() == store);
m_context.addAssertion(symbArray->length() == oldLength);
assignment(memberAccess->expression(), symbArray->currentValue());
auto oldLength = symbArray->length();
auto store = smtutil::Expression::store(
symbArray->elements(),
symbArray->length() - 1,
_right
);
symbArray->increaseIndex();
m_context.addAssertion(symbArray->elements() == store);
m_context.addAssertion(symbArray->length() == oldLength);
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

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
// SMTIgnoreCex: yes
// ----
// Warning 6368: (159-169): CHC: Out of bounds access happens here.
// Warning 6328: (152-181): CHC: Assertion violation happens here.