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

[SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests.

Browse Source
This commit is contained in:
Leonardo Alt 2018-03-09 16:19:03 +01:00
parent 6a940f0a99
commit c2d26eb6a2
11 changed files with 125 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
libsolidity/formal/SMTChecker.cpp
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::supportedType(_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::typeBool(_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::typeInteger(_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::supportedType(_identifier.annotation().type->category()))
defineExpr(_identifier, currentValue(*decl));
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
@ -444,21 +445,36 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
void SMTChecker::compareOperation(BinaryOperation const& _op)
{
solAssert(_op.annotation().commonType, "");
if (SSAVariable::supportedType(_op.annotation().commonType.get()))
if (SSAVariable::supportedType(_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::typeInteger(_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
{
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 +744,10 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm
bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
{
if (SSAVariable::supportedType(_varDecl.type().get()))
if (SSAVariable::supportedType(_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

21
libsolidity/formal/SSAVariable.cpp
View File

@ -27,15 +27,15 @@ 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 (typeInteger(_decl.type()->category()))
m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
else if (dynamic_cast<BoolType const*>(_decl->type().get()))
else if (typeBool(_decl.type()->category()))
m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface);
else
{
@ -43,10 +43,19 @@ SSAVariable::SSAVariable(
}
}
bool SSAVariable::supportedType(Type const* _decl)
bool SSAVariable::supportedType(Type::Category _category)
{
return dynamic_cast<IntegerType const*>(_decl) ||
dynamic_cast<BoolType const*>(_decl);
return typeInteger(_category) || typeBool(_category);
}
bool SSAVariable::typeInteger(Type::Category _category)
{
return _category == Type::Category::Integer;
}
bool SSAVariable::typeBool(Type::Category _category)
{
return _category == Type::Category::Bool;
}
void SSAVariable::resetIndex()

6
libsolidity/formal/SSAVariable.h
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
);
@ -69,7 +69,9 @@ public:
void setUnknownValue();
/// So far Int and Bool are supported.
static bool supportedType(Type const* _decl);
static bool supportedType(Type::Category _category);
static bool typeInteger(Type::Category _category);
static bool typeBool(Type::Category _category);
private:
smt::Expression valueAtSequence(int _seq) const

29
libsolidity/formal/SolverInterface.h
View File

@ -133,12 +133,22 @@ public:
Expression operator()(Expression _a) const
{
solAssert(
(sort == Sort::IntIntFun || sort == Sort::IntBoolFun) && arguments.empty(),
arguments.empty(),
"Attempted function application to non-function."
);
if (sort == Sort::IntIntFun)
switch (sort)
{
case Sort::IntIntFun:
return Expression(name, _a, Sort::Int);
return Expression(name, _a, Sort::Bool);
case Sort::IntBoolFun:
return Expression(name, _a, Sort::Bool);
default:
solAssert(
false,
"Attempted function application to invalid type."
);
break;
}
}
std::string const name;
@ -170,11 +180,18 @@ public:
virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
{
solAssert(_domain == Sort::Int && (_codomain == Sort::Int || _codomain == Sort::Bool), "Function sort not supported.");
solAssert(_domain == Sort::Int, "Function sort not supported.");
// Subclasses should do something here
if (_codomain == Sort::Int)
switch (_codomain)
{
case Sort::Int:
return Expression(std::move(_name), {}, Sort::IntIntFun);
return Expression(std::move(_name), {}, Sort::IntBoolFun);
case Sort::Bool:
return Expression(std::move(_name), {}, Sort::IntBoolFun);
default:
solAssert(false, "Function sort not supported.");
break;
}
}
virtual Expression newInteger(std::string _name)
{

4
libsolidity/formal/SymbolicBoolVariable.cpp
View File

@ -24,12 +24,12 @@ using namespace dev;
using namespace dev::solidity;
SymbolicBoolVariable::SymbolicBoolVariable(
Declaration const* _decl,
Declaration const& _decl,
smt::SolverInterface&_interface
):
SymbolicVariable(_decl, _interface)
{
solAssert(m_declaration->type()->category() == Type::Category::Bool, "");
solAssert(m_declaration.type()->category() == Type::Category::Bool, "");
m_expression = make_shared<smt::Expression>(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Bool));
}

2
libsolidity/formal/SymbolicBoolVariable.h
View File

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

6
libsolidity/formal/SymbolicIntVariable.cpp
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));
}

2
libsolidity/formal/SymbolicIntVariable.h
View File

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

4
libsolidity/formal/SymbolicVariable.cpp
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());
}

4
libsolidity/formal/SymbolicVariable.h
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;
};

40
test/libsolidity/SMTChecker.cpp
View File

@ -377,6 +377,46 @@ BOOST_AUTO_TEST_CASE(bool_simple)
}
)";
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)