From b731957e65a64cf087d050edb0dc4345459b2bcf Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 7 Sep 2021 00:14:28 +0200 Subject: [PATCH] Fix BMCs constraints on internal functions --- Changelog.md | 1 + libsolidity/formal/BMC.cpp | 3 +- .../smtCheckerTests/functions/payable_1.sol | 15 ++++++++ .../smtCheckerTests/functions/payable_2.sol | 27 ++++++++++++++ .../special/block_vars_bmc_internal.sol | 37 +++++++++++++++++++ .../special/block_vars_chc_internal.sol | 32 ++++++++++++++++ .../smtCheckerTests/special/many_internal.sol | 30 +++++++++++++++ .../special/msg_vars_bmc_internal.sol | 32 ++++++++++++++++ .../special/msg_vars_chc_internal.sol | 28 ++++++++++++++ .../special/tx_vars_bmc_internal.sol | 22 +++++++++++ .../special/tx_vars_chc_internal.sol | 20 ++++++++++ 11 files changed, 246 insertions(+), 1 deletion(-) create mode 100644 test/libsolidity/smtCheckerTests/functions/payable_1.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/payable_2.sol create mode 100644 test/libsolidity/smtCheckerTests/special/block_vars_bmc_internal.sol create mode 100644 test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol create mode 100644 test/libsolidity/smtCheckerTests/special/many_internal.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_vars_bmc_internal.sol create mode 100644 test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol create mode 100644 test/libsolidity/smtCheckerTests/special/tx_vars_bmc_internal.sol create mode 100644 test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol diff --git a/Changelog.md b/Changelog.md index bd62be0ce..b4cd2187c 100644 --- a/Changelog.md +++ b/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. diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index dc7547433..24c6a5231 100644 --- a/libsolidity/formal/BMC.cpp +++ b/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(); } diff --git a/test/libsolidity/smtCheckerTests/functions/payable_1.sol b/test/libsolidity/smtCheckerTests/functions/payable_1.sol new file mode 100644 index 000000000..c17691fa5 --- /dev/null +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/functions/payable_2.sol b/test/libsolidity/smtCheckerTests/functions/payable_2.sol new file mode 100644 index 000000000..6411eae62 --- /dev/null +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/special/block_vars_bmc_internal.sol b/test/libsolidity/smtCheckerTests/special/block_vars_bmc_internal.sol new file mode 100644 index 000000000..51a330d8e --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol new file mode 100644 index 000000000..ca4873d67 --- /dev/null +++ b/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 +// ---- diff --git a/test/libsolidity/smtCheckerTests/special/many_internal.sol b/test/libsolidity/smtCheckerTests/special/many_internal.sol new file mode 100644 index 000000000..eb68fd9ac --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/special/msg_vars_bmc_internal.sol b/test/libsolidity/smtCheckerTests/special/msg_vars_bmc_internal.sol new file mode 100644 index 000000000..100284dd7 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol new file mode 100644 index 000000000..e8190ce3a --- /dev/null +++ b/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 +// ---- diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_bmc_internal.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_bmc_internal.sol new file mode 100644 index 000000000..137864a33 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol new file mode 100644 index 000000000..53ce010aa --- /dev/null +++ b/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 +// ----