From 8a42e3f87acb121b60c0cd02c890c2008012af5c Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 28 Oct 2019 17:27:39 +0100 Subject: [PATCH] [SMTChecker] Support assignments to m-d arrays and mappings --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 137 +++++++++--------- .../smtCheckerTests/types/array_branch_2d.sol | 2 - .../smtCheckerTests/types/array_branch_3d.sol | 2 - .../types/array_branches_2d.sol | 4 - .../types/array_branches_3d.sol | 4 - .../types/array_struct_array_branches_2d.sol | 6 +- .../smtCheckerTests/types/mapping_2d_1.sol | 2 - .../types/mapping_2d_1_fail.sol | 1 - .../smtCheckerTests/types/mapping_3d_1.sol | 2 - .../types/mapping_3d_1_fail.sol | 1 - .../types/struct_array_branches_2d.sol | 6 +- .../types/struct_array_branches_3d.sol | 6 +- 13 files changed, 79 insertions(+), 95 deletions(-) diff --git a/Changelog.md b/Changelog.md index dfef78edb..82aa335da 100644 --- a/Changelog.md +++ b/Changelog.md @@ -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: diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 8f4b369da..11dfd3f8c 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -774,78 +774,79 @@ void SMTEncoder::arrayAssignment() void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide) { - auto const& indexAccess = dynamic_cast(_expr); - if (auto const& id = dynamic_cast(&indexAccess.baseExpression())) + auto toStore = _rightHandSide; + auto indexAccess = dynamic_cast(&_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(prefix); - solAssert(mapPrefix, ""); - prefix = mapPrefix->valueType(); - } - else - { - auto arrayPrefix = dynamic_cast(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.baseExpression())) - { - auto identifier = dynamic_cast(leftmostBase(indexAccess)); - if (identifier) + if (auto const& id = dynamic_cast(&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(prefix); + solAssert(mapPrefix, ""); + prefix = mapPrefix->valueType(); + } + else + { + auto arrayPrefix = dynamic_cast(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->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) diff --git a/test/libsolidity/smtCheckerTests/types/array_branch_2d.sol b/test/libsolidity/smtCheckerTests/types/array_branch_2d.sol index e08d10060..a68ea8b60 100644 --- a/test/libsolidity/smtCheckerTests/types/array_branch_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_branch_2d.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/types/array_branch_3d.sol b/test/libsolidity/smtCheckerTests/types/array_branch_3d.sol index 4a1c81c42..87eda064c 100644 --- a/test/libsolidity/smtCheckerTests/types/array_branch_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_branch_3d.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/types/array_branches_2d.sol b/test/libsolidity/smtCheckerTests/types/array_branches_2d.sol index 3f5b9d644..79f23ad5e 100644 --- a/test/libsolidity/smtCheckerTests/types/array_branches_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_branches_2d.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/types/array_branches_3d.sol b/test/libsolidity/smtCheckerTests/types/array_branches_3d.sol index 0d502df3d..6ab84ec6a 100644 --- a/test/libsolidity/smtCheckerTests/types/array_branches_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_branches_3d.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol b/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol index 725cecc86..ee92be251 100644 --- a/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/types/mapping_2d_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_2d_1.sol index b6474903a..3afab9550 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_2d_1.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_2d_1.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/types/mapping_2d_1_fail.sol b/test/libsolidity/smtCheckerTests/types/mapping_2d_1_fail.sol index dd4d568ef..6072d3f2e 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_2d_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_2d_1_fail.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/types/mapping_3d_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_3d_1.sol index 6c5f439a7..b2a90c913 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_3d_1.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_3d_1.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/types/mapping_3d_1_fail.sol b/test/libsolidity/smtCheckerTests/types/mapping_3d_1_fail.sol index dfd4ddafc..aed10ca1f 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_3d_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_3d_1_fail.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol index e8fbd3d15..fe5fca87f 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol index 2ba32209e..c91e163ba 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol @@ -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.