Merge pull request #5272 from ethereum/smt_special_vars

[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash

10 files changed, 128 insertions, 17 deletions

diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index c7e60256..195004cb 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -133,23 +133,6 @@ BOOST_AUTO_TEST_CASE(assignment_in_declaration)
 	CHECK_SUCCESS_NO_WARNINGS(text);
 }
 
-BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars)
-{
-	string text = R"(
-		contract C {
-			function g() public pure {}
-			function f() public view {
-				uint a = 3;
-				this.g();
-				assert(a == 3);
-				g();
-				assert(a == 3);
-			}
-		}
-	)";
-	CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call");
-}
-
 BOOST_AUTO_TEST_CASE(branches_merge_variables)
 {
 	// Branch does not touch variable a
diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol
new file mode 100644
index 00000000..d0f263eb
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public payable {
+		assert(blockhash(2) > 0);
+	}
+}
+// ----
+// Warning: (86-98): Assertion checker does not yet support this special variable.
+// Warning: (86-98): Assertion checker does not yet implement this type.
+// Warning: (86-102): Assertion checker does not yet implement the type bytes32 for comparisons
+// Warning: (86-102): Internal error: Expression undefined for SMT solver.
+// Warning: (79-103): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/difficulty.sol b/test/libsolidity/smtCheckerTests/special/difficulty.sol
new file mode 100644
index 00000000..4469d4e5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/difficulty.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint difficulty) public view {
+		assert(block.difficulty == difficulty);
+	}
+}
+// ----
+// Warning: (91-129): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/gasleft.sol b/test/libsolidity/smtCheckerTests/special/gasleft.sol
new file mode 100644
index 00000000..857230fe
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/gasleft.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public view {
+		assert(gasleft() > 0);
+		uint g = gasleft();
+		assert(g < gasleft());
+		assert(g >= gasleft());
+	}
+}
+// ----
+// Warning: (76-97): Assertion violation happens here
+// Warning: (123-144): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/many.sol b/test/libsolidity/smtCheckerTests/special/many.sol
new file mode 100644
index 00000000..40e5d987
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/many.sol
@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public payable {
+		assert(msg.sender == block.coinbase);
+		assert(block.difficulty == block.gaslimit);
+		assert(block.number == block.timestamp);
+		assert(tx.gasprice == msg.value);
+		assert(tx.origin == msg.sender);
+		uint x = block.number;
+		assert(x + 2 > block.number);
+		assert(now > 10);
+		assert(gasleft() > 100);
+	}
+}
+// ----
+// Warning: (79-115): Assertion violation happens here
+// Warning: (119-161): Assertion violation happens here
+// Warning: (165-204): Assertion violation happens here
+// Warning: (208-240): Assertion violation happens here
+// Warning: (244-275): Assertion violation happens here
+// Warning: (311-316): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (336-352): Assertion violation happens here
+// Warning: (356-379): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol
new file mode 100644
index 00000000..7e748f09
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_data.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public payable {
+		assert(msg.data.length > 0);
+	}
+}
+// ----
+// Warning: (86-101): Assertion checker does not yet support this expression.
+// Warning: (86-94): Assertion checker does not yet support this special variable.
+// Warning: (86-94): Assertion checker does not yet implement this type.
+// Warning: (86-101): Internal error: Expression undefined for SMT solver.
+// Warning: (79-106): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol
new file mode 100644
index 00000000..dd2366e2
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public view {
+		address a = msg.sender;
+		address b = msg.sender;
+		assert(a == b);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol
new file mode 100644
index 00000000..ad45d076
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public view {
+		require(msg.sender != address(0));
+		address a = msg.sender;
+		address b = msg.sender;
+		assert(a == b);
+	}
+}
+// ----
+// Warning: (98-108): Assertion checker does not yet implement this expression.
+// Warning: (98-108): Internal error: Expression undefined for SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol
new file mode 100644
index 00000000..9a4eefd5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(address c) public view {
+		address a = msg.sender;
+		address b = msg.sender;
+		assert(a == b);
+		assert(c == msg.sender);
+	}
+}
+// ----
+// Warning: (155-178): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol
new file mode 100644
index 00000000..6f832179
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public payable {
+		assert(msg.sig == 0x00000000);
+	}
+}
+// ----
+// Warning: (86-93): Assertion checker does not yet support this special variable.
+// Warning: (86-93): Assertion checker does not yet implement this type.
+// Warning: (86-107): Assertion checker does not yet implement the type bytes4 for comparisons
+// Warning: (86-107): Internal error: Expression undefined for SMT solver.
+// Warning: (79-108): Assertion violation happens here