aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2018-03-13 16:35:31 +0800
committerGitHub <noreply@github.com>2018-03-13 16:35:31 +0800
commitf2614be95f71a274db3c172661726dd007e90cf7 (patch)
treee324d1751243949f308d27c372670cf8e0e393f8
parent886dc0512cba2c6bd6198eca88f1e84c55d392e5 (diff)
parent9b64dc501da5c743b948e4dca844a6cd67766be1 (diff)
downloaddexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.tar.gz
dexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.tar.zst
dexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.zip
Merge pull request #3647 from leonardoalt/smt_bool
[SMTChecker] Support to Bool variables
-rw-r--r--libsolidity/formal/SMTChecker.cpp49
-rw-r--r--libsolidity/formal/SSAVariable.cpp21
-rw-r--r--libsolidity/formal/SSAVariable.h8
-rw-r--r--libsolidity/formal/SolverInterface.h32
-rw-r--r--libsolidity/formal/SymbolicBoolVariable.cpp43
-rw-r--r--libsolidity/formal/SymbolicBoolVariable.h47
-rw-r--r--libsolidity/formal/SymbolicIntVariable.cpp6
-rw-r--r--libsolidity/formal/SymbolicIntVariable.h2
-rw-r--r--libsolidity/formal/SymbolicVariable.cpp4
-rw-r--r--libsolidity/formal/SymbolicVariable.h4
-rw-r--r--test/libsolidity/SMTChecker.cpp138
11 files changed, 318 insertions, 36 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 1da5b291..8f4abdc2 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -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
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index 4e6bcbcb..f3213e03 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -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()
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index 275e8590..bf5dae3b 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/libsolidity/formal/SSAVariable.h
@@ -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
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 88487310..0bdebb6c 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -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)
{
diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp
new file mode 100644
index 00000000..e5c56e46
--- /dev/null
+++ b/libsolidity/formal/SymbolicBoolVariable.cpp
@@ -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)
+{
+}
diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h
new file mode 100644
index 00000000..3510b770
--- /dev/null
+++ b/libsolidity/formal/SymbolicBoolVariable.h
@@ -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);
+};
+
+}
+}
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
index d08dc155..eb7b1c17 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -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));
}
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
index afa25f1b..eb36b899 100644
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ b/libsolidity/formal/SymbolicIntVariable.h
@@ -33,7 +33,7 @@ class SymbolicIntVariable: public SymbolicVariable
{
public:
SymbolicIntVariable(
- Declaration const* _decl,
+ Declaration const& _decl,
smt::SolverInterface& _interface
);
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
index 629049ea..d59b55b1 100644
--- a/libsolidity/formal/SymbolicVariable.cpp
+++ b/libsolidity/formal/SymbolicVariable.cpp
@@ -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());
}
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
index 93258250..75eb9fa5 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -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;
};
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 12b5f439..beb933a4 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -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