diff --git a/Changelog.md b/Changelog.md index f602e41d6..6f32ca053 100644 --- a/Changelog.md +++ b/Changelog.md @@ -9,6 +9,7 @@ Bugfixes: * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine. * SMTChecker: Fix internal error on conversion from string literal to byte. * SMTChecker: Fix internal error when using tuples of rational literals inside the conditional operator. + * SMTChecker: Fix internal error when assigning state variable via contract's name. * Code generator: Fix missing creation dependency tracking for abstract contracts. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 7efb78205..d6019eeea 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1061,10 +1061,9 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) auto const& exprType = _memberAccess.expression().annotation().type; solAssert(exprType, ""); - auto identifier = dynamic_cast(&_memberAccess.expression()); if (exprType->category() == Type::Category::Magic) { - if (identifier) + if (auto const* identifier = dynamic_cast(&_memberAccess.expression())) { auto const& name = identifier->name(); solAssert(name == "block" || name == "msg" || name == "tx", ""); @@ -1109,13 +1108,23 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) } else if (exprType->category() == Type::Category::TypeType) { - if (identifier && dynamic_cast(identifier->annotation().referencedDeclaration)) + auto const* decl = expressionToDeclaration(_memberAccess.expression()); + if (dynamic_cast(decl)) { auto enumType = dynamic_cast(accessType); solAssert(enumType, ""); defineExpr(_memberAccess, enumType->memberValue(_memberAccess.memberName())); + + return false; + } + else if (dynamic_cast(decl)) + { + if (auto const* var = dynamic_cast(_memberAccess.annotation().referencedDeclaration)) + { + defineExpr(_memberAccess, currentValue(*var)); + return false; + } } - return false; } else if (exprType->category() == Type::Category::Address) { @@ -1245,6 +1254,23 @@ void SMTEncoder::arrayAssignment() void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide) { + if (auto const* memberAccess = dynamic_cast(&_expr)) + { + if (dynamic_cast(expressionToDeclaration(memberAccess->expression()))) + { + if (auto const* var = dynamic_cast(memberAccess->annotation().referencedDeclaration)) + { + if (var->hasReferenceOrMappingType()) + resetReferences(*var); + + m_context.addAssertion(m_context.newValue(*var) == _rightHandSide); + m_context.expression(_expr)->increaseIndex(); + defineExpr(_expr, currentValue(*var)); + return; + } + } + } + auto toStore = _rightHandSide; auto const* lastExpr = &_expr; while (true) @@ -1306,7 +1332,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre m_context.addAssertion(m_context.newValue(*varDecl) == toStore); m_context.expression(*id)->increaseIndex(); - defineExpr(*id,currentValue(*varDecl)); + defineExpr(*id, currentValue(*varDecl)); break; } else @@ -2287,16 +2313,25 @@ set SMTEncoder::touchedVariables(ASTNode const& _nod return m_variableUsage.touchedVariables(_node, callStack); } +Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr) +{ + if (auto const* identifier = dynamic_cast(&_expr)) + return identifier->annotation().referencedDeclaration; + if (auto const* outerMemberAccess = dynamic_cast(&_expr)) + return outerMemberAccess->annotation().referencedDeclaration; + return nullptr; +} + VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr) { - if (auto identifier = dynamic_cast(&_expr)) - { - if (auto decl = dynamic_cast(identifier->annotation().referencedDeclaration)) + // We do not use `expressionToDeclaration` here because we are not interested in + // struct.field, for example. + if (auto const* identifier = dynamic_cast(&_expr)) + if (auto const* varDecl = dynamic_cast(identifier->annotation().referencedDeclaration)) { - solAssert(m_context.knownVariable(*decl), ""); - return decl; + solAssert(m_context.knownVariable(*varDecl), ""); + return varDecl; } - } return nullptr; } diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index fb563412f..748dcc80b 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -280,7 +280,11 @@ protected: /// @returns variables that are touched in _node's subtree. std::set touchedVariables(ASTNode const& _node); - /// @returns the VariableDeclaration referenced by an Identifier or nullptr. + /// @returns the declaration referenced by _expr, if any, + /// and nullptr otherwise. + Declaration const* expressionToDeclaration(Expression const& _expr); + + /// @returns the VariableDeclaration referenced by an Expression or nullptr. VariableDeclaration const* identifierToVariable(Expression const& _expr); /// Creates symbolic expressions for the returned values diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol new file mode 100644 index 000000000..68b05367f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol @@ -0,0 +1,30 @@ +pragma experimental SMTChecker; +contract A { + int x; + int y; + function a() public { + require(A.x < 100); + A.y = A.x++; + assert(A.y == A.x - 1); + // Fails + assert(A.y == 0); + A.y = ++A.x; + assert(A.y == A.x); + delete A.x; + assert(A.x == 0); + A.y = A.x--; + assert(A.y == A.x + 1); + assert(A.y == 0); + A.y = --A.x; + assert(A.y == A.x); + A.x += 10; + // Fails + assert(A.y == 0); + assert(A.y + 10 == A.x); + A.x -= 10; + assert(A.y == A.x); + } +} +// ---- +// Warning 6328: (160-176): CHC: Assertion violation happens here. +// Warning 6328: (373-389): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol new file mode 100644 index 000000000..124be3f7a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract A { + uint[] a; + function f() public { + A.a.push(2); + assert(A.a[A.a.length - 1] == 2); + A.a.pop(); + // Fails + assert(A.a.length > 0); + assert(A.a.length == 0); + } +} +// ---- +// Warning 6328: (156-178): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol new file mode 100644 index 000000000..3f5243105 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol @@ -0,0 +1,31 @@ +==== Source: AASource ==== +pragma experimental SMTChecker; +import "AASource" as AA; +contract A { + int x; + int y; + function a() public { + require(A.x < 100); + AA.A.y = A.x++; + assert(A.y == AA.A.x - 1); + // Fails + assert(AA.A.y == 0); + A.y = ++AA.A.x; + assert(A.y == A.x); + delete AA.A.x; + assert(A.x == 0); + A.y = A.x--; + assert(AA.A.y == AA.A.x + 1); + A.y = --A.x; + assert(A.y == A.x); + AA.A.x += 10; + // Fails + assert(A.y == 0); + assert(A.y + 10 == A.x); + A.x -= 10; + assert(AA.A.y == A.x); + } +} +// ---- +// Warning 6328: (AASource:191-210): CHC: Assertion violation happens here. +// Warning 6328: (AASource:402-418): CHC: Assertion violation happens here.