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 #10763 from blishko/smt-abi-fixes

Browse Source 
[SMTChecker] Small fixes in handling ABI functions
This commit is contained in:
Leonardo 2021-01-14 16:00:49 +01:00 committed by GitHub
commit 110e0e1f25
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 44 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/SMTEncoder.cpp
View File

@ -773,7 +773,7 @@ void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
optional<smtutil::Expression> arg;
if (inTypes.size() == 1)
arg = expr(*args.at(0));
arg = expr(*args.at(0), inTypes.at(0));
else
{
auto inputSort = dynamic_cast<smtutil::ArraySort&>(*symbFunction.sort).domain;

17
libsolidity/formal/SymbolicState.cpp
View File

@ -203,15 +203,20 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFuncti
if (t->kind() == FunctionType::Kind::ABIDecode)
{
/// abi.decode : (bytes, tuple_of_types(return_types)) -> (return_types)
solAssert(args.size() == 2, "Unexpected number of arguments for abi.decode");
inTypes.emplace_back(TypeProvider::bytesMemory());
auto const* tupleType = dynamic_cast<TupleType const*>(args.at(1)->annotation().type);
solAssert(tupleType, "");
for (auto t: tupleType->components())
auto argType = args.at(1)->annotation().type;
if (auto const* tupleType = dynamic_cast<TupleType const*>(argType))
for (auto componentType: tupleType->components())
{
auto typeType = dynamic_cast<TypeType const*>(t);
auto typeType = dynamic_cast<TypeType const*>(componentType);
solAssert(typeType, "");
outTypes.emplace_back(typeType->actualType());
}
else if (auto const* typeType = dynamic_cast<TypeType const*>(argType))
outTypes.emplace_back(typeType->actualType());
else
solAssert(false, "Unexpected argument of abi.decode");
}
else
{
@ -264,14 +269,14 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFuncti
/// Otherwise we create a tuple wrapping the necessary input or output types.
auto typesToSort = [](auto const& _types, string const& _name) -> shared_ptr<Sort> {
if (_types.size() == 1)
return smtSort(*_types.front());
return smtSortAbstractFunction(*_types.front());
vector<string> inNames;
vector<SortPointer> sorts;
for (unsigned i = 0; i < _types.size(); ++i)
{
inNames.emplace_back(_name + "_input_" + to_string(i));
sorts.emplace_back(smtSort(*_types.at(i)));
sorts.emplace_back(smtSortAbstractFunction(*_types.at(i)));
}
return make_shared<smtutil::TupleSort>(
_name + "_input",

11
test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
function f(bytes calldata data) external pure returns (uint256[] memory) {
return abi.decode(data, (uint256[]));
}
}
// ----
// Warning 8364: (148-157): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (147-158): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (148-157): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (147-158): Assertion checker does not yet implement type type(uint256[] memory)

9
test/libsolidity/smtCheckerTests/abi/abi_encode_function.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f() public view {
abi.encode(this.f);
}
}
// ----
// Warning 6031: (86-92): Internal error: Expression undefined for SMT solver.
// Warning 6031: (86-92): Internal error: Expression undefined for SMT solver.

9
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal_2.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeStringLiteral(bytes4 sel) public pure {
bytes memory b1 = abi.encodeWithSelector("");
require(sel == "");
bytes memory b2 = abi.encodeWithSelector(sel);
assert(b1.length == b2.length); // should hold
}
}