From 762f79f84d793c287a74cbe9dda254d09d9c11dc Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 29 Apr 2019 11:39:24 +0200 Subject: [PATCH] Refactor assignment handling --- libsolidity/formal/SMTChecker.cpp | 122 ++++++++++++++++++------------ libsolidity/formal/SMTChecker.h | 14 ++++ 2 files changed, 89 insertions(+), 47 deletions(-) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 9baab9b54..442dcea65 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -341,15 +341,15 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl) void SMTChecker::endVisit(Assignment const& _assignment) { - static map const compoundToArithmetic{ - {Token::AssignAdd, Token::Add}, - {Token::AssignSub, Token::Sub}, - {Token::AssignMul, Token::Mul}, - {Token::AssignDiv, Token::Div}, - {Token::AssignMod, Token::Mod} + static set const compoundOps{ + Token::AssignAdd, + Token::AssignSub, + Token::AssignMul, + Token::AssignDiv, + Token::AssignMod }; Token op = _assignment.assignmentOperator(); - if (op != Token::Assign && !compoundToArithmetic.count(op)) + if (op != Token::Assign && !compoundOps.count(op)) m_errorReporter.warning( _assignment.location(), "Assertion checker does not yet implement this assignment operator." @@ -359,48 +359,19 @@ void SMTChecker::endVisit(Assignment const& _assignment) _assignment.location(), "Assertion checker does not yet implement type " + _assignment.annotation().type->toString() ); - else if ( - dynamic_cast(&_assignment.leftHandSide()) || - dynamic_cast(&_assignment.leftHandSide()) - ) - { - boost::optional leftHandSide; - VariableDeclaration const* decl = nullptr; - auto identifier = dynamic_cast(&_assignment.leftHandSide()); - if (identifier) - { - decl = dynamic_cast(identifier->annotation().referencedDeclaration); - solAssert(decl, ""); - solAssert(knownVariable(*decl), ""); - leftHandSide = currentValue(*decl); - } - else - leftHandSide = expr(_assignment.leftHandSide()); - - solAssert(leftHandSide, ""); - smt::Expression rightHandSide = - compoundToArithmetic.count(op) ? - arithmeticOperation( - compoundToArithmetic.at(op), - *leftHandSide, - expr(_assignment.rightHandSide()), - _assignment.annotation().type, - _assignment.location() - ) : - expr(_assignment.rightHandSide()) - ; - defineExpr(_assignment, rightHandSide); - - if (identifier) - assignment(*decl, _assignment, _assignment.location()); - else - arrayIndexAssignment(_assignment.leftHandSide(), expr(_assignment)); - } else - m_errorReporter.warning( - _assignment.location(), - "Assertion checker does not yet implement such assignments." + { + auto rightHandSide = compoundOps.count(op) ? + compoundAssignment(_assignment) : + expr(_assignment.rightHandSide()); + defineExpr(_assignment, rightHandSide); + assignment( + _assignment.leftHandSide(), + expr(_assignment), + _assignment.annotation().type, + _assignment.location() ); + } } void SMTChecker::endVisit(TupleExpression const& _tuple) @@ -1237,6 +1208,50 @@ smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _rig return _left / _right; } +void SMTChecker::assignment( + Expression const& _left, + smt::Expression const& _right, + TypePointer const& _type, + langutil::SourceLocation const& _location +) +{ + if (!isSupportedType(_type->category())) + m_errorReporter.warning( + _location, + "Assertion checker does not yet implement type " + _type->toString() + ); + else if (auto varDecl = identifierToVariable(_left)) + assignment(*varDecl, _right, _location); + else if (dynamic_cast(&_left)) + arrayIndexAssignment(_left, _right); + else + m_errorReporter.warning( + _location, + "Assertion checker does not yet implement such assignments." + ); +} + +smt::Expression SMTChecker::compoundAssignment(Assignment const& _assignment) +{ + static map const compoundToArithmetic{ + {Token::AssignAdd, Token::Add}, + {Token::AssignSub, Token::Sub}, + {Token::AssignMul, Token::Mul}, + {Token::AssignDiv, Token::Div}, + {Token::AssignMod, Token::Mod} + }; + Token op = _assignment.assignmentOperator(); + solAssert(compoundToArithmetic.count(op), ""); + auto decl = identifierToVariable(_assignment.leftHandSide()); + return arithmeticOperation( + compoundToArithmetic.at(op), + decl ? currentValue(*decl) : expr(_assignment.leftHandSide()), + expr(_assignment.rightHandSide()), + _assignment.annotation().type, + _assignment.location() + ); +} + void SMTChecker::assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location) { assignment(_variable, expr(_value), _location); @@ -1811,3 +1826,16 @@ set SMTChecker::touchedVariables(ASTNode const& _nod solAssert(!m_functionPath.empty(), ""); return m_variableUsage.touchedVariables(_node, m_functionPath); } + +VariableDeclaration const* SMTChecker::identifierToVariable(Expression const& _expr) +{ + if (auto identifier = dynamic_cast(&_expr)) + { + if (auto decl = dynamic_cast(identifier->annotation().referencedDeclaration)) + { + solAssert(knownVariable(*decl), ""); + return decl; + } + } + return nullptr; +} diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 2f24e78b3..1c21aceeb 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -135,7 +135,18 @@ private: smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type); void assignment(VariableDeclaration const& _variable, Expression const& _value, langutil::SourceLocation const& _location); + /// Handles assignments to variables of different types. void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, langutil::SourceLocation const& _location); + /// Handles assignments between generic expressions. + /// Will also be used for assignments of tuple components. + void assignment( + Expression const& _left, + smt::Expression const& _right, + TypePointer const& _type, + langutil::SourceLocation const& _location + ); + /// Computes the right hand side of a compound assignment. + smt::Expression compoundAssignment(Assignment const& _assignment); /// Maps a variable to an SSA index. using VariableIndices = std::unordered_map; @@ -274,6 +285,9 @@ private: /// @returns variables that are touched in _node's subtree. std::set touchedVariables(ASTNode const& _node); + /// @returns the VariableDeclaration referenced by an Identifier or nullptr. + VariableDeclaration const* identifierToVariable(Expression const& _expr); + std::shared_ptr m_interface; VariableUsage m_variableUsage; bool m_loopExecutionHappened = false;