diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 44 |
1 files changed, 40 insertions, 4 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index c4dee22d..425c5c1e 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -58,6 +58,19 @@ void SMTChecker::analyze(SourceUnit const& _source) _source.accept(*this); } +bool SMTChecker::visit(ContractDefinition const& _contract) +{ + for (auto _var : _contract.stateVariables()) + if (_var->type()->isValueType()) + createVariable(*_var); + return true; +} + +void SMTChecker::endVisit(ContractDefinition const&) +{ + m_stateVariables.clear(); +} + void SMTChecker::endVisit(VariableDeclaration const& _varDecl) { if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value()) @@ -72,13 +85,13 @@ bool SMTChecker::visit(FunctionDefinition const& _function) "Assertion checker does not yet support constructors and functions with modifiers." ); m_currentFunction = &_function; - // We only handle local variables, so we clear at the beginning of the function. - // If we add storage variables, those should be cleared differently. m_interface->reset(); m_variables.clear(); + m_variables.insert(m_stateVariables.begin(), m_stateVariables.end()); m_pathConditions.clear(); m_loopExecutionHappened = false; initializeLocalVariables(_function); + resetStateVariables(); return true; } @@ -586,6 +599,12 @@ void SMTChecker::checkCondition( expressionsToEvaluate.emplace_back(currentValue(*var)); expressionNames.push_back(var->name()); } + for (auto const& var: m_stateVariables) + if (knownVariable(*var.first)) + { + expressionsToEvaluate.emplace_back(currentValue(*var.first)); + expressionNames.push_back(var.first->name()); + } } smt::CheckResult result; vector<string> values; @@ -607,7 +626,8 @@ void SMTChecker::checkCondition( message << " for:\n"; solAssert(values.size() == expressionNames.size(), ""); for (size_t i = 0; i < values.size(); ++i) - message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n"; + if (expressionsToEvaluate.at(i).name != values.at(i)) + message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n"; } else message << "."; @@ -722,6 +742,15 @@ void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) setZeroValue(*retParam); } +void SMTChecker::resetStateVariables() +{ + for (auto const& variable: m_stateVariables) + { + newValue(*variable.first); + setUnknownValue(*variable.first); + } +} + void SMTChecker::resetVariables(vector<Declaration const*> _variables) { for (auto const* decl: _variables) @@ -752,7 +781,14 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) if (SSAVariable::isSupportedType(_varDecl.type()->category())) { solAssert(m_variables.count(&_varDecl) == 0, ""); - m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); + solAssert(m_stateVariables.count(&_varDecl) == 0, ""); + if (_varDecl.isLocalVariable()) + m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); + else + { + solAssert(_varDecl.isStateVariable(), ""); + m_stateVariables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); + } return true; } else |