cerc-io/solidity
11
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 #9426 from ethereum/smt_fix_1_tuple

Browse Source 
[SMTChecker] Fix ICE in 1-tuple chain
This commit is contained in:
chriseth
2020-07-23 15:38:17 +02:00
committed by GitHub
parent 1a4c896775 9d2a0947e9
commit 336fe94422
10 changed files with 68 additions and 21 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+29 -20
View File
@@ -425,17 +425,13 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
solAssert(symbTuple, "");
auto const& symbComponents = symbTuple->components();
auto const* tupleComponents = &_tuple.components();
while (tupleComponents->size() == 1)
{
auto innerTuple = dynamic_pointer_cast<TupleExpression>(tupleComponents->front());
solAssert(innerTuple, "");
tupleComponents = &innerTuple->components();
}
solAssert(symbComponents.size() == tupleComponents->size(), "");
auto const* tuple = dynamic_cast<TupleExpression const*>(innermostTuple(_tuple));
solAssert(tuple, "");
auto const& tupleComponents = tuple->components();
solAssert(symbComponents.size() == tupleComponents.size(), "");
for (unsigned i = 0; i < symbComponents.size(); ++i)
{
auto tComponent = tupleComponents->at(i);
auto tComponent = tupleComponents.at(i);
if (tComponent)
{
if (auto varDecl = identifierToVariable(*tComponent))
@@ -454,8 +450,7 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
/// Parenthesized expressions are also TupleExpression regardless their type.
auto const& components = _tuple.components();
solAssert(components.size() == 1, "");
if (smt::isSupportedType(components.front()->annotation().type->category()))
defineExpr(_tuple, expr(*components.front()));
defineExpr(_tuple, expr(*components.front()));
}
}
@@ -729,11 +724,7 @@ void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
void SMTEncoder::endVisit(Identifier const& _identifier)
{
if (_identifier.annotation().willBeWrittenTo)
{
// Will be translated as part of the node that requested the lvalue.
}
else if (auto decl = identifierToVariable(_identifier))
if (auto decl = identifierToVariable(_identifier))
defineExpr(_identifier, currentValue(*decl));
else if (_identifier.annotation().type->category() == Type::Category::Function)
visitFunctionIdentifier(_identifier);
@@ -1449,10 +1440,14 @@ void SMTEncoder::assignment(
"Tuple assignments should be handled by tupleAssignment."
);
Expression const* left = &_left;
if (auto const* tuple = dynamic_cast<TupleExpression const*>(left))
left = innermostTuple(*tuple);
if (!smt::isSupportedType(_type->category()))
{
// Give it a new index anyway to keep the SSA scheme sound.
if (auto varDecl = identifierToVariable(_left))
if (auto varDecl = identifierToVariable(*left))
m_context.newValue(*varDecl);
m_errorReporter.warning(
@@ -1461,10 +1456,10 @@ void SMTEncoder::assignment(
"Assertion checker does not yet implement type " + _type->toString()
);
}
else if (auto varDecl = identifierToVariable(_left))
else if (auto varDecl = identifierToVariable(*left))
assignment(*varDecl, _right);
else if (dynamic_cast<IndexAccess const*>(&_left))
arrayIndexAssignment(_left, _right);
else if (dynamic_cast<IndexAccess const*>(left))
arrayIndexAssignment(*left, _right);
else
m_errorReporter.warning(
8182_error,
@@ -1901,6 +1896,20 @@ Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
return base;
}
Expression const* SMTEncoder::innermostTuple(TupleExpression const& _tuple)
{
solAssert(!_tuple.isInlineArray(), "");
TupleExpression const* tuple = &_tuple;
Expression const* expr = tuple;
while (tuple && !tuple->isInlineArray() && tuple->components().size() == 1)
{
expr = tuple->components().front().get();
tuple = dynamic_cast<TupleExpression const*>(expr);
}
solAssert(expr, "");
return expr;
}
set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node)
{
vector<CallableDeclaration const*> callStack;
libsolidity/formal/SMTEncoder.h
+3
View File
@@ -54,6 +54,9 @@ public:
/// @returns the leftmost identifier in a multi-d IndexAccess.
static Expression const* leftmostBase(IndexAccess const& _indexAccess);
/// @returns the innermost element in a chain of 1-tuples.
static Expression const* innermostTuple(TupleExpression const& _tuple);
/// @returns the FunctionDefinition of a FunctionCall
/// if possible or nullptr.
static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall);