[SMTChecker] Support to Bool variables

This commit is contained in:
Leonardo Alt 2018-01-21 13:58:56 +01:00
parent 886dc0512c
commit 6a940f0a99
7 changed files with 205 additions and 8 deletions

View File

@ -444,7 +444,7 @@ 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::supportedType(_op.annotation().commonType.get()))
{
smt::Expression left(expr(_op.leftExpression()));
smt::Expression right(expr(_op.rightExpression()));

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>
@ -34,6 +35,8 @@ SSAVariable::SSAVariable(
if (dynamic_cast<IntegerType const*>(_decl->type().get()))
m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
else if (dynamic_cast<BoolType const*>(_decl->type().get()))
m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface);
else
{
solAssert(false, "");
@ -42,7 +45,8 @@ SSAVariable::SSAVariable(
bool SSAVariable::supportedType(Type const* _decl)
{
return dynamic_cast<IntegerType const*>(_decl);
return dynamic_cast<IntegerType const*>(_decl) ||
dynamic_cast<BoolType const*>(_decl);
}
void SSAVariable::resetIndex()

View File

@ -68,7 +68,7 @@ public:
void setZeroValue();
void setUnknownValue();
/// So far Int is supported.
/// So far Int and Bool are supported.
static bool supportedType(Type const* _decl);
private:

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,12 @@ public:
Expression operator()(Expression _a) const
{
solAssert(
sort == Sort::IntIntFun && arguments.empty(),
(sort == Sort::IntIntFun || sort == Sort::IntBoolFun) && arguments.empty(),
"Attempted function application to non-function."
);
return Expression(name, _a, Sort::Int);
if (sort == Sort::IntIntFun)
return Expression(name, _a, Sort::Int);
return Expression(name, _a, Sort::Bool);
}
std::string const name;
@ -167,9 +170,11 @@ 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 && (_codomain == Sort::Int || _codomain == Sort::Bool), "Function sort not supported.");
// Subclasses should do something here
return Expression(std::move(_name), {}, Sort::IntIntFun);
if (_codomain == Sort::Int)
return Expression(std::move(_name), {}, Sort::IntIntFun);
return Expression(std::move(_name), {}, Sort::IntBoolFun);
}
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

@ -329,6 +329,104 @@ 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);
}
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