cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Refactoring how storage and local variables are managed.

Browse Source
This commit is contained in:
Leonardo Alt 2018-06-05 11:46:21 +02:00
parent 8999a2f375
commit 678a769cd7
2 changed files with 29 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
libsolidity/formal/SMTChecker.cpp
View File

@ -68,7 +68,7 @@ bool SMTChecker::visit(ContractDefinition const& _contract)
void SMTChecker::endVisit(ContractDefinition const&) void SMTChecker::endVisit(ContractDefinition const&)
{ {
m_stateVariables.clear(); m_variables.clear();
} }
void SMTChecker::endVisit(VariableDeclaration const& _varDecl) void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
@ -86,12 +86,10 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
); );
m_currentFunction = &_function; m_currentFunction = &_function;
m_interface->reset(); m_interface->reset();
m_variables.clear();
m_variables.insert(m_stateVariables.begin(), m_stateVariables.end());
m_pathConditions.clear(); m_pathConditions.clear();
m_loopExecutionHappened = false; m_loopExecutionHappened = false;
initializeLocalVariables(_function);
resetStateVariables(); resetStateVariables();
initializeLocalVariables(_function);
return true; return true;
} }
@ -100,6 +98,7 @@ void SMTChecker::endVisit(FunctionDefinition const&)
// TOOD we could check for "reachability", i.e. satisfiability here. // TOOD we could check for "reachability", i.e. satisfiability here.
// We only handle local variables, so we clear at the beginning of the 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. // If we add storage variables, those should be cleared differently.
clearLocalVariables();
m_currentFunction = nullptr; m_currentFunction = nullptr;
} }
@ -583,19 +582,7 @@ void SMTChecker::checkCondition(
expressionsToEvaluate.emplace_back(*_additionalValue); expressionsToEvaluate.emplace_back(*_additionalValue);
expressionNames.push_back(_additionalValueName); expressionNames.push_back(_additionalValueName);
} }
for (auto const& param: m_currentFunction->parameters()) for (auto const& var: m_variables)
if (knownVariable(*param))
{
expressionsToEvaluate.emplace_back(currentValue(*param));
expressionNames.push_back(param->name());
}
for (auto const& var: m_currentFunction->localVariables())
if (knownVariable(*var))
{
expressionsToEvaluate.emplace_back(currentValue(*var));
expressionNames.push_back(var->name());
}
for (auto const& var: m_stateVariables)
if (knownVariable(*var.first)) if (knownVariable(*var.first))
{ {
expressionsToEvaluate.emplace_back(currentValue(*var.first)); expressionsToEvaluate.emplace_back(currentValue(*var.first));
@ -740,10 +727,15 @@ void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
void SMTChecker::resetStateVariables() void SMTChecker::resetStateVariables()
{ {
for (auto const& variable: m_stateVariables) for (auto const& variable: m_variables)
{ {
newValue(*variable.first); VariableDeclaration const* _decl = dynamic_cast<VariableDeclaration const*>(variable.first);
setUnknownValue(*variable.first); solAssert(_decl, "");
if (_decl->isStateVariable())
{
newValue(*variable.first);
setUnknownValue(*variable.first);
}
} }
} }
@ -777,14 +769,7 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
if (SSAVariable::isSupportedType(_varDecl.type()->category())) if (SSAVariable::isSupportedType(_varDecl.type()->category()))
{ {
solAssert(m_variables.count(&_varDecl) == 0, ""); solAssert(m_variables.count(&_varDecl) == 0, "");
solAssert(m_stateVariables.count(&_varDecl) == 0, ""); m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
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; return true;
} }
else else
@ -909,3 +894,16 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
{ {
m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e)); m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
} }
void SMTChecker::clearLocalVariables()
{
for (auto it = m_variables.begin(); it != m_variables.end(); )
{
VariableDeclaration const* _decl = dynamic_cast<VariableDeclaration const*>(it->first);
solAssert(_decl, "");
if (_decl->isLocalVariable())
it = m_variables.erase(it);
else
++it;
}
}

4
libsolidity/formal/SMTChecker.h
View File

@ -161,12 +161,14 @@ private:
/// Add to the solver: the given expression implied by the current path conditions /// Add to the solver: the given expression implied by the current path conditions
void addPathImpliedExpression(smt::Expression const& _e); void addPathImpliedExpression(smt::Expression const& _e);
/// Clears the local variables of a function.
void clearLocalVariables();
std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<smt::SolverInterface> m_interface;
std::shared_ptr<VariableUsage> m_variableUsage; std::shared_ptr<VariableUsage> m_variableUsage;
bool m_loopExecutionHappened = false; bool m_loopExecutionHappened = false;
std::map<Expression const*, smt::Expression> m_expressions; std::map<Expression const*, smt::Expression> m_expressions;
std::map<Declaration const*, SSAVariable> m_variables; std::map<Declaration const*, SSAVariable> m_variables;
std::map<Declaration const*, SSAVariable> m_stateVariables;
std::vector<smt::Expression> m_pathConditions; std::vector<smt::Expression> m_pathConditions;
ErrorReporter& m_errorReporter; ErrorReporter& m_errorReporter;