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

Merge pull request #9513 from ethereum/smt_fix_fixed_bytes_access

Browse Source 
[SMTChecker] Fix ICE on fixed bytes access
This commit is contained in:
chriseth 2020-07-28 23:24:04 +02:00 committed by GitHub
commit aea75d0f5b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 48 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -7,7 +7,7 @@ Compiler Features:
Bugfixes:
* SMTChecker: Fix internal error on fixed bytes index access.
### 0.7.0 (2020-07-28)

19
libsolidity/formal/SMTEncoder.cpp
View File

@ -923,6 +923,15 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
return;
if (_indexAccess.baseExpression().annotation().type->category() == Type::Category::FixedBytes)
{
m_errorReporter.warning(
7989_error,
_indexAccess.location(),
"Assertion checker does not yet support index accessing fixed bytes."
);
return;
}
shared_ptr<smt::SymbolicVariable> array;
if (auto const* id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
@ -930,16 +939,6 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
auto varDecl = identifierToVariable(*id);
solAssert(varDecl, "");
array = m_context.variable(*varDecl);
if (varDecl->type()->category() == Type::Category::FixedBytes)
{
m_errorReporter.warning(
7989_error,
_indexAccess.location(),
"Assertion checker does not yet support index accessing fixed bytes."
);
return;
}
}
else if (auto const* innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
{

9
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract c {
bytes10[6] data2;
function test() public view returns (bytes10 r2) {
r2 = data2[4][5];
}
}
// ----
// Warning 7989: (123-134): Assertion checker does not yet support index accessing fixed bytes.

11
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
function f(bytes calldata x, uint y) external pure {
x[8][0];
x[8][5%y];
}
}
// ----
// Warning 7989: (101-108): Assertion checker does not yet support index accessing fixed bytes.
// Warning 7989: (112-121): Assertion checker does not yet support index accessing fixed bytes.
// Warning 3046: (117-120): Division by zero happens here

18
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol Normal file
View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
contract C {
bytes16[][] a;
function g() internal view returns (bytes16[] storage) {
return a[2];
}
function h() internal view returns (bytes16) {
return a[2][2];
}
function f() external view {
g()[3][4];
h()[5];
}
}
// ----
// Warning 9118: (238-244): Assertion checker does not yet implement this expression.
// Warning 7989: (238-247): Assertion checker does not yet support index accessing fixed bytes.
// Warning 7989: (251-257): Assertion checker does not yet support index accessing fixed bytes.