diff --git a/Changelog.md b/Changelog.md index 7fcc99cbb..a59bf8959 100644 --- a/Changelog.md +++ b/Changelog.md @@ -20,6 +20,7 @@ Bugfixes: * SMTChecker: Fix false positive and false negative on ``push`` as LHS of a compound assignment. * SMTChecker: Fix false positive in contracts that cannot be deployed. * SMTChecker: Fix internal error on public getter returning dynamic data on older EVM versions where these are not available. + * SMTChecker: Fix internal error on try-catch with function call in catch block. AST Changes: diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 17ad9f652..1caf3228a 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -208,22 +208,18 @@ bool BMC::visit(IfStatement const& _node) auto conditionExpr = expr(_node.condition()); // visit true branch auto [indicesEndTrue, trueEndPathCondition] = visitBranch(&_node.trueStatement(), conditionExpr); - auto touchedVars = touchedVariables(_node.trueStatement()); // visit false branch decltype(indicesEndTrue) indicesEndFalse; auto falseEndPathCondition = currentPathConditions() && !conditionExpr; if (_node.falseStatement()) - { std::tie(indicesEndFalse, falseEndPathCondition) = visitBranch(_node.falseStatement(), !conditionExpr); - touchedVars += touchedVariables(*_node.falseStatement()); - } else indicesEndFalse = copyVariableIndices(); // merge the information from branches setPathCondition(trueEndPathCondition || falseEndPathCondition); - mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse); + mergeVariables(expr(_node.condition()), indicesEndTrue, indicesEndFalse); return false; } @@ -258,8 +254,7 @@ bool BMC::visit(Conditional const& _op) bool BMC::visit(WhileStatement const& _node) { auto indicesBeforeLoop = copyVariableIndices(); - auto touchedVars = touchedVariables(_node); - m_context.resetVariables(touchedVars); + m_context.resetVariables(touchedVariables(_node)); decltype(indicesBeforeLoop) indicesAfterLoop; if (_node.isDoWhile()) { @@ -294,7 +289,7 @@ bool BMC::visit(WhileStatement const& _node) if (!_node.isDoWhile()) _node.condition().accept(*this); - mergeVariables(touchedVars, expr(_node.condition()), indicesAfterLoop, copyVariableIndices()); + mergeVariables(expr(_node.condition()), indicesAfterLoop, copyVariableIndices()); m_loopExecutionHappened = true; return false; @@ -344,7 +339,7 @@ bool BMC::visit(ForStatement const& _node) _node.condition()->accept(*this); auto forCondition = _node.condition() ? expr(*_node.condition()) : smtutil::Expression(true); - mergeVariables(touchedVars, forCondition, indicesAfterLoop, copyVariableIndices()); + mergeVariables(forCondition, indicesAfterLoop, copyVariableIndices()); m_loopExecutionHappened = true; return false; @@ -363,20 +358,16 @@ bool BMC::visit(TryStatement const& _tryStatement) auto const& clauses = _tryStatement.clauses(); m_context.addAssertion(clauseId >= 0 && clauseId < clauses.size()); solAssert(clauses[0].get() == _tryStatement.successClause(), "First clause of TryStatement should be the success clause"); - vector> touchedVars; vector> clausesVisitResults; for (size_t i = 0; i < clauses.size(); ++i) - { clausesVisitResults.push_back(visitBranch(clauses[i].get())); - touchedVars.push_back(touchedVariables(*clauses[i])); - } // merge the information from all clauses smtutil::Expression pathCondition = clausesVisitResults.front().second; auto currentIndices = clausesVisitResults[0].first; for (size_t i = 1; i < clauses.size(); ++i) { - mergeVariables(touchedVars[i - 1] + touchedVars[i], clauseId == i, clausesVisitResults[i].first, currentIndices); + mergeVariables(clauseId == i, clausesVisitResults[i].first, currentIndices); currentIndices = copyVariableIndices(); pathCondition = pathCondition || clausesVisitResults[i].second; } diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 82498745d..8d8de5daa 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -600,12 +600,10 @@ bool SMTEncoder::visit(Conditional const& _op) _op.condition().accept(*this); auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition())).first; - auto touchedVars = touchedVariables(_op.trueExpression()); auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition())).first; - touchedVars += touchedVariables(_op.falseExpression()); - mergeVariables(touchedVars, expr(_op.condition()), indicesEndTrue, indicesEndFalse); + mergeVariables(expr(_op.condition()), indicesEndTrue, indicesEndFalse); defineExpr(_op, smtutil::Expression::ite( expr(_op.condition()), @@ -1916,13 +1914,13 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op) if (_op.getOperator() == Token::And) { auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first; - mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); + mergeVariables(!expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression())); } else { auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first; - mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); + mergeVariables(expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression())); } } @@ -2347,38 +2345,20 @@ Type const* SMTEncoder::typeWithoutPointer(Type const* _type) return _type; } -void SMTEncoder::mergeVariables(set const& _variables, smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) +void SMTEncoder::mergeVariables(smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) { - auto cmp = [] (VariableDeclaration const* var1, VariableDeclaration const* var2) { - return var1->id() < var2->id(); - }; - set sortedVars(begin(_variables), end(_variables), cmp); - - /// Knowledge about references is erased if a reference is assigned, - /// so those also need their SSA's merged. - /// This does not cause scope harm since the symbolic variables - /// are kept alive. - for (auto const& var: _indicesEndTrue) + for (auto const& entry: _indicesEndTrue) { - solAssert(_indicesEndFalse.count(var.first), ""); - if ( - _indicesEndFalse.at(var.first) != var.second && - !sortedVars.count(var.first) - ) - sortedVars.insert(var.first); - } - - for (auto const* decl: sortedVars) - { - solAssert(_indicesEndTrue.count(decl) && _indicesEndFalse.count(decl), ""); - auto trueIndex = static_cast(_indicesEndTrue.at(decl)); - auto falseIndex = static_cast(_indicesEndFalse.at(decl)); - solAssert(trueIndex != falseIndex, ""); - m_context.addAssertion(m_context.newValue(*decl) == smtutil::Expression::ite( - _condition, - valueAtIndex(*decl, trueIndex), - valueAtIndex(*decl, falseIndex)) - ); + VariableDeclaration const* var = entry.first; + auto trueIndex = entry.second; + if (_indicesEndFalse.count(var) && _indicesEndFalse.at(var) != trueIndex) + { + m_context.addAssertion(m_context.newValue(*var) == smtutil::Expression::ite( + _condition, + valueAtIndex(*var, trueIndex), + valueAtIndex(*var, _indicesEndFalse.at(var))) + ); + } } } @@ -2555,7 +2535,7 @@ SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices() void SMTEncoder::resetVariableIndices(VariableIndices const& _indices) { for (auto const& var: _indices) - m_context.variable(*var.first)->setIndex(static_cast(var.second)); + m_context.variable(*var.first)->setIndex(var.second); } void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 00236bf2a..ac435c465 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -266,7 +266,7 @@ protected: void expressionToTupleAssignment(std::vector> const& _variables, Expression const& _rhs); /// Maps a variable to an SSA index. - using VariableIndices = std::unordered_map; + using VariableIndices = std::unordered_map; /// Visits the branch given by the statement, pushes and pops the current path conditions. /// @param _condition if present, asserts that this condition is true within the branch. @@ -295,10 +295,9 @@ protected: /// @returns whether _a or a subtype of _a is the same as _b. bool sameTypeOrSubtype(Type const* _a, Type const* _b); - /// Given two different branches and the touched variables, - /// merge the touched variables into after-branch ite variables - /// using the branch condition as guard. - void mergeVariables(std::set const& _variables, smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse); + /// Given the state of the symbolic variables at the end of two different branches, + /// create a merged state using the given branch condition. + void mergeVariables(smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse); /// Tries to create an uninitialized variable and returns true on success. bool createVariable(VariableDeclaration const& _varDecl); diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_call_in_catch_1.sol b/test/libsolidity/smtCheckerTests/try_catch/try_call_in_catch_1.sol new file mode 100644 index 000000000..830db0c45 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_call_in_catch_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function f() public returns (uint) { + try this.f() { + } catch Error(string memory) { + g(); + } + } + function g() public pure returns (address) { + } +} +// ---- +// Warning 6321: (78-82): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_call_in_catch_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_call_in_catch_2.sol new file mode 100644 index 000000000..76b86cf04 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_call_in_catch_2.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; +contract C { + function f() public returns (uint, uint) { + try this.f() { + } catch Error(string memory) { + g(); + } + } + function g() public pure { + int test = 1; + } +} +// ---- +// Warning 6321: (78-82): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. +// Warning 6321: (84-88): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. +// Warning 2072: (199-207): Unused local variable.