Merge pull request #11861 from ethereum/smt_value

[SMTChecker] Support `value` in CHC for external function calls

test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol

@@ -0,0 +1,14 @@
+contract C {
+	function g(address payable i) public {
+		require(address(this).balance == 100);
+		i.call{value: 10}("");
+		// Disabled due to Spacer nondeterminism
+		//assert(address(this).balance == 90); // should hold
+		// Disabled due to Spacer nondeterminism
+		//assert(address(this).balance == 100); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (96-117): Return value of low-level calls not used.

test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol

@@ -0,0 +1,15 @@
+contract C {
+	function g(address payable i) public {
+		require(address(this).balance == 100);
+		i.call{value: 0}("");
+		assert(address(this).balance == 100); // should hold
+		assert(address(this).balance == 20); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (96-116): Return value of low-level calls not used.
+// Warning 6328: (120-156): CHC: Assertion violation might happen here.
+// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    i.call{value: 0}("") -- untrusted external call
+// Warning 4661: (120-156): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/call_with_value_3.sol

@@ -0,0 +1,15 @@
+contract C {
+	function g(address payable i) public {
+		require(address(this).balance > 100);
+		i.call{value: 20}("");
+		assert(address(this).balance > 0); // should hold
+		// Disabled due to Spacer nondeterminism
+		//assert(address(this).balance == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (95-116): Return value of low-level calls not used.
+// Warning 6328: (120-153): CHC: Assertion violation might happen here.
+// Warning 4661: (120-153): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol

@@ -0,0 +1,14 @@
+contract C {
+	function g() public {
+		require(address(this).balance == 100);
+		this.h{value: 10}();
+		assert(address(this).balance == 100); // should hold
+		assert(address(this).balance == 90); // should fail
+	}
+
+	function h() external payable {}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (157-192): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol

@@ -0,0 +1,15 @@
+contract C {
+	function g(uint i) public {
+		require(address(this).balance == 100);
+		this.h{value: i}();
+		assert(address(this).balance == 100); // should hold
+		assert(address(this).balance == 90); // should fail
+	}
+
+	function h() external payable {}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (162-197): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_1.sol

@@ -0,0 +1,18 @@
+interface I {
+	function f() external payable;
+}
+
+contract C {
+	function g(I i) public {
+		require(address(this).balance == 100);
+		i.f{value: 10}();
+		assert(address(this).balance == 90); // should hold
+		// Disabled due to Spacer nondeterminism
+		//assert(address(this).balance == 100); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (151-186): CHC: Assertion violation might happen here.
+// Warning 4661: (151-186): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol

@@ -0,0 +1,18 @@
+interface I {
+	function f() external payable;
+}
+
+contract C {
+	function g(I i) public {
+		require(address(this).balance == 100);
+		i.f{value: 0}();
+		assert(address(this).balance == 100); // should hold
+		assert(address(this).balance == 90); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (150-186): CHC: Assertion violation might happen here.
+// Warning 6328: (205-240): CHC: Assertion violation happens here.
+// Warning 4661: (150-186): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol

@@ -0,0 +1,18 @@
+interface I {
+	function f() external payable;
+}
+
+contract C {
+	function g(I i) public {
+		require(address(this).balance > 100);
+		i.f{value: 20}();
+		assert(address(this).balance > 0); // should hold
+		assert(address(this).balance == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (150-183): CHC: Assertion violation might happen here.
+// Warning 6328: (202-236): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    i.f{value: 20}() -- untrusted external call
+// Warning 4661: (150-183): BMC: Assertion violation happens here.