[SMTChecker] Support to Bool variables

7 files changed, 205 insertions, 8 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 1da5b291..83784ead 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -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()));
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index 4e6bcbcb..4f8080ab 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>
@@ -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()
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index 275e8590..d283ad9e 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/libsolidity/formal/SSAVariable.h
@@ -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:
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 88487310..38d3236e 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,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)
 	{
diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp
new file mode 100644
index 00000000..e2a5687d
--- /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..bff56ad0
--- /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/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 12b5f439..b97fc80e 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -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