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

[SMTChecker] Fix ICE for arrays and mappings of functions.

Browse Source
This commit is contained in:
Leonardo Alt 2019-11-29 18:06:44 +01:00
parent 27097b3eca
commit 5adc2a40b9
7 changed files with 48 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -17,6 +17,7 @@ Build System:
Bugfixes:
* SMTChecker: Fix internal error when using ``abi.decode``.
* SMTChecker: Fix internal error when using arrays or mappings of functions.

11
libsolidity/formal/SymbolicTypes.cpp
View File

@ -63,7 +63,7 @@ SortPointer smtSort(solidity::Type const& _type)
{
auto mapType = dynamic_cast<solidity::MappingType const*>(&_type);
solAssert(mapType, "");
return make_shared<ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
return make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
}
else if (isStringLiteral(_type.category()))
{
@ -77,7 +77,7 @@ SortPointer smtSort(solidity::Type const& _type)
solAssert(isArray(_type.category()), "");
auto arrayType = dynamic_cast<solidity::ArrayType const*>(&_type);
solAssert(arrayType, "");
return make_shared<ArraySort>(make_shared<Sort>(Kind::Int), smtSort(*arrayType->baseType()));
return make_shared<ArraySort>(make_shared<Sort>(Kind::Int), smtSortAbstractFunction(*arrayType->baseType()));
}
}
default:
@ -94,6 +94,13 @@ vector<SortPointer> smtSort(vector<solidity::TypePointer> const& _types)
return sorts;
}
SortPointer smtSortAbstractFunction(solidity::Type const& _type)
{
if (isFunction(_type.category()))
return make_shared<Sort>(Kind::Int);
return smtSort(_type);
}
Kind smtKind(solidity::Type::Category _category)
{
if (isNumber(_category))

3
libsolidity/formal/SymbolicTypes.h
View File

@ -32,6 +32,9 @@ namespace smt
/// Returns the SMT sort that models the Solidity type _type.
SortPointer smtSort(solidity::Type const& _type);
std::vector<SortPointer> smtSort(std::vector<solidity::TypePointer> const& _types);
/// If _type has type Function, abstract it to Integer.
/// Otherwise return smtSort(_type).
SortPointer smtSortAbstractFunction(solidity::Type const& _type);
/// Returns the SMT kind that models the Solidity type type category _category.
Kind smtKind(solidity::Type::Category _category);

5
test/libsolidity/smtCheckerTests/types/data_location_in_function_type.sol Normal file
View File

@ -0,0 +1,5 @@
pragma experimental SMTChecker;
library L {
struct Nested { uint y; }
function c(function(Nested memory) external returns (uint)[] storage) external pure {}
}

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

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
struct Nested { uint y; }
// ensure that we consider array of function pointers as reference type
function b(function(Nested memory) external returns (uint)[] storage) internal pure {}
function c(function(Nested memory) external returns (uint)[] memory) public pure {}
function d(function(Nested memory) external returns (uint)[] calldata) external pure {}
}
// ----

14
test/libsolidity/smtCheckerTests/types/function_type_arrays.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
function(uint) external returns (uint)[] public x;
function(uint) internal returns (uint)[10] y;
function f() view public {
function(uint) returns (uint)[10] memory a;
function(uint) returns (uint)[10] storage b = y;
function(uint) external returns (uint)[] memory c;
c = new function(uint) external returns (uint)[](200);
a; b;
}
}
// ----
// Warning: (361-410): Assertion checker does not yet implement this type of function call.

7
test/libsolidity/smtCheckerTests/types/mapping_and_array_of_functions.sol Normal file
View File

@ -0,0 +1,7 @@
pragma experimental SMTChecker;
contract test {
mapping (address => function() internal returns (uint)) a;
mapping (address => function() external) b;
mapping (address => function() external[]) c;
function() external[] d;
}