[SMTChecker] Support bound function calls

6 files changed, 91 insertions, 0 deletions

diff --git a/Changelog.md b/Changelog.md
index fae28bb7..197419fa 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
  * Code generator: Do not perform redundant double cleanup on unsigned integers when loading from calldata.
  * SMTChecker: Support ``msg``, ``tx`` and ``block`` member variables.
  * SMTChecker: Support ``gasleft()`` and ``blockhash()`` functions.
+ * SMTChecker: Support internal bound function calls.
 
 
 Bugfixes:
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 9a2b9bbf..bbc78c0c 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -457,6 +457,14 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 	else if (_funDef && _funDef->isImplemented())
 	{
 		vector<smt::Expression> funArgs;
+		auto const& funType = dynamic_cast<FunctionType const*>(_calledExpr->annotation().type.get());
+		solAssert(funType, "");
+		if (funType->bound())
+		{
+			auto const& boundFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
+			solAssert(boundFunction, "");
+			funArgs.push_back(expr(boundFunction->expression()));
+		}
 		for (auto arg: _funCall.arguments())
 			funArgs.push_back(expr(*arg));
 		initializeFunctionCallParameters(*_funDef, funArgs);
@@ -548,6 +556,10 @@ void SMTChecker::endVisit(Return const& _return)
 
 bool SMTChecker::visit(MemberAccess const& _memberAccess)
 {
+	auto const& accessType = _memberAccess.annotation().type;
+	if (accessType->category() == Type::Category::Function)
+		return true;
+
 	auto const& exprType = _memberAccess.expression().annotation().type;
 	solAssert(exprType, "");
 	if (exprType->category() == Type::Category::Magic)
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_bound_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_bound_1.sol
new file mode 100644
index 00000000..5e9722de
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_bound_1.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+library L
+{
+	function add(uint x, uint y) internal pure returns (uint) {
+		require(x < 1000);
+		require(y < 1000);
+		return x + y;
+	}
+}
+
+contract C
+{
+	using L for uint;
+	function f(uint x) public pure {
+		uint y = x.add(999);
+		assert(y < 10000);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol
new file mode 100644
index 00000000..99c785d0
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+library L
+{
+	function add(uint x, uint y) internal pure returns (uint) {
+		require(x < 1000);
+		require(y < 1000);
+		return x + y;
+	}
+}
+
+contract C
+{
+	using L for uint;
+	function f(uint x) public pure {
+		uint y = x.add(999);
+		assert(y < 1000);
+	}
+}
+// ----
+// Warning: (261-277): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol
new file mode 100644
index 00000000..2ceb9e60
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+library L
+{
+	function add(uint x, uint y) internal pure returns (uint) {
+		require(x < 1000);
+		require(y < 1000);
+		return x + y;
+	}
+}
+
+contract C
+{
+	function f(uint x) public pure {
+		uint y = L.add(x, 999);
+		assert(y < 10000);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol
new file mode 100644
index 00000000..32419700
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol
@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+library L
+{
+	function add(uint x, uint y) internal pure returns (uint) {
+		require(x < 1000);
+		require(y < 1000);
+		return x + y;
+	}
+}
+
+contract C
+{
+	function f(uint x) public pure {
+		uint y = L.add(x, 999);
+		assert(y < 1000);
+	}
+}
+// ----
+// Warning: (245-261): Assertion violation happens here