Merge pull request #10244 from blishko/this-external-calls

[SMTChecker] Analyzing external calls to `this`

test/libsolidity/smtCheckerTests/functions/this_external_call.sol

@@ -9,9 +9,7 @@ contract C
 	function g(uint y) public {
 		require(y < 1000);
 		this.f(y);
-		// Fails as false positive because CHC does not support `this`.
 		assert(x < 1000);
 	}
 }
 // ----
-// Warning 6328: (227-243): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+    uint a;
+    function f(uint x) public {
+        this.g(x);
+        assert(a == x);
+        assert(a != 42);
+    }
+
+    function g(uint x) public {
+        a = x;
+    }
+}
+// ----
+// Warning 6328: (141-156): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol

@@ -10,9 +10,7 @@ contract C
 	function g(uint y) public {
 		require(y < 1000);
 		uint z = this.f(y);
-		// Fails as false positive because CHC does not support `this`.
 		assert(z < 1000);
 	}
 }
 // ----
-// Warning 6328: (263-279): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_call_sender.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+    address lastCaller;
+
+    constructor() {
+        lastCaller = msg.sender;
+    }
+
+    modifier log {
+        lastCaller = msg.sender;
+        _;
+    }
+
+    function test() log public {
+        assert(lastCaller == msg.sender);
+        this.g();
+        assert(lastCaller == address(this));
+        assert(lastCaller == msg.sender);
+        assert(lastCaller == address(0));
+    }
+
+    function g() log public {
+    }
+}
+// ----
+// Warning 6328: (347-379): CHC: Assertion violation happens here.
+// Warning 6328: (389-421): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_call_tx_origin.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test() view public {
+		require(address(this) != tx.origin);
+		assert(!this.g());
+	}
+
+	function g() view public returns (bool) {
+		return msg.sender == tx.origin;
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint public x;
+
+	function f() public view {
+		uint y = this.x();
+		assert(y == x); // This fails as false positive because of lack of support for external getters.
+	}
+}
+// ----
+// Warning 6328: (114-128): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint) public map;
+
+	function f() public view {
+		uint y = this.map(2);
+		assert(y == map[2]); // This fails as false positive because of lack of support for external getters.
+	}
+}
+// ----
+// Warning 6328: (137-156): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => mapping (uint => uint)) public map;
+
+	function f() public view {
+		uint y = this.map(2, 3);
+		assert(y == map[2][3]); // This fails as false positive because of lack of support for external getters.
+	}
+}
+// ----
+// Warning 6328: (158-180): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_state.sol

@@ -6,7 +6,6 @@ contract C
     function g() public {
 		x = 0;
         this.h();
-		// Fails as false positive because CHC does not support `this`.
 		assert(x == 2);
     }
     function h() public {
@@ -14,4 +13,3 @@ contract C
     }
 }
 // ----
-// Warning 6328: (186-200): CHC: Assertion violation happens here.