diff options
author | chriseth <chris@ethereum.org> | 2018-03-13 16:35:31 +0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-13 16:35:31 +0800 |
commit | f2614be95f71a274db3c172661726dd007e90cf7 (patch) | |
tree | e324d1751243949f308d27c372670cf8e0e393f8 | |
parent | 886dc0512cba2c6bd6198eca88f1e84c55d392e5 (diff) | |
parent | 9b64dc501da5c743b948e4dca844a6cd67766be1 (diff) | |
download | dexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.tar dexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.tar.gz dexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.tar.bz2 dexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.tar.lz dexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.tar.xz 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.cpp | 49 | ||||
-rw-r--r-- | libsolidity/formal/SSAVariable.cpp | 21 | ||||
-rw-r--r-- | libsolidity/formal/SSAVariable.h | 8 | ||||
-rw-r--r-- | libsolidity/formal/SolverInterface.h | 32 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicBoolVariable.cpp | 43 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicBoolVariable.h | 47 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicIntVariable.cpp | 6 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicIntVariable.h | 2 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicVariable.cpp | 4 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicVariable.h | 4 | ||||
-rw-r--r-- | test/libsolidity/SMTChecker.cpp | 138 |
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 |