Merge pull request #3647 from leonardoalt/smt_bool

[SMTChecker] Support to Bool variables
This commit is contained in:
chriseth 2018-03-13 09:35:31 +01:00 committed by GitHub
commit f2614be95f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 318 additions and 36 deletions

View File

@ -205,7 +205,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
_assignment.location(),
"Assertion checker does not yet implement compound assignment."
);
else if (_assignment.annotation().type->category() != Type::Category::Integer)
else if (!SSAVariable::isSupportedType(_assignment.annotation().type->category()))
m_errorReporter.warning(
_assignment.location(),
"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
@ -266,14 +266,15 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
{
case Token::Not: // !
{
solAssert(_op.annotation().type->category() == Type::Category::Bool, "");
solAssert(SSAVariable::isBool(_op.annotation().type->category()), "");
defineExpr(_op, !expr(_op.subExpression()));
break;
}
case Token::Inc: // ++ (pre- or postfix)
case Token::Dec: // -- (pre- or postfix)
{
solAssert(_op.annotation().type->category() == Type::Category::Integer, "");
solAssert(SSAVariable::isInteger(_op.annotation().type->category()), "");
solAssert(_op.subExpression().annotation().lValueRequested, "");
if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
{
@ -370,7 +371,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{
// Will be translated as part of the node that requested the lvalue.
}
else if (SSAVariable::supportedType(_identifier.annotation().type.get()))
else if (SSAVariable::isSupportedType(_identifier.annotation().type->category()))
defineExpr(_identifier, currentValue(*decl));
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
@ -444,21 +445,37 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
void SMTChecker::compareOperation(BinaryOperation const& _op)
{
solAssert(_op.annotation().commonType, "");
if (_op.annotation().commonType->category() == Type::Category::Integer)
if (SSAVariable::isSupportedType(_op.annotation().commonType->category()))
{
smt::Expression left(expr(_op.leftExpression()));
smt::Expression right(expr(_op.rightExpression()));
Token::Value op = _op.getOperator();
smt::Expression value = (
op == Token::Equal ? (left == right) :
op == Token::NotEqual ? (left != right) :
op == Token::LessThan ? (left < right) :
op == Token::LessThanOrEqual ? (left <= right) :
op == Token::GreaterThan ? (left > right) :
/*op == Token::GreaterThanOrEqual*/ (left >= right)
);
shared_ptr<smt::Expression> value;
if (SSAVariable::isInteger(_op.annotation().commonType->category()))
{
value = make_shared<smt::Expression>(
op == Token::Equal ? (left == right) :
op == Token::NotEqual ? (left != right) :
op == Token::LessThan ? (left < right) :
op == Token::LessThanOrEqual ? (left <= right) :
op == Token::GreaterThan ? (left > right) :
/*op == Token::GreaterThanOrEqual*/ (left >= right)
);
}
else // Bool
{
solAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "");
value = make_shared<smt::Expression>(
op == Token::Equal ? (left == right) :
op == Token::NotEqual ? (left != right) :
op == Token::LessThan ? (!left && right) :
op == Token::LessThanOrEqual ? (!left || right) :
op == Token::GreaterThan ? (left && !right) :
/*op == Token::GreaterThanOrEqual*/ (left || !right)
);
}
// TODO: check that other values for op are not possible.
defineExpr(_op, value);
defineExpr(_op, *value);
}
else
m_errorReporter.warning(
@ -728,10 +745,10 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm
bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
{
if (SSAVariable::supportedType(_varDecl.type().get()))
if (SSAVariable::isSupportedType(_varDecl.type()->category()))
{
solAssert(m_variables.count(&_varDecl) == 0, "");
m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface));
m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
return true;
}
else

View File

@ -17,6 +17,7 @@
#include <libsolidity/formal/SSAVariable.h>
#include <libsolidity/formal/SymbolicBoolVariable.h>
#include <libsolidity/formal/SymbolicIntVariable.h>
#include <libsolidity/ast/AST.h>
@ -26,23 +27,35 @@ using namespace dev;
using namespace dev::solidity;
SSAVariable::SSAVariable(
Declaration const* _decl,
Declaration const& _decl,
smt::SolverInterface& _interface
)
{
resetIndex();
if (dynamic_cast<IntegerType const*>(_decl->type().get()))
if (isInteger(_decl.type()->category()))
m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
else if (isBool(_decl.type()->category()))
m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface);
else
{
solAssert(false, "");
}
}
bool SSAVariable::supportedType(Type const* _decl)
bool SSAVariable::isSupportedType(Type::Category _category)
{
return dynamic_cast<IntegerType const*>(_decl);
return isInteger(_category) || isBool(_category);
}
bool SSAVariable::isInteger(Type::Category _category)
{
return _category == Type::Category::Integer;
}
bool SSAVariable::isBool(Type::Category _category)
{
return _category == Type::Category::Bool;
}
void SSAVariable::resetIndex()

View File

@ -37,7 +37,7 @@ public:
/// @param _decl Used to determine the type and forwarded to the symbolic var.
/// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver.
SSAVariable(
Declaration const* _decl,
Declaration const& _decl,
smt::SolverInterface& _interface
);
@ -68,8 +68,10 @@ public:
void setZeroValue();
void setUnknownValue();
/// So far Int is supported.
static bool supportedType(Type const* _decl);
/// So far Int and Bool are supported.
static bool isSupportedType(Type::Category _category);
static bool isInteger(Type::Category _category);
static bool isBool(Type::Category _category);
private:
smt::Expression valueAtSequence(int _seq) const

View File

@ -46,7 +46,8 @@ enum class Sort
{
Int,
Bool,
IntIntFun // Function of one Int returning a single Int
IntIntFun, // Function of one Int returning a single Int
IntBoolFun // Function of one Int returning a single Bool
};
/// C++ representation of an SMTLIB2 expression.
@ -132,10 +133,22 @@ public:
Expression operator()(Expression _a) const
{
solAssert(
sort == Sort::IntIntFun && arguments.empty(),
arguments.empty(),
"Attempted function application to non-function."
);
return Expression(name, _a, Sort::Int);
switch (sort)
{
case Sort::IntIntFun:
return Expression(name, _a, Sort::Int);
case Sort::IntBoolFun:
return Expression(name, _a, Sort::Bool);
default:
solAssert(
false,
"Attempted function application to invalid type."
);
break;
}
}
std::string const name;
@ -167,9 +180,18 @@ public:
virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
{
solAssert(_domain == Sort::Int && _codomain == Sort::Int, "Function sort not supported.");
solAssert(_domain == Sort::Int, "Function sort not supported.");
// Subclasses should do something here
return Expression(std::move(_name), {}, Sort::IntIntFun);
switch (_codomain)
{
case Sort::Int:
return Expression(std::move(_name), {}, Sort::IntIntFun);
case Sort::Bool:
return Expression(std::move(_name), {}, Sort::IntBoolFun);
default:
solAssert(false, "Function sort not supported.");
break;
}
}
virtual Expression newInteger(std::string _name)
{

View File

@ -0,0 +1,43 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/SymbolicBoolVariable.h>
#include <libsolidity/ast/AST.h>
using namespace std;
using namespace dev;
using namespace dev::solidity;
SymbolicBoolVariable::SymbolicBoolVariable(
Declaration const& _decl,
smt::SolverInterface&_interface
):
SymbolicVariable(_decl, _interface)
{
solAssert(m_declaration.type()->category() == Type::Category::Bool, "");
m_expression = make_shared<smt::Expression>(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Bool));
}
void SymbolicBoolVariable::setZeroValue(int _seq)
{
m_interface.addAssertion(valueAtSequence(_seq) == smt::Expression(false));
}
void SymbolicBoolVariable::setUnknownValue(int)
{
}

View File

@ -0,0 +1,47 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#pragma once
#include <libsolidity/formal/SymbolicVariable.h>
#include <libsolidity/ast/Types.h>
namespace dev
{
namespace solidity
{
/**
* Specialization of SymbolicVariable for Bool
*/
class SymbolicBoolVariable: public SymbolicVariable
{
public:
SymbolicBoolVariable(
Declaration const& _decl,
smt::SolverInterface& _interface
);
/// Sets the var to false.
void setZeroValue(int _seq);
/// Does nothing since the SMT solver already knows the valid values.
void setUnknownValue(int _seq);
};
}
}

View File

@ -24,12 +24,12 @@ using namespace dev;
using namespace dev::solidity;
SymbolicIntVariable::SymbolicIntVariable(
Declaration const* _decl,
Declaration const& _decl,
smt::SolverInterface& _interface
):
SymbolicVariable(_decl, _interface)
{
solAssert(m_declaration->type()->category() == Type::Category::Integer, "");
solAssert(m_declaration.type()->category() == Type::Category::Integer, "");
m_expression = make_shared<smt::Expression>(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Int));
}
@ -40,7 +40,7 @@ void SymbolicIntVariable::setZeroValue(int _seq)
void SymbolicIntVariable::setUnknownValue(int _seq)
{
auto const& intType = dynamic_cast<IntegerType const&>(*m_declaration->type());
auto const& intType = dynamic_cast<IntegerType const&>(*m_declaration.type());
m_interface.addAssertion(valueAtSequence(_seq) >= minValue(intType));
m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(intType));
}

View File

@ -33,7 +33,7 @@ class SymbolicIntVariable: public SymbolicVariable
{
public:
SymbolicIntVariable(
Declaration const* _decl,
Declaration const& _decl,
smt::SolverInterface& _interface
);

View File

@ -24,7 +24,7 @@ using namespace dev;
using namespace dev::solidity;
SymbolicVariable::SymbolicVariable(
Declaration const* _decl,
Declaration const& _decl,
smt::SolverInterface& _interface
):
m_declaration(_decl),
@ -34,7 +34,7 @@ SymbolicVariable::SymbolicVariable(
string SymbolicVariable::uniqueSymbol() const
{
return m_declaration->name() + "_" + to_string(m_declaration->id());
return m_declaration.name() + "_" + to_string(m_declaration.id());
}

View File

@ -37,7 +37,7 @@ class SymbolicVariable
{
public:
SymbolicVariable(
Declaration const* _decl,
Declaration const& _decl,
smt::SolverInterface& _interface
);
@ -60,7 +60,7 @@ protected:
return (*m_expression)(_seq);
}
Declaration const* m_declaration;
Declaration const& m_declaration;
std::shared_ptr<smt::Expression> m_expression = nullptr;
smt::SolverInterface& m_interface;
};

View File

@ -329,6 +329,144 @@ BOOST_AUTO_TEST_CASE(ways_to_merge_variables)
CHECK_WARNING(text, "Assertion violation happens here");
}
BOOST_AUTO_TEST_CASE(bool_simple)
{
string text = R"(
contract C {
function f(bool x) public pure {
assert(x);
}
}
)";
CHECK_WARNING(text, "Assertion violation happens here");
text = R"(
contract C {
function f(bool x, bool y) public pure {
assert(x == y);
}
}
)";
CHECK_WARNING(text, "Assertion violation happens here");
text = R"(
contract C {
function f(bool x, bool y) public pure {
bool z = x || y;
assert(!(x && y) || z);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(bool x) public pure {
if(x) {
assert(x);
} else {
assert(!x);
}
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(bool x) public pure {
bool y = x;
assert(x == y);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(bool x) public pure {
require(x);
bool y;
y = false;
assert(x || y);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(bool x) public pure {
bool y;
assert(x <= y);
}
}
)";
CHECK_WARNING(text, "Assertion violation happens here");
text = R"(
contract C {
function f(bool x) public pure {
bool y;
assert(x >= y);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(bool x) public pure {
require(x);
bool y;
assert(x > y);
assert(y < x);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
}
BOOST_AUTO_TEST_CASE(bool_int_mixed)
{
string text = R"(
contract C {
function f(bool x) public pure {
uint a;
if(x)
a = 1;
assert(!x || a > 0);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(bool x, uint a) public pure {
require(!x || a > 0);
uint b = a;
assert(!x || b > 0);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(bool x, bool y) public pure {
uint a;
if (x) {
if (y) {
a = 0;
} else {
a = 1;
}
} else {
if (y) {
a = 1;
} else {
a = 0;
}
}
bool xor_x_y = (x && !y) || (!x && y);
assert(!xor_x_y || a > 0);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
}
BOOST_AUTO_TEST_CASE(while_loop_simple)
{
// Check that variables are cleared