cerc-io/solidity
11
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 #9881 from ethereum/smt_fixed_bytes_index_access

Browse Source 
[SMTChecker] Support fixed bytes index access
This commit is contained in:
Leonardo
2020-09-25 11:32:56 +02:00
committed by GitHub
parent 5711d664aa df8c6d94e3
commit 57e1b2cb92
10 changed files with 88 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+29 -6
View File
@@ -977,13 +977,36 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
return;
if (_indexAccess.baseExpression().annotation().type->category() == Type::Category::FixedBytes)
if (auto const* type = dynamic_cast<FixedBytesType const*>(_indexAccess.baseExpression().annotation().type))
{
m_errorReporter.warning(
7989_error,
_indexAccess.location(),
"Assertion checker does not yet support index accessing fixed bytes."
);
smtutil::Expression base = expr(_indexAccess.baseExpression());
if (type->numBytes() == 1)
defineExpr(_indexAccess, base);
else
{
auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_indexAccess.baseExpression().annotation().type);
solAssert(!isSigned, "");
solAssert(bvSize >= 16, "");
solAssert(bvSize % 8 == 0, "");
smtutil::Expression idx = expr(*_indexAccess.indexExpression());
auto bvBase = smtutil::Expression::int2bv(base, bvSize);
auto bvShl = smtutil::Expression::int2bv(idx * 8, bvSize);
auto bvShr = smtutil::Expression::int2bv(bvSize - 8, bvSize);
auto result = (bvBase << bvShl) >> bvShr;
auto anyValue = expr(_indexAccess);
m_context.expression(_indexAccess)->increaseIndex();
unsigned numBytes = bvSize / 8;
auto withBound = smtutil::Expression::ite(
idx < numBytes,
smtutil::Expression::bv2int(result, false),
anyValue
);
defineExpr(_indexAccess, withBound);
}
return;
}