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 #11069 from blishko/smt-array-slice-fix

Browse Source 
[SMTChecker] Use same sort name for array slice as for the underlying array
This commit is contained in:
Leonardo 2021-03-09 16:39:12 +01:00 committed by GitHub
commit 5677df86af
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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

@ -10,8 +10,10 @@ Compiler Features:
Bugfixes:
* 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 pushing to ``string`` casted to ``bytes``.
AST Changes:
### 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;
auto sliceArrayType = dynamic_cast<ArraySliceType const*>(&_type);
ArrayType const* arrayType = sliceArrayType ? &sliceArrayType->arrayType() : dynamic_cast<ArrayType const*>(&_type);
if (
auto arrayType = dynamic_cast<ArrayType const*>(&_type);
(arrayType && (arrayType->isString() || arrayType->isByteArray())) ||
_type.category() == frontend::Type::Category::ArraySlice ||
_type.category() == frontend::Type::Category::StringLiteral
)
tupleName = "bytes";
else if (auto arrayType = dynamic_cast<ArrayType const*>(&_type))
else if (arrayType)
{
auto baseType = arrayType->baseType();
// 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: (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 6328: (644-674): CHC: Assertion violation might happen here.
// Warning 1218: (895-925): CHC: Error trying to invoke SMT solver.
// 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: (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.