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

[SMTChecker] Use same sort name for array slice as for the underlying array.

Browse Source
This commit is contained in:
Martin Blicha 2021-03-09 11:02:50 +01:00
parent 1d95f95635
commit 5af01f6896
5 changed files with 30 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -8,8 +8,10 @@ Compiler Features:
Bugfixes: Bugfixes:
* SMTChecker: Fix internal error on ``FixedBytes`` constant initialized with string literal. * SMTChecker: Fix internal error on ``FixedBytes`` constant initialized with string literal.
* SMTChecker: Fix internal error on array slices.
* SMTChecker: Fix internal error on calling public getter on a state variable of type array (possibly nested) of structs. * SMTChecker: Fix internal error on calling public getter on a state variable of type array (possibly nested) of structs.
* SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``. * SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``.
AST Changes: AST Changes:
### 0.8.2 (2021-03-02) ### 0.8.2 (2021-03-02)

6
libsolidity/formal/SymbolicTypes.cpp
View File

@ -93,14 +93,14 @@ SortPointer smtSort(frontend::Type const& _type)
} }
string tupleName; string tupleName;
auto sliceArrayType = dynamic_cast<ArraySliceType const*>(&_type);
ArrayType const* arrayType = sliceArrayType ? &sliceArrayType->arrayType() : dynamic_cast<ArrayType const*>(&_type);
if ( if (
auto arrayType = dynamic_cast<ArrayType const*>(&_type);
(arrayType && (arrayType->isString() || arrayType->isByteArray())) || (arrayType && (arrayType->isString() || arrayType->isByteArray())) ||
_type.category() == frontend::Type::Category::ArraySlice ||
_type.category() == frontend::Type::Category::StringLiteral _type.category() == frontend::Type::Category::StringLiteral
) )
tupleName = "bytes"; tupleName = "bytes";
else if (auto arrayType = dynamic_cast<ArrayType const*>(&_type)) else if (arrayType)
{ {
auto baseType = arrayType->baseType(); auto baseType = arrayType->baseType();
// Solidity allows implicit conversion also when assigning arrays. // Solidity allows implicit conversion also when assigning arrays.

4
test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol
View File

@ -22,10 +22,12 @@ contract C {
} }
// ---- // ----
// Warning 6328: (312-342): CHC: Assertion violation happens here. // Warning 6328: (312-342): CHC: Assertion violation happens here.
// Warning 6328: (548-578): CHC: Assertion violation happens here. // Warning 1218: (548-578): CHC: Error trying to invoke SMT solver.
// Warning 6328: (548-578): CHC: Assertion violation might happen here.
// Warning 1218: (644-674): CHC: Error trying to invoke SMT solver. // Warning 1218: (644-674): CHC: Error trying to invoke SMT solver.
// Warning 6328: (644-674): CHC: Assertion violation might happen here. // Warning 6328: (644-674): CHC: Assertion violation might happen here.
// Warning 1218: (895-925): CHC: Error trying to invoke SMT solver. // Warning 1218: (895-925): CHC: Error trying to invoke SMT solver.
// Warning 6328: (895-925): CHC: Assertion violation might happen here. // Warning 6328: (895-925): CHC: Assertion violation might happen here.
// Warning 4661: (548-578): BMC: Assertion violation happens here.
// Warning 4661: (644-674): BMC: Assertion violation happens here. // Warning 4661: (644-674): BMC: Assertion violation happens here.
// Warning 4661: (895-925): BMC: Assertion violation happens here. // Warning 4661: (895-925): BMC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/operators/slices_2.sol Normal file
View File

@ -0,0 +1,5 @@
pragma experimental SMTChecker;
contract e {
function f(uint[] calldata) internal {}
function h(uint[] calldata c) external { f(c[:]); }
}

17
test/libsolidity/smtCheckerTests/operators/slices_3.sol Normal file
View File

@ -0,0 +1,17 @@
pragma experimental SMTChecker;
contract C {
int[] s;
function f(int[] calldata b, uint256 start, uint256 end) public returns (int) {
s = b[start:end];
uint len = end - start;
assert(len == s.length);
for (uint i = 0; i < len; i++) {
assert(b[start:end][i] == s[i]);
}
return s[0];
}
}
// ----
// Warning 6328: (259-290): CHC: Assertion violation might happen here.
// Warning 4661: (259-290): BMC: Assertion violation happens here.