Skip to content

[SMTChecker] Support to integer and Bool storage vars #3947

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
May 15, 2018
Merged

[SMTChecker] Support to integer and Bool storage vars #3947

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2dbb35d
[SMTChecker] Support to integer and Bool storage vars
Apr 18, 2018
4117e85
[SMTChecker] Declaring all state vars before any function is visited
Apr 30, 2018
a0b4210
Testing state vars that are declared after functions that use them
May 2, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Changelog.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down
44 changes: 40 additions & 4 deletions libsolidity/formal/SMTChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,19 @@ void SMTChecker::analyze(SourceUnit const& _source)
_source.accept(*this);
}

bool SMTChecker::visit(ContractDefinition const& _contract)
{
for (auto _var : _contract.stateVariables())
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This does not include inherited state variables, so we have to be careful once we add inheritance.

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())
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, I think this was always wrong with variables like var (a, b) = f().

Expand All @@ -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());
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

m_variables is mostly used in a way that works for both local and state vars, that's why I decided to have only one map (instead of this one and another m_stateVariables) and add the state vars to m_variables in the beginning of a function visit

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this can still be refactored a little better, for example having only a single map where the entries know when they have to be reset and how, but we can merge it like that for now.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this can still be refactored a little better, for example having only a single map where the entries know when they have to be reset and how, but we can merge it like that for now.

m_pathConditions.clear();
m_loopExecutionHappened = false;
initializeLocalVariables(_function);
resetStateVariables();
return true;
}

Expand Down Expand Up @@ -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;
Expand All @@ -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";
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This if had to be added so that state variables that are not touched by a function don't appear in a counterexample, since they don't have a model. In that case, the solver returns the name of the SMT variable itself as the model. Right now this happens only for Bool. The reason is that when we set a Bool var to unknown, no constraint is added to the solver, therefore if the function doesn't do anything with this state var, it's just not there. Since integers have constraints for the unknown case, integer state variables will have a model even if they're not used.

So, we should choose one out of the following 3 cases for how counterexamples are shown:

  1. As it is in this PR: unused state integer vars get a model, Bools don't.
  2. Unused Bool state vars should have a model too. This case is probably simple to create, we just have to add the trivial constraint (or var (not var)) in the unknown case.
  3. No unused state vars should have models. This is more complicated and would require changes in the class VariableUsage or something similar

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's fine this way.

}
else
message << ".";
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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));
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we have this distinction in the first place? If we do not add the state variables to m_variables, they are not taken into account when unifying branches.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The distinction is because state vars are visited before functions, so we keep a single copy while visiting all the functions, and add them to m_variables in the beginning of each function

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So, the thing about state vars being visited before functions: has to be done manually

}
return true;
}
else
Expand Down
4 changes: 4 additions & 0 deletions libsolidity/formal/SMTChecker.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,8 @@ class SMTChecker: private ASTConstVisitor
// 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;
Expand Down Expand Up @@ -111,6 +113,7 @@ class SMTChecker: private ASTConstVisitor
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
Expand Down Expand Up @@ -163,6 +166,7 @@ class SMTChecker: private ASTConstVisitor
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;

Expand Down
1 change: 0 additions & 1 deletion libsolidity/formal/VariableUsage.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 &&
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This might not work correctly for tuple assignments, I created an issue for that: #4141

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

True, I wanted to check that after a similar comment from you

varDecl->annotation().type->isValueType()
)
Expand Down
76 changes: 76 additions & 0 deletions test/libsolidity/SMTChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down