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 in abi.decode

Browse Source
This commit is contained in:
Leonardo Alt 2019-11-15 14:48:11 +01:00
parent 79af19db83
commit d818746e0c
20 changed files with 144 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -7,6 +7,7 @@ Compiler Features:
Bugfixes:
* SMTChecker: Fix internal error when using ``abi.decode``.

85
libsolidity/formal/SMTEncoder.cpp
View File

@ -208,17 +208,14 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
solAssert(symbTuple, "");
auto const& components = symbTuple->components();
auto const& declarations = _varDecl.declarations();
if (!components.empty())
{
solAssert(components.size() == declarations.size(), "");
for (unsigned i = 0; i < declarations.size(); ++i)
if (
components.at(i) &&
declarations.at(i) &&
m_context.knownVariable(*declarations.at(i))
)
assignment(*declarations.at(i), components.at(i)->currentValue(declarations.at(i)->type()));
}
solAssert(components.size() == declarations.size(), "");
for (unsigned i = 0; i < declarations.size(); ++i)
if (
components.at(i) &&
declarations.at(i) &&
m_context.knownVariable(*declarations.at(i))
)
assignment(*declarations.at(i), components.at(i)->currentValue(declarations.at(i)->type()));
}
}
else if (m_context.knownVariable(*_varDecl.declarations().front()))
@ -320,24 +317,23 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
{
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
solAssert(symbTuple, "");
if (symbTuple->components().empty())
auto const& symbComponents = symbTuple->components();
auto const& tupleComponents = _tuple.components();
solAssert(symbComponents.size() == _tuple.components().size(), "");
for (unsigned i = 0; i < symbComponents.size(); ++i)
{
vector<shared_ptr<smt::SymbolicVariable>> components;
for (auto const& component: _tuple.components())
if (component)
{
if (auto varDecl = identifierToVariable(*component))
components.push_back(m_context.variable(*varDecl));
else
{
solAssert(m_context.knownExpression(*component), "");
components.push_back(m_context.expression(*component));
}
}
auto sComponent = symbComponents.at(i);
auto tComponent = tupleComponents.at(i);
if (sComponent && tComponent)
{
if (auto varDecl = identifierToVariable(*tComponent))
m_context.addAssertion(sComponent->currentValue() == currentValue(*varDecl));
else
components.push_back(nullptr);
solAssert(components.size() == _tuple.components().size(), "");
symbTuple->setComponents(move(components));
{
solAssert(m_context.knownExpression(*tComponent), "");
m_context.addAssertion(sComponent->currentValue() == expr(*tComponent));
}
}
}
}
else
@ -609,12 +605,22 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
defineExpr(_identifier, m_context.thisAddress());
m_uninterpretedTerms.insert(&_identifier);
}
else if (smt::isSupportedType(_identifier.annotation().type->category()))
// TODO: handle MagicVariableDeclaration here
m_errorReporter.warning(
_identifier.location(),
"Assertion checker does not yet support the type of this variable."
);
else if (
_identifier.annotation().type->category() != Type::Category::Modifier
)
createExpr(_identifier);
}
void SMTEncoder::endVisit(ElementaryTypeNameExpression const& _typeName)
{
auto const& typeType = dynamic_cast<TypeType const&>(*_typeName.annotation().type);
auto result = smt::newSymbolicVariable(
*TypeProvider::uint256(),
typeType.actualType()->toString(false),
m_context
);
solAssert(!result.first && result.second, "");
m_context.createExpression(_typeName, result.second);
}
void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
@ -1503,15 +1509,18 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
{
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
solAssert(symbTuple, "");
if (symbTuple->components().empty())
auto const& symbComponents = symbTuple->components();
solAssert(symbComponents.size() == returnParams.size(), "");
for (unsigned i = 0; i < symbComponents.size(); ++i)
{
vector<shared_ptr<smt::SymbolicVariable>> components;
for (auto param: returnParams)
auto sComponent = symbComponents.at(i);
auto param = returnParams.at(i);
solAssert(param, "");
if (sComponent)
{
solAssert(m_context.knownVariable(*param), "");
components.push_back(m_context.variable(*param));
m_context.addAssertion(sComponent->currentValue() == currentValue(*param));
}
symbTuple->setComponents(move(components));
}
}
else if (returnParams.size() == 1)

2
libsolidity/formal/SMTEncoder.h
View File

@ -27,6 +27,7 @@
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/formal/VariableUsage.h>
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/ASTVisitor.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
@ -82,6 +83,7 @@ protected:
void endVisit(BinaryOperation const& _node) override;
void endVisit(FunctionCall const& _node) override;
void endVisit(Identifier const& _node) override;
void endVisit(ElementaryTypeNameExpression const& _node) override;
void endVisit(Literal const& _node) override;
void endVisit(Return const& _node) override;
bool visit(MemberAccess const& _node) override;

20
libsolidity/formal/SymbolicVariables.cpp
View File

@ -248,12 +248,16 @@ SymbolicTupleVariable::SymbolicTupleVariable(
SymbolicVariable(_type, _type, move(_uniqueName), _context)
{
solAssert(isTuple(m_type->category()), "");
}
void SymbolicTupleVariable::setComponents(vector<shared_ptr<SymbolicVariable>> _components)
{
solAssert(m_components.empty(), "");
auto const& tupleType = dynamic_cast<solidity::TupleType const*>(m_type);
solAssert(_components.size() == tupleType->components().size(), "");
m_components = move(_components);
auto const& tupleType = dynamic_cast<TupleType const&>(*m_type);
auto const& componentsTypes = tupleType.components();
for (unsigned i = 0; i < componentsTypes.size(); ++i)
if (componentsTypes.at(i))
{
string componentName = m_uniqueName + "_component_" + to_string(i);
auto result = smt::newSymbolicVariable(*componentsTypes.at(i), componentName, m_context);
solAssert(result.second, "");
m_components.emplace_back(move(result.second));
}
else
m_components.emplace_back(nullptr);
}

2
libsolidity/formal/SymbolicVariables.h
View File

@ -250,8 +250,6 @@ public:
return m_components;
}
void setComponents(std::vector<std::shared_ptr<SymbolicVariable>> _components);
private:
std::vector<std::shared_ptr<SymbolicVariable>> m_components;
};

2
test/libsolidity/smtCheckerTests/complex/MerkleProof.sol
View File

@ -35,6 +35,8 @@ library MerkleProof {
// ----
// Warning: (755-767): Assertion checker does not yet support this expression.
// Warning: (988-991): Assertion checker does not yet implement type abi
// Warning: (988-1032): Assertion checker does not yet implement this type of function call.
// Warning: (1175-1178): Assertion checker does not yet implement type abi
// Warning: (1175-1219): Assertion checker does not yet implement this type of function call.
// Warning: (755-767): Assertion checker does not yet support this expression.

2
test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
View File

@ -83,7 +83,7 @@ contract InternalCall {
// Warning: (1144-1206): Function state mutability can be restricted to pure
// Warning: (1212-1274): Function state mutability can be restricted to pure
// Warning: (1280-1342): Function state mutability can be restricted to pure
// Warning: (771-774): Assertion checker does not yet implement type abi
// Warning: (782-813): Type conversion is not yet fully supported and might yield false positives.
// Warning: (771-814): Assertion checker does not yet implement this type of function call.
// Warning: (825-830): Assertion checker does not yet support the type of this variable.
// Warning: (1403-1408): Assertion checker does not yet implement this type of function call.

1
test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol
View File

@ -9,5 +9,6 @@ contract C {
// ----
// Warning: (133-143): Unused local variable.
// Warning: (133-143): Assertion checker does not yet support the type of this variable.
// Warning: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer)
// Warning: (146-163): Assertion checker does not yet implement type struct C.A memory
// Warning: (146-163): Assertion checker does not yet implement this expression.

2
test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol
View File

@ -6,5 +6,7 @@ contract C {
}
// ----
// Warning: (31-64): Experimental features are turned on. Do not use experimental features on live deployments.
// Warning: (162-165): Assertion checker does not yet implement type abi
// Warning: (162-176): Assertion checker does not yet implement this type of function call.
// Warning: (178-181): Assertion checker does not yet implement type abi
// Warning: (178-203): Assertion checker does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/functions/functions_library_1.sol
View File

@ -16,3 +16,5 @@ contract C
assert(y < 10000);
}
}
// ----
// Warning: (228-229): Assertion checker does not yet implement type type(library L)

1
test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol
View File

@ -17,4 +17,5 @@ contract C
}
}
// ----
// Warning: (228-229): Assertion checker does not yet implement type type(library L)
// Warning: (245-261): Assertion violation happens here

15
test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol Normal file
View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
pragma experimental "ABIEncoderV2";
contract C {
struct S { uint x; uint[] b; }
function f() public pure returns (S memory, bytes memory) {
return abi.decode("abc", (S, bytes));
}
}
// ----
// Warning: (32-67): Experimental features are turned on. Do not use experimental features on live deployments.
// Warning: (151-159): Assertion checker does not yet support the type of this variable.
// Warning: (188-191): Assertion checker does not yet implement type abi
// Warning: (207-208): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning: (188-217): Assertion checker does not yet implement this type of function call.

20
test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
pragma experimental "ABIEncoderV2";
contract C {
function f() public pure {
(uint x1, bool b1) = abi.decode("abc", (uint, bool));
(uint x2, bool b2) = abi.decode("abc", (uint, bool));
// False positive until abi.* are implemented as uninterpreted functions.
assert(x1 == x2);
}
}
// ----
// Warning: (32-67): Experimental features are turned on. Do not use experimental features on live deployments.
// Warning: (125-132): Unused local variable.
// Warning: (183-190): Unused local variable.
// Warning: (136-139): Assertion checker does not yet implement type abi
// Warning: (136-167): Assertion checker does not yet implement this type of function call.
// Warning: (194-197): Assertion checker does not yet implement type abi
// Warning: (194-225): Assertion checker does not yet implement this type of function call.
// Warning: (303-319): Assertion violation happens here

24
test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol Normal file
View File

@ -0,0 +1,24 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
(uint a1, bytes32 b1, C c1) = abi.decode("abc", (uint, bytes32, C));
(uint a2, bytes32 b2, C c2) = abi.decode("abc", (uint, bytes32, C));
// False positive until abi.* are implemented as uninterpreted functions.
assert(a1 == a2);
assert(a1 != a2);
}
}
// ----
// Warning: (88-98): Unused local variable.
// Warning: (100-104): Unused local variable.
// Warning: (161-171): Unused local variable.
// Warning: (173-177): Unused local variable.
// Warning: (108-111): Assertion checker does not yet implement type abi
// Warning: (142-143): Assertion checker does not yet implement type type(contract C)
// Warning: (108-145): Assertion checker does not yet implement this type of function call.
// Warning: (181-184): Assertion checker does not yet implement type abi
// Warning: (215-216): Assertion checker does not yet implement type type(contract C)
// Warning: (181-218): Assertion checker does not yet implement this type of function call.
// Warning: (296-312): Assertion violation happens here
// Warning: (315-331): Assertion violation happens here

1
test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol
View File

@ -10,5 +10,6 @@ contract C
}
}
// ----
// Warning: (132-133): Assertion checker does not yet implement type type(enum C.D)
// Warning: (132-136): Type conversion is not yet fully supported and might yield false positives.
// Warning: (140-160): Assertion violation happens here

3
test/libsolidity/smtCheckerTests/types/address_call.sol
View File

@ -20,3 +20,6 @@ contract C
// ----
// Warning: (224-240): Unused local variable.
// Warning: (260-275): Assertion violation happens here
// Warning: (279-293): Assertion violation happens here
// Warning: (297-316): Assertion violation happens here
// Warning: (320-344): Assertion violation happens here

3
test/libsolidity/smtCheckerTests/types/address_delegatecall.sol
View File

@ -20,3 +20,6 @@ contract C
// ----
// Warning: (224-240): Unused local variable.
// Warning: (268-283): Assertion violation happens here
// Warning: (287-301): Assertion violation happens here
// Warning: (305-324): Assertion violation happens here
// Warning: (328-352): Assertion violation happens here

3
test/libsolidity/smtCheckerTests/types/address_staticcall.sol
View File

@ -20,3 +20,6 @@ contract C
// ----
// Warning: (224-240): Unused local variable.
// Warning: (266-281): Assertion violation happens here
// Warning: (285-299): Assertion violation happens here
// Warning: (303-322): Assertion violation happens here
// Warning: (326-350): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/types/struct_1.sol
View File

@ -17,8 +17,10 @@ contract C
// Warning: (157-170): Unused local variable.
// Warning: (157-170): Assertion checker does not yet support the type of this variable.
// Warning: (139-146): Assertion checker does not yet implement type struct C.S storage ref
// Warning: (149-150): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning: (149-153): Assertion checker does not yet implement type struct C.S memory
// Warning: (149-153): Assertion checker does not yet implement this expression.
// Warning: (139-153): Assertion checker does not yet implement type struct C.S storage ref
// Warning: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning: (173-177): Assertion checker does not yet implement type struct C.S memory
// Warning: (173-177): Assertion checker does not yet implement this expression.

2
test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol
View File

@ -15,9 +15,11 @@ contract C {
}
// ----
// Warning: (112-120): Assertion checker does not yet support the type of this variable.
// Warning: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning: (137-141): Assertion checker does not yet implement type struct C.S memory
// Warning: (137-141): Assertion checker does not yet implement this expression.
// Warning: (193-203): Assertion checker does not yet support the type of this variable.
// Warning: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning: (137-141): Assertion checker does not yet implement type struct C.S memory
// Warning: (137-141): Assertion checker does not yet implement this expression.
// Warning: (227-228): Assertion checker does not yet implement type struct C.S memory