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

[SMTChecker] fix handling of assignments of array/mapping state variable accessed using contract name

Browse Source
This commit is contained in:
Martin Blicha
2021-03-12 14:01:07 +01:00
parent 1265b39904
commit 0cb75293f9
2 changed files with 24 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+16 -16
View File
@@ -1498,22 +1498,6 @@ void SMTEncoder::arrayAssignment()
void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
{
if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
{
if (dynamic_cast<ContractDefinition const*>(expressionToDeclaration(memberAccess->expression())))
{
if (auto const* var = dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration))
{
if (var->hasReferenceOrMappingType())
resetReferences(*var);
assignment(*var, _rightHandSide);
defineExpr(_expr, currentValue(*var));
return;
}
}
}
auto toStore = _rightHandSide;
auto const* lastExpr = &_expr;
while (true)
@@ -1556,6 +1540,14 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
);
return;
}
if (auto varDecl = identifierToVariable(*memberAccess))
{
if (varDecl->hasReferenceOrMappingType())
resetReferences(*varDecl);
assignment(*varDecl, toStore);
break;
}
auto symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(base));
solAssert(symbStruct, "");
@@ -2680,6 +2672,14 @@ VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _e
solAssert(m_context.knownVariable(*varDecl), "");
return varDecl;
}
// But we are interested in "contract.var", because that is the same as just "var".
if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
if (dynamic_cast<ContractDefinition const*>(expressionToDeclaration(memberAccess->expression())))
if (auto const* varDecl = dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration))
{
solAssert(m_context.knownVariable(*varDecl), "");
return varDecl;
}
return nullptr;
}