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 #11905 from ethereum/smt_cleanup_typetype

Browse Source 
[SMTChecker] Cleanup spurious messages about TypeTypes
This commit is contained in:
Leonardo 2021-09-07 17:46:57 +02:00 committed by GitHub
commit 6feed460cf
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 38 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
libsolidity/formal/SMTEncoder.cpp
View File

@ -560,6 +560,24 @@ bool SMTEncoder::visit(Conditional const& _op)
return false;
}
bool SMTEncoder::visit(FunctionCall const& _funCall)
{
auto functionCallKind = *_funCall.annotation().kind;
if (functionCallKind != FunctionCallKind::FunctionCall)
return true;
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
// We do not want to visit the TypeTypes in the second argument of `abi.decode`.
// Those types are checked/used in SymbolicState::buildABIFunctions.
if (funType.kind() == FunctionType::Kind::ABIDecode)
{
if (auto arg = _funCall.arguments().front())
arg->accept(*this);
return false;
}
return true;
}
void SMTEncoder::endVisit(FunctionCall const& _funCall)
{
auto functionCallKind = *_funCall.annotation().kind;

1
libsolidity/formal/SMTEncoder.h
View File

@ -152,6 +152,7 @@ protected:
bool visit(BinaryOperation const& _node) override;
void endVisit(BinaryOperation const& _node) override;
bool visit(Conditional const& _node) override;
bool visit(FunctionCall const& _node) override;
void endVisit(FunctionCall const& _node) override;
bool visit(ModifierInvocation const& _node) override;
void endVisit(Identifier const& _node) override;

2
test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol
View File

@ -6,5 +6,3 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 8364: (116-125): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (115-126): Assertion checker does not yet implement type type(uint256[] memory)

14
test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol
View File

@ -32,20 +32,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (283-289): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (291-297): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (532-538): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (540-546): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (548-554): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (769-775): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (769-777): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (779-785): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (779-787): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 1218: (1009-1037): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1056-1084): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1103-1131): CHC: Error trying to invoke SMT solver.

3
test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol
View File

@ -9,6 +9,3 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 8364: (183-189): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (183-192): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
// Warning 8364: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer)

2
test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
View File

@ -13,6 +13,4 @@ contract C {
// Warning 2072: (82-86): Unused local variable.
// Warning 2072: (140-150): Unused local variable.
// Warning 2072: (152-156): Unused local variable.
// Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)
// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\na1 = 2437\nb1 = 10\nc1 = 9\na2 = 2437\nb2 = 10\nc2 = 9\n\nTransaction trace:\nC.constructor()\nC.f(data)

10
test/libsolidity/smtCheckerTests/types/abi_type_type_1.sol Normal file
View File

@ -0,0 +1,10 @@
contract C {
function f(bytes memory d) public pure {
(bool a, uint x) = abi.decode(d, (bool, uint));
assert(a == (x == 2)); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (107-128): CHC: Assertion violation happens here.\nCounterexample:\n\na = true\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(d)

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

@ -0,0 +1,9 @@
contract C {
function f(bytes memory d) public pure {
assert(abi.decode(d, (bool))); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (57-86): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(d)