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

11 files changed, 125 insertions, 41 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 83784ead..d4f94f16 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::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
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index 4f8080ab..3f2a61f1 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -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()
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index d283ad9e..7e2ebc8c 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
 	);
 
@@ -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
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 38d3236e..0bdebb6c 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -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)
 	{
diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp
index e2a5687d..e5c56e46 100644
--- a/libsolidity/formal/SymbolicBoolVariable.cpp
+++ b/libsolidity/formal/SymbolicBoolVariable.cpp
@@ -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));
 }
 
diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h
index bff56ad0..3510b770 100644
--- a/libsolidity/formal/SymbolicBoolVariable.h
+++ b/libsolidity/formal/SymbolicBoolVariable.h
@@ -33,7 +33,7 @@ class SymbolicBoolVariable: public SymbolicVariable
 {
 public:
 	SymbolicBoolVariable(
-		Declaration const* _decl,
+		Declaration const& _decl,
 		smt::SolverInterface& _interface
 	);
 
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 b97fc80e..beb933a4 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -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)