diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 100 |
1 files changed, 82 insertions, 18 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index e5648eb3..db0cec7f 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -363,6 +363,10 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) visitAssert(_funCall); else if (funType.kind() == FunctionType::Kind::Require) visitRequire(_funCall); + else if (funType.kind() == FunctionType::Kind::GasLeft) + visitGasLeft(_funCall); + else if (funType.kind() == FunctionType::Kind::BlockHash) + visitBlockHash(_funCall); else if (funType.kind() == FunctionType::Kind::Internal) inlineFunctionCall(_funCall); else @@ -393,6 +397,22 @@ void SMTChecker::visitRequire(FunctionCall const& _funCall) addPathImpliedExpression(expr(*args[0])); } +void SMTChecker::visitGasLeft(FunctionCall const& _funCall) +{ + string gasLeft = "gasleft"; + // We increase the variable index since gasleft changes + // inside a tx. + defineSpecialVariable(gasLeft, _funCall, true); + m_specialVariables.at(gasLeft)->setUnknownValue(); +} + +void SMTChecker::visitBlockHash(FunctionCall const& _funCall) +{ + string blockHash = "blockhash"; + // TODO Define blockhash as an uninterpreted function + defineSpecialVariable(blockHash, _funCall); +} + void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) { FunctionDefinition const* _funDef = nullptr; @@ -460,7 +480,11 @@ void SMTChecker::endVisit(Identifier const& _identifier) } else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) { - if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require) + if (fun->kind() == FunctionType::Kind::Assert || + fun->kind() == FunctionType::Kind::Require || + fun->kind() == FunctionType::Kind::GasLeft || + fun->kind() == FunctionType::Kind::BlockHash + ) return; createExpr(_identifier); } @@ -468,6 +492,8 @@ void SMTChecker::endVisit(Identifier const& _identifier) { if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration)) defineExpr(_identifier, currentValue(*decl)); + else if (_identifier.name() == "now") + defineSpecialVariable(_identifier.name(), _identifier); else // TODO: handle MagicVariableDeclaration here m_errorReporter.warning( @@ -496,7 +522,7 @@ void SMTChecker::endVisit(Literal const& _literal) void SMTChecker::endVisit(Return const& _return) { - if (hasExpr(*_return.expression())) + if (knownExpr(*_return.expression())) { auto returnParams = m_functionPath.back()->returnParameters(); if (returnParams.size() > 1) @@ -509,6 +535,45 @@ void SMTChecker::endVisit(Return const& _return) } } +bool SMTChecker::visit(MemberAccess const& _memberAccess) +{ + auto const& exprType = _memberAccess.expression().annotation().type; + solAssert(exprType, ""); + if (exprType->category() == Type::Category::Magic) + { + defineSpecialVariable(_memberAccess.memberName(), _memberAccess); + return false; + } + else + m_errorReporter.warning( + _memberAccess.location(), + "Assertion checker does not yet support this expression." + ); + + return true; +} + +void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _expr, bool _increaseIndex) +{ + if (!knownSpecialVariable(_name)) + { + auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); + m_specialVariables.emplace(_name, result.second); + result.second->setUnknownValue(); + if (result.first) + m_errorReporter.warning( + _expr.location(), + "Assertion checker does not yet support this special variable." + ); + } + else if (_increaseIndex) + m_specialVariables.at(_name)->increaseIndex(); + // The default behavior is not to increase the index since + // most of the special values stay the same throughout a tx. + defineExpr(_expr, m_specialVariables.at(_name)->currentValue()); +} + + void SMTChecker::arithmeticOperation(BinaryOperation const& _op) { switch (_op.getOperator()) @@ -681,11 +746,15 @@ void SMTChecker::checkCondition( expressionNames.push_back(_additionalValueName); } for (auto const& var: m_variables) - if (knownVariable(*var.first)) - { - expressionsToEvaluate.emplace_back(currentValue(*var.first)); - expressionNames.push_back(var.first->name()); - } + { + expressionsToEvaluate.emplace_back(currentValue(*var.first)); + expressionNames.push_back(var.first->name()); + } + for (auto const& var: m_specialVariables) + { + expressionsToEvaluate.emplace_back(var.second->currentValue()); + expressionNames.push_back(var.first); + } } smt::CheckResult result; vector<string> values; @@ -910,7 +979,7 @@ void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _varia bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { // This might be the case for multiple calls to the same function. - if (hasVariable(_varDecl)) + if (knownVariable(_varDecl)) return true; auto const& type = _varDecl.type(); solAssert(m_variables.count(&_varDecl) == 0, ""); @@ -927,11 +996,6 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) return true; } -string SMTChecker::uniqueSymbol(Expression const& _expr) -{ - return "expr_" + to_string(_expr.id()); -} - bool SMTChecker::knownVariable(VariableDeclaration const& _decl) { return m_variables.count(&_decl); @@ -969,7 +1033,7 @@ void SMTChecker::setUnknownValue(VariableDeclaration const& _decl) smt::Expression SMTChecker::expr(Expression const& _e) { - if (!hasExpr(_e)) + if (!knownExpr(_e)) { m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." ); createExpr(_e); @@ -977,20 +1041,20 @@ smt::Expression SMTChecker::expr(Expression const& _e) return m_expressions.at(&_e)->currentValue(); } -bool SMTChecker::hasExpr(Expression const& _e) const +bool SMTChecker::knownExpr(Expression const& _e) const { return m_expressions.count(&_e); } -bool SMTChecker::hasVariable(VariableDeclaration const& _var) const +bool SMTChecker::knownSpecialVariable(string const& _var) const { - return m_variables.count(&_var); + return m_specialVariables.count(_var); } void SMTChecker::createExpr(Expression const& _e) { solAssert(_e.annotation().type, ""); - if (hasExpr(_e)) + if (knownExpr(_e)) m_expressions.at(&_e)->increaseIndex(); else { |