[SMTChecker] Inline calls to internal functions

22 files changed, 290 insertions, 7 deletions

diff --git a/test/boostTest.cpp b/test/boostTest.cpp
index d27ba1f6..34eeaec9 100644
--- a/test/boostTest.cpp
+++ b/test/boostTest.cpp
@@ -145,6 +145,13 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] )
 		"yulOptimizerTests",
 		dev::yul::test::YulOptimizerTest::create
 	) > 0, "no Yul Optimizer tests found");
+	if (!dev::test::Options::get().disableSMT)
+		solAssert(registerTests(
+			master,
+			dev::test::Options::get().testPath / "libsolidity",
+			"smtCheckerTests",
+			SyntaxTest::create
+		) > 0, "no SMT checker tests found");
 	if (dev::test::Options::get().disableIPC)
 	{
 		for (auto suite: {
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 1f6f765f..c7e60256 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -137,16 +137,17 @@ BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars)
 {
 	string text = R"(
 		contract C {
-			function f() public {
+			function g() public pure {}
+			function f() public view {
 				uint a = 3;
-				this.f();
+				this.g();
 				assert(a == 3);
-				f();
+				g();
 				assert(a == 3);
 			}
 		}
 	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
+	CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call");
 }
 
 BOOST_AUTO_TEST_CASE(branches_merge_variables)
@@ -569,7 +570,10 @@ BOOST_AUTO_TEST_CASE(constant_condition)
 			}
 		}
 	)";
-	CHECK_WARNING(text, "Condition is always true");
+	CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{
+		"Condition is always true",
+		"Assertion checker does not yet implement this type of function call"
+	}));
 	text = R"(
 		contract C {
 			function f(uint x) public pure {
@@ -577,7 +581,10 @@ BOOST_AUTO_TEST_CASE(constant_condition)
 			}
 		}
 	)";
-	CHECK_WARNING(text, "Condition is always false");
+	CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{
+		"Condition is always false",
+		"Assertion checker does not yet implement this type of function call"
+	}));
 	// a plain literal constant is fine
 	text = R"(
 		contract C {
@@ -586,7 +593,7 @@ BOOST_AUTO_TEST_CASE(constant_condition)
 			}
 		}
 	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
+	CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call");
 }
 
 
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol
new file mode 100644
index 00000000..25a42db6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(42);
+		assert(x > 0);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
new file mode 100644
index 00000000..a70aaf61
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (161-174): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol
new file mode 100644
index 00000000..aff24b03
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return k(x);
+	}
+
+	function k(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(2);
+		assert(x > 0);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
new file mode 100644
index 00000000..9baeb935
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return k(x);
+	}
+
+	function k(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (229-242): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol
new file mode 100644
index 00000000..3793f411
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = (h)(42);
+		assert(x > 0);
+	}
+}
+
+// ----
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol
new file mode 100644
index 00000000..e3c80594
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = (h)(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (163-176): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol
new file mode 100644
index 00000000..d2f8ab1d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function g() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			g();
+		}
+		else
+			assert(a == 0);
+	}
+}
+
+// ----
+// Warning: (111-114): Assertion checker does not support recursive function calls.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
new file mode 100644
index 00000000..d5b83f00
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			g();
+		}
+		else
+			assert(a == 0);
+	}
+	function g() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			f();
+		}
+		else
+			assert(a == 0);
+	}
+}
+// ----
+// Warning: (206-209): Assertion checker does not support recursive function calls.
+// Warning: (111-114): Assertion checker does not support recursive function calls.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol
new file mode 100644
index 00000000..2f7563dd
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		assert(a > 0);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol
new file mode 100644
index 00000000..ad735768
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol
@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(0);
+		assert(a > 0);
+	}
+}
+
+// ----
+// Warning: (144-157): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol
new file mode 100644
index 00000000..2f95d8af
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		f(42);
+		assert(a > 1);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol
new file mode 100644
index 00000000..5d972f96
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		f(0);
+		assert(a > 0);
+	}
+}
+
+// ----
+// Warning: (152-165): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol
new file mode 100644
index 00000000..7693ad81
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); for (;x;) {} }
+}
+// ----
+// Warning: (98-99): For loop condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol
new file mode 100644
index 00000000..ed1ad73a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { for (;x;) {} }
+	function g() public pure { f(true); }
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol
new file mode 100644
index 00000000..364fe8d1
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function f(bool x) public pure { require(x); if (x) {} }
+}
+// ----
+// Warning: (95-96): Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol
new file mode 100644
index 00000000..e76badf2
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { x = true; require(x); }
+}
+// ----
+// Warning: (98-99): Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol
new file mode 100644
index 00000000..5cae940b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); }
+	function g() public pure { f(true); }
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol
new file mode 100644
index 00000000..66396dd8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); while (x) {} }
+}
+// ----
+// Warning: (99-100): While loop condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol
new file mode 100644
index 00000000..5000eeb6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { while (x) {} }
+	function g() public pure { f(true); }
+}
diff --git a/test/tools/isoltest.cpp b/test/tools/isoltest.cpp
index bdc89fb3..1b6fd54a 100644
--- a/test/tools/isoltest.cpp
+++ b/test/tools/isoltest.cpp
@@ -328,6 +328,7 @@ int main(int argc, char *argv[])
 		TestTool::editor = "/usr/bin/editor";
 
 	fs::path testPath;
+	bool disableSMT = false;
 	bool formatted = true;
 	po::options_description options(
 		R"(isoltest, tool for interactively managing test contracts.
@@ -340,6 +341,7 @@ Allowed options)",
 	options.add_options()
 		("help", "Show this help screen.")
 		("testpath", po::value<fs::path>(&testPath), "path to test files")
+		("no-smt", "disable SMT checker")
 		("no-color", "don't use colors")
 		("editor", po::value<string>(&TestTool::editor), "editor for opening contracts");
 
@@ -360,6 +362,9 @@ Allowed options)",
 			formatted = false;
 
 		po::notify(arguments);
+
+		if (arguments.count("no-smt"))
+			disableSMT = true;
 	}
 	catch (std::exception const& _exception)
 	{
@@ -395,6 +400,20 @@ Allowed options)",
 	else
 		return 1;
 
+	if (!disableSMT)
+	{
+		if (auto stats = runTestSuite(
+			"SMT Checker",
+			testPath / "libsolidity",
+			"smtCheckerTests",
+			SyntaxTest::create,
+			formatted
+		))
+			global_stats += *stats;
+		else
+			return 1;
+	}
+
 	cout << endl << "Summary: ";
 	FormattedScope(cout, formatted, {BOLD, global_stats ? GREEN : RED}) <<
 		 global_stats.successCount << "/" << global_stats.testCount;