Fix BMCs constraints on internal functions

Changelog.md

@@ -25,6 +25,7 @@ Bugfixes:
  * SMTChecker: Fix false negative caused by ``push`` on storage array references returned by internal functions.
  * SMTChecker: Fix false positive in external calls from constructors.
  * SMTChecker: Fix internal error on some multi-source uses of ``abi.*``, cryptographic functions and constants.
+ * SMTChecker: Fix BMC's constraints regarding internal functions.
  * Type Checker: Disallow modifier declarations and definitions in interfaces.
  * Yul Optimizer: Fix a crash in LoadResolver, when ``keccak256`` has particular non-identifier arguments.
 

libsolidity/formal/BMC.cpp

@@ -188,7 +188,8 @@ bool BMC::visit(FunctionDefinition const& _function)
 	{
 		reset();
 		initFunction(_function);
-		m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function));
+		if (_function.isConstructor() || _function.isPublic())
+			m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function));
 		resetStateVariables();
 	}
 

test/libsolidity/smtCheckerTests/functions/payable_1.sol

@@ -0,0 +1,15 @@
+contract C {
+	function g() external {
+		f();
+	}
+
+	function h() external payable {
+		f();
+	}
+
+	function f() internal {
+		require(msg.value == 0);
+	}
+}
+// ====
+// SMTEngine: all

test/libsolidity/smtCheckerTests/functions/payable_2.sol

@@ -0,0 +1,27 @@
+contract C {
+	function g() external {
+		f();
+		h();
+		i();
+	}
+
+	function g2() external payable {
+		i();
+	}
+
+	function f() internal {
+		require(msg.value == 0);
+	}
+
+	function h() internal {
+		assert(msg.value == 0); // should hold
+	}
+
+	function i() internal {
+		assert(msg.value == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ value: 35 }\n    C.i(){ value: 35 } -- internal call

test/libsolidity/smtCheckerTests/special/block_vars_bmc_internal.sol

@@ -0,0 +1,37 @@
+contract C {
+	address coin;
+	uint dif;
+	uint gas;
+	uint number;
+	uint timestamp;
+	function f() public {
+		coin = block.coinbase;
+		dif = block.difficulty;
+		gas = block.gaslimit;
+		number = block.number;
+		timestamp = block.timestamp;
+
+		g();
+	}
+	function g() internal view {
+		assert(uint160(coin) >= 0); // should hold
+		assert(dif >= 0); // should hold
+		assert(gas >= 0); // should hold
+		assert(number >= 0); // should hold
+		assert(timestamp >= 0); // should hold
+
+		assert(coin == block.coinbase); // should fail with BMC
+		assert(dif == block.difficulty); // should fail with BMC
+		assert(gas == block.gaslimit); // should fail with BMC
+		assert(number == block.number); // should fail with BMC
+		assert(timestamp == block.timestamp); // should fail with BMC
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (473-503): BMC: Assertion violation happens here.
+// Warning 4661: (531-562): BMC: Assertion violation happens here.
+// Warning 4661: (590-619): BMC: Assertion violation happens here.
+// Warning 4661: (647-677): BMC: Assertion violation happens here.
+// Warning 4661: (705-741): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol

@@ -0,0 +1,32 @@
+contract C {
+	address coin;
+	uint dif;
+	uint gas;
+	uint number;
+	uint timestamp;
+	function f() public {
+		coin = block.coinbase;
+		dif = block.difficulty;
+		gas = block.gaslimit;
+		number = block.number;
+		timestamp = block.timestamp;
+
+		g();
+	}
+	function g() internal view {
+		assert(uint160(coin) >= 0); // should hold
+		assert(dif >= 0); // should hold
+		assert(gas >= 0); // should hold
+		assert(number >= 0); // should hold
+		assert(timestamp >= 0); // should hold
+
+		assert(coin == block.coinbase); // should hold with CHC
+		assert(dif == block.difficulty); // should hold with CHC
+		assert(gas == block.gaslimit); // should hold with CHC
+		assert(number == block.number); // should hold with CHC
+		assert(timestamp == block.timestamp); // should hold with CHC
+	}
+}
+// ====
+// SMTEngine: chc
+// ----

test/libsolidity/smtCheckerTests/special/many_internal.sol

@@ -0,0 +1,30 @@
+contract C
+{
+	function f() public payable {
+		g();
+	}
+	function g() internal {
+		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;
+		unchecked { x += 2; }
+		assert(x > block.number);
+		assert(block.timestamp > 10);
+		assert(gasleft() > 100);
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (81-117): CHC: Assertion violation happens here.
+// Warning 6328: (121-163): CHC: Assertion violation happens here.
+// Warning 6328: (167-206): CHC: Assertion violation happens here.
+// Warning 6328: (210-242): CHC: Assertion violation happens here.
+// Warning 6328: (246-277): CHC: Assertion violation happens here.
+// Warning 6328: (330-354): CHC: Assertion violation happens here.
+// Warning 6328: (358-386): CHC: Assertion violation happens here.
+// Warning 6328: (390-413): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/msg_vars_bmc_internal.sol

@@ -0,0 +1,32 @@
+contract C {
+	bytes data;
+	address sender;
+	bytes4 sig;
+	uint value;
+	function f() public payable {
+		data = msg.data;
+		sender = msg.sender;
+		sig = msg.sig;
+		value = msg.value;
+
+		g();
+	}
+	function g() internal view {
+		assert(data.length >= 0); // should hold
+		assert(uint160(sender) >= 0); // should hold
+		assert(uint32(sig) >= 0); // should hold
+		assert(value >= 0); // should hold
+
+		assert(data.length == msg.data.length); // should fail with BMC
+		assert(sender == msg.sender); // should fail with BMC
+		assert(sig == msg.sig); // should fail with BMC
+		assert(value == msg.value); // should fail with BMC
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (394-432): BMC: Assertion violation happens here.
+// Warning 4661: (460-488): BMC: Assertion violation happens here.
+// Warning 4661: (516-538): BMC: Assertion violation happens here.
+// Warning 4661: (566-592): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol

@@ -0,0 +1,28 @@
+contract C {
+	bytes data;
+	address sender;
+	bytes4 sig;
+	uint value;
+	function f() public payable {
+		data = msg.data;
+		sender = msg.sender;
+		sig = msg.sig;
+		value = msg.value;
+
+		g();
+	}
+	function g() internal view {
+		assert(data.length >= 0); // should hold
+		assert(uint160(sender) >= 0); // should hold
+		assert(uint32(sig) >= 0); // should hold
+		assert(value >= 0); // should hold
+
+		assert(data.length == msg.data.length); // should hold with CHC
+		assert(sender == msg.sender); // should hold with CHC
+		assert(sig == msg.sig); // should hold with CHC
+		assert(value == msg.value); // should hold with CHC
+	}
+}
+// ====
+// SMTEngine: chc
+// ----

test/libsolidity/smtCheckerTests/special/tx_vars_bmc_internal.sol

@@ -0,0 +1,22 @@
+contract C {
+	uint gas;
+	address origin;
+	function f() public {
+		gas = tx.gasprice;
+		origin = tx.origin;
+
+		g();
+	}
+	function g() internal view {
+		assert(gas >= 0); // should hold
+		assert(uint160(origin) >= 0); // should hold
+
+		assert(gas == tx.gasprice); // should fail with BMC
+		assert(origin == tx.origin); // should fail with BMC
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (233-259): BMC: Assertion violation happens here.
+// Warning 4661: (287-314): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol

@@ -0,0 +1,20 @@
+contract C {
+	uint gas;
+	address origin;
+	function f() public {
+		gas = tx.gasprice;
+		origin = tx.origin;
+
+		g();
+	}
+	function g() internal view {
+		assert(gas >= 0); // should hold
+		assert(uint160(origin) >= 0); // should hold
+
+		assert(gas == tx.gasprice); // should hold with CHC
+		assert(origin == tx.origin); // should hold with CHC
+	}
+}
+// ====
+// SMTEngine: chc
+// ----