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 #7582 from ethereum/smt_multid_array_assignment

Browse Source 
[SMTChecker] Support assignments to m-d arrays and mappings
This commit is contained in:
Leonardo 2019-11-04 17:37:33 +01:00 committed by GitHub
commit 1eac3d1d83
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
13 changed files with 79 additions and 95 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -5,6 +5,7 @@ Language Features:
Compiler Features:
* Code Generator: Use SELFBALANCE for ``address(this).balance`` if using Istanbul EVM
* SMTChecker: Support assignments to multi-dimensional arrays and mappings.
Bugfixes:

137
libsolidity/formal/SMTEncoder.cpp
View File

@ -774,78 +774,79 @@ void SMTEncoder::arrayAssignment()
void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide)
{
auto const& indexAccess = dynamic_cast<IndexAccess const&>(_expr);
if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess.baseExpression()))
auto toStore = _rightHandSide;
auto indexAccess = dynamic_cast<IndexAccess const*>(&_expr);
solAssert(indexAccess, "");
while (true)
{
auto varDecl = identifierToVariable(*id);
solAssert(varDecl, "");
if (varDecl->hasReferenceOrMappingType())
m_context.resetVariables([&](VariableDeclaration const& _var) {
if (_var == *varDecl)
return false;
// If both are state variables no need to clear knowledge.
if (_var.isStateVariable() && varDecl->isStateVariable())
return false;
TypePointer prefix = _var.type();
TypePointer originalType = typeWithoutPointer(varDecl->type());
while (
prefix->category() == Type::Category::Mapping ||
prefix->category() == Type::Category::Array
)
{
if (*originalType == *typeWithoutPointer(prefix))
return true;
if (prefix->category() == Type::Category::Mapping)
{
auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
solAssert(mapPrefix, "");
prefix = mapPrefix->valueType();
}
else
{
auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
solAssert(arrayPrefix, "");
prefix = arrayPrefix->baseType();
}
}
return false;
});
smt::Expression store = smt::Expression::store(
m_context.variable(*varDecl)->currentValue(),
expr(*indexAccess.indexExpression()),
_rightHandSide
);
m_context.addAssertion(m_context.newValue(*varDecl) == store);
// Update the SMT select value after the assignment,
// necessary for sound models.
defineExpr(indexAccess, smt::Expression::select(
m_context.variable(*varDecl)->currentValue(),
expr(*indexAccess.indexExpression())
));
}
else if (dynamic_cast<IndexAccess const*>(&indexAccess.baseExpression()))
{
auto identifier = dynamic_cast<Identifier const*>(leftmostBase(indexAccess));
if (identifier)
if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess->baseExpression()))
{
auto varDecl = identifierToVariable(*identifier);
m_context.newValue(*varDecl);
}
auto varDecl = identifierToVariable(*id);
solAssert(varDecl, "");
m_errorReporter.warning(
indexAccess.location(),
"Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays."
);
if (varDecl->hasReferenceOrMappingType())
m_context.resetVariables([&](VariableDeclaration const& _var) {
if (_var == *varDecl)
return false;
// If both are state variables no need to clear knowledge.
if (_var.isStateVariable() && varDecl->isStateVariable())
return false;
TypePointer prefix = _var.type();
TypePointer originalType = typeWithoutPointer(varDecl->type());
while (
prefix->category() == Type::Category::Mapping ||
prefix->category() == Type::Category::Array
)
{
if (*originalType == *typeWithoutPointer(prefix))
return true;
if (prefix->category() == Type::Category::Mapping)
{
auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
solAssert(mapPrefix, "");
prefix = mapPrefix->valueType();
}
else
{
auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
solAssert(arrayPrefix, "");
prefix = arrayPrefix->baseType();
}
}
return false;
});
smt::Expression store = smt::Expression::store(
m_context.variable(*varDecl)->currentValue(),
expr(*indexAccess->indexExpression()),
toStore
);
m_context.addAssertion(m_context.newValue(*varDecl) == store);
// Update the SMT select value after the assignment,
// necessary for sound models.
defineExpr(*indexAccess, smt::Expression::select(
m_context.variable(*varDecl)->currentValue(),
expr(*indexAccess->indexExpression())
));
break;
}
else if (auto base = dynamic_cast<IndexAccess const*>(&indexAccess->baseExpression()))
{
toStore = smt::Expression::store(expr(*base), expr(*indexAccess->indexExpression()), toStore);
indexAccess = base;
}
else
{
m_errorReporter.warning(
_expr.location(),
"Assertion checker does not yet implement this expression."
);
break;
}
}
else
m_errorReporter.warning(
_expr.location(),
"Assertion checker does not yet implement this expression."
);
}
void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)

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

@ -11,6 +11,4 @@ contract C
}
}
// ----
// Warning: (90-97): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (115-122): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (130-149): Assertion violation happens here

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

@ -11,6 +11,4 @@ contract C
}
}
// ----
// Warning: (92-102): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (120-130): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (138-160): Assertion violation happens here

4
test/libsolidity/smtCheckerTests/types/array_branches_2d.sol
View File

@ -13,7 +13,3 @@ contract C
}
}
// ----
// Warning: (90-97): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (115-122): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (138-145): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (153-172): Assertion violation happens here

4
test/libsolidity/smtCheckerTests/types/array_branches_3d.sol
View File

@ -13,7 +13,3 @@ contract C
}
}
// ----
// Warning: (92-102): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (120-130): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (146-156): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (164-186): Assertion violation happens here

6
test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol
View File

@ -17,15 +17,15 @@ contract C
// Warning: (124-130): Assertion checker does not yet support this expression.
// Warning: (124-128): Assertion checker does not yet implement type struct C.S memory
// Warning: (124-133): Assertion checker does not yet implement this expression.
// Warning: (124-136): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (124-136): Assertion checker does not yet implement this expression.
// Warning: (154-160): Assertion checker does not yet support this expression.
// Warning: (154-158): Assertion checker does not yet implement type struct C.S memory
// Warning: (154-163): Assertion checker does not yet implement this expression.
// Warning: (154-166): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (154-166): Assertion checker does not yet implement this expression.
// Warning: (182-188): Assertion checker does not yet support this expression.
// Warning: (182-186): Assertion checker does not yet implement type struct C.S memory
// Warning: (182-191): Assertion checker does not yet implement this expression.
// Warning: (182-194): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (182-194): Assertion checker does not yet implement this expression.
// Warning: (209-215): Assertion checker does not yet support this expression.
// Warning: (209-213): Assertion checker does not yet implement type struct C.S memory
// Warning: (209-218): Assertion checker does not yet implement this expression.

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

@ -10,5 +10,3 @@ contract C
}
}
// ----
// Warning: (134-145): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (154-178): Assertion violation happens here

1
test/libsolidity/smtCheckerTests/types/mapping_2d_1_fail.sol
View File

@ -10,5 +10,4 @@ contract C
}
}
// ----
// Warning: (134-145): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (154-178): Assertion violation happens here

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

@ -10,5 +10,3 @@ contract C
}
}
// ----
// Warning: (152-167): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (176-204): Assertion violation happens here

1
test/libsolidity/smtCheckerTests/types/mapping_3d_1_fail.sol
View File

@ -10,5 +10,4 @@ contract C
}
}
// ----
// Warning: (152-167): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (176-204): Assertion violation happens here

6
test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol
View File

@ -19,15 +19,15 @@ contract C
// Warning: (117-120): Assertion checker does not yet support this expression.
// Warning: (117-118): Assertion checker does not yet implement type struct C.S memory
// Warning: (117-123): Assertion checker does not yet implement this expression.
// Warning: (117-126): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (117-126): Assertion checker does not yet implement this expression.
// Warning: (144-147): Assertion checker does not yet support this expression.
// Warning: (144-145): Assertion checker does not yet implement type struct C.S memory
// Warning: (144-150): Assertion checker does not yet implement this expression.
// Warning: (144-153): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (144-153): Assertion checker does not yet implement this expression.
// Warning: (169-172): Assertion checker does not yet support this expression.
// Warning: (169-170): Assertion checker does not yet implement type struct C.S memory
// Warning: (169-175): Assertion checker does not yet implement this expression.
// Warning: (169-178): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (169-178): Assertion checker does not yet implement this expression.
// Warning: (193-196): Assertion checker does not yet support this expression.
// Warning: (193-194): Assertion checker does not yet implement type struct C.S memory
// Warning: (193-199): Assertion checker does not yet implement this expression.

6
test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol
View File

@ -18,15 +18,15 @@ contract C
// Warning: (124-127): Assertion checker does not yet support this expression.
// Warning: (124-125): Assertion checker does not yet implement type struct C.S memory
// Warning: (124-130): Assertion checker does not yet implement this expression.
// Warning: (124-136): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (124-136): Assertion checker does not yet implement this expression.
// Warning: (154-157): Assertion checker does not yet support this expression.
// Warning: (154-155): Assertion checker does not yet implement type struct C.S memory
// Warning: (154-160): Assertion checker does not yet implement this expression.
// Warning: (154-166): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (154-166): Assertion checker does not yet implement this expression.
// Warning: (182-185): Assertion checker does not yet support this expression.
// Warning: (182-183): Assertion checker does not yet implement type struct C.S memory
// Warning: (182-188): Assertion checker does not yet implement this expression.
// Warning: (182-194): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (182-194): Assertion checker does not yet implement this expression.
// Warning: (209-212): Assertion checker does not yet support this expression.
// Warning: (209-210): Assertion checker does not yet implement type struct C.S memory
// Warning: (209-215): Assertion checker does not yet implement this expression.