Merge pull request #3947 from ethereum/smt_storage

[SMTChecker] Support to integer and Bool storage vars
This commit is contained in:
chriseth 2018-05-15 14:54:41 +02:00 committed by GitHub
commit 63861aac4a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 121 additions and 5 deletions

View File

@ -10,6 +10,7 @@ Features:
* Optimizer: Remove unnecessary masking of the result of known short instructions (``ADDRESS``, ``CALLER``, ``ORIGIN`` and ``COINBASE``).
* Parser: Display nicer error messages by showing the actual tokens and not internal names.
* Parser: Use the entire location of the token instead of only its starting position as source location for parser errors.
* SMT Checker: Support state variables of integer and bool type.
* Type Checker: Deprecate the ``years`` unit denomination and raise a warning for it (or an error as experimental 0.5.0 feature).
* Type Checker: Make literals (without explicit type casting) an error for tight packing as experimental 0.5.0 feature.
* Type Checker: Warn about wildcard tuple assignments (this will turn into an error with version 0.5.0).

View File

@ -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

View File

@ -50,6 +50,8 @@ private:
// because the order of expression evaluation is undefined
// TODO: or just force a certain order, but people might have a different idea about that.
virtual bool visit(ContractDefinition const& _node) override;
virtual void endVisit(ContractDefinition const& _node) override;
virtual void endVisit(VariableDeclaration const& _node) override;
virtual bool visit(FunctionDefinition const& _node) override;
virtual void endVisit(FunctionDefinition const& _node) override;
@ -111,6 +113,7 @@ private:
smt::CheckResult checkSatisfiable();
void initializeLocalVariables(FunctionDefinition const& _function);
void resetStateVariables();
void resetVariables(std::vector<Declaration const*> _variables);
/// Given two different branches and the touched variables,
/// merge the touched variables into after-branch ite variables
@ -163,6 +166,7 @@ private:
bool m_loopExecutionHappened = false;
std::map<Expression const*, smt::Expression> m_expressions;
std::map<Declaration const*, SSAVariable> m_variables;
std::map<Declaration const*, SSAVariable> m_stateVariables;
std::vector<smt::Expression> m_pathConditions;
ErrorReporter& m_errorReporter;

View File

@ -33,7 +33,6 @@ VariableUsage::VariableUsage(ASTNode const& _node)
solAssert(declaration, "");
if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
if (
varDecl->isLocalVariable() &&
identifier->annotation().lValueRequested &&
varDecl->annotation().type->isValueType()
)

View File

@ -467,6 +467,82 @@ BOOST_AUTO_TEST_CASE(bool_int_mixed)
CHECK_SUCCESS_NO_WARNINGS(text);
}
BOOST_AUTO_TEST_CASE(storage_value_vars)
{
string text = R"(
contract C
{
address a;
bool b;
uint c;
function f(uint x) public {
if (x == 0)
{
a = 100;
b = true;
}
else
{
a = 200;
b = false;
}
assert(a > 0 && b);
}
}
)";
CHECK_WARNING(text, "Assertion violation happens here");
text = R"(
contract C
{
address a;
bool b;
uint c;
function f() public view {
assert(c > 0);
}
}
)";
CHECK_WARNING(text, "Assertion violation happens here");
text = R"(
contract C
{
function f(uint x) public {
if (x == 0)
{
a = 100;
b = true;
}
else
{
a = 200;
b = false;
}
assert(b == (a < 200));
}
function g() public view {
require(a < 100);
assert(c >= 0);
}
address a;
bool b;
uint c;
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C
{
function f() public view {
assert(c > 0);
}
uint c;
}
)";
CHECK_WARNING(text, "Assertion violation happens here");
}
BOOST_AUTO_TEST_CASE(while_loop_simple)
{
// Check that variables are cleared